Refactor syntatic code style (#45)

theories/Core/Base.v

@@ -0,0 +1,7 @@
+#[global] Declare Scope exp_scope.
+#[global] Delimit Scope exp_scope with exp.
+
+#[global] Bind Scope exp_scope with Sortclass.
+
+#[global] Declare Custom Entry judg.
+Notation "{{ x }}" := x (at level 0, x custom judg at level 99, format "'{{'  x  '}}'").

theories/Core/Syntactic/CtxEquiv.v

@@ -1,27 +1,22 @@
-Require Import Unicode.Utf8_core.
-
-Require Import LibTactics.
-Require Import Syntactic.Syntax.
-Require Import Syntactic.System.
-Require Import Syntactic.SystemLemmas.
+From Mcltt Require Import Base LibTactics Syntax System SystemLemmas.
 
 #[local]
 Ltac gen_ctxeq_helper_IH ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper H :=
   match type of H with
-  | {{ ?Γ ⊢ ?M : ?A }} => pose proof ctxeq_exp_helper _ _ _ H
-  | {{ ?Γ ⊢ ?M ≈ ?N : ?A }} => pose proof ctxeq_exp_eq_helper _ _ _ _ H
-  | {{ ?Γ ⊢s ?σ : ?Δ }} => pose proof ctxeq_sub_helper _ _ _ H
-  | {{ ?Γ ⊢s ?σ ≈ ?τ : ?Δ }} => pose proof ctxeq_sub_eq_helper _ _ _ _ H
+  | {{ ~?Γ ⊢ ~?M : ~?A }} => pose proof ctxeq_exp_helper _ _ _ H
+  | {{ ~?Γ ⊢ ~?M ≈ ~?N : ~?A }} => pose proof ctxeq_exp_eq_helper _ _ _ _ H
+  | {{ ~?Γ ⊢s ~?σ : ~?Δ }} => pose proof ctxeq_sub_helper _ _ _ H
+  | {{ ~?Γ ⊢s ~?σ ≈ ~?τ : ~?Δ }} => pose proof ctxeq_sub_eq_helper _ _ _ _ H
   | _ => idtac
   end.
 
-Lemma ctxeq_exp_helper : forall {Γ M A}, {{ Γ ⊢ M : A }} -> ∀ {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢ M : A }}
+Lemma ctxeq_exp_helper : forall {Γ M A}, {{ Γ ⊢ M : A }} -> forall {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢ M : A }}
 with
