porder.v

(****************************************************************************                                                                                       Buchberger : Canonical polynomial                                                                                                                       Laurent Thery February 97 (revised Mai 98)                                                                                                    ****************************************************************************)
Section Porder.
Require Import Lexicographic_Exponentiation.
Require Import Relation_Definitions.
Require Import Inverse_Image.
Require Import Inclusion.
Require Import PolyList.
Require Import Relation_Operators.

(* A is a set with a well founded operation  *)
Variable A:Set.
Variable ltA:A -> A ->Prop.
Hypothesis ltA_trans:(transitive A ltA).
Hypothesis eqA_dec:(x, y:A){x=y}+{~ x=y}.
Hypothesis ltA_dec:(x, y:A){(ltA x y)}+{(ltA y x)}+{x=y}.
Hypothesis ltA_nonrefl:(x:A)~ (ltA x x).
Hypothesis wf_ltA:(well_founded A ltA).
Hints Resolve ltA_nonrefl.

(* B is another set *)
Variable B:Set.

(* f is a function from B to A *)
Variable f:B ->A.

(* We define ltB and eqB by projection on A *)

Definition ltB: B -> B ->Prop := [a, b:B](ltA (f a) (f b)).
Hints Unfold ltB.

Theorem ltB_trans: (transitive B ltB).
Unfold transitive ltB; Auto.
Intros x y z H' H'0; Apply ltA_trans with y := (f y); Auto.
Qed.

Definition eqB: B -> B ->Prop := [a, b:B](f a)=(f b).
Hints Unfold ltB eqB.
(* eqB have the expected properties *)

Lemma eqB_refl: (reflexive B eqB).
Red; Auto.
Qed.

Lemma eqB_sym: (symmetric B eqB).
Red; Auto.
Qed.

Lemma eqB_trans: (transitive B eqB).
Red; Unfold eqB.
Intros x y z H' H'0; Rewrite H'; Auto.
Qed.

Lemma eqB_compat_ltBr: (a, b, c:B) (eqB b c) -> (ltB a b) ->(ltB a c).
Unfold eqB; Unfold ltB; Intros a b c H; Rewrite H; Auto.
Qed.

Lemma eqB_compat_ltBl: (a, b, c:B) (eqB b c) -> (ltB b a) ->(ltB c a).
Unfold eqB; Unfold ltB; Intros a b c H; Rewrite H; Auto.
Qed.

Theorem eqB_dec: (x, y:B){(eqB x y)}+{~ (eqB x y)}.
Intros x y; Unfold eqB; Simpl; Auto.
Qed.

Theorem ltB_dec: (x, y:B){(ltB x y)}+{(ltB y x)}+{(eqB x y)}.
Intros x y; Exact (ltA_dec (f x) (f y)).
Qed.

Lemma ltB_not_eqB: (m, n:B) (eqB m n) ->~ (ltB m n).
Unfold eqB ltB; Simpl; Intros m n H; Rewrite H; Auto.
Qed.

Lemma eqB_not_ltB: (m, n:B) (ltB m n) ->~ (eqB m n).
Unfold eqB ltB not; Simpl; Intros m n H Q; Absurd (ltA (f m) (f n)); Auto;
Rewrite Q; Auto.
Qed.

Theorem ltB_not_refl: (x:B)~ (ltB x x).
Unfold ltB; Auto.
Qed.
Hints Resolve ltB_not_eqB eqB_not_ltB ltB_not_refl.

Lemma ltB_not_ltB: (m, n:B) (ltB m n) ->~ (ltB n m).
Intros m n H'; Red; Intros H'0; Absurd (ltB m m); Auto.
Apply ltB_trans with y := n; Auto.
Qed.
Hints Resolve ltB_not_ltB.

Lemma ltB_eqB: (a, b, c, d:B) (eqB a b) -> (eqB c d) -> (ltB a c) ->(ltB b d).
Unfold eqB ltB; Intros a b c d R1 R2; Rewrite R1; Rewrite R2; Auto.
Qed.

Lemma ltB_eqBr: (a, b, c:B) (eqB a b) -> (ltB a c) ->(ltB b c).
Intros a b c H' H'0; Apply ltB_eqB with a := a c := c; Auto.
Qed.

Lemma ltB_eqBl: (a, b, c:B) (eqB a b) -> (ltB c a) ->(ltB c b).
Intros a b c H' H'0; Apply ltB_eqB with a := c c := a; Auto.
Qed.

