Triplet.v

Require Export Normalize.
Require Export Relation_Definitions.
Require Export PolyList.

Mutual Inductive EqualBefore[n:rNat; f:rNat ->bool; g:rNat ->bool]: Prop :=
     EqualBeforeDef: ((m:rNat) (rle m n) ->(f m)=(g m)) ->(EqualBefore n f g) .
Hints Resolve EqualBeforeDef.

Lemma EqualBeforeElim:
  (n:rNat) (f, g:rNat ->bool) (EqualBefore n f g) ->(f n)=(g n).
Intros n f g H'; Inversion H'; Auto.
Qed.

Lemma EqualBeforeTrans: (n:rNat)(transitive rNat ->bool (EqualBefore n)).
Intros n; Red; Auto.
Intros x y z H' H'0; Apply EqualBeforeDef; Auto.
Intros m H'1; Apply trans_eq with y := (y m); Auto.
Inversion H'; Auto.
Inversion H'0; Auto.
Qed.

Lemma EqualBeforeLt:
  (n, m:rNat) (f, g:rNat ->bool) (rle n m) -> (EqualBefore m f g) ->
  (EqualBefore n f g).
Intros n m f g H' H'0; Inversion H'0; Apply EqualBeforeDef; Auto.
Intros m0 H'1; Apply H; Auto.
Apply rleTrans with y := n; Auto.
Qed.

Lemma EqualBeforeSym: (n:rNat)(symmetric rNat ->bool (EqualBefore n)).
Intros n; Red.
Intros x y H'; Inversion H'; Apply EqualBeforeDef; Auto.
Intros m H'0; Apply sym_eq; Auto.
Qed.
Hints Resolve EqualBeforeSym.

Fixpoint maxVar[e:rExpr]: rNat :=
   Cases e of
       rT => rO
      | rF => rO
      | (rV n) => n
      | (rN p) => (maxVar p)
      | (rNode n p q) => (rmax (maxVar p) (maxVar q))
   end.

Theorem inLt: (e:rExpr) (n:rNat) (inRExpr n e) ->(rle n (maxVar e)).
Induction e; Intros.
Inversion H.
Inversion H.
Inversion H; Simpl; Auto.
Inversion H0; Simpl; Auto.
Inversion H1; Simpl; Auto.
Apply rleTrans with y := (maxVar r0); Auto.
Apply rleTrans with y := (maxVar r1); Auto.
Qed.

Theorem EqualBeforeREval:
  (f, g:rNat ->bool) (e:rExpr) (EqualBefore (maxVar e) f g) ->
  (rEval f e)=(rEval g e).
Intros f g e H'.
Apply support; Auto.
Intros n H'0.
Apply EqualBeforeElim; Auto.
Apply EqualBeforeLt with m := (maxVar e); Auto.
Apply inLt; Auto.
Qed.

Mutual Inductive triplet: Set :=
     Triplet: rBoolOp -> rZ -> rZ -> rZ ->triplet .

Definition evalTriplet: (rNat ->bool) -> triplet ->bool :=
   [f:rNat ->bool] [t:triplet]
      Cases t of
          (Triplet n v1 v2 v3) =>
            (eqb (fEval f v1) ((rBoolOpFun n) (fEval f v2) (fEval f v3)))
      end.

Definition maxVarTriplet :=
   [t:triplet]
      Cases t of
          (Triplet n v1 v2 v3) => (rmax (rmax (valRz v1) (valRz v2)) (valRz v3))
      end.

Mutual Inductive inTriplet: rNat -> triplet ->Prop :=
     inFirst:
       (r:rNat) (i1, i2, i3:rZ) (n:rBoolOp) (inRz r i1) ->
       (inTriplet r (Triplet n i1 i2 i3))
    | inSecond:
        (r:rNat) (i1, i2, i3:rZ) (n:rBoolOp) (inRz r i2) ->
        (inTriplet r (Triplet n i1 i2 i3))
    | inThird:
        (r:rNat) (i1, i2, i3:rZ) (n:rBoolOp) (inRz r i3) ->
        (inTriplet r (Triplet n i1 i2 i3)) .
