Make_triplets_def.v

Require Export EqNat.
Require Export Max.
Require Export Compare_dec.
Require Export Int.
Require Export Normalise.

Definition egaux_avant :=
   [n:nat] [f, g:nat ->bool] (k:nat) (le k n) ->(f k)=(g k).

Lemma egaux_avant_elim:
  (n:nat) (f, g:nat ->bool) (egaux_avant n f g) ->(f n)=(g n).
Intros; Unfold egaux_avant; Intros; Auto.
Qed.

Lemma egaux_avant_refl: (n:nat) (f:nat ->bool)(egaux_avant n f f).
Intros; Unfold egaux_avant; Intros; Auto.
Qed.

Lemma egaux_avant_trans:
  (n:nat) (f, g, h:nat ->bool) (egaux_avant n f g) -> (egaux_avant n g h) ->
  (egaux_avant n f h).
Unfold egaux_avant; Intros; Auto.
Rewrite (H k); Auto.
Qed.

Lemma egaux_avant_crois:
  (n, m:nat) (f, g:nat ->bool) (le n m) -> (egaux_avant m f g) ->
  (egaux_avant n f g).
Unfold egaux_avant; Intros; Apply H0; Apply le_trans with n; Auto.
Qed.
Hint egaux_avant_elim egaux_avant_refl egaux_avant_trans egaux_avant_crois.

Lemma egaux_avant_sym:
  (n:nat) (f, g:nat ->bool) (egaux_avant n f g) ->(egaux_avant n g f).
Unfold egaux_avant; Intros; Auto.
Rewrite H; Auto.
Qed.
Hint egaux_avant_sym.

Lemma egaux_avant_S:
  (n:nat) (f, g:nat ->bool) (egaux_avant n f g) -> (f (S n))=(g (S n)) ->
  (egaux_avant (S n) f g).
Unfold egaux_avant; Intros; Auto.
Case (le_lt_dec k n); Auto.
Intros.
Cut k=(S n); Auto.
Intros N; Rewrite N; Auto.
Qed.
Hint egaux_avant_S.

Fixpoint max_var[e:expr2]: nat :=
   Cases e of
       T2 => O
      | F2 => O
      | (V2 n) => n
      | (N2 p) => (max_var p)
      | (Node2 n p q) => (max (max_var p) (max_var q))
   end.

Theorem th_le_max_var: (e:expr2) (n:nat) (in_expr2 n e) ->(le n (max_var e)).
Induction e; Intros.
Inversion H.
Inversion H.
Inversion H; Simpl; Auto.
Inversion H0; Simpl; Auto.
Inversion H1;
 [Simpl; Apply le_trans with (max_var e0) |
   Simpl; Apply le_trans with (max_var e1)]; Auto.
Qed.

Theorem support2b:
  (f, g:nat ->bool) (e:expr2) (egaux_avant (max_var e) f g) ->
  (eval2 f e)=(eval2 g e).
Unfold egaux_avant; Intros; Apply support2; Intros; Apply H;
 Apply th_le_max_var; Auto.
Qed.

Mutual Inductive triplet: Set :=
     Eq: node2 -> int -> int -> int ->triplet .

Definition eval_triplet: (nat ->bool) -> triplet ->bool :=
   [f:nat ->bool] [t:triplet]
      Cases t of
          (Eq n v1 v2 v3) =>
            (eqb (eval_int f v1) ((f_assoc n) (eval_int f v2) (eval_int f v3)))
      end.

Definition max_var_triplet :=
   [t:triplet]
      Cases t of
          (Eq n v1 v2 v3) =>
            (max (nat_of_int v1) (max (nat_of_int v2) (nat_of_int v3)))
      end.

Mutual Inductive in_triplet: int -> triplet ->Prop :=
     in_t1: (n:node2) (i1, i2, i3:int)(in_triplet i1 (Eq n i1 i2 i3))
    | in_t2: (n:node2) (i1, i2, i3:int)(in_triplet i2 (Eq n i1 i2 i3))
    | in_t3: (n:node2) (i1, i2, i3:int)(in_triplet i3 (Eq n i1 i2 i3)) .
