seq.v

(****************************************************************************                                                                                       Buchberger : Equality over polynomials                                                                                                                  Laurent Thery February 97 (revised Mai 98)                                                                                                    ****************************************************************************)
Require Export Relation_Definitions.
Require Import Arith.
Require Import Compare_dec.

(* definition of eqP and properties *)
Section Seq.
Load "shyp_porder".
Load "mod_porder".

(* New Constructions *)

Definition size := (!length Term).

Definition sizel :=
   [m:(list Term) * (list Term)]
      Cases m of
          (pair l1 l2) => (plus (size l1) (size l2))
      end.

Definition lessP :=
   [m1, m2:(list Term) * (list Term)](lt (sizel m1) (sizel m2)).
Hints Unfold lessP.

Lemma wf_lessP: (well_founded (list Term) * (list Term) lessP).
Red.
Cut (n:nat) (a:(list Term) * (list Term)) (lt (sizel a) n) ->
    (Acc (list Term) * (list Term) lessP a).
Intros H' a.
Apply H' with n := (S (sizel a)); Auto.
Intros n; Elim n; Clear n.
Intros a H; Inversion H.
Intros n H' a H'0; Try Assumption.
Apply Acc_intro.
Intros y H'1; Try Assumption.
Apply H'.
Unfold lessP in H'1.
Apply lt_le_trans with (sizel a); Auto with arith.
Qed.
Hints Resolve wf_lessP.

Theorem pX_inj:
  (n1, n2:Term) (l1, l2:(list Term)) n1=n2 -> l1=l2 ->(pX n1 l1)=(pX n2 l2).
Intros n1 n2 l1 l2 H' H'0; Try Assumption.
Rewrite H'0; Rewrite H'; Auto.
Qed.
Hints Resolve pX_inj.

Lemma pX_invl: (a, b:Term) (p, q:(list Term)) (pX a p)=(pX b q) ->a=b.
Intros a b p q H'; Inversion H'; Auto.
Qed.
Hints Unfold pX.

Lemma pX_invr: (p, q:(list Term)) (a, b:Term) (pX a p)=(pX b q) ->p=q.
Unfold pX pX.
Intros p q a b H'; Inversion H'; Auto.
Qed.

Theorem canonicalpO: (canonical pO).
Apply (canonicalDef ? ltM ? T2M zeroP zeroP_dec); Simpl; Auto.
Unfold olist ltB; Simpl; Auto.
Apply d_nil; Auto.
Qed.

Theorem canonical1: (a:Term) ~ (zeroP a) ->(canonical (pX a pO)).
Intros a H; Apply (canonicalDef ? ltM ? T2M zeroP zeroP_dec); Simpl; Auto.
Unfold olist ltB; Simpl; Auto.
Apply d_one.
Case (zeroP_dec a); Auto.
Qed.
Hints Resolve canonical1 canonical0.

Mutual Inductive eqP: (list Term) -> (list Term) ->Prop :=
     eqP0: (eqP pO pO)
    | eqpP1:
        (ma, mb:Term) (p, q:(list Term)) (eqTerm ma mb) -> (eqP p q) ->
        (eqP (pX ma p) (pX mb q)) .
Hints Resolve eqP0 eqpP1.

Theorem eqp_refl: (reflexive (list Term) eqP).
Red.
Intros x; Elim x; Auto.
Qed.

Theorem eqp_sym: (symmetric (list Term) eqP).
Red.
Intros x y H'; Elim H'; Auto.
Qed.

Lemma eqp_inv1: (p:(list Term)) (eqP pO p) ->p=pO.
Intros p H'; Inversion H'; Auto.
Qed.

Theorem eqp_inv2: (p:(list Term)) (eqP p pO) ->p=pO.
Intros p H'; Inversion H'; Auto.
Qed.

Theorem eqp_inv3l:
  (a, b:Term) (p, q:(list Term)) (eqP (pX a p) (pX b q)) ->(eqTerm a b).
Intros a b p q H'; Simple Inversion H'; Auto.
Inversion H0.
Rewrite (pX_invl ma a p0 p); Auto; Rewrite (pX_invl mb b q0 q); Auto.
Qed.

