From 2a167c9a7796939982fa79b4f5adfc7842c97d0e Mon Sep 17 00:00:00 2001 From: ppedrot Date: Thu, 28 Jun 2012 15:08:52 +0000 Subject: 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 --- plugins/btauto/Algebra.v | 259 ++++++++++++++++++++++++++--------------------- 1 file changed, 144 insertions(+), 115 deletions(-) (limited to 'plugins/btauto/Algebra.v') 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. -- cgit v1.2.3