# Library Buchberger.POrder

Require Import Lexicographic_Exponentiation.
Require Import Relation_Definitions.
Require Import Inverse_Image.
Require Import Inclusion.
Require Import List.
Require Import Relation_Operators.
Require Import Monomials.
Require Import Term.
Require Import CoefStructure.
Require Import OrderStructure.
Section Porder.

Set Implicit Arguments.
Unset Strict Implicit.

Definition ltT (a b : Term A n) : Prop := ltM (T2M a) (T2M b).
Hint Unfold ltT.
Set Strict Implicit.
Unset Implicit Arguments.

Theorem ltT_trans : transitive (Term A n) ltT.
unfold transitive, ltT in |- ×; auto.
intros x y z H' H'0; apply (ltM_trans _ _ _ _ os) with (y := T2M y); auto.
Qed.

Lemma eqT_compat_ltTr :
a b c : Term A n, eqT b c -> ltT a b ltT a c.
unfold eqT in |- *; unfold ltT in |- *; intros a b c H; rewrite H; auto.
Qed.

Lemma eqT_compat_ltTl :
a b c : Term A n, eqT b c ltT b a ltT c a.
unfold eqT in |- ×; unfold ltT in |- ×; intros a b c H; rewrite H; auto.
Qed.

Theorem eqT_dec : x y : Term A n, {eqT x y} + {~ eqT x y}.
intros x y; unfold eqT in |- *; simpl in |- *; auto.
apply eqmon_dec.
Qed.

Theorem ltT_dec : x y : Term A n, {ltT x y} + {ltT y x} + {eqT x y}.
intros x y; exact (ltM_dec (T2M x) (T2M y)).
Qed.

Lemma ltT_not_eqT : x y : Term A n, eqT x y ¬ ltT x y.
unfold eqT, ltT in |- *; simpl in |- *; intros x y H; rewrite H; auto.
apply ltM_nonrefl with (1 := os).
Qed.

Lemma eqT_not_ltT : x y : Term A n, ltT x y ¬ eqT x y.
unfold eqT, ltT, not in |- *; simpl in |- *; intros x y H Q;
absurd (ltM (T2M x) (T2M y)); auto; rewrite Q; auto.
apply ltM_nonrefl with (1 := os).
Qed.

Theorem ltT_not_refl : x : Term A n, ¬ ltT x x.
intros x; unfold ltT in |- *; apply ltM_nonrefl with (1 := os).
Qed.
Hint Resolve ltT_not_eqT eqT_not_ltT ltT_not_refl.

Lemma ltT_not_ltT : x y : Term A n, ltT x y ¬ ltT y x.
intros x y H'; red in |- *; intros H'0; absurd (ltT x x); auto.
apply ltT_trans with (y := y); auto.
Qed.
Hint Resolve ltT_not_ltT.

Lemma ltT_eqT :
a b c d : Term A n, eqT a b eqT c d ltT a c ltT b d.
unfold eqT, ltT in |- *; intros a b c d R1 R2; rewrite R1; rewrite R2; auto.
Qed.

Let eqT_refl := eqT_refl A n.

Lemma ltT_eqTr : a b c : Term A n, eqT a b ltT a c ltT b c.
intros a b c H' H'0; apply ltT_eqT with (a := a) (c := c); auto.
Qed.

Lemma ltT_eqTl : a b c : Term A n, eqT a b ltT c a ltT c b.
intros a b c H' H'0; apply ltT_eqT with (a := c) (c := a); auto.
Qed.

Theorem multTerm_ltT_l :
m1 m2 m3,
ltT m1 m2 ltT (multTerm multA m3 m1) (multTerm multA m3 m2).
intros a b c; case a; case b; case c; unfold ltT in |- *; simpl in |- *; auto.
intros a0 m a1 m0 a2 m1 H.
apply ltM_plusl with (1 := os); auto.
Qed.

Theorem multTerm_ltT_r :
m1 m2 m3,
ltT m1 m2 ltT (multTerm multA m1 m3) (multTerm multA m2 m3).
intros a b c; case a; case b; case c; unfold ltT in |- *; simpl in |- *; auto.
intros; apply ltM_plusr with (1 := os); auto.
Qed.

Theorem T1_is_min_ltT : a, ¬ ltT a (T1 A1 n).
intros a; case a; unfold ltT in |- *; simpl in |- *; auto.
intros a0 m; unfold M1 in |- *; apply (M1_min _ _ _ _ os); auto.
Qed.

Theorem minusTerm_ltT_l :
a b c, eqT a b ltT a c ltT (minusTerm minusA a b) c.
intros a b c; case a; case b; case c; unfold ltT in |- *; simpl in |- *; auto.
Qed.

