proposition: Theorem optimize_0plus_sound: forall a, aeval (optimize_0plus a) = aeval a.
proof: Proof. intros a. induction a. - reflexivity. - destruct a1. + destruct n. * simpl. apply IHa2. * simpl. rewrite IHa2. reflexivity. + simpl. simpl in IHa1. rewrite IHa1. rewrite IHa2. reflexivity. + simpl. simpl in IHa1. rewrite IHa1. rewrite IHa2. reflexivity. + simpl. simpl in IHa1. rewrite IHa1. rewrite IHa2. reflexivity. - simpl. rewrite IHa1. rewrite IHa2. reflexivity. - simpl. rewrite IHa1. rewrite IHa2. reflexivity. Qed.
imports: Coq.Bool.Bool Coq.Arith.Arith Coq.Arith.EqNat Coq.omega.Omega Coq.Lists.List Coq.omega.Omega Maps