210 lines
7.1 KiB
Coq
210 lines
7.1 KiB
Coq
Require Import List.
|
||
Import ListNotations.
|
||
|
||
Require Import ssreflect.
|
||
|
||
From Equations Require Import Equations.
|
||
|
||
|
||
Inductive type: Type :=
|
||
| BVal: type
|
||
| NVal: type
|
||
| Arrow: type -> type -> type.
|
||
|
||
Fixpoint typeDe (t: type): Type :=
|
||
match t with
|
||
| BVal => bool
|
||
| NVal => nat
|
||
| Arrow t1 t2 => (typeDe t1) -> (typeDe t2)
|
||
end.
|
||
|
||
Declare Scope ty_scope.
|
||
Delimit Scope ty_scope with ty.
|
||
Notation "'⟦' t '⟧'" := (typeDe t) (at level 20): ty_scope.
|
||
Infix "⇒" := Arrow (at level 25, right associativity): ty_scope.
|
||
|
||
Inductive ref {A: Type}: A -> list A -> Type :=
|
||
| Here: forall (a:A) (ls:list A),
|
||
ref a (a::ls)
|
||
| Further: forall {a: A} {ls: list A} (x: A),
|
||
ref a ls -> ref a (x::ls).
|
||
|
||
(* Theorem refListNonNil: forall {A: Type} (a:A) (ls: list A), *)
|
||
(* ref a ls -> ls <> nil. *)
|
||
(* Proof. *)
|
||
(* move => A a ls H. *)
|
||
(* by elim: H. *)
|
||
(* Qed. *)
|
||
|
||
Inductive env: list type -> Type :=
|
||
| ENil: env []
|
||
| ECons: forall {τs: list type} {τ: type},
|
||
typeDe τ -> env τs -> env (τ::τs).
|
||
(* ⣤ ‼ *)
|
||
|
||
(* Fixpoint lookup {t: type} {ts: list type} (en: env ts): ref t ts -> typeDe t. refine ( *)
|
||
(* match en with *)
|
||
(* | ENil => fun rf => _ *)
|
||
(* | ECons ts' t' v en' => fun rf => *)
|
||
(* (match rf with *)
|
||
(* | Here _ _ => *)
|
||
(* fun ts' t v en' => _ *)
|
||
(* | Further _ _ _ rf' => *)
|
||
(* fun ts' t v en' => _ *)
|
||
(* end) ts' t v en' _ *)
|
||
(* end). *)
|
||
|
||
|
||
(* https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Lookup.20env.20with.20dependent.20types *)
|
||
Equations lookupEnv {τ: type} {τs: list type}
|
||
(en: env τs) (rf: ref τ τs): typeDe τ :=
|
||
lookupEnv (ECons v _) (Here _ _) := v ;
|
||
lookupEnv (ECons _ en') (Further _ rf') := lookupEnv en' rf'.
|
||
|
||
(* Print lookupEnv. *)
|
||
|
||
|
||
(* Fixpoint lookupEnv {τs: list type}: env τs -> *)
|
||
(* forall τ:type, ref τ τs -> typeDe τ. refine ( fun en => *)
|
||
(* match en with *)
|
||
(* | ENil => fun τ rf => _ *)
|
||
(* | ECons _ _ v en' => fun τ rf => _ *)
|
||
(* (1* match rf' with *1) *)
|
||
(* (1* | Here τ _ => _ *1) *)
|
||
(* (1* | Further _ _ _ rf' => _ *1) *)
|
||
(* (1* end *1) *)
|
||
(* end). *)
|
||
(* - by pose proof (refListNonNil _ _ rf). *)
|
||
(* - destruct rf as [a ls | a a0 ls rf'] eqn:HcaseRef. *)
|
||
|
||
Module LC.
|
||
Inductive term: list type -> type -> Type :=
|
||
| Var: forall (τs: list type) (τ: type),
|
||
ref τ τs -> term τs τ
|
||
| App: forall (τs: list type) (τ1 τ2: type),
|
||
term τs (Arrow τ1 τ2) -> term τs τ1 -> term τs τ2
|
||
| Abs: forall (τs: list type) (τ1 τ2: type),
|
||
term (τ1 :: τs) τ2 -> term τs (Arrow τ1 τ2).
|
||
|
||
Fixpoint termDe {τs: list type} {τ: type}
|
||
(tm: term τs τ): env τs -> typeDe τ :=
|
||
match tm with
|
||
| Var _ _ rf =>
|
||
fun en => lookupEnv en rf
|
||
| App _ _ _ tm1 tm2 =>
|
||
fun en => (termDe tm1 en) (termDe tm2 en)
|
||
| Abs _ _ _ f =>
|
||
fun en v => termDe f (ECons v en)
|
||
end.
|
||
|
||
(* This would've worked too. *)
|
||
(* Equations termDe {Γ: list type} {τ: type} *)
|
||
(* (tm: term Γ τ) (en: env Γ): typeDe τ := *)
|
||
(* termDe (Var _ _ rf) en := lookupEnv en rf; *)
|
||
(* termDe (App _ _ _ tm1 tm2) en := (termDe tm1 en) (termDe tm2 en); *)
|
||
(* termDe (Abs _ _ _ f) en := fun v => termDe f (ECons _ _ v en). *)
|
||
(* Print termDe. *)
|
||
End LC.
|
||
|
||
Module SKI.
|
||
Open Scope ty_scope.
|
||
|
||
Inductive term {τs: list type}: forall (τ: type),
|
||
(env τs -> typeDe τ) -> Type :=
|
||
| I: forall (τ: type),
|
||
term (τ ⇒ τ)
|
||
(fun (en: env τs) (x: ⟦τ⟧) => x)
|
||
| K: forall (τ1 τ2: type),
|
||
term (τ1 ⇒ τ2 ⇒ τ1)
|
||
(fun (en: env τs) (x1: ⟦τ1⟧) (x2: ⟦τ2⟧) => x1)
|
||
| S: forall (τa τb τx: type),
|
||
term ((τx ⇒ τa ⇒ τb) ⇒ (τx ⇒ τa) ⇒ τx ⇒ τb)
|
||
(fun (en: env τs)
|
||
(f: ⟦τx ⇒ τa ⇒ τb⟧) (g: ⟦τx ⇒ τa⟧) (x: ⟦τx⟧) =>
|
||
(f x) (g x))
|
||
| Var: forall (τ: type)
|
||
(rf: ref τ τs),
|
||
term τ (fun (en: env τs) => lookupEnv en rf)
|
||
| App: forall {τa τb: type} {f: ⟦τa ⇒ τb⟧} {b: ⟦τb⟧},
|
||
term (τa ⇒ τb) (fun en: env τs => f) ->
|
||
term τb (fun en: env τs => b) ->
|
||
term ((τa ⇒ τb) ⇒ τa ⇒ τb)
|
||
(fun (en: env τs) (f: ⟦τa ⇒ τb⟧) (a: ⟦τa⟧) => f a).
|
||
#[global] Arguments term: clear implicits.
|
||
|
||
(* Equations abs {σ τ: type} {τs: list type} {f: env (σ::τs) -> typeDe τ} *)
|
||
(* (t: term (σ::τs) τ f) *)
|
||
(* : term τs (σ ⇒ τ) (fun (en: env τs) => (fun (x: ⟦σ⟧) => f (ECons x en))) := *)
|
||
(* abs (I _) => App (K _ _) (I _). *)
|
||
(* abs (K _ _ _) => _; *)
|
||
(* abs (S _ _ _ _) => _; *)
|
||
(* abs (Var _ _ rf) => _; *)
|
||
(* abs (App _ _) => _. *)
|
||
|
||
Fixpoint abs {σ τ: type} {τs: list type} {f: env (σ::τs) -> typeDe τ}
|
||
(tm: term (σ::τs) τ f)
|
||
: term τs (σ ⇒ τ) (fun (en: env τs) => (fun (x: ⟦σ⟧) => f (ECons x en))).
|
||
refine (
|
||
match tm with
|
||
| I ty => _
|
||
| K _ _ => _
|
||
| S _ _ _ => _
|
||
| Var _ rf => _
|
||
| App _ _ => _
|
||
end).
|
||
- Check (App (K _ _) (I ty)).
|
||
Check (@App τs _ _ _ _ (K τ σ) (I _)).
|
||
Check (App (K _ σ) (I ty)).
|
||
shelve.
|
||
-
|
||
refine (App (K _ _) (I _)).
|
||
|
||
|
||
(* Inductive term: forall (τs: list type) (τ: type), env τs -> typeDe τ -> Type := *)
|
||
(* | I: forall (τs: list type) (τ: type) (en: env τs), *)
|
||
(* term τs (τ ⇒ τ) en (fun x: ⟦τ⟧ => x) *)
|
||
(* | K: forall (τs: list type) (τ1 τ2: type) (en: env τs), *)
|
||
(* term τs (τ1 ⇒ τ2 ⇒ τ1) en (fun (x1: ⟦τ1⟧) (x2: ⟦τ2⟧) => x1) *)
|
||
(* | S: forall (τs: list type) (τa τb τx: type) (en: env τs), *)
|
||
(* term τs ((τx ⇒ τa ⇒ τb) ⇒ (τx ⇒ τa) ⇒ τx ⇒ τb) en *)
|
||
(* (fun (f: ⟦τx ⇒ τa ⇒ τb⟧) (g: ⟦τx ⇒ τa⟧) (x: ⟦τx⟧) => (f x) (g x)). *)
|
||
|
||
|
||
(* Inductive term: forall (τs: list type) (τ: type), *)
|
||
(* env τs -> typeDe τ -> Type := *)
|
||
(* | I: forall (τs: list type) (X: type) (en: env τs), *)
|
||
(* term τs (X ⇒ X) en *)
|
||
(* (fun x: typeDe X => x) *)
|
||
(* | K: forall (τs: list type) (X Y: type), *)
|
||
(* term τs (X ⇒ Y ⇒ X) *)
|
||
(* (fun (x:typeDe X) (y: typeDe Y) => x) *)
|
||
(* | S: forall (τs: list type) (X Y Z: type), *)
|
||
(* term τs ((X ⇒ Y ⇒ Z) ⇒ *)
|
||
(* (X ⇒ Y) ⇒ *)
|
||
(* (X ⇒ Z)) *)
|
||
(* (fun (f: typeDe (X ⇒ Y ⇒ Z)) *)
|
||
(* (g: typeDe (X ⇒ Y)) *)
|
||
(* (x: typeDe X) => (f x) (g x)) *)
|
||
(* | App: forall (X Y: type) (f: typeDe (X ⇒ Y)) (x: typeDe X), *)
|
||
(* term (X ⇒ Y) f -> term X x -> term Y (f x) *)
|
||
(* | Var: forall (X Y: type) (f: typeDe (X ⇒ Y)), *)
|
||
(* term (X ⇒ Y) f -> term X x -> term (X ⇒ Y) f. *)
|
||
|
||
(* Inductive term: forall (τ: type), typeDe τ -> Type := *)
|
||
(* | I: forall X: type, *)
|
||
(* term (Arrow X X) *)
|
||
(* (fun x: typeDe X => x) *)
|
||
(* | K: forall X Y: type, *)
|
||
(* term (Arrow X (Arrow Y X)) *)
|
||
(* (fun (x:typeDe X) (y: typeDe Y) => x) *)
|
||
(* | S: forall X Y Z: type, *)
|
||
(* term (Arrow *)
|
||
(* (Arrow X (Arrow Y Z)) *)
|
||
(* (Arrow *)
|
||
(* (Arrow X Y) *)
|
||
(* (Arrow X Z))) *)
|
||
(* (fun (f: typeDe (Arrow X (Arrow Y Z))) *)
|
||
(* (g: typeDe (Arrow X Y)) *)
|
||
(* (x: typeDe X) => (f x) (g x)). *)
|
||
End SKI.
|