Replace nat indices with positive one in Btauto.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15499 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 229 insertions, 160 deletions

diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v
index e3ac563fb..a515deefd 100644
--- a/plugins/btauto/Algebra.v
+++ b/plugins/btauto/Algebra.v
@@ -1,4 +1,4 @@
-Require Import Bool Arith DecidableClass.
+Require Import Bool PArith DecidableClass ROmega.
 
 Ltac bool :=
 repeat match goal with
@@ -57,10 +57,10 @@ Ltac case_decide := match goal with
   let b := fresh "b" in
   let H := fresh "H" in
   define (@decide P D) b H; destruct b; try_decide
-| [ |- context [nat_compare ?x ?y] ] =>
-  destruct (nat_compare_spec x y); try (exfalso; omega)
-| [ X : context [nat_compare ?x ?y] |- _ ] =>
-  destruct (nat_compare_spec x y); try (exfalso; omega)
+| [ |- context [Pos.compare ?x ?y] ] =>
+  destruct (Pos.compare_spec x y); try (exfalso; zify; romega)
+| [ X : context [Pos.compare ?x ?y] |- _ ] =>
+  destruct (Pos.compare_spec x y); try (exfalso; zify; romega)
 end.
 
 Section Definitions.
@@ -72,7 +72,7 @@ Section Definitions.
 
 Inductive poly :=
 | Cst : bool -> poly
-| Poly : poly -> nat -> poly -> poly.
+| Poly : poly -> positive -> poly -> poly.
 
 (* TODO: We should use [positive] instead of [nat] to encode variables, for 
  efficiency purpose. *)
@@ -84,23 +84,41 @@ Inductive null : poly -> Prop :=
   polynomial [p] satisfies [valid n p] whenever it is well-formed and each of 
   its variable indices is < [n]. *)
 
-Inductive valid : nat -> poly -> Prop :=
+Inductive valid : positive -> poly -> Prop :=
 | valid_cst : forall k c, valid k (Cst c)
 | valid_poly : forall k p i q,
-  i < k -> ~ null q -> valid i p -> valid (S i) q -> valid k (Poly p i q).
+  Pos.lt i k -> ~ null q -> valid i p -> valid (Pos.succ i) q -> valid k (Poly p i q).
 
 (** Linear polynomials are valid polynomials in which every variable appears at 
   most once. *)
 
-Inductive linear : nat -> poly -> Prop :=
+Inductive linear : positive -> poly -> Prop :=
 | linear_cst : forall k c, linear k (Cst c)
-| linear_poly : forall k p i q, i < k -> ~ null q ->
+| linear_poly : forall k p i q, Pos.lt i k -> ~ null q ->
   linear i p -> linear i q -> linear k (Poly p i q).
 
 End Definitions.
 
 Section Computational.
 
+Program Instance Decidable_PosEq : forall (p q : positive), Decidable (p = q) :=
+  { Decidable_witness := Pos.eqb p q }.
+Next Obligation.
+apply Pos.eqb_eq.
+Qed.
+
+Program Instance Decidable_PosLt : forall p q, Decidable (Pos.lt p q) :=
+  { Decidable_witness := Pos.ltb p q }.
+Next Obligation.
+apply Pos.ltb_lt.
+Qed.
+
+Program Instance Decidable_PosLe : forall p q, Decidable (Pos.le p q) :=
+  { Decidable_witness := Pos.leb p q }.
+Next Obligation.
+apply Pos.leb_le.
+Qed.
+
 (** * The core reflexive part. *)
 
 Hint Constructors valid.
@@ -135,18 +153,22 @@ Qed.
 Program Instance Decidable_null : forall p, Decidable (null p) := {
   Decidable_witness := match p with Cst false => true | _ => false end
 }.
-
 Next Obligation.
 split.
   destruct p as [[]|]; first [discriminate|constructor].
   inversion 1; trivial.
 Qed.
 
+Definition list_nth {A} p (l : list A) def :=
+  Pos.peano_rect (fun _ => list A -> A)
+    (fun l => match l with nil => def | cons t l => t end)
+    (fun _ F l => match l with nil => def | cons t l => F l end) p l.
+
 Fixpoint eval var (p : poly) :=
 match p with
 | Cst c => c
 | Poly p i q =>
-  let vi := List.nth i var false in
+  let vi := list_nth i var false in
   xorb (eval var p) (andb vi (eval var q))
 end.
 
@@ -154,8 +176,8 @@ Fixpoint valid_dec k p :=
 match p with
 | Cst c => true
 | Poly p i q =>
