doTriplet.v

(* One step propagation *)

Require Export unionState.
Require Export stateExtra.

(*We define the Stalmarck One Step Saturation as a relation *)

Mutual Inductive doTripletP[S:State]: triplet -> State ->Prop :=
     doTripletAndPpmq:
       (p, q, r:rZ) (eqStateRz S p (rZComp q)) ->
       (doTripletP
          S (Triplet rAnd p q r) (addEq (q, rZTrue) (addEq (r, rZFalse) S)))
    | doTripletAndPpmr:
        (p, q, r:rZ) (eqStateRz S p (rZComp r)) ->
        (doTripletP
           S (Triplet rAnd p q r) (addEq (q, rZFalse) (addEq (r, rZTrue) S)))
    | doTripletAndPqr:
        (p, q, r:rZ) (eqStateRz S q r) ->
        (doTripletP S (Triplet rAnd p q r) (addEq (p, r) S))
    | doTripletAndPqmr:
        (p, q, r:rZ) (eqStateRz S q (rZComp r)) ->
        (doTripletP S (Triplet rAnd p q r) (addEq (p, rZFalse) S))
    | doTripletAndPpT:
        (p, q, r:rZ) (eqStateRz S p rZTrue) ->
        (doTripletP
           S (Triplet rAnd p q r) (addEq (q, rZTrue) (addEq (r, rZTrue) S)))
    | doTripletAndPqT:
        (p, q, r:rZ) (eqStateRz S q rZTrue) ->
        (doTripletP S (Triplet rAnd p q r) (addEq (p, r) S))
    | doTripletAndPqF:
        (p, q, r:rZ) (eqStateRz S q rZFalse) ->
        (doTripletP S (Triplet rAnd p q r) (addEq (p, rZFalse) S))
    | doTripletAndPrT:
        (p, q, r:rZ) (eqStateRz S r rZTrue) ->
        (doTripletP S (Triplet rAnd p q r) (addEq (p, q) S))
    | doTripletAndPrF:
        (p, q, r:rZ) (eqStateRz S r rZFalse) ->
        (doTripletP S (Triplet rAnd p q r) (addEq (p, rZFalse) S))
    | doTripletEqPpq:
        (p, q, r:rZ) (eqStateRz S p q) ->
        (doTripletP S (Triplet rEq p q r) (addEq (r, rZTrue) S))
    | doTripletEqPpmq:
        (p, q, r:rZ) (eqStateRz S p (rZComp q)) ->
        (doTripletP S (Triplet rEq p q r) (addEq (r, rZFalse) S))
    | doTripletEqPpr:
        (p, q, r:rZ) (eqStateRz S p r) ->
        (doTripletP S (Triplet rEq p q r) (addEq (q, rZTrue) S))
    | doTripletEqPpmr:
        (p, q, r:rZ) (eqStateRz S p (rZComp r)) ->
        (doTripletP S (Triplet rEq p q r) (addEq (q, rZFalse) S))
    | doTripletEqPqr:
        (p, q, r:rZ) (eqStateRz S q r) ->
        (doTripletP S (Triplet rEq p q r) (addEq (p, rZTrue) S))
    | doTripletEqPqmr:
        (p, q, r:rZ) (eqStateRz S q (rZComp r)) ->
        (doTripletP S (Triplet rEq p q r) (addEq (p, rZFalse) S))
    | doTripletEqPpT:
        (p, q, r:rZ) (eqStateRz S p rZTrue) ->
        (doTripletP S (Triplet rEq p q r) (addEq (q, r) S))
    | doTripletEqPpF:
        (p, q, r:rZ) (eqStateRz S p rZFalse) ->
        (doTripletP S (Triplet rEq p q r) (addEq (q, (rZComp r)) S))
    | doTripletEqPqT:
        (p, q, r:rZ) (eqStateRz S q rZTrue) ->
        (doTripletP S (Triplet rEq p q r) (addEq (p, r) S))
    | doTripletEqPqF:
        (p, q, r:rZ) (eqStateRz S q rZFalse) ->
        (doTripletP S (Triplet rEq p q r) (addEq (p, (rZComp r)) S))
    | doTripletEqPrT:
        (p, q, r:rZ) (eqStateRz S r rZTrue) ->
        (doTripletP S (Triplet rEq p q r) (addEq (p, q) S))
    | doTripletEqPrF:
        (p, q, r:rZ) (eqStateRz S r rZFalse) ->
        (doTripletP S (Triplet rEq p q r) (addEq (p, (rZComp q)) S)) .