Hint in_t1 in_t2 in_t3.

Lemma th_max_var_triplet:
  (t:triplet) (i:int) (in_triplet i t) ->(le (nat_of_int i) (max_var_triplet t)).
Intros.
Inversion H; Simpl; Auto.
Apply le_trans with (max (nat_of_int i) (nat_of_int i3)); Auto.
Apply le_trans with (max (nat_of_int i2) (nat_of_int i)); Auto.
Qed.
Hint th_max_var_triplet.

Lemma th_eval_triplet:
  (f, g:nat ->bool) (t:triplet) (egaux_avant (max_var_triplet t) f g) ->
  (eval_triplet f t)=(eval_triplet g t).
Unfold egaux_avant; Intros f g t; Case t; Intros; Simpl; Auto.
Rewrite (th_eval_int f g i); Rewrite (th_eval_int f g i0);
 Rewrite (th_eval_int f g i1); Auto.
Qed.
Hint th_eval_triplet.

Fixpoint make_triplets_rec[e:expr2]:
   (list triplet) -> nat ->(list triplet) * (int * nat) :=
   [l:(list triplet)] [n:nat]
      Cases e of
          T2 => (l, (Un, n))
         | F2 => (l, (Moins_Un, n))
         | (V2 i) => (l, ((P i), n))
         | (N2 p) => Cases (make_triplets_rec p l n) of
                         (pair l1 (pair s1 n1)) => (l1, ((moins s1), n1))
                     end
         | (Node2 node p q) => Cases (make_triplets_rec p l n) of
                                   (pair l1 (pair s1 n1)) =>
                                     Cases (make_triplets_rec q l1 n1) of
                                         (pair l2 (pair s2 n2)) =>
                                           ((cons (Eq node (P (S n2)) s1 s2) l2),
                                            ((P (S n2)), (S n2)))
                                     end
                               end
      end.

Definition make_triplets: expr2 ->(list triplet) * (int * nat) :=
   [e:expr2](make_triplets_rec e (nil triplet) (max_var e)).

Fixpoint max_var_triplets[l:(list triplet)]: nat :=
   Cases l of
       nil => O
      | (cons t q) => (max (max_var_triplet t) (max_var_triplets q))
   end.

Mutual Inductive realise_triplets: (nat ->bool) -> (list triplet) ->Prop :=
     realise_nil: (f:nat ->bool)(realise_triplets f (nil triplet))
    | realise_cons:
        (f:nat ->bool)
        (t:triplet)
        (l:(list triplet)) (realise_triplets f l) -> (eval_triplet f t)=true ->
        (realise_triplets f (cons t l)) .
Hint realise_nil realise_cons.

Lemma realise_triplets_in_triplet:
  (f:nat ->bool) (l:(list triplet))
  (iff (realise_triplets f l) (t:triplet) (In t l) ->(eval_triplet f t)=true).
Split; Elim l; Auto.
Intros.
Absurd (In t (nil triplet)); Auto.
Intros.
Inversion H1; Inversion H0; Auto; Rewrite <- H2; Auto.
Qed.

Lemma realise_crois:
  (f:nat ->bool)
  (l1, l2:(list triplet)) (realise_triplets f l1) -> (incl l2 l1) ->
  (realise_triplets f l2).
Unfold incl.
Intros.
Case (realise_triplets_in_triplet f l1); Intros Lemme11 Lemme12.
Case (realise_triplets_in_triplet f l2); Intros Lemme21 Lemme22.
Apply Lemme22.
Intros t Ht.
Apply Lemme11; Auto.
Qed.

Lemma max_var_triplets_crois:
  (l:(list triplet)) (t:triplet)
  (le (max_var_triplets l) (max_var_triplets (cons t l))).
Intros.
Unfold max_var_triplets.
Case l; Auto.
Qed.

