proposition: Theorem addInterAuxProp : forall (L : list rZ) (Ar1 Ar2 Ar3 : rArray vM) (War1 : wellFormedArray Ar1) (War2 : wellFormedArray Ar2) (War3 : wellFormedArray Ar3) (S1 S2 S3 : State), rArrayState Ar1 S1 -> rArrayState Ar2 S2 -> rArrayState Ar3 S3 -> inclState S1 S2 -> inclState S1 S3 -> match addInterAux Ar2 Ar3 L Ar1 with | (Ar4, L1) => wellFormedArray Ar4 /\ (exists S4 : State, rArrayState Ar4 S4 /\ inclState S4 S2 /\ inclState S4 S3 /\ inclState S1 S4 /\ (forall a : rNat, InRz (rZPlus a) L -> eqStateRz S4 (rZPlus a) (getEquivMin Ar2 Ar3 a))) /\ (forall e : rNat, ~ InRz (rZPlus e) L1 -> rArrayGet _ Ar4 e = rArrayGet _ Ar1 e) /\ OlistRz L1 end.
proof: Proof. intros L Ar1 Ar2 Ar3 H' H'0 H'1 S1 S2 S3 H'2 H'3 H'4 H'5 H'6. elim L; simpl in |- *. split; [ idtac | split; [ exists S1; repeat split | idtac ] ]; auto with stalmarck. intros H'7; apply rArrayStateDef1 with (S := S1); auto with stalmarck. intros H'7; apply rArrayStateDef2 with (Ar := Ar1); auto with stalmarck. intros a H'7; inversion H'7. split; auto with stalmarck. red in |- *; apply OlistNil; auto with stalmarck. intros a l; case (addInterAux Ar2 Ar3 l Ar1). intros Ar3' L2 H'7; Elimc H'7; intros H'7 H'8; Elimc H'8; intros H'8 H'9; Elimc H'8; intros S4 E; Elimc E; intros H'8 H'10; Elimc H'10; intros H'10 H'11; Elimc H'11; intros H'11 H'12; Elimc H'12; intros H'12 H'13. Elimc H'9; intros H'9 H'14. generalize (addEqMemCorrect Ar3' (rZPlus (valRz a)) (getEquivMin Ar2 Ar3 (valRz a)) S4 H'7 H'8); case (addEqMem Ar3' (rZPlus (valRz a)) (getEquivMin Ar2 Ar3 (valRz a))); auto with stalmarck. intros Ar3'' b L2'; case b. intros H'15; absurd (contradictory S2). apply rArrayContradictory with (Ar := Ar2); auto with stalmarck. case H'15. intros x H'16; exists x. apply eqStateIncl with (S1 := addEq (rZPlus (valRz a), getEquivMin Ar2 Ar3 (valRz a)) S4); auto with stalmarck. apply inclStateAddEqInv; auto with stalmarck. apply getEquivMinEq1; auto with stalmarck. intros H'15; Elimc H'15; intros H'15 H'16; Elimc H'16; intros H'16 H'17; Elimc H'17; intros H'17 H'18. split; auto with stalmarck; split; auto with stalmarck. exists (addEq (rZPlus (valRz a), getEquivMin Ar2 Ar3 (valRz a)) S4); repeat split; auto with stalmarck. intros H'19; apply rArrayStateDef1 with (1 := H'16); auto with stalmarck. intros H'19; apply rArrayStateDef2 with (1 := H'16); auto with stalmarck. apply inclStateAddEqInv; auto with stalmarck. apply getEquivMinEq1; auto with stalmarck. apply inclStateAddEqInv; auto with stalmarck. apply getEquivMinEq2; auto with stalmarck. apply inclStateTrans with S4; auto with stalmarck. intros a0 H'19; inversion H'19. case eqRzElim with (1 := H1); auto with stalmarck. intros H'20; rewrite <- H'20; simpl in |- *; auto with stalmarck. intros H'20; replace a with (rZComp (rZPlus a0)). simpl in |- *; auto with stalmarck. rewrite H'20; rewrite rZCompInv; auto with stalmarck. apply eqStateaddEq2; auto with stalmarck. split; auto with stalmarck. intros e H'19. rewrite H'18; auto with stalmarck. apply H'9; auto with stalmarck. Contradict H'19; auto with stalmarck. unfold appendRz in |- *. generalize (appendfInclEq1 _ rZlt eqRz rZltEDec L2 L2'); intros H'22; inversion H'22; auto with stalmarck. apply H; auto with stalmarck. Contradict H'19; auto with stalmarck. unfold appendRz in |- *. generalize (appendfInclEq2 _ rZlt eqRz eqrZSym eqrZTrans rZltEDec L2 L2'); intros H'20; inversion H'20; auto with stalmarck. apply H; auto with stalmarck. red in |- *; unfold appendRz in |- *; apply appendfOlist; auto with stalmarck. try exact rZltEqComp. Qed.
imports: Stalmarck(rZ) Stalmarck(OrderedListEq) Stalmarck(LetP) Coq(Relation_Definitions) Stalmarck(state) Stalmarck(restrictState) Stalmarck(ltState)