syntaxAlchemist/ladder-calculus
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

equiv_debruijn: add more hints & simplify TEq_Symm proof

Browse source
This commit is contained in:
Michael Sippel 2024-09-20 20:35:29 +02:00
parent 1d6fb9ab6d
commit 377f57e124
1 changed files with 7 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
coq/equiv_debruijn.v
View file

@ -3,6 +3,8 @@ Require Import terms_debruijn.
Open Scope ladder_type_scope. Open Scope ladder_type_scope.
Open Scope ladder_expr_scope. Open Scope ladder_expr_scope.
Create HintDb type_eq_hints.
Reserved Notation "S '-->distribute-ladder' T" (at level 40). Reserved Notation "S '-->distribute-ladder' T" (at level 40).
Inductive type_distribute_ladder : type_DeBruijn -> type_DeBruijn -> Prop := Inductive type_distribute_ladder : type_DeBruijn -> type_DeBruijn -> Prop :=
@ -38,6 +40,7 @@ Inductive type_distribute_ladder : type_DeBruijn -> type_DeBruijn -> Prop :=
where "S '-->distribute-ladder' T" := (type_distribute_ladder S T). where "S '-->distribute-ladder' T" := (type_distribute_ladder S T).
Hint Constructors type_distribute_ladder : type_eq_hints.
Reserved Notation "S '-->condense-ladder' T" (at level 40). Reserved Notation "S '-->condense-ladder' T" (at level 40).
Inductive type_condense_ladder : type_DeBruijn -> type_DeBruijn -> Prop := Inductive type_condense_ladder : type_DeBruijn -> type_DeBruijn -> Prop :=
@ -73,9 +76,6 @@ Inductive type_condense_ladder : type_DeBruijn -> type_DeBruijn -> Prop :=
where "S '-->condense-ladder' T" := (type_condense_ladder S T). where "S '-->condense-ladder' T" := (type_condense_ladder S T).
Create HintDb type_eq_hints.
Hint Constructors type_distribute_ladder : type_eq_hints.
Hint Constructors type_condense_ladder : type_eq_hints. Hint Constructors type_condense_ladder : type_eq_hints.
(** Inversion Lemma: (** Inversion Lemma:
@ -104,6 +104,8 @@ Proof.
all: auto with type_eq_hints. all: auto with type_eq_hints.
Qed. Qed.
Hint Resolve condense_inverse :type_eq_hints.
Hint Resolve distribute_inverse :type_eq_hints.
(** Define the equivalence relation as reflexive, transitive hull. $\label{coq:type-equiv}$ *) (** Define the equivalence relation as reflexive, transitive hull. $\label{coq:type-equiv}$ *)
@ -147,7 +149,7 @@ Inductive type_eq : type_DeBruijn -> type_DeBruijn -> Prop :=
where "S '===' T" := (type_eq S T). where "S '===' T" := (type_eq S T).
Hint Constructors type_eq : type_eq_hints.
(** Symmetry of === *) (** Symmetry of === *)
Lemma TEq_Symm : Lemma TEq_Symm :
@ -156,25 +158,5 @@ Lemma TEq_Symm :
Proof. Proof.
intros. intros.
induction H. induction H.
all: eauto with *.
apply TEq_Refl.
apply TEq_Trans with (y:=y).
apply IHtype_eq2.
apply IHtype_eq1.
apply TEq_SubFun.
auto. auto.
apply TEq_SubMorph.
auto. auto.
apply TEq_LadderAssocRL.
apply TEq_LadderAssocLR.
apply TEq_Condense.
apply distribute_inverse.
apply H.
apply TEq_Distribute.
apply condense_inverse.
apply H.
Qed. Qed.