Lemma max_var_triplets_crois2:
  (l:(list triplet)) (t:triplet)
  (le (max_var_triplet t) (max_var_triplets (cons t l))).
Intros.
Unfold max_var_triplets.
Case l; Auto.
Qed.

Lemma support_triplets:
  (f, g:nat ->bool)
  (l:(list triplet))
  (realise_triplets f l) -> (egaux_avant (max_var_triplets l) f g) ->
  (realise_triplets g l).
Induction l; Auto.
Intros; Apply realise_cons; Auto.
Apply H; Inversion H0; Auto.
Apply (egaux_avant_crois
         (max_var_triplets l0) (max_var_triplets (cons a l0)) f g); Auto.
Apply max_var_triplets_crois.
Inversion H0; Auto.
Rewrite <- (th_eval_triplet f g a); Auto.
Apply (egaux_avant_crois (max_var_triplet a) (max_var_triplets (cons a l0)) f g);
 Auto.
Apply max_var_triplets_crois2.
Qed.
Hint support_triplets.

Lemma th_max_1:
  (l:(list triplet))
  (t:triplet)
  (n:nat) (le (max_var_triplets l) n) -> (le (max_var_triplet t) n) ->
  (le (max_var_triplets (cons t l)) n).
Intros.
Cut (max (max_var_triplet t) (max_var_triplets l))=(max_var_triplets (cons t l)).
Intros; Rewrite <- H1; Auto.
Apply (max_case_Prop (max_var_triplet t) (max_var_triplets l) [m:nat](le m n));
 Auto.
Auto.
Qed.
Hint th_max_1.

Lemma th_max_2:
  (node:node2)
  (i1, i2, i3:int)
  (n:nat)
  (le (nat_of_int i1) n) -> (le (nat_of_int i2) n) -> (le (nat_of_int i3) n) ->
  (le (max_var_triplet (Eq node i1 i2 i3)) n).
Intros.
Unfold max_var_triplet.
Apply (max_case_Prop
         (nat_of_int i1) (max (nat_of_int i2) (nat_of_int i3)) [m:nat](le m n));
 Auto.
Apply (max_case_Prop (nat_of_int i2) (nat_of_int i3) [m:nat](le m n)); Auto.
Qed.
Hint th_max_2.

Lemma th_le_max_int_n:
  (e:expr2)
  (l, l1:(list triplet))
  (n, n1:nat)
  (s1:int) (le (max_var e) n) -> (make_triplets_rec e l n)=(l1, (s1, n1)) ->
  (le (nat_of_int s1) n1).
Induction e; Simpl; Auto.
Intros; Inversion H0; Simpl; Auto.
Intros; Inversion H0; Simpl; Auto.
Intros; Inversion H0; Simpl; Rewrite <- H4; Auto.
Intros e1 H1 l l2 n n2 s2 H.
Generalize (refl_equal (list triplet) * (int * nat) (make_triplets_rec e1 l n)).
Pattern 2 3 (make_triplets_rec e1 l n).
Case (make_triplets_rec e1 l n); Intros l1 p1.
Case p1; Intros s1 n1.
Intros Eg1 N; Inversion N; Auto.
Rewrite nat_of_int_moins.
Rewrite <- H4; Apply (H1 l l1 n n1 s1); Auto.
Intros node e1 H1 e2 H2 l l3 n n3 s3 H.
Case (make_triplets_rec e1 l n); Intros l1 p1.
Case p1; Intros s1 n1.
Case (make_triplets_rec e2 l1 n1); Intros l2 p2.
Case p2; Intros s2 n2.
Intros N; Inversion N; Auto.
Qed.
Hint th_le_max_int_n.

