From 18c144a919a6991d0815c0e352a2815bd7d5f443 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Thu, 27 Jun 2024 19:00:25 -0400
Subject: [PATCH 1/6] subtyping in the PER model

---
 theories/Core/Semantic/PER/CoreTactics.v |   4 +-
 theories/Core/Semantic/PER/Definitions.v |  28 +++++
 theories/Core/Semantic/PER/Lemmas.v      | 140 +++++++++++++++++++++++
 3 files changed, 170 insertions(+), 2 deletions(-)

diff --git a/theories/Core/Semantic/PER/CoreTactics.v b/theories/Core/Semantic/PER/CoreTactics.v
index 506b4a5a..597b40c6 100644
--- a/theories/Core/Semantic/PER/CoreTactics.v
+++ b/theories/Core/Semantic/PER/CoreTactics.v
@@ -45,12 +45,12 @@ Ltac destruct_rel_typ :=
 (** Universe/Element PER Helper Tactics *)
 
 Ltac basic_invert_per_univ_elem H :=
-  simp per_univ_elem in H;
+  progress simp per_univ_elem in H;
   inversion H;
   subst;
   try rewrite <- per_univ_elem_equation_1 in *.
 
 Ltac basic_per_univ_elem_econstructor :=
-  simp per_univ_elem;
+  progress simp per_univ_elem;
   econstructor;
   try rewrite <- per_univ_elem_equation_1 in *.
diff --git a/theories/Core/Semantic/PER/Definitions.v b/theories/Core/Semantic/PER/Definitions.v
index a26e915d..cb1fd879 100644
--- a/theories/Core/Semantic/PER/Definitions.v
+++ b/theories/Core/Semantic/PER/Definitions.v
@@ -227,6 +227,34 @@ Section Per_univ_elem_ind_def.
   | i, a, b, R, H := per_univ_elem_ind' i a b R _.
 End Per_univ_elem_ind_def.
 