Theorem invTerm_ltT_l : a c, ltT a c ltT (invTerm invA a) c.
intros a b; case a; case b; unfold ltT in |- *; simpl in |- *; auto.
Qed.
Set Implicit Arguments.
Unset Strict Implicit.

Definition pX := cons (A:=Term A n).
Set Strict Implicit.
Unset Implicit Arguments.

Definition pO := nil (A:=Term A n).

Let consA := cons (A:=mon n).

Let nilA := nil (A:=mon n).

Let listA := list (mon n).
Hint Unfold consA nilA listA.

Fixpoint fP (a : list (Term A n)) : listA :=
match a with
| nilnilA
| b :: pconsA (T2M b) (fP p)
end.

Theorem fP_app : p q : list (Term A n), fP (p ++ q) = fP p ++ fP q.
intros p; elim p; simpl in |- *; auto.
intros a l H' q.
rewrite (H' q); auto.
Qed.

Let DescA := Desc (mon n) ltM.
Set Implicit Arguments.
Unset Strict Implicit.

Definition olist (p : list (Term A n)) := DescA (fP p).
Hint Resolve d_nil d_one.
Hint Unfold olist DescA.
Set Strict Implicit.
Unset Implicit Arguments.

Theorem olistOne : a b : Term A n, ltT b a olist (pX a (pX b pO)).
unfold olist, ltT in |- *; simpl in |- *; auto.
intros a b H'.
generalize (d_conc _ ltM (T2M b) (T2M a) nilA); simpl in |- *; auto.
Qed.
Hint Resolve olistOne.

Theorem olistO : olist pO.
unfold olist, ltT in |- *; simpl in |- *; auto.
red in |- *; unfold nilA in |- *; apply d_nil.
Qed.

Lemma app2_inv :
(x y z t : mon n) (p : listA),
(p ++ consA x nilA) ++ consA y nilA = consA z (consA t nilA)
x = z y = t.
intros x y z t p; case p; simpl in |- *; auto.
intros H'; injection H'; simpl in |- *; auto.
intros a l; case l; simpl in |- *; auto.
intros H'; discriminate H'.
intros a0 l0; case l0; simpl in |- *; auto.
intros H'; discriminate H'.
intros a1 l1 H'; discriminate H'.
Qed.

Theorem olist_ltT :
(l : list (Term A n)) (a b : Term A n),
olist (l ++ pX a (pX b pO)) ltT b a.
unfold ltT, olist in |- *; simpl in |- *; auto.
intros l a b.
rewrite (fP_app l (pX a (pX b pO))); simpl in |- *; auto.
intros H'.
elim (dist_Desc_concat _ ltM (fP l) (consA (T2M a) (consA (T2M 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 (T2M a) (T2M b) l0); [ intros H'8 H'9 | idtac ]; auto.
rewrite H'9; rewrite H'8; auto.
Qed.

Theorem olist_cons :
(l : list _) a b, ltT b a olist (pX b l) olist (pX a (pX b l)).
intros l; pattern l in |- *; apply (rev_ind (A:=Term A n)); auto.
intros x l0; case l0.
simpl in |- ×.
unfold olist in |- *; simpl in |- ×.
intros H' a b H'0 H'1; try assumption.
apply (d_conc _ ltM (T2M x) (T2M b) (consA (T2M a) nilA)).
generalize (olist_ltT pO); unfold ltT, olist in |- *; simpl in |- *; auto.
apply (olistOne a b); auto.
intros b l1 H' a b0 H'0; generalize H'; pattern l1 in |- *;
apply (rev_ind (A:=Term A n)); unfold ltT, olist in |- *;
simpl in |- *; auto.
intros H'2 H'3.
apply (d_conc _ ltM (T2M x) (T2M b) (consA (T2M a) (consA (T2M b0) nilA)));
auto.
generalize (olist_ltT (b0 :: nil)); unfold ltT, olist in |- *; simpl in |- *;
auto.
simpl in |- *; apply H'2; auto.
apply (desc_prefix _ ltM (consA (T2M b0) (consA (T2M b) nilA)) (T2M x)); auto.
intros x1 l2; rewrite (fP_app (l2 ++ x1 :: nil) (x :: nil));
rewrite (fP_app l2 (x1 :: nil)); rewrite (fP_app l2 (x :: nil)).
intros H'2 H'3 H'4;
apply
(d_conc _ ltM (T2M x) (T2M x1)
(consA (T2M a) (consA (T2M b0) (consA (T2M b) (fP l2))))).
generalize (olist_ltT (pX b0 (pX b l2))); unfold olist, ltT in |- *;
intros H'5; apply H'5.
rewrite (fP_app (pX b0 (pX b l2)) (pX x1 (pX x pO))); simpl in |- *; auto.
generalize (app_ass (fP l2) (consA (T2M x1) nilA) (consA (T2M x) nilA));
simpl in |- *; auto; unfold consA in |- ×.
intros H'6; rewrite <- H'6; simpl in |- *; auto.
simpl in |- *; apply H'3; auto; apply (desc_prefix _ ltM) with (a := T2M x);
auto.
Qed.

Lemma fp_tail : x p, fP (p ++ x :: nil) = fP p ++ T2M x :: nil.
intros x p; elim p; simpl in |- *; auto.
intros a l H'; 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_eqT :
a b p, olist (pX a p) eqT a b olist (pX b p).
unfold olist, eqT in |- ×.
simpl in |- *; auto.
intros a b p H' H'0; rewrite <- H'0; auto.
Qed.

Theorem olist_pX_order : l a b, olist (pX a (pX b l)) ltT b a.
intros l a b H'.
elim (dist_Desc_concat _ ltM (consA (T2M a) (consA (T2M b) nilA)) (fP l));
[ intros H'5 H'6 | idtac ]; auto.
apply olist_ltT with (l := pO); auto.
Qed.

Theorem olist_X : (l : list _) a, olist (pX a l) olist l.
intros l a H'.
elim (dist_Desc_concat _ ltM (consA (T2M a) nilA) (fP l));
[ intros H'5 H'6 | idtac ]; auto.
Qed.

Theorem olist_imp_olist :
l a b, olist (pX a (pX b l)) olist (pX a l).
intros l; case l.
intros a b H'.
elim (dist_Desc_concat _ ltM (consA (T2M a) nilA) (consA (T2M b) nilA));
[ intros H'5 H'6 | idtac ]; auto.
intros b l0 a b0 H'.
apply olist_cons; auto.
apply ltT_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 := b :: l0); auto.
apply olist_X with (a := b0); auto.
apply olist_X with (a := a); auto.
Qed.
Set Implicit Arguments.
Unset Strict Implicit.

Inductive ltP : list (Term A n) list (Term A n) Prop :=
| ltPO : x p, ltP pO (pX x p)
| ltP_hd : x y p q, ltT x y ltP (pX x p) (pX y q)
| ltP_tl : x y p q, eqT x y ltP p q ltP (pX x p) (pX y q).
Set Strict Implicit.
Unset Implicit Arguments.

Lemma fltP : p q, ltP p q Ltl _ ltM (fP p) (fP q).
intros p q H'; elim H'; auto.
simpl in |- *; intros; apply (Lt_nil (mon n)); auto.
simpl in |- *; intros; apply (Lt_hd (mon n)); auto.
simpl in |- *; unfold eqT in |- *; (intros x y p1 q1 H; rewrite H).
simpl in |- *; intros; apply (Lt_tl (mon n)); auto.
Qed.
Hint Resolve fltP.

Theorem ltp_not_refl : x, ¬ ltP x x.
intros x; elim x.
red in |- *; intros H'; inversion H'.
intros a l H'; red in |- *; 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 (ltT_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.
Hint Resolve ltPO.

Theorem ltP_trans : x y z, 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 ltT_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 ltT_eqTl 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 ltT_eqTr with (a := y0).
apply (eqT_sym A n); auto.
injection H0.
intros H'5 H'6; rewrite <- H'6; auto.
rewrite <- H2.
intros H'4 H'5; apply ltP_tl; auto.
apply (eqT_trans A n) 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 p, olist (pX a p) ltP p (pX a pO).
intros a p; case p; auto.
intros b l H'.
apply ltP_hd; auto.
apply olist_pX_order with (l := l); auto.
Qed.

Theorem ltP_pX_olist :
a p, 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 in |- *; simpl in |- *;
unfold consA, nilA in |- ×.
apply d_one; auto.
intros b l H' H'0.
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.
unfold pO in |- *; intros H'3 H'4; inversion H'4.
Qed.

Theorem ltP_order_comp :
(a b c : Term A n) (p q : list (Term A n)),
ltP (pX b p) (pX a q) ltT a c ltT b c.
intros a b c p q H1; inversion_clear H1.
intros; apply ltT_trans with (y := a); auto.
apply eqT_compat_ltTl.
apply eqT_sym; trivial.
Qed.
Hint Resolve ltP_order_comp.

Set Implicit Arguments.
Unset Strict Implicit.

Definition nZterm : list (Term A n) Prop.
intros H'; elim H'.
exact True.
intros a P1 Rec.
exact (Rec ¬ zeroP (A:=A) A0 eqA (n:=n) a).
Defined.

Definition canonical (a : list (Term A n)) : Prop := olist a nZterm a.
Set Strict Implicit.
Unset Implicit Arguments.

Theorem canonical_imp_olist : a, canonical a olist a.
intros a H'; elim H'; auto.
Qed.
Hint Resolve canonical_imp_olist.

Theorem canonical0 :
a b,
ltT b a
¬ zeroP (A:=A) A0 eqA (n:=n) a
¬ zeroP (A:=A) A0 eqA (n:=n) b canonical (pX a (pX b pO)).
intros a b H' H'0 H'1; simpl in |- *; auto.
split; simpl in |- *; auto.
Qed.

Theorem canonical_ltT :
l a b, canonical (l ++ pX a (pX b pO)) ltT b a.
intros l a b H'; auto.
apply olist_ltT with (l := l); auto.
Qed.

Theorem canonical_nzeroP :
a p, canonical (pX a p) ¬ zeroP (A:=A) A0 eqA (n:=n) a.
intros a p H'; red in |- *; intros H'0; inversion H'.
generalize H0; simpl in |- *; intuition; auto.
Qed.

Theorem canonical_cons :
l a b,
ltT b a
¬ zeroP (A:=A) A0 eqA (n:=n) a
canonical (pX b l) canonical (pX a (pX b l)).
intros l a b H' H'0 H'1; split; simpl in |- *; auto.
apply olist_cons; auto.
repeat split; auto.
inversion H'1; simpl in H0; intuition.
apply canonical_nzeroP with (p := l); auto.
Qed.

Theorem canonical_pX_eqT :
a b p,
canonical (pX a p)
eqT a b ¬ zeroP (A:=A) A0 eqA (n:=n) b canonical (pX b p).
intros a b p H' H'0 H'1.
split; auto.
apply olist_pX_eqT with (a := a); auto.
simpl in |- *; split; auto.
case H'; simpl in |- *; intuition.
Qed.

Theorem canonical_pX_order :
l a b, canonical (pX a (pX b l)) ltT b a.
intros l a b H'; auto.
apply olist_pX_order with (l := l); auto.
Qed.

Theorem canonical_imp_canonical :
l a, canonical (pX a l) canonical l.
intros l a H'.
split; auto.
apply olist_X with (a := a); auto.
elim H'; simpl in |- *; intuition.
Qed.

Theorem canonical_skip_fst :
l a b, canonical (pX a (pX b l)) canonical (pX a l).
intros l a b H'; split; auto.
apply olist_imp_olist with (b := b); auto.
inversion H'.
generalize H0; simpl in |- *; intuition.
Qed.

Theorem canonical_pX_ltP : a p, 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 p,
canonical p
¬ zeroP (A:=A) A0 eqA (n:=n) a ltP p (pX a pO) canonical (pX a p).
intros a p H' H'0 H'1; split; auto.
apply ltP_pX_olist; auto.
inversion H'.
generalize H0 H'0; simpl in |- *; case (zeroP_dec A A0 eqA eqA_dec n a); auto.
Qed.

Theorem not_double_canonical :
(a : Term A n) (p : list (Term A n)), ¬ canonical (pX a (pX a p)).
intros a p; red in |- *; intros H'; try exact H'.
absurd (ltT a a); auto.
apply canonical_pX_order with (l := p); auto.
Qed.

Theorem canonical_imp_in_nzero :
p : list (Term A n),
canonical p a : Term A n, In a p ¬ zeroP (A:=A) A0 eqA (n:=n) a.
intros p; elim p; auto.
intros a l H' H'0 a0 H'1; elim H'1; auto.
intros H'2; rewrite <- H'2.
apply canonical_nzeroP with (p := l); auto.
intros H'2; auto.
apply H'; auto.
apply canonical_imp_canonical with (a := a); auto.
Qed.

Set Implicit Arguments.
Unset Strict Implicit.

Definition poly := {a : list _ | canonical a}.

Definition sltP (sa sb : poly) : Prop :=
let (p, H1) return Prop := sa in let (q, H2) return Prop := sb in ltP p q.

Definition fspoly (sa : poly) : Pow _ ltM :=
let (p, H) return (Pow _ ltM) := sa in
exist DescA (fP p) (canonical_imp_olist p H).
Set Strict Implicit.
Unset Implicit Arguments.

Theorem fsltP :
p q : poly, sltP p q lex_exp _ ltM (fspoly p) (fspoly q).
intros p q; case p; case q; unfold lex_exp in |- *; simpl in |- *; auto.
Qed.
Hint Resolve fsltP.

Theorem sltp_wf : well_founded sltP.
lapply (wf_inverse_image poly (Pow _ ltM) (lex_exp _ ltM) fspoly);
[ intros H'3 | idtac ].
apply
wf_incl with (R2 := fun x y : polylex_exp _ ltM (fspoly x) (fspoly y));
auto.
red in |- *; auto.
apply (wf_lex_exp _ ltM); auto; apply ltM_wf with (1 := os).
Qed.
End Porder.