Module Problem1. Require Import List. Require Import chap15. Infix "::" := CONS (at level 60, right associativity). Definition MULT : NAT -> NAT -> NAT := fun a : NAT => fun b : NAT => recNAT (fun r : UNIT + NAT => caseu r ZERO (PLUS b)) a. Eval cbv in (MULT 3 5) : nat. Eval cbv in (MULT 3 0) : nat. Definition PRED : NAT -> NAT := fun n : NAT => let (pred, _) := recNAT (fun r : UNIT + (NAT * NAT) => caseu r (ZERO, ZERO) (fun p : NAT * NAT => (snd p, SUCC (snd p)))) n in pred. Eval cbv in (PRED 3) : nat. Eval cbv in (PRED 0) : nat. Definition MINUS : NAT -> NAT -> NAT := fun a : NAT => fun b : NAT => recNAT (fun r : UNIT + NAT => caseu r a PRED) b. Eval cbv in (MINUS 5 3) : nat. Eval cbv in (MINUS 5 7) : nat. Definition GT : NAT -> NAT -> BOOL := fun a : NAT => fun b : NAT => recNAT (fun r : UNIT + BOOL => caseu r FALSE (fun _ => TRUE)) (MINUS a b). Eval cbv in (IFBOOL (GT 4 3) THEN 1 ELSE 0) : nat. Eval cbv in (IFBOOL (GT 4 4) THEN 1 ELSE 0) : nat. Definition LENGTH : LIST -> NAT := fun l : LIST => recLIST (fun r : UNIT + NAT * NAT => caseu r ZERO (fun p : NAT * NAT => SUCC (snd p))) l. Eval cbv in (LENGTH NIL) : nat. Eval cbv in (LENGTH (3 :: 1 :: 2 :: NIL)) : nat. Definition APPEND : LIST -> LIST -> LIST := fun l1 : LIST => fun l2 : LIST => recLIST (fun r : UNIT + NAT * LIST => caseu r l2 (fun p : NAT * LIST => CONS (fst p) (snd p))) l1. Eval cbv in listnat_of_LIST (APPEND NIL NIL). Eval cbv in listnat_of_LIST (APPEND NIL (CONS 3 (CONS 1 NIL))). Eval cbv in listnat_of_LIST (APPEND (CONS 4 (CONS 2 NIL)) (CONS 3 (CONS 1 NIL))). Eval cbv in listnat_of_LIST (APPEND (CONS 4 (CONS 2 NIL)) NIL). Definition POWER : NAT -> STREAM := fun n : NAT => genSTREAM (fun p : NAT => let next := MULT p n in (p, next)) 1. Definition FACTORIAL : STREAM := genSTREAM (fun p : NAT * NAT => let (n, prev) := p in let out := MULT n prev in (out, (SUCC n, out))) (1 : NAT, 1 : NAT). Definition TAKE : STREAM -> NAT -> LIST := fun s : STREAM => fun n : NAT => fst (recNAT (fun r : UNIT + LIST * STREAM => caseu r (NIL, s) (fun p : LIST * STREAM => let (tl, stream) := p in let (hd, stream') := outSTREAM stream in (APPEND tl (hd :: NIL), stream'))) n). Eval cbv in listnat_of_LIST (TAKE (POWER 2) 7). Eval cbv in listnat_of_LIST (TAKE FACTORIAL 5). Definition MERGE : STREAM -> STREAM -> STREAM := fun s1 => fun s2 => genSTREAM (fun p : STREAM * STREAM => let (s1, s2) := p in let (a, s1') := outSTREAM s1 in let (b, s2') := outSTREAM s2 in IFBOOL (GT a b) THEN (b, (s1, s2')) ELSE (a, (s1', s2))) (s1, s2). Eval cbv in listnat_of_LIST (TAKE (MERGE (POWER 2) FACTORIAL) 12). End Problem1. Module Problem2. Definition e0 : forall t, t -> t := fun T : Type => fun x : T => x. (* "fun T : Type" is "Lambda T" *) Definition e1 : forall t1, forall t2, forall t3, (t1 -> t2) -> (t2 -> t3) -> (t1 -> t3) := fun T1 : Type => fun T2 : Type => fun T3 : Type => fun f1 : T1 -> T2 => fun f2 : T2 -> T3 => fun x : T1 => f2 (f1 x). Variable T : Type. Definition e2 : (forall t, t -> t) -> T -> T := fun x : forall t, t -> t => x (T -> T) (x T). (* tau_0 = T -> T tau_1 = T tau_2 = (forall t, t -> t) -> (T -> T) *) Definition e3 : (forall t : Prop, t -> t) -> (forall t : Prop, t -> t) := fun x : forall t : Prop, t -> t => x (forall t : Prop, t -> t) x. (* tau_3 = forall t, t -> t tau_4 = (forall t, t -> t) -> (forall t, t -> t) Need t to be Prop so that (forall t, t -> t) is still Prop If t : Type0 then (forall t, t -> t) : Type1 *) Definition e4 : (forall t, t -> t) -> (forall t, t -> t) := fun x : forall t, t -> t => fun t : Type => x (t -> t) (x t). (* tau_5 = t -> t tau_6 = (forall t, t -> t) -> (forall t, t -> t) *) Definition NAT := forall t, (t -> t) -> t -> t. Definition e5 : NAT -> NAT -> NAT := fun m : NAT => fun n : NAT => fun t : Type => n (t -> t) (m t). (* All are predicative except for e3 (that's why we have to bound t to Prop -- Set and Type are predicative, but Prop is impredicative. *) (* Only e0 and e1 are valid prenex fragments. *) End Problem2. Module Problem3. Inductive STACK := S : forall t, t -> (nat -> t -> t) -> (t -> nat * t + unit) -> STACK. (* isomorphic to exists t, (emp : t, push : nat -> t -> t, pop : t -> nat * t + unit) *) Inductive Stk := Nil : Stk | Cons : nat -> Stk -> Stk. Definition e_impl : STACK := S Stk Nil Cons (* pack Stk with as STACK *) (fun stk : Stk => match stk with | Nil => inr _ tt | Cons n s => inl _ (n, s) end). Inductive STACKext := Sext : forall t, t -> (nat -> t -> t) -> (t -> nat * t + unit) -> (t -> nat + unit) -> STACKext. (* isomorphic to exists t, (emp : t, push : nat -> t -> t, pop : t -> nat * t + unit, peek2 : t -> nat + unit) *) Definition e_client : STACK -> STACKext := fun s => match s with (* open s as *) S typ emp push pop => (* typ with *) Sext typ emp push pop (fun s => match pop s with | inr _ => inr _ tt | inl (_, s') => match pop s' with | inr _ => inr _ tt | inl (n, _) => inl _ n end end) end. (* test cases *) Definition peek2_0 := match e_client e_impl with Sext t emp _ _ peek2 => peek2 emp end. Definition peek2_1 := match e_client e_impl with Sext t emp push _ peek2 => peek2 (push 1 emp) end. Definition peek2_2 := match e_client e_impl with Sext t emp push _ peek2 => peek2 (push 2 (push 1 emp)) end. Definition peek2_3 := match e_client e_impl with Sext t emp push _ peek2 => peek2 (push 3 (push 2 (push 1 emp))) end. Eval cbv in peek2_0. (* inr nat tt *) Eval cbv in peek2_1. (* inr nat tt *) Eval cbv in peek2_2. (* inl unit 1 *) Eval cbv in peek2_3. (* inl unit 2 *) End Problem3. Module Problem4. (* soundness and completeness statement at the end of this file *) Require Import List. Require Import Lists.SetoidPermutation. (* Basic inductive expression definition *) Hypothesis Var : Type. Inductive Expr : Type := | z : Expr | s : Expr -> Expr | ifz : Expr -> Expr -> Var * Expr -> Expr | ap : Expr -> Expr -> Expr | lam : Var * Expr -> Expr | var : Var -> Expr | Fix : Var * Expr -> Expr . Inductive isVal : Expr -> Type := | val_z : isVal z | val_s : forall e, isVal e -> isVal (s e) | val_lam : forall ve, isVal (lam ve) . Fixpoint bisVal (e : Expr) : bool := match e with | z => true | s e' => bisVal e' | lam _ => true | _ => false end. (* Context definition *) Inductive Cxt : Type := | c_here : Cxt | c_s : Cxt -> Cxt | c_ifz : Cxt -> Expr -> Var * Expr -> Cxt | c_ap : Cxt -> Expr -> Cxt . (* interactions between contexts and expressions *) Inductive ExprDecomp : Expr -> Cxt -> Expr -> Type := | d_here : forall e : Expr, ExprDecomp e c_here e | d_s : forall e : Expr, forall E : Cxt, forall e' : Expr, ExprDecomp e E e' -> ExprDecomp (s e) (c_s E) e' | d_ifz : forall e e1 : Expr, forall ve2 : Var * Expr, forall E : Cxt, forall e' : Expr, ExprDecomp e E e' -> ExprDecomp (ifz e e1 ve2) (c_ifz E e1 ve2) e' | d_ap : forall e e1 : Expr, forall E : Cxt, forall e' : Expr, ExprDecomp e E e' -> ExprDecomp (ap e e1) (c_ap E e1) e' . Fixpoint cxtComp (E E' : Cxt) : Cxt := (* E' at the c_here in E *) match E with | c_here => E' | c_s E1 => c_s (cxtComp E1 E') | c_ifz E1 e1 ve2 => c_ifz (cxtComp E1 E') e1 ve2 | c_ap E1 arg => c_ap (cxtComp E1 E') arg end. Fixpoint cxtApp (E : Cxt)(e : Expr) : Expr := match E with | c_here => e | c_s E' => s (cxtApp E' e) | c_ifz E' e1 ve2 => ifz (cxtApp E' e) e1 ve2 | c_ap E' arg => ap (cxtApp E' e) arg end. Definition exprDecomp (E : Cxt)(e : Expr) : ExprDecomp (cxtApp E e) E e. intros. induction E. apply d_here. apply d_s. exact IHE. apply d_ifz. exact IHE. apply d_ap. exact IHE. Defined. Lemma valueNoDecomp (e : Expr)(E : Cxt)(a : Expr) : isVal e -> ExprDecomp e E a -> isVal a. intros val decomp. induction decomp. trivial. inversion val; auto. inversion val; auto. inversion val; auto. Qed. Lemma CxtCompApp (E E' : Cxt)(e : Expr) : cxtApp (cxtComp E E') e = cxtApp E (cxtApp E' e). intros. induction E; unfold cxtComp; unfold cxtApp; fold cxtComp; fold cxtApp. trivial. rewrite IHE; trivial. rewrite IHE; trivial. rewrite IHE; trivial. Qed. Hypothesis subst : list (Var * Expr) -> Expr -> Expr. Hypothesis subst_cong : forall s1 s2 : list (Var * Expr), PermutationA eq s1 s2 -> forall e : Expr, subst s1 e = subst s2 e. (* contextual semantics *) Inductive ExprSem : Expr -> Expr -> Type := | es_ifzz : forall e1 : Expr, forall ve2 : Var * Expr, ExprSem (ifz z e1 ve2) e1 | es_ifzs : forall v : Expr, forall e1 : Expr, forall ve2 : Var * Expr, isVal v -> ExprSem (ifz (s v) e1 ve2) (subst ((fst ve2, v) :: nil) (snd ve2)) | es_ap : forall ve : Var * Expr, forall e' : Expr, ExprSem (ap (lam ve) e') (subst ((fst ve, e') :: nil) (snd ve)) | es_fix : forall ve : Var * Expr, ExprSem (Fix ve) (subst ((fst ve, Fix ve) :: nil) (snd ve)). Inductive CxtSem : Expr -> Expr -> Type := | cs_expr : forall E : Cxt, forall e e' : Expr, ExprSem e e' -> CxtSem (cxtApp E e) (cxtApp E e'). (* control machine *) Inductive Frame : Type := | f_s : Frame | f_ifz : Expr -> Var * Expr -> Frame | f_ap : Expr -> Frame. Definition Stack : Type := list Frame. Fixpoint stackApp (k : Stack)(e : Expr) : Expr := match k with | nil => e | f_s :: k' => stackApp k' (s e) | f_ifz e' ve :: k' => stackApp k' (ifz e e' ve) | f_ap e' :: k' => stackApp k' (ap e e') end. (* isomorphism from Cxt to Stack *) Fixpoint Cxt2Stack (E : Cxt) : Stack := match E with | c_here => nil | c_s E' => Cxt2Stack E' ++ f_s :: nil | c_ifz E' e ve => Cxt2Stack E' ++ f_ifz e ve :: nil | c_ap E' e => Cxt2Stack E' ++ f_ap e :: nil end. Fixpoint Stack2Cxt (s : Stack) : Cxt := match s with | nil => c_here | f_s :: s' => cxtComp (Stack2Cxt s') (c_s c_here) | f_ifz e ve :: s' => cxtComp (Stack2Cxt s') (c_ifz c_here e ve) | f_ap e :: s' => cxtComp (Stack2Cxt s') (c_ap c_here e) end. Lemma appIdent (k : Stack)(e : Expr) : cxtApp (Stack2Cxt k) e = stackApp k e. generalize dependent e. induction k. intros; unfold cxtApp; unfold Stack2Cxt; unfold stackApp; trivial. intro e; elim a. unfold stackApp; fold stackApp. unfold Stack2Cxt; fold Stack2Cxt. rewrite CxtCompApp. rewrite <- IHk. unfold cxtApp at 2; trivial. intros. unfold stackApp; fold stackApp. unfold Stack2Cxt; fold Stack2Cxt. rewrite CxtCompApp. rewrite <- IHk. unfold cxtApp at 2; trivial. intros. unfold stackApp; fold stackApp. unfold Stack2Cxt; fold Stack2Cxt. rewrite CxtCompApp. rewrite <- IHk. unfold cxtApp at 2; trivial. Qed. Lemma CxtCompStack (E E' : Cxt) : Cxt2Stack E' ++ Cxt2Stack E = Cxt2Stack (cxtComp E E'). induction E. unfold cxtComp; unfold Cxt2Stack at 1; symmetry; apply app_nil_end. unfold cxtComp; unfold Cxt2Stack at 2; fold cxtComp; fold Cxt2Stack. rewrite ass_app; rewrite IHE. unfold Cxt2Stack at 2; fold Cxt2Stack; trivial. unfold cxtComp; unfold Cxt2Stack at 2; fold cxtComp; fold Cxt2Stack. rewrite ass_app; rewrite IHE. unfold Cxt2Stack at 2; fold Cxt2Stack; trivial. unfold cxtComp; unfold Cxt2Stack at 2; fold cxtComp; fold Cxt2Stack. rewrite ass_app; rewrite IHE. unfold Cxt2Stack at 2; fold Cxt2Stack; trivial. Qed. (* eval_pair k e == k |> e ret_pair k e == k <| e *) Inductive mach_pair : Type := | eval_pair : Stack -> Expr -> mach_pair | ret_pair : Stack -> Expr -> mach_pair . Inductive MachSem : mach_pair -> mach_pair -> Type := | ms_z : forall k : Stack, MachSem (eval_pair k z) (ret_pair k z) | ms_s : forall (k : Stack)(e : Expr), MachSem (eval_pair k (s e)) (eval_pair (f_s :: k) e) | ms_s_ret : forall (k : Stack)(e : Expr), MachSem (ret_pair (f_s :: k) e) (ret_pair k (s e)) | ms_ifz : forall (k : Stack)(e e1 : Expr)(ve2 : Var * Expr), MachSem (eval_pair k (ifz e e1 ve2)) (eval_pair (f_ifz e1 ve2 :: k) e) | ms_ifzz : forall (k : Stack)(e1 : Expr)(ve2 : Var * Expr), MachSem (ret_pair (f_ifz e1 ve2 :: k) z) (eval_pair k e1) | ms_ifzs : forall (k : Stack)(e e1 : Expr)(ve2 : Var * Expr), MachSem (ret_pair (f_ifz e1 ve2 :: k) (s e)) (eval_pair k (subst ((fst ve2, e) :: nil) (snd ve2))) | ms_lam : forall (k : Stack)(ve : Var * Expr), MachSem (eval_pair k (lam ve)) (ret_pair k (lam ve)) | ms_ap : forall (k : Stack)(e1 e2 : Expr), MachSem (eval_pair k (ap e1 e2)) (eval_pair (f_ap e2 :: k) e1) | ms_ap_ret : forall (k : Stack)(e2 : Expr)(ve : Var * Expr), MachSem (ret_pair (f_ap e2 :: k) (lam ve)) (eval_pair k (subst ((fst ve, e2) :: nil) (snd ve))) | ms_fix : forall (k : Stack)(ve : Var * Expr), MachSem (eval_pair k (Fix ve)) (eval_pair k (subst ((fst ve, Fix ve) :: nil) (snd ve))) . (* generic transitive reflexive closure for relations *) Inductive TransClos {A : Type}(rel : A -> A -> Type) : A -> A -> Type := | Refl : forall a : A, TransClos rel a a | Step : forall a b c : A, rel a b -> TransClos rel b c -> TransClos rel a c. Definition CxtSemClos := TransClos CxtSem. Definition MachSemClos := TransClos MachSem. (* utilities for working on TransClos *) Definition One {A : Type}{rel : A -> A -> Type}{a b : A} : rel a b -> TransClos rel a b := fun r => Step rel a b b r (Refl rel b). Lemma transclos_trans {A : Type}{rel : A -> A -> Type}{a b c : A} : TransClos rel a b -> TransClos rel b c -> TransClos rel a c. intros ab bc. induction ab. trivial. apply Step with b. trivial. auto. Qed. (* Control Machine semantics properties *) (* k |> v --> k <| v *) Lemma machsem_val_ret (e : Expr) : isVal e -> forall k : Stack, MachSemClos (eval_pair k e) (ret_pair k e). intros val. induction e. intro; apply One; apply ms_z. inversion val; intro. apply (transclos_trans (b := eval_pair (f_s :: k) e)). apply One; apply ms_s. apply (transclos_trans (b := ret_pair (f_s :: k) e)). apply IHe; trivial. apply One; apply ms_s_ret. inversion val. inversion val. intro; apply One; apply ms_lam. inversion val. inversion val. Qed. (* k |> e --> k' <| v means v is value *) Lemma machsem_ret_val (e e' : Expr)(k k' : Stack) : MachSem (eval_pair k e) (ret_pair k' e') -> isVal e'. intros mach. inversion mach. apply val_z. apply val_lam. Qed. (* unfolding context to the stack *) Lemma machsem_unfold (e : Expr)(E : Cxt)(e' : Expr) : ExprDecomp e E e' -> forall k : Stack, MachSemClos (eval_pair k e) (eval_pair (Cxt2Stack E ++ k) e'). intros decomp. induction decomp. unfold Cxt2Stack; unfold app. intros; apply Refl. intros k. eapply transclos_trans. eapply One; apply ms_s. unfold Cxt2Stack; fold Cxt2Stack. rewrite app_ass; unfold app at 2. apply IHdecomp. intros k. eapply transclos_trans. eapply One; apply ms_ifz. unfold Cxt2Stack; fold Cxt2Stack. rewrite app_ass; unfold app at 2. apply IHdecomp. intros k. eapply transclos_trans. eapply One; apply ms_ap. unfold Cxt2Stack; fold Cxt2Stack. rewrite app_ass; unfold app at 2. apply IHdecomp. Qed. (* folding the stack to contexts enclosing the value *) Lemma machsem_fold (e : Expr)(E : Cxt)(e' : Expr) : ExprDecomp e E e' -> isVal e -> forall k : Stack, MachSemClos (eval_pair (Cxt2Stack E ++ k) e') (ret_pair k e). intros decomp val k. eapply transclos_trans. apply machsem_val_ret. apply (valueNoDecomp e E e'); trivial. generalize dependent k. induction decomp. unfold Cxt2Stack; unfold app. intros; apply Refl. unfold Cxt2Stack; fold Cxt2Stack. intros k. rewrite app_ass; unfold app at 2. eapply transclos_trans. inversion val. apply IHdecomp; trivial. apply One; apply ms_s_ret. inversion val. inversion val. Qed. (* Existential record: might not be general enough *) Inductive SomeMachSemClos (e e' : Expr) : Type := TheMachSemClos : forall E : Cxt, forall a a' : Expr, ExprDecomp e E a -> ExprDecomp e' E a' -> (forall k : Stack, MachSemClos (eval_pair k a) (eval_pair k a')) -> SomeMachSemClos e e'. (* lemmas for completeness *) Lemma onestep_completeness (e e' : Expr) : CxtSem e e' -> SomeMachSemClos e e'. intros cxt. elim cxt; intros E a a' a2a'. induction a2a'. apply (TheMachSemClos (cxtApp E (ifz z e1 ve2)) (cxtApp E e1) E (ifz z e1 ve2) e1 (exprDecomp E (ifz z e1 ve2)) (exprDecomp E e1)). intro k; apply (transclos_trans (b := ret_pair (f_ifz e1 ve2 :: k) z)). apply (transclos_trans (b := eval_pair (f_ifz e1 ve2 :: k) z)). apply One; apply ms_ifz. apply machsem_val_ret; apply val_z. apply One; apply ms_ifzz. apply (TheMachSemClos (cxtApp E (ifz (s v) e1 ve2)) (cxtApp E (subst ((fst ve2, v) :: nil) (snd ve2))) E (ifz (s v) e1 ve2) (subst ((fst ve2, v) :: nil) (snd ve2)) (exprDecomp E (ifz (s v) e1 ve2)) (exprDecomp E (subst ((fst ve2, v) :: nil) (snd ve2)))). intro k; apply (transclos_trans (b := ret_pair (f_ifz e1 ve2 :: k) (s v))). apply (transclos_trans (b := eval_pair (f_ifz e1 ve2 :: k) (s v))). apply One; apply ms_ifz. apply machsem_val_ret; apply val_s; trivial. apply One; apply ms_ifzs. apply (TheMachSemClos (cxtApp E (ap (lam ve) e'0)) (cxtApp E (subst ((fst ve, e'0) :: nil) (snd ve))) E (ap (lam ve) e'0) (subst ((fst ve, e'0) :: nil) (snd ve)) (exprDecomp E (ap (lam ve) e'0)) (exprDecomp E (subst ((fst ve, e'0) :: nil) (snd ve)))). intro k; apply (transclos_trans (b := ret_pair (f_ap e'0 :: k) (lam ve))). apply (transclos_trans (b := eval_pair (f_ap e'0 :: k) (lam ve))). apply One; apply ms_ap. apply machsem_val_ret; apply val_lam. apply One; apply ms_ap_ret. apply (TheMachSemClos (cxtApp E (Fix ve)) (cxtApp E (subst ((fst ve, Fix ve) :: nil) (snd ve))) E (Fix ve) (subst ((fst ve, Fix ve) :: nil) (snd ve)) (exprDecomp E (Fix ve)) (exprDecomp E (subst ((fst ve, Fix ve) :: nil) (snd ve)))). intro k; apply One; apply ms_fix. Qed. Lemma gen_completeness (e e' : Expr) : CxtSemClos e e' -> isVal e' -> forall E : Cxt, forall a : Expr, ExprDecomp e E a -> forall k : Stack, MachSemClos (eval_pair (Cxt2Stack E ++ k) a) (ret_pair k e'). (* induction step needs onestep_completeness, but not so easy *) Admitted. (* lemmas for soundness *) Lemma subst_soundness (e e' : Expr) : CxtSem e e' -> forall k : Stack, CxtSem (stackApp k e) (stackApp k e'). Admitted. Definition machStateApp pr := match pr with | eval_pair k e => stackApp k e | ret_pair k e => stackApp k e end. Lemma onestep_soundness pr pr' : MachSem pr pr' -> CxtSemClos (machStateApp pr) (machStateApp pr'). (* 1 step for for ms_ifzz, ms_ifzs, ms_ap_ret, and ms_fix; 0 step for the rest *) Admitted. Lemma gen_soundness pr pr' : MachSemClos pr pr' -> CxtSemClos (machStateApp pr) (machStateApp pr'). Admitted. (* Completeness and soundness *) Theorem completeness (e e' : Expr) : CxtSemClos e e' -> isVal e' -> MachSemClos (eval_pair nil e) (ret_pair nil e'). intros cxt val. apply (gen_completeness e e' cxt val c_here e (d_here e) nil). Qed. Theorem soundness (e e' : Expr) : MachSemClos (eval_pair nil e) (ret_pair nil e') -> CxtSemClos e e' * isVal e'. intros mach. split. apply (gen_soundness _ _ mach). (* isVal part can be proved with machsem_ret_val and machsem_val_ret on the last eval_pair in mach *) Admitted. End Problem4.