Hints Resolve inFirst inSecond inThird.

Lemma inLtMaxTriplet:
  (t:triplet) (i:rNat) (inTriplet i t) ->(rle i (maxVarTriplet t)).
Intros t; Case t; Simpl; Auto.
Intros r r0 r1 r2 i H'; Inversion H'; Auto.
Inversion H1; Simpl; Auto.
Inversion H1; Simpl; Auto.
Inversion H1; Simpl; Auto.
Qed.
Hints Resolve inLtMaxTriplet.

Lemma EqualBeforeEvalTriplet:
  (f, g:rNat ->bool) (t:triplet) (EqualBefore (maxVarTriplet t) f g) ->
  (evalTriplet f t)=(evalTriplet g t).
Intros f g t; Case t; Simpl; Auto.
Intros r r0 r1 r2 H'; Inversion H'.
Cut (fEval f r0)=(fEval g r0); [Intros Eq1; Rewrite Eq1 | Idtac]; Auto.
Cut (fEval f r1)=(fEval g r1); [Intros Eq2; Rewrite Eq2 | Idtac]; Auto.
Cut (fEval f r2)=(fEval g r2); [Intros Eq3; Rewrite Eq3 | Idtac]; Auto.
Generalize H; Case r2; Simpl; Auto; Intros r3 H'0; Rewrite H'0; Simpl; Auto.
Generalize H; Case r1; Simpl; Auto; Intros r3 H'0; Rewrite H'0; Simpl; Auto.
Generalize H; Case r0; Simpl; Auto; Intros r3 H'0; Rewrite H'0; Simpl; Auto.
Qed.
Hints Resolve EqualBeforeEvalTriplet.

Mutual Inductive tripletResult: Set :=
     tRC: (list triplet) -> rZ -> rNat ->tripletResult .

Local nT := (nil triplet).

Fixpoint maxVarTriplets[l:(list triplet)]: rNat :=
   Cases l of
       nil => rO
      | (cons t q) => (rmax (maxVarTriplet t) (maxVarTriplets q))
   end.

Mutual Inductive realizeTriplets: (rNat ->bool) -> (list triplet) ->Prop :=
     realizeNil: (f:rNat ->bool)(realizeTriplets f nT)
    | realizeCons:
        (f:rNat ->bool)
        (t:triplet)
        (l:(list triplet)) (realizeTriplets f l) -> (evalTriplet f t)=true ->
        (realizeTriplets f (cons t l)) .
Hints Resolve realizeNil realizeCons.

Lemma realizeTripletsIn:
  (f:rNat ->bool) (l:(list triplet)) (realizeTriplets f l) ->
  (t:triplet) (In t l) ->(evalTriplet f t)=true.
Intros f l H'; Elim H'; Auto.
Intros f0 t H'0; Inversion H'0; Auto.
Intros f0 t l0 H'0 H'1 H'2 t0 H'3; Case H'3; Auto.
Intros H'4; Rewrite <- H'4; Auto.
Qed.
Hints Resolve realizeTripletsIn.

Lemma inRealizeTriplets:
  (f:rNat ->bool)
  (l:(list triplet)) ((t:triplet) (In t l) ->(evalTriplet f t)=true) ->
  (realizeTriplets f l).
Intros f l; Elim l; Auto with datatypes.
Qed.
Hints Resolve inRealizeTriplets.

Lemma realizeTripletIncl:
  (f:rNat ->bool)
  (l1, l2:(list triplet)) (realizeTriplets f l1) -> (incl l2 l1) ->
  (realizeTriplets f l2).
Intros f l1 l2 H' H'0.
Apply inRealizeTriplets; Auto.
Intros t H'1.
Apply realizeTripletsIn with l := l1; Auto.
Qed.

Lemma maxVarTripletConsLeft:
  (l:(list triplet)) (t:triplet)
  (rle (maxVarTriplets l) (maxVarTriplets (cons t l))).
Intros l; Case l; Simpl; Auto.
Qed.