-  negb (decide (null q)) && decide (i < k) &&
-    valid_dec i p && valid_dec (S i) q
+  negb (decide (null q)) && decide (i < k)%positive &&
+    valid_dec i p && valid_dec (Pos.succ i) q
 end.
 
 Program Instance Decidable_valid : forall n p, Decidable (valid n p) := {
@@ -182,7 +204,7 @@ match pl with
   fix F pr {struct pr} := match pr with
   | Cst cr => Poly (poly_add pl pr) il ql
   | Poly pr ir qr =>
-    match nat_compare il ir with
+    match Pos.compare il ir with
     | Eq =>
       let qs := poly_add ql qr in
       (* Ensure validity *)
@@ -214,7 +236,7 @@ match p with
   if decide (null p) then p
   else Poly (Cst false) k p
 | Poly p i q =>
-  if decide (i <= k) then Poly (Cst false) k (Poly p i q)
+  if decide (i <= k)%positive then Poly (Cst false) k (Poly p i q)
   else Poly (poly_mul_mon k p) i (poly_mul_mon k q)
 end.
 
@@ -268,20 +290,21 @@ Section Validity.
 
 Hint Constructors valid linear.
 
-Lemma valid_le_compat : forall k l p, valid k p -> k <= l -> valid l p.
+Lemma valid_le_compat : forall k l p, valid k p -> (k <= l)%positive -> valid l p.
 Proof.
-intros k l p H Hl; induction H; constructor; eauto with arith.
+intros k l p H Hl; induction H; constructor; eauto.
+now eapply Pos.lt_le_trans; eassumption.
 Qed.
 
-Lemma linear_le_compat : forall k l p, linear k p -> k <= l -> linear l p.
+Lemma linear_le_compat : forall k l p, linear k p -> (k <= l)%positive -> linear l p.
 Proof.
-intros k l p H; revert l; induction H; intuition.
+intros k l p H; revert l; induction H; constructor; eauto; zify; romega.
 Qed.
 
 Lemma linear_valid_incl : forall k p, linear k p -> valid k p.
 Proof.
 intros k p H; induction H; constructor; auto.
-eapply valid_le_compat; eauto.
+eapply valid_le_compat; eauto; zify; romega.
 Qed.
 
 End Validity.
@@ -296,35 +319,35 @@ intros p var []; reflexivity.
 Qed.
 
 Lemma eval_extensional_eq_compat : forall p var1 var2,
-  (forall x, List.nth x var1 false = List.nth x var2 false) -> eval var1 p = eval var2 p.
+  (forall x, list_nth x var1 false = list_nth x var2 false) -> eval var1 p = eval var2 p.
 Proof.
 intros p var1 var2 H; induction p; simpl; try_rewrite; auto.
 Qed.
 
 Lemma eval_suffix_compat : forall k p var1 var2,
-  (forall i, i < k -> List.nth i var1 false = List.nth i var2 false) -> valid k p ->
+  (forall i, (i < k)%positive -> list_nth i var1 false = list_nth i var2 false) -> valid k p ->
   eval var1 p = eval var2 p.
 Proof.
 intros k p var1 var2 Hvar Hv; revert var1 var2 Hvar.
 induction Hv; intros var1 var2 Hvar; simpl; [now auto|].
-rewrite Hvar; [|now auto]; erewrite (IHHv1 var1 var2); [|now intuition].
-erewrite (IHHv2 var1 var2); [ring|now intuition].
+rewrite Hvar; [|now auto]; erewrite (IHHv1 var1 var2).
+  + erewrite (IHHv2 var1 var2); [ring|].
+    intros; apply Hvar; zify; omega.
+  + intros; apply Hvar; zify; omega.
 Qed.
 
 End Evaluation.
 
 Section Algebra.
 
-Require Import NPeano.
-
 (* Compatibility with evaluation *)
 
 Lemma poly_add_compat : forall pl pr var, eval var (poly_add pl pr) = xorb (eval var pl) (eval var pr).
 Proof.
 intros pl; induction pl; intros pr var; simpl.
-  induction pr; simpl; auto; solve [try_rewrite; ring].
-  induction pr; simpl; auto; try solve [try_rewrite; simpl; ring].
-  destruct (nat_compare_spec n n0); repeat case_decide; simpl; first [try_rewrite; ring|idtac].
++ induction pr; simpl; auto; solve [try_rewrite; ring].
++ induction pr; simpl; auto; try solve [try_rewrite; simpl; ring].
+  destruct (Pos.compare_spec p p0); repeat case_decide; simpl; first [try_rewrite; ring|idtac].
     try_rewrite; ring_simplify; repeat rewrite xorb_assoc.
     match goal with [ |- context [xorb (andb ?b1 ?b2) (andb ?b1 ?b3)] ] =>
       replace (xorb (andb b1 b2) (andb b1 b3)) with (andb b1 (xorb b2 b3)) by ring
@@ -339,12 +362,12 @@ Lemma poly_mul_cst_compat : forall v p var,
 Proof.
 intros v p; induction p; intros var; simpl; [ring|].
 case_decide; simpl; try_rewrite; [ring_simplify|ring].
-replace (v && List.nth n var false && eval var p2) with (List.nth n var false && (v && eval var p2)) by ring.
+replace (v && list_nth p2 var false && eval var p3) with (list_nth p2 var false && (v && eval var p3)) by ring.
 rewrite <- IHp2; inversion H; simpl; ring.
 Qed.
 
 Lemma poly_mul_mon_compat : forall i p var,
-  eval var (poly_mul_mon i p) = (List.nth i var false && eval var p).
+  eval var (poly_mul_mon i p) = (list_nth i var false && eval var p).
 Proof.
 intros i p var; induction p; simpl; case_decide; simpl; try_rewrite; try ring.
 inversion H; ring.
@@ -358,50 +381,55 @@ intros pl; induction pl; intros pr var; simpl.
   apply poly_mul_cst_compat.
   case_decide; simpl.
     rewrite IHpl1; ring_simplify.
-    replace (eval var pr && List.nth n var false && eval var pl2)
-    with (List.nth n var false && (eval var pl2 && eval var pr)) by ring.
+    replace (eval var pr && list_nth p var false && eval var pl2)
+    with (list_nth p var false && (eval var pl2 && eval var pr)) by ring.
     now rewrite <- IHpl2; inversion H; simpl; ring.
     rewrite poly_add_compat, poly_mul_mon_compat, IHpl1, IHpl2; ring.
 Qed.
 
 Hint Extern 5 =>
 match goal with
-| [ |- max ?x ?y <= ?z ] =>
-  apply Nat.max_case_strong; intros; omega
-| [ |- ?z <= max ?x ?y ] =>
-  apply Nat.max_case_strong; intros; omega
+| [ |- (Pos.max ?x ?y <= ?z)%positive ] =>
+  apply Pos.max_case_strong; intros; zify; romega
+| [ |- (?z <= Pos.max ?x ?y)%positive ] =>
+  apply Pos.max_case_strong; intros; zify; romega
+| [ |- (Pos.max ?x ?y < ?z)%positive ] =>
+  apply Pos.max_case_strong; intros; zify; romega
+| [ |- (?z < Pos.max ?x ?y)%positive ] =>
+  apply Pos.max_case_strong; intros; zify; romega
+| _ => zify; omega
 end.
-Hint Resolve Nat.le_max_r Nat.le_max_l.
+Hint Resolve Pos.le_max_r Pos.le_max_l.
 
 Hint Constructors valid linear.
 
 (* Compatibility of validity w.r.t algebraic operations *)
 
 Lemma poly_add_valid_compat : forall kl kr pl pr, valid kl pl -> valid kr pr ->
-  valid (max kl kr) (poly_add pl pr).
+  valid (Pos.max kl kr) (poly_add pl pr).
 Proof.
 intros kl kr pl pr Hl Hr; revert kr pr Hr; induction Hl; intros kr pr Hr; simpl.
-  eapply valid_le_compat; [clear k|apply Nat.le_max_r].
-  now induction Hr; auto.
-  assert (Hle : max (S i) kr <= max k kr).
-    apply Nat.max_case_strong; intros; apply Nat.max_case_strong; intros; auto; omega.
-  apply (valid_le_compat (max (S i) kr)); [|assumption].
+{ eapply valid_le_compat; [clear k|apply Pos.le_max_r].
+  now induction Hr; auto. }
+{  assert (Hle : (Pos.max (Pos.succ i) kr <= Pos.max k kr)%positive) by auto.
+  apply (valid_le_compat (Pos.max (Pos.succ i) kr)); [|assumption].
   clear - IHHl1 IHHl2 Hl2 Hr H0; induction Hr.
     constructor; auto.
-      now rewrite <- (Nat.max_id i); intuition.
-    destruct (nat_compare_spec i i0); subst; try case_decide; repeat (constructor; intuition).
-      now apply (valid_le_compat (max i0 i0)); [now auto|]; rewrite Nat.max_id; auto.
-      now apply (valid_le_compat (max i0 i0)); [now auto|]; rewrite Nat.max_id; auto.
-      now apply (valid_le_compat (max (S i0) (S i0))); [now auto|]; rewrite Nat.max_id; auto.
-      now apply (valid_le_compat (max (S i) i0)); intuition.
-      now apply (valid_le_compat (max i (S i0))); intuition.
+      now rewrite <- (Pos.max_id i); intuition.
+    destruct (Pos.compare_spec i i0); subst; try case_decide; repeat (constructor; intuition).
+      + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; auto.
+      + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; zify; romega.
+      + apply (valid_le_compat (Pos.max (Pos.succ i0) (Pos.succ i0))); [now auto|]; rewrite Pos.max_id; zify; romega.
+      + apply (valid_le_compat (Pos.max (Pos.succ i) i0)); intuition.
+      + apply (valid_le_compat (Pos.max i (Pos.succ i0))); intuition.
+}
 Qed.
 
 Lemma poly_mul_cst_valid_compat : forall k v p, valid k p -> valid k (poly_mul_cst v p).
 Proof.
 intros k v p H; induction H; simpl; [now auto|].
 case_decide; [|now auto].
-eapply (valid_le_compat i); [now auto|omega].
+eapply (valid_le_compat i); [now auto|zify; romega].
 Qed.
 
 Lemma poly_mul_mon_null_compat : forall i p, null (poly_mul_mon i p) -> null p.
@@ -409,50 +437,51 @@ Proof.
 intros i p; induction p; simpl; case_decide; simpl; inversion 1; intuition.
 Qed.
 
-Lemma poly_mul_mon_valid_compat : forall k i p, valid k p -> valid (max (S i) k) (poly_mul_mon i p).
+Lemma poly_mul_mon_valid_compat : forall k i p,
+  valid k p -> valid (Pos.max (Pos.succ i) k) (poly_mul_mon i p).
 Proof.
 intros k i p H; induction H; simpl poly_mul_mon; case_decide; intuition.
-apply (valid_le_compat (S i)); auto; constructor; intuition.
-match goal with [ H : null ?p |- _ ] => solve[inversion H] end.
-apply (valid_le_compat k); auto; constructor; intuition.
-  assert (X := poly_mul_mon_null_compat); intuition eauto.
-  now cutrewrite <- (max (S i) i0 = i0); intuition.
-  now cutrewrite <- (max (S i) (S i0) = S i0); intuition.
++ apply (valid_le_compat (Pos.succ i)); auto; constructor; intuition.
+  - match goal with [ H : null ?p |- _ ] => solve[inversion H] end.
++ apply (valid_le_compat k); auto; constructor; intuition.
+  - assert (X := poly_mul_mon_null_compat); intuition eauto.
+  - cutrewrite <- (Pos.max (Pos.succ i) i0 = i0); intuition.
+  - cutrewrite <- (Pos.max (Pos.succ i) (Pos.succ i0) = Pos.succ i0); intuition.
 Qed.
 
 Lemma poly_mul_valid_compat : forall kl kr pl pr, valid kl pl -> valid kr pr ->
-  valid (max kl kr) (poly_mul pl pr).
+  valid (Pos.max kl kr) (poly_mul pl pr).
 Proof.
 intros kl kr pl pr Hl Hr; revert kr pr Hr.
 induction Hl; intros kr pr Hr; simpl.
-  apply poly_mul_cst_valid_compat; auto.
++ apply poly_mul_cst_valid_compat; auto.
   apply (valid_le_compat kr); now auto.
-  apply (valid_le_compat (max (max i kr) (max (S i) (max (S i) kr)))).
-    case_decide.
-      now apply (valid_le_compat (max i kr)); auto.
-      apply poly_add_valid_compat; auto.
-      now apply poly_mul_mon_valid_compat; intuition.
-    repeat apply Nat.max_case_strong; omega.
++ apply (valid_le_compat (Pos.max (Pos.max i kr) (Pos.max (Pos.succ i) (Pos.max (Pos.succ i) kr)))).
+  - case_decide.
+    { apply (valid_le_compat (Pos.max i kr)); auto. }
+    { apply poly_add_valid_compat; auto.
+      now apply poly_mul_mon_valid_compat; intuition. }
+  - repeat apply Pos.max_case_strong; zify; omega.
 Qed.
 
 (* Compatibility of linearity wrt to linear operations *)
 
 Lemma poly_add_linear_compat : forall kl kr pl pr, linear kl pl -> linear kr pr ->
-  linear (max kl kr) (poly_add pl pr).
+  linear (Pos.max kl kr) (poly_add pl pr).
 Proof.
 intros kl kr pl pr Hl; revert kr pr; induction Hl; intros kr pr Hr; simpl.
-  apply (linear_le_compat kr); [|apply Nat.max_case_strong; omega].
++ apply (linear_le_compat kr); [|apply Pos.max_case_strong; zify; omega].
   now induction Hr; constructor; auto.
-  apply (linear_le_compat (max kr (S i))); [|repeat apply Nat.max_case_strong; omega].
++ apply (linear_le_compat (Pos.max kr (Pos.succ i))); [|now auto].
   induction Hr; simpl.
-    constructor; auto.
-    replace i with (max i i) by (apply Nat.max_id); apply IHHl1; now constructor.
-    destruct (nat_compare_spec i i0); subst; try case_decide; repeat (constructor; intuition).
-      now apply (linear_le_compat (max i0 i0)); [now auto|]; rewrite Nat.max_id; auto.
-      now apply (linear_le_compat (max i0 i0)); [now auto|]; rewrite Nat.max_id; auto.
-      now apply (linear_le_compat (max i0 i0)); [now auto|]; rewrite Nat.max_id; auto.
-      now apply (linear_le_compat (max i0 (S i))); intuition.
-      apply (linear_le_compat (max i (S i0))); intuition.
+  - constructor; auto.
+    replace i with (Pos.max i i) by (apply Pos.max_id); intuition.
+  - destruct (Pos.compare_spec i i0); subst; try case_decide; repeat (constructor; intuition).
+    { apply (linear_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; auto. }
+    { apply (linear_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; auto. }
+    { apply (linear_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; auto. }
+    { apply (linear_le_compat (Pos.max i0 (Pos.succ i))); intuition. }
+    { apply (linear_le_compat (Pos.max i (Pos.succ i0))); intuition. }
 Qed.
 
 End Algebra.
@@ -461,27 +490,27 @@ Section Reduce.
 
 (* A stronger version of the next lemma *)
 
-Lemma reduce_aux_eval_compat : forall k p var, valid (S k) p ->
-  (List.nth k var false && eval var (reduce_aux k p) = List.nth k var false && eval var p).
+Lemma reduce_aux_eval_compat : forall k p var, valid (Pos.succ k) p ->
+  (list_nth k var false && eval var (reduce_aux k p) = list_nth k var false && eval var p).
 Proof.
 intros k p var; revert k; induction p; intros k Hv; simpl; auto.
 inversion Hv; case_decide; subst.
-  rewrite poly_add_compat; ring_simplify.
++ rewrite poly_add_compat; ring_simplify.
   specialize (IHp1 k); specialize (IHp2 k).
-  destruct (List.nth k var false); ring_simplify; [|now auto].
-  rewrite <- (andb_true_l (eval var p1)), <- (andb_true_l (eval var p2)).
+  destruct (list_nth k var false); ring_simplify; [|now auto].
+  rewrite <- (andb_true_l (eval var p1)), <- (andb_true_l (eval var p3)).
   rewrite <- IHp2; auto; rewrite <- IHp1; [ring|].
-  apply (valid_le_compat k); now auto.
-  remember (List.nth k var false) as b; destruct b; ring_simplify; [|now auto].
+  apply (valid_le_compat k); [now auto|zify; omega].
++ remember (list_nth k var false) as b; destruct b; ring_simplify; [|now auto].
   case_decide; simpl.
-    rewrite <- (IHp2 n); [inversion H|now auto]; simpl.
-    replace (eval var p1) with (List.nth k var false && eval var p1) by (rewrite <- Heqb; ring); rewrite <- (IHp1 k).
-      rewrite <- Heqb; ring.
-      now apply (valid_le_compat n); [auto|omega].
-    rewrite (IHp2 n); [|now auto].
-    replace (eval var p1) with (List.nth k var false && eval var p1) by (rewrite <- Heqb; ring).
+  - rewrite <- (IHp2 p2); [inversion H|now auto]; simpl.
+    replace (eval var p1) with (list_nth k var false && eval var p1) by (rewrite <- Heqb; ring); rewrite <- (IHp1 k).
+    { rewrite <- Heqb; ring. }
+    { apply (valid_le_compat p2); [auto|zify; omega]. }
+  - rewrite (IHp2 p2); [|now auto].
+    replace (eval var p1) with (list_nth k var false && eval var p1) by (rewrite <- Heqb; ring).
     rewrite <- (IHp1 k); [rewrite <- Heqb; ring|].
-    apply (valid_le_compat n); [auto|omega].
+    apply (valid_le_compat p2); [auto|zify; omega].
 Qed.
 
 (* Reduction preserves evaluation by boolean assignations *)
@@ -491,44 +520,44 @@ Lemma reduce_eval_compat : forall k p var, valid k p ->
 Proof.
 intros k p var H; induction H; simpl; auto.
 case_decide; try_rewrite; simpl.
-  rewrite <- reduce_aux_eval_compat; auto; inversion H3; simpl; ring.
-  repeat rewrite reduce_aux_eval_compat; try_rewrite; now auto.
++ rewrite <- reduce_aux_eval_compat; auto; inversion H3; simpl; ring.
++ repeat rewrite reduce_aux_eval_compat; try_rewrite; now auto.
 Qed.
 
-Lemma reduce_aux_le_compat : forall k l p, valid k p -> k <= l ->
+Lemma reduce_aux_le_compat : forall k l p, valid k p -> (k <= l)%positive ->
   reduce_aux l p = reduce_aux k p.
 Proof.
 intros k l p; revert k l; induction p; intros k l H Hle; simpl; auto.
-  inversion H; subst; repeat case_decide; subst; try (exfalso; omega).
-    now apply IHp1; [|now auto]; eapply valid_le_compat; [eauto|omega].
-    f_equal; apply IHp1; auto.
-    now eapply valid_le_compat; [eauto|omega].
+inversion H; subst; repeat case_decide; subst; try (exfalso; zify; omega).
++ apply IHp1; [|now auto]; eapply valid_le_compat; [eauto|zify; omega].
++ f_equal; apply IHp1; auto.
+  now eapply valid_le_compat; [eauto|zify; omega].
 Qed.
 
 (* Reduce projects valid polynomials into linear ones *)
 
-Lemma linear_reduce_aux : forall i p, valid (S i) p -> linear i (reduce_aux i p).
+Lemma linear_reduce_aux : forall i p, valid (Pos.succ i) p -> linear i (reduce_aux i p).
 Proof.
 intros i p; revert i; induction p; intros i Hp; simpl.
-  constructor.
-  inversion Hp; subst; case_decide; subst.
-    rewrite <- (Nat.max_id i) at 1; apply poly_add_linear_compat.
-      apply IHp1; eapply valid_le_compat; eauto.
-      now intuition.
-  case_decide.
-    apply IHp1; eapply valid_le_compat; [eauto|omega].
-    constructor; try omega; auto.
-    erewrite (reduce_aux_le_compat n); [|assumption|omega].
-    now apply IHp1; eapply valid_le_compat; eauto.
++ constructor.
++ inversion Hp; subst; case_decide; subst.
+  - rewrite <- (Pos.max_id i) at 1; apply poly_add_linear_compat.
+    { apply IHp1; eapply valid_le_compat; [eassumption|zify; omega]. }
+    { intuition. }
+  - case_decide.
+  { apply IHp1; eapply valid_le_compat; [eauto|zify; omega]. }
+  { constructor; try (zify; omega); auto.
+    erewrite (reduce_aux_le_compat p2); [|assumption|zify; omega].
+    apply IHp1; eapply valid_le_compat; [eauto|]; zify; omega. }
 Qed.
 
 Lemma linear_reduce : forall k p, valid k p -> linear k (reduce p).
 Proof.
 intros k p H; induction H; simpl.
-  now constructor.
-  case_decide.
-    eapply linear_le_compat; [eauto|omega].
-    constructor; auto.
++ now constructor.
++ case_decide.
+  - eapply linear_le_compat; [eauto|zify; omega].
+  - constructor; auto.
     apply linear_reduce_aux; auto.
 Qed.
 
diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v
index 1327e5e2f..e31948ffe 100644
--- a/plugins/btauto/Reflect.v
+++ b/plugins/btauto/Reflect.v
@@ -1,11 +1,11 @@
-Require Import Bool DecidableClass Algebra Ring NPeano.
+Require Import Bool DecidableClass Algebra Ring PArith ROmega.
 
 Section Bool.
 
 (* Boolean formulas and their evaluations *)
 
 Inductive formula :=
-| formula_var : nat -> formula
+| formula_var : positive -> formula
 | formula_btm : formula
 | formula_top : formula
 | formula_cnj : formula -> formula -> formula
@@ -15,7 +15,7 @@ Inductive formula :=
 | formula_ifb : formula -> formula -> formula -> formula.
 
 Fixpoint formula_eval var f := match f with
-| formula_var x => List.nth x var false 
+| formula_var x => list_nth x var false 
 | formula_btm => false
 | formula_top => true
 | formula_cnj fl fr => (formula_eval var fl) && (formula_eval var fr)
@@ -80,20 +80,21 @@ Qed.
 Hint Extern 5 => change 0 with (min 0 0).
 Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat.
 Local Hint Constructors valid.
+Hint Extern 5 => zify; omega.
 
 (* Compatibility with validity *)
 
 Lemma poly_of_formula_valid_compat : forall f, exists n, valid n (poly_of_formula f).
 Proof.
 intros f; induction f; simpl.
-  now exists (S n); constructor; intuition; inversion H.
-  now exists 0; auto.
-  now exists 0; auto.
-  now destruct IHf1 as [n1 Hn1]; destruct IHf2 as [n2 Hn2]; exists (max n1 n2); auto.
-  now destruct IHf1 as [n1 Hn1]; destruct IHf2 as [n2 Hn2]; exists (max (max n1 n2) (max n1 n2)); auto.
-  now destruct IHf as [n Hn]; exists (max 0 n); auto.
-  now destruct IHf1 as [n1 Hn1]; destruct IHf2 as [n2 Hn2]; exists (max n1 n2); auto.
-  destruct IHf1 as [n1 Hn1]; destruct IHf2 as [n2 Hn2]; destruct IHf3 as [n3 Hn3]; eexists; eauto.
++ exists (Pos.succ p); constructor; intuition; inversion H.
++ exists 1%positive; auto.
++ exists 1%positive; auto.
++ destruct IHf1 as [n1 Hn1]; destruct IHf2 as [n2 Hn2]; exists (Pos.max n1 n2); auto.
++ destruct IHf1 as [n1 Hn1]; destruct IHf2 as [n2 Hn2]; exists (Pos.max (Pos.max n1 n2) (Pos.max n1 n2)); auto.
++ destruct IHf as [n Hn]; exists (Pos.max 1 n); auto.
++ destruct IHf1 as [n1 Hn1]; destruct IHf2 as [n2 Hn2]; exists (Pos.max n1 n2); auto.
++ destruct IHf1 as [n1 Hn1]; destruct IHf2 as [n2 Hn2]; destruct IHf3 as [n3 Hn3]; eexists; eauto.
 Qed.
 
 (* The soundness lemma ; alas not complete! *)
@@ -138,11 +139,10 @@ rewrite <- (reduce_eval_compat nr (poly_of_formula fr)); auto.
 rewrite Heq; reflexivity.
 Qed.
 
-Fixpoint make_last {A} n (x def : A) :=
-match n with
-| 0 => cons x nil
-| S n => cons def (make_last n x def)
-end.
+Definition make_last {A} n (x def : A) :=
+  Pos.peano_rect (fun _ => list A)
+    (cons x nil)
+    (fun _ F => cons def F) n.
 
 (* Replace the nth element of a list *)
 
@@ -150,10 +150,8 @@ Fixpoint list_replace l n b :=
 match l with
 | nil => make_last n b false
 | cons a l =>
-  match n with
-  | 0 => cons b l
-  | S n => cons a (list_replace l n b)
-  end
+  Pos.peano_rect _
+    (cons b l) (fun n _ => cons a (list_replace l n b)) n
 end.
 
 (** Extract a non-null witness from a polynomial *)
@@ -172,32 +170,72 @@ match p with
     list_replace var i false
 end.
 
+Lemma list_nth_base : forall A (def : A) l,
+  list_nth 1 l def = match l with nil => def | cons x _ => x end.
+Proof.
+intros A def l; unfold list_nth.
+rewrite Pos.peano_rect_base; reflexivity.
+Qed.
+
+Lemma list_nth_succ : forall A n (def : A) l,
+  list_nth (Pos.succ n) l def =
+    match l with nil => def | cons _ l => list_nth n l def end.
+Proof.
+intros A def l; unfold list_nth.
+rewrite Pos.peano_rect_succ; reflexivity.
+Qed.
+
+Lemma list_nth_nil : forall A n (def : A),
+  list_nth n nil def = def.
+Proof.
+intros A n def; induction n using Pos.peano_rect.
++ rewrite list_nth_base; reflexivity.
++ rewrite list_nth_succ; reflexivity.
+Qed.
+
 Lemma make_last_nth_1 : forall A n i x def, i <> n ->
-  List.nth i (@make_last A n x def) def = def.
+  list_nth i (@make_last A n x def) def = def.
 Proof.
-intros A n; induction n; intros i x def Hd; simpl.
-  destruct i; [exfalso; omega|now destruct i; auto].
-  destruct i; intuition.
+intros A n; induction n using Pos.peano_rect; intros i x def Hd; simpl.
++ unfold make_last; rewrite Pos.peano_rect_base.
+  induction i using Pos.peano_case; [elim Hd; reflexivity|].
+  rewrite list_nth_succ, list_nth_nil; reflexivity.
++ unfold make_last; rewrite Pos.peano_rect_succ; fold (make_last n x def).
+  induction i using Pos.peano_case.
+  - rewrite list_nth_base; reflexivity.
+  - rewrite list_nth_succ; apply IHn; zify; omega.
 Qed.
 
-Lemma make_last_nth_2 : forall A n x def, List.nth n (@make_last A n x def) def = x.
+Lemma make_last_nth_2 : forall A n x def, list_nth n (@make_last A n x def) def = x.
 Proof.
-intros A n; induction n; intros x def; simpl; auto.
+intros A n; induction n using Pos.peano_rect; intros x def; simpl.
++ reflexivity.
++ unfold make_last; rewrite Pos.peano_rect_succ; fold (make_last n x def).
+  rewrite list_nth_succ; auto.
 Qed.
 
 Lemma list_replace_nth_1 : forall var i j x, i <> j ->
-  List.nth i (list_replace var j x) false = List.nth i var false.
+  list_nth i (list_replace var j x) false = list_nth i var false.
 Proof.
 intros var; induction var; intros i j x Hd; simpl.
-  rewrite make_last_nth_1; [destruct i; reflexivity|assumption].
-  destruct i; destruct j; simpl; solve [auto|congruence].
++ rewrite make_last_nth_1, list_nth_nil; auto.
++ induction j using Pos.peano_rect.
+  - rewrite Pos.peano_rect_base.
+    induction i using Pos.peano_rect; [now elim Hd; auto|].
+    rewrite 2list_nth_succ; reflexivity.
+  - rewrite Pos.peano_rect_succ.
+    induction i using Pos.peano_rect.
+    { rewrite 2list_nth_base; reflexivity. }
+    { rewrite 2list_nth_succ; apply IHvar; zify; omega. }
 Qed.
 
-Lemma list_replace_nth_2 : forall var i x, List.nth i (list_replace var i x) false = x.
+Lemma list_replace_nth_2 : forall var i x, list_nth i (list_replace var i x) false = x.
 Proof.
 intros var; induction var; intros i x; simpl.
-  now apply make_last_nth_2.
-  now destruct i; simpl in *; [reflexivity|auto].
++ now apply make_last_nth_2.
++ induction i using Pos.peano_rect.
+  - rewrite Pos.peano_rect_base, list_nth_base; reflexivity.
+  - rewrite Pos.peano_rect_succ, list_nth_succ; auto.
 Qed.
 
 (* The witness is correct only if the polynomial is linear *)
@@ -213,10 +251,10 @@ intros k p Hl Hp; induction Hl; simpl.
       assert (Hrw : b = true); [|rewrite Hrw; reflexivity]
     end.
     erewrite eval_suffix_compat; [now eauto| |now apply linear_valid_incl; eauto].
-    now intros j Hd; apply list_replace_nth_1; omega.
+    now intros j Hd; apply list_replace_nth_1; zify; omega.
     rewrite list_replace_nth_2, xorb_false_r.
     erewrite eval_suffix_compat; [now eauto| |now apply linear_valid_incl; eauto].
-    now intros j Hd; apply list_replace_nth_1; omega.
+    now intros j Hd; apply list_replace_nth_1; zify; omega.
 Qed.
 
 (* This should be better when using the [vm_compute] tactic instead of plain reflexivity. *)
@@ -235,7 +273,7 @@ rewrite <- xorb_false_l; change false with (eval var (Cst false)).
 rewrite <- poly_add_compat, <- Heq.
 repeat rewrite poly_add_compat.
 rewrite (reduce_eval_compat nl); [|assumption].
-rewrite (reduce_eval_compat (max nl nr)); [|apply poly_add_valid_compat; assumption].
+rewrite (reduce_eval_compat (Pos.max nl nr)); [|apply poly_add_valid_compat; assumption].
 rewrite (reduce_eval_compat nr); [|assumption].
 rewrite poly_add_compat; ring.
 Qed.
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 0f89f348e..caa6eac2e 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -34,18 +34,20 @@ module CoqList = struct
 
 end
 
-module CoqNat = struct
-  let path = ["Init"; "Datatypes"]
-  let typ = get_constant path "nat"
-  let _S = get_constant path "S"
-  let _O = get_constant path "O"
+module CoqPositive = struct
+  let path = ["Numbers"; "BinNums"]
+  let typ = get_constant path "positive"
+  let _xH = get_constant path "xH"
+  let _xO = get_constant path "xO"
+  let _xI = get_constant path "xI"
 
   (* A coq nat from an int *)
   let rec of_int n =
-    if n <= 0 then Lazy.force _O
+    if n <= 1 then Lazy.force _xH
     else
-      let ans = of_int (pred n) in
-      lapp _S [|ans|]
+      let ans = of_int (n / 2) in
+      if n mod 2 = 0 then lapp _xO [|ans|]
+      else lapp _xI [|ans|]
 
 end
 
@@ -70,7 +72,7 @@ module Env = struct
       let () = incr off in
       i
 
-  let empty () = (ConstrHashtbl.create 16, ref 0)
+  let empty () = (ConstrHashtbl.create 16, ref 1)
 
   let to_list (env, _) =
     (* we need to get an ordered list *)
@@ -159,7 +161,7 @@ module Btauto = struct
   let soundness = get_constant ["btauto"; "Reflect"] "reduce_poly_of_formula_sound_alt"
 
   let rec convert = function
-  | Bool.Var n -> lapp f_var [|CoqNat.of_int n|]
+  | Bool.Var n -> lapp f_var [|CoqPositive.of_int n|]
   | Bool.Const true -> Lazy.force f_top
   | Bool.Const false -> Lazy.force f_btm
   | Bool.Andb (b1, b2) -> lapp f_cnj [|convert b1; convert b2|]