-ctxeq_exp_eq_helper : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> ∀ {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢ M ≈ M' : A }}
+ctxeq_exp_eq_helper : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> forall {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢ M ≈ M' : A }}
 with
-ctxeq_sub_helper : forall {Γ Γ' σ}, {{ Γ ⊢s σ : Γ' }} -> ∀ {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢s σ : Γ' }}
+ctxeq_sub_helper : forall {Γ Γ' σ}, {{ Γ ⊢s σ : Γ' }} -> forall {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢s σ : Γ' }}
 with
-ctxeq_sub_eq_helper : forall {Γ Γ' σ σ'}, {{ Γ ⊢s σ ≈ σ' : Γ' }} -> ∀ {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}.
+ctxeq_sub_eq_helper : forall {Γ Γ' σ σ'}, {{ Γ ⊢s σ ≈ σ' : Γ' }} -> forall {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}.
 Proof with solve [mauto].
   (* ctxeq_exp_helper *)
   - intros * HM * HΓΔ. gen Δ.
@@ -37,7 +32,7 @@ Proof with solve [mauto].
 
     + econstructor...
 
-    + assert (∃ B i, {{ #x : B ∈ Δ }} ∧ {{ Γ ⊢ A ≈ B : Type@i }} ∧ {{ Δ ⊢ A ≈ B : Type@i }}) as [? [? [? [? ?]]]]...
+    + assert (exists B i, {{ #x : B ∈ Δ }} /\ {{ Γ ⊢ A ≈ B : Type@i }} /\ {{ Δ ⊢ A ≈ B : Type@i }}) as [? [? [? [? ?]]]]...
 
   (* ctxeq_exp_eq_helper *)
   - intros * HMM' * HΓΔ. gen Δ.
@@ -49,10 +44,10 @@ Proof with solve [mauto].
     1-5: assert {{ Δ ⊢ B : Type@i }} by eauto.
     1-5: assert {{ ⊢ Γ, B ≈ Δ, B }}...
 
-    + assert (∃ B i, {{ #x : B ∈ Δ }} ∧ {{ Γ ⊢ A ≈ B : Type@i }} ∧ {{ Δ ⊢ A ≈ B : Type@i }}) as [? [? [? [? ?]]]]...
+    + assert (exists B i, {{ #x : B ∈ Δ }} /\ {{ Γ ⊢ A ≈ B : Type@i }} /\ {{ Δ ⊢ A ≈ B : Type@i }}) as [? [? [? [? ?]]]]...
 
     + inversion_clear HΓΔ as [|? Δ0 ? ? C'].
-      assert (∃ D i', {{ #x : D ∈ Δ0 }} ∧ {{ Γ0 ⊢ B ≈ D : Type@i' }} ∧ {{ Δ0 ⊢ B ≈ D : Type@i' }}) as [D [i0 [? [? ?]]]] by mauto.
+      assert (exists D i', {{ #x : D ∈ Δ0 }} /\ {{ Γ0 ⊢ B ≈ D : Type@i' }} /\ {{ Δ0 ⊢ B ≈ D : Type@i' }}) as [D [i0 [? [? ?]]]] by mauto.
       assert {{ Δ0, C' ⊢ B[Wk] ≈ D[Wk] : Type @ i0 }}...
 
   (* ctxeq_sub_helper *)

theories/Core/Syntactic/Presup.v

@@ -1,20 +1,12 @@
-Require Import Unicode.Utf8_core.
-Require Import Setoid.
-
-Require Import LibTactics.
-Require Import Syntactic.Syntax.
-Require Import Syntactic.System.
-Require Import Syntactic.SystemLemmas.
-Require Import Syntactic.CtxEquiv.
-Require Import Syntactic.Relations.
+From Mcltt Require Import Base CtxEquiv LibTactics Relations Syntax System SystemLemmas.
 
 Ltac gen_presup_ctx H :=
   match type of H with
-  | {{ ⊢ ?Γ ≈ ?Δ }} =>
+  | {{ ⊢ ~?Γ ≈ ~?Δ }} =>
       let HΓ := fresh "HΓ" in
       let HΔ := fresh "HΔ" in
       pose proof presup_ctx_eq H as [HΓ HΔ]
-  | {{ ?Γ ⊢s ?σ : ?Δ }} =>
+  | {{ ~?Γ ⊢s ~?σ : ~?Δ }} =>
       let HΓ := fresh "HΓ" in
       let HΔ := fresh "HΔ" in
       pose proof presup_sub_ctx H as [HΓ HΔ]
@@ -23,19 +15,19 @@ Ltac gen_presup_ctx H :=
 
 Ltac gen_presup_IH presup_exp presup_exp_eq presup_sub_eq H :=
   match type of H with
-  | {{ ?Γ ⊢ ?M : ?A }} =>
+  | {{ ~?Γ ⊢ ~?M : ~?A }} =>
       let HΓ := fresh "HΓ" in
       let i := fresh "i" in
       let HAi := fresh "HAi" in
       pose proof presup_exp _ _ _ H as [HΓ [i HAi]]
-  | {{ ?Γ ⊢ ?M ≈ ?N : ?A }} =>
+  | {{ ~?Γ ⊢ ~?M ≈ ~?N : ~?A }} =>
       let HΓ := fresh "HΓ" in
       let i := fresh "i" in
       let HM := fresh "HM" in
       let HN := fresh "HN" in
       let HAi := fresh "HAi" in
       pose proof presup_exp_eq _ _ _ _ H as [HΓ [HM [HN [i HAi]]]]
-  | {{ ?Γ ⊢s ?σ ≈ ?τ : ?Δ }} =>
+  | {{ ~?Γ ⊢s ~?σ ≈ ~?τ : ~?Δ }} =>
       let HΓ := fresh "HΓ" in
       let Hσ := fresh "Hσ" in
       let Hτ := fresh "Hτ" in
@@ -44,9 +36,9 @@ Ltac gen_presup_IH presup_exp presup_exp_eq presup_sub_eq H :=
   | _ => gen_presup_ctx H
   end.
 
-Lemma presup_exp : forall {Γ M A}, {{ Γ ⊢ M : A }} -> {{ ⊢ Γ }} ∧ ∃ i, {{ Γ ⊢ A : Type@i }}
-with presup_exp_eq : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> {{ ⊢ Γ }} ∧ {{ Γ ⊢ M : A }} ∧ {{ Γ ⊢ M' : A }} ∧ ∃ i, {{ Γ ⊢ A : Type@i }}
-with presup_sub_eq : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }} ∧ {{ Γ ⊢s σ : Δ }} ∧ {{ Γ ⊢s σ' : Δ }} ∧ {{ ⊢ Δ }}.
+Lemma presup_exp : forall {Γ M A}, {{ Γ ⊢ M : A }} -> {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ A : Type@i }}
+with presup_exp_eq : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> {{ ⊢ Γ }} /\ {{ Γ ⊢ M : A }} /\ {{ Γ ⊢ M' : A }} /\ exists i, {{ Γ ⊢ A : Type@i }}
+with presup_sub_eq : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }} /\ {{ Γ ⊢s σ : Δ }} /\ {{ Γ ⊢s σ' : Δ }} /\ {{ ⊢ Δ }}.
 Proof with solve [mauto].
   (* presup_exp *)
   - intros * HM.
@@ -179,15 +171,15 @@ Proof with solve [mauto].
       assert {{ Γ ⊢ B[Wk][σ ,, N'] ≈ B[σ] : Type@i }} by mauto.
       enough {{ Γ ⊢ #0[σ ,, N'] : B[Wk][σ ,, N'] }}...
 
-    + assert (∃ i, {{ Δ ⊢ C : Type@i }}) as [i'] by mauto.
+    + assert (exists i, {{ Δ ⊢ C : Type@i }}) as [i'] by mauto.
       assert {{ Γ ⊢s Wk∘(σ ,, N) ≈ σ : Δ }} by mauto.
       assert {{ Γ ⊢ C[Wk∘(σ ,, N)] ≈ C[σ] : Type@i' }} by mauto.
       assert {{ Δ, B ⊢s Wk : Δ }} by mauto.
       assert {{ Γ ⊢ C[Wk][σ ,, N] ≈ C[σ] : Type@i' }} by mauto.
       assert {{ Δ, B ⊢ #(S x) : C[Wk] }} by mauto.
       enough {{ Γ ⊢ #(S x)[σ ,, N] : C[Wk][σ ,, N] }}...
 
-    + assert (∃ i, {{ Δ ⊢ C : Type@i }}) as []...
+    + assert (exists i, {{ Δ ⊢ C : Type@i }}) as []...
 
   - intros * Hσσ'.
     inversion_clear Hσσ'; (on_all_hyp: gen_presup_IH presup_exp presup_exp_eq presup_sub_eq); clear presup_exp presup_exp_eq presup_sub_eq; repeat split; mauto.

theories/Core/Syntactic/Relations.v

@@ -1,12 +1,6 @@
-Require Import Unicode.Utf8_core.
-Require Import Setoid.
-Require Import Coq.Program.Equality.
+From Coq Require Import Setoid.
 
-Require Import LibTactics.
-Require Import Syntactic.Syntax.
-Require Import Syntactic.System.
-Require Import Syntactic.SystemLemmas.
-Require Import Syntactic.CtxEquiv.
+From Mcltt Require Import Base CtxEquiv LibTactics Syntax System SystemLemmas.
 
 Lemma ctx_eq_refl : forall {Γ}, {{ ⊢ Γ }} -> {{ ⊢ Γ ≈ Γ }}.
 Proof with mauto.
@@ -36,12 +30,12 @@ Add Relation (ctx) (wf_ctx_eq)
     transitivity proved by @ctx_eq_trans
     as ctx_eq.
 
-Add Parametric Relation (Γ : ctx) (T : typ) : (exp) (λ t t', {{ Γ ⊢ t ≈ t' : T }})
-    symmetry proved by (λ t t', wf_exp_eq_sym Γ t t' T)
-    transitivity proved by (λ t t' t'', wf_exp_eq_trans Γ t t' T t'')
+Add Parametric Relation (Γ : ctx) (T : typ) : (exp) (fun t t' => {{ Γ ⊢ t ≈ t' : T }})
+    symmetry proved by (fun t t' => wf_exp_eq_sym Γ t t' T)
+    transitivity proved by (fun t t' t'' => wf_exp_eq_trans Γ t t' T t'')
     as exp_eq.                                                
 
-Add Parametric Relation (Γ Δ : ctx) : (sub) (λ σ τ, {{ Γ ⊢s σ ≈ τ : Δ }})
-    symmetry proved by (λ σ τ, wf_sub_eq_sym Γ σ τ Δ)
-    transitivity proved by (λ σ τ ρ, wf_sub_eq_trans Γ σ τ Δ ρ)
+Add Parametric Relation (Γ Δ : ctx) : (sub) (fun σ τ => {{ Γ ⊢s σ ≈ τ : Δ }})
+    symmetry proved by (fun σ τ => wf_sub_eq_sym Γ σ τ Δ)
+    transitivity proved by (fun σ τ ρ => wf_sub_eq_trans Γ σ τ Δ ρ)
     as sub_eq.

theories/Core/Syntactic/Syntax.v

@@ -1,5 +1,6 @@
-Require Import String.
-Require Import List.
+From Coq Require Import List String.
+
+From Mcltt Require Import Base.
 
 (* CST term *)
 Module Cst.
@@ -37,6 +38,9 @@ with sub : Set :=
 | a_compose : sub -> sub -> sub
 | a_extend : sub -> exp -> sub.
 
+Notation ctx := (list exp).
+Notation typ := exp.
+
 Fixpoint nat_to_exp n : exp :=
   match n with
   | 0 => a_zero
@@ -60,39 +64,87 @@ Definition exp_to_num e :=
   | None => None
   end.
 
-#[global] Declare Custom Entry exp.
-#[global] Declare Scope exp_scope.
-#[global] Delimit Scope exp_scope with exp.
 #[global] Bind Scope exp_scope with exp.
 #[global] Bind Scope exp_scope with sub.
-#[global] Bind Scope exp_scope with Sortclass.
 Open Scope exp_scope.
-Open Scope nat_scope.
+
+#[global] Declare Custom Entry exp.
 
 Notation "{{{ x }}}" := x (at level 0, x custom exp at level 99, format "'{{{'  x  '}}}'") : exp_scope.
 Notation "( x )" := x (in custom exp at level 0, x custom exp at level 60) : exp_scope.
 Notation "~ x" := x (in custom exp at level 0, x constr at level 0) : exp_scope.
-Notation "x" := x (in custom exp at level 0, x constr at level 0) : exp_scope.
+Notation "x" := x (in custom exp at level 0, x global) : exp_scope.
 Notation "e [ s ]" := (a_sub e s) (in custom exp at level 0, s custom exp at level 60) : exp_scope.
-Notation "'λ' T e" := (a_fn T e) (in custom exp at level 0, T custom exp at level 0, e custom exp at level 60) : exp_scope.
+Notation "'λ' A e" := (a_fn A e) (in custom exp at level 0, A custom exp at level 0, e custom exp at level 60) : exp_scope.
 Notation "f x .. y" := (a_app .. (a_app f x) .. y) (in custom exp at level 40, f custom exp, x custom exp at next level, y custom exp at next level) : exp_scope.
 Notation "'ℕ'" := a_nat (in custom exp) : exp_scope.
 Notation "'Type' @ n" := (a_typ n) (in custom exp at level 0, n constr at level 0) : exp_scope.
-Notation "'Π' T S" := (a_pi T S) (in custom exp at level 0, T custom exp at level 0, S custom exp at level 60) : exp_scope.
-Number Notation exp num_to_exp exp_to_num : exp_scope.
+Notation "'Π' A B" := (a_pi A B) (in custom exp at level 0, A custom exp at level 0, B custom exp at level 60) : exp_scope.
 Notation "'zero'" := a_zero (in custom exp at level 0) : exp_scope.
 Notation "'succ' e" := (a_succ e) (in custom exp at level 0, e custom exp at level 0) : exp_scope.
-Notation "'rec' e 'return' m | 'zero' -> ez | 'succ' -> es 'end'" := (a_natrec m ez es e) (in custom exp at level 0, m custom exp at level 60, ez custom exp at level 60, es custom exp at level 60, e custom exp at level 60) : exp_scope.
+Notation "'rec' e 'return' A | 'zero' -> ez | 'succ' -> es 'end'" := (a_natrec A ez es e) (in custom exp at level 0, A custom exp at level 60, ez custom exp at level 60, es custom exp at level 60, e custom exp at level 60) : exp_scope.
 Notation "'#' n" := (a_var n) (in custom exp at level 0, n constr at level 0) : exp_scope.
 Notation "'Id'" := a_id (in custom exp at level 0) : exp_scope.
 Notation "'Wk'" := a_weaken (in custom exp at level 0) : exp_scope.
 
-Notation "⋅" := nil (in custom exp at level 0) : exp_scope.
-Notation "x , y" := (cons y x) (in custom exp at level 50) : exp_scope.
-
 Infix "∘" := a_compose (in custom exp at level 40) : exp_scope.
 Infix ",," := a_extend (in custom exp at level 50) : exp_scope.
 Notation "'q' σ" := ({{{ σ ∘ Wk ,, # 0 }}}) (in custom exp at level 30) : exp_scope.
 
-Notation ctx := (list exp).
-Notation typ := exp.
+Notation "⋅" := nil (in custom exp at level 0) : exp_scope.
+Notation "x , y" := (cons y x) (in custom exp at level 50) : exp_scope.
+
+Inductive nf : Set :=
+| nf_typ : nat -> nf
+| nf_nat : nf
+| nf_zero : nf
+| nf_succ : nf -> nf
+| nf_pi : nf -> nf -> nf
+| nf_fn : nf -> nf -> nf
+| nf_neut : ne -> nf
+with ne : Set :=
+| ne_natrec : nf -> nf -> nf -> ne -> ne
+| ne_app : ne -> nf -> ne
+| ne_var : nat -> ne
+.
+
+#[global] Declare Custom Entry nf.
+
+#[global] Bind Scope exp_scope with nf.
+#[global] Bind Scope exp_scope with ne.
+
+Notation "n{{{ x }}}" := x (at level 0, x custom nf at level 99, format "'n{{{'  x  '}}}'") : exp_scope.
+Notation "( x )" := x (in custom nf at level 0, x custom nf at level 60) : exp_scope.
+Notation "~ x" := x (in custom nf at level 0, x constr at level 0) : exp_scope.
+Notation "x" := x (in custom nf at level 0, x global) : exp_scope.
+Notation "'λ' A e" := (nf_fn A e) (in custom nf at level 0, A custom nf at level 0, e custom nf at level 60) : exp_scope.
+Notation "f x .. y" := (ne_app .. (ne_app f x) .. y) (in custom nf at level 40, f custom nf, x custom nf at next level, y custom nf at next level) : exp_scope.
+Notation "'ℕ'" := nf_nat (in custom nf) : exp_scope.
+Notation "'Type' @ n" := (nf_typ n) (in custom nf at level 0, n constr at level 0) : exp_scope.
+Notation "'Π' A B" := (nf_pi A B) (in custom nf at level 0, A custom nf at level 0, B custom nf at level 60) : exp_scope.
+Notation "'zero'" := nf_zero (in custom nf at level 0) : exp_scope.
+Notation "'succ' M" := (nf_succ M) (in custom nf at level 0, M custom nf at level 0) : exp_scope.
+Notation "'rec' M 'return' A | 'zero' -> MZ | 'succ' -> MS 'end'" := (ne_natrec A MZ MS M) (in custom nf at level 0, A custom nf at level 60, MZ custom nf at level 60, MS custom nf at level 60, M custom nf at level 60) : exp_scope.
+Notation "'#' n" := (ne_var n) (in custom nf at level 0, n constr at level 0) : exp_scope.
+Notation "'⇑' M" := (nf_neut M) (in custom nf at level 0, M custom nf at level 0) : exp_scope.
+
+Fixpoint nf_to_exp (M : nf) : exp :=
+  match M with
+  | nf_typ i => a_typ i
+  | nf_nat => a_nat
+  | nf_zero => a_zero
+  | nf_succ M => a_succ (nf_to_exp M)
+  | nf_pi A B => a_pi (nf_to_exp A) (nf_to_exp B)
+  | nf_fn A M => a_fn (nf_to_exp A) (nf_to_exp M)
+  | nf_neut M => ne_to_exp M
+  end
+with ne_to_exp (M : ne) : exp :=
+  match M with
+  | ne_natrec A MZ MS M => a_natrec (nf_to_exp A) (nf_to_exp MZ) (nf_to_exp MS) (ne_to_exp M)
+  | ne_app M N => a_app (ne_to_exp M) (nf_to_exp N)
+  | ne_var x => a_var x
+  end
+.
+
+Coercion nf_to_exp : nf >-> exp.
+Coercion ne_to_exp : ne >-> exp.

theories/Core/Syntactic/System.v

@@ -1,11 +1,7 @@
-Require Import List.
-Require Import Unicode.Utf8_core.
+From Coq Require Import List.
 
-Require Import LibTactics.
-Require Import Syntactic.Syntax.
+From Mcltt Require Import Base LibTactics Syntax.
 
-#[global] Declare Custom Entry judg.
-Notation "{{ x }}" := x (at level 0, x custom judg at level 99, format "'{{'  x  '}}'").
 Reserved Notation "⊢ Γ" (in custom judg at level 80, Γ custom exp).
 Reserved Notation "⊢ Γ ≈ Γ'" (in custom judg at level 80, Γ custom exp, Γ' custom exp).
 Reserved Notation "Γ ⊢ M ≈ M' : A" (in custom judg at level 80, Γ custom exp, M custom exp, M' custom exp, A custom exp).