address comments

theories/Core/Semantic/PER/CoreTactics.v

@@ -18,20 +18,26 @@ Ltac destruct_rel_mod_eval :=
     match goal with
     | H : (forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ ?in_rel }}), rel_mod_eval _ _ _ _ _ _) |- _ =>
         destruct_rel_by_assumption in_rel H; mark H
+    | H : rel_mod_eval _ _ _ _ _ _ |- _ =>
+        dependent destruction H
     end;
   unmark_all.
 Ltac destruct_rel_mod_app :=
   repeat
     match goal with
     | H : (forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ ?in_rel }}), rel_mod_app _ _ _ _ _) |- _ =>
         destruct_rel_by_assumption in_rel H; mark H
+    | H : rel_mod_app _ _ _ _ _ |- _ =>
+        dependent destruction H
     end;
   unmark_all.
 Ltac destruct_rel_typ :=
   repeat
     match goal with
     | H : (forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ ?in_rel }}), rel_typ _ _ _ _ _ _) |- _ =>
         destruct_rel_by_assumption in_rel H; mark H
+    | H : rel_typ _ _ _ _ _ _ |- _ =>
+        dependent destruction H
     end;
   unmark_all.
 

theories/Core/Soundness/LogicalRelation/Lemmas.v

@@ -113,7 +113,7 @@ Proof.
     simpl_glu_rel; repeat split; mauto.
 
   intros.
-  specialize (H3 _ _ _ H2 H7); mauto.
+  specialize (H4 _ _ _ H2 H7); mauto.
 Qed.
 
 
@@ -198,21 +198,17 @@ Lemma glu_univ_elem_trm_per : forall i P El A B,
       R a a.
 Proof.
   induction 1 using glu_univ_elem_ind; intros;
-    try do 2 match goal with
-      | H : per_univ_elem _ _ _ _ |- _ => invert_per_univ_elem H
-      end;
+    try do 2 match_by_head1 per_univ_elem ltac:(fun H => invert_per_univ_elem H);
     simpl_glu_rel;
     mauto 4.
-  specialize (H14 a0 a0) as [? _].
-  specialize (H14 H6).
+
   intros.
   destruct_rel_mod_app.
   destruct_rel_mod_eval.
   functional_eval_rewrite_clear.
   do_per_univ_elem_irrel_assert.
 
-  econstructor; eauto.
-  apply H23. trivial.
+  econstructor; firstorder eauto.
 Qed.
 
 Lemma glu_univ_elem_trm_typ : forall i P El A B,