Hints Resolve
doTripletAndPpmq doTripletAndPpmr doTripletAndPqr doTripletAndPqmr
doTripletAndPpT doTripletAndPqT doTripletAndPqF doTripletAndPrT doTripletAndPrF
doTripletEqPpq doTripletEqPpmq doTripletEqPpr doTripletEqPpmr doTripletEqPqr
doTripletEqPqmr doTripletEqPpT doTripletEqPpF doTripletEqPqT doTripletEqPqF
doTripletEqPrT doTripletEqPrF.

Theorem doTripletEqAux1:
  (p, q:rZ)
  (S1, S3:State)
  (t:triplet)
  (doTripletP S1 t (addEq (p, q) S1)) ->
  (eqState S1 S3) -> (doTripletP S3 t (addEq (p, q) S3)) ->
  (Ex [S4:State] (doTripletP S3 t S4) /\ (eqState S4 (addEq (p, q) S1))).
Intros p q S1 S3 t H' H'0 H'1; Exists (addEq (p, q) S3); Split; Auto.
Qed.

Theorem doTripletEqAux2:
  (p, q, r, s:rZ)
  (S1, S3:State)
  (t:triplet)
  (doTripletP S1 t (addEq (p, q) (addEq (r, s) S1))) ->
  (eqState S1 S3) -> (doTripletP S3 t (addEq (p, q) (addEq (r, s) S3))) ->
  (ex
     State
     [S4:State]
     (doTripletP S3 t S4) /\ (eqState S4 (addEq (p, q) (addEq (r, s) S1)))).
Intros p q r s S1 S3 t H' H'0; Exists (addEq (p, q) (addEq (r, s) S3)); Split;
Auto.
Qed.

Theorem doTripletEqCompEx:
  (S1, S2, S3:State) (t:triplet) (doTripletP S1 t S2) -> (eqState S1 S3) ->
  (Ex [S4:State] (doTripletP S3 t S4) /\ (eqState S4 S2)).
