proposition: Theorem addEqMemCorrect : forall (Ar : rArray vM) (a b : rZ) (S : State), wellFormedArray Ar -> rArrayState Ar S -> match addEqMem Ar a b with | triple Ar' false L => wellFormedArray Ar' /\ rArrayState Ar' (addEq (a, b) S) /\ OlistRz L /\ (forall c : rNat, ~ InRz (rZPlus c) L -> rArrayGet _ Ar' c = rArrayGet _ Ar c) | triple Ar' true L => contradictory (addEq (a, b) S) end.
proof: Proof. intros Ar a b S War H'; unfold addEqMem, letP in |- *. case (rZltEDec (evalZ Ar a) (evalZ Ar b)); simpl in |- *. intros s; case s; simpl in |- *. intros H'0; split. apply updateWellFormed; auto with stalmarck. apply GetClassNProp; auto with stalmarck. apply GetClassNProp; auto with stalmarck. split. red in |- *; intros c d; repeat split; intros H0. case (updateCorrect Ar War (valRz (evalZ Ar a)) (valRz (evalZ Ar b)) (samePolRz (evalZ Ar a) (evalZ Ar b)) (getClassN Ar (valRz (evalZ Ar a))) (getClassN Ar (valRz (evalZ Ar b)))) with (S := S) (c := c) (d := d); auto with stalmarck; auto with stalmarck. apply GetClassNProp; auto with stalmarck. apply GetClassNProp; auto with stalmarck. intros H'1 H'2; apply H'1; auto with stalmarck. apply eqStateIncl with (2 := H0); auto with stalmarck. apply inclStateIn; simpl in |- *; auto with stalmarck. intros a0 b0 H'3; Elimc H'3; intros H'3. inversion H'3; auto with stalmarck. apply eqStateRzTrans with (b := evalZ Ar a0). apply eqStateaddEq2. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZInv; auto with stalmarck. apply eqStateRzTrans with (b := evalZ Ar b0). case (evalZ Ar a0); case (evalZ Ar b0); simpl in |- *; auto with stalmarck. apply eqStateaddEq2. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZInv; auto with stalmarck. apply eqStateaddEq2; auto with stalmarck. apply eqStateIncl with (addEq (rZPlus (valRz (evalZ Ar a)), samePol (samePolRz (evalZ Ar a) (evalZ Ar b)) (valRz (evalZ Ar b))) S); auto with stalmarck. apply inclStateIn; simpl in |- *; auto with stalmarck. intros a0 b0 H'1; Elimc H'1; intros H'1; auto with stalmarck. inversion H'1; auto with stalmarck. apply eqStateRzTrans with (b := samePolRz (evalZ Ar a) a). apply eqStateaddEq2. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. generalize (evalZInv Ar War a); CaseEq (evalZ Ar a); simpl in |- *; auto with stalmarck. intros r H'2; rewrite H'2; auto with stalmarck. intros r H'2 H'3; rewrite evalZComp; rewrite H'2; rewrite <- H'3; case (evalN Ar r); auto with stalmarck. apply eqStateRzTrans with (b := samePolRz (evalZ Ar a) b); auto with stalmarck. case (evalZ Ar a); simpl in |- *; auto with stalmarck. apply eqStateaddEq2. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. case (evalZ Ar a); simpl in |- *; auto with stalmarck. generalize (evalZInv Ar War b); CaseEq (evalZ Ar b); simpl in |- *; auto with stalmarck. generalize (evalZInv Ar War b); CaseEq (evalZ Ar b); simpl in |- *; auto with stalmarck. intros r H'2 H'3; rewrite evalZComp; rewrite H'3; rewrite <- H'2; auto with stalmarck. intros r H'2 H'3; rewrite evalZComp; rewrite H'2; rewrite <- H'3; auto with stalmarck. case (updateCorrect Ar War (valRz (evalZ Ar a)) (valRz (evalZ Ar b)) (samePolRz (evalZ Ar a) (evalZ Ar b)) (getClassN Ar (valRz (evalZ Ar a))) (getClassN Ar (valRz (evalZ Ar b)))) with (S := S) (c := c) (d := d); auto with stalmarck; auto with stalmarck. apply GetClassNProp; auto with stalmarck. apply GetClassNProp; auto with stalmarck. split. red in |- *; apply OlistCons; auto with stalmarck. apply getClassOlist; auto with stalmarck. intros c H'1. apply updateArrayOtherwise; auto with stalmarck. Contradict H'1; simpl in |- *; auto with stalmarck. red in |- *; repeat apply InEqSkip; auto with stalmarck. Contradict H'1; rewrite H'1; simpl in |- *; auto with stalmarck. red in |- *; apply InEqHead; auto with stalmarck. Contradict H'1; rewrite H'1; auto with stalmarck. red in |- *; apply InEqSkip; apply InEqHead; auto with stalmarck. intros H'0; split. apply updateWellFormed; auto with stalmarck. apply GetClassNProp; auto with stalmarck. apply GetClassNProp; auto with stalmarck. split. red in |- *; intros c d; split; intros H0. case (updateCorrect Ar War (valRz (evalZ Ar b)) (valRz (evalZ Ar a)) (samePolRz (evalZ Ar b) (evalZ Ar a)) (getClassN Ar (valRz (evalZ Ar b))) (getClassN Ar (valRz (evalZ Ar a)))) with (S := S) (c := c) (d := d); auto with stalmarck. apply GetClassNProp; auto with stalmarck. apply GetClassNProp; auto with stalmarck. intros H'1 H'2; apply H'1; auto with stalmarck. apply eqStateIncl with (2 := H0); auto with stalmarck. apply inclStateIn; simpl in |- *; auto with stalmarck. intros a0 b0 H'3; Elimc H'3; intros H'3. inversion H'3; auto with stalmarck. apply eqStateRzTrans with (b := evalZ Ar a0). apply eqStateaddEq2. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZInv; auto with stalmarck. apply eqStateRzTrans with (b := evalZ Ar b0). case (evalZ Ar a0); case (evalZ Ar b0); simpl in |- *; auto with stalmarck; intros r1 r2; apply eqStateInvInv; auto with stalmarck. apply eqStateaddEq2. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZInv; auto with stalmarck. apply eqStateaddEq2; auto with stalmarck. apply eqStateIncl with (addEq (rZPlus (valRz (evalZ Ar a)), samePol (samePolRz (evalZ Ar a) (evalZ Ar b)) (valRz (evalZ Ar b))) S); auto with stalmarck. apply inclStateIn; simpl in |- *; auto with stalmarck. intros a0 b0 H'1; Elimc H'1; intros H'1. inversion H'1; auto with stalmarck. apply eqStateRzTrans with (b := samePolRz (evalZ Ar a) a). apply eqStateaddEq2. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. generalize (evalZInv Ar War a); CaseEq (evalZ Ar a); simpl in |- *; auto with stalmarck. intros r H'2; rewrite H'2; auto with stalmarck. intros r H'2 H'3; rewrite evalZComp; rewrite H'2; rewrite <- H'3; case (evalN Ar r); auto with stalmarck. apply eqStateRzTrans with (b := samePolRz (evalZ Ar a) b); auto with stalmarck. case (evalZ Ar a); simpl in |- *; auto with stalmarck. apply eqStateaddEq2. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. case (evalZ Ar a); simpl in |- *; auto with stalmarck. generalize (evalZInv Ar War b); CaseEq (evalZ Ar b); simpl in |- *; auto with stalmarck. generalize (evalZInv Ar War b); CaseEq (evalZ Ar b); simpl in |- *; auto with stalmarck. intros r H'2 H'3; rewrite evalZComp; rewrite H'3; rewrite <- H'2; auto with stalmarck. intros r H'2 H'3; rewrite evalZComp; rewrite H'2; rewrite <- H'3; auto with stalmarck. apply eqStateRzIn; unfold addEq in |- *; auto with datatypes stalmarck. apply eqStateIncl with (addEq (rZPlus (valRz (evalZ Ar b)), samePol (samePolRz (evalZ Ar b) (evalZ Ar a)) (valRz (evalZ Ar a))) S); auto with stalmarck. apply inclStateIn; simpl in |- *; auto with stalmarck. intros a0 b0 H'1; Elimc H'1; intros H'1; auto with stalmarck. inversion H'1; auto with stalmarck. case (evalZ Ar a); case (evalZ Ar b); simpl in |- *; auto with stalmarck; intros r1 r2; apply eqStateInvInv; auto with stalmarck. case (updateCorrect Ar War (valRz (evalZ Ar b)) (valRz (evalZ Ar a)) (samePolRz (evalZ Ar b) (evalZ Ar a)) (getClassN Ar (valRz (evalZ Ar b))) (getClassN Ar (valRz (evalZ Ar a)))) with (S := S) (c := c) (d := d); auto with stalmarck; auto with stalmarck. apply GetClassNProp; auto with stalmarck. apply GetClassNProp; auto with stalmarck. split; auto with stalmarck. red in |- *; apply OlistCons; auto with stalmarck. apply getClassOlist; auto with stalmarck. intros c H'1. apply updateArrayOtherwise; auto with stalmarck. Contradict H'1; simpl in |- *; auto with stalmarck. red in |- *; repeat apply InEqSkip; auto with stalmarck. Contradict H'1; rewrite H'1; simpl in |- *; auto with stalmarck. red in |- *; apply InEqHead; auto with stalmarck. Contradict H'1; rewrite H'1; auto with stalmarck. red in |- *; apply InEqSkip; apply InEqHead; auto with stalmarck. case (rZDec (evalZ Ar a) (evalZ Ar b)); simpl in |- *; auto with stalmarck. intros H'0 H'1; split; auto with stalmarck. split; auto with stalmarck. red in |- *; intros c d; split; intros H'2. apply rArrayStateDef1 with (S := S); auto with stalmarck. apply eqStateIncl with (2 := H'2); auto with stalmarck. apply inclStateIn; simpl in |- *; auto with stalmarck. intros a0 b0 H'3; Elimc H'3; intros H'3; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. inversion H'3; auto with stalmarck. rewrite <- H1; rewrite <- H0; auto with stalmarck. apply eqStateaddEq2. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. split; auto with stalmarck. red in |- *; apply OlistNil; auto with stalmarck. intros H'0 H'1; red in |- *; exists a. apply eqStateRzTrans with (b := b); auto with stalmarck. apply eqStateaddEq2; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. rewrite evalZComp; auto with stalmarck. generalize H'0 H'1; case (evalZ Ar a); case (evalZ Ar b); unfold eqRz in |- *; simpl in |- *; intros r r0 H'4 H'5; rewrite H'5; auto with stalmarck; case H'4; rewrite H'5; auto with stalmarck. Qed.
imports: Stalmarck(stateDec)