Lemma make_crois:
  (e:expr2)
  (l, l':(list triplet))
  (n, n':nat) (s':int) (make_triplets_rec e l n)=(l', (s', n')) ->(le n n').
Induction e;
 [Intros l l' n n' s'; Simpl; Intros N; Inversion N |
   Intros l l' n n' s'; Simpl; Intros N; Inversion N |
   Intros n0 l l' n n' s'; Simpl; Intros N; Inversion N |
   Intros e1 H1 l l' n n' s'; Simpl;
    Generalize (refl_equal
                  (list triplet) * (int * nat) (make_triplets_rec e1 l n));
    Pattern 2 3 (make_triplets_rec e1 l n); Case (make_triplets_rec e1 l n);
    Intros l1 p1; Case p1; Intros s1 n1; Intros Eg1 N; Inversion N |
   Intros node e1 H1 e2 H2 l l' n n' s'; Simpl;
    Generalize (refl_equal
                  (list triplet) * (int * nat) (make_triplets_rec e1 l n));
    Pattern 2 3 (make_triplets_rec e1 l n); Case (make_triplets_rec e1 l n);
    Intros l1 p1; Case p1; Intros s1 n1; Intros Eg1;
    Generalize (refl_equal
                  (list triplet) * (int * nat) (make_triplets_rec e2 l1 n1));
    Pattern 2 3 (make_triplets_rec e2 l1 n1); Case (make_triplets_rec e2 l1 n1);
    Intros l2 p2; Case p2; Intros s2 n2; Intros Eg2 N; Inversion N]; Auto.
Rewrite <- H3; Auto.
Apply (H1 l l1 n n1 s1); Auto.
Apply le_trans with n2; Auto.
Apply le_trans with n1; Auto.
Apply (H1 l l1 n n1 s1); Auto.
Apply (H2 l1 l2 n1 n2 s2); Auto.
Qed.
Hint make_crois.

Lemma make_crois2:
  (e:expr2)
  (l, l1:(list triplet))
  (n, n1:nat) (s1:int) (make_triplets_rec e l n)=(l1, (s1, n1)) ->(incl l l1).
Induction e;
 [Intros l l' n n' s'; Simpl; Intros N; Inversion N |
   Intros l l' n n' s'; Simpl; Intros N; Inversion N |
   Intros n0 l l' n n' s'; Simpl; Intros N; Inversion N |
   Intros e1 H1 l l' n n' s'; Simpl;
    Generalize (refl_equal
                  (list triplet) * (int * nat) (make_triplets_rec e1 l n));
    Pattern 2 3 (make_triplets_rec e1 l n); Case (make_triplets_rec e1 l n);
    Intros l1 p1; Case p1; Intros s1 n1; Intros Eg1 N; Inversion N |
   Intros node e1 H1 e2 H2 l l' n n' s'; Simpl;
    Generalize (refl_equal
                  (list triplet) * (int * nat) (make_triplets_rec e1 l n));
    Pattern 2 3 (make_triplets_rec e1 l n); Case (make_triplets_rec e1 l n);
    Intros l1 p1; Case p1; Intros s1 n1; Intros Eg1;
    Generalize (refl_equal
                  (list triplet) * (int * nat) (make_triplets_rec e2 l1 n1));
    Pattern 2 3 (make_triplets_rec e2 l1 n1); Case (make_triplets_rec e2 l1 n1);
    Intros l2 p2; Case p2; Intros s2 n2; Intros Eg2 N; Inversion N]; Auto.
Rewrite <- H0; Auto.
Apply (H1 l l1 n n1 s1); Auto.
Apply incl_tl; Auto.
Apply incl_tran with l1; Auto.
Apply (H1 l l1 n n1 s1); Auto.
Apply (H2 l1 l2 n1 n2 s2); Auto.
Qed.
Hint make_crois2.

Lemma max_var_e1:
  (n:node2) (e1, e2:expr2)(le (max_var e1) (max_var (Node2 n e1 e2))).
Intros.
Cut (max_var (Node2 n e1 e2))=(max (max_var e1) (max_var e2)); Auto.
Intros A; Rewrite A; Auto.
Qed.

Lemma max_var_e2:
  (n:node2) (e1, e2:expr2)(le (max_var e2) (max_var (Node2 n e1 e2))).
Intros.
Cut (max_var (Node2 n e1 e2))=(max (max_var e1) (max_var e2)); Auto.
Intros A; Rewrite A; Auto.
Qed.
Hint max_var_e1 max_var_e2.

Lemma max_var_triplets_le:
  (e:expr2)
  (l, l':(list triplet))
  (n, n':nat)
  (s':int)
  (le (max_var e) n) ->
  (le (max_var_triplets l) n) -> (make_triplets_rec e l n)=(l', (s', n')) ->
  (le (max_var_triplets l') n').
Induction e;
 [Intros l l' n n' s' Hyp0 Hyp1; Simpl; Intros N; Inversion N |
   Intros l l' n n' s' Hyp0 Hyp1; Simpl; Intros N; Inversion N |
   Intros n0 l l' n n' s' Hyp0 Hyp1; Simpl; Intros N; Inversion N |
   Intros e1 H1 l l' n n' s' Hyp0 Hyp1; Simpl;
    Generalize (refl_equal
                  (list triplet) * (int * nat) (make_triplets_rec e1 l n));
    Pattern 2 3 (make_triplets_rec e1 l n); Case (make_triplets_rec e1 l n);
    Intros l1 p1; Case p1; Intros s1 n1; Intros Eg1 N; Inversion N |
   Intros node e1 H1 e2 H2 l l' n n' s' Hyp0 Hyp1; Simpl;
    Generalize (refl_equal
                  (list triplet) * (int * nat) (make_triplets_rec e1 l n));
    Pattern 2 3 (make_triplets_rec e1 l n); Case (make_triplets_rec e1 l n);
    Intros l1 p1; Case p1; Intros s1 n1; Intros Eg1;
    Generalize (refl_equal
                  (list triplet) * (int * nat) (make_triplets_rec e2 l1 n1));
    Pattern 2 3 (make_triplets_rec e2 l1 n1); Case (make_triplets_rec e2 l1 n1);
    Intros l2 p2; Case p2; Intros s2 n2; Intros Eg2 N; Inversion N]; Auto.
Rewrite <- H2; Rewrite <- H0; Auto.
Rewrite <- H2; Rewrite <- H0; Auto.
Rewrite <- H2; Rewrite <- H0; Auto.
Rewrite <- H3; Rewrite <- H0; Auto.
Apply (H1 l l1 n n1 s1); Auto.
Apply th_max_1.
Apply le_trans with n2; Auto.
Apply (H2 l1 l2 n1 n2 s2); Auto.
Apply le_trans with (max_var (Node2 node e1 e2)); Auto.
Apply le_trans with n; Auto.
Apply (make_crois e1 l l1 n n1 s1); Auto.
Apply (H1 l l1 n n1 s1); Auto.
Apply le_trans with (max_var (Node2 node e1 e2)); Auto.
Apply th_max_2; Auto.
Apply le_trans with n1; Auto.
Apply (th_le_max_int_n e1 l l1 n n1 s1); Auto.
Apply le_trans with (max_var (Node2 node e1 e2)); Auto.
Apply le_trans with n2; Auto.
Apply (make_crois e2 l1 l2 n1 n2 s2); Auto.
Apply le_trans with n2; Auto.
Apply (th_le_max_int_n e2 l1 l2 n1 n2 s2); Auto.
Apply le_trans with (max_var (Node2 node e1 e2)); Auto.
Apply le_trans with n; Auto.
Apply (make_crois e1 l l1 n n1 s1); Auto.
Qed.

Definition solution :=
   [n:nat] [g:nat ->bool] [s:bool] [m:nat]
      Cases (le_lt_dec m n) of
          left => (g m)
         | right => s
      end.

Lemma egaux_avant_sol:
  (g:nat ->bool) (n:nat) (s:bool)(egaux_avant n g (solution n g s)).
Intros.
Unfold egaux_avant; Intros k Hk.
Intros; Unfold solution.
Case (le_lt_dec k n); Auto.
Intros HA.
Absurd (lt n k); Auto.
Qed.
Hint egaux_avant_sol.

14/09/98, 09:21