Intros S1 S2 S3 t H' H'1; Inversion H';
Apply doTripletEqAux2 Orelse Apply doTripletEqAux1; Auto;
Generalize (eqStateEq ? ? ? ? H'1 H); Auto.
Qed.

Theorem doTripletUnionEx1:
  (p, q:rZ) (S1:State) (t:triplet) (doTripletP S1 t (addEq (p, q) S1)) ->
  (Ex [S3:State] (addEq (p, q) S1)=(unionState S3 S1)).
Intros p q S1 t H'; Exists (cons (p, q) (nil rZ * rZ)); Auto.
Qed.

Theorem doTripletUnionEx2:
  (p, q, r, s:rZ)
  (S1:State) (t:triplet) (doTripletP S1 t (addEq (p, q) (addEq (r, s) S1))) ->
  (Ex [S3:State] (addEq (p, q) (addEq (r, s) S1))=(unionState S3 S1)).
Intros p q r s S1 t H'; Exists (cons (p, q) (cons (r, s) (nil ?))); Auto.
Qed.

Theorem doTripletUnionEx:
  (S1, S2:State) (t:triplet) (doTripletP S1 t S2) ->
  (Ex [S3:State] S2=(unionState S3 S1)).
Intros S1 S2 t H'; Inversion H';
Apply doTripletUnionEx2 with t := t Orelse Apply doTripletUnionEx1 with t := t;
Auto; Rewrite H1; Auto.
Qed.
(* The result is always bigger *)

Theorem doTripletIncl:
  (S1, S2:State) (t:triplet) (doTripletP S1 t S2) ->(inclState S1 S2).
Intros S1 S2 t H'.
Case (doTripletUnionEx S1 S2 t); Auto.
Intros x H'0; Rewrite H'0; Auto.
Qed.

Theorem doTripletUnionAux1:
  (p, q:rZ)
  (S1, S3:State)
  (t:triplet)
  (doTripletP (unionState S3 S1) t (addEq (p, q) (unionState S3 S1))) ->
  (Ex [S4:State]
  (doTripletP (unionState S3 S1) t S4) /\
  (eqState S4 (unionState S3 (addEq (p, q) S1)))).
Intros p q S1 S3 t H'; Exists (addEq (p, q) (unionState S3 S1)); Split; Auto.
Apply eqStateTrans with (unionState (unionState (cons (p, q) (nil ?)) S3) S1);
Auto.
Apply eqStateTrans with (unionState (unionState S3 (cons (p, q) (nil ?))) S1);
Auto.
Apply eqStateSym; Auto.
Replace (addEq (p, q) S1) with (unionState (cons (p, q) (nil ?)) S1); Auto.
Apply unionStateAssoc; Auto.
Qed.

Theorem doTripletUnionAux2:
  (p, q, r, s:rZ)
  (S1, S3:State)
  (t:triplet)
  (doTripletP
     (unionState S3 S1) t (addEq (p, q) (addEq (r, s) (unionState S3 S1)))) ->
  (Ex [S4:State]
  (doTripletP (unionState S3 S1) t S4) /\
  (eqState S4 (unionState S3 (addEq (p, q) (addEq (r, s) S1))))).
Intros p q r s S1 S3 t H';
Exists (addEq (p, q) (addEq (r, s) (unionState S3 S1))); Split; Auto.
Apply eqStateTrans
     with (unionState (unionState (cons (p, q) (cons (r, s) (nil ?))) S3) S1);
Auto.
Apply eqStateTrans
     with (unionState (unionState S3 (cons (p, q) (cons (r, s) (nil ?)))) S1);
Auto.
Apply eqStateTrans
     with (unionState S3 (unionState (cons (p, q) (cons (r, s) (nil ?))) S1));
Auto.
Apply eqStateSym; Auto.
Apply unionStateAssoc.
Qed.

Theorem doTripletCongruentEx:
  (S1, S2, S3:State) (t:triplet) (doTripletP S1 t S2) ->
  (Ex [S4:State]
  (doTripletP (unionState S3 S1) t S4) /\ (eqState S4 (unionState S3 S2))).
Intros S1 S2 S3 t H'; Inversion H';
Apply doTripletUnionAux2 Orelse Apply doTripletUnionAux1; Auto;
Generalize (eqStateIncl ? ? ? ? (unionStateInclR S3 S1) H); Auto.
Qed.

Theorem doTripletMonotoneEx:
  (S1, S2, S3:State) (t:triplet) (doTripletP S1 t S3) -> (inclState S1 S2) ->
  (Ex [S4:State] (doTripletP S2 t S4) /\ (inclState S3 S4)).
Intros S1 S2 S3 t H' H'0.
Elim (doTripletCongruentEx S1 S3 S2 t);
[Intros S4 E; Elim E; Intros H'6 H'7; Clear E | Idtac]; Auto.
Elim (doTripletEqCompEx (unionState S2 S1) S4 S2 t);
[Intros S5 E; Elim E; Intros H'9 H'10; Clear E | Idtac | Idtac]; Auto.
Exists S5; Split; Auto.
Apply inclStateTrans with S2 := (unionState S2 S3); Auto.
Apply inclStateEqStateComp with S1 := S4 S3 := S4; Auto.
Red; Auto.
Qed.

Theorem doTripletConflEx:
  (t1, t2:triplet)
  (S1, S2, S3:State) (doTripletP S1 t1 S2) -> (doTripletP S1 t2 S3) ->
  (Ex [S4:State]
  (Ex [S5:State]
  (doTripletP S2 t2 S4) /\ ((doTripletP S3 t1 S5) /\ (eqState S4 S5)))).
Intros t1 t2 S1 S2 S3 H' H'0.
Elim (doTripletUnionEx S1 S2 t1); [Intros S4 E; Rewrite E | Idtac]; Auto.
Elim (doTripletUnionEx S1 S3 t2); [Intros S5 E0; Rewrite E0 | Idtac]; Auto.
Elim (doTripletCongruentEx S1 S2 S5 t1);
[Intros S6 E1; Elim E1; Intros H'6 H'7; Clear E1 | Idtac]; Auto.
Elim (doTripletCongruentEx S1 S3 S4 t2);
[Intros S7 E1; Elim E1; Intros H'8 H'9; Clear E1 | Idtac]; Auto.
Exists S7; Exists S6; Split; [Idtac | Split]; Auto.
Apply eqStateTrans with S2 := (unionState S4 S3); Auto.
Rewrite E0.
Apply eqStateTrans with S2 := (unionState S5 S2); Auto.
Rewrite E.
Apply eqStateTrans with S2 := (unionState (unionState S4 S5) S1); Auto.
Apply unionStateAssoc; Auto.
Apply eqStateTrans with S2 := (unionState (unionState S5 S4) S1); Auto.
Apply eqStateSym; Auto.
Apply unionStateAssoc; Auto.
Qed.

Lemma realizeStateEvalAux1:
  (f:rNat ->bool)
  (p, q, r, s, t, u:rZ)
  (S:State)
  (EqS:(eqStateRz S p q))
  ((rZEval f p)=(rZEval f q) ->
   (rZEval f r)=(rZEval f s) /\ (rZEval f t)=(rZEval f u)) ->
  (realizeState f S) ->(realizeState f (addEq (r, s) (addEq (t, u) S))).
Intros f p q r s t u S H' H'0 H'1.
Elim H'0; [Intros H'3 H'4; Clear H'0 | Clear H'0].
Apply realizeStateAddEq; Auto.
Apply realizeStateInv with S := S; Auto.
Qed.

Lemma realizeStateEvalAux2:
  (f:rNat ->bool)
  (p, q, r, s:rZ)
  (S:State)
  (EqS:(eqStateRz S p q))
  ((rZEval f p)=(rZEval f q) ->(rZEval f r)=(rZEval f s)) ->
  (realizeState f S) ->(realizeState f (addEq (r, s) S)).
Intros f p q r s S H' H'0 H'1.
LApply H'0; [Intros H'2; Clear H'0 | Clear H'0].
Apply realizeStateAddEq; Auto.
Apply realizeStateInv with S := S; Auto.
Qed.

