Set Implicit Arguments. Require Import Omega. Fixpoint plus (n : nat) (m : nat) : nat := match n with | O => m | S n' => S (plus n' m) end. Fixpoint mult (n m : nat) : nat := match n with | O => O | S n' => plus m (mult n' m) end. Lemma mult_S x y : mult x (S y) = plus (mult x y) x. Proof. Admitted. Lemma mult_com (x y : nat) : mult x y = mult y x. Proof. Admitted. Lemma mult_dist (x y z: nat) : mult (plus x y) z = plus (mult x z) (mult y z). Proof. Admitted. (* For this part of the homework, we will consider how we might reason about a * a simple language of arithmetic expressions. *) Inductive arith : Set := | Const (n : nat) | Plus (e1 e2 : arith) | Times (e1 e2 : arith). (* Here are a few examples of specific expressions. *) Example ex1 := Const 42. Example ex2 := Plus (Const 1) (Times (Const 2) (Const 3)). (* Write a definition that computes the size of an arithmetic expression * This should be equivalent to the size of the expression's abstract syntax tree *) Fixpoint size (e : arith) : nat. Admitted. (* What's the longest path from the root of a syntax tree to a leaf? *) Fixpoint depth (e : arith) : nat. Admitted. Theorem depth_le_size : forall e, depth e <= size e. Proof. (* you will need to use the omega tactic in this proof. *) (* SearchAbout is also your friend! *) Admitted. Fixpoint commuter (e : arith) : arith := match e with | Const _ => e | Plus e1 e2 => Plus (commuter e2) (commuter e1) | Times e1 e2 => Times (commuter e2) (commuter e1) end. Theorem size_commuter : forall e, size (commuter e) = size e. Proof. Admitted. Theorem commuter_inverse : forall e, commuter (commuter e) = e. Proof. Admitted.