Clean up some modules (#248)

* Remove an unused module

* Reorder some modules

theories/Algorithmic/Typing/Lemmas.v

@@ -268,8 +268,7 @@ Proof.
     assert {{ Γ ⊢ B'[Id,,N] ⊆ B[Id,,N] }} by mauto 3.
     assert {{ Γ ⊢ W ⊆ B[Id,,N] }} by (transitivity {{{ B'[Id,,N] }}}; mauto 3).
     econstructor; mauto 4 using alg_subtyping_complete.
-  - assert (exists i, {{ Γ ⊢ A : Type@i }}) as [i] by mauto 3.
-    assert (exists W, nbe_ty Γ A W /\ {{ Γ ⊢ A ≈ W : Type@i }}) as [W []] by (eapply soundness_ty; mauto 3).
+  - assert (exists W, nbe_ty Γ A W /\ {{ Γ ⊢ A ≈ W : Type@i }}) as [W []] by (eapply soundness_ty; mauto 3).
     econstructor; mauto 4 using alg_subtyping_complete.
 Qed.
 

theories/CoqMakefile.mk.local-late

@@ -63,4 +63,5 @@ $(DEPGRAPHDOC): $(DEPGRAPHDOT) $(DEPPOSTPROCESSSCRIPT)
 depgraphdoc: $(DEPGRAPHDOC)
 
 clean::
-	@rm $(DEPGRAPHDOT) $(DEPGRAPHDOC)
+	@echo "CLEAN $(DEPGRAPHDOT) $(DEPGRAPHDOC)"
+	@rm -f $(DEPGRAPHDOT) $(DEPGRAPHDOC)

theories/Core/Completeness/Consequences/Types.v

@@ -3,7 +3,7 @@ From Mcltt Require Import LibTactics.
 From Mcltt.Core Require Import Base.
 From Mcltt.Core Require Export Completeness.
 From Mcltt.Core.Semantic Require Import Realizability.
-From Mcltt.Core.Syntactic Require Export CoreInversions.
+From Mcltt.Core.Syntactic Require Export SystemOpt.
 Import Domain_Notations.
 
 Lemma exp_eq_typ_implies_eq_level : forall {Γ i j k},

theories/Core/Soundness/LogicalRelation/CoreLemmas.v

@@ -841,7 +841,7 @@ Proof.
           mauto 4.
         symmetry.
         bulky_rewrite_in H4.
-        assert {{ Δ0 ⊢ Π IT[σ∘σ0] (OT[q (σ∘σ0)]) ≈ (Π IT OT)[σ∘σ0] : Type@(S (max i4 i)) }} by mauto.
+        assert {{ Δ0 ⊢ Π IT[σ∘σ0] (OT[q (σ∘σ0)]) ≈ (Π IT OT)[σ∘σ0] : Type@_ }} by mauto.
         eapply wf_exp_eq_conv'; mauto 4.
       }
 

theories/Core/Soundness/Realizability.v

@@ -42,7 +42,7 @@ Lemma var_weaken_gen : forall Δ σ Γ,
       {{ Δ ⊢ #(length Γ1)[σ] ≈ #(length Δ - length Γ2 - 1) : ^(iter (S (length Γ1)) (fun A => {{{ A[Wk] }}}) A0)[σ] }}.
 Proof.
   induction 1; intros; subst; gen_presups.
-  - pose proof (app_ctx_vlookup _ _ _ _ HΔ eq_refl) as Hvar.
+  - pose proof (app_ctx_vlookup _ _ _ _ ltac:(eassumption) eq_refl) as Hvar.
     gen_presup Hvar.
     clear_dups.
     apply wf_sub_id_inversion in Hτ.

theories/Core/Syntactic/CoreInversions.v

@@ -1,9 +1,32 @@
 From Coq Require Import Setoid.
 From Mcltt Require Import LibTactics.
 From Mcltt.Core Require Import Base.
-From Mcltt.Core.Syntactic Require Export SystemOpt.
+From Mcltt.Core.Syntactic Require Export CtxEq.
 Import Syntax_Notations.
 
+Lemma wf_typ_inversion : forall {Γ i A},
+    {{ Γ ⊢ Type@i : A }} ->
+    {{ Γ ⊢ Type@(S i) ⊆ A }}.
+Proof with mautosolve.
+  intros * H.
+  dependent induction H...
+Qed.
+
+#[export]
+Hint Resolve wf_typ_inversion : mcltt.
+
+Lemma wf_nat_inversion : forall Γ A,
+    {{ Γ ⊢ ℕ : A }} ->
+    {{ Γ ⊢ Type@0 ⊆ A }}.
+Proof with mautosolve 4.
+  intros * H.
+  assert (forall i, 0 <= i) by lia.
+  dependent induction H...
+Qed.
+
+#[export]
+Hint Resolve wf_nat_inversion : mcltt.
+
 Corollary wf_zero_inversion : forall Γ A,
     {{ Γ ⊢ zero : A }} ->
     {{ Γ ⊢ ℕ ⊆ A }}.
@@ -37,23 +60,48 @@ Proof with mautosolve.
   pose (A0 := A).
   dependent induction H;
     try (specialize (IHwf_exp1 _ _ _ _ eq_refl));
-    destruct_conjs;
-    assert {{ Γ ⊢s Id : Γ }} by mauto 3;
-    repeat split...
+    destruct_conjs; gen_core_presups; repeat split...
 Qed.
 
 #[export]
 Hint Resolve wf_natrec_inversion : mcltt.
 
+Lemma wf_pi_inversion : forall {Γ A B C},
+    {{ Γ ⊢ Π A B : C }} ->
+    exists i, {{ Γ ⊢ A : Type@i }} /\ {{ Γ, A ⊢ B : Type@i }} /\ {{ Γ ⊢ Type@i ⊆ C }}.
+Proof with mautosolve 4.
+  intros * H.
+  dependent induction H;
+    try specialize (IHwf_exp1 _ _ eq_refl);
+    destruct_conjs; gen_core_presups; eexists...
+Qed.
+
+#[export]
+Hint Resolve wf_pi_inversion : mcltt.
+
+Corollary wf_pi_inversion' : forall {Γ A B i},
+    {{ Γ ⊢ Π A B : Type@i }} ->
+    {{ Γ ⊢ A : Type@i }} /\ {{ Γ, A ⊢ B : Type@i }}.
+Proof with mautosolve 4.
+  intros * [j [? []]]%wf_pi_inversion.
+  assert {{ Γ, A ⊢s Wk : Γ }} by mauto 4.
+  assert {{ Γ, A ⊢ Type@j ⊆ Type@j[Wk] }} by (econstructor; mauto 4).
+  assert {{ Γ, A ⊢ Type@j[Wk] ⊆ Type@i[Wk] }} by mauto 4.
+  assert {{ Γ, A ⊢ Type@i[Wk] ⊆ Type@i }} by (econstructor; mauto 4).
+  enough {{ Γ, A ⊢ Type@j ⊆ Type@i }}...
+Qed.
+
+#[export]
+Hint Resolve wf_pi_inversion' : mcltt.
+
 Corollary wf_fn_inversion : forall {Γ A M C},
     {{ Γ ⊢ λ A M : C }} ->
     exists B, {{ Γ, A ⊢ M : B }} /\ {{ Γ ⊢ Π A B ⊆ C }}.
-Proof with mautosolve 4.
+Proof with solve [mauto using lift_exp_max_left, lift_exp_max_right].
   intros * H.
   dependent induction H;
     try specialize (IHwf_exp1 _ _ eq_refl);
-    destruct_conjs;
-    gen_presups;
+    destruct_conjs; gen_core_presups;
     eexists; split...
 Qed.
 
@@ -63,7 +111,7 @@ Hint Resolve wf_fn_inversion : mcltt.
 Lemma wf_app_inversion : forall {Γ M N C},
     {{ Γ ⊢ M N : C }} ->
     exists A B, {{ Γ ⊢ M : Π A B }} /\ {{ Γ ⊢ N : A }} /\ {{ Γ ⊢ B[Id,,N] ⊆ C }}.
-Proof with mautosolve.
+Proof with mautosolve 4.
   intros * H.
   dependent induction H;
     try specialize (IHwf_exp1 _ _ eq_refl);
@@ -80,10 +128,8 @@ Lemma wf_vlookup_inversion : forall {Γ x A},
 Proof with mautosolve 4.
   intros * H.
   dependent induction H;
-    [assert (exists i, {{ Γ ⊢ A : Type@i }}) as [] by mauto 4 |];
     try (specialize (IHwf_exp1 _ eq_refl));
-    destruct_conjs;
-    eexists; split...
+    destruct_conjs; gen_core_presups; eexists; split...
 Qed.
 
 #[export]
@@ -92,13 +138,13 @@ Hint Resolve wf_vlookup_inversion : mcltt.
 Lemma wf_exp_sub_inversion : forall {Γ M σ A},
     {{ Γ ⊢ M[σ] : A }} ->
     exists Δ A', {{ Γ ⊢s σ : Δ }} /\ {{ Δ ⊢ M : A' }} /\ {{ Γ ⊢ A'[σ] ⊆ A }}.
-Proof with mautosolve.
+Proof with mautosolve 3.
   intros * H.
   dependent induction H;
     try (specialize (IHwf_exp1 _ _ eq_refl));
     destruct_conjs;
-    gen_presups;
-    do 2 eexists; split...
+    do 2 eexists; repeat split; mauto 3.
+  assert (exists j, {{ Δ ⊢ A : Type@j }}) as [] by mauto 2 using presup_exp_typ...
 Qed.
 
 #[export]
@@ -111,7 +157,7 @@ Lemma wf_sub_id_inversion : forall Γ Δ,
     {{ ⊢ Γ ⊆ Δ }}.
 Proof.
   intros * H.
-  dependent induction H; mautosolve.
+  dependent induction H; mautosolve 3.
 Qed.
 
 #[export]
@@ -125,7 +171,7 @@ Proof.
   dependent induction H;
     firstorder;
     progressive_inversion;
-    repeat eexists; mauto.
+    repeat eexists; mautosolve 3.
 Qed.
 
 #[export]
@@ -134,9 +180,9 @@ Hint Resolve wf_sub_weaken_inversion : mcltt.
 Lemma wf_sub_compose_inversion : forall {Γ1 σ1 σ2 Γ3},
     {{ Γ1 ⊢s σ1 ∘ σ2 : Γ3 }} ->
     exists Γ2, {{ Γ1 ⊢s σ2 : Γ2 }} /\ {{ Γ2 ⊢s σ1 : Γ3 }}.
-Proof with mautosolve 4.
+Proof with mautosolve 3.
   intros * H.
-  dependent induction H; mauto.
+  dependent induction H; mauto 3.
   specialize (IHwf_sub _ _ eq_refl).
   destruct_conjs.
   eexists.

theories/Core/Syntactic/Corollaries.v

@@ -1,23 +1,23 @@
 From Coq Require Import Setoid Nat.
 From Mcltt Require Import LibTactics.
 From Mcltt.Core Require Import Base.
-From Mcltt.Core.Syntactic Require Export CoreInversions.
+From Mcltt.Core.Syntactic Require Export SystemOpt.
 Import Syntax_Notations.
 
 Corollary sub_id_typ : forall Γ M A,
     {{ Γ ⊢ M : A }} ->
-    {{ Γ ⊢ M : A [ Id ] }}.
+    {{ Γ ⊢ M : A[Id] }}.
 Proof.
   intros.
   gen_presups.
-  econstructor; mauto 4.
+  mauto 4.
 Qed.
 
 #[export]
 Hint Resolve sub_id_typ : mcltt.
 
 Corollary invert_sub_id : forall Γ M A,
-    {{ Γ ⊢ M [ Id ] : A }} ->
+    {{ Γ ⊢ M[Id] : A }} ->
     {{ Γ ⊢ M : A }}.
 Proof.
   intros * [? [? [?%wf_sub_id_inversion []]]]%wf_exp_sub_inversion.
@@ -41,7 +41,7 @@ Qed.
 Hint Resolve invert_sub_id_typ : mcltt.
 
 Lemma invert_compose_id : forall {Γ σ Δ},
-    {{ Γ ⊢s σ ∘ Id : Δ }} ->
+    {{ Γ ⊢s σ∘Id : Δ }} ->
     {{ Γ ⊢s σ : Δ }}.
 Proof.
   intros * [? []]%wf_sub_compose_inversion.
@@ -72,7 +72,7 @@ Open Scope list_scope.
 
 Lemma app_ctx_lookup : forall Δ T Γ n,
     length Δ = n ->
-    {{ #n : ^(iter (S n) (fun T => {{{T [ Wk ]}}}) T) ∈ ^(Δ ++ T :: Γ) }}.
+    {{ #n : ^(iter (S n) (fun T => {{{ T[Wk] }}}) T) ∈ ^(Δ ++ T :: Γ) }}.
 Proof.
   induction Δ; intros; simpl in *; subst; mauto.
 Qed.
@@ -90,15 +90,15 @@ Qed.
 Lemma app_ctx_vlookup : forall Δ T Γ n,
     {{ ⊢ ^(Δ ++ T :: Γ) }} ->
     length Δ = n ->
-    {{ ^(Δ ++ T :: Γ) ⊢ #n : ^(iter (S n) (fun T => {{{T [ Wk ]}}}) T) }}.
+    {{ ^(Δ ++ T :: Γ) ⊢ #n : ^(iter (S n) (fun T => {{{ T[Wk] }}}) T) }}.
 Proof.
   intros. econstructor; auto using app_ctx_lookup.
 Qed.
 
 Lemma sub_q_eq : forall Δ A i Γ σ σ',
-                   {{ Δ ⊢ A : Type@i }} ->
-                   {{ Γ ⊢s σ ≈ σ' : Δ }} ->
-                   {{ Γ, A[σ] ⊢s q σ ≈ q σ' : Δ, A }}.
+    {{ Δ ⊢ A : Type@i }} ->
+    {{ Γ ⊢s σ ≈ σ' : Δ }} ->
+    {{ Γ, A[σ] ⊢s q σ ≈ q σ' : Δ, A }}.
 Proof.
   intros. gen_presup H0.
   econstructor; mauto 3.
@@ -112,7 +112,7 @@ Lemma wf_subtyp_subst_eq : forall Δ A B,
     {{ Δ ⊢ A ⊆ B }} ->
     forall Γ σ σ',
       {{ Γ ⊢s σ ≈ σ' : Δ }} ->
-      {{ Γ ⊢ A [σ] ⊆ B[σ'] }}.
+      {{ Γ ⊢ A[σ] ⊆ B[σ'] }}.
 Proof.
   induction 1; intros * Hσσ'; gen_presup Hσσ'.
   - eapply wf_subtyp_refl'.
@@ -128,7 +128,7 @@ Lemma wf_subtyp_subst : forall Δ A B,
     {{ Δ ⊢ A ⊆ B }} ->
     forall Γ σ,
       {{ Γ ⊢s σ : Δ }} ->
-      {{ Γ ⊢ A [σ] ⊆ B[σ] }}.
+      {{ Γ ⊢ A[σ] ⊆ B[σ] }}.
 Proof.
   intros; mauto 2 using wf_subtyp_subst_eq.
 Qed.
@@ -183,11 +183,11 @@ Qed.
 Hint Resolve exp_succ_sub_rhs : mcltt.
 
 Lemma sub_decompose_q : forall Γ S i σ Δ Δ' τ t,
-  {{Γ ⊢ S : Type@i}} ->
-  {{Δ ⊢s σ : Γ}} ->
-  {{Δ' ⊢s τ : Δ}} ->
-  {{Δ' ⊢ t : S [ σ ] [ τ ]}} ->
-  {{Δ' ⊢s q σ ∘ (τ ,, t) ≈ σ ∘ τ ,, t : Γ, S}}.
+  {{ Γ ⊢ S : Type@i }} ->
+  {{ Δ ⊢s σ : Γ }} ->
+  {{ Δ' ⊢s τ : Δ }} ->
+  {{ Δ' ⊢ t : S[σ][τ] }} ->
+  {{ Δ' ⊢s q σ ∘ (τ ,, t) ≈ σ ∘ τ ,, t : Γ, S }}.
 Proof.
   intros. gen_presups.
   simpl. autorewrite with mcltt.
@@ -205,11 +205,11 @@ Qed.
 Hint Rewrite -> @sub_decompose_q using mauto 4 : mcltt.
 
 Lemma sub_decompose_q_typ : forall Γ S T i σ Δ Δ' τ t,
-  {{Γ, S ⊢ T : Type@i}} ->
-  {{Δ ⊢s σ : Γ}} ->
-  {{Δ' ⊢s τ : Δ}} ->
-  {{Δ' ⊢ t : S [ σ ] [ τ ]}} ->
-  {{Δ' ⊢ T [ σ ∘ τ ,, t ] ≈ T [ q σ ] [ τ ,, t ] : Type@i}}.
+  {{ Γ, S ⊢ T : Type@i }} ->
+  {{ Δ ⊢s σ : Γ }} ->
+  {{ Δ' ⊢s τ : Δ }} ->
+  {{ Δ' ⊢ t : S[σ][τ] }} ->
+  {{ Δ' ⊢ T[σ∘τ,,t] ≈ T[q σ][τ,,t] : Type@i}}.
 Proof.
   intros. gen_presups.
   autorewrite with mcltt.