Theorem realizeStateEval:
  (f:rNat ->bool)
  (S1, S2:State)
  (t:triplet)
  (realizeState f S1) ->
  (doTripletP S1 t S2) -> (tEval f t)=true -> (f zero)=true ->
  (realizeState f S2).
Intros f S1 S2 t H' H'0; Elim H'0; Simpl; Auto; Intros p q r H'1 H'2 H'3;
Apply realizeStateEvalAux1 with 1 := H'1
  Orelse Apply realizeStateEvalAux2 with 1 := H'1; Auto;
Try Rewrite rZEvalCompInv; Try Rewrite rZEvalCompInv; Generalize H'2;
Try Repeat Rewrite H'3; Case (rZEval f p); Simpl; Case (rZEval f q); Simpl;
Case (rZEval f r); Simpl; Auto; Try Repeat Rewrite H'3; Auto.
Qed.

Lemma evalRealizeStateAux1:
  (A:Prop)
  (f:rNat ->bool)
  (p, q, r, s, t, u:rZ)
  (S:State)
  (EqS:(eqStateRz S p q))
  ((rZEval f p)=(rZEval f q) /\
   ((rZEval f r)=(rZEval f s) /\ (rZEval f t)=(rZEval f u)) ->A) ->
  (realizeState f (addEq (r, s) (addEq (t, u) S))) ->A.
Intros A f p q r s t u S H' H'0 H'1.
LApply H'0; [Intros H'2 | Split; [Idtac | Split]]; Auto.
Apply realizeStateInv with S := S; Auto.
Apply realizeStateIncl with 1 := H'1; Auto.
Apply realizeStateInv with 1 := H'1; Auto.
Apply realizeStateInv with 1 := H'1; Auto.
Qed.