Lemma maxVarTripletConsRight:
  (l:(list triplet)) (t:triplet)
  (rle (maxVarTriplet t) (maxVarTriplets (cons t l))).
Intros l; Case l; Simpl; Auto.
Qed.
Hints Resolve maxVarTripletConsLeft maxVarTripletConsRight.

Lemma supportTriplets:
  (f, g:rNat ->bool)
  (l:(list triplet))
  (realizeTriplets f l) -> (EqualBefore (maxVarTriplets l) f g) ->
  (realizeTriplets g l).
Intros f g l H'; Elim H'; Auto.
Intros f0 t l0 H'0 H'1 H'2 H'3; Apply realizeCons; Auto.
Apply H'1; Auto.
Apply EqualBeforeLt with m := (maxVarTriplets (cons t l0)); Auto.
Apply trans_eq with y := (evalTriplet f0 t); Auto.
Apply sym_eq.
Apply EqualBeforeEvalTriplet; Auto.
Apply EqualBeforeLt with m := (maxVarTriplets (cons t l0)); Auto.
Qed.
Hints Resolve supportTriplets.

Lemma maxVarNodeLeft:
  (n:rBoolOp) (e1, e2:rExpr)(rle (maxVar e1) (maxVar (rNode n e1 e2))).
Simpl; Auto.
Qed.
Hints Resolve maxVarNodeLeft.

Lemma maxVarNodeRight:
  (n:rBoolOp) (e1, e2:rExpr)(rle (maxVar e2) (maxVar (rNode n e1 e2))).
Simpl; Auto.
Qed.
Hints Resolve maxVarNodeRight.

Definition ExtendFun :=
   [n:rNat] [g:rNat ->bool] [s:bool] [m:rNat]
      Cases (rleDecBis m n) of
          left => (g m)
         | right => s
      end.

Lemma EqualBeforeExtend:
  (g:rNat ->bool) (n:rNat) (s:bool)(EqualBefore n g (ExtendFun n g s)).
Intros g n s; Simpl; Auto.
Apply EqualBeforeDef; Auto.
Intros m H'; Unfold ExtendFun; Case (rleDecBis m n); Auto.
Intros H'0; Case H'0; Auto.
Qed.
Hints Resolve EqualBeforeExtend.

Lemma ExtendFunfEval:
  (g:rNat ->bool) (n:rNat) (p:rZ) (s:bool) (rZLe p n) ->
  (fEval (ExtendFun n g s) p)=(fEval g p).
Intros g n p; Case p; Unfold rZLe; Simpl; Auto.
Intros r s H'.
Unfold ExtendFun.
Case (rleDecBis r n); Auto.
Intros H'0; Case H'0; Auto.
Intros r s H'; Unfold ExtendFun; Case (rleDecBis r n); Auto.
Intros H'0; Case H'0; Auto.
Qed.

Lemma EqualBeforefEval:
  (f, g:rNat ->bool) (n:rNat) (p:rZ) (rZLe p n) -> (EqualBefore n f g) ->
  (fEval f p)=(fEval g p).
Intros f g n p; Case p; Unfold rZLe; Simpl; Auto.
Intros r H' H'0; Inversion H'0; Auto.
Intros r H' H'0; Inversion H'0; Auto.
Rewrite (H r); Auto.
Qed.

Theorem EqualBeforeNext:
  (f, g:rNat ->bool)
  (n:rNat) (EqualBefore n f g) -> (f (rnext n))=(g (rnext n)) ->
  (EqualBefore (rnext n) f g).
