add more gluing lemmas

theories/Core/Soundness/LogicalRelation/Definitions.v

@@ -277,14 +277,6 @@ Inductive glu_typ i Γ M A B : Prop :=
     glu_typ i Γ M A B.
 
 
-Ltac simpl_glu_rel1 :=
-  match goal with
-  | H : ?R <∙> _, H1 : ?R _ _ |- _ => apply H in H1; simpl in H1
-  | H : ?R <∙> _, H1 : ?R _ _ _ _ |- _ => apply H in H1; simpl in H1
-  | H : ?R <∙> _ |- ?R _ _ => apply H; simpl
-  | H : ?R <∙> _ |- ?R _ _ _ _ => apply H; simpl
-  end.
-
 Ltac invert_glu_rel1 :=
   match goal with
   | H : pi_typ_pred _ _ _ _ _ _ _ |- _ =>

theories/Core/Soundness/LogicalRelation/Lemmas.v

@@ -13,6 +13,9 @@ Proof.
   induction 1; mauto.
 Qed.
 
+#[local]
+ Hint Resolve glu_nat_per_nat : mcltt.
+
 Lemma glu_nat_escape : forall Γ m a,
     glu_nat Γ m a ->
     {{ ⊢ Γ }} ->
@@ -63,7 +66,7 @@ Qed.
 
 #[global]
   Ltac simpl_glu_rel :=
-  repeat simpl_glu_rel1;
+  apply_equiv_left;
   repeat invert_glu_rel1;
   destruct_all;
   gen_presups.
@@ -154,3 +157,62 @@ Lemma glu_nat_resp_wk : forall Γ m a,
 Proof.
   mauto using glu_nat_resp_wk'.
 Qed.
+#[export]
+ Hint Resolve glu_nat_resp_wk : mcltt.
+
+Lemma glu_univ_elem_trm_escape : forall i P El A B,
+    glu_univ_elem i P El A B ->
+    forall Γ t T a,
+      El Γ t T a ->
+      {{ Γ ⊢ t : T }}.
+Proof.
+  induction 1 using glu_univ_elem_ind; intros;
+    simpl_glu_rel; mauto 4.
+
+  specialize (H4 (length Γ)).
+  specialize (H (length Γ)).
+  assert {{ Γ ⊢w Id : Γ }} by mauto.
+  destruct_all.
+  specialize (H5 _ _ _ _ H6 H9 H7).
+  gen_presup H5.
+  mauto.
+Qed.
+
+Lemma glu_univ_elem_per : forall i P El A B,
+    glu_univ_elem i P El A B ->
+    exists R, per_univ_elem i R A B.
+Proof.
+  induction 1 using glu_univ_elem_ind; intros; eexists;
+    try solve [per_univ_elem_econstructor; try reflexivity; trivial].
+
+  - subst. eapply per_univ_elem_core_univ'; trivial.
+    reflexivity.
+  - invert_per_univ_elem H3. mauto.
+Qed.
+
+Lemma glu_univ_elem_trm_per : forall i P El A B,
+    glu_univ_elem i P El A B ->
+    forall Γ t T a R,
+      El Γ t T a ->
+      per_univ_elem i R A B ->
+      R a a.
+Proof.
+  induction 1 using glu_univ_elem_ind; intros;
+    match goal with
+    | H : per_univ_elem _ _ _ _ |- _ => invert_per_univ_elem H
+    end;
+    simpl_glu_rel;
+    mauto 4.
+
+  invert_per_univ_elem H3.
+  specialize (H16 a0 a0) as [? _].
+  specialize (H16 H7).
+  intros.
+  destruct_rel_mod_app.
+  destruct_rel_mod_eval.
+  functional_eval_rewrite_clear.
+  do_per_univ_elem_irrel_assert.
+
+  econstructor; eauto.
+  apply H23. trivial.
+Qed.

theories/LibTactics.v

@@ -1,5 +1,7 @@
 From Coq Require Export Program.Equality Program.Tactics Lia RelationClasses.
 
+Open Scope predicate_scope.
+
 Create HintDb mcltt discriminated.
 
 (** Generalization of Variables *)
@@ -226,3 +228,40 @@ 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
+  end.
+
+#[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 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
+  | H : relation_equivalence ?R _, H1 : ?T |- _ => tac1 H R H1 T
+  | H : ?R <∙> _ |- ?G => tac2 H R G
+  | H : relation_equivalence ?R _ |- ?G => tac2 H R G
+  end.
+
+
+#[global]
+  Ltac apply_equiv_left := repeat apply_equiv_left1.
+
+
+#[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 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
+  | H : relation_equivalence _ ?R, H1 : ?T |- _ => tac1 H R H1 T
+  | H : _ <∙> ?R |- ?G => tac2 H R G
+  | H : relation_equivalence _ ?R |- ?G => tac2 H R G
+  end.
+
+#[global]
+  Ltac apply_equiv_right := repeat apply_equiv_right1.