Lemma evalRealizeStateAux2:
  (A:Prop)
  (f:rNat ->bool)
  (p, q, r, s:rZ)
  (S:State)
  (EqS:(eqStateRz S p q))
  ((rZEval f p)=(rZEval f q) /\ (rZEval f r)=(rZEval f s) ->A) ->
  (realizeState f (addEq (r, s) S)) ->A.
Intros A f p q r s S H' H'0 H'1.
LApply H'0; [Intros H'2 | Split]; Auto.
Apply realizeStateInv with S := S; Auto.
Apply realizeStateIncl with 1 := H'1; Auto.
Apply realizeStateInv with 1 := H'1; Auto.
Qed.

Theorem evalRealizeState:
  (f:rNat ->bool)
  (S1, S2:State)
  (t:triplet) (doTripletP S1 t S2) -> (realizeState f S2) -> (f zero)=true ->
  (tEval f t)=true.
Intros f S1 S2 t H'; Elim H'; Intros p q r H'1 H2 H'3;
Apply evalRealizeStateAux1 with 1 := H'1 3 := H2
  Orelse Apply evalRealizeStateAux2 with 1 := H'1 3 := H2;
Try Rewrite rZEvalCompInv; Try Rewrite rZEvalCompInv; Simpl; Case (rZEval f p);
Simpl; Case (rZEval f q); Simpl; Case (rZEval f r); Simpl; Auto;
Try Repeat Rewrite H'3; Auto; Intuition.
Qed.
(* Prove that the semantic of doTriplet is correct *)

Theorem realizeStateEvalEquiv:
  (f:rNat ->bool)
  (S1, S2:State)
  (t:triplet) (doTripletP S1 t S2) -> (realizeState f S1) -> (f zero)=true ->
  (iff (realizeState f S2) (tEval f t)=true).
Intros f S1 S2 H' H'0; Red.
Split; Intros H'1.
Apply evalRealizeState with 1 := H'0; Auto.
Apply realizeStateEval with 2 := H'0; Auto.
Qed.

Theorem doTripletBisIncl:
  (t:triplet) (S1, S2:State) (doTripletP S1 t S2) ->
  (S3:State) (doTripletP S1 t S3) ->(inclState S3 S2).
Intros t S1 S2 H12 S3 H13.
Apply realizeStateInclInv; Intros f Pfzero Pf2; Unfold realizeState;
Intros i j Pij; Apply realizeStateInv with S := S3; Auto.
Cut (realizeState f S1); [Intros Pf1 | Idtac].
Apply realizeStateEval with S1 := S1 t := t; Auto.
Apply evalRealizeState with S1 := S1 S2 := S2; Auto.
Apply realizeStateIncl with S1 := S2; Auto.
Apply doTripletIncl with t := t; Auto.
Qed.

(*It does not matter which rule you apply *)

Theorem doTripletEq:
  (S1, S2, S3:State) (t:triplet) (doTripletP S1 t S2) -> (doTripletP S1 t S3) ->
  (eqState S2 S3).
Intros S1 S2 S3 t H' H'0.
Red; Split; Apply doTripletBisIncl with S1 := S1 t := t; Auto.
Qed.
(* Monotony of the saturation *)

Theorem doTripletEqMonotone:
  (S1, S2, S3, S4:State)
  (t:triplet)
  (doTripletP S1 t S3) -> (doTripletP S2 t S4) -> (inclState S1 S2) ->
  (inclState S3 S4).
Intros S1 S2 S3 S4 t H' H'0 H'1.
Elim (doTripletMonotoneEx S1 S2 S3 t);
[Intros S5 E; Elim E; Intros H'8 H'9; Clear E | Idtac | Idtac]; Auto.
Apply inclStateEqStateComp with S1 := S3 S3 := S5; Auto.
Apply doTripletEq with S1 := S2 t := t; Auto.
Qed.
(* It is compatible *)

Theorem doTripletEqComp:
  (t:triplet)
  (S1, S2, S3, S4:State)
  (doTripletP S1 t S3) -> (doTripletP S2 t S4) -> (eqState S1 S2) ->
  (eqState S3 S4).
