From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 plugins/setoid_ring/Ncring_polynom.v | 63 ++++++++++++++++++++----------------
 1 file changed, 35 insertions(+), 28 deletions(-)

(limited to 'plugins/setoid_ring/Ncring_polynom.v')

diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v
index eefc9428..5845b629 100644
--- a/plugins/setoid_ring/Ncring_polynom.v
+++ b/plugins/setoid_ring/Ncring_polynom.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -103,7 +103,7 @@ Variable P:Pol.
 
 (* Xi^n * P + Q
 les variables de tete de Q ne sont pas forcement < i 
-mais Q est normalisé : variables de tete decroissantes *)
+mais Q est normalisé : variables de tete decroissantes *)
 
 Fixpoint PaddX (i n:positive)(Q:Pol){struct Q}:=
   match Q with
@@ -216,8 +216,8 @@ Definition Psub(P P':Pol):= P ++ (--P').
   intros l P i n Q;unfold mkPX.
   destruct P;try (simpl;reflexivity).
   assert (Hh := ring_morphism_eq  c 0). 
-simpl; case_eq (Ceqb c 0);simpl;try reflexivity.
-intros.
+  simpl; case_eq (Ceqb c 0);simpl;try reflexivity.
+  intros.
   rewrite Hh. rewrite ring_morphism0.
   rsimpl. apply Ceqb_eq. trivial.
   destruct (Pos.compare_spec i p).
@@ -416,10 +416,13 @@ Qed.
  Variable pow_th : power_theory Cp_phi rpow.
 
  (** evaluation of polynomial expressions towards R *)
+
  Fixpoint PEeval (l:list R) (pe:PExpr C) {struct pe} : R :=
    match pe with
+   | PEO => 0
+   | PEI => 1
    | PEc c => [c]
-   | PEX j => nth 0 j l
+   | PEX _ j => nth 0 j l
    | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2)
    | PEsub pe1 pe2 => (PEeval l pe1) - (PEeval l pe2)
    | PEmul pe1 pe2 => (PEeval l pe1) * (PEeval l pe2)
@@ -500,8 +503,10 @@ Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) :=
 
   Fixpoint norm_aux (pe:PExpr C) : Pol :=
    match pe with
+   | PEO => Pc cO
+   | PEI => Pc cI
    | PEc c => Pc c
-   | PEX j => mk_X j
+   | PEX _ j => mk_X j
    | PEadd pe1 (PEopp pe2) =>
      Psub (norm_aux pe1) (norm_aux pe2)
    | PEadd pe1 pe2 => Padd (norm_aux  pe1) (norm_aux pe2)
@@ -520,28 +525,30 @@ Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) :=
   Proof.
    intros.
    induction pe.
-Esimpl3. Esimpl3. simpl.
- rewrite IHpe1;rewrite IHpe2.
- destruct pe2; Esimpl3. 
-unfold Psub.
-destruct pe1; destruct pe2; rewrite Padd_ok; rewrite Popp_ok; reflexivity.
-simpl. unfold Psub. rewrite IHpe1;rewrite IHpe2.
-destruct pe1. destruct pe2; rewrite Padd_ok; rewrite Popp_ok; try reflexivity.
-Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3.
- Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3.
-simpl. rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. reflexivity.
-simpl. rewrite IHpe; Esimpl3. 
-simpl.
-   rewrite Ppow_N_ok; (intros;try reflexivity). 
-   rewrite rpow_pow_N.  Esimpl3.
-   induction n;simpl. Esimpl3. induction p; simpl.
-  try rewrite IHp;try rewrite IHpe;
- repeat rewrite Pms_ok;
-      repeat rewrite Pmul_ok;reflexivity.
-rewrite Pmul_ok. try rewrite IHp;try rewrite IHpe;
- repeat rewrite Pms_ok;
-      repeat rewrite Pmul_ok;reflexivity. trivial.
-exact pow_th.
+   - now simpl; rewrite <- ring_morphism0.
+   - now simpl; rewrite <- ring_morphism1.
+   - Esimpl3. 
+   - Esimpl3. 
+   - simpl.
+     rewrite IHpe1;rewrite IHpe2.
+     destruct pe2; Esimpl3. 
+     unfold Psub.
+     destruct pe1; destruct pe2; rewrite Padd_ok; rewrite Popp_ok; reflexivity.
+   - simpl. unfold Psub. rewrite IHpe1;rewrite IHpe2.
+     now destruct pe1; 
+       [destruct pe2; rewrite Padd_ok; rewrite Popp_ok; Esimpl3 | Esimpl3..]. 
+   - simpl. rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. reflexivity.
+   - now simpl; rewrite IHpe; Esimpl3. 
+   - simpl.
+     rewrite Ppow_N_ok; (intros;try reflexivity). 
+     rewrite rpow_pow_N; [| now apply pow_th]. 
+     induction n;simpl; [now Esimpl3|]. 
+     induction p; simpl; trivial.
+     + try rewrite IHp;try rewrite IHpe;
+         repeat rewrite Pms_ok; repeat rewrite Pmul_ok;reflexivity.
+     + rewrite Pmul_ok. 
+       try rewrite IHp;try rewrite IHpe; repeat rewrite Pms_ok;
+         repeat rewrite Pmul_ok;reflexivity. 
   Qed.
 
  Lemma norm_subst_spec :
-- 
cgit v1.2.3