(* ********************************************** *) (* Types and Semantics for Programming Languages *) (* ********************************************** *) (* Place an X in front of the appropriate statement *) (* [ ] I have done Problems 1 and 2 *) (* [ ] I have done Problems 1 and 3 *) Require Import Coq.Bool.Bool. Require Import Coq.Arith.Arith. Require Import Coq.Arith.EqNat. Require Import Coq.Lists.List. Import ListNotations. Require Export Maps. (* ********************************************** *) (* Problem 1 *) (* ********************************************** *) Inductive member {X:Type} : X -> list X -> Prop := | member_here : forall (x:X) (xs:list X), member x (x :: xs) | member_later : forall (x:X) (y:X) (xs:list X), member x xs -> member x (y::xs). Theorem app_member_left : forall (X:Type) (x:X) (xs ys : list X), member x xs -> member x (xs ++ ys). Proof. intros X x xs ys H. induction H. * simpl. apply member_here. * simpl. apply member_later. apply IHmember. Qed. Theorem app_member_right : forall (X:Type) (x:X) (xs ys : list X), member x ys -> member x (xs ++ ys). Proof. intros X x xs ys H. induction xs as [| y xs]. * simpl. apply H. * simpl. apply member_later. apply IHxs. Qed. Theorem app_member_1 : forall (X:Type) (x:X) (xs ys:list X), member x xs \/ member x ys -> member x (xs ++ ys). Proof. intros X x xs ys H. inversion H as [LH|RH]. * apply app_member_left. apply LH. * apply app_member_right. apply RH. Qed. Theorem app_member_2 : forall (X:Type) (x:X) (xs ys:list X), member x (xs ++ ys) -> member x xs \/ member x ys. Proof. intros X x xs ys H. induction xs as [| y xs]. * right. simpl in H. apply H. * simpl in H. inversion H. + subst. left. apply member_here. + subst. apply IHxs in H2. inversion H2. - left. apply member_later. apply H0. - right. apply H0. Qed. (* ********************************************** *) (* Problem 2 *) (* ********************************************** *) (* States *) Definition state := total_map nat. Definition empty_state : state := t_empty 0. Definition X : id := Id 0. Definition Y : id := Id 1. Definition Z : id := Id 2. (* Arithmetic and boolean expressions *) Inductive aexp : Type := | ANum : nat -> aexp | AId : id -> aexp | APlus : aexp -> aexp -> aexp | AMinus : aexp -> aexp -> aexp | AMult : aexp -> aexp -> aexp. Inductive bexp : Type := | BTrue : bexp | BFalse : bexp | BEq : aexp -> aexp -> bexp | BLe : aexp -> aexp -> bexp | BNot : bexp -> bexp | BAnd : bexp -> bexp -> bexp. Fixpoint aeval (st : state) (a : aexp) : nat := match a with | ANum n => n | AId x => st x | APlus a1 a2 => (aeval st a1) + (aeval st a2) | AMinus a1 a2 => (aeval st a1) - (aeval st a2) | AMult a1 a2 => (aeval st a1) * (aeval st a2) end. Fixpoint beval (st : state) (b : bexp) : bool := match b with | BTrue => true | BFalse => false | BEq a1 a2 => beq_nat (aeval st a1) (aeval st a2) | BLe a1 a2 => leb (aeval st a1) (aeval st a2) | BNot b1 => negb (beval st b1) | BAnd b1 b2 => andb (beval st b1) (beval st b2) end. (* Commands *) Inductive com : Type := | CSkip : com | CAss : id -> aexp -> com | CSeq : com -> com -> com | CIf : bexp -> com -> com -> com | CWhile : bexp -> com -> com | CCountdown : id -> com -> com. (* !!! *) Notation "'SKIP'" := CSkip. Notation "x '::=' a" := (CAss x a) (at level 60). Notation "c1 ;; c2" := (CSeq c1 c2) (at level 80, right associativity). Notation "'IFB' b 'THEN' c1 'ELSE' c2 'FI'" := (CIf b c1 c2) (at level 80, right associativity). Notation "'WHILE' b 'DO' c 'END'" := (CWhile b c) (at level 80, right associativity). Notation "'COUNTDOWN' x 'DO' c 'END'" := (* !!! *) (CCountdown x c) (at level 80, right associativity). (* !!! *) (* Evaluation relation *) Reserved Notation "c1 '/' st '\\' st'" (at level 40, st at level 39). Inductive ceval : com -> state -> state -> Prop := | E_Skip : forall st, SKIP / st \\ st | E_Ass : forall st a1 n x, aeval st a1 = n -> (x ::= a1) / st \\ (t_update st x n) | E_Seq : forall c1 c2 st st' st'', c1 / st \\ st' -> c2 / st' \\ st'' -> (c1 ;; c2) / st \\ st'' | E_IfTrue : forall st st' b c1 c2, beval st b = true -> c1 / st \\ st' -> (IFB b THEN c1 ELSE c2 FI) / st \\ st' | E_IfFalse : forall st st' b c1 c2, beval st b = false -> c2 / st \\ st' -> (IFB b THEN c1 ELSE c2 FI) / st \\ st' | E_WhileEnd : forall b st c, beval st b = false -> (WHILE b DO c END) / st \\ st | E_WhileLoop : forall st st' st'' b c, beval st b = true -> c / st \\ st' -> (WHILE b DO c END) / st' \\ st'' -> (WHILE b DO c END) / st \\ st'' | E_CountdownEnd : forall st x c, st x = 0 -> (COUNTDOWN x DO c END) / st \\ st | E_CountdownLoop : forall st st' st'' st''' x c, st x > 0 -> c / st \\ st' -> st'' = t_update st' x (st' x - 1) -> (COUNTDOWN x DO c END) / st'' \\ st''' -> (COUNTDOWN x DO c END) / st \\ st''' where "c1 '/' st '\\' st'" := (ceval c1 st st'). (* Assertions *) Definition Assertion := state -> Prop. Definition assert_implies (P Q : Assertion) : Prop := forall st, P st -> Q st. Notation "P ->> Q" := (assert_implies P Q) (at level 80) : hoare_spec_scope. Open Scope hoare_spec_scope. Notation "P <<->> Q" := (P ->> Q /\ Q ->> P) (at level 80) : hoare_spec_scope. (* Hoare triples *) Definition hoare_triple (P:Assertion) (c:com) (Q:Assertion) : Prop := forall st st', c / st \\ st' -> P st -> Q st'. Notation "{{ P }} c {{ Q }}" := (hoare_triple P c Q) (at level 90, c at next level) : hoare_spec_scope. (* Assertions *) Definition bassn b : Assertion := fun st => (beval st b = true). Lemma bexp_eval_true : forall b st, beval st b = true -> (bassn b) st. Proof. intros b st Hbe. unfold bassn. assumption. Qed. Lemma bexp_eval_false : forall b st, beval st b = false -> ~ ((bassn b) st). Proof. intros b st Hbe contra. unfold bassn in contra. rewrite -> contra in Hbe. inversion Hbe. Qed. (* Assignment *) (* ------------------------------ (hoare_asgn) {{Q [X |-> a]}} X::=a {{Q}} *) Definition assn_sub X a P : Assertion := fun (st : state) => P (t_update st X (aeval st a)). Notation "P [ X |-> a ]" := (assn_sub X a P) (at level 10). Theorem hoare_asgn : forall Q X a, {{Q [X |-> a]}} (X ::= a) {{Q}}. Proof. unfold hoare_triple. intros Q X a st st' HE HQ. inversion HE. subst. unfold assn_sub in HQ. assumption. Qed. (* Consequence *) (* {{P'}} c {{Q'}} P ->> P' Q' ->> Q ----------------------------- (hoare_consequence) {{P}} c {{Q}} *) Theorem hoare_consequence_pre : forall (P P' Q : Assertion) c, {{P'}} c {{Q}} -> P ->> P' -> {{P}} c {{Q}}. Proof. intros P P' Q c Hhoare Himp. intros st st' Hc HP. apply (Hhoare st st'). assumption. apply Himp. assumption. Qed. Theorem hoare_consequence_post : forall (P Q Q' : Assertion) c, {{P}} c {{Q'}} -> Q' ->> Q -> {{P}} c {{Q}}. Proof. intros P Q Q' c Hhoare Himp. intros st st' Hc HP. apply Himp. apply (Hhoare st st'). assumption. assumption. Qed. Theorem hoare_consequence : forall (P P' Q Q' : Assertion) c, {{P'}} c {{Q'}} -> P ->> P' -> Q' ->> Q -> {{P}} c {{Q}}. Proof. intros P P' Q Q' c Hht HPP' HQ'Q. apply hoare_consequence_pre with (P' := P'). apply hoare_consequence_post with (Q' := Q'). assumption. assumption. assumption. Qed. (* Skip *) (* -------------------- (hoare_skip) {{ P }} SKIP {{ P }} *) Theorem hoare_skip : forall P, {{P}} SKIP {{P}}. Proof. intros P st st' H HP. inversion H. subst. assumption. Qed. (* Sequencing *) (* {{ P }} c1 {{ Q }} {{ Q }} c2 {{ R }} --------------------- (hoare_seq) {{ P }} c1;;c2 {{ R }} *) Theorem hoare_seq : forall P Q R c1 c2, {{Q}} c2 {{R}} -> {{P}} c1 {{Q}} -> {{P}} c1;;c2 {{R}}. Proof. intros P Q R c1 c2 H1 H2 st st' H12 Pre. inversion H12; subst. apply (H1 st'0 st'); try assumption. apply (H2 st st'0); assumption. Qed. (* Conditional *) (* {{P /\ b}} c1 {{Q}} {{P /\ ~b}} c2 {{Q}} ------------------------------------ (hoare_if) {{P}} IFB b THEN c1 ELSE c2 FI {{Q}} *) Theorem hoare_if : forall P Q b c1 c2, {{fun st => P st /\ bassn b st}} c1 {{Q}} -> {{fun st => P st /\ ~(bassn b st)}} c2 {{Q}} -> {{P}} (IFB b THEN c1 ELSE c2 FI) {{Q}}. Proof. intros P Q b c1 c2 HTrue HFalse st st' HE HP. inversion HE; subst. - (* b is true *) apply (HTrue st st'). assumption. split. assumption. apply bexp_eval_true. assumption. - (* b is false *) apply (HFalse st st'). assumption. split. assumption. apply bexp_eval_false. assumption. Qed. (* While *) (* {{P /\ b}} c {{P}} ----------------------------------- (hoare_while) {{P}} WHILE b DO c END {{P /\ ~b}} The proposition [P] is called an _invariant_ of the loop. *) Lemma hoare_while : forall P b c, {{fun st => P st /\ bassn b st}} c {{P}} -> {{P}} WHILE b DO c END {{fun st => P st /\ ~ (bassn b st)}}. Proof. intros P b c Hhoare st st' He HP. remember (WHILE b DO c END) as wcom eqn:Heqwcom. induction He; try (inversion Heqwcom); subst; clear Heqwcom. - (* E_WhileEnd *) split. assumption. apply bexp_eval_false. assumption. - (* E_WhileLoop *) apply IHHe2. reflexivity. apply (Hhoare st st'). assumption. split. assumption. apply bexp_eval_true. assumption. Qed. (* {{P /\ x > 0}} c {{P[x |-> x-1]}} --------------------------------------- (hoare_countdown) {{P}} COUNTDOWN x DO c END {{P /\ x=0}} *) Lemma hoare_countdown : forall P x c, (* !!! *) {{fun st => P st /\ st x > 0}} c (* !!! *) {{fun st' => P (t_update st' x (st' x - 1))}} -> (* !!! *) {{P}} COUNTDOWN x DO c END {{fun st => P st /\ st x = 0}}. (* !!! *) Proof. (* !!! *) intros P x c Hhoare st st' He HP. (* !!! *) remember (COUNTDOWN x DO c END) as ccom eqn:Heqccom. (* !!! *) induction He; try (inversion Heqccom); subst; clear Heqccom. (* !!! *) - (* E_CountdownEnd *) (* !!! *) split. assumption. assumption. (* !!! *) - (* E_CountdownLoop *) (* !!! *) apply IHHe2. reflexivity. (* !!! *) apply (Hhoare st st'). assumption. split. assumption. assumption. (* !!! *) Qed. (* !!! *) (* ********************************************** *) (* Problem 3 *) (* ********************************************** *) (* Types *) Inductive ty : Type := | TBool : ty | TArrow : ty -> ty -> ty | TTree : ty -> ty. (* !!! *) (* Terms *) Inductive tm : Type := | tvar : id -> tm | tapp : tm -> tm -> tm | tabs : id -> ty -> tm -> tm | ttrue : tm | tfalse : tm | tif : tm -> tm -> tm -> tm | tleaf : tm (* !!! *) | tbranch : tm -> tm -> tm -> tm (* !!! *) | ttcase : tm -> tm -> id -> id -> id -> tm -> tm. (* !!! *) (* Values *) Inductive value : tm -> Prop := | v_abs : forall x T t, value (tabs x T t) | v_true : value ttrue | v_false : value tfalse | v_leaf : (* !!! *) value tleaf (* !!! *) | v_branch : forall v1 v2 v3, (* !!! *) value v1 -> (* !!! *) value v2 -> (* !!! *) value v3 -> (* !!! *) value (tbranch v1 v2 v3). (* !!! *) Hint Constructors value. (* Substitution *) Reserved Notation "'[' x ':=' s ']' t" (at level 20). Fixpoint subst (x:id) (s:tm) (t:tm) : tm := match t with | tvar x' => if beq_id x x' then s else t | tabs x' T t1 => tabs x' T (if beq_id x x' then t1 else ([x:=s] t1)) | tapp t1 t2 => tapp ([x:=s] t1) ([x:=s] t2) | ttrue => ttrue | tfalse => tfalse | tif t1 t2 t3 => tif ([x:=s] t1) ([x:=s] t2) ([x:=s] t3) | tleaf => (* !!! *) tleaf (* !!! *) | tbranch t1 t2 t3 => (* !!! *) tbranch ([x:=s] t1) ([x:=s] t2) ([x:=s] t3) (* !!! *) | ttcase t1 t2 xt y zt t3 => (* !!! *) ttcase ([x := s] t1) ([x := s] t2) xt y zt (* !!! *) (if beq_id x xt || beq_id x y || beq_id x zt (* !!! *) then t3 (* !!! *) else ([x:=s] t3)) (* !!! *) end where "'[' x ':=' s ']' t" := (subst x s t). (* Evaluation relation *) Reserved Notation "t1 '==>' t2" (at level 40). Inductive step : tm -> tm -> Prop := | ST_AppAbs : forall x T t12 v2, value v2 -> (tapp (tabs x T t12) v2) ==> [x:=v2]t12 | ST_App1 : forall t1 t1' t2, t1 ==> t1' -> tapp t1 t2 ==> tapp t1' t2 | ST_App2 : forall v1 t2 t2', value v1 -> t2 ==> t2' -> tapp v1 t2 ==> tapp v1 t2' | ST_IfTrue : forall t1 t2, (tif ttrue t1 t2) ==> t1 | ST_IfFalse : forall t1 t2, (tif tfalse t1 t2) ==> t2 | ST_If : forall t1 t1' t2 t3, t1 ==> t1' -> (tif t1 t2 t3) ==> (tif t1' t2 t3) | ST_BranchLeft : forall t1 t2 t3 t1', (* !!! *) t1 ==> t1' -> (* !!! *) tbranch t1 t2 t3 ==> tbranch t1' t2 t3 (* !!! *) | ST_BranchMiddle : forall v1 t2 t3 t2', (* !!! *) value v1 -> (* !!! *) t2 ==> t2' -> (* !!! *) tbranch v1 t2 t3 ==> tbranch v1 t2' t3 (* !!! *) | ST_BranchRight : forall v1 v2 t3 t3', (* !!! *) value v1 -> (* !!! *) value v2 -> (* !!! *) t3 ==> t3' -> (* !!! *) tbranch v1 v2 t3 ==> tbranch v1 v2 t3' (* !!! *) | ST_TCase : forall t1 t2 xt y zt t3 t1', (* !!! *) t1 ==> t1' -> (* !!! *) (ttcase t1 t2 xt y zt t3) ==> (ttcase t1' t2 xt y zt t3) (* !!! *) | ST_TCaseLeaf : forall t2 xt y zt t3, (* !!! *) (ttcase tleaf t2 xt y zt t3) ==> t2 (* !!! *) | ST_TCaseBranch : forall v11 v12 v13 t2 xt y zt t3, (* !!! *) value v11 -> (* !!! *) value v12 -> (* !!! *) value v13 -> (* !!! *) ttcase (tbranch v11 v12 v13) t2 xt y zt t3 ==> (* !!! *) [xt:=v11]([y:=v12]([zt:=v13]t3)) (* !!! *) where "t1 '==>' t2" := (step t1 t2). Hint Constructors step. (* Contexts *) Definition context := partial_map ty. (* Typing relation *) Reserved Notation "Gamma '|-' t '\in' T" (at level 40). Inductive has_type : context -> tm -> ty -> Prop := | T_Var : forall Gamma x T, Gamma x = Some T -> Gamma |- tvar x \in T | T_Abs : forall Gamma x T11 T12 t12, update Gamma x T11 |- t12 \in T12 -> Gamma |- tabs x T11 t12 \in TArrow T11 T12 | T_App : forall T11 T12 Gamma t1 t2, Gamma |- t1 \in TArrow T11 T12 -> Gamma |- t2 \in T11 -> Gamma |- tapp t1 t2 \in T12 | T_True : forall Gamma, Gamma |- ttrue \in TBool | T_False : forall Gamma, Gamma |- tfalse \in TBool | T_If : forall t1 t2 t3 T Gamma, Gamma |- t1 \in TBool -> Gamma |- t2 \in T -> Gamma |- t3 \in T -> Gamma |- tif t1 t2 t3 \in T | T_Leaf : forall Gamma T, (* !!! *) Gamma |- tleaf \in TTree T (* !!! *) | T_Branch : forall Gamma t1 t2 t3 T, (* !!! *) Gamma |- t1 \in TTree T -> (* !!! *) Gamma |- t2 \in T -> (* !!! *) Gamma |- t3 \in TTree T -> (* !!! *) Gamma |- tbranch t1 t2 t3 \in TTree T (* !!! *) | T_TCase : forall Gamma T T' t1 t2 xt y zt t3, (* !!! *) Gamma |- t1 \in TTree T -> (* !!! *) Gamma |- t2 \in T' -> (* !!! *) update (update (update Gamma xt (TTree T)) y T) zt (TTree T) (* !!! *) |- t3 \in T' -> (* !!! *) Gamma |- ttcase t1 t2 xt y zt t3 \in T' (* !!! *) where "Gamma '|-' t '\in' T" := (has_type Gamma t T). Hint Constructors has_type. (* Canonical Forms *) Lemma canonical_forms_bool : forall t, empty |- t \in TBool -> value t -> (t = ttrue) \/ (t = tfalse). Proof. intros t HT HVal. inversion HVal; intros; subst; try inversion HT; auto. Qed. Lemma canonical_forms_fun : forall t T1 T2, empty |- t \in (TArrow T1 T2) -> value t -> exists x u, t = tabs x T1 u. Proof. intros t T1 T2 HT HVal. inversion HVal; intros; subst; try inversion HT; subst; auto. exists x. exists t0. auto. Qed. Lemma canonical_forms_tree : forall t T, (* !!! *) empty |- t \in (TTree T) -> (* !!! *) value t -> (* !!! *) (t = tleaf \/ (* !!! *) exists v1 v2 v3, (* !!! *) value v1 /\ value v2 /\ value v3 /\ t = tbranch v1 v2 v3). (* !!! *) Proof. (* !!! *) intros t T HT HVal. (* !!! *) inversion HVal; intros; subst; try inversion HT. (* !!! *) * (* tleaf *) (* !!! *) left. auto. (* !!! *) * (* tbranch *) (* !!! *) subst. right. exists v1. exists v2. exists v3. auto. (* !!! *) Qed. (* !!! *) (* Progress, by induction on type derivation *) Theorem progress : forall t T, empty |- t \in T -> value t \/ exists t', t ==> t'. Proof with eauto. intros t T Ht. remember (@empty ty) as Gamma. induction Ht; subst Gamma... - (* T_Var *) (* contradictory: variables cannot be typed in an empty context *) inversion H. - (* T_App *) (* [t] = [t1 t2]. Proceed by cases on whether [t1] is a value or steps... *) right. destruct IHHt1... + (* t1 is a value *) destruct IHHt2... * (* t2 is also a value *) assert (exists x0 t0, t1 = tabs x0 T11 t0). eapply canonical_forms_fun; eauto. destruct H1 as [x0 [t0 Heq]]. subst. exists ([x0:=t2]t0)... * (* t2 steps *) inversion H0 as [t2' Hstp]. exists (tapp t1 t2')... + (* t1 steps *) inversion H as [t1' Hstp]. exists (tapp t1' t2)... - (* T_If *) right. destruct IHHt1... + (* t1 is a value *) destruct (canonical_forms_bool t1); subst; eauto. + (* t1 also steps *) inversion H as [t1' Hstp]. exists (tif t1' t2 t3)... - (* T_Branch *) (* !!! *) destruct IHHt1. reflexivity. (* !!! *) (* t1 is a value *) (* !!! *) destruct IHHt2. reflexivity. (* !!! *) (* t2 is a value *) (* !!! *) destruct IHHt3. reflexivity. (* !!! *) (* t3 is a value *) (* !!! *) left... (* !!! *) (* t3 steps *) (* !!! *) inversion H1 as [t3' step3]. (* !!! *) right. exists (tbranch t1 t2 t3')... (* !!! *) (* t2 steps *) (* !!! *) inversion H0 as [t2' step2]. (* !!! *) right. exists (tbranch t1 t2' t3)... (* !!! *) (* t1 steps *) (* !!! *) inversion H as [t1' step1]. (* !!! *) right. exists (tbranch t1' t2 t3)... (* !!! *) - (* T_TCase *) (* !!! *) destruct IHHt1. reflexivity. (* !!! *) + (* t1 is a value *) (* !!! *) right. (* !!! *) destruct (canonical_forms_tree t1 T); subst; auto. (* !!! *) * (* t1 = tleaf *) (* !!! *) exists t2... (* !!! *) * (* t1 = tbranch v1 v2 v3 *) (* !!! *) inversion H0 as [v1 [v2 [v3 [Hval1 [Hval2 [Hval3 Heq]]]]]]. (* !!! *) subst. exists ([xt:=v1]([y:=v2]([zt:=v3]t3)))... (* !!! *) + (* t1 steps *) (* !!! *) inversion H as [t1' Hstep]. (* !!! *) right. exists (ttcase t1' t2 xt y zt t3)... (* !!! *) Qed.