Intros f g n H' H'0; Inversion H'.
Apply EqualBeforeDef; Auto.
Intros m; Case (rleDecBis m n); Auto.
Intros H'1 H'2.
Elim (rleNext m n); [Intros H'4; Rewrite H'4 | Intros H'4 | Idtac]; Auto.
Qed.

Mutual Inductive maxTriplet: rNat -> triplet ->Prop :=
     maxTripletDef:
       (n:rNat)
       (r:rBoolOp) (i1, i2, i3:rZ) (rZLe i1 n) -> (rZLe i2 n) -> (rZLe i3 n) ->
       (maxTriplet n (Triplet r i1 i2 i3)) .

Theorem maxTripletInv1:
  (n:rNat) (r:rBoolOp) (i1, i2, i3:rZ) (maxTriplet n (Triplet r i1 i2 i3)) ->
  (rZLe i1 n).
Intros n r i1 i2 i3 H'; Inversion H'; Auto.
Qed.

Theorem maxTripletInv2:
  (n:rNat) (r:rBoolOp) (i1, i2, i3:rZ) (maxTriplet n (Triplet r i1 i2 i3)) ->
  (rZLe i2 n).
Intros n r i1 i2 i3 H'; Inversion H'; Auto.
Qed.

Theorem maxTripletInv3:
  (n:rNat) (r:rBoolOp) (i1, i2, i3:rZ) (maxTriplet n (Triplet r i1 i2 i3)) ->
  (rZLe i3 n).
Intros n r i1 i2 i3 H'; Inversion H'; Auto.
Qed.

Mutual Inductive maxListTriplet[n:rNat]: (list triplet) ->Prop :=
     maxListTripletNil: (maxListTriplet n (nil triplet))
    | maxListTripletCons:
        (t:triplet)
        (L:(list triplet)) (maxTriplet n t) -> (maxListTriplet n L) ->
        (maxListTriplet n (cons t L)) .

Theorem maxListTripletInv:
  (n:rNat) (t:triplet) (L:(list triplet)) (maxListTriplet n L) -> (In t L) ->
  (maxTriplet n t).
Intros n t L H'; Elim H'; Auto.
Intros H'0; Inversion H'0.
Simpl; Auto.
Intros t0 L0 H'0 H'1 H'2 H'3; Elim H'3;
[Intros H'4; Rewrite <- H'4 | Intros H'4]; Auto.
Qed.

Theorem inCons: (t:triplet) (L:(list triplet))(In t (cons t L)).
Simpl; Auto.
Qed.

Theorem maxListTripletTail:
  (n:rNat) (t:triplet) (L:(list triplet)) (maxListTriplet n (cons t L)) ->
  (maxListTriplet n L).
Intros n t L H'; Inversion H'; Auto.
Qed.

Theorem MaxTripletLe:
  (a, b:rNat) (t:triplet) (maxTriplet a t) -> (rle a b) ->(maxTriplet b t).
Intros a b t H' leab; Inversion H'.
Apply maxTripletDef; Apply rZLeTrans with n := a; Auto.
Qed.

Theorem MaxTripletMaxVarTriplet: (t:triplet)(maxTriplet (maxVarTriplet t) t).
Intros t; Case t.
Intros r r0 r1 r2.
Apply maxTripletDef; Auto.
Case r0; Case r1; Case r2; Unfold rZLe; Simpl; Auto.
Case r0; Case r1; Case r2; Unfold rZLe; Simpl; Auto.
Case r0; Case r1; Case r2; Unfold rZLe; Simpl; Auto.
Qed.

Theorem MaxTripletListLe:
  (a, b:rNat) (L:(list triplet)) (maxListTriplet a L) -> (rle a b) ->
  (maxListTriplet b L).
Intros a b L H'; Elim H'; Simpl; Auto.
Intros H'0.
Apply maxListTripletNil; Auto.
Intros t L0 H'0 H'1 H'2 H'3.
Apply maxListTripletCons; Auto.
Apply MaxTripletLe with a := a; Auto.
Qed.

Theorem maxListTripletmaxVarTriplets:
  (L:(list triplet))(maxListTriplet (maxVarTriplets L) L).
Intros L; Elim L; Simpl; Auto.
Apply maxListTripletNil; Auto.
Intros a l H'.
Apply maxListTripletCons; Auto.
Apply MaxTripletLe with a := (maxVarTriplet a); Auto.
Apply MaxTripletMaxVarTriplet; Auto.
Apply MaxTripletListLe with a := (maxVarTriplets l); Auto.
Qed.

04/02/99, 11:03