Intros t S1 S2 S3 S4 H' H'0 H'1.
Elim (doTripletEqCompEx S1 S3 S2 t);
[Intros S5 E; Elim E; Intros H'8 H'9; Clear E | Idtac | Idtac]; Auto.
Apply eqStateTrans with S2 := S5; Auto.
Apply doTripletEq with S1 := S2 t := t; Auto.
Qed.
(* It is confluent *)

Theorem doTripletConfl:
  (t1, t2:triplet)
  (S1, S2, S3, S4, S5:State)
  (doTripletP S1 t1 S2) ->
  (doTripletP S2 t2 S4) -> (doTripletP S1 t2 S3) -> (doTripletP S3 t1 S5) ->
  (eqState S4 S5).
Intros t1 t2 S1 S2 S3 S4 S5 H' H'0 H'1 H'2.
Elim (doTripletConflEx t1 t2 S1 S2 S3);
[Intros S6 E; Elim E; Intros S7 E0; Elim E0; Intros H'10 H'11; Elim H'11;
   Intros H'12 H'13; Clear H'11 E0 E | Idtac | Idtac]; Auto.
Apply eqStateTrans with S2 := S6.
Apply doTripletEqComp with t := t2 S1 := S2 S2 := S2; Auto.
Apply eqStateTrans with S2 := S7; Auto.
Apply doTripletEqComp with t := t1 S1 := S3 S2 := S3; Auto.
Qed.

Theorem doTripletInvolExAux1:
  (tr:triplet)
  (p, q:rZ)
  (S1, S3:State)
  (inclState (addEq (p, q) S1) S3) ->
  (inclState S1 S3) -> (doTripletP S3 tr (addEq (p, q) S3)) ->
  (ex State [S4:State](doTripletP S3 tr S4) /\ (eqState S3 S4)).
Intros tr p q S1 S3 H' H'0 H'1; Exists (addEq (p, q) S3); Split; Auto.
Generalize (eqStateIncl (addEq (p, q) S1)); Intros Eq1; Red; Auto 8.
Qed.

Theorem doTripletInvolExAux2:
  (tr:triplet)
  (p, q, r, s:rZ)
  (S1, S3:State)
  (inclState (addEq (p, q) (addEq (r, s) S1)) S3) ->
  (inclState S1 S3) -> (doTripletP S3 tr (addEq (p, q) (addEq (r, s) S3))) ->
  (ex State [S4:State](doTripletP S3 tr S4) /\ (eqState S3 S4)).
Intros tr p q r s S1 S3 H' H'0 H'1; Exists (addEq (p, q) (addEq (r, s) S3));
Split; Auto.
Generalize (eqStateIncl (addEq (p, q) (addEq (r, s) S1))); Intros Eq1; Red;
Auto 8.
Qed.

Theorem doTripletInvolEx:
  (t:triplet) (S1, S2, S3:State) (doTripletP S1 t S2) -> (inclState S2 S3) ->
  (Ex [S4:State] (doTripletP S3 t S4) /\ (eqState S3 S4)).
Intros t S1 S2 S3 H' H'0; (Generalize (eqStateIncl S1); Intros Eq0);
Cut (inclState S1 S3);
[Idtac |
   Apply inclStateTrans with S2 := S2; Auto; Apply doTripletIncl with t := t;
    Auto]; Generalize H'0; Clear H'0; Elim H'; Intros p q r H'0 H'1 H'2;
Apply doTripletInvolExAux2 with 1 := H'1
  Orelse Apply doTripletInvolExAux1 with 1 := H'1; Auto.
Qed.
(* We use a triplet only once *)

Theorem doTripletInvol:
  (t:triplet)
  (S1, S2, S3, S4:State)
  (doTripletP S1 t S2) -> (inclState S2 S3) -> (doTripletP S3 t S4) ->
  (eqState S3 S4).
Intros t S1 S2 S3 S4 H' H'0 H'1.
Elim (doTripletInvolEx t S1 S2 S3);
[Intros S5 E; Elim E; Intros H'8 H'9; Clear E | Idtac | Idtac]; Auto.
Apply eqStateTrans with S2 := S5; Auto.
Apply doTripletEqComp with t := t S1 := S3 S2 := S3; Auto.
Qed.

29/06/100, 12:53