splus.v
(****************************************************************************
Buchberger : addition over polynomials
Laurent Thery February 97 (revised Mai 98)
***************************************************************************
definition of plusP *)
Section SPlus.
Load "shyp_splus".
Load "mod_seq".
Require Import Arith.
Require Import Compare_dec.
Theorem
plusTerm_eqM1: (m1, m2:Term) (eqM m1 m2) ->(eqM (plusTerm m1 m2) m1).
Exact plusTerm_eq1.
Qed.
Hints Resolve plusTerm_eqM1.
Theorem
plusTerm_eqM2: (m1, m2:Term) (eqM m1 m2) ->(eqM (plusTerm m1 m2) m2).
Exact plusTerm_eq2.
Qed.
Hints Resolve plusTerm_eqM2.
Mutual Inductive
plusP: (list Term) -> (list Term) -> (list Term) ->Prop :=
nillu1: (l1:(list Term))(plusP pO l1 l1)
| nillu2: (l1:(list Term))(plusP l1 pO l1)
| mainu1:
(a1, a2:Term)
(l1, l2, l3:(list Term)) (order a2 a1) -> (plusP l1 (pX a2 l2) l3) ->
(plusP (pX a1 l1) (pX a2 l2) (pX a1 l3))
| mainu2a:
(a1, a2:Term)
(l1, l2, l3:(list Term))
(plusP l1 l2 l3) -> (eqM a1 a2) -> (zeroP (plusTerm a1 a2)) ->
(plusP (pX a1 l1) (pX a2 l2) l3)
| mainu2b:
(a1, a2:Term)
(l1, l2, l3:(list Term))
(plusP l1 l2 l3) -> (eqM a1 a2) -> ~ (zeroP (plusTerm a1 a2)) ->
(plusP (pX a1 l1) (pX a2 l2) (pX (plusTerm a1 a2) l3))
| mainu3:
(a1, a2:Term)
(l1, l2, l3:(list Term)) (order a1 a2) -> (plusP (pX a1 l1) l2 l3) ->
(plusP (pX a1 l1) (pX a2 l2) (pX a2 l3)) .
Hints Resolve nillu1 nillu2 mainu1 mainu2a mainu2b mainu3.
Definition
projsig1 :=
[A:Set] [P:A ->Prop] [H:(sig A P)](<A>Case H of [a:?] [_:?]a end).
Require Import LetP.
Definition
plusp:
(l:(list Term) * (list Term)){a:(list Term) | (plusP (Fst l) (Snd l) a)}.
Idtac.
Intros l; Pattern l.
Apply well_founded_induction with A := (list Term) * (list Term) R := lessP;
Auto.
Intros x; Case x; Intros p q; Simpl.
Case p; Clear p.
Intros H'; Exists q; Auto.
Intros a1 m1; Case q; Clear q.
Intros H'; Exists (pX a1 m1); Auto.
Intros a2 m2 H'; Case (order_dec a1 a2); [Intros P; Case P; Clear P | Idtac];
Intros H1.
LApply (H' ((pX a1 m1), m2)); Simpl;
[Intros Rec; Case Rec; Clear Rec; Intros Orec Prec | Idtac].
Exists (pX a2 Orec); Auto.
Red; Red; Simpl; Auto with arith.
LApply (H' (m1, (pX a2 m2))); Simpl;
[Intros Rec; Case Rec; Clear Rec; Intros Orec Prec | Idtac].
Exists (pX a1 Orec); Auto.
Red; Red; Simpl; Auto.
Apply LetP with A := Term h := (plusTerm a1 a2).
Intros letA eqL0; Case (zeroP_dec letA); Intros H'0.
LApply (H' (m1, m2)); Simpl;
[Intros Rec; Case Rec; Clear Rec; Intros Orec Prec | Idtac].
Exists Orec; Auto.
Rewrite eqL0 in H'0; Auto.
Red; Red; Simpl; Auto with arith.
LApply (H' (m1, m2)); Simpl;
[Intros Rec; Case Rec; Clear Rec; Intros Orec Prec | Idtac].
Exists (pX letA Orec); Auto.
Rewrite eqL0; Auto.
Rewrite eqL0 in H'0; Auto.
Red; Red; Simpl; Auto with arith.
Defined.
Definition
pluspf :=
[l1, l2:(list Term)](projsig1 (list Term) ? (plusp (l1, l2))).
Hints Unfold projsig1 pluspf.
Lemma
plusP_inv:
(p, q, l:(list Term)) (a, b:Term) (plusP (pX a p) (pX b q) l) ->
(Ex [l1:(list Term)]
(order b a) /\ ((plusP p (pX b q) l1) /\ l=(pX a l1)) \/
((order a b) /\ ((plusP (pX a p) q l1) /\ l=(pX b l1)) \/
(eqM a b) /\
((zeroP (plusTerm a b)) /\ (plusP p q l) \/
~ (zeroP (plusTerm a b)) /\ ((plusP p q l1) /\ l=(pX (plusTerm a b) l1))))).
Intros p q l a b H'; Simple Inversion H'.
Discriminate H.
Discriminate H0.
Rewrite <- H3; Rewrite (pX_invl a2 b l2 q H2); Rewrite (pX_invr l2 q a2 b H2);
Rewrite (pX_invl a1 a l1 p H1); Rewrite (pX_invr l1 p a1 a H1).
Intros H'0 H'1; Exists l3; Left; Split;
[Idtac | Split; [Try Assumption | Idtac]]; Auto.
Rewrite <- H3.
Intros H'0 H'1 H'2; Exists l3; Right; Right.
Rewrite <- (pX_invl a2 b l2 q H3); Rewrite <- (pX_invl a1 a l1 p H2); Auto.
Rewrite <- (pX_invr l2 q a2 b H3); Rewrite <- (pX_invr l1 p a1 a H2); Auto.
Rewrite <- H4; Auto.
Intros H'0 H'1 H'2; Exists l3; Right; Right.
Rewrite <- (pX_invl a2 b l2 q H3); Rewrite <- (pX_invl a1 a l1 p H2); Auto.
Rewrite <- (pX_invr l2 q a2 b H3); Rewrite <- (pX_invr l1 p a1 a H2); Auto.
Intros H'0 H'1; Exists l3; Right; Left; Split;
[Idtac | Split; [Try Assumption | Idtac]]; Auto.
Rewrite <- (pX_invl a2 b l2 q H2); Rewrite <- (pX_invl a1 a l1 p H1); Auto.
Rewrite <- (pX_invl a1 a l1 p H1); Rewrite <- (pX_invr l2 q a2 b H2);
Rewrite <- (pX_invr l1 p a1 a H1); Auto.
Rewrite <- H3; Rewrite <- (pX_invl a2 b l2 q H2); Auto.
Qed.
Theorem
uniq_plusp:
(l:(list Term) * (list Term))
(l3, l4:(list Term))
(plusP (Fst l) (Snd l) l3) -> (plusP (Fst l) (Snd l) l4) ->l3=l4.
Unfold pX pX.
Intros l; Pattern l.
Apply well_founded_ind
with A := (list Term) * (list Term) R := lessP 1 := wf_lessP.
Intros x; Case x; Clear x.
Intros l1 l2; Case l1; Clear l1.
Intros H' l3 l4 H'0 H'2; Inversion H'2; Inversion H'0; Auto.
Case l2; Clear l2.
Simpl; Intros n0 l0 H' l3 l4 H'0 H'2.
Inversion H'2; Inversion H'0; Auto.
Simpl; Intros n2 l2 n1 l1 Induc l3 l4 Hl3 Hl4.
Case (plusP_inv l1 l2 l4 n1 n2); Auto.
Intros x H'; Elim H';
[Intros H'0; Elim H'0; Intros H'1 H'2; Elim H'2; Intros H'3 H'4; Rewrite H'4;
Clear H'2 H'0 H' | Intros H'0; Clear H'].
Case (plusP_inv l1 l2 l3 n1 n2); Auto.
Intros x0 H'; Elim H';
[Intros H'0; Elim H'0; Intros H'2 H'5; Elim H'5; Intros H'6 H'7; Rewrite H'7;
Clear H'5 H'0 H' | Intros H'0; Clear H']; Auto.
Apply pX_inj; Auto.
Apply Induc with y := (l1, (cons n2 l2)); Simpl; Auto.
Red; Red; Simpl; Auto.
Elim H'0;
[Intros H'; Elim H'; Intros H'2 H'5; Try Exact H'2; Clear H' H'0 |
Intros H'; Clear H'0].
Absurd (order n1 n2); Auto.
Elim H'; Intros H'0 H'2; Try Exact H'0; Clear H'.
Absurd (eqM n2 n1); Auto.
Apply eqM_sym; Auto.
Elim H'0;
[Intros H'; Elim H'; Intros H'1 H'2; Elim H'2; Intros H'3 H'4; Rewrite H'4;
Clear H'2 H' H'0 | Intros H'; Clear H'0].
Case (plusP_inv l1 l2 l3 n1 n2); Auto.
Intros x0 H'; Elim H';
[Intros H'0; Elim H'0; Intros H'2 H'5; Clear H'0 H' | Intros H'0; Clear H'].
Absurd (order n1 n2); Auto.
Elim H'0;
[Intros H'; Elim H'; Intros H'2 H'5; Elim H'5; Intros H'6 H'7; Rewrite H'7;
Clear H'5 H' H'0 | Intros H'; Clear H'0].
Apply pX_inj; Auto.
Apply Induc with y := ((pX n1 l1), l2); Simpl; Auto.
Red; Red; Simpl; Auto with arith.
Elim H'; Intros H'0 H'2; Try Exact H'0; Clear H'.
Absurd (eqM n1 n2); Auto.
Elim H'; Intros H'0 H'1; Try Exact H'0; Clear H'.
Case (plusP_inv l1 l2 l3 n1 n2); Auto.
Intros x0 H'; Elim H';
[Intros H'2; Elim H'2; Intros H'3 H'4; Try Exact H'3; Clear H'2 H' |
Intros H'2; Clear H'].
Absurd (eqM n2 n1); Auto.
Apply eqM_sym; Auto.
Elim H'2;
[Intros H'; Elim H'; Intros H'3 H'4; Try Exact H'3; Clear H' H'2 |
Intros H'; Clear H'2].
Absurd (eqM n1 n2); Auto.
Elim H'; Intros H'2 H'3; Elim H'3;
[Intros H'4; Elim H'4; Intros H'5 H'6; Try Exact H'5; Clear H'4 H'3 H' |
Intros H'4; Clear H'3 H'].
Elim H'1;
[Intros H'; Clear H'1 |
Intros H'; Elim H'; Intros H'3 H'4; Apply H'3 Orelse Elim H'3; Clear H' H'1];
Auto.
Elim H'; Intros H'1 H'3; Clear H'.
Apply Induc with y := (l1, l2); Auto; Red; Simpl; Auto.
Red; Red; Simpl; Auto with arith.
Elim H'4; Intros H' H'3; Elim H'3; Intros H'5 H'6; Rewrite H'6; Clear H'3 H'4.
Elim H'1;
[Intros H'3; Clear H'1 |
Intros H'3; Elim H'3; Intros H'4 H'7; Elim H'7; Intros H'8 H'9; Rewrite H'9;
Clear H'7 H'3 H'1].
Elim H'3; Intros H'1 H'4; Try Exact H'1; Clear H'3.
Apply H' Orelse Elim H'; Try Assumption.
Apply pX_inj; Auto.
Apply Induc with y := (l1, l2); Auto.
Red; Red; Simpl; Auto with arith.
Qed.
Theorem
pluspf_is_plusP: (l1, l2:(list Term))(plusP l1 l2 (pluspf l1 l2)).
Intros l1 l2; Try Assumption.
Unfold pluspf; Case (plusp <(list Term), (list Term)> (l1, l2)); Simpl; Auto.
Qed.
Hints Resolve pluspf_is_plusP.
Theorem
order_plusP:
(l1, l2, l3:(list Term))
(a:Term)
(plusP l1 l2 l3) ->
(canonical (pX a l1)) -> (canonical (pX a l2)) -> (canonical l3) ->
(canonical (pX a l3)).
Intros l1 l2 l3 a H'; Generalize a; Elim H'; Auto.
Intros a1 a2 l4 l5 l6 H'0 H'1 H'2 a0 H'3 H'4 H'5.
Apply canonical_cons; Auto.
Apply canonical_imp_order with l := l4; Auto.
Apply canonical_nzeroP with p := (pX a1 l4); Auto.
Intros a1 a2 l4 l5 l6 H'0 H'1 H'2 H'3 a0 H'4 H'5 H'6.
Apply H'1; Auto.
Apply canonical_skip_fst with b := a1; Auto.
Apply canonical_skip_fst with b := a2; Auto.
Intros a1 a2 l4 l5 l6 H'0 H'1 H'2 H'3 a0 H'4 H'5 H'6.
Apply canonical_cons; Auto.
Apply order_eqM_r with a := a1; Auto.
Apply eqM_sym; Auto.
Apply canonical_imp_order with l := l4; Auto.
Apply canonical_nzeroP with p := (pX a1 l4); Auto.
Intros a1 a2 l4 l5 l6 H'0 H'1 H'2 a0 H'3 H'4 H'5.
Apply canonical_cons; Auto.
Apply canonical_imp_order with l := l5; Auto.
Apply canonical_nzeroP with p := (pX a1 l4); Auto.
Qed.
Theorem
canonical_plusP:
(l1, l2, l3:(list Term))
(plusP l1 l2 l3) -> (canonical l1) -> (canonical l2) ->(canonical l3).
Intros l1 l2 l3 H'; Elim H'; Auto.
Intros a1 a2 l4 l5 l6 H'0 H'1 H'2 H'3 H'4; Try Assumption.
Apply order_plusP with l1 := l4 l2 := (pX a2 l5); Auto.
Apply canonical_cons; Auto.
Apply canonical_nzeroP with p := l4; Auto.
Apply H'2; Auto.
Apply canonical_imp_canonical with a := a1; Auto.
Intros a1 a2 l4 l5 l6 H'0 H'1 H'2 H'3 H'4 H'5.
Apply H'1; Auto.
Apply canonical_imp_canonical with a := a1; Auto.
Apply canonical_imp_canonical with a := a2; Auto.
Intros a1 a2 l4 l5 l6 H'0 H'1 H'2 H'3 H'4 H'5.
Apply order_plusP with l1 := l4 l2 := l5; Auto.
Apply canonical_pX_eqM with a := a1; Auto.
Apply eqM_sym; Auto.
Apply canonical_pX_eqM with a := a2; Auto; Auto.
Apply eqM_sym; Red; Apply plusTerm_eqM2; Auto.
Apply H'1.
Apply canonical_imp_canonical with a := a1; Auto.
Apply canonical_imp_canonical with a := a2; Auto.
Intros a1 a2 l4 l5 l6 H'0 H'1 H'2 H'3 H'4.
Apply order_plusP with l1 := (pX a1 l4) l2 := l5; Auto.
Apply canonical_cons; Auto.
Apply canonical_nzeroP with p := l5; Auto.
Apply H'2; Auto.
Apply canonical_imp_canonical with a := a2; Auto.
Qed.
Theorem
canonical_pluslmf:
(l1, l2:(list Term)) (canonical l1) -> (canonical l2) ->
(canonical (pluspf l1 l2)).
Intros l1 l2 H' H'0; Generalize (pluspf_is_plusP l1 l2); Intros u1.
Apply canonical_plusP with l1 := l1 l2 := l2; Auto.
Qed.
Theorem
pO_plusP_inv1: (p, q:(list Term)) (plusP pO p q) ->p=q.
Intros p; Elim p.
Intros q H'; Inversion H'; Auto.
Intros a l H' q H'0; Inversion H'0; Auto.
Qed.
Theorem
pO_plusP_inv2: (p, q:(list Term)) (plusP p pO q) ->p=q.
Intros p; Elim p.
Intros q H'; Inversion H'; Auto.
Intros a l H' q H'0; Inversion H'0; Auto.
Qed.
Hints Resolve eqp_refl.
Theorem
plusP_decomp:
(a:Term) (p:(list Term)) (canonical (pX a p)) ->(plusP (pX a pO) p (pX a p)).
Intros a p; Case p; Auto.
Intros m l H'; Try Assumption.
Apply mainu1; Auto.
Apply canonical_imp_order with l := l; Auto.
Qed.
Theorem
plusP_inv1:
(a, b:Term)
(p, q, s:(list Term)) (plusP (pX a p) (pX b q) s) -> (order b a) ->
s=(pX a (pluspf p (pX b q))).
Intros a b p q s H'; Simple Inversion H'.
Inversion H.
Inversion H0.
Rewrite <- H3; Rewrite <- (pX_invl a1 a l1 p);
Try Rewrite <- (pX_invl a2 b l2 q); Auto.
Rewrite <- (pX_invr l2 q a2 b); Try Rewrite <- (pX_invr l1 p a1 a); Auto.
Intros H'0 H'1 H'2; Apply pX_inj; Auto.
Apply uniq_plusp with l := (l1, (pX a2 l2)); Simpl; Auto.
Rewrite <- (pX_invl a1 a l1 p); Try Rewrite <- (pX_invl a2 b l2 q); Auto.
Intros H'0 H'1 H'2 H'3; Absurd (order a2 a1); Auto.
Apply order_not_eqM; Auto; Apply eqM_sym; Auto.
Rewrite <- (pX_invl a1 a l1 p); Try Rewrite <- (pX_invl a2 b l2 q); Auto.
Intros H'0 H'1 H'2 H'3; Absurd (order a2 a1); Auto.
Apply order_not_eqM; Auto; Apply eqM_sym; Auto.
Intros H'0 H'1 H'2; Absurd (order a2 a1); Auto.
Rewrite (pX_invl a1 a l1 p); Try Rewrite (pX_invl a2 b l2 q); Auto.
Qed.
Theorem
plusP_inv2:
(a, b:Term)
(p, q, s:(list Term)) (plusP (pX a p) (pX b q) s) -> (order a b) ->
s=(pX b (pluspf (pX a p) q)).
Intros a b p q s H'; Simple Inversion H'.
Inversion H.
Inversion H0.
Rewrite <- (pX_invl a1 a l1 p); Try Rewrite <- (pX_invl a2 b l2 q); Auto.
Intros H'0 H'1 H'2; Absurd (order a2 a1); Auto.
Rewrite <- (pX_invl a1 a l1 p); Try Rewrite <- (pX_invl a2 b l2 q); Auto.
Intros H'0 H'1 H'2 H'3; Absurd (order a1 a2); Auto.
Rewrite <- (pX_invl a1 a l1 p); Try Rewrite <- (pX_invl a2 b l2 q); Auto.
Intros H'0 H'1 H'2 H'3; Absurd (order a1 a2); Auto.
Rewrite <- H3; Intros H'0 H'1 H'2; Apply pX_inj; Auto.
Apply pX_invl with p := l2 q := q; Auto.
Apply uniq_plusp with l := ((pX a1 l1), l2); Simpl; Auto.
Rewrite H1; Rewrite (pX_invr l2 q a2 b); Auto.
Qed.
Theorem
plusP_inv3a:
(a, b:Term)
(p, q, s:(list Term))
(eqM a b) -> (zeroP (plusTerm a b)) -> (plusP (pX a p) (pX b q) s) ->
s=(pluspf p q).
Intros a b p q s Eqd Z0 H'; Simple Inversion H'.
Inversion H.
Inversion H0.
Rewrite (pX_invl a1 a l1 p); Try Rewrite (pX_invl a2 b l2 q); Auto.
Intros H'0; Absurd (order b a); Auto.
Apply order_not_eqM; Apply eqM_sym; Auto.
Rewrite <- H4; Rewrite <- (pX_invr l2 q a2 b);
Try Rewrite <- (pX_invr l1 p a1 a); Auto.
Intros H'0 H'1 H'2; Apply uniq_plusp with l := (l1, l2); Auto.
Rewrite (pX_invl a1 a l1 p); Try Rewrite (pX_invl a2 b l2 q); Auto.
Intros H'0 H'1 H'2; Elim H'2; Try Assumption.
Intros H'0; Absurd (order a b); Auto.
Rewrite <- (pX_invl a1 a l1 p); Try Rewrite <- (pX_invl a2 b l2 q); Auto.
Qed.
Theorem
plusP_inv3b:
(a, b:Term)
(p, q, s:(list Term))
(eqM a b) -> ~ (zeroP (plusTerm a b)) -> (plusP (pX a p) (pX b q) s) ->
s=(pX (plusTerm a b) (pluspf p q)).
Intros a b p q s Eqd Z0 H'; Simple Inversion H'.
Inversion H.
Inversion H0.
Rewrite (pX_invl a1 a l1 p); Try Rewrite (pX_invl a2 b l2 q); Auto.
Intros H'0; Absurd (order b a); Auto.
Apply order_not_eqM; Apply eqM_sym; Auto.
Try Rewrite <- H3; Try Rewrite <- (pX_invr l2 q a2 b);
Try Rewrite <- (pX_invr l1 p a1 a); Auto.
Rewrite (pX_invl a1 a l1 p); Try Rewrite (pX_invl a2 b l2 q); Auto.
Intros H'0 H'1 H'2.
Apply Z0 Orelse Elim Z0; Try Assumption.
Intros H'0 H'1 H'2; Rewrite <- H4.
Intros; Apply pX_inj; Auto.
Rewrite (pX_invl a1 a l1 p); Try Rewrite (pX_invl a2 b l2 q); Auto.
Apply uniq_plusp with l := (l1, l2); Auto.
Rewrite <- (pX_invr l2 q a2 b); Try Rewrite <- (pX_invr l1 p a1 a); Auto.
Intros H'0; Absurd (order a b); Auto.
Rewrite <- (pX_invl a1 a l1 p); Try Rewrite <- (pX_invl a2 b l2 q); Auto.
Qed.
Theorem
pluspf_inv1:
(a, b:Term) (p, q:(list Term)) (order b a) ->
(eqP (pX a (pluspf p (pX b q))) (pluspf (pX a p) (pX b q))).
Intros a b p q H'; Try Assumption.
Rewrite (plusP_inv1 a b p q (pluspf (pX a p) (pX b q))); Auto.
Qed.
Theorem
pluspf_inv2:
(a, b:Term) (p, q:(list Term)) (order a b) ->
(eqP (pX b (pluspf (pX a p) q)) (pluspf (pX a p) (pX b q))).
Intros a b p q H'; Try Assumption.
Rewrite (plusP_inv2 a b p q (pluspf (pX a p) (pX b q))); Auto.
Qed.
Theorem
pluspf_inv3a:
(a, b:Term) (p, q:(list Term)) (eqM a b) -> (zeroP (plusTerm a b)) ->
(eqP (pluspf p q) (pluspf (pX a p) (pX b q))).
Intros a b p q H' Z; Try Assumption.
Rewrite (plusP_inv3a a b p q (pluspf (pX a p) (pX b q))); Auto.
Qed.
Theorem
pluspf_inv3b:
(a, b:Term) (p, q:(list Term)) (eqM a b) -> ~ (zeroP (plusTerm a b)) ->
(eqP (pX (plusTerm a b) (pluspf p q)) (pluspf (pX a p) (pX b q))).
Intros a b p q H' Z; Try Assumption.
Rewrite (plusP_inv3b a b p q (pluspf (pX a p) (pX b q))); Auto.
Qed.
Hints Resolve pluspf_inv1 pluspf_inv2 pluspf_inv3a pluspf_inv3b.
Theorem
plusP_com:
(p, q, r, s:(list Term)) (plusP p q r) -> (plusP q p s) ->(eqP r s).
Intros p q r s H'; Generalize s; Elim H'; Clear s H'; Auto.
Intros l1 s H'; Try Assumption.
Rewrite (pO_plusP_inv2 l1 s); Auto.
Intros l1 s H'; Rewrite (pO_plusP_inv1 l1 s); Auto.
Intros a1 a2 l1 l2 l3 H' H'0 H'1 s H'2.
Rewrite (plusP_inv2 a2 a1 l2 l1 s); Auto.
Intros a1 a2 l1 l2 l3 H' H'0 H'1 H'2 s R.
Rewrite (plusP_inv3a a2 a1 l2 l1 s); Auto.
Apply eqM_sym; Auto.
Apply zeroP_comp_eqTerm with a := (plusTerm a1 a2); Auto.
Intros a1 a2 l1 l2 l3 H' H'0 H'1 H'2 s H'3.
Rewrite (plusP_inv3b a2 a1 l2 l1 s); Auto.
Apply eqM_sym; Auto.
Red; Intros H'4; Apply H'2.
Apply zeroP_comp_eqTerm with a := (plusTerm a2 a1); Auto.
Intros a1 a2 l1 l2 l3 H' H'0 H'1 s H'2.
Rewrite (plusP_inv1 a2 a1 l2 l1 s); Auto.
Qed.
Theorem
pluspf_com: (p, q:(list Term))(eqP (pluspf p q) (pluspf q p)).
Intros p q; Apply (plusP_com p q (pluspf p q) (pluspf q p)); Auto.
Qed.
Theorem
plusP_zero_pOl: (p, q:(list Term)) (plusP pO p q) ->(eqP p q).
Intros p q H'; Inversion H'; Auto.
Qed.
Theorem
plusP_zero_pOr: (p, q:(list Term)) (plusP p pO q) ->(eqP p q).
Intros p q H'; Inversion H'; Auto.
Qed.
Theorem
plusTerm_orderr:
(a, b, c:Term) (eqM a b) -> (order c a) ->(order c (plusTerm a b)).
Intros a b c; Unfold order ltB eqM eqB; Intros H';
Generalize (plusTerm_eq1 a b); Unfold order ltB eqM eqB.
Intros H'1; Rewrite H'1; Auto.
Qed.
Theorem
plusTerm_orderl:
(a, b, c:Term) (eqM a b) -> (order a c) ->(order (plusTerm a b) c).
Intros a b c; Unfold order ltB eqM eqB; Intros H';
Generalize (plusTerm_eq1 a b); Unfold order ltB eqM eqB.
Intros H'1; Rewrite H'1; Auto.
Qed.
Hints Resolve plusP_zero_pOl plusP_zero_pOr.
Hints Resolve eqp_trans.
Theorem
plusP_uniq_eqP:
(p, q, r, s:(list Term)) (plusP p q r) -> (plusP p q s) ->(eqP r s).
Intros p q r s H' H'0; Rewrite (uniq_plusp (p, q) r s); Auto.
Qed.
Hints Resolve plusP_uniq_eqP.
Theorem
pO_pluspf_inv1: (p:(list Term))p=(pluspf pO p).
Intros p.
Apply uniq_plusp with l := (pO, p); Auto.
Qed.
Theorem
pO_pluspf_inv2: (p:(list Term))p=(pluspf p pO).
Intros p.
Apply uniq_plusp with l := (p, pO); Auto.
Qed.
Theorem
pluspf_inv1_eq:
(a, b:Term) (p, q:(list Term)) (order b a) ->
(pX a (pluspf p (pX b q)))=(pluspf (pX a p) (pX b q)).
Intros a b p q H'; Rewrite (plusP_inv1 a b p q (pluspf (pX a p) (pX b q))); Auto.
Qed.
Theorem
pluspf_inv2_eq:
(a, b:Term) (p, q:(list Term)) (order a b) ->
(pX b (pluspf (pX a p) q))=(pluspf (pX a p) (pX b q)).
Intros a b p q H'; Rewrite (plusP_inv2 a b p q (pluspf (pX a p) (pX b q))); Auto.
Qed.
Theorem
pluspf_inv3a_eq:
(a, b:Term) (p, q:(list Term)) (eqM a b) -> (zeroP (plusTerm a b)) ->
(pluspf p q)=(pluspf (pX a p) (pX b q)).
Intros a b p q H' H1'; Rewrite (plusP_inv3a a b p q (pluspf (pX a p) (pX b q)));
Auto.
Qed.
Theorem
pluspf_inv3b_eq:
(a, b:Term) (p, q:(list Term)) (eqM a b) -> ~ (zeroP (plusTerm a b)) ->
(pX (plusTerm a b) (pluspf p q))=(pluspf (pX a p) (pX b q)).
Intros a b p q H' H1'; Rewrite (plusP_inv3b a b p q (pluspf (pX a p) (pX b q)));
Auto.
Qed.
Theorem
order_pluspf:
(l1, l2:(list Term))
(a:Term) (canonical (pX a l1)) -> (canonical (pX a l2)) ->
(canonical (pX a (pluspf l1 l2))).
Intros l1 l2 a H' H'0.
Apply order_plusP with l1 := l1 l2 := l2; Auto.
Apply canonical_pluslmf; Auto.
Apply canonical_imp_canonical with a := a; Auto.
Apply canonical_imp_canonical with a := a; Auto.
Qed.
Theorem
pluspf_inv1_eqa:
(a:Term) (p, q:(list Term)) (canonical (pX a p)) -> (canonical (pX a q)) ->
<(list Term)> (pX a (pluspf p q))=(pluspf (pX a p) q).
Intros a p q; Case q; Auto.
Rewrite <- pO_pluspf_inv2; Auto.
Rewrite <- pO_pluspf_inv2; Auto.
Intros a0 l H'0 H'1.
Apply pluspf_inv1_eq; Auto.
Apply canonical_imp_order with l := l; Auto.
Qed.
Theorem
pluspf_inv2_eqa:
(a:Term) (p, q:(list Term)) (canonical (pX a p)) -> (canonical (pX a q)) ->
<(list Term)> (pX a (pluspf p q))=(pluspf p (pX a q)).
Intros a p; Case p; Auto.
Intros q H'0 H'1.
Rewrite <- pO_pluspf_inv1; Auto.
Rewrite <- pO_pluspf_inv1; Auto.
Intros a0 l q H'0 H'1.
Apply pluspf_inv2_eq; Auto.
Apply canonical_imp_order with l := l; Auto.
Qed.
Theorem
pluspf3_assoc:
(l:(list Term) * ((list Term) * (list Term)))
(canonical (Fst l)) ->
(canonical (Fst (Snd l))) -> (canonical (Snd (Snd l))) ->
(eqP
(pluspf (pluspf (Fst l) (Fst (Snd l))) (Snd (Snd l)))
(pluspf (Fst l) (pluspf (Fst (Snd l)) (Snd (Snd l))))).
Intros l; Pattern l.
Apply (well_founded_ind ? lessP3 wf_lessP3).
Intros x; Case x; Intros p z; Case z; Intros q r; Simpl; Clear x z; Auto.
Case p.
Rewrite <- pO_pluspf_inv1; Auto.
Case q.
Intros a l0; Rewrite <- pO_pluspf_inv1; Rewrite <- pO_pluspf_inv2; Auto.
Case r; Simpl; Auto.
Intros a l0 a0 l1; Rewrite <- pO_pluspf_inv2; Rewrite <- pO_pluspf_inv2; Auto.
Intros a l0 a0 l1 a1 l2 H' H'0 H'1 H'2.
Cut (canonical l0); [Intros C0 | Apply canonical_imp_canonical with a := a];
Auto.
Cut (canonical l1); [Intros C1 | Apply canonical_imp_canonical with a := a0];
Auto.
Cut (canonical l2); [Intros C2 | Apply canonical_imp_canonical with a := a1];
Auto.
Cut ~ (zeroP a); [Intros nZ0 | Apply canonical_nzeroP with p := l0]; Auto.
Cut ~ (zeroP a0); [Intros nZ1 | Apply canonical_nzeroP with p := l1]; Auto.
Cut ~ (zeroP a1); [Intros nZ2 | Apply canonical_nzeroP with p := l2]; Auto.
Change (eqP
(pluspf (pluspf (pX a1 l2) (pX a0 l1)) (pX a l0))
(pluspf (pX a1 l2) (pluspf (pX a0 l1) (pX a l0)))).
Case (order_dec a1 a0); [Intros H0; Case H0; Clear H0 | Idtac]; Intros H0.
Case (order_dec a0 a); [Intros H1; Case H1; Clear H1 | Idtac]; Intros H1.
Cut (order a1 a); [Intros Ord0 | Apply order_trans with y := a0]; Auto.
Rewrite <- (pluspf_inv2_eq a1 a0 l2 l1); Auto.
Rewrite <- (pluspf_inv2_eq a0 a (pluspf (pX a1 l2) l1) l0); Auto.
Rewrite <- (pluspf_inv2_eq a0 a l1 l0); Auto.
Rewrite <- (pluspf_inv2_eq a1 a l2 (pluspf (pX a0 l1) l0)); Auto.
Apply eqpP1; Auto.
Rewrite (pluspf_inv2_eq a1 a0 l2 l1); Auto.
Apply H'
with y :=
<(list Term), (list Term) * (list Term)>
((pX a1 l2), <(list Term), (list Term)> ((pX a0 l1), l0)); Simpl;
Auto.
Red; Red; Simpl; Auto with arith.
Rewrite <- (pluspf_inv1_eq a0 a l1 l0); Auto.
Rewrite <- (pluspf_inv2_eq a1 a0 l2 l1); Auto.
Rewrite <- (pluspf_inv2_eq a1 a0 l2 (pluspf l1 (pX a l0))); Auto.
Rewrite <- (pluspf_inv1_eq a0 a (pluspf (pX a1 l2) l1) l0); Auto.
Apply eqpP1; Auto.
Apply H'
with y :=
<(list Term), (list Term) * (list Term)>
((pX a1 l2), <(list Term), (list Term)> (l1, (pX a l0))); Simpl;
Auto.
Red; Red; Simpl; Auto with arith.
Cut (order a1 a); [Intros Ord0 | Apply order_eqM_l with a := a0]; Auto.
Case (zeroP_dec (plusTerm a0 a)); Intros Z0.
Rewrite <- (pluspf_inv3a_eq a0 a l1 l0); Auto.
Rewrite <- (pluspf_inv2_eq a1 a0 l2 l1); Auto.
Rewrite <- (pluspf_inv3a_eq a0 a (pluspf (pX a1 l2) l1) l0); Auto.
Apply H'
with y :=
<(list Term), (list Term) * (list Term)>
((pX a1 l2), <(list Term), (list Term)> (l1, l0)); Simpl; Auto.
Red; Red; Simpl; Auto with arith.
Cut (order a1 (plusTerm a0 a));
[Intros Ord1 | Apply order_eqM_l with a := a0; Auto; Apply eqM_sym]; Auto.
Rewrite <- (pluspf_inv2_eq a1 a0 l2 l1); Auto.
Rewrite <- (pluspf_inv3b_eq a0 a l1 l0); Auto.
Rewrite <- (pluspf_inv3b_eq a0 a (pluspf (pX a1 l2) l1) l0); Auto.
Rewrite <- (pluspf_inv2_eq a1 (plusTerm a0 a) l2 (pluspf l1 l0)); Auto.
Apply eqpP1; Auto.
Apply H'
with y :=
<(list Term), (list Term) * (list Term)>
((pX a1 l2), <(list Term), (list Term)> (l1, l0)); Simpl; Auto.
Red; Red; Simpl; Auto with arith.
Rewrite <- (pluspf_inv1_eq a1 a0 l2 l1); Auto.
Case (order_dec a0 a); [Intros H1; Case H1; Clear H1 | Idtac]; Intros H1.
Rewrite <- (pluspf_inv2_eq a0 a l1 l0); Auto.
Case (order_dec a1 a); [Intros H2; Case H2; Clear H2 | Idtac]; Intros H2.
Rewrite <- (pluspf_inv2_eq a1 a (pluspf l2 (pX a0 l1)) l0); Auto.
Rewrite <- (pluspf_inv2_eq a1 a l2 (pluspf (pX a0 l1) l0)); Auto.
Apply eqpP1; Auto.
Rewrite (pluspf_inv1_eq a1 a0 l2 l1); Auto.
Apply H'
with y :=
<(list Term), (list Term) * (list Term)>
((pX a1 l2), <(list Term), (list Term)> ((pX a0 l1), l0)); Simpl;
Auto.
Red; Red; Simpl; Auto with arith.
Rewrite <- (pluspf_inv1_eq a1 a l2 (pluspf (pX a0 l1) l0)); Auto.
Rewrite <- (pluspf_inv1_eq a1 a (pluspf l2 (pX a0 l1)) l0); Auto.
Apply eqpP1; Auto.
Rewrite (pluspf_inv2_eq a0 a l1 l0); Auto.
Apply H'
with y :=
<(list Term), (list Term) * (list Term)>
(l2, <(list Term), (list Term)> ((pX a0 l1), (pX a l0))); Simpl;
Auto.
Red; Red; Simpl; Auto.
Cut (order a0 (plusTerm a1 a));
[Intros Ord1 | Apply order_eqM_l with a := a; Auto; Apply eqM_sym]; Auto.
Case (zeroP_dec (plusTerm a1 a)); Intros Z0.
Rewrite <- (pluspf_inv3a_eq a1 a (pluspf l2 (pX a0 l1)) l0); Auto.
Rewrite <- (pluspf_inv3a_eq a1 a l2 (pluspf (pX a0 l1) l0)); Auto.
Apply H'
with y :=
<(list Term), (list Term) * (list Term)>
(l2, <(list Term), (list Term)> ((pX a0 l1), l0)); Simpl; Auto.
Red; Red; Simpl; Auto with arith.
Rewrite <- (pluspf_inv3b_eq a1 a (pluspf l2 (pX a0 l1)) l0); Auto.
Rewrite <- (pluspf_inv3b_eq a1 a l2 (pluspf (pX a0 l1) l0)); Auto.
Apply eqpP1; Auto.
Apply H'
with y :=
<(list Term), (list Term) * (list Term)>
(l2, <(list Term), (list Term)> ((pX a0 l1), l0)); Simpl; Auto.
Red; Red; Simpl; Auto with arith.
Cut (order a a1); [Intros Ord0 | Apply order_trans with y := a0];
Auto with arith.
Rewrite <- (pluspf_inv1_eq a0 a l1 l0); Auto.
Rewrite <- (pluspf_inv1_eq a1 a0 l2 (pluspf l1 (pX a l0))); Auto.
Rewrite <- (pluspf_inv1_eq a1 a (pluspf l2 (pX a0 l1)) l0); Auto.
Apply eqpP1; Auto.
Rewrite (pluspf_inv1_eq a0 a l1 l0); Auto.
Apply H'
with y :=
<(list Term), (list Term) * (list Term)>
(l2, <(list Term), (list Term)> ((pX a0 l1), (pX a l0))); Simpl;
Auto.
Red; Red; Simpl; Auto.
Cut (order a a1); [Intros Ord0 | Apply order_eqM_r with a := a0]; Auto.
Case (zeroP_dec (plusTerm a0 a)); Intros Z0.
Rewrite <- (pluspf_inv3a_eq a0 a l1 l0); Auto.
Rewrite <- (pluspf_inv1_eqa a1 l2 (pluspf l1 l0)); Auto.
Rewrite <- (pluspf_inv1_eq a1 a (pluspf l2 (pX a0 l1)) l0); Auto.
Apply eqpP1; Auto.
Apply eqp_trans with y := (pluspf l2 (pluspf (pX a0 l1) (pX a l0))); Auto.
Apply H'
with y :=
<(list Term), (list Term) * (list Term)>
(l2, <(list Term), (list Term)> ((pX a0 l1), (pX a l0))); Simpl;
Auto.
Red; Red; Simpl; Auto.
Rewrite <- (pluspf_inv3a_eq a0 a l1 l0); Auto.
Apply order_pluspf; Auto.
Apply canonical_skip_fst with b := a0; Auto.
Apply canonical_skip_fst with b := a; Auto.
Cut (order (plusTerm a0 a) a1);
[Intros Ord1 | Apply order_eqM_r with a := a0; Auto; Apply eqM_sym]; Auto.
Rewrite <- (pluspf_inv3b_eq a0 a l1 l0); Auto.
Rewrite <- (pluspf_inv1_eq a1 a (pluspf l2 (pX a0 l1)) l0); Auto.
Rewrite <- (pluspf_inv1_eq a1 (plusTerm a0 a) l2 (pluspf l1 l0)); Auto.
Apply eqpP1; Auto.
Apply eqp_trans with y := (pluspf l2 (pluspf (pX a0 l1) (pX a l0))); Auto.
Apply H'
with y :=
<(list Term), (list Term) * (list Term)>
(l2, <(list Term), (list Term)> ((pX a0 l1), (pX a l0))); Simpl;
Auto.
Red; Red; Simpl; Auto.
Rewrite <- (pluspf_inv3b_eq a0 a l1 l0); Auto.
Case (zeroP_dec (plusTerm a1 a0)); Intros Z0.
Rewrite <- (pluspf_inv3a_eq a1 a0 l2 l1); Auto.
Case (order_dec a1 a); [Intros H2; Case H2; Clear H2 | Idtac]; Intros H2.
Cut (order a0 a); [Intros Ord0 | Apply order_eqM_r with a := a1]; Auto.
Rewrite <- (pluspf_inv2_eq a0 a l1 l0); Auto.
Rewrite <- (pluspf_inv2_eq a1 a l2 (pluspf (pX a0 l1) l0)); Auto.
Apply eqp_trans with y := (pX a (pluspf (pluspf (pX a1 l2) (pX a0 l1)) l0));
Auto.
Rewrite <- (pluspf_inv3a_eq a1 a0 l2 l1); Auto.
Rewrite <- (pluspf_inv2_eqa a (pluspf l2 l1) l0); Auto.
Apply order_pluspf; Auto.
Apply canonical_skip_fst with b := a1; Auto.
Apply canonical_skip_fst with b := a0; Auto.
Apply eqpP1; Auto.
Apply H'
with y :=
<(list Term), (list Term) * (list Term)>
((pX a1 l2), <(list Term), (list Term)> ((pX a0 l1), l0)); Simpl;
Auto.
Red; Red; Simpl; Auto with arith.
Cut (order a a0); [Intros Ord0 | Apply order_eqM_l with a := a1]; Auto.
Rewrite <- (pluspf_inv1_eq a0 a l1 l0); Auto.
Rewrite <- (pluspf_inv3a_eq a1 a0 l2 (pluspf l1 (pX a l0))); Auto.
Apply H'
with y :=
<(list Term), (list Term) * (list Term)>
(l2, <(list Term), (list Term)> (l1, (pX a l0))); Simpl; Auto.
Red; Red; Simpl; Auto with arith.
Case (zeroP_dec (plusTerm a0 a)); Intros Z1.
Cut (eqM a0 a);
[Intros eqTerm0 | Apply eqM_trans with y := a1; Auto; Apply eqM_sym]; Auto.
Cut (eqM a (plusTerm a1 a0));
[Intros eqTerm1 | Apply eqM_trans with y := a0; Auto; Apply eqM_sym]; Auto.
Cut (eqM (plusTerm a a1) a0);
[Intros eqTerm2 |
Apply eqM_trans with y := a; [Apply plusTerm_eqM1 | Idtac]; Apply eqM_sym];
Auto.
Cut (eqM (plusTerm a1 a) a0);
[Intros eqTerm3 | Apply eqM_trans with y := a; Auto; Apply eqM_sym]; Auto.
Cut (eqM a1 (plusTerm a a0));
[Intros eqTerm4 |
Apply eqM_trans with y := a0; Auto; Apply eqM_sym; Auto; Apply plusTerm_eqM2;
Apply eqM_sym]; Auto.
Cut (eqM a1 (plusTerm a0 a));
[Intros eqTerm5 |
Apply eqM_trans with y := a0; Auto; Apply eqM_sym; Auto; Apply plusTerm_eqM2;
Apply eqM_sym]; Auto.
Rewrite <- (pluspf_inv3a_eq a0 a l1 l0); Auto.
Rewrite <- (pluspf_inv2_eqa a (pluspf l2 l1) l0); Auto.
Rewrite <- (pluspf_inv1_eqa a1 l2 (pluspf l1 l0)); Auto.
Apply eqpP1; Auto.
Apply eqTerm_trans with y := (plusTerm a (plusTerm a1 a0)); Auto.
Apply eqTerm_trans with y := (plusTerm a1 (plusTerm a0 a)); Auto.
Apply eqTerm_trans with y := (plusTerm a1 (plusTerm a a0)); Auto.
Apply eqTerm_trans with y := (plusTerm (plusTerm a a1) a0); Auto.
Apply eqTerm_trans with y := (plusTerm (plusTerm a1 a) a0); Auto.
Apply H'
with y :=
<(list Term), (list Term) * (list Term)>
(l2, <(list Term), (list Term)> (l1, l0)); Simpl; Auto.
Red; Red; Simpl; Auto with arith.
Apply order_pluspf; Auto.
Apply canonical_pX_eqM with a := a0; Auto.
Apply eqM_sym; Auto.
Apply canonical_pX_eqM with a := a; Auto.
Apply eqM_sym; Auto.
Apply order_pluspf; Auto.
Apply canonical_pX_eqM with a := a1; Auto.
Apply canonical_pX_eqM with a := a0; Auto.
Cut (eqM a0 a);
[Intros Ord0 | Apply eqM_trans with y := a1; Auto; Apply eqM_sym]; Auto.
Cut (eqM a (plusTerm a1 a0));
[Intros eqTerm1 | Apply eqM_trans with y := a0; Auto; Apply eqM_sym]; Auto.
Rewrite <- (pluspf_inv3b_eq a0 a l1 l0); Auto.
Rewrite <- (pluspf_inv3b_eq a1 (plusTerm a0 a) l2 (pluspf l1 l0)); Auto.
Rewrite <- (pluspf_inv2_eqa a (pluspf l2 l1) l0); Auto.
Apply eqpP1; Auto.
Apply eqTerm_trans with y := (plusTerm a (plusTerm a1 a0)); Auto.
Apply eqTerm_trans with y := (plusTerm (plusTerm a1 a0) a); Auto.
Apply H'
with y :=
<(list Term), (list Term) * (list Term)>
(l2, <(list Term), (list Term)> (l1, l0)); Simpl; Auto.
Red; Red; Simpl; Auto with arith.
Apply order_pluspf; Auto.
Apply canonical_pX_eqM with a := a1; Auto.
Apply canonical_pX_eqM with a := a0; Auto.
Apply eqM_trans with y := a; Auto; Apply eqM_sym; Auto.
Red; Intros H'3; Absurd (zeroP a); Auto.
Apply zeroP_comp_eqTerm with a := (plusTerm a1 (plusTerm a0 a)); Auto.
Apply eqTerm_trans with y := (plusTerm (plusTerm a1 a0) a); Auto.
Rewrite <- (pluspf_inv3b_eq a1 a0 l2 l1); Auto.
Case (order_dec a0 a); [Intros H1; Case H1; Clear H1 | Idtac]; Intros H1.
Cut (order a1 a);
[Intros Ord0 | Apply order_eqM_r with a := a0; Auto; Apply eqM_sym]; Auto.
Cut (order (plusTerm a1 a0) a);
[Intros Ord1 | Apply order_eqM_r with a := a0; Auto; Apply eqM_sym]; Auto.
Rewrite <- (pluspf_inv2_eq a0 a l1 l0); Auto.
Rewrite <- (pluspf_inv2_eq a1 a l2 (pluspf (pX a0 l1) l0)); Auto.
Rewrite <- (pluspf_inv2_eq (plusTerm a1 a0) a (pluspf l2 l1) l0); Auto.
Apply eqpP1; Auto.
Apply eqp_trans with y := (pluspf (pluspf (pX a1 l2) (pX a0 l1)) l0); Auto.
Rewrite <- (pluspf_inv3b_eq a1 a0 l2 l1); Auto.
Apply H'
with y :=
<(list Term), (list Term) * (list Term)>
((pX a1 l2), <(list Term), (list Term)> ((pX a0 l1), l0)); Simpl;
Auto.
Red; Red; Simpl; Auto with arith.
Cut (order a a1);
[Intros Ord0 | Apply order_eqM_l with a := a0; Auto; Apply eqM_sym]; Auto.
Cut (order a (plusTerm a1 a0));
[Intros Ord1 | Apply order_eqM_l with a := a0; Auto; Apply eqM_sym]; Auto.
Rewrite <- (pluspf_inv1_eq a0 a l1 l0); Auto.
Rewrite <- (pluspf_inv3b_eq a1 a0 l2 (pluspf l1 (pX a l0))); Auto.
Rewrite <- (pluspf_inv1_eq (plusTerm a1 a0) a (pluspf l2 l1) l0); Auto.
Apply eqpP1; Auto.
Apply H'
with y :=
<(list Term), (list Term) * (list Term)>
(l2, <(list Term), (list Term)> (l1, (pX a l0))); Simpl; Auto.
Red; Red; Simpl; Auto with arith.
Cut (eqM a1 (plusTerm a0 a));
[Intros eqTerm1 | Apply eqM_trans with y := a0; Auto; Apply eqM_sym]; Auto.
Cut (eqM a1 a);
[Intros eqM0 | Apply eqM_trans with y := a0; Auto; Apply eqM_sym]; Auto.
Case (zeroP_dec (plusTerm a0 a)); Intros Z1.
Rewrite <- (pluspf_inv3a_eq a0 a l1 l0); Auto.
Rewrite <- (pluspf_inv1_eqa a1 l2 (pluspf l1 l0)); Auto.
Cut ~ (zeroP (plusTerm (plusTerm a1 a0) a)); [Intros Z2 | Idtac].
Rewrite <- (pluspf_inv3b_eq (plusTerm a1 a0) a (pluspf l2 l1) l0); Auto.
Apply eqpP1; Auto.
Apply eqTerm_trans with y := (plusTerm a1 (plusTerm a0 a)); Auto.
Apply H'
with y :=
<(list Term), (list Term) * (list Term)>
(l2, <(list Term), (list Term)> (l1, l0)); Simpl; Auto.
Red; Red; Simpl; Auto with arith.
Apply eqM_trans with y := a1; Auto; Apply eqM_sym; Auto.
Red; Intros H'3; Absurd (zeroP a1); Auto.
Apply zeroP_comp_eqTerm with a := (plusTerm (plusTerm a1 a0) a); Auto.
Apply eqTerm_trans with y := (plusTerm a1 (plusTerm a0 a)); Auto.
Apply order_pluspf; Auto.
Apply canonical_pX_eqM with a := a0; Auto.
Apply eqM_sym; Auto.
Apply canonical_pX_eqM with a := a; Auto.
Apply eqM_sym; Auto.
Rewrite <- (pluspf_inv3b_eq a0 a l1 l0); Auto.
Cut (eqTerm (plusTerm (plusTerm a1 a0) a) (plusTerm a1 (plusTerm a0 a)));
[Intros eqTerm0 | Idtac].
Case (zeroP_dec (plusTerm (plusTerm a1 a0) a)); Intros Z2.
Rewrite <- (pluspf_inv3a_eq (plusTerm a1 a0) a (pluspf l2 l1) l0); Auto.
Rewrite <- (pluspf_inv3a_eq a1 (plusTerm a0 a) l2 (pluspf l1 l0)); Auto.
Apply H'
with y :=
<(list Term), (list Term) * (list Term)>
(l2, <(list Term), (list Term)> (l1, l0)); Simpl; Auto.
Red; Red; Simpl; Auto with arith.
Apply zeroP_comp_eqTerm with a := (plusTerm (plusTerm a1 a0) a); Auto.
Apply eqM_trans with y := a0; Auto; Apply eqM_sym; Auto.
Rewrite <- (pluspf_inv3b_eq (plusTerm a1 a0) a (pluspf l2 l1) l0); Auto.
Rewrite <- (pluspf_inv3b_eq a1 (plusTerm a0 a) l2 (pluspf l1 l0)); Auto.
Apply eqpP1; Auto.
Apply H'
with y :=
<(list Term), (list Term) * (list Term)>
(l2, <(list Term), (list Term)> (l1, l0)); Simpl; Auto.
Red; Red; Simpl; Auto with arith.
Apply nzeroP_comp_eqTerm with a := (plusTerm (plusTerm a1 a0) a); Auto.
Apply eqM_trans with y := a0; Auto; Apply eqM_sym; Auto.
Apply plusTerm_assoc; Auto.
Qed.
Theorem
pluspf_assoc:
(p, q, r:(list Term)) (canonical p) -> (canonical q) -> (canonical r) ->
(eqP (pluspf (pluspf p q) r) (pluspf p (pluspf q r))).
Intros p q r H' H'0 H'1.
Apply pluspf3_assoc with l := (p, (q, r)); Auto.
Qed.
Hints Resolve pluspf_assoc.
Theorem
eqp_pluspf_com_l:
(p, q, r:(list Term))
(eqP p q) -> (canonical p) -> (canonical q) -> (canonical r) ->
(eqP (pluspf p r) (pluspf q r)).
Intros p q r H'; Generalize r; Elim H'; Clear r H'.
Intros r H' H'0 H'1; Rewrite <- pO_pluspf_inv1; Auto.
Intros ma mb p0 q0 H' H'0 H'1 r H'2 H'3 H'4.
Cut (canonical p0); [Intros C0 | Apply canonical_imp_canonical with a := ma];
Auto.
Cut (canonical q0); [Intros C1 | Apply canonical_imp_canonical with a := mb];
Auto.
Cut ~ (zeroP ma); [Intros nZ0 | Apply canonical_nzeroP with p := p0]; Auto.
Cut ~ (zeroP mb); [Intros nZ1 | Apply canonical_nzeroP with p := q0]; Auto.
Generalize H'4; Elim r; Clear H'4 r.
Intros H'4; Rewrite <- pO_pluspf_inv2; Rewrite <- pO_pluspf_inv2; Auto.
Intros a l H'4 H'5.
Cut (canonical l); [Intros C2 | Apply canonical_imp_canonical with a := a]; Auto.
Cut ~ (zeroP a); [Intros nZ2 | Apply canonical_nzeroP with p := l]; Auto.
Change (eqP (pluspf (pX ma p0) (pX a l)) (pluspf (pX mb q0) (pX a l))).
Case (order_dec ma a); [Intros H0; Case H0; Clear H0 | Idtac]; Intros H0.
Cut (order mb a); [Intros Or0 | Idtac].
Rewrite <- (pluspf_inv2_eq ma a p0 l); Auto.
Rewrite <- (pluspf_inv2_eq mb a q0 l); Auto.
Apply order_eqM_r with a := ma; Auto.
Cut (order a mb); [Intros Or0 | Idtac]; Auto.
Rewrite <- (pluspf_inv1_eq ma a p0 l); Auto.
Rewrite <- (pluspf_inv1_eq mb a q0 l); Auto.
Apply order_eqM_l with a := ma; Auto.
Cut (eqTerm (plusTerm ma a) (plusTerm mb a)); [Intros eqTerm0 | Idtac]; Auto.
Case (zeroP_dec (plusTerm ma a)); Intros Z0.
Rewrite <- (pluspf_inv3a_eq ma a p0 l); Auto.
Rewrite <- (pluspf_inv3a_eq mb a q0 l); Auto.
Apply eqM_trans with y := ma; Auto.
Apply zeroP_comp_eqTerm with a := (plusTerm ma a); Auto.
Rewrite <- (pluspf_inv3b_eq ma a p0 l); Auto.
Rewrite <- (pluspf_inv3b_eq mb a q0 l); Auto.
Apply eqM_trans with y := ma; Auto.
Red; Intros H'6; Apply Z0.
Apply zeroP_comp_eqTerm with a := (plusTerm mb a); Auto.
Apply eqTerm_plusTerm_comp; Auto.
Change (eqM mb a).
Apply eqM_trans with y := ma; Auto.
Qed.
Theorem
eqp_pluspf_com_r:
(p, q, r:(list Term))
(eqP p q) -> (canonical p) -> (canonical q) -> (canonical r) ->
(eqP (pluspf r p) (pluspf r q)).
Intros p q r H'; Generalize r; Elim H'; Clear r H'.
Intros r H' H'0 H'1; Rewrite <- pO_pluspf_inv2; Auto.
Intros ma mb p0 q0 H' H'0 H'1 r H'2 H'3 H'4.
Cut (canonical p0); [Intros C0 | Apply canonical_imp_canonical with a := ma];
Auto.
Cut (canonical q0); [Intros C1 | Apply canonical_imp_canonical with a := mb];
Auto.
Cut ~ (zeroP ma); [Intros nZ0 | Apply canonical_nzeroP with p := p0]; Auto.
Cut ~ (zeroP mb); [Intros nZ1 | Apply canonical_nzeroP with p := q0]; Auto.
Generalize H'4; Elim r; Clear H'4 r.
Intros H'4; Rewrite <- pO_pluspf_inv1; Rewrite <- pO_pluspf_inv1; Auto.
Intros a l H'4 H'5.
Cut (canonical l); [Intros C2 | Apply canonical_imp_canonical with a := a]; Auto.
Cut ~ (zeroP a); [Intros nZ2 | Apply canonical_nzeroP with p := l]; Auto.
Change (eqP (pluspf (pX a l) (pX ma p0)) (pluspf (pX a l) (pX mb q0))).
Case (order_dec ma a); [Intros H0; Case H0; Clear H0 | Idtac]; Intros H0.
Cut (order mb a); [Intros Or0 | Idtac].
Rewrite <- (pluspf_inv1_eq a ma l p0); Auto.
Rewrite <- (pluspf_inv1_eq a mb l q0); Auto.
Apply order_eqM_r with a := ma; Auto.
Cut (order a mb); [Intros Or0 | Idtac]; Auto.
Rewrite <- (pluspf_inv2_eq a ma l p0); Auto.
Rewrite <- (pluspf_inv2_eq a mb l q0); Auto.
Apply order_eqM_l with a := ma; Auto.
Cut (eqTerm (plusTerm a ma) (plusTerm a mb)); [Intros eqTerm0 | Idtac]; Auto.
Case (zeroP_dec (plusTerm a ma)); Intros Z0.
Rewrite <- (pluspf_inv3a_eq a ma l p0); Auto.
Rewrite <- (pluspf_inv3a_eq a mb l q0); Auto.
Apply eqM_trans with y := ma; Auto; Apply eqM_sym; Auto.
Apply zeroP_comp_eqTerm with a := (plusTerm a ma); Auto.
Apply eqM_sym; Auto.
Rewrite <- (pluspf_inv3b_eq a ma l p0); Auto.
Rewrite <- (pluspf_inv3b_eq a mb l q0); Auto.
Apply eqM_trans with y := ma; Auto; Apply eqM_sym; Auto.
Red; Intros H'6; Apply Z0.
Apply zeroP_comp_eqTerm with a := (plusTerm a mb); Auto.
Apply eqM_sym; Auto.
Apply eqTerm_plusTerm_comp; Auto.
Change (eqM a mb).
Apply eqM_trans with y := ma; Auto.
Apply eqM_sym; Auto.
Qed.
Theorem
eqp_pluspf_com:
(p, q, r, t:(list Term))
(canonical p) ->
(canonical q) -> (canonical r) -> (canonical t) -> (eqP p r) -> (eqP q t) ->
(eqP (pluspf p q) (pluspf r t)).
Intros p q r t H' H'0 H'1 H'2 H'3 H'4.
Apply eqp_trans with y := (pluspf r q); Auto.
Apply eqp_pluspf_com_l; Auto.
Apply eqp_pluspf_com_r; Auto.
Qed.
Hints Resolve eqp_pluspf_com.
Theorem
p0_pluspf_l: (p:(list Term))(eqP (pluspf pO p) p).
Intros p; Rewrite <- pO_pluspf_inv1; Auto.
Qed.
Theorem
p0_pluspf_r: (p:(list Term))(eqP (pluspf p pO) p).
Intros p; Rewrite <- pO_pluspf_inv2; Auto.
Qed.
Definition
splus: poly -> poly ->poly.
Intros sp1 sp2.
Case sp1; Case sp2.
Intros p1 H'1 p2 H'2; Exists (pluspf p1 p2); Auto.
Apply canonical_pluslmf; Auto.
Defined.
End SPlus.
18/01/99, 21:47