(** * Lecture 07 *) Require Import Bool. Require Import ZArith. Require Import IMPSyntax. Require Import IMPSemantics. (** ** Pseudo Denotational Semantics *) (** Here we're going to explore what's called "denoting" *) (** When we take a program and denote it, we simply give the meaning of the program *) (** in terms of something else *) (** Here, we'll use the existing meaning of Coq to denote our programs *) (** If we have a binary operation, the meaning of that binary operation is a *) (** coq function of type Z -> Z -> Z *) Definition denote_binop (op: binop) : Z -> Z -> Z := exec_op op. (** When we denote an expression, the meaning of it depends on the current heap *) (** Thus, the coq type of a denoted expresssion is heap -> Z *) Fixpoint denote_expr (e: expr) : heap -> Z := match e with | Int i => fun _ => i | Var v => fun h => h v | BinOp op e1 e2 => let f := denote_binop op in let x := denote_expr e1 in let y := denote_expr e2 in fun h => f (x h) (y h) end. (** Let's play with denoting a few toy examples *) Eval cbv in (denote_expr ("x" [+] "y")). Eval cbv in ((denote_expr ("x" [+] "y")) empty). Eval cbv in (denote_expr ("x" [+] 1)). Eval cbv in ((denote_expr ("x" [+] 1)) empty). (** Note that for expressions, essentially the only difference between denoting and interpreting is *) (** the stage at which the heap matters. When interpreting a program, we start with a *) (** heap and expression, and crawl over the expression tree with both. *) (** When denoting an expression, we crawl over the entire expression _without_ the heap, giving meaning to the expression for all heaps *) (** Only afterwards do we derive meaning by providing a particular heap *) (** Here we can prove that we denoted expressions correctly. *) (** We want the meaning to match up in all cases *) Lemma denote_expr_interp_expr: forall e h, (denote_expr e) h = interp_expr h e. Proof. induction e; simpl; intros; auto. unfold denote_binop. congruence. Qed. (** already connected interp_expr to eval, so now get denote connections "for free" *) (** Here we can show that our denotation function matches our evaluation relation *) Lemma denote_expr_eval: forall e h i, (denote_expr e) h = i <-> eval h e i. Proof. intros. rewrite denote_expr_interp_expr. split. - apply interp_expr_eval. - apply eval_interp_expr. Qed. (** Helpful little function *) (** Stands for "option bind" *) (** For more info as for why it's named that, see documentation about monads *) Definition obind {A B: Type} (oa: option A) (f: A -> option B) : option B := match oa with | None => None | Some a => f a end. (** Here we give meaning to statements *) (** Note that this has type nat -> heap -> option heap *) (** instead of simply heap -> heap *) (** the nat will encode the amount of fuel we give to the program *) (** as the program could diverge *) (** the option encodes the fact that evaluation could fail *) (** though the only way to fail is running out of fuel *) (** careful to detect timeout (running out of fuel)! *) Fixpoint denote_stmt (s: stmt) : nat -> heap -> option heap := match s with | Nop => fun _ h => Some h | Assign v e => let de := denote_expr e in fun _ h => Some (update h v (de h)) | Seq e1 e2 => let d1 := denote_stmt e1 in let d2 := denote_stmt e2 in fun n h => obind (d1 n h) (d2 n) | Cond e s => let de := denote_expr e in let ds := denote_stmt s in fun n h => if Z_eq_dec 0 (de h) then Some h else ds n h | While e s => let de := denote_expr e in let ds := denote_stmt s in fix loop n h := match n with | O => None | S m => if Z_eq_dec 0 (de h) then Some h else obind (ds n h) (loop m) end end. Theorem nat_strong_ind' : forall P : nat -> Prop, P 0%nat -> (forall n, (forall m, (m <= n)%nat -> P m) -> P (S n)) -> forall n, (forall m, (m <= n)%nat -> P m). Proof. induction n; intros. - assert (m = 0%nat) by omega. subst. auto. - assert ((m <= n)%nat \/ m = S n) by omega. intuition. subst. auto. Qed. Lemma nat_strong_ind : forall (P : nat -> Prop), P 0%nat -> (forall n, (forall m, (m <= n)%nat -> P m) -> P (S n)) -> forall n, P n. Proof. intros. eapply nat_strong_ind'; eauto. Qed. (** Here's what we might use for a different kind of induction on nats *) (** If we wanted to do different induction like we talked about in class *) (** This is what we might do *) Lemma nat_parity_ind : forall (P : nat -> Prop), P 0%nat -> P 1%nat -> (forall n, P n -> P (S (S n))) -> forall n, P n. Proof. induction n using nat_strong_ind; intros. eauto. destruct n. eauto. eapply H1. eapply H2. omega. Qed.