diff --git a/theories/Core/Semantic/Domain.v b/theories/Core/Semantic/Domain.v new file mode 100644 index 00000000..4813dd28 --- /dev/null +++ b/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. diff --git a/theories/Core/Semantic/Evaluate.v b/theories/Core/Semantic/Evaluate.v new file mode 100644 index 00000000..c40c3d07 --- /dev/null +++ b/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) +. diff --git a/theories/Core/Semantic/Readback.v b/theories/Core/Semantic/Readback.v new file mode 100644 index 00000000..13ad389b --- /dev/null +++ b/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 +. diff --git a/theories/_CoqProject b/theories/_CoqProject index 0480f05f..82f5e936 100644 --- a/theories/_CoqProject +++ b/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