Add domain and related props

theories/Core/Semantic/Domain.v

@@ -0,0 +1,55 @@
+From Mcltt Require Import Syntax.
+
+Reserved Notation "'env'".
+
+Inductive domain : Set :=
+| d_nat : domain
+| d_pi : domain -> env -> exp -> domain
+| d_univ : nat -> domain
+| d_zero : domain
+| d_succ : domain -> domain
+| d_fn : env -> exp -> domain
+| d_neut : domain -> domain_ne -> domain
+with domain_ne : Set :=
+(** Notice that the number x here is not a de Bruijn index but an absolute
+    representation of names.  That is, this number does not change relative to the
+    binding structure it currently exists in.
+ *)
+| d_var : forall (x : nat), domain_ne
+| d_app : domain_ne -> domain_nf -> domain_ne
+| d_natrec : env -> typ -> domain -> exp -> domain_ne -> domain_ne
+with domain_nf : Set :=
+| d_dom : domain -> domain -> domain_nf
+where "'env'" := (nat -> domain).
+
+#[global] Declare Custom Entry domain.
+#[global] Bind Scope exp_scope with domain.
+
+Notation "'d{{{' x '}}}'" := x (at level 0, x custom domain at level 99) : exp_scope.
+Notation "( x )" := x (in custom domain at level 0, x custom domain at level 60) : exp_scope.
+Notation "~ x" := x (in custom domain at level 0, x constr at level 0) : exp_scope.
+Notation "x" := x (in custom domain at level 0, x global) : exp_scope.
+Notation "'λ' p M" := (d_fn p M) (in custom domain at level 0, p custom domain at level 30, M custom exp at level 30) : exp_scope.
+Notation "f x .. y" := (d_app .. (d_app f x) .. y) (in custom domain at level 40, f custom domain, x custom domain at next level, y custom domain at next level) : exp_scope.
+Notation "'ℕ'" := d_nat (in custom domain) : exp_scope.
+Notation "'𝕌' @ n" := (d_univ n) (in custom domain at level 0, n constr at level 0) : exp_scope.
+Notation "'Π' a p B" := (d_pi a p B) (in custom domain at level 0, a custom domain at level 30, p custom domain at level 0, B custom exp at level 30) : exp_scope.
+Notation "'zero'" := d_zero (in custom domain at level 0) : exp_scope.
+Notation "'succ' m" := (d_succ m) (in custom domain at level 30, m custom domain at level 30) : exp_scope.
+Notation "'rec' m 'under' p 'return' P | 'zero' -> mz | 'succ' -> MS 'end'" := (d_natrec p P mz MS m) (in custom domain at level 0, P custom exp at level 60, mz custom domain at level 60, MS custom exp at level 60, p custom domain at level 60, m custom domain at level 60) : exp_scope.
+Notation "'!' n" := (d_var n) (in custom domain at level 0, n constr at level 0) : exp_scope.
+Notation "'⇑' a m" := (d_neut a m) (in custom domain at level 0, a custom domain at level 30, m custom domain at level 30) : exp_scope.
+Notation "'⇓' a m" := (d_dom a m) (in custom domain at level 0, a custom domain at level 30, m custom domain at level 30) : exp_scope.
+Notation "'⇑!' a n" := (d_neut a (d_var n)) (in custom domain at level 0, a custom domain at level 30, n constr at level 0) : exp_scope.
+
+Definition empty_env : env := fun x => d{{{ zero }}}.
+Definition extend_env (p : env) (d : domain) : env :=
+  fun n =>
+    match n with
+    | 0 => d
+    | S n' => p n'
+    end.
+Notation "p ↦ m" := (extend_env p m) (in custom domain at level 20, left associativity) : exp_scope.
+
+Definition drop_env (p : env) : env := fun n => p (S n).
+Notation "p '↯'" := (drop_env p) (in custom domain at level 10, p custom domain) : exp_scope.

theories/Core/Semantic/Evaluate.v

