Reorganize code

theories/Algorithmic/Typing/Lemmas.v

@@ -3,26 +3,11 @@ From Mcltt.Algorithmic Require Import Typing.Definitions.
 From Mcltt.Algorithmic Require Export Subtyping.Lemmas.
 From Mcltt.Core Require Import Soundness Completeness.
 From Mcltt.Core.Completeness Require Import Consequences.Rules.
+From Mcltt.Core.Semantic Require Import Consequences.
 From Mcltt.Core.Syntactic Require Export SystemOpt.
 From Mcltt.Frontend Require Import Elaborator.
 Import Domain_Notations.
 
-(* There might be a better file for this. *)
-Lemma idempotent_nbe_ty : forall {Γ i A B C},
-    {{ Γ ⊢ A : Type@i }} ->
-    nbe_ty Γ A B ->
-    nbe_ty Γ B C ->
-    B = C.
-Proof.
-  intros.
-  assert {{ Γ ⊢ A ≈ B : Type@i }} as [? []]%completeness_ty by mauto 2 using soundness_ty'.
-  functional_nbe_rewrite_clear.
-  reflexivity.
-Qed.
-
-#[local]
-Hint Resolve idempotent_nbe_ty : mcltt.
-
 Lemma functional_alg_type_infer : forall {Γ A A' M},
     {{ Γ ⊢a M ⟹ A }} ->
     {{ Γ ⊢a M ⟹ A' }} ->

theories/Core/Semantic/Consequences.v

@@ -1,6 +1,8 @@
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness Completeness.Consequences.Inversions Completeness.Consequences.Types Completeness.LogicalRelation Readback Soundness.
-From Mcltt.Core Require Export SystemOpt.
+From Mcltt.Core Require Import Completeness Soundness.
+From Mcltt.Core.Completeness Require Import Consequences.Types LogicalRelation.
+From Mcltt.Core.Semantic Require Import NbE.
+From Mcltt.Core.Syntactic Require Export SystemOpt.
 Import Domain_Notations.
 
 Lemma adjust_exp_eq_level : forall {Γ A A' i j},
@@ -55,3 +57,18 @@ Proof.
   match_by_head1 read_nf ltac:(fun H => inversion_clear H).
   do 2 eexists; mauto.
 Qed.
+
+Lemma idempotent_nbe_ty : forall {Γ i A B C},
+    {{ Γ ⊢ A : Type@i }} ->
+    nbe_ty Γ A B ->
+    nbe_ty Γ B C ->
+    B = C.
+Proof.
+  intros.
+  assert {{ Γ ⊢ A ≈ B : Type@i }} as [? []]%completeness_ty by mauto 2 using soundness_ty'.
+  functional_nbe_rewrite_clear.
+  reflexivity.
+Qed.
+
+#[export]
+Hint Resolve idempotent_nbe_ty : mcltt.

theories/Core/Soundness/NatCases.v

@@ -131,19 +131,6 @@ Qed.
 #[export]
 Hint Resolve glu_rel_sub_extend_nat : mcltt.
 
-Lemma exp_eq_typ_q_sigma_then_weak_weak_extend_succ_var_1 : forall {Δ σ Γ i A},
-    {{ Δ ⊢s σ : Γ }} ->
-    {{ Γ, ℕ ⊢ A : Type@i }} ->
-    {{ Δ, ℕ, A[q σ] ⊢ A[q σ][Wk∘Wk,,succ #1] ≈ A[Wk∘Wk,,succ #1][q (q σ)] : Type@i }}.
-Proof.
-  intros.
-  autorewrite with mcltt.
-  rewrite -> @sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1; mauto 2.
-  eapply exp_eq_refl.
-  eapply exp_sub_typ; mauto 2.
-  econstructor; mauto 3.
-Qed.
-
 Lemma glu_rel_exp_natrec_zero_helper : forall {i Γ SbΓ A MZ MS Δ M σ p am P El},
     {{ EG Γ ∈ glu_ctx_env ↘ SbΓ }} ->
     {{ Γ, ℕ ⊢ A : Type@i }} ->

theories/Core/Syntactic/Corollaries.v

@@ -485,3 +485,23 @@ Qed.
 Hint Resolve sub_eq_q_compose_nat : mcltt.
 #[export]
 Hint Rewrite -> @sub_eq_q_compose_nat using mauto 4 : mcltt.
+
+Lemma exp_eq_typ_q_sigma_then_weak_weak_extend_succ_var_1 : forall {Δ σ Γ i A},
+    {{ Δ ⊢s σ : Γ }} ->
+    {{ Γ, ℕ ⊢ A : Type@i }} ->
+    {{ Δ, ℕ, A[q σ] ⊢ A[q σ][Wk∘Wk,,succ #1] ≈ A[Wk∘Wk,,succ #1][q (q σ)] : Type@i }}.
+Proof.
+  intros.
+  assert {{ Δ, ℕ ⊢s q σ : Γ, ℕ }} by mauto 3.
+  assert {{ Δ, ℕ, A[q σ] ⊢s Wk∘Wk,,succ #1 : Δ, ℕ }} by mauto 3.
+  assert {{ Δ, ℕ, A[q σ] ⊢ A[q σ][Wk∘Wk,,succ #1] ≈ A[q σ∘(Wk∘Wk,,succ #1)] : Type@i }} as -> by mauto 3.
+  assert {{ Δ, ℕ, A[q σ] ⊢s q (q σ) : Γ, ℕ, A }} by mauto 3.
+  assert {{ Δ, ℕ, A[q σ] ⊢ A[Wk∘Wk,,succ #1][q (q σ)] ≈ A[(Wk∘Wk,,succ #1)∘q (q σ)] : Type@i }} as -> by mauto 3.
+  rewrite -> @sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1; mauto 2.
+  eapply exp_eq_refl.
+  eapply exp_sub_typ; mauto 2.
+  econstructor; mauto 3.
+Qed.
+
+#[export]
+Hint Resolve exp_eq_typ_q_sigma_then_weak_weak_extend_succ_var_1 : mcltt.

theories/Frontend/Elaborator.v

@@ -149,9 +149,8 @@ Inductive closed_at : exp -> nat -> Prop :=
  | ca_succ : forall a n, closed_at a n -> closed_at (a_succ a) n
  | ca_natrec : forall n m z s l, closed_at n l -> closed_at m (1+l) -> closed_at z l -> closed_at s (2+l) -> closed_at (a_natrec m z s n) l
 .
-(* TODO: JH: create our own hint database. *)
 #[local]
-Hint Constructors closed_at: core.
+Hint Constructors closed_at: mcltt.
 
 (*Lemma for the well_scoped proof, lookup succeeds if var is in context*)
 Lemma lookup_known (s : string) (ctx : list string) (H_in : List.In s ctx) : exists n : nat, (lookup s ctx = Some n /\ n < List.length ctx).
@@ -217,33 +216,33 @@ Qed.
 Lemma well_scoped (cst : Cst.obj) : forall ctx,  cst_variables cst [<=] StrSProp.of_list ctx  ->
 exists a : exp, (elaborate cst ctx = Some a) /\ (closed_at a (List.length ctx)).
 Proof.
-  induction cst; intros; simpl in *; eauto.
-  - destruct (IHcst _ H) as [ast [-> ?]]; eauto.
+  induction cst; intros; simpl in *; mauto.
+  - destruct (IHcst _ H) as [ast [-> ?]]; mauto.
   - assert (cst_variables cst1 [<=] StrSProp.of_list ctx) by fsetdec.
     assert (cst_variables cst2 [<=] StrSProp.of_list (s :: ctx)) by (simpl; fsetdec).
     assert (cst_variables cst3 [<=] StrSProp.of_list ctx) by fsetdec.
     assert (cst_variables cst4 [<=] StrSProp.of_list (s0 :: s1 :: ctx)) by (simpl; fsetdec).
     destruct (IHcst1 _ H0) as [ast [-> ?]];
       destruct (IHcst2 _ H1) as [ast' [-> ?]];
       destruct (IHcst3 _ H2) as [ast'' [-> ?]];
-      destruct (IHcst4 _ H3) as [ast''' [-> ?]]; eauto.
+      destruct (IHcst4 _ H3) as [ast''' [-> ?]]; mauto.
   - assert (cst_variables cst1 [<=] StrSProp.of_list ctx) by fsetdec.
     assert (cst_variables cst2 [<=] StrSProp.of_list ctx) by fsetdec.
     destruct (IHcst1 _ H0) as [ast [-> ?]];
-      destruct (IHcst2 _ H1) as [ast' [-> ?]]; eauto.
+      destruct (IHcst2 _ H1) as [ast' [-> ?]]; mauto.
   - assert (cst_variables cst1 [<=] StrSProp.of_list ctx) by fsetdec.
     assert (cst_variables cst2 [<=] StrSProp.of_list (s :: ctx)) by (simpl; fsetdec).
     destruct (IHcst1 _ H0) as [ast [-> ?]];
-      destruct (IHcst2 _ H1) as [ast' [-> ?]]; eauto.
+      destruct (IHcst2 _ H1) as [ast' [-> ?]]; mauto.
   - assert (cst_variables cst1 [<=] StrSProp.of_list ctx) by fsetdec.
     assert (cst_variables cst2 [<=] StrSProp.of_list (s :: ctx)) by (simpl; fsetdec).
     destruct (IHcst1 _ H0) as [ast [-> ?]];
-      destruct (IHcst2 _ H1) as [ast' [-> ?]]; eauto.
+      destruct (IHcst2 _ H1) as [ast' [-> ?]]; mauto.
   - apply Subset_to_In in H.
     edestruct lookup_known as [? [-> ?]]; [auto |].
     apply (In_nth _ _ s)  in H.
     destruct H as [? [? ?]].
-    eauto.
+    mauto.
 Qed.