proposition: Lemma ZM_correct (vm : list G) (e1 e2 : AGExpr) : let isZero (n : Z) := match n with Z0 => true | _ => false end in all isZero (ZMnorm (AGAdd e1 (AGOpp e2))) = true -> AGeval vm e1 = AGeval vm e2.
proof: Proof. set (e := AGAdd e1 (AGOpp e2)); intros isZero Hzeros. rewrite <- (addx0 (AGeval vm e1)), <- (add0x (AGeval vm e2)). rewrite <- (addNx (AGeval vm e2)), addA at 1; f_equal. change (addG (AGeval vm e1) (oppG (AGeval vm e2))) with (AGeval vm e). rewrite <- !ZM_norm_subst; revert vm Hzeros. induction (ZMnorm e) as [|x xs IHxs]; destruct vm as [|v vm]; simpl; trivial. now destruct x; try discriminate; rewrite add0x; apply IHxs. Qed.
imports: Coq(ZArith)