## Stream: Coq users

### Topic: pairs and lists

#### Adrián García (Sep 16 2021 at 00:38):

Considering these definitions (where Formula is an usual modal logic formula):

``````Definition LabelledHyp : Type := (nat * Formula)%type.
Definition LCtx : Type := slist LabelledHyp.
``````

I'm able to define an Inductive like this:

``````Inductive DC_Proof : LCtx -> LCtx -> Formula -> Prop :=
| dc_thyp : forall (D: LCtx) (G G': LCtx) (n : nat) (A: Formula),
DC_Proof D ((G,(pair n A));G') A
``````

but is it possible to define it with LabelledHyp and is there a way to destruct the pair? Something like:

``````Inductive DC_Proof : LCtx -> LCtx -> Formula -> Prop :=

| dc_thyp : forall (D: LCtx) (G G': LCtx) ((n, A) : LabelledHyp),
DC_Proof D ((G,(pair n A));G') A
``````

#### Adrián García (Sep 16 2021 at 00:42):

And slist is my definition for snoc lists but it's replaceable for lists with no problem

#### Meven Lennon-Bertrand (Sep 16 2021 at 07:34):

What you are looking for looks like the so-called Irrefutable patterns. In a definition you could write something like

``````Definition dc_thyp (D G G' : LCtx) (l : LabelledHyp) := let 'pair n A := l in …
``````

but because of the restriction on what a constructor type can be, you cannot literally do this here. The closest I got was

``````Inductive DC_Proof : LCtx -> LCtx -> Formula -> Prop :=
| dc_thyp : forall (D: LCtx) (G G': LCtx) (l : LabelledHyp),
DC_Proof D ((G,(pair n A));G') (let 'pair _ A := l in A).
``````

#### Adrián García (Sep 16 2021 at 22:21):

Thanks, and as you said I'm not able to find a way to use the let inside as in a `Definition`, I'll keep looking for a way

Last updated: Feb 01 2023 at 12:30 UTC