Theorem eqp_inv3r:
  (a, b:Term) (p, q:(list Term)) (eqP (pX a p) (pX b q)) ->(eqP p q).
Intros a b p q H'; Simple Inversion H'; Auto.
Inversion H0.
Rewrite (pX_invr p0 p ma a); Auto; Rewrite (pX_invr q0 q mb b); Auto.
Qed.

Theorem eqp_trans: (transitive (list Term) eqP).
Red.
Intros x; Elim x; Auto.
Intros y z H'; Inversion H'.
Intros H'0; Inversion H'0; Auto.
Intros a l H' y z H'0; Inversion H'0; Simpl.
Simpl in H0; Simpl in H.
Intros H'1; Inversion H'1; Simpl; Auto.
Simpl in H5; Simpl in H4.
Apply eqpP1.
Apply eqTerm_trans with y := ma0; Auto.
Rewrite H4; Auto.
Rewrite H0.
Apply H' with y := p0; Auto.
Rewrite H5.
Rewrite <- H0; Auto.
Qed.
Hints Resolve eqp_refl.

Theorem eqTerm_imp_eqM: (a, b:Term) (eqTerm a b) ->(eqM a b).
Exact eqTerm_imp_eq.
Qed.
Hints Resolve eqTerm_imp_eqM.

Theorem ltP_refl_pX:
  (a:Term) (p:(list Term)) (canonical (pX a p)) ->(ltP p (pX a p)).
Intros a p; Case p; Auto.
Intros a0 l H'; Try Assumption.
Apply ltP_trans with y := (pX a pO); Auto.
Qed.

Theorem eqp_eqTerm:
  (a, b:Term) (p, q:(list Term)) (eqP (pX a p) (pX b q)) ->(eqTerm a b).
Intros a b p q H'; Inversion H'.
Simpl in H3; Simpl in H1; Simpl in H0; Simpl in H.
Rewrite <- H; Rewrite <- H1; Auto.
Qed.

Theorem ltp_eqp_comp:
  (p, q, r, s:(list Term))
  (ltP p q) -> (canonical p) -> (canonical q) -> (eqP p r) -> (eqP q s) ->
  (ltP r s).
Intros p q r s H'; Generalize r s; Elim H'; Clear r s H'; Auto.
Intros x p0 r s H'0 H'1 H'2 H'3; Inversion H'2; Inversion H'3; Auto.
Intros x y p0 q0 r s H'0 H'1 H'2 H'3 H'4; Inversion H'3; Auto.
Simpl in H0; Simpl in H.
Rewrite H in H1; Clear H2 H0 H H'3 ma.
Inversion H'4; Auto.
Simpl in H0; Simpl in H.
Rewrite H in H2; Clear H4 H0 H H'4 ma.
Apply ltP_hd; Auto.
Apply order_eqM_l with a := y; Auto.
Apply order_eqM_r with a := x; Auto.
Intros x y p0 q0 H' H'0 H'1 r s H'2 H'3 H'4 H'5.
Inversion H'4; Auto.
Simpl in H0; Simpl in H.
Rewrite H in H1; Rewrite H0 in H3; Clear H2 H0 H H'4 ma.
Inversion H'5; Auto.
Simpl in H0; Simpl in H.
Rewrite H in H2; Rewrite H0 in H5; Clear H4 H0 H H'5 ma.
Apply ltP_tl; Auto.
Apply eqM_trans with y := x; Auto.
Apply eqM_trans with y := y; Auto.
Apply H'1; Auto.
Apply canonical_imp_canonical with a := x; Auto.
Apply canonical_imp_canonical with a := y; Auto.
Qed.

Theorem nzeroP_comp_eqTerm:
  (a, b:Term) ~ (zeroP a) -> (eqTerm a b) ->~ (zeroP b).
Intros a b H' H'0; Red; Intros H'1.
Apply H'.
Apply zeroP_comp_eqTerm with a := b; Auto.
Qed.

Theorem eqp_imp_canonical:
  (p, q:(list Term)) (eqP p q) -> (canonical p) ->(canonical q).
