proposition: Theorem updatePointToClassClassRef1 : forall (r : rNat) (s : rZ) (Lr : list rZ), rArrayGet _ updateArray r = class Lr -> In s Lr -> rArrayGet _ updateArray (valRz s) = ref (samePol s r).
proof: Proof. intros r s Lr. case (rNatDec r a); intros eqra. rewrite eqra; auto with stalmarck; rewrite updateArraya; auto with stalmarck; intros H'; inversion H'. unfold fappendRz in |- *; unfold appendRz in |- *; intros Eqt. case (fappendfInv rZ) with (6 := Eqt); try exact rZltEqComp; auto with stalmarck. intro; apply samePolRzEqRz; auto with stalmarck. intro Eqt'; rewrite updateArrayOtherwise; auto with stalmarck. apply wfPcc1 with (Lr := La); auto with stalmarck. red in |- *; intros H'2; absurd (a = b); auto with stalmarck. red in |- *; intros H'3; absurd (rlt a b); auto with stalmarck. rewrite <- H'3; auto with stalmarck. apply wellFormedArrayInRzBothImpEq with (2 := geta) (3 := getb) (c := rZPlus (valRz s)); auto with stalmarck. red in |- *. unfold InRz in |- *. unfold InRz in |- *; intros; apply InEqComp with (a := s); auto with stalmarck. apply inImpInEq; auto with stalmarck. red in |- *; intros H'2; absurd (InRz (rZPlus a) La). apply wellFormedArrayInImpNotEqSimpl with (2 := geta); auto with stalmarck. rewrite <- H'2. unfold InRz in |- *; simpl in |- *; intros; apply InEqComp with (a := s); auto with stalmarck. apply inImpInEq; auto with stalmarck. red in |- *; intros H'2; absurd (InRz (rZPlus b) La); auto with stalmarck. apply wellFormedArrayInImpNotEq with (2 := getb) (3 := geta); auto with stalmarck. rewrite <- H'2. unfold InRz in |- *; simpl in |- *; intros; apply InEqComp with (a := s); auto with stalmarck. apply inImpInEq; auto with stalmarck. intro Eqt'; elim (appendfInv rZ rZlt eqRz rZltEDec (rZPlus b :: nil) Lb (samePolRz pol s)); auto with stalmarck. simpl in |- *; intros Int. Elimc Int; intros Int; [ idtac | Elimc Int; clear Int ]; auto with stalmarck. replace (valRz s) with b. rewrite updateArrayb; auto with stalmarck. generalize Int; case s; case pol; simpl in |- *; auto with stalmarck; intros; discriminate. rewrite <- (samePolRzValRz pol b); rewrite Int; case pol; case s; simpl in |- *; auto with stalmarck. intros Int; replace (valRz s) with (valRz (samePolRz pol s)); auto with stalmarck. rewrite updateArrayInb; auto with stalmarck. case pol; case s; simpl in |- *; auto with stalmarck. case pol; case s; simpl in |- *; auto with stalmarck. rewrite <- (PolyListAux.map_id rZ (samePolRz pol) (samePolRzsamePolRz pol) (appendf rZ rZlt eqRz rZltEDec (rZPlus b :: nil) Lb)) ; auto with stalmarck. apply in_map; auto with stalmarck. case (rNatDec r b); intros eqrb. rewrite eqrb; auto with stalmarck; rewrite updateArrayb; auto with stalmarck; intros H'; discriminate. case (InRzDec (rZPlus r) Lb); intros InRLb; auto with stalmarck. case (InEqInv (rZPlus r) Lb); auto with stalmarck; intros InRLb'. replace r with (valRz (rZPlus r)); auto with stalmarck; rewrite updateArrayInb; auto with stalmarck; intros H'; discriminate. replace r with (valRz (rZMinus r)); auto with stalmarck; rewrite updateArrayInb; auto with stalmarck; intros H'; discriminate. case (rNatDec (valRz s) a); intros eqsa. intros H' H'0. absurd (InRz (rZPlus a) Lr); auto with stalmarck. apply wellFormedArrayInImpNotEq with (Ar := Ar) (b := r) (La := La); auto with stalmarck. apply updateGetIsClass with (1 := H'); auto with stalmarck. red in |- *; apply InEqComp with (a := s); auto with stalmarck. apply inImpInEq; auto with stalmarck. case (rNatDec (valRz s) b); intros eqsb. intros H' H'0. absurd (InRz (rZPlus b) Lr); auto with stalmarck. apply wellFormedArrayInImpNotEq with (Ar := Ar) (b := r) (La := Lb); auto with stalmarck. apply updateGetIsClass with (1 := H'); auto with stalmarck. red in |- *; apply InEqComp with (a := s); auto with stalmarck. apply inImpInEq; auto with stalmarck. rewrite updateArrayOtherwise; auto with stalmarck. intros H' H'0; rewrite updateArrayOtherwise; auto with stalmarck. apply wfPcc1 with (Lr := Lr); auto with stalmarck. red in |- *; intros H'2; absurd (r = b); auto with stalmarck. apply wellFormedArrayInRzBothImpEq with (Ar := Ar) (c := s) (La := Lr) (Lb := Lb); auto with stalmarck. red in |- *; apply InEqComp with (a := s); auto with stalmarck. apply inImpInEq; auto with stalmarck. red in |- *; apply InEqComp with (a := rZPlus (valRz s)); auto with stalmarck. Qed.