From 377f57e1240e7d21f23dda2c0073b43d6c152f91 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Fri, 20 Sep 2024 20:35:29 +0200
Subject: [PATCH] equiv_debruijn: add more hints & simplify TEq_Symm proof
---
coq/equiv_debruijn.v | 32 +++++++-------------------------
1 file changed, 7 insertions(+), 25 deletions(-)
diff --git a/coq/equiv_debruijn.v b/coq/equiv_debruijn.v
index 0feaebf..8d7f3cf 100644
--- a/coq/equiv_debruijn.v
+++ b/coq/equiv_debruijn.v
@@ -3,6 +3,8 @@ Require Import terms_debruijn.
Open Scope ladder_type_scope.
Open Scope ladder_expr_scope.
+Create HintDb type_eq_hints.
+
Reserved Notation "S '-->distribute-ladder' T" (at level 40).
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).
+Hint Constructors type_distribute_ladder : type_eq_hints.
Reserved Notation "S '-->condense-ladder' T" (at level 40).
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).
-Create HintDb type_eq_hints.
-
-Hint Constructors type_distribute_ladder : type_eq_hints.
Hint Constructors type_condense_ladder : type_eq_hints.
(** Inversion Lemma:
@@ -104,6 +104,8 @@ Proof.
all: auto with type_eq_hints.
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}$ *)
@@ -147,7 +149,7 @@ Inductive type_eq : type_DeBruijn -> type_DeBruijn -> Prop :=
where "S '===' T" := (type_eq S T).
-
+Hint Constructors type_eq : type_eq_hints.
(** Symmetry of === *)
Lemma TEq_Symm :
@@ -156,25 +158,5 @@ Lemma TEq_Symm :
Proof.
intros.
induction H.
-
- 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.
+ all: eauto with *.
Qed.