Local pX := (!cons B).

Local pO := (!nil B).

Local consA := (!cons A).

Local nilA := (!nil A).

Local listA := (list A).
Hints Unfold consA nilA listA.
(* We extend f on the list of B *)

Fixpoint fP[a:(list B)]: listA :=
   (<listA>Case a of nilA [b:B] [p:(list B)](consA (f b) (fP p)) end).

Theorem fP_app: (p, q:(list B))(fP (app p q))=(app (fP p) (fP q)).
Intros p; Elim p; Simpl; Auto.
Intros a l H' q; Try Assumption.
Rewrite (H' q); Auto.
Qed.

Local DescA := (Desc A ltA).

Definition olist := [p:(list B)](DescA (fP p)).
Hints Resolve d_nil d_one.
Hints Unfold olist DescA.
(* Trivial properties of olist*)

Theorem olist0: (a, b:B) (ltB b a) ->(olist (pX a (pX b pO))).
Unfold olist ltB; Simpl; Auto.
Intros a b H'; Try Assumption.
Generalize (d_conc A ltA (f b) (f a) nilA); Simpl; Auto.
Qed.
Hints Resolve olist0.

Lemma app2_inv:
  (x, y, z, t:A)
  (p:listA)
  (app (app p (consA x nilA)) (consA y nilA))=(consA z (consA t (nil A))) ->
  x=z /\ y=t.
Intros x y z t p; Case p; Simpl; Auto.
Intros H'; Injection H'; Simpl; Auto.
Intros a l; Case l; Simpl; Auto.
Intros H'; Discriminate H'.
Intros a0 l0; Case l0; Simpl; Auto.
Intros H'; Discriminate H'.
Intros a1 l1 H'; Discriminate H'.
Qed.

Theorem olist_ltB:
  (l:(list B)) (a, b:B) (olist (app l (pX a (pX b pO)))) ->(ltB b a).
Unfold ltB olist; Simpl; Auto.
Intros l a b; Try Assumption.
Rewrite (fP_app l (pX a (pX b pO))); Simpl; Auto.
Intros H'; Try Assumption.
Elim (dist_Desc_concat A ltA (fP l) (consA (f a) (consA (f b) nilA)));
[Intros H'5 H'6; Try Exact H'6 | Idtac]; Auto.
Simple Inversion H'6.
Discriminate H.
Discriminate H.
Elim (app2_inv y x (f a) (f b) l0); [Intros H'8 H'9; Try Exact H'9 | Idtac];
Auto.
Rewrite H'9; Rewrite H'8; Auto.
Qed.

Theorem olist_cons:
  (l:(list B)) (a, b:B) (ltB b a) -> (olist (pX b l)) ->(olist (pX a (pX b l))).
Intros l; Pattern l; Apply (!rev_ind B); Auto.
Intros x l0; Case l0.
Simpl.
Unfold olist; Simpl.
Intros H' a b H'0 H'1; Try Assumption.
Apply (d_conc A ltA (f x) (f b) (consA (f a) nilA)).
Generalize (olist_ltB pO); Unfold ltB olist; Simpl; Auto.
Apply (olist0 a b); Auto.
Intros b l1 H' a b0 H'0; Generalize H'; Pattern l1; Apply (!rev_ind B);
Unfold ltB olist; Simpl; Auto.
Intros H'2 H'3.
Apply (d_conc A ltA (f x) (f b) (consA (f a) (consA (f b0) nilA))); Auto.
Generalize (olist_ltB (cons b0 (nil B))); Unfold ltB olist; Simpl; Auto.
Simpl; Apply H'2; Auto.
Apply (desc_prefix A ltA (consA (f b0) (consA (f b) nilA)) (f x)); Auto.
Intros x1 l2; Rewrite (fP_app (app l2 (cons x1 (nil B))) (cons x (nil B)));
Rewrite (fP_app l2 (cons x1 (nil B))); Rewrite (fP_app l2 (cons x (nil B))).
Intros H'2 H'3 H'4;
Apply (d_conc
          A ltA (f x) (f x1) (consA (f a) (consA (f b0) (consA (f b) (fP l2))))).
Generalize (olist_ltB (pX b0 (pX b l2))); Unfold olist ltB; Intros H'5;
Apply H'5.
Rewrite (fP_app (pX b0 (pX b l2)) (pX x1 (pX x pO))); Simpl; Auto.
Generalize (app_ass (fP l2) (consA (f x1) nilA) (consA (f x) nilA)); Simpl;
Auto; Unfold consA.
Intros H'6; Rewrite <- H'6; Simpl; Auto.
Simpl; Apply H'3; Auto; Apply (desc_prefix A ltA) with a := (f x); Auto.
Qed.

Lemma fp_tail:
  (x:B) (p:(list B))
  (fP (app p (cons x (nil B))))=(app (fP p) (cons (f x) (nil A))).
Intros x p; Elim p; Simpl; Auto.
Intros a l H'; Try Assumption.
Rewrite H'; Auto.
Qed.

Lemma descA_subst: (a, b:listA) b=a -> (DescA a) ->(DescA b).
Intros a b H'; Rewrite H'; Auto.
Qed.

Theorem olist_pX_eqC:
  (a, b:B) (p:(list B)) (olist (pX a p)) -> (eqB a b) ->(olist (pX b p)).
Unfold olist eqB.
Simpl; Auto.
Intros a b p H' H'0; Rewrite <- H'0; Auto.
Qed.

Theorem olist_pX_order:
  (l:(list B)) (a, b:B) (olist (pX a (pX b l))) ->(ltB b a).
Intros l a b H'; Try Assumption.
Elim (dist_Desc_concat A ltA (consA (f a) (consA (f b) nilA)) (fP l));
[Intros H'5 H'6; Try Exact H'5 | Idtac]; Auto.
Apply olist_ltB with l := pO; Auto.
Qed.

Theorem olist_X: (l:(list B)) (a:B) (olist (pX a l)) ->(olist l).
Intros l a H'; Try Assumption.
Elim (dist_Desc_concat A ltA (consA (f a) nilA) (fP l));
[Intros H'5 H'6; Try Exact H'5 | Idtac]; Auto.
Qed.

Theorem olist_imp_olist:
  (l:(list B)) (a, b:B) (olist (pX a (pX b l))) ->(olist (pX a l)).
Intros l; Case l.
Intros a b H'; Try Assumption.
Elim (dist_Desc_concat A ltA (consA (f a) nilA) (consA (f b) nilA));
[Intros H'5 H'6; Try Exact H'5 | Idtac]; Auto.
Intros b l0 a b0 H'; Try Assumption.
Apply olist_cons; Auto.
Apply ltB_trans with y := b0.
Apply olist_pX_order with l := l0; Auto.
Apply olist_X with a := a; Auto.
Apply olist_pX_order with l := (cons b l0); Auto.
Apply olist_X with a := b0; Auto.
Apply olist_X with a := a; Auto.
Qed.
(* Definition of a lexicographic order on (list B) *)

Mutual Inductive ltP: (list B) -> (list B) ->Prop :=
     ltPO: (x:B) (p:(list B))(ltP pO (pX x p))
    | ltP_hd: (x, y:B) (p, q:(list B)) (ltB x y) ->(ltP (pX x p) (pX y q))
    | ltP_tl:
        (x, y:B) (p, q:(list B)) (eqB x y) -> (ltP p q) ->
        (ltP (pX x p) (pX y q)) .

Lemma fltP: (p, q:(list B)) (ltP p q) ->(Ltl A ltA (fP p) (fP q)).
Intros p q H'; Elim H'; Auto.
Simpl; Intros; Apply (Lt_nil A); Auto.
Simpl; Intros; Apply (Lt_hd A); Auto.
Simpl; Unfold eqB; (Intros x y p1 q1 H; Rewrite H).
Simpl; Intros; Apply (Lt_tl A); Auto.
Qed.
Hints Resolve fltP.

Theorem ltp_not_refl: (x:(list B))~ (ltP x x).
Intros x; Elim x.
Red; Intros H'; Inversion H'.
Intros a l H'; Red; Intros H'0; Simple Inversion H'0.
Discriminate H.
Injection H1.
Injection H0.
Intros H'1 H'2 H'3 H'4; Rewrite H'2; Rewrite H'4; Intros H'5.
Apply (ltB_not_refl a); Auto.
Injection H1; Injection H2.
Intros H'1 H'2 H'3 H'4; Rewrite H'1; Rewrite H'3; Auto.
Qed.
Hints Resolve ltPO.

Theorem ltP_trans: (x, y, z:(list B)) (ltP x y) -> (ltP y z) ->(ltP x z).
Intros x y z H'; Generalize z; Clear z; Elim H'.
Intros x0 p z; Case z; Auto.
Intros H'0; Inversion H'0.
Intros x0 y0 p q H'0 z H'1; Simple Inversion H'1.
Discriminate H.
Rewrite <- H1.
Intros H'2; Try Assumption.
Apply ltP_hd; Auto.
Apply ltB_trans with y := y0; Auto.
Injection H0.
Intros H'3 H'4; Rewrite <- H'4; Auto.
Rewrite <- H2.
Intros H'2 H'3; Apply ltP_hd; Auto.
Apply ltB_eqBl with a := x1; Auto.
Injection H1.
Intros H'4 H'5; Rewrite H'5; Auto.
Intros x0 y0 p q H'0 H'1 H'2 z H'3; Simple Inversion H'3.
Discriminate H.
Rewrite <- H1; Auto.
Intros H'4; Apply ltP_hd; Auto.
Apply ltB_eqBr with a := y0.
Apply eqB_sym; Auto.
Injection H0.
Intros H'5 H'6; Rewrite <- H'6; Auto.
Rewrite <- H2.
Intros H'4 H'5; Apply ltP_tl; Auto.
Apply eqB_trans with y := x1; Auto.
Injection H1.
Intros H'6 H'7; Rewrite H'7; Auto.
Apply H'2; Auto.
Injection H1.
Intros H'6; Rewrite <- H'6; Auto.
Qed.

Theorem olist_pX_ltP: (a:B) (p:(list B)) (olist (pX a p)) ->(ltP p (pX a pO)).
Intros a p; Case p; Auto.
Intros b l H'; Try Assumption.
Apply ltP_hd; Auto.
Apply olist_pX_order with l := l; Auto.
Qed.

Theorem ltP_pX_olist:
  (a:B) (p:(list B)) (olist p) -> (ltP p (pX a pO)) ->(olist (pX a p)).
Intros a p; Case p; Auto.
Intros H' H'1; Unfold olist DescA consA; Simpl; Unfold consA nilA.
Apply d_one; Auto.
Intros b l H' H'0; Try Assumption.
Apply olist_cons; Auto.
Simple Inversion H'0.
Discriminate H.
Injection H1; Injection H0; Intros H'1 H'2 H'3 H'4; (Rewrite H'2; Rewrite H'4);
Auto.
Injection H2; Intros H'1 H'2; Rewrite H'1; Auto.
Intros H'3 H'4; Inversion H'4.
Qed.
Variable zeroP:B ->Prop.
Variable zeroP_dec:(a:B){(zeroP a)}+{~ (zeroP a)}.

Definition nZterm: (list B) ->Prop.
Intros H'; Elim H'.
Exact True.
Intros a P1 Rec.
Case (zeroP_dec a).
Intros H'0; Exact False.
Intros H'0; Exact Rec.
Defined.

Mutual Inductive canonical: (list B) ->Prop :=
     canonicalDef: (a:(list B)) (olist a) -> (nZterm a) ->(canonical a) .

Theorem canonical_imp_olist: (a:(list B)) (canonical a) ->(olist a).
Intros a H'; Elim H'; Auto.
Qed.
Hints Resolve canonical_imp_olist.

Theorem canonical0:
  (a, b:B) (ltB b a) -> ~ (zeroP a) -> ~ (zeroP b) ->
  (canonical (pX a (pX b pO))).
Intros a b H' H'0 H'1; Simpl; Auto.
Apply canonicalDef; Simpl; Auto.
Case (zeroP_dec a); Simpl; Auto.
Case (zeroP_dec b); Simpl; Auto.
Qed.

Theorem canonical_ltB:
  (l:(list B)) (a, b:B) (canonical (app l (pX a (pX b pO)))) ->(ltB b a).
Intros l a b H'; Auto.
Apply olist_ltB with l := l; Auto.
Qed.

Theorem canonical_nzeroP: (a:B) (p:(list B)) (canonical (pX a p)) ->~ (zeroP a).
Intros a p H'; Red; Intros H'0; Inversion H'.
Generalize H0; Simpl; Case (zeroP_dec a); Auto.
Qed.

Theorem canonical_cons:
  (l:(list B)) (a, b:B) (ltB b a) -> ~ (zeroP a) -> (canonical (pX b l)) ->
  (canonical (pX a (pX b l))).
Intros l a b H' H'0 H'1; Apply canonicalDef; Simpl; Auto.
Apply olist_cons; Auto.
Case (zeroP_dec a); Simpl; Auto.
Case (zeroP_dec b); Simpl; Auto.
Intros H'2 H'3.
LApply (canonical_nzeroP b l); [Intros H'6; Apply H'6 Orelse Elim H'6 | Idtac];
Auto.
Inversion H'1.
Generalize H0; Simpl; Case (zeroP_dec b); Auto.
Intros H'2 H'3; Elim H'3.
Qed.

Theorem canonical_pX_eqC:
  (a, b:B) (p:(list B)) (canonical (pX a p)) -> (eqB a b) -> ~ (zeroP b) ->
  (canonical (pX b p)).
Intros a b p H' H'0 H'1.
Apply canonicalDef; Auto.
Apply olist_pX_eqC with a := a; Auto.
Inversion H'.
Generalize H0; Simpl; Case (zeroP_dec a); Case (zeroP_dec b); Simpl; Auto.
Intros H'2 H'3 H'4; Elim H'4.
Qed.

Theorem canonical_pX_order:
  (l:(list B)) (a, b:B) (canonical (pX a (pX b l))) ->(ltB b a).
Intros l a b H'; Auto.
Apply olist_pX_order with l := l; Auto.
Qed.

Theorem canonical_imp_canonical:
  (l:(list B)) (a:B) (canonical (pX a l)) ->(canonical l).
Intros l a H'.
Apply canonicalDef; Auto.
Apply olist_X with a := a; Auto.
Inversion H'.
Generalize H0; Simpl; Case (zeroP_dec a); Auto.
Intros H'0 H'1; Elim H'1.
Qed.

Theorem ocanonical_skip_fst:
  (l:(list B)) (a, b:B) (canonical (pX a (pX b l))) ->(canonical (pX a l)).
Intros l a b H'; Apply canonicalDef; Auto.
Apply olist_imp_olist with b := b; Auto.
Inversion H'.
Generalize H0; Simpl; Case (zeroP_dec a); Case (zeroP_dec b); Auto.
Intros H'0 H'1 H'2; Elim H'2.
Qed.

Theorem ocanonical_pX_ltP:
  (a:B) (p:(list B)) (canonical (pX a p)) ->(ltP p (pX a pO)).
Intros a p H'; Auto.
Apply olist_pX_ltP; Auto.
Qed.

Theorem ltP_pX_canonical:
  (a:B) (p:(list B)) (canonical p) -> ~ (zeroP a) -> (ltP p (pX a pO)) ->
  (canonical (pX a p)).
Intros a p H' H'0 H'1; Apply canonicalDef; Auto.
Apply ltP_pX_olist; Auto.
Inversion H'.
Generalize H0 H'0; Simpl; Case (zeroP_dec a); Auto.
Qed.

Local poly := {a:(list B) | (canonical a)}.

(* Ltp on the ordered polynome *)

Definition sltP: poly -> poly ->Prop :=
   [sa, sb:poly]
   (<Prop>Case sa of
     [p:(list B)] [H1:(canonical p)]
     (<Prop>Case sb of [q:(list B)] [H2:(canonical q)](ltP p q) end) end).

Definition fspoly: poly ->(Pow A ltA) :=
   [sa:poly]
   (<(Pow A ltA)>Case sa of
     [p:(list B)] [H:(canonical p)]
     (exist listA DescA (fP p) (canonical_imp_olist p H)) end).

Theorem fsltP: (p, q:poly) (sltP p q) ->(lex_exp A ltA (fspoly p) (fspoly q)).
Intros p q; Case p; Case q; Unfold lex_exp; Simpl; Auto.
Qed.
Hints Resolve fsltP.
(* Main theorem the order on the spoly is well_founded *)

Theorem sltp_wf: (well_founded poly sltP).
LApply (wf_inverse_image poly (Pow A ltA) (lex_exp A ltA) fspoly);
[Intros H'3; Try Exact H'3 | Idtac].
Apply wf_incl with R2 := [x, y:poly](lex_exp A ltA (fspoly x) (fspoly y)); Auto.
Red; Auto.
Apply (wf_lex_exp A ltA); Auto; Exact wf_ltA.
Qed.
End Porder.

18/01/99, 18:41