[coq] use equations plugin for jfp pearl nov 2023
This commit is contained in:
parent
3a63656658
commit
9a69fea179
|
@ -1,6 +1,11 @@
|
||||||
Require Import List.
|
Require Import List.
|
||||||
Import ListNotations.
|
Import ListNotations.
|
||||||
|
|
||||||
|
Require Import ssreflect.
|
||||||
|
|
||||||
|
From Equations Require Import Equations.
|
||||||
|
|
||||||
|
|
||||||
Inductive type: Type :=
|
Inductive type: Type :=
|
||||||
| BVal: type
|
| BVal: type
|
||||||
| NVal: type
|
| NVal: type
|
||||||
|
@ -13,84 +18,132 @@ Fixpoint typeDe (t: type): Type :=
|
||||||
| Arrow t1 t2 => (typeDe t1) -> (typeDe t2)
|
| Arrow t1 t2 => (typeDe t1) -> (typeDe t2)
|
||||||
end.
|
end.
|
||||||
|
|
||||||
|
Declare Scope ty_scope.
|
||||||
Module SKI.
|
Delimit Scope ty_scope with ty.
|
||||||
Inductive term: forall (τ: type), typeDe τ -> Type :=
|
Notation "'⟦' t '⟧'" := (typeDe t) (at level 20): ty_scope.
|
||||||
| I: forall τ: type,
|
Infix "⇒" := Arrow (at level 25, right associativity): ty_scope.
|
||||||
term (Arrow τ τ)
|
|
||||||
(fun x => x)
|
|
||||||
| K: forall τ1 τ2: type,
|
|
||||||
term (Arrow τ1 (Arrow τ2 τ1))
|
|
||||||
(fun v1 v2 => v1).
|
|
||||||
End SKI.
|
|
||||||
|
|
||||||
(* Definition ctxt: Type := list type. *)
|
|
||||||
|
|
||||||
|
|
||||||
Inductive ref {A: Type}: A -> list A -> Type :=
|
Inductive ref {A: Type}: A -> list A -> Type :=
|
||||||
| Here: forall (a:A) (ls:list A),
|
| Here: forall (a:A) (ls:list A),
|
||||||
ref a (a::ls)
|
ref a (a::ls)
|
||||||
| Further: forall (a x: A) (ls: list A),
|
| Further: forall (a x: A) (ls: list A),
|
||||||
ref a ls -> ref a (x::ls).
|
ref a ls -> ref a (x::ls).
|
||||||
(* Arguments ref: clear implicits. *)
|
|
||||||
|
(* 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 :=
|
Inductive env: list type -> Type :=
|
||||||
| ENil: env []
|
| ENil: env []
|
||||||
| ECons: forall (τs: list type) (τ: type),
|
| ECons: forall (τs: list type) (τ: type),
|
||||||
typeDe τ -> env τs -> env (τ::τs).
|
typeDe τ -> env τs -> env (τ::τs).
|
||||||
|
|
||||||
Fixpoint lookup {τ: type}: forall {τs: list type}, ref τ τs -> env τs -> typeDe τ.
|
(* Fixpoint lookup {t: type} {ts: list type} (en: env ts): ref t ts -> typeDe t. refine ( *)
|
||||||
refine(fun τs rf en => _).
|
(* match en with *)
|
||||||
refine (
|
(* | ENil => fun rf => _ *)
|
||||||
match rf with
|
(* | ECons ts' t' v en' => fun rf => *)
|
||||||
| Here _ _ =>
|
(* (match rf with *)
|
||||||
match en with
|
(* | Here _ _ => *)
|
||||||
| ENil => _
|
(* fun ts' t v en' => _ *)
|
||||||
| ECons _ _ v _ => v
|
(* | Further _ _ _ rf' => *)
|
||||||
end
|
(* fun ts' t v en' => _ *)
|
||||||
| Further _ _ τs' rf' => _
|
(* end) ts' t v en' _ *)
|
||||||
end).
|
(* end). *)
|
||||||
shelve.
|
|
||||||
refine (
|
|
||||||
match en with
|
|
||||||
| ENil => _
|
|
||||||
| ECons _ _ v _ => _
|
|
||||||
end).
|
|
||||||
Check lookup _ _ rf' τs'.
|
|
||||||
|
|
||||||
Fixpoint lookup {τs: list type} {τ: type} (rf: ref τ τs) (en: env τs): typeDe τ.
|
|
||||||
refine(
|
|
||||||
match rf with
|
|
||||||
| Here _ _ =>
|
|
||||||
match en with
|
|
||||||
| ENil => _
|
|
||||||
| ECons _ _ v _ => _
|
|
||||||
end
|
|
||||||
| Further _ _ _ rf' => lookup _ _ rf' en
|
|
||||||
end).
|
|
||||||
|
|
||||||
Inductive term: ctxt -> type -> Type :=
|
(* https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Lookup.20env.20with.20dependent.20types *)
|
||||||
| Var: forall (Γ:ctxt) (τ: type),
|
Equations lookupEnv {τ: type} {τs: list type}
|
||||||
ref τ Γ -> term Γ τ
|
(en: env τs) (rf: ref τ τs): typeDe τ :=
|
||||||
| App: forall (Γ: ctxt) (τ1 τ2: type),
|
lookupEnv (ECons _ _ v _) (Here _ _) := v ;
|
||||||
term Γ (Arrow τ1 τ2)
|
lookupEnv (ECons _ _ _ en') (Further _ _ _ rf') := lookupEnv en' rf'.
|
||||||
-> term Γ τ1
|
|
||||||
-> term Γ τ2
|
|
||||||
| Abs: forall (Γ: ctxt) (τ1 τ2: type),
|
|
||||||
term (τ1 :: Γ) τ2
|
|
||||||
-> term Γ (Arrow τ1 τ2).
|
|
||||||
|
|
||||||
(* Variables with their types *)
|
(* Print lookupEnv. *)
|
||||||
Inductive env: ctxt -> Type :=
|
|
||||||
| ENil: env []
|
|
||||||
| ECons: forall (Γ: ctxt) (τ: type),
|
|
||||||
typeDe τ -> env Γ -> env (τ :: Γ).
|
|
||||||
|
|
||||||
(* Find a value in an environment *)
|
|
||||||
Fixpoint lookup {Γ: ctxt} {τ: type}
|
(* Fixpoint lookupEnv {τs: list type}: env τs -> *)
|
||||||
(rf: ref τ Γ): typeDe τ.
|
(* forall τ:type, ref τ τs -> typeDe τ. refine ( fun en => *)
|
||||||
refine (
|
(* match en with *)
|
||||||
match rf with
|
(* | ENil => fun τ rf => _ *)
|
||||||
| Here a Γ' => _
|
(* | ECons _ _ v en' => fun τ rf => _ *)
|
||||||
| Away a _ ls rf' => lookup _ _ rf'
|
(* (1* match rf' with *1) *)
|
||||||
end).
|
(* (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.
|
||||||
|
|
||||||
|
Compute typeDe (Arrow BVal (Arrow NVal BVal)).
|
||||||
|
Compute typeDe (Arrow (Arrow BVal NVal) BVal).
|
||||||
|
|
||||||
|
Module SKI.
|
||||||
|
Open Scope ty_scope.
|
||||||
|
|
||||||
|
Inductive term: forall (τ: type), env τs -> typeDe τ -> Type :=
|
||||||
|
| I: forall X: type,
|
||||||
|
term (X ⇒ X)
|
||||||
|
(fun x: typeDe X => x)
|
||||||
|
| K: forall X Y: type,
|
||||||
|
term (X ⇒ Y ⇒ X)
|
||||||
|
(fun (x:typeDe X) (y: typeDe Y) => x)
|
||||||
|
| S: forall X Y Z: type,
|
||||||
|
term ((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.
|
||||||
|
|
Loading…
Reference in New Issue