Add helper lemmas

theories/Core/Completeness.v

@@ -1,6 +1,6 @@
 From Mcltt Require Import Base LibTactics.
 From Mcltt.Core Require Import Completeness.FundamentalTheorem Semantic.Realizability.
-From Mcltt.Core Require Export Completeness.LogicalRelation Semantic.NbE System.
+From Mcltt.Core Require Export Semantic.NbE SystemOpt.
 Import Domain_Notations.
 
 Theorem completeness : forall {Γ M M' A},
@@ -9,7 +9,7 @@ Theorem completeness : forall {Γ M M' A},
 Proof with mautosolve.
   intros * [env_relΓ]%completeness_fundamental_exp_eq.
   destruct_conjs.
-  assert (exists p p', initial_env Γ p /\ initial_env Γ p' /\ {{ Dom p ≈ p' ∈ env_relΓ }}) as [p] by (apply per_ctx_then_per_env_initial_env; eauto).
+  assert (exists p p', initial_env Γ p /\ initial_env Γ p' /\ {{ Dom p ≈ p' ∈ env_relΓ }}) as [p] by (eauto using per_ctx_then_per_env_initial_env).
   destruct_conjs.
   functional_initial_env_rewrite_clear.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).

theories/Core/Completeness/ContextCases.v

@@ -1,6 +1,6 @@
-From Coq Require Import Morphisms_Relations RelationClasses.
+From Coq Require Import Morphisms_Relations.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.UniverseCases System.
+From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.UniverseCases.
 Import Domain_Notations.
 
 Proposition valid_ctx_empty :

theories/Core/Completeness/FunctionCases.v

@@ -1,6 +1,6 @@
-From Coq Require Import Morphisms_Relations Relation_Definitions RelationClasses.
+From Coq Require Import Morphisms_Relations Relation_Definitions.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.TermStructureCases Completeness.UniverseCases System.
+From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.TermStructureCases Completeness.UniverseCases.
 Import Domain_Notations.
 
 Lemma rel_exp_of_pi_inversion : forall {Γ M M' A B},

theories/Core/Completeness/FundamentalTheorem.v

@@ -1,14 +1,13 @@
 From Mcltt Require Import Base LibTactics.
 From Mcltt.Core Require Import
-  Completeness.LogicalRelation
   Completeness.ContextCases
   Completeness.FunctionCases
   Completeness.NatCases
   Completeness.SubstitutionCases
   Completeness.TermStructureCases
   Completeness.UniverseCases
-  Completeness.VariableCases
-  System.
+  Completeness.VariableCases.
+From Mcltt.Core Require Export Completeness.LogicalRelation SystemOpt.
 Import Domain_Notations.
 
 Section completeness_fundamental.

theories/Core/Completeness/LogicalRelation/Definitions.v

@@ -1,6 +1,6 @@
 From Coq Require Import Relations.
 From Mcltt Require Import Base.
-From Mcltt.Core Require Export Evaluation PER.
+From Mcltt.Core Require Export PER.
 Import Domain_Notations.
 
 Inductive rel_exp M p M' p' (R : relation domain) : Prop :=

theories/Core/Completeness/LogicalRelation/Tactics.v

@@ -1,6 +1,5 @@
-From Coq Require Import Morphisms_Relations RelationClasses.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Evaluation PER System.
+From Mcltt.Core Require Import PER.
 Import Domain_Notations.
 
 Ltac eexists_rel_exp :=

theories/Core/Completeness/NatCases.v

@@ -1,6 +1,6 @@
-From Coq Require Import Morphisms_Relations Relation_Definitions RelationClasses.
+From Coq Require Import Morphisms_Relations.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.SubstitutionCases Completeness.TermStructureCases Completeness.UniverseCases Semantic.Realizability System.
+From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.SubstitutionCases Completeness.TermStructureCases Completeness.UniverseCases Semantic.Realizability.
 Import Domain_Notations.
 
 Lemma rel_exp_of_nat_inversion : forall {Γ M M'},
@@ -335,7 +335,7 @@ Lemma eval_natrec_rel : forall {Γ env_relΓ MZ MZ' MS MS' A A' i m m'},
     {{ Γ, ℕ, A ⊨ MS ≈ MS' : A[Wk∘Wk,,succ(#1)] }} ->
     {{ Dom m ≈ m' ∈ per_nat }} ->
     (forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_relΓ }}),
-      forall (elem_rel : relation domain),
+      forall elem_rel,
         rel_typ i A d{{{ p ↦ m }}} A d{{{ p' ↦ m' }}} elem_rel ->
         exists r r',
           {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r }} /\
@@ -423,7 +423,8 @@ Lemma rel_exp_natrec_cong_rel_typ: forall {Γ A A' i M M' env_relΓ},
     forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_relΓ }}) n n',
       {{ ⟦ M ⟧ p ↘ n }} ->
       {{ ⟦ M' ⟧ p' ↘ n' }} ->
-      exists elem_rel, rel_typ i A d{{{ p ↦ n }}} A d{{{ p' ↦ n' }}} elem_rel.
+      exists elem_rel,
+        rel_typ i A d{{{ p ↦ n }}} A d{{{ p' ↦ n' }}} elem_rel.
 Proof.
   pose proof (@relation_equivalence_pointwise domain).
   pose proof (@relation_equivalence_pointwise env).
@@ -495,8 +496,7 @@ Lemma eval_natrec_sub_rel : forall {Γ env_relΓ σ Δ env_relΔ MZ MZ' MS MS' A
     {{ Dom m ≈ m' ∈ per_nat }} ->
     (forall p p'
         (equiv_p_p' : {{ Dom p ≈ p' ∈ env_relΓ }})
-        o o'
-        (elem_rel : relation domain),
+        o o' elem_rel,
         {{ ⟦ σ ⟧s p ↘ o }} ->
         {{ ⟦ σ ⟧s p' ↘ o' }} ->
         {{ Dom o ≈ o' ∈ env_relΔ }} ->
@@ -586,7 +586,8 @@ Lemma rel_exp_natrec_sub_rel_typ: forall {Γ σ Δ A i M env_relΓ},
     {{ Δ, ℕ ⊨ A : Type@i }} ->
     {{ Δ ⊨ M : ℕ }} ->
     forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_relΓ }}),
-    exists elem_rel, rel_typ i {{{ A[σ,,M[σ]] }}} p {{{ A[σ,,M[σ]] }}} p' elem_rel.
+    exists elem_rel,
+      rel_typ i {{{ A[σ,,M[σ]] }}} p {{{ A[σ,,M[σ]] }}} p' elem_rel.
 Proof.
   pose proof (@relation_equivalence_pointwise domain).
   pose proof (@relation_equivalence_pointwise env).
@@ -675,7 +676,7 @@ Lemma rel_exp_nat_beta_succ_rel_typ : forall {Γ env_relΓ A i M},
     {{ Γ, ℕ ⊨ A : Type@i }} ->
     {{ Γ ⊨ M : ℕ }} ->
     forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_relΓ }}),
-    exists elem_rel : relation domain,
+    exists elem_rel,
       rel_typ i {{{ A[Id,,succ M] }}} p {{{ A[Id,,succ M] }}} p' elem_rel.
 Proof.
   pose proof (@relation_equivalence_pointwise domain).
@@ -708,7 +709,7 @@ Proof.
   eexists_rel_exp.
   intros.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
-  assert (exists elem_rel : relation domain,
+  assert (exists elem_rel,
              rel_typ i {{{ A[Id,,succ M] }}} p {{{ A[Id,,succ M] }}} p' elem_rel) as [elem_rel]
       by (eapply rel_exp_nat_beta_succ_rel_typ; mauto).
   eexists; split; [eassumption |].

theories/Core/Completeness/SubstitutionCases.v

@@ -1,6 +1,6 @@
 From Coq Require Import Morphisms_Relations RelationClasses.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness.ContextCases Completeness.LogicalRelation Completeness.UniverseCases System.
+From Mcltt.Core Require Import Completeness.ContextCases Completeness.LogicalRelation Completeness.UniverseCases.
 Import Domain_Notations.
 
 Lemma rel_sub_id : forall {Γ},

theories/Core/Completeness/TermStructureCases.v

@@ -1,6 +1,6 @@
 From Coq Require Import Morphisms_Relations RelationClasses.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.UniverseCases System.
+From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.UniverseCases.
 Import Domain_Notations.
 
 Lemma rel_exp_sub_cong : forall {Δ M M' A σ σ' Γ},

theories/Core/Completeness/VariableCases.v

@@ -1,6 +1,6 @@
-From Coq Require Import Morphisms_Relations RelationClasses.
+From Coq Require Import Morphisms_Relations.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness.LogicalRelation System.
+From Mcltt.Core Require Import Completeness.LogicalRelation SystemOpt.
 Import Domain_Notations.
 
 Lemma valid_lookup : forall {Γ x A env_rel}

theories/Core/Semantic/NbE.v

@@ -1,6 +1,5 @@
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Evaluation Readback.
-From Mcltt.Core Require Export Domain.
+From Mcltt.Core Require Export Domain Evaluation Readback.
 Import Domain_Notations.
 
 Generalizable All Variables.

theories/Core/Semantic/PER/CoreTactics.v

@@ -1,7 +1,7 @@
 From Coq Require Import Lia PeanoNat Relation_Definitions RelationClasses.
 From Equations Require Import Equations.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Evaluation PER.Definitions Readback.
+From Mcltt.Core Require Import PER.Definitions.
 Import Domain_Notations.
 
 Ltac destruct_rel_by_assumption in_rel H :=

theories/Core/Semantic/PER/Definitions.v

@@ -1,8 +1,7 @@
 From Coq Require Import Lia PeanoNat Relation_Definitions RelationClasses.
 From Equations Require Import Equations.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Evaluation Readback.
-From Mcltt Require Export Domain.
+From Mcltt.Core Require Export Domain Evaluation Readback.
 Import Domain_Notations.
 
 Notation "'Dom' a ≈ b ∈ R" := ((R a b : Prop) : Prop) (in custom judg at level 90, a custom domain, b custom domain, R constr).

theories/Core/Semantic/PER/Lemmas.v

@@ -1,7 +1,7 @@
 From Coq Require Import Equivalence Lia Morphisms Morphisms_Prop Morphisms_Relations PeanoNat Relation_Definitions RelationClasses.
 From Equations Require Import Equations.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Evaluation PER.Definitions PER.CoreTactics Readback.
+From Mcltt.Core Require Import PER.Definitions PER.CoreTactics.
 Import Domain_Notations.
 
 Add Parametric Morphism A : PER

theories/Core/Semantic/Realizability.v

@@ -1,7 +1,7 @@
 From Coq Require Import Lia Morphisms_Relations PeanoNat Relation_Definitions.
 From Equations Require Import Equations.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Export Evaluation NbE PER Readback.
+From Mcltt.Core Require Export NbE PER.
 Import Domain_Notations.
 
 Lemma per_nat_then_per_top : forall {n m},

theories/Core/Soundness/LogicalRelation/Definitions.v

@@ -2,9 +2,8 @@ From Coq Require Import Relation_Definitions RelationClasses.
 From Equations Require Import Equations.
 
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import System.Definitions Evaluation Readback PER.Definitions.
-From Mcltt Require Export Domain.
-From Mcltt.Core.Soundness Require Export Weakening.Definition.
+From Mcltt.Core Require Import System.Definitions.
+From Mcltt.Core Require Export Domain PER.Definitions Soundness.Weakening.Definition.
 
 Import Domain_Notations.
 Global Open Scope predicate_scope.

theories/Core/Soundness/LogicalRelation/Lemmas.v

@@ -1,7 +1,7 @@
 From Coq Require Import Morphisms Morphisms_Relations.
-From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Evaluation PER Presup CtxEq Readback Syntactic.Corollaries System.Lemmas.
 
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Import PER Syntactic.Corollaries.
 From Mcltt.Core.Soundness Require Import LogicalRelation.Definitions.
 From Mcltt.Core.Soundness Require Export Weakening.Lemmas.
 Import Domain_Notations.
@@ -262,7 +262,7 @@ Proof.
     eapply H2; eauto.
     assert {{ Γ ⊢ m ≈ t' : Π IT OT }} as Hty by mauto.
     assert {{ Δ ⊢ IT [ σ ] : Type @ i4 }} by mauto 3.
-    eapply wf_exp_eq_sub_cong with (Γ := Δ) in Hty; [|mauto 4].
+    eapply wf_exp_eq_sub_cong with (Γ := Δ) in Hty; [| eapply sub_eq_refl; mauto 3].
     autorewrite with mcltt in Hty.
     eapply wf_exp_eq_app_cong with (N := m') (N' := m') in Hty; try pi_univ_level_tac; [|mauto 2].
     autorewrite with mcltt in Hty.

theories/Core/Soundness/Weakening/Lemmas.v

@@ -1,7 +1,7 @@
 From Coq Require Import Program.Equality.
 
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import CtxEq Presup Syntactic.Corollaries System Weakening.Definition.
+From Mcltt.Core Require Import Syntactic.Corollaries Weakening.Definition.
 Import Syntax_Notations.
 
 Lemma weakening_escape : forall Γ σ Δ,

theories/Core/Syntactic/Corollaries.v

@@ -1,6 +1,6 @@
 From Coq Require Import Setoid.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import CtxEq Presup.
+From Mcltt.Core Require Export SystemOpt.
 Import Syntax_Notations.
 
 Corollary invert_id : forall Γ Δ,
@@ -20,7 +20,7 @@ Corollary sub_id_typ : forall Γ M A,
 Proof.
   intros.
   gen_presups.
-  mauto 6.
+  econstructor; mauto 4.
 Qed.
 
 #[export]
@@ -40,5 +40,7 @@ Hint Resolve invert_sub_id : mcltt.
 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.
-  intros. gen_presups. mauto 4.
+  intros.
+  gen_presups.
+  mauto 4.
 Qed.

theories/Core/Syntactic/Presup.v

@@ -257,33 +257,6 @@ Qed.
 #[export]
 Hint Resolve presup_exp presup_exp_eq presup_sub_eq : mcltt.
 
-#[local]
-Ltac invert_wf_ctx1 H :=
-  match type of H with
-  | {{ ⊢ ~_ , ~_ }} =>
-      let H' := fresh "H" in
-      pose proof H as H';
-      progressive_invert H'
-  end.
-
-Ltac invert_wf_ctx :=
-  (on_all_hyp: fun H => invert_wf_ctx1 H);
-  clear_dups.
-
 Ltac gen_presup H := gen_presup_IH @presup_exp @presup_exp_eq @presup_sub_eq H.
 
-Ltac gen_presups := (on_all_hyp: fun H => gen_presup H); invert_wf_ctx;  clear_dups.
-
-Lemma wf_ctx_eq_extend' : forall (Γ Δ : ctx) (A : typ) (i : nat) (A' : typ),
-    {{ ⊢ Γ ≈ Δ }} ->
-    {{ Γ ⊢ A ≈ A' : Type@i }} ->
-    {{ ⊢ Γ , A ≈ Δ , A' }}.
-Proof.
-  intros. gen_presups.
-  econstructor; mauto.
-Qed.
-
-#[export]
-Hint Resolve wf_ctx_eq_extend' : mcltt.
-#[export]
-Remove Hints wf_ctx_eq_extend : mcltt.
+Ltac gen_presups := (on_all_hyp: fun H => gen_presup H); invert_wf_ctx; clear_dups.

theories/Core/Syntactic/System.v

@@ -1 +1 @@
-From Mcltt Require Export System.Definitions System.Lemmas.
+From Mcltt Require Export System.Definitions System.Lemmas System.Tactics.

theories/Core/Syntactic/System/Tactics.v

@@ -0,0 +1,16 @@
+From Mcltt Require Import Base LibTactics.
+From Mcltt Require Export System.Definitions.
+Import Syntax_Notations.
+
+#[local]
+Ltac invert_wf_ctx1 H :=
+  match type of H with
+  | {{ ⊢ ~_ , ~_ }} =>
+      let H' := fresh "H" in
+      pose proof H as H';
+      progressive_invert H'
+  end.
+
+Ltac invert_wf_ctx :=
+  (on_all_hyp: fun H => invert_wf_ctx1 H);
+  clear_dups.