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
And slist is my definition for snoc lists but it's replaceable for lists with no problem
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).
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: Oct 13 2024 at 01:02 UTC