add start of jfp-pearl nov 2023

coq/jfp-swiestra-2023-Nov.v

@@ -0,0 +1,96 @@
+Require Import List.
+Import ListNotations.
+
+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.
+
+
+Module SKI.
+  Inductive term: forall (τ: type), typeDe τ -> Type :=
+  | I: forall τ: type,
+      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 :=
+| Here: forall (a:A) (ls:list A),
+    ref a (a::ls)
+| Further: forall (a x: A) (ls: list A),
+    ref a ls -> ref a (x::ls).
+(* Arguments ref: clear implicits. *)
+
+Inductive env: list type -> Type :=
+| ENil: env []
+| ECons: forall (τs: list type) (τ: type),
+    typeDe τ -> env τs -> env (τ::τs).
+
+Fixpoint lookup {τ: type}: forall {τs: list type}, ref τ τs -> env τs -> typeDe τ.
+refine(fun τs rf en => _).
+refine (
+  match rf with
+  | Here _ _ => 
+      match en with
+      | ENil => _
+      | ECons _ _ v _ => v
+      end
+  | Further _ _ τs' rf' => _
+  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 :=
+| Var: forall (Γ:ctxt) (τ: type),
+    ref τ Γ -> term Γ τ
+| App: forall (Γ: ctxt) (τ1 τ2: type),
+    term Γ (Arrow τ1 τ2)
+ -> term Γ τ1
+ -> term Γ τ2
+| Abs: forall (Γ: ctxt) (τ1 τ2: type),
+    term (τ1 :: Γ) τ2
+ -> term Γ (Arrow τ1 τ2).
+
+(* Variables with their types *)
+Inductive env: ctxt -> Type :=
+| ENil: env []
+| ECons: forall (Γ: ctxt) (τ: type),
+    typeDe τ -> env Γ -> env (τ :: Γ).
+
+(* Find a value in an environment *)
+Fixpoint lookup {Γ: ctxt} {τ: type}
+  (rf: ref τ Γ): typeDe τ.
+refine (
+  match rf with
+  | Here a Γ' => _
+  | Away a _ ls rf' => lookup _ _ rf'
+  end).