Intros p q H'; Elim H'; Auto.
Intros ma mb p0 q0 H'0 H'1 H'2 H'3; Try Assumption.
Apply canonical_pX_eqM with a := ma; Auto.
Apply ltP_pX_canonical; Auto.
Apply H'2.
Apply canonical_imp_canonical with a := ma; Auto.
Red; Intros H'4.
LApply (canonical_nzeroP ma p0);
[Intros H'8; Apply H'8 Orelse Elim H'8 | Idtac]; Auto.
Apply ltp_eqp_comp with p := p0 q := (pX ma pO); Auto.
Apply canonical_imp_canonical with a := ma; Auto.
Apply canonical1; Auto.
Apply canonical_nzeroP with p := p0; Auto.
Apply nzeroP_comp_eqTerm with a := ma; Auto.
Apply canonical_nzeroP with p := p0; Auto.
Qed.

Definition sizel3 :=
   [m:(list Term) * ((list Term) * (list Term))]
      Cases m of
          (pair l1 (pair l2 l3)) => (plus (size l1) (plus (size l2) (size l3)))
      end.

Definition lessP3 :=
   [m1, m2:(list Term) * ((list Term) * (list Term))]
   (lt (sizel3 m1) (sizel3 m2)).

Lemma wf_lessP3:
  (well_founded (list Term) * ((list Term) * (list Term)) lessP3).
Red.
Cut (n:nat) (a:(list Term) * ((list Term) * (list Term))) (lt (sizel3 a) n) ->
    (Acc (list Term) * ((list Term) * (list Term)) lessP3 a).
Intros H' a.
Apply H' with n := (S (sizel3 a)); Auto.
Intros n; Elim n; Clear n.
Intros a H; Inversion H.
Intros n H' a H'0; Apply Acc_intro.
Intros y H'1; Apply H'.
Unfold lessP in H'1; Apply lt_le_trans with (sizel3 a); Auto with arith.
Qed.
Hints Resolve wf_lessP3.

Definition eqPf:
  (pq:(list Term) * (list Term))
  {(eqP (Fst pq) (Snd pq))}+{~ (eqP (Fst pq) (Snd pq))}.
Intros pq; Pattern pq;
Apply well_founded_induction
      with A := (list Term) * (list Term) R := lessP 1 := wf_lessP; Clear pq.
Intros pq; Case pq; Simpl; Clear pq.
Intros p; Case p; Clear p.
Intros q; Case q; Clear q.
Intros H'; Left; Auto.
Intros b q H'; Right; Red; Intros H'0; Inversion H'0.
Intros a p q; Case q; Clear q.
Intros H'; Right; Red; Intros H'0; Inversion H'0.
Intros b q Rec; Case (eqTerm_dec a b); Simpl in Rec; Intros eqTerm0.
Case (Rec (p, q)); Unfold lessP; Simpl; Auto with arith.
Intros H'; Right; Red; Intros H'0.
Apply H'.
Apply eqp_inv3r with a := a b := b; Auto.
Right; Red; Intros H'.
Apply eqTerm0.
Apply eqp_eqTerm with p := p q := q; Auto.
Defined.
(* Theorem on polynomials  and equality *)

Definition seqP: poly -> poly ->Prop.
Intros sp1 sp2; Case sp1; Case sp2.
Intros p1 H'1 p2 H'2; Exact (eqP p1 p2).
Defined.

Theorem seqp_dec: (p, q:poly){(seqP p q)}+{~ (seqP p q)}.
Intros p q; Case p; Case q; Simpl.
Intros x H' x0 H'0.
Apply (eqPf (x, x0)).
Qed.

Theorem seqp_refl: (reflexive poly seqP).
Red.
Intros p; Case p; Simpl.
Intros x H'.
Apply eqp_refl.
Qed.

Theorem seqp_sym: (symmetric poly seqP).
Red.
Intros p q; Case p; Case q; Simpl.
Intros x H' x0 H'0 H'1.
Apply eqp_sym; Auto.
Qed.

Theorem seqp_trans: (transitive poly seqP).
Red.
Intros p q r; Case p; Case q; Case r; Simpl.
Intros x H' x0 H'0 x1 H'1 H'2 H'3.
Apply eqp_trans with y := x0; Auto.
Qed.
End Seq.

18/01/99, 19:17