+Reserved Notation "'Sub' a <: b 'at' i" (in custom judg at level 90, a custom domain, b custom domain, i constr).
+
+Inductive per_subtyp : nat -> domain -> domain -> Prop :=
+| per_subtyp_neut :
+  `( {{ Dom b ≈ b' ∈ per_bot }} ->
+     {{ Sub ⇑ a b <: ⇑ a' b' at i }} )
+| per_subtyp_nat :
+  `( {{ Sub ℕ <: ℕ at i }} )
+| per_subtyp_univ :
+  `( i <= j ->
+     j < k ->
+     {{ Sub 𝕌@i <: 𝕌@j at k }} )
+| per_subtyp_pi :
+  `( forall (in_rel : relation domain) elem_rel elem_rel',
+        {{ DF a ≈ a' ∈ per_univ_elem i ↘ in_rel }} ->
+        (forall c c' b b',
+            {{ Dom c ≈ c' ∈ in_rel }} ->
+            {{ ⟦ B ⟧ p ↦ c ↘ b }} ->
+            {{ ⟦ B' ⟧ p' ↦ c' ↘ b' }} ->
+            {{ Sub b <: b' at i }}) ->
+        {{ DF Π a p B ≈ Π a p B ∈ per_univ_elem i ↘ elem_rel }} ->
+        {{ DF Π a' p' B' ≈ Π a' p' B' ∈ per_univ_elem i ↘ elem_rel' }} ->
+        {{ Sub Π a p B <: Π a' p' B' at i }})
+where "'Sub' a <: b 'at' i" := (per_subtyp i a b) (in custom judg) : type_scope.
+
+#[export]
+ Hint Constructors per_subtyp : mcltt.
+
 (** Context/Environment PER *)
 
 Definition rel_typ (i : nat) (A : typ) (p : env) (A' : typ) (p' : env) R' := rel_mod_eval (per_univ_elem i) A p A' p' R'.
diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v
index de7efe87..cef57e38 100644
--- a/theories/Core/Semantic/PER/Lemmas.v
+++ b/theories/Core/Semantic/PER/Lemmas.v
@@ -615,6 +615,146 @@ Proof with mautosolve.
   assert (j <= max i j) by lia...
 Qed.
 
+Lemma per_subtyp_to_univ_elem : forall a b i,
+    {{ Sub a <: b at i }} ->
+    exists R R',
+      {{ DF a ≈ a ∈ per_univ_elem i ↘ R }} /\
+        {{ DF b ≈ b ∈ per_univ_elem i ↘ R' }}.
+Proof.
+  destruct 1; do 2 eexists; mauto;
+    split; per_univ_elem_econstructor; mauto;
+    try apply Equivalence_Reflexive.
+  lia.
+Qed.
+
+
+Lemma PER_refl1 A (R : relation A) `(per : PER A R) : forall a b, R a b -> R a a.
+Proof.
+  intros.
+  etransitivity; [eassumption |].
+  symmetry. assumption.
+Qed.
+
+Lemma PER_refl2 A (R : relation A) `(per : PER A R) : forall a b, R a b -> R b b.
+Proof.
+  intros. symmetry in H.
+  apply PER_refl1 in H;
+    auto.
+Qed.
+
+Ltac saturate_refl :=
+  repeat match goal with
+    | H : ?R ?a ?b |- _ =>
+        tryif unify a b
+        then fail
+        else
+          directed pose proof (PER_refl1 _ _ _ _ _ H);
+        directed pose proof (PER_refl2 _ _ _ _ _ H);
+        fail_if_dup
+    end.
+
+
+Lemma per_elem_subtyping : forall A B i,
+    {{ Sub A <: B at i }} ->
+    forall R R' a b,
+      {{ DF A ≈ A ∈ per_univ_elem i ↘ R }} ->
+      {{ DF B ≈ B ∈ per_univ_elem i ↘ R' }} ->
+      R a b ->
+      R' a b.
+Proof.
+  induction 1; intros.
+  4:clear H2 H3.
+  all:(on_all_hyp: fun H => directed invert_per_univ_elem H);
+    apply_equiv_left;
+    trivial.
+  - firstorder mauto.
+  - intros.
+    handle_per_univ_elem_irrel.
+    assert (in_rel c c') by (apply_equiv_left; trivial).
+    assert (in_rel1 c c') by (apply_equiv_left; trivial).
+    destruct_rel_mod_eval.
+    destruct_rel_mod_app.
+    econstructor; eauto.
+    saturate_refl.
+    deepexec H1 ltac:(fun H => apply H).
+    trivial.
+Qed.
+
+
+Lemma per_subtyp_refl : forall a b i R,
+    {{ DF a ≈ b ∈ per_univ_elem i ↘ R }} ->
+    {{ Sub a <: b at i }} /\ {{ Sub b <: a at i }}.
+Proof.
+  simpl; induction 1 using per_univ_elem_ind;
+    subst;
+    mauto;
+    destruct_all.
+
+  assert ({{ DF Π A p B ≈ Π A' p' B' ∈ per_univ_elem i ↘ elem_rel }})
+    by (eapply per_univ_elem_pi'; eauto; intros; destruct_rel_mod_eval; mauto).
+  saturate_refl.
+  split; econstructor; eauto.
+  - intros;
+      destruct_rel_mod_eval;
+      functional_eval_rewrite_clear;
+      trivial.
+  - symmetry. eassumption.
+  - intros. symmetry in H12.
+      destruct_rel_mod_eval;
+      functional_eval_rewrite_clear;
+      trivial.
+Qed.
+
+Lemma per_subtyp_refl1 : forall a b i R,
+    {{ DF a ≈ b ∈ per_univ_elem i ↘ R }} ->
+    {{ Sub a <: b at i }}.
+Proof.
+  intros.
+  apply per_subtyp_refl in H.
+  firstorder.
+Qed.
+
+Lemma per_subtyp_refl2 : forall a b i R,
+    {{ DF a ≈ b ∈ per_univ_elem i ↘ R }} ->
+    {{ Sub b <: a at i }}.
+Proof.
+  intros.
+  apply per_subtyp_refl in H.
+  firstorder.
+Qed.
+
+Lemma per_subtyp_trans : forall A1 A2 i,
+    {{ Sub A1 <: A2 at i }} ->
+    forall A3,
+      {{ Sub A2 <: A3 at i }} ->
+      {{ Sub A1 <: A3 at i }}.
+Proof.
+  induction 1; intros ? Hsub; simpl in *.
+  1-3:progressive_inversion;
+  mauto.
+  - econstructor; lia.
+  - dependent destruction Hsub.
+    handle_per_univ_elem_irrel.
+    econstructor; eauto.
+    + etransitivity; eassumption.
+    + intros.
+      saturate_refl.
+      directed invert_per_univ_elem H6.
+      directed invert_per_univ_elem H7.
+      destruct_rel_mod_eval.
+      functional_eval_rewrite_clear.
+      deepexec (H0 c c') ltac:(fun H => pose proof H).
+      deepexec (H5 c' c') ltac:(fun H => pose proof H);
+        [ apply_equiv_left; trivial |].
+      eauto.
+Qed.
+
+#[export]
+  Instance per_subtyp_trans_ins i : Transitive (per_subtyp i).
+Proof.
+  eauto using per_subtyp_trans.
+Qed.
+
 Add Parametric Morphism : per_ctx_env
     with signature (@relation_equivalence env) ==> eq ==> eq ==> iff as per_ctx_env_morphism_iff.
 Proof with mautosolve.

From fd30c664537f61280830e5927114b663fcf1baf2 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Thu, 27 Jun 2024 19:52:23 -0400
Subject: [PATCH 2/6] prove cumulativity

---
 theories/Core/Semantic/PER/Lemmas.v | 44 ++++++++++++++---------------
 1 file changed, 22 insertions(+), 22 deletions(-)

diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v
index cef57e38..4e5407d4 100644
--- a/theories/Core/Semantic/PER/Lemmas.v
+++ b/theories/Core/Semantic/PER/Lemmas.v
@@ -680,47 +680,31 @@ Proof.
     trivial.
 Qed.
 
-
-Lemma per_subtyp_refl : forall a b i R,
+Lemma per_subtyp_refl1 : forall a b i R,
     {{ DF a ≈ b ∈ per_univ_elem i ↘ R }} ->
-    {{ Sub a <: b at i }} /\ {{ Sub b <: a at i }}.
+    {{ Sub a <: b at i }}.
 Proof.
   simpl; induction 1 using per_univ_elem_ind;
     subst;
     mauto;
     destruct_all.
-
   assert ({{ DF Π A p B ≈ Π A' p' B' ∈ per_univ_elem i ↘ elem_rel }})
     by (eapply per_univ_elem_pi'; eauto; intros; destruct_rel_mod_eval; mauto).
   saturate_refl.
-  split; econstructor; eauto.
-  - intros;
-      destruct_rel_mod_eval;
-      functional_eval_rewrite_clear;
-      trivial.
-  - symmetry. eassumption.
-  - intros. symmetry in H12.
+  econstructor; eauto.
+  intros;
       destruct_rel_mod_eval;
       functional_eval_rewrite_clear;
       trivial.
 Qed.
 
-Lemma per_subtyp_refl1 : forall a b i R,
-    {{ DF a ≈ b ∈ per_univ_elem i ↘ R }} ->
-    {{ Sub a <: b at i }}.
-Proof.
-  intros.
-  apply per_subtyp_refl in H.
-  firstorder.
-Qed.
-
 Lemma per_subtyp_refl2 : forall a b i R,
     {{ DF a ≈ b ∈ per_univ_elem i ↘ R }} ->
     {{ Sub b <: a at i }}.
 Proof.
   intros.
-  apply per_subtyp_refl in H.
-  firstorder.
+  symmetry in H.
+  eauto using per_subtyp_refl1.
 Qed.
 
 Lemma per_subtyp_trans : forall A1 A2 i,
@@ -749,12 +733,28 @@ Proof.
       eauto.
 Qed.
 
+#[export]
+ Hint Resolve per_subtyp_trans : mcltt.
+
 #[export]
   Instance per_subtyp_trans_ins i : Transitive (per_subtyp i).
 Proof.
   eauto using per_subtyp_trans.
 Qed.
 
+Lemma per_subtyp_cumu : forall A1 A2 i,
+    {{ Sub A1 <: A2 at i }} ->
+    forall j,
+      i <= j ->
+      {{ Sub A1 <: A2 at j }}.
+Proof.
+  induction 1; intros; econstructor; mauto.
+  lia.
+Qed.
+
+#[export]
+ Hint Resolve per_subtyp_cumu : mcltt.
+
 Add Parametric Morphism : per_ctx_env
     with signature (@relation_equivalence env) ==> eq ==> eq ==> iff as per_ctx_env_morphism_iff.
 Proof with mautosolve.

From 84c448959abad9e2982027c1a7b53473d24e9005 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Fri, 28 Jun 2024 10:05:59 -0400
Subject: [PATCH 3/6] add subtyping between contexts

---
 theories/Core/Semantic/PER/Definitions.v | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/theories/Core/Semantic/PER/Definitions.v b/theories/Core/Semantic/PER/Definitions.v
index cb1fd879..10e2a7f4 100644
--- a/theories/Core/Semantic/PER/Definitions.v
+++ b/theories/Core/Semantic/PER/Definitions.v
@@ -291,3 +291,26 @@ Definition valid_ctx : ctx -> Prop := fun Γ => per_ctx Γ Γ.
 Hint Transparent valid_ctx : mcltt.
 #[export]
 Hint Unfold valid_ctx : mcltt.
+
+Reserved Notation "'SubE' Γ <: Δ" (in custom judg at level 90, Γ custom exp, Δ custom exp).
+
+
+Inductive per_ctx_subtyp : ctx -> ctx -> Prop :=
+| per_ctx_subtyp_nil :
+  {{ SubE ⋅ <: ⋅ }}
+| per_ctx_subtyp_cons :
+  `{ forall tail_rel' env_rel env_rel',
+        {{ SubE Γ <: Γ' }} ->
+        {{ EF Γ' ≈ Γ' ∈ per_ctx_env ↘ tail_rel' }} ->
+        (forall p p' a a'
+           (equiv_p_p' : {{ Dom p ≈ p' ∈ tail_rel }}),
+            {{ ⟦ A ⟧ p ↘ a }} ->
+            {{ ⟦ A' ⟧ p' ↘ a' }} ->
+            {{ Sub a <: a' at i }}) ->
+        {{ EF Γ , A ≈ Γ , A ∈ per_ctx_env ↘ env_rel }} ->
+        {{ EF Γ' , A' ≈ Γ' , A' ∈ per_ctx_env ↘ env_rel' }} ->
+        {{ SubE Γ, A <: Γ', A' }} }
+where "'SubE' Γ <: Δ" := (per_ctx_subtyp Γ Δ) (in custom judg) : type_scope.
+
+#[export]
+Hint Constructors per_ctx_subtyp : mcltt.

From 8774884641fe175fd586baec69959e0a6c2b6efe Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Fri, 28 Jun 2024 10:47:13 -0400
Subject: [PATCH 4/6] subtyping lemma for contexts

---
 theories/Core/Semantic/PER/Definitions.v |  2 +-
 theories/Core/Semantic/PER/Lemmas.v      | 64 +++++++++++++++++++++++-
 2 files changed, 63 insertions(+), 3 deletions(-)

diff --git a/theories/Core/Semantic/PER/Definitions.v b/theories/Core/Semantic/PER/Definitions.v
index 10e2a7f4..2d849638 100644
--- a/theories/Core/Semantic/PER/Definitions.v
+++ b/theories/Core/Semantic/PER/Definitions.v
@@ -303,7 +303,7 @@ Inductive per_ctx_subtyp : ctx -> ctx -> Prop :=
         {{ SubE Γ <: Γ' }} ->
         {{ EF Γ' ≈ Γ' ∈ per_ctx_env ↘ tail_rel' }} ->
         (forall p p' a a'
-           (equiv_p_p' : {{ Dom p ≈ p' ∈ tail_rel }}),
+           (equiv_p_p' : {{ Dom p ≈ p' ∈ tail_rel' }}),
             {{ ⟦ A ⟧ p ↘ a }} ->
             {{ ⟦ A' ⟧ p' ↘ a' }} ->
             {{ Sub a <: a' at i }}) ->
diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v
index 4e5407d4..e3190dd5 100644
--- a/theories/Core/Semantic/PER/Lemmas.v
+++ b/theories/Core/Semantic/PER/Lemmas.v
@@ -663,8 +663,8 @@ Lemma per_elem_subtyping : forall A B i,
       R' a b.
 Proof.
   induction 1; intros.
-  4:clear H2 H3.
-  all:(on_all_hyp: fun H => directed invert_per_univ_elem H);
+  all:handle_per_univ_elem_irrel;
+    (on_all_hyp: fun H => directed invert_per_univ_elem H);
     apply_equiv_left;
     trivial.
   - firstorder mauto.
@@ -755,6 +755,22 @@ Qed.
 #[export]
  Hint Resolve per_subtyp_cumu : mcltt.
 
+Lemma per_subtyp_cumu_left : forall A1 A2 i j,
+    {{ Sub A1 <: A2 at i }} ->
+    {{ Sub A1 <: A2 at max i j }}.
+Proof.
+  intros. eapply per_subtyp_cumu; try eassumption.
+  lia.
+Qed.
+
+Lemma per_subtyp_cumu_right : forall A1 A2 i j,
+    {{ Sub A1 <: A2 at i }} ->
+    {{ Sub A1 <: A2 at max j i }}.
+Proof.
+  intros. eapply per_subtyp_cumu; try eassumption.
+  lia.
+Qed.
+
 Add Parametric Morphism : per_ctx_env
     with signature (@relation_equivalence env) ==> eq ==> eq ==> iff as per_ctx_env_morphism_iff.
 Proof with mautosolve.
@@ -1031,3 +1047,47 @@ Proof.
   intros * [? H].
   induction H; simpl; congruence.
 Qed.
+
+Lemma per_ctx_subtyp_to_env : forall Γ Δ,
+    {{ SubE Γ <: Δ }} ->
+    exists R R',
+      {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ R }} /\
+        {{ EF Δ ≈ Δ ∈ per_ctx_env ↘ R' }}.
+Proof.
+  destruct 1; destruct_all.
+  - repeat eexists; econstructor; apply Equivalence_Reflexive.
+  - eauto.
+Qed.
+
+Lemma per_ctx_env_subtyping : forall Γ Δ,
+    {{ SubE Γ <: Δ }} ->
+    forall R R' p p',
+      {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ R }} ->
+      {{ EF Δ ≈ Δ ∈ per_ctx_env ↘ R' }} ->
+      R p p' ->
+      R' p p'.
+Proof.
+  induction 1; intros.
+  all:handle_per_ctx_env_irrel;
+    (on_all_hyp: fun H => directed invert_per_ctx_env H);
+    apply_equiv_left;
+    trivial.
+
+  handle_per_ctx_env_irrel.
+  destruct_all.
+  deepexec IHper_ctx_subtyp ltac:(fun H => pose proof H).
+  deepexec H2 ltac:(fun H => destruct H as []).
+  deepexec H12 ltac:(fun H => destruct H as []).
+  deepexec H1 ltac:(fun H => pose proof H).
+  destruct (per_subtyp_to_univ_elem _ _ _ H15) as [? [? [? ?]]].
+  handle_per_univ_elem_irrel.
+  eexists; try eassumption.
+
+  eapply per_elem_subtyping with (i := max x (max i0 i)).
+  + eauto using per_subtyp_cumu_right.
+  + saturate_refl.
+    eauto using per_univ_elem_cumu_max_left, per_univ_elem_cumu_max_right.
+  + saturate_refl.
+    eauto using per_univ_elem_cumu_max_left.
+  + trivial.
+Qed.

From 0eefa3a20f969ff11cdffb83b7bc328dbcb8ae37 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Fri, 28 Jun 2024 13:59:30 -0400
Subject: [PATCH 5/6] prove transitivity of context subtyping

---
 theories/Core/Semantic/PER/Definitions.v |  6 +-
 theories/Core/Semantic/PER/Lemmas.v      | 89 ++++++++++++++++++++++--
 theories/LibTactics.v                    | 28 +++++---
 3 files changed, 102 insertions(+), 21 deletions(-)

diff --git a/theories/Core/Semantic/PER/Definitions.v b/theories/Core/Semantic/PER/Definitions.v
index 2d849638..525e395b 100644
--- a/theories/Core/Semantic/PER/Definitions.v
+++ b/theories/Core/Semantic/PER/Definitions.v
@@ -299,11 +299,11 @@ Inductive per_ctx_subtyp : ctx -> ctx -> Prop :=
 | per_ctx_subtyp_nil :
   {{ SubE ⋅ <: ⋅ }}
 | per_ctx_subtyp_cons :
-  `{ forall tail_rel' env_rel env_rel',
+  `{ forall tail_rel env_rel env_rel',
         {{ SubE Γ <: Γ' }} ->
-        {{ EF Γ' ≈ Γ' ∈ per_ctx_env ↘ tail_rel' }} ->
+        {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ tail_rel }} ->
         (forall p p' a a'
-           (equiv_p_p' : {{ Dom p ≈ p' ∈ tail_rel' }}),
+           (equiv_p_p' : {{ Dom p ≈ p' ∈ tail_rel }}),
             {{ ⟦ A ⟧ p ↘ a }} ->
             {{ ⟦ A' ⟧ p' ↘ a' }} ->
             {{ Sub a <: a' at i }}) ->
diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v
index e3190dd5..8bf74077 100644
--- a/theories/Core/Semantic/PER/Lemmas.v
+++ b/theories/Core/Semantic/PER/Lemmas.v
@@ -653,6 +653,20 @@ Ltac saturate_refl :=
         fail_if_dup
     end.
 
+Ltac saturate_refl_for hd :=
+  repeat match goal with
+    | H : ?R ?a ?b |- _ =>
+        unify R hd;
+        tryif unify a b
+        then fail
+        else
+          directed pose proof (PER_refl1 _ _ _ _ _ H);
+        directed pose proof (PER_refl2 _ _ _ _ _ H);
+        fail_if_dup
+    end.
+
+Ltac solve_refl :=
+  solve [reflexivity || apply Equivalence_Reflexive].
 
 Lemma per_elem_subtyping : forall A B i,
     {{ Sub A <: B at i }} ->
@@ -677,7 +691,6 @@ Proof.
     econstructor; eauto.
     saturate_refl.
     deepexec H1 ltac:(fun H => apply H).
-    trivial.
 Qed.
 
 Lemma per_subtyp_refl1 : forall a b i R,
@@ -1077,17 +1090,79 @@ Proof.
   destruct_all.
   deepexec IHper_ctx_subtyp ltac:(fun H => pose proof H).
   deepexec H2 ltac:(fun H => destruct H as []).
-  deepexec H12 ltac:(fun H => destruct H as []).
+  deepexec H11 ltac:(fun H => destruct H as []).
   deepexec H1 ltac:(fun H => pose proof H).
   destruct (per_subtyp_to_univ_elem _ _ _ H15) as [? [? [? ?]]].
   handle_per_univ_elem_irrel.
   eexists; try eassumption.
 
   eapply per_elem_subtyping with (i := max x (max i0 i)).
-  + eauto using per_subtyp_cumu_right.
-  + saturate_refl.
-    eauto using per_univ_elem_cumu_max_left, per_univ_elem_cumu_max_right.
-  + saturate_refl.
+  - eauto using per_subtyp_cumu_right.
+  - saturate_refl.
     eauto using per_univ_elem_cumu_max_left.
-  + trivial.
+  - saturate_refl.
+    eauto using per_univ_elem_cumu_max_left, per_univ_elem_cumu_max_right.
+  - trivial.
+Qed.
+
+Lemma per_ctx_subtyp_refl1 : forall Γ Δ R,
+    {{ EF Γ ≈ Δ ∈ per_ctx_env ↘ R }} ->
+    {{ SubE Γ <: Δ }}.
+Proof.
+  induction 1; mauto.
+
+  assert (exists R, {{ EF Γ , A ≈ Γ' , A' ∈ per_ctx_env ↘ R }}) by
+    (eexists; eapply @per_ctx_env_cons' with (i := i); eassumption).
+  destruct_all.
+  econstructor; try solve [saturate_refl; mauto 2].
+  intros.
+  unfold rel_typ in *.
+  destruct_rel_mod_eval.
+  simplify_evals.
+  eauto using per_subtyp_refl1.
+Qed.
+
+Lemma per_ctx_subtyp_refl2 : forall Γ Δ R,
+    {{ EF Γ ≈ Δ ∈ per_ctx_env ↘ R }} ->
+    {{ SubE Δ <: Γ }}.
+Proof.
+  intros. symmetry in H. eauto using per_ctx_subtyp_refl1.
+Qed.
+
+Lemma per_ctx_subtyp_trans : forall Γ1 Γ2,
+    {{ SubE Γ1 <: Γ2 }} ->
+    forall Γ3,
+      {{ SubE Γ2 <: Γ3 }} ->
+      {{ SubE Γ1 <: Γ3 }}.
+Proof.
+  induction 1; intros;
+    progressive_inversion;
+      mauto 1;
+      clear_PER.
+
+  handle_per_ctx_env_irrel.
+  econstructor; try eassumption.
+  - firstorder.
+  - instantiate (1 := max i i0).
+    intros.
+    cutexec per_ctx_env_subtyping H ltac:(fun H => deepexec H ltac:(fun H => pose proof H)).
+    cutexec per_ctx_env_subtyping H7 ltac:(fun H => deepexec H ltac:(fun H => pose proof H)).
+    deepexec H22 ltac:(fun H => destruct H as []).
+
+    etransitivity.
+    + saturate_refl_for tail_rel4.
+      apply_equiv_right.
+      deepexec (H1 p p) ltac:(fun H => eauto using per_subtyp_cumu_left, H).
+    + eapply per_subtyp_cumu_right.
+      eapply H9; eauto.
+      apply_equiv_left; trivial.
+Qed.
+
+#[export]
+ Hint Resolve per_ctx_subtyp_trans : mcltt.
+
+#[export]
+  Instance per_ctx_subtyp_trans_ins : Transitive per_ctx_subtyp.
+Proof.
+  eauto using per_ctx_subtyp_trans.
 Qed.
diff --git a/theories/LibTactics.v b/theories/LibTactics.v
index 8ed1439f..d1f5c4f6 100644
--- a/theories/LibTactics.v
+++ b/theories/LibTactics.v
@@ -266,12 +266,11 @@ Ltac deepexec lem tac :=
       exvar T ltac:(fun x =>
                       lazymatch type of T with
                       | Prop => match goal with
-                            | H : _ |- _ => unify x H
-                            | _ => idtac
+                            | H : _ |- _ => unify x H; deepexec constr:(lem x) tac
+                            | _ => deepexec constr:(lem x) tac
                             end
-                      | _ => idtac
-                      end;
-                      deepexec constr:(lem x) tac)
+                      | _ => deepexec constr:(lem x) tac
+                      end)
   | _ => tac lem
   end.
 
@@ -291,14 +290,13 @@ Ltac cutexec lem C tac :=
                         unify x C;
                         tac lem
                       else
-                        (lazymatch type of T with
+                        lazymatch type of T with
                          | Prop => match goal with
-                               | H : _ |- _ => unify x H
-                               | _ => idtac
+                               | H : _ |- _ => unify x H; cutexec constr:(lem x) C tac
+                               | _ => cutexec constr:(lem x) C tac
                                end
-                         | _ => idtac
-                         end;
-                         cutexec constr:(lem x) C tac))
+                         | _ => cutexec constr:(lem x) C tac
+                         end)
   | _ => tac lem
   end.
 
@@ -348,3 +346,11 @@ Ltac unify_args H P :=
 
 #[global]
   Ltac apply_equiv_right := repeat apply_equiv_right1.
+
+#[global]
+  Ltac clear_PER :=
+  repeat match goal with
+    | H : PER _ |- _ => clear H
+    | H : Symmetric _ |- _ => clear H
+    | H : Transitive _ |- _ => clear H
+    end.

From 8c88ef82596a79a1205879cc7de949864294863a Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Fri, 28 Jun 2024 15:46:46 -0400
Subject: [PATCH 6/6] empty