@@ -261,7 +257,7 @@ Proof.
     intros.
     destruct_rel_mod_eval.
     assert {{ Δ ⊢ m' : IT [ σ ]}} by eauto using glu_univ_elem_trm_escape.
-    edestruct H11 as [? []]; eauto.
+    edestruct H12 as [? []]; eauto.
     eexists; split; eauto.
     eapply H2; eauto.
     assert {{ Γ ⊢ m ≈ t' : Π IT OT }} as Hty by mauto.

theories/Core/Syntactic/Corollaries.v

@@ -37,13 +37,6 @@ Qed.
 #[export]
 Hint Resolve invert_sub_id : mcltt.
 
-Add Parametric Morphism i Γ Δ : a_sub
-    with signature wf_exp_eq Δ {{{ Type@i }}} ==> wf_sub_eq Γ Δ ==> wf_exp_eq Γ {{{ Type@i }}} as sub_typ_cong.
-Proof.
-  intros. gen_presups. mauto 4.
-Qed.
-
-
 Add Parametric Morphism i Γ Δ t (H : {{ Δ ⊢ t : Type@i }}) : (a_sub t)
     with signature wf_sub_eq Γ Δ ==> wf_exp_eq Γ {{{ Type@i }}} as sub_typ_cong1.
 Proof.

theories/Core/Syntactic/System/Definitions.v

@@ -339,22 +339,3 @@ Qed.
   Hint Rewrite -> wf_sub_eq_id_compose_right wf_sub_eq_id_compose_left
                    wf_sub_eq_compose_assoc (* prefer right association *)
                    wf_sub_eq_p_extend using mauto 4 : mcltt.
-
-
-Definition a_extend_eq_cong_rel i Γ Δ A : relation (sub -> exp -> sub) :=
-  fun e1 e2 =>
-    forall (σ σ' : sub) (M M' : typ),
-      {{ Γ ⊢s σ ≈ σ' : Δ }} ->
-      {{ Δ ⊢ A : Type @ i }} ->
-      {{ Γ ⊢ M ≈ M' : ~ A [ σ ] }} ->
-      {{ Γ ⊢s ~(e1 σ M) ≈ ~ (e2 σ' M') : Δ, A }}.
-Arguments a_extend_eq_cong_rel i Γ Δ A/.
-#[export]
-  Typeclasses Transparent a_extend_eq_cong_rel.
-
-(* this morphism is added this way because the intended ==> syntax does not allow to add the well-formedness of A *)
-#[export]
-  Instance a_extend_eq_cong_morph i Γ Δ A : Proper (a_extend_eq_cong_rel i Γ Δ A) a_extend.
-Proof.
-  econstructor; eauto.
-Qed.

theories/LibTactics.v

@@ -150,6 +150,13 @@ Ltac clean_replace_by exp0 exp1 tac :=
 
 Tactic Notation "clean" "replace" uconstr(exp0) "with" uconstr(exp1) "by" tactic3(tac) := clean_replace_by exp0 exp1 tac.
 
+#[global]
+  Ltac find_head t :=
+  lazymatch t with
+  | ?t' _ => find_head t'
+  | _ => t
+  end.
+
 Ltac match_by_head1 head tac :=
   match goal with
   | [ H : ?X _ _ _ _ _ _ _ _ _ _ |- _ ] => unify X head; tac H
@@ -229,16 +236,89 @@ Ltac predicate_resolve :=
 (* intuition tactic default setting *)
 Ltac Tauto.intuition_solver ::= auto with mcltt core solve_subterm.
 
-#[global]
-  Ltac find_head t :=
-  lazymatch t with
-  | ?t' _ => find_head t'
-  | _ => t
+Ltac exvar T tac :=
+  lazymatch type of T with
+  | Prop =>
+      let H := fresh "H" in
+      unshelve evar (H : T);
+      [|
+        let H' := eval unfold H in H in
+          clear H; tac H']
+  | _ =>
+      let x := fresh "x" in
+      evar (x : T);
+      let x' := eval unfold x in x in
+        clear x; tac x'
+  end.
+
+(* this tactic traverses to the bottom of a lemma following universals and conjunctions to the bottom and apply a tactic *)
+Ltac deepexec lem tac :=
+  let T := type of lem in
+  let T' := eval simpl in T in
+  let ST := eval unfold iff in T' in
+  match ST with
+  | _ /\ _ => deepexec constr:(proj1 lem) tac
+            || deepexec constr:(proj2 lem) tac
+  | forall _ : ?T, _ =>
+      exvar T ltac:(fun x =>
+                      lazymatch type of T with
+                      | Prop => match goal with
+                            | H : _ |- _ => unify x H
+                            | _ => idtac
+                            end
+                      | _ => idtac
+                      end;
+                      deepexec constr:(lem x) tac)
+  | _ => tac lem
   end.
 
+(* this tactic is similar to above, but the traversal cuts off when it sees an assumption applicable to a cut-off argument C *)
+Ltac cutexec lem C tac :=
+  let CT := type of C in
+  let T := type of lem in
+  let T' := eval simpl in T in
+  let ST := eval unfold iff in T' in
+  lazymatch ST with
+  | _ /\ _ => cutexec constr:(proj1 lem) C tac
+            || cutexec constr:(proj2 lem) C tac
+  | forall _ : ?T, _ =>
+      exvar T ltac:(fun x =>
+                      tryif unify T CT
+                      then
+                        unify x C;
+                        tac lem
+                      else
+                        (lazymatch type of T with
+                         | Prop => match goal with
+                               | H : _ |- _ => unify x H
+                               | _ => idtac
+                               end
+                         | _ => idtac
+                         end;
+                         cutexec constr:(lem x) C tac))
+  | _ => tac lem
+  end.
+
+
+Ltac unify_args H P :=
+  lazymatch P with
+  | ?P' ?x =>
+      let r := unify_args H P' in
+      constr:(r x)
+  | _ => H
+  end.
+
+#[global]
+  Ltac strong_apply H X :=
+  let H' := fresh "H" in
+  let T := type of X in
+  let R := unify_args H T in
+  cutexec R X ltac:(fun L => pose proof (L X) as H'; simpl in H'; clear X; rename H' into X).
+
+
 #[global]
   Ltac apply_equiv_left1 :=
-  let tac1 := fun H R H1 T => (let h := find_head T in unify R h; apply H in H1; simpl in H1) in
+  let tac1 := fun H R H1 T => (let h := find_head T in unify R h; strong_apply H H1) in
   let tac2 := fun H R G => (let h := find_head G in unify R h; apply H; simpl) in
   match goal with
   | H : ?R <∙> _, H1 : ?T |- _ => tac1 H R H1 T
@@ -254,7 +334,7 @@ Ltac Tauto.intuition_solver ::= auto with mcltt core solve_subterm.
 
 #[global]
   Ltac apply_equiv_right1 :=
-  let tac1 := fun H R H1 T => (let h := find_head T in unify R h; apply H in H1; simpl in H1) in
+  let tac1 := fun H R H1 T => (let h := find_head T in unify R h; strong_apply H H1) in
   let tac2 := fun H R G => (let h := find_head G in unify R h; apply H; simpl) in
   match goal with
   | H : _ <∙> ?R, H1 : ?T |- _ => tac1 H R H1 T