(*** Semantics 2009/10 ***) (*** assignment 1 ***) Inductive bool : Type := true | false. Inductive nat : Type := O | S : nat->nat. Fixpoint plus x y := match x with O => y | S x' => S(plus x' y) end. Notation "x + y" := (plus x y) (at level 50, left associativity). (*** Exercise 1: commutativity of plus ***) (* fill in your statement and proof here *) (*** Exercise 2: leq ***) (** 2a: definition of leq **) Fixpoint leq x y := (* fill in your definition here *) Notation "x <= y" := (leq x y). (** 2b: reflexivity of leq **) (* fill in your statement and proof here *) (** 2c: translation invariance **) Proposition leq_l: forall x y z, (x <= y) = true -> (z+x <= z+y) = true. (* fill in your proof here *) Proposition leq_r: forall x y z, (x <= y) = true -> (x + z <= y + z) = true. (* fill in your proof here *) (** hint: rewriting with instantiations **) Proposition Demo: forall (f: nat->nat) x, (forall y, f y=y) -> (f x,f x)=(f x,f(f x)). Proof. intros. (* At this point we could use rewrite H. *) (* this rewrites all occurrences of f x by x *) (* and leads to the proof goal (x,x) = (x,f x). *) (* Another rewrite H will solve this goal. *) (* However, a more direct proof is to use a *) (* single rewrite of "f(f x)" to "f x" instead. *) (* We can tell Coq to instantiate the *) (* universally quantified "z" in "H" by "f x" to achieve this: *) rewrite H with (y:=f x). trivial. Qed. (*** Exercise 3: iter ***) (** 3a: definition of iter **) Fixpoint iter (f:nat->nat) n x := (* fill in your definition here *) (** 3b: commutation property of iter **) Proposition iter_comm: forall f n x, iter f n (f x) = f(iter f n x). (* fill in your proof here *) (** 3c: plus from iter **) Proposition iter_plus: forall n x, iter S n x = n+x. (* fill in your proof here *)