proposition: Theorem updateCorrect : forall c d : rZ, eqStateRz (addEq (rZPlus a, samePol pol b) S) c d <-> evalZ (updateArray a b pol La Lb Ar) c = evalZ (updateArray a b pol La Lb Ar) d.
proof: Proof. intros c d; split. cut (exists S' : _, S' = addEq (rZPlus a, samePol pol b) S). intros H'; Elimc H'; intros S' E; rewrite <- E. intros H'; generalize E; elim H'; auto with stalmarck. intros a0 b0 S0 H'0 H'1; rewrite H'1 in H'0. simpl in H'0; case H'0. intros H'2; inversion H'2. rewrite updateEvalZab. case pol; auto with stalmarck. intros H'2; apply updateEvalZ2. case (SisAr a0 b0); auto with stalmarck. intros a0 b0 S0 H'0 H'1 H'2; repeat rewrite evalZComp; apply EqrZComp; auto with stalmarck. intros a0 b0 S0 H'0 H'1 H'2; apply sym_equal; auto with stalmarck. intros a0 b0 c0 S0 H'0 H'1 H'2 H'3 H'4; rewrite H'1; auto with stalmarck. intros a0 b0 c0 S0 H'0 H'1 H'2; absurd (evalZ (updateArray a b pol La Lb Ar) a0 = evalZ (updateArray a b pol La Lb Ar) (rZComp a0)); auto with stalmarck. rewrite evalZComp; auto with stalmarck. exists (addEq (rZPlus a, samePol pol b) S); auto with stalmarck. case (rNatDec (valRz (evalZ Ar c)) b); intros Eqt. rewrite updateEvalZb; auto with stalmarck. case (rNatDec (valRz (evalZ Ar d)) b); intros Eqt'. rewrite updateEvalZb; auto with stalmarck. intros tmp; apply eqStateaddEq2. case (SisAr c d); intros H' H'0; apply H'0; auto with stalmarck. generalize Eqt; rewrite <- Eqt'; generalize tmp; case (evalZ Ar c); case (evalZ Ar d); case pol; simpl in |- *; auto with stalmarck; intros r0 r1 r2 H0 H1; rewrite H1; try discriminate; auto with stalmarck. rewrite updateEvalZO; auto with stalmarck. intros H0; apply eqStateRzTrans with (b := samePolRz (evalZ Ar c) (rZPlus b)). apply eqStateaddEq2. case (SisAr c (samePolRz (evalZ Ar c) (rZPlus b))); intros H' H'0; apply H'0; auto with stalmarck. rewrite <- Eqt; generalize (evalZInv Ar War c); case (evalZ Ar c); simpl in |- *; auto with stalmarck. apply eqStateRzTrans with (b := samePolRz (evalZ Ar c) (samePolRz pol (rZPlus a))). case (evalZ Ar c); case pol; simpl in |- *; auto with stalmarck; intros r1 r2; apply eqStateInvInv; simpl in |- *; auto with stalmarck. apply eqStateaddEq2. case (SisAr (samePolRz (evalZ Ar c) (samePolRz pol (rZPlus a))) d); intros H' H'0; apply H'0; auto with stalmarck. rewrite <- H0; case pol; case (evalZ Ar c); simpl in |- *; intros r1 r2; unfold evalN in |- *; rewrite geta; auto with stalmarck. rewrite updateEvalZO; auto with stalmarck. case (rNatDec (valRz (evalZ Ar d)) b); intros Eqt'. rewrite updateEvalZb; auto with stalmarck. intros H0; apply eqStateRzTrans with (b := samePolRz (evalZ Ar d) (samePolRz pol (rZPlus a))). apply eqStateaddEq2. case (SisAr c (samePolRz (evalZ Ar d) (samePolRz pol (rZPlus a)))); intros H' H'0; apply H'0; auto with stalmarck. rewrite H0; case pol; case (evalZ Ar d); simpl in |- *; intros r1 r2; unfold evalN in |- *; rewrite geta; auto with stalmarck. apply eqStateRzTrans with (b := samePolRz (evalZ Ar d) (rZPlus b)). case (evalZ Ar d); case pol; simpl in |- *; auto with stalmarck. apply eqStateaddEq2. case (SisAr (samePolRz (evalZ Ar d) (rZPlus b)) d); intros H' H'0; apply H'0; auto with stalmarck. rewrite <- Eqt'; generalize (evalZInv Ar War d); case (evalZ Ar d); simpl in |- *; auto with stalmarck. rewrite updateEvalZO; auto with stalmarck. intros H'; apply eqStateaddEq2. case (SisAr c d); auto with stalmarck. Qed.