@@ -0,0 +1,77 @@
+From Mcltt Require Import Base.
+From Mcltt Require Import Domain.
+From Mcltt Require Import Syntax.
+From Mcltt Require Import System.
+
+Reserved Notation "'⟦' M '⟧' p '↘' r" (in custom judg at level 80, M custom exp at level 99, p custom domain at level 99, r custom domain at level 99).
+Reserved Notation "'rec' m '⟦return' A | 'zero' -> MZ | 'succ' -> MS 'end⟧' p '↘' r" (in custom judg at level 80, m custom domain at level 99, A custom exp at level 99, MZ custom exp at level 99, MS custom exp at level 99, p custom domain at level 99, r custom domain at level 99).
+Reserved Notation "'$|' m '&' n '|↘' r" (in custom judg at level 80, m custom domain at level 99, n custom domain at level 99, r custom domain at level 99).
+Reserved Notation "'⟦' σ '⟧s' p '↘' p'" (in custom judg at level 80, σ custom exp at level 99, p custom domain at level 99, p' custom domain at level 99).
+
+Generalizable All Variables.
+
+Inductive eval_exp : exp -> env -> domain -> Prop :=
+| eval_exp_typ :
+  `( {{ ⟦ Type@i ⟧ p ↘ 𝕌@i }} )
+| eval_exp_nat :
+  `( {{ ⟦ ℕ ⟧ p ↘ 𝕟 }} )
+| eval_exp_zero :
+  `( {{ ⟦ zero ⟧ p ↘ zero }} )
+| eval_exp_succ :
+  `( {{ ⟦ M ⟧ p ↘ m }} ->
+     {{ ⟦ succ M ⟧ p ↘ succ m }} )
+| eval_exp_natrec :
+  `( {{ ⟦ M ⟧ p ↘ m }} ->
+     {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r }} ->
+     {{ ⟦ rec M return A | zero -> MZ | succ -> MS end ⟧ p ↘ r }} )
+| eval_exp_pi :
+  `( {{ ⟦ A ⟧ p ↘ a }} ->
+     {{ ⟦ Π A B ⟧ p ↘ Π a p B }} )
+| eval_exp_fn :
+  `( {{ ⟦ λ A M ⟧ p ↘ λ p M }} )
+| eval_exp_app :
+  `( {{ ⟦ M ⟧ p ↘ m }} ->
+     {{ ⟦ N ⟧ p ↘ n }} ->
+     {{ $| m & n |↘ r }} ->
+     {{ ⟦ M N ⟧ p ↘ r }} )
+| eval_exp_sub :
+  `( {{ ⟦ σ ⟧s p ↘ p' }} ->
+     {{ ⟦ M ⟧ p' ↘ m }} ->
+     {{ ⟦ M[σ] ⟧ p ↘ m }} )
+where "'⟦' e '⟧' p '↘' r" := (eval_exp e p r) (in custom judg)
+with eval_natrec : exp -> exp -> exp -> domain -> env -> domain -> Prop :=
+| eval_natrec_zero :
+  `( {{ ⟦ MZ ⟧ p ↘ mz }} ->
+     {{ rec zero ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ mz }} )
+| eval_natrec_succ :
+  `( {{ rec b ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r }} ->
+     {{ ⟦ MS ⟧ p ↦ b ↦ r ↘ ms }} ->
+     {{ rec succ b ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ ms }} )
+| eval_natrec_neut :
+  `( {{ ⟦ MZ ⟧ p ↘ mz }} ->
+     {{ ⟦ A ⟧ p ↦ ⇑ 𝕟 m ↘ a }} ->
+     {{ rec ⇑ 𝕟 m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ ⇑ a (rec m under p return A | zero -> mz | succ -> MS end) }} )
+where "'rec' m '⟦return' A | 'zero' -> MZ | 'succ' -> MS 'end⟧' p '↘' r" := (eval_natrec A MZ MS m p r) (in custom judg)
+with eval_app : domain -> domain -> domain -> Prop :=
+| eval_app_fn :
+  `( {{ ⟦ M ⟧ p ↦ n ↘ m }} ->
+     {{ $| λ p M & n |↘ m }} )
+| eval_app_neut :
+  `( {{ ⟦ B ⟧ p ↦ n ↘ b }} ->
+     {{ $| ⇑ (Π a p B) m & n |↘ ⇑ b (m (⇓ a N)) }} )
+where "'$|' m '&' n '|↘' r" := (eval_app m n r) (in custom judg)
+with eval_sub : sub -> env -> env -> Prop :=
+| eval_sub_id :
+  `( {{ ⟦ Id ⟧s p ↘ p }} )
+| eval_sub_weaken :
+  `( {{ ⟦ Wk ⟧s p ↘ p↯ }} )
+| eval_sub_extend :
+  `( {{ ⟦ σ ⟧s p ↘ p' }} ->
+     {{ ⟦ M ⟧ p ↘ m }} ->
+     {{ ⟦ σ ,, M ⟧s p ↘ p' ↦ m }} )
+| eval_sub_compose :
+  `( {{ ⟦ τ ⟧s p ↘ p' }} ->
+     {{ ⟦ σ ⟧s p' ↘ p'' }} ->
+     {{ ⟦ σ ∘ τ ⟧s p ↘ p'' }} )
+where "'⟦' σ '⟧s' p '↘' p'" := (eval_sub σ p p') (in custom judg)
+.

theories/Core/Semantic/Readback.v

@@ -0,0 +1,83 @@
+From Mcltt Require Import Base.
+From Mcltt Require Import Domain.
+From Mcltt Require Import Evaluate.
+From Mcltt Require Import Syntax.
+From Mcltt Require Import System.
+
+Reserved Notation "'Rnf' m 'in' s ↘ M" (in custom judg at level 80, m custom domain, s constr, M custom nf).
+Reserved Notation "'Rne' m 'in' s ↘ M" (in custom judg at level 80, m custom domain, s constr, M custom nf).
+Reserved Notation "'Rtyp' m 'in' s ↘ M" (in custom judg at level 80, m custom domain, s constr, M custom nf).
+
+Generalizable All Variables.
+
+Inductive read_nf : nat -> domain_nf -> nf -> Prop :=
+| read_nf_type :
+  `( {{ Rtyp a in s ↘ A }} ->
+     {{ Rnf ⇓ 𝕌@i a in s ↘ A }} )
+| read_nf_zero :
+  `( {{ Rnf ⇓ ℕ zero in s ↘ zero }} )
+| read_nf_succ :
+  `( {{ Rnf ⇓ ℕ m in s ↘ M }} ->
+     {{ Rnf ⇓ ℕ (succ m) in s ↘ succ M }} )
+| read_nf_nat_neut :
+  `( {{ Rne m in s ↘ M }} ->
+     {{ Rnf ⇓ ℕ (⇑ ℕ m) in s ↘ ⇑ M }} )
+| read_nf_fn :
+  (* Nf of arg type *)
+  `( {{ Rtyp a in s ↘ A }} ->
+
+     (* Nf of eta-expanded body *)
+     {{ $| m & ⇑! a s |↘ m' }} ->
+     {{ ⟦ B ⟧ p ↦ ⇑! a s ↘ b }} ->
+     {{ Rnf ⇓ b m' in S s ↘ M }} ->
+
+     {{ Rnf ⇓ (Π a p B) m in s ↘ λ A M }} )
+| read_nf_neut :
+  `( {{ Rne m in s ↘ M }} ->
+     {{ Rnf ⇓ (⇑ a b) (⇑ c m) in s ↘ ⇑ M }} )
+where "'Rnf' m 'in' s ↘ M" := (read_nf s m M) (in custom judg) : exp_scope
+with read_ne : nat -> domain_ne -> ne -> Prop :=
+| read_ne_var :
+  `( {{ Rne !x in s ↘ #(s - x - 1) }} )
+| read_ne_app :
+  `( {{ Rne m in s ↘ M }} ->
+     {{ Rnf n in s ↘ N }} ->
+     {{ Rne m n in s ↘ M N }} )
+| read_ne_natrec :
+  (* Nf of motive *)
+  `( {{ ⟦ B ⟧ p ↦ ⇑! ℕ s ↘ b }} ->
+     {{ Rtyp b in S s ↘ B' }} ->
+
+     (* Nf of mz *)
+     {{ ⟦ B ⟧ p ↦ zero ↘ bz }} ->
+     {{ Rnf ⇓ bz mz in s ↘ MZ }} ->
+
+     (* Nf of MS *)
+     {{ ⟦ B ⟧ p ↦ succ (⇑! ℕ s) ↘ bs }} ->
+     {{ ⟦ MS ⟧ p ↦ ⇑! ℕ s ↦ ⇑! b (S s) ↘ ms }} ->
+     {{ Rnf ⇓ bs ms in S (S s) ↘ MS' }} ->
+
+     (* Ne of m *)
+     {{ Rne m in s ↘ M }} ->
+
+     {{ Rne rec m under p return B | zero -> mz | succ -> MS end in s ↘ rec M return B' | zero -> MZ | succ -> MS' end }} )
+where "'Rne' m 'in' s ↘ M" := (read_ne s m M) (in custom judg) : exp_scope
+with read_typ : nat -> domain -> nf -> Prop :=
+| read_typ_univ :
+  `( {{ Rtyp 𝕌@i in s ↘ Type@i }} )
+| read_typ_nat :
+  `( {{ Rtyp ℕ in s ↘ ℕ }} )
+| read_typ_pi :
+  (* Nf of arg type *)
+  `( {{ Rtyp a in s ↘ A }} ->
+
+     (* Nf of ret type *)
+     {{ ⟦ B ⟧ p ↦ ⇑! a s ↘ b }} ->
+     {{ Rtyp b in S s ↘ B' }} ->
+
+     {{ Rtyp Π a p B in s ↘ Π A B' }})
+| read_typ_neut :
+  `( {{ Rne b in s ↘ B }} ->
+     {{ Rtyp ⇑ a b in s ↘ ⇑ B }})
+where "'Rtyp' m 'in' s ↘ M" := (read_typ s m M) (in custom judg) : exp_scope
+.

theories/_CoqProject

@@ -3,6 +3,9 @@
 -arg -w -arg -notation-overridden
 
 ./Core/Base.v
+./Core/Semantic/Domain.v
+./Core/Semantic/Evaluate.v
+./Core/Semantic/Readback.v
 ./Core/Syntactic/CtxEquiv.v
 ./Core/Syntactic/Presup.v
 ./Core/Syntactic/Relations.v