proposition: Theorem optimize_0plus_sound: forall a, aeval (optimize_0plus a) = aeval a.
proof: Proof. intros a. induction a. - reflexivity. - destruct a1 eqn:Ea1. + destruct n eqn:En. * 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(Init.Nat) Coq(Arith.Arith) Coq(Arith.EqNat) Coq(Lia) Coq(Lists.List) Coq(Strings.String) LF(Maps)