triplet.v
(* Definition of triplets *)
Require Export Bool.
Require Export rZ.
Require Export PolyList.
Require Export normalize.
(* Lifting of f from rNat-> bool to rZ -> bool compatible with rZComp *)
Definition
rZEval: (rNat ->bool) -> rZ ->bool :=
[f:rNat ->bool] [r:rZ]
Cases r of
(rZPlus n) => (f n)
| (rZMinus n) => (negb (f n))
end.
(* A triplet is an operation plus 3 rZ
a = b /\ c are coded as (Triplet rAnd a b c) *)
Mutual Inductive
triplet: Set :=
Triplet: rBoolOp -> rZ -> rZ -> rZ ->triplet .
(* Equality on triplets is decidable *)
Definition
tripletDec: (t1, t2:triplet){t1=t2}+{~ t1=t2}.
Intros t1 t2; Case t1; Case t2.
Intros Op p q r Op' p' q' r'; Case Op; Case Op';
Try (Intros; Right; Red; Intros Eqt; Inversion Eqt; Auto; Fail);
Case (rZDec p p');
Try (Intros; Right; Red; Intros Eqt; Inversion Eqt; Auto; Fail);
Case (rZDec q q');
Try (Intros; Right; Red; Intros Eqt; Inversion Eqt; Auto; Fail);
Case (rZDec r r');
Try (Intros; Right; Red; Intros Eqt; Inversion Eqt; Auto; Fail);
(Intros Eq1 Eq2 Eq3; Rewrite Eq1; Rewrite Eq2; Rewrite Eq3); Auto.
Qed.
(* Evaluation tEval(a=b/\c)=(f(a)=f(b)/\f(b)) *)
Definition
tEval: (rNat ->bool) -> triplet ->bool :=
[f:rNat ->bool] [t:triplet]
Cases t of
(Triplet n v1 v2 v3) =>
(eqb (rZEval f v1) ((rBoolOpFun n) (rZEval f v2) (rZEval f v3)))
end.
(* f realizes a list of triplets if its evaluates all the triplets to true *)
Definition
realizeTriplets: (rNat ->bool) -> (list triplet) ->Prop :=
[f:rNat ->bool] [L:(list triplet)] (t:triplet) (In t L) ->(tEval f t)=true.
Theorem
realizeTripletNil: (f:rNat ->bool)(realizeTriplets f (nil ?)).
Intros f; Red.
Intros t H'; Inversion H'.
Qed.
Hints Resolve realizeTripletNil.
Theorem
realizeTripletCons:
(f:rNat ->bool)
(t:triplet) (L:(list triplet)) (tEval f t)=true -> (realizeTriplets f L) ->
(realizeTriplets f (cons t L)).
Intros f t L H' H'0; Red; Simpl.
Intros t0 H'1; Elim H'1; Intros H'2; Auto; Rewrite <- H'2; Auto.
Qed.
Hints Resolve realizeTripletCons.
Theorem
realizeTripletIncl:
(f:rNat ->bool)
(L1, L2:(list triplet)) (realizeTriplets f L1) -> (incl L2 L1) ->
(realizeTriplets f L2).
Intros f L1 L2 H'0 H'1; Red; Auto.
Qed.
Hints Resolve realizeTripletIncl.
(* An equation is valid if every f that realizes f and f(rZrue)=true
then f(a)=f(b) *)
Definition
validEquation: (list triplet) -> rZ -> rZ ->Prop :=
[L:(list triplet)]
[a, b:rZ] (f:rNat ->bool) (realizeTriplets f L) -> (f zero)=true ->
(rZEval f a)=(rZEval f b).
(* What is the maximal variable of a triplet *)
Definition
maxVarTriplet :=
[t:triplet]
Cases t of
(Triplet n v1 v2 v3) => (rmax (rmax (valRz v1) (valRz v2)) (valRz v3))
end.
(* Iteration to compute the max of a list of triplets *)
Fixpoint
maxVarTriplets[l:(list triplet)]: rNat :=
Cases l of
nil => zero
| (cons t q) => (rmax (maxVarTriplet t) (maxVarTriplets q))
end.
(*Check if a variable is in a triplet *)
Definition
inTriplet :=
[a:rZ] [t:triplet]
Cases t of
(Triplet n v1 v2 v3) => (eqRz a v1) \/ ((eqRz a v2) \/ (eqRz a v3))
end.
Definition
inTripletDec:
(a:rZ) (t:triplet){(inTriplet a t)}+{~ (inTriplet a t)}.
Intros a t; Case t; Simpl; Intros b v1 v2 v3; Unfold eqRz.
Case (rNatDec (valRz a) (valRz v1)); Auto; Case (rNatDec (valRz a) (valRz v2));
Auto; Case (rNatDec (valRz a) (valRz v3)); Auto.
Intros H' H'0 H'1; Right; Red; Intros H'2; Elim H'2; Clear H'2; Intros H'2;
[Idtac | Elim H'2; Clear H'2; Intros H'2]; Auto.
Qed.
(*Check if a variable is in a list of triplets*)
Fixpoint
inTriplets[v:rZ; l:(list triplet)]: Prop :=
Cases l of
nil => (eqRz v (rZPlus zero))
| (cons t q) => (inTriplet v t) \/ (inTriplets v q)
end.
Definition
inTripletsDec:
(a:rZ) (L:(list triplet)){(inTriplets a L)}+{~ (inTriplets a L)}.
Intros a L; Elim L; Simpl; Auto.
Unfold eqRz; Apply rNatDec; Auto.
Intros a0 l H'; Case H'; Auto.
Case (inTripletDec a a0); Auto.
Intros H'0 H'1; Right; Red; Intros H'2; Elim H'2; Auto.
Qed.
Theorem
inTripletsTrue: (L:(list triplet))(inTriplets rZTrue L).
Intros L; Elim L; Simpl; Auto.
Qed.
Theorem
inTripletsFalse: (L:(list triplet))(inTriplets rZFalse L).
Intros L; Elim L; Simpl; Auto.
Qed.
Theorem
inTripletsComp:
(L:(list triplet)) (v:rZ) (inTriplets v L) ->(inTriplets (rZComp v) L).
Intros L; Elim L; Simpl; Auto.
Unfold eqRz; Auto.
Intros v H'; Rewrite <- H'; Case v; Auto.
Intros a; Case a; Simpl; Auto.
Unfold eqRz; Auto.
Intros H' r r0 r1 l H'0 v H'1; Elim H'1; Clear H'1; Intros H'1;
[Elim H'1; Clear H'1; Intros H'1;
[Rewrite <- H'1 | Elim H'1; Clear H'1; Intros H'1; Rewrite <- H'1] | Idtac];
Auto; Case v; Auto.
Qed.
Theorem
inTripletsCompInv:
(L:(list triplet)) (v:rZ) (inTriplets (rZComp v) L) ->(inTriplets v L).
Intros L v H'; Rewrite (rZCompInvol v).
Apply inTripletsComp; Auto.
Qed.
Theorem
inTripletsIn:
(t:triplet) (L:(list triplet)) (v:rZ) (inTriplet v t) -> (In t L) ->
(inTriplets v L).
Intros t L; Elim L; Simpl; Auto.
Intros v H' H'0; Elim H'0; Auto.
Intros a l H' v H'0 H'1; Elim H'1; Intros H'2; Auto; Rewrite H'2; Auto.
Qed.
Fixpoint
varTriplets[L:(list triplet)]: (list rZ) :=
Cases L of
nil => (cons rZTrue (nil ?))
| (cons (Triplet _ p q r) L') =>
(cons p (cons q (cons r (varTriplets L'))))
end.
Lemma
varTripletTrue: (L:(list triplet))(In rZTrue (varTriplets L)).
Induction L; Simpl; Auto.
Intros t L' HR; Case t; Simpl; Auto.
Qed.
Lemma
varTripletTriplet1:
(p, q, r:rZ) (b:rBoolOp) (L:(list triplet)) (In (Triplet b p q r) L) ->
(In p (varTriplets L)).
Induction L; Simpl; Auto.
Intros t L' HR Ht; Elim Ht; Intros Ht1; [Rewrite Ht1 | Case t]; Simpl; Auto.
Qed.
Lemma
varTripletTriplet2:
(p, q, r:rZ) (b:rBoolOp) (L:(list triplet)) (In (Triplet b p q r) L) ->
(In q (varTriplets L)).
Induction L; Simpl; Auto.
Intros t L' HR Ht; Elim Ht; Intros Ht1; [Rewrite Ht1 | Case t]; Simpl; Auto.
Qed.
Lemma
varTripletsTriplet3:
(p, q, r:rZ) (b:rBoolOp) (L:(list triplet)) (In (Triplet b p q r) L) ->
(In r (varTriplets L)).
Induction L; Simpl; Auto.
Intros t L' HR Ht; Elim Ht; Intros Ht1; [Rewrite Ht1 | Case t]; Simpl; Auto.
Qed.
Lemma
eqRzElim: (a, b:rZ) (eqRz a b) ->a=b \/ a=(rZComp b).
Intros a b; Case a; Case b; Unfold eqRz; Simpl; Intros r r0 H'; Rewrite H'; Auto.
Qed.
Lemma
inTripletsVarTriplet:
(L:(list triplet)) (a:rZ) (inTriplets a L) ->
(In a (varTriplets L)) \/ (In (rZComp a) (varTriplets L)).
Intros L; Elim L; Simpl; Auto.
Intros a H'; Case (eqRzElim ? ? H'); Intros H'1; Rewrite H'1; Auto.
Intros a; Case a; Auto.
Intros r r0 r1 r2 l H' a0 H'0; Elim H'0; Clear H'0; Intros H'0; Auto.
Simpl in H'0; Case H'0; Clear H'0; Intros H'0;
[Idtac | Case H'0; Clear H'0; Intros H'0]; Case (eqRzElim ? ? H'0); Intros H'1;
Rewrite H'1; Simpl; Auto.
Elim (H' ? H'0); Auto with datatypes.
Qed.
29/06/100, 12:53