Update PER tactic

Beluga-lang · May 22, 2024 · b080b96 · b080b96
1 parent 51369fd
commit b080b96
Show file tree

Hide file tree

Showing 4 changed files with 135 additions and 77 deletions.
diff --git a/theories/Core/Completeness/FunctionCases.v b/theories/Core/Completeness/FunctionCases.v
@@ -12,26 +12,23 @@ Ltac extract_output_info_with p c p' c' env_rel :=
    destruct_by_head rel_typ;
    destruct_by_head rel_exp).
 
-Lemma rel_exp_pi_core : forall {i p o B p' o' B'} {tail_rel : relation env}
-    (head_rel : forall p p', {{ Dom p ≈ p' ∈ tail_rel }} -> relation domain)
-    (equiv_p_p' : {{ Dom p ≈ p' ∈ tail_rel }})
-    {out_rel},
+Lemma rel_exp_pi_core : forall {i o B o' B' R out_rel},
     (forall c c',
-        head_rel p p' equiv_p_p' c c' ->
+        R c c' ->
         rel_exp B d{{{ o ↦ c }}} B' d{{{ o' ↦ c' }}} (per_univ i)) ->
     (* We use this equality to make unification on `out_rel` works *)
-    (out_rel = fun c c' (equiv_c_c' : head_rel p p' equiv_p_p' c c') m m' =>
-                 forall b b' R,
+    (out_rel = fun c c' (equiv_c_c' : R c c') m m' =>
+                 forall b b' R',
                    {{ ⟦ B ⟧ o ↦ c ↘ b }} ->
                    {{ ⟦ B' ⟧ o' ↦ c' ↘ b' }} ->
-                   per_univ_elem i R b b' -> R m m') ->
-    (forall c c' (equiv_c_c' : head_rel p p' equiv_p_p' c c'), rel_typ i B d{{{ o ↦ c }}} B' d{{{ o' ↦ c' }}} (out_rel c c' equiv_c_c')).
+                   per_univ_elem i R' b b' -> R' m m') ->
+    (forall c c' (equiv_c_c' : R c c'), rel_typ i B d{{{ o ↦ c }}} B' d{{{ o' ↦ c' }}} (out_rel c c' equiv_c_c')).
 Proof with intuition.
   pose proof (@relation_equivalence_pointwise domain).
   pose proof (@relation_equivalence_pointwise env).
   intros.
   subst.
-  (on_all_hyp: destruct_rel_by_assumption (head_rel p p' equiv_p_p')).
+  (on_all_hyp: destruct_rel_by_assumption R).
   destruct_by_head rel_exp.
   econstructor; mauto.
   destruct_by_head per_univ.
@@ -49,9 +46,7 @@ Proof with intuition.
   intros * [env_relΓ] [env_relΓA].
   destruct_conjs.
   pose (env_relΓA0 := env_relΓA).
-  match_by_head (per_ctx_env env_relΓA)
-    ltac:(fun H => eapply per_ctx_env_cons_clear_inversion in H; [| eassumption]).
-  destruct_conjs.
+  match_by_head (per_ctx_env env_relΓA) invert_per_ctx_env.
   eexists_rel_exp.
   intros.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
@@ -63,7 +58,7 @@ Proof with intuition.
   eexists (per_univ _).
   split; [> econstructor; only 1-2: repeat econstructor; eauto ..].
   eexists.
-  per_univ_elem_econstructor; eauto with typeclass_instances.
+  per_univ_elem_econstructor; eauto.
   - intros.
     eapply rel_exp_pi_core; eauto.
     + clear dependent c.
@@ -87,10 +82,9 @@ Proof with intuition.
   pose proof (@relation_equivalence_pointwise env).
   intros * [env_relΓ] [env_relΔ] [env_relΔA].
   destruct_conjs.
+  pose (env_relΔ0 := env_relΔ).
   pose (env_relΔA0 := env_relΔA).
-  match_by_head (per_ctx_env env_relΔA)
-    ltac:(fun H => eapply per_ctx_env_cons_clear_inversion in H; [| eassumption]).
-  destruct_conjs.
+  match_by_head (per_ctx_env env_relΔA) invert_per_ctx_env.
   handle_per_ctx_env_irrel.
   eexists_rel_exp.
   intros.
@@ -105,7 +99,7 @@ Proof with intuition.
   eexists.
   split; [> econstructor; only 1-2: repeat econstructor; eauto ..].
   eexists.
-  per_univ_elem_econstructor; eauto with typeclass_instances.
+  per_univ_elem_econstructor; eauto.
   - intros.
     eapply rel_exp_pi_core; eauto.
     + clear dependent c.
@@ -131,9 +125,7 @@ Proof with intuition.
   intros * [env_relΓ] [env_relΓA].
   destruct_conjs.
   pose (env_relΓA0 := env_relΓA).
-  match_by_head (per_ctx_env env_relΓA)
-    ltac:(fun H => eapply per_ctx_env_cons_clear_inversion in H; [| eassumption]).
-  destruct_conjs.
+  match_by_head (per_ctx_env env_relΓA) invert_per_ctx_env.
   handle_per_ctx_env_irrel.
   eexists_rel_exp.
   intros.
@@ -144,8 +136,7 @@ Proof with intuition.
   functional_eval_rewrite_clear.
   eexists.
   split; [> econstructor; only 1-2: repeat econstructor; eauto ..].
-  - per_univ_elem_econstructor; [eapply per_univ_elem_cumu_max_left | | |];
-      eauto with typeclass_instances.
+  - per_univ_elem_econstructor; [eapply per_univ_elem_cumu_max_left | |]; eauto.
     + intros.
       eapply rel_exp_pi_core; eauto.
       * clear dependent c.
@@ -175,18 +166,15 @@ Proof with intuition.
   intros * [env_relΓ [? [env_relΔ]]] [env_relΔA].
   destruct_conjs.
   pose (env_relΔA0 := env_relΔA).
-  match_by_head (per_ctx_env env_relΔA)
-    ltac:(fun H => eapply per_ctx_env_cons_clear_inversion in H; [| eassumption]).
-  destruct_conjs.
+  match_by_head (per_ctx_env env_relΔA) invert_per_ctx_env.
   handle_per_ctx_env_irrel.
   eexists_rel_exp.
   intros.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
   (on_all_hyp: destruct_rel_by_assumption env_relΔ).
   eexists.
   split; [> econstructor; only 1-2: repeat econstructor; eauto ..].
-  - per_univ_elem_econstructor; [eapply per_univ_elem_cumu_max_left | | |];
-      eauto with typeclass_instances.
+  - per_univ_elem_econstructor; [eapply per_univ_elem_cumu_max_left | |]; eauto.
     + intros.
       eapply rel_exp_pi_core; eauto.
       * clear dependent c.
@@ -222,17 +210,14 @@ Proof with intuition.
   assert (equiv_p'_p' : env_relΓ p' p') by (etransitivity; [symmetry |]; eauto).
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
   destruct_by_head rel_typ.
-  functional_eval_rewrite_clear.
-  invert_rel_typ_body.
   handle_per_univ_elem_irrel.
+  invert_rel_typ_body.
   destruct_by_head rel_exp.
   functional_eval_rewrite_clear.
-  assert (in_rel0 m1 m2) by (etransitivity; [| symmetry]; eauto).
+  rename x into in_rel.
+  assert (in_rel m1 m2) by (etransitivity; [| symmetry]; eauto).
   assert (in_rel m1 m'2) by intuition.
-  assert (in_rel m1 m2) by intuition.
   (on_all_hyp: destruct_rel_by_assumption in_rel).
-  (on_all_hyp: destruct_rel_by_assumption in_rel0).
-  (on_all_hyp_rev: destruct_rel_by_assumption in_rel0).
   handle_per_univ_elem_irrel.
   eexists.
   split; [> econstructor; only 1-2: econstructor ..].
@@ -259,9 +244,8 @@ Proof with intuition.
   (on_all_hyp: destruct_rel_by_assumption env_relΔ).
   destruct_by_head rel_typ.
   invert_rel_typ_body.
-  handle_per_univ_elem_irrel.
   destruct_by_head rel_exp.
-  functional_eval_rewrite_clear.
+  rename x into in_rel.
   (on_all_hyp_rev: destruct_rel_by_assumption in_rel).
   eexists.
   split; [> econstructor; only 1-2: econstructor ..].
@@ -280,9 +264,7 @@ Proof with intuition.
   intros * [env_relΓA] [env_relΓ].
   destruct_conjs.
   pose (env_relΓA0 := env_relΓA).
-  match_by_head (per_ctx_env env_relΓA)
-    ltac:(fun H => eapply per_ctx_env_cons_clear_inversion in H; [| eassumption]).
-  destruct_conjs.
+  match_by_head (per_ctx_env env_relΓA) invert_per_ctx_env.
   handle_per_ctx_env_irrel.
   eexists_rel_exp.
   intros.

diff --git a/theories/Core/Completeness/LogicalRelation/Tactics.v b/theories/Core/Completeness/LogicalRelation/Tactics.v
@@ -16,6 +16,7 @@ Ltac eexists_rel_subst :=
 
 Ltac invert_rel_typ_body :=
   dir_inversion_by_head eval_exp; subst;
+  functional_eval_rewrite_clear;
   match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H); subst;
   clear_refl_eqs;
   handle_per_univ_elem_irrel;

diff --git a/theories/Core/Semantic/PER/CoreTactics.v b/theories/Core/Semantic/PER/CoreTactics.v
@@ -37,13 +37,13 @@ Ltac destruct_rel_typ :=
 
 (** Universe/Element PER Helper Tactics *)
 
-Ltac invert_per_univ_elem H :=
+Ltac basic_invert_per_univ_elem H :=
   simp per_univ_elem in H;
   inversion H;
   subst;
   try rewrite <- per_univ_elem_equation_1 in *.
 
-Ltac per_univ_elem_econstructor :=
+Ltac basic_per_univ_elem_econstructor :=
   simp per_univ_elem;
   econstructor;
   try rewrite <- per_univ_elem_equation_1 in *.