Stream: Coq users

Topic: pairs and lists


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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