summaryrefslogtreecommitdiff
path: root/plugins/omega
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/omega')
-rw-r--r--plugins/omega/Omega.v59
-rw-r--r--plugins/omega/OmegaLemmas.v302
-rw-r--r--plugins/omega/OmegaPlugin.v11
-rw-r--r--plugins/omega/PreOmega.v445
-rw-r--r--plugins/omega/coq_omega.ml1823
-rw-r--r--plugins/omega/g_omega.ml447
-rw-r--r--plugins/omega/omega.ml716
-rw-r--r--plugins/omega/omega_plugin.mllib4
-rw-r--r--plugins/omega/vo.itarget4
9 files changed, 3411 insertions, 0 deletions
diff --git a/plugins/omega/Omega.v b/plugins/omega/Omega.v
new file mode 100644
index 00000000..30b94571
--- /dev/null
+++ b/plugins/omega/Omega.v
@@ -0,0 +1,59 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(**************************************************************************)
+(* *)
+(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *)
+(* *)
+(* Pierre Crégut (CNET, Lannion, France) *)
+(* *)
+(**************************************************************************)
+
+(* $Id$ *)
+
+(* We do not require [ZArith] anymore, but only what's necessary for Omega *)
+Require Export ZArith_base.
+Require Export OmegaLemmas.
+Require Export PreOmega.
+Declare ML Module "omega_plugin".
+
+Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l
+ Zplus_0_r Zmult_1_l Zplus_opp_l Zplus_opp_r Zmult_plus_distr_l
+ Zmult_plus_distr_r: zarith.
+
+Require Export Zhints.
+
+(*
+(* The constant minus is required in coq_omega.ml *)
+Require Minus.
+*)
+
+Hint Extern 10 (_ = _ :>nat) => abstract omega: zarith.
+Hint Extern 10 (_ <= _) => abstract omega: zarith.
+Hint Extern 10 (_ < _) => abstract omega: zarith.
+Hint Extern 10 (_ >= _) => abstract omega: zarith.
+Hint Extern 10 (_ > _) => abstract omega: zarith.
+
+Hint Extern 10 (_ <> _ :>nat) => abstract omega: zarith.
+Hint Extern 10 (~ _ <= _) => abstract omega: zarith.
+Hint Extern 10 (~ _ < _) => abstract omega: zarith.
+Hint Extern 10 (~ _ >= _) => abstract omega: zarith.
+Hint Extern 10 (~ _ > _) => abstract omega: zarith.
+
+Hint Extern 10 (_ = _ :>Z) => abstract omega: zarith.
+Hint Extern 10 (_ <= _)%Z => abstract omega: zarith.
+Hint Extern 10 (_ < _)%Z => abstract omega: zarith.
+Hint Extern 10 (_ >= _)%Z => abstract omega: zarith.
+Hint Extern 10 (_ > _)%Z => abstract omega: zarith.
+
+Hint Extern 10 (_ <> _ :>Z) => abstract omega: zarith.
+Hint Extern 10 (~ (_ <= _)%Z) => abstract omega: zarith.
+Hint Extern 10 (~ (_ < _)%Z) => abstract omega: zarith.
+Hint Extern 10 (~ (_ >= _)%Z) => abstract omega: zarith.
+Hint Extern 10 (~ (_ > _)%Z) => abstract omega: zarith.
+
+Hint Extern 10 False => abstract omega: zarith. \ No newline at end of file
diff --git a/plugins/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v
new file mode 100644
index 00000000..56a854d6
--- /dev/null
+++ b/plugins/omega/OmegaLemmas.v
@@ -0,0 +1,302 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+Require Import ZArith_base.
+Open Local Scope Z_scope.
+
+(** Factorization lemmas *)
+
+Theorem Zred_factor0 : forall n:Z, n = n * 1.
+ intro x; rewrite (Zmult_1_r x); reflexivity.
+Qed.
+
+Theorem Zred_factor1 : forall n:Z, n + n = n * 2.
+Proof.
+ exact Zplus_diag_eq_mult_2.
+Qed.
+
+Theorem Zred_factor2 : forall n m:Z, n + n * m = n * (1 + m).
+Proof.
+ intros x y; pattern x at 1 in |- *; rewrite <- (Zmult_1_r x);
+ rewrite <- Zmult_plus_distr_r; trivial with arith.
+Qed.
+
+Theorem Zred_factor3 : forall n m:Z, n * m + n = n * (1 + m).
+Proof.
+ intros x y; pattern x at 2 in |- *; rewrite <- (Zmult_1_r x);
+ rewrite <- Zmult_plus_distr_r; rewrite Zplus_comm;
+ trivial with arith.
+Qed.
+
+Theorem Zred_factor4 : forall n m p:Z, n * m + n * p = n * (m + p).
+Proof.
+ intros x y z; symmetry in |- *; apply Zmult_plus_distr_r.
+Qed.
+
+Theorem Zred_factor5 : forall n m:Z, n * 0 + m = m.
+Proof.
+ intros x y; rewrite <- Zmult_0_r_reverse; auto with arith.
+Qed.
+
+Theorem Zred_factor6 : forall n:Z, n = n + 0.
+Proof.
+ intro; rewrite Zplus_0_r; trivial with arith.
+Qed.
+
+(** Other specific variants of theorems dedicated for the Omega tactic *)
+
+Lemma new_var : forall x : Z, exists y : Z, x = y.
+intros x; exists x; trivial with arith.
+Qed.
+
+Lemma OMEGA1 : forall x y : Z, x = y -> 0 <= x -> 0 <= y.
+intros x y H; rewrite H; auto with arith.
+Qed.
+
+Lemma OMEGA2 : forall x y : Z, 0 <= x -> 0 <= y -> 0 <= x + y.
+exact Zplus_le_0_compat.
+Qed.
+
+Lemma OMEGA3 : forall x y k : Z, k > 0 -> x = y * k -> x = 0 -> y = 0.
+
+intros x y k H1 H2 H3; apply (Zmult_integral_l k);
+ [ unfold not in |- *; intros H4; absurd (k > 0);
+ [ rewrite H4; unfold Zgt in |- *; simpl in |- *; discriminate
+ | assumption ]
+ | rewrite <- H2; assumption ].
+Qed.
+
+Lemma OMEGA4 : forall x y z : Z, x > 0 -> y > x -> z * y + x <> 0.
+
+unfold not in |- *; intros x y z H1 H2 H3; cut (y > 0);
+ [ intros H4; cut (0 <= z * y + x);
+ [ intros H5; generalize (Zmult_le_approx y z x H4 H2 H5); intros H6;
+ absurd (z * y + x > 0);
+ [ rewrite H3; unfold Zgt in |- *; simpl in |- *; discriminate
+ | apply Zle_gt_trans with x;
+ [ pattern x at 1 in |- *; rewrite <- (Zplus_0_l x);
+ apply Zplus_le_compat_r; rewrite Zmult_comm;
+ generalize H4; unfold Zgt in |- *; case y;
+ [ simpl in |- *; intros H7; discriminate H7
+ | intros p H7; rewrite <- (Zmult_0_r (Zpos p));
+ unfold Zle in |- *; rewrite Zcompare_mult_compat;
+ exact H6
+ | simpl in |- *; intros p H7; discriminate H7 ]
+ | assumption ] ]
+ | rewrite H3; unfold Zle in |- *; simpl in |- *; discriminate ]
+ | apply Zgt_trans with x; [ assumption | assumption ] ].
+Qed.
+
+Lemma OMEGA5 : forall x y z : Z, x = 0 -> y = 0 -> x + y * z = 0.
+
+intros x y z H1 H2; rewrite H1; rewrite H2; simpl in |- *; trivial with arith.
+Qed.
+
+Lemma OMEGA6 : forall x y z : Z, 0 <= x -> y = 0 -> 0 <= x + y * z.
+
+intros x y z H1 H2; rewrite H2; simpl in |- *; rewrite Zplus_0_r; assumption.
+Qed.
+
+Lemma OMEGA7 :
+ forall x y z t : Z, z > 0 -> t > 0 -> 0 <= x -> 0 <= y -> 0 <= x * z + y * t.
+
+intros x y z t H1 H2 H3 H4; rewrite <- (Zplus_0_l 0); apply Zplus_le_compat;
+ apply Zmult_gt_0_le_0_compat; assumption.
+Qed.
+
+Lemma OMEGA8 : forall x y : Z, 0 <= x -> 0 <= y -> x = - y -> x = 0.
+
+intros x y H1 H2 H3; elim (Zle_lt_or_eq 0 x H1);
+ [ intros H4; absurd (0 < x);
+ [ change (0 >= x) in |- *; apply Zle_ge; apply Zplus_le_reg_l with y;
+ rewrite H3; rewrite Zplus_opp_r; rewrite Zplus_0_r;
+ assumption
+ | assumption ]
+ | intros H4; rewrite H4; trivial with arith ].
+Qed.
+
+Lemma OMEGA9 : forall x y z t : Z, y = 0 -> x = z -> y + (- x + z) * t = 0.
+
+intros x y z t H1 H2; rewrite H2; rewrite Zplus_opp_l; rewrite Zmult_0_l;
+ rewrite Zplus_0_r; assumption.
+Qed.
+
+Lemma OMEGA10 :
+ forall v c1 c2 l1 l2 k1 k2 : Z,
+ (v * c1 + l1) * k1 + (v * c2 + l2) * k2 =
+ v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2).
+
+intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
+ repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
+ rewrite (Zplus_permute (l1 * k1) (v * c2 * k2)); trivial with arith.
+Qed.
+
+Lemma OMEGA11 :
+ forall v1 c1 l1 l2 k1 : Z,
+ (v1 * c1 + l1) * k1 + l2 = v1 * (c1 * k1) + (l1 * k1 + l2).
+
+intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
+ repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
+ trivial with arith.
+Qed.
+
+Lemma OMEGA12 :
+ forall v2 c2 l1 l2 k2 : Z,
+ l1 + (v2 * c2 + l2) * k2 = v2 * (c2 * k2) + (l1 + l2 * k2).
+
+intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
+ repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
+ rewrite Zplus_permute; trivial with arith.
+Qed.
+
+Lemma OMEGA13 :
+ forall (v l1 l2 : Z) (x : positive),
+ v * Zpos x + l1 + (v * Zneg x + l2) = l1 + l2.
+
+intros; rewrite Zplus_assoc; rewrite (Zplus_comm (v * Zpos x) l1);
+ rewrite (Zplus_assoc_reverse l1); rewrite <- Zmult_plus_distr_r;
+ rewrite <- Zopp_neg; rewrite (Zplus_comm (- Zneg x) (Zneg x));
+ rewrite Zplus_opp_r; rewrite Zmult_0_r; rewrite Zplus_0_r;
+ trivial with arith.
+Qed.
+
+Lemma OMEGA14 :
+ forall (v l1 l2 : Z) (x : positive),
+ v * Zneg x + l1 + (v * Zpos x + l2) = l1 + l2.
+
+intros; rewrite Zplus_assoc; rewrite (Zplus_comm (v * Zneg x) l1);
+ rewrite (Zplus_assoc_reverse l1); rewrite <- Zmult_plus_distr_r;
+ rewrite <- Zopp_neg; rewrite Zplus_opp_r; rewrite Zmult_0_r;
+ rewrite Zplus_0_r; trivial with arith.
+Qed.
+Lemma OMEGA15 :
+ forall v c1 c2 l1 l2 k2 : Z,
+ v * c1 + l1 + (v * c2 + l2) * k2 = v * (c1 + c2 * k2) + (l1 + l2 * k2).
+
+intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
+ repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
+ rewrite (Zplus_permute l1 (v * c2 * k2)); trivial with arith.
+Qed.
+
+Lemma OMEGA16 : forall v c l k : Z, (v * c + l) * k = v * (c * k) + l * k.
+
+intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
+ repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
+ trivial with arith.
+Qed.
+
+Lemma OMEGA17 : forall x y z : Z, Zne x 0 -> y = 0 -> Zne (x + y * z) 0.
+
+unfold Zne, not in |- *; intros x y z H1 H2 H3; apply H1;
+ apply Zplus_reg_l with (y * z); rewrite Zplus_comm;
+ rewrite H3; rewrite H2; auto with arith.
+Qed.
+
+Lemma OMEGA18 : forall x y k : Z, x = y * k -> Zne x 0 -> Zne y 0.
+
+unfold Zne, not in |- *; intros x y k H1 H2 H3; apply H2; rewrite H1;
+ rewrite H3; auto with arith.
+Qed.
+
+Lemma OMEGA19 : forall x : Z, Zne x 0 -> 0 <= x + -1 \/ 0 <= x * -1 + -1.
+
+unfold Zne in |- *; intros x H; elim (Zle_or_lt 0 x);
+ [ intros H1; elim Zle_lt_or_eq with (1 := H1);
+ [ intros H2; left; change (0 <= Zpred x) in |- *; apply Zsucc_le_reg;
+ rewrite <- Zsucc_pred; apply Zlt_le_succ; assumption
+ | intros H2; absurd (x = 0); auto with arith ]
+ | intros H1; right; rewrite <- Zopp_eq_mult_neg_1; rewrite Zplus_comm;
+ apply Zle_left; apply Zsucc_le_reg; simpl in |- *;
+ apply Zlt_le_succ; auto with arith ].
+Qed.
+
+Lemma OMEGA20 : forall x y z : Z, Zne x 0 -> y = 0 -> Zne (x + y * z) 0.
+
+unfold Zne, not in |- *; intros x y z H1 H2 H3; apply H1; rewrite H2 in H3;
+ simpl in H3; rewrite Zplus_0_r in H3; trivial with arith.
+Qed.
+
+Definition fast_Zplus_comm (x y : Z) (P : Z -> Prop)
+ (H : P (y + x)) := eq_ind_r P H (Zplus_comm x y).
+
+Definition fast_Zplus_assoc_reverse (n m p : Z) (P : Z -> Prop)
+ (H : P (n + (m + p))) := eq_ind_r P H (Zplus_assoc_reverse n m p).
+
+Definition fast_Zplus_assoc (n m p : Z) (P : Z -> Prop)
+ (H : P (n + m + p)) := eq_ind_r P H (Zplus_assoc n m p).
+
+Definition fast_Zplus_permute (n m p : Z) (P : Z -> Prop)
+ (H : P (m + (n + p))) := eq_ind_r P H (Zplus_permute n m p).
+
+Definition fast_OMEGA10 (v c1 c2 l1 l2 k1 k2 : Z) (P : Z -> Prop)
+ (H : P (v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2))) :=
+ eq_ind_r P H (OMEGA10 v c1 c2 l1 l2 k1 k2).
+
+Definition fast_OMEGA11 (v1 c1 l1 l2 k1 : Z) (P : Z -> Prop)
+ (H : P (v1 * (c1 * k1) + (l1 * k1 + l2))) :=
+ eq_ind_r P H (OMEGA11 v1 c1 l1 l2 k1).
+Definition fast_OMEGA12 (v2 c2 l1 l2 k2 : Z) (P : Z -> Prop)
+ (H : P (v2 * (c2 * k2) + (l1 + l2 * k2))) :=
+ eq_ind_r P H (OMEGA12 v2 c2 l1 l2 k2).
+
+Definition fast_OMEGA15 (v c1 c2 l1 l2 k2 : Z) (P : Z -> Prop)
+ (H : P (v * (c1 + c2 * k2) + (l1 + l2 * k2))) :=
+ eq_ind_r P H (OMEGA15 v c1 c2 l1 l2 k2).
+Definition fast_OMEGA16 (v c l k : Z) (P : Z -> Prop)
+ (H : P (v * (c * k) + l * k)) := eq_ind_r P H (OMEGA16 v c l k).
+
+Definition fast_OMEGA13 (v l1 l2 : Z) (x : positive) (P : Z -> Prop)
+ (H : P (l1 + l2)) := eq_ind_r P H (OMEGA13 v l1 l2 x).
+
+Definition fast_OMEGA14 (v l1 l2 : Z) (x : positive) (P : Z -> Prop)
+ (H : P (l1 + l2)) := eq_ind_r P H (OMEGA14 v l1 l2 x).
+Definition fast_Zred_factor0 (x : Z) (P : Z -> Prop)
+ (H : P (x * 1)) := eq_ind_r P H (Zred_factor0 x).
+
+Definition fast_Zopp_eq_mult_neg_1 (x : Z) (P : Z -> Prop)
+ (H : P (x * -1)) := eq_ind_r P H (Zopp_eq_mult_neg_1 x).
+
+Definition fast_Zmult_comm (x y : Z) (P : Z -> Prop)
+ (H : P (y * x)) := eq_ind_r P H (Zmult_comm x y).
+
+Definition fast_Zopp_plus_distr (x y : Z) (P : Z -> Prop)
+ (H : P (- x + - y)) := eq_ind_r P H (Zopp_plus_distr x y).
+
+Definition fast_Zopp_involutive (x : Z) (P : Z -> Prop) (H : P x) :=
+ eq_ind_r P H (Zopp_involutive x).
+
+Definition fast_Zopp_mult_distr_r (x y : Z) (P : Z -> Prop)
+ (H : P (x * - y)) := eq_ind_r P H (Zopp_mult_distr_r x y).
+
+Definition fast_Zmult_plus_distr_l (n m p : Z) (P : Z -> Prop)
+ (H : P (n * p + m * p)) := eq_ind_r P H (Zmult_plus_distr_l n m p).
+Definition fast_Zmult_opp_comm (x y : Z) (P : Z -> Prop)
+ (H : P (x * - y)) := eq_ind_r P H (Zmult_opp_comm x y).
+
+Definition fast_Zmult_assoc_reverse (n m p : Z) (P : Z -> Prop)
+ (H : P (n * (m * p))) := eq_ind_r P H (Zmult_assoc_reverse n m p).
+
+Definition fast_Zred_factor1 (x : Z) (P : Z -> Prop)
+ (H : P (x * 2)) := eq_ind_r P H (Zred_factor1 x).
+
+Definition fast_Zred_factor2 (x y : Z) (P : Z -> Prop)
+ (H : P (x * (1 + y))) := eq_ind_r P H (Zred_factor2 x y).
+
+Definition fast_Zred_factor3 (x y : Z) (P : Z -> Prop)
+ (H : P (x * (1 + y))) := eq_ind_r P H (Zred_factor3 x y).
+
+Definition fast_Zred_factor4 (x y z : Z) (P : Z -> Prop)
+ (H : P (x * (y + z))) := eq_ind_r P H (Zred_factor4 x y z).
+
+Definition fast_Zred_factor5 (x y : Z) (P : Z -> Prop)
+ (H : P y) := eq_ind_r P H (Zred_factor5 x y).
+
+Definition fast_Zred_factor6 (x : Z) (P : Z -> Prop)
+ (H : P (x + 0)) := eq_ind_r P H (Zred_factor6 x).
diff --git a/plugins/omega/OmegaPlugin.v b/plugins/omega/OmegaPlugin.v
new file mode 100644
index 00000000..21535f0d
--- /dev/null
+++ b/plugins/omega/OmegaPlugin.v
@@ -0,0 +1,11 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id$ *)
+
+Declare ML Module "omega_plugin".
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
new file mode 100644
index 00000000..a5a085a9
--- /dev/null
+++ b/plugins/omega/PreOmega.v
@@ -0,0 +1,445 @@
+Require Import Arith Max Min ZArith_base NArith Nnat.
+
+Open Local Scope Z_scope.
+
+
+(** * zify: the Z-ification tactic *)
+
+(* This tactic searches for nat and N and positive elements in the goal and
+ translates everything into Z. It is meant as a pre-processor for
+ (r)omega; for instance a positivity hypothesis is added whenever
+ - a multiplication is encountered
+ - an atom is encountered (that is a variable or an unknown construct)
+
+ Recognized relations (can be handled as deeply as allowed by setoid rewrite):
+ - { eq, le, lt, ge, gt } on { Z, positive, N, nat }
+
+ Recognized operations:
+ - on Z: Zmin, Zmax, Zabs, Zsgn are translated in term of <= < =
+ - on nat: + * - S O pred min max nat_of_P nat_of_N Zabs_nat
+ - on positive: Zneg Zpos xI xO xH + * - Psucc Ppred Pmin Pmax P_of_succ_nat
+ - on N: N0 Npos + * - Nsucc Nmin Nmax N_of_nat Zabs_N
+*)
+
+
+
+
+(** I) translation of Zmax, Zmin, Zabs, Zsgn into recognized equations *)
+
+Ltac zify_unop_core t thm a :=
+ (* Let's introduce the specification theorem for t *)
+ let H:= fresh "H" in assert (H:=thm a);
+ (* Then we replace (t a) everywhere with a fresh variable *)
+ let z := fresh "z" in set (z:=t a) in *; clearbody z.
+
+Ltac zify_unop_var_or_term t thm a :=
+ (* If a is a variable, no need for aliasing *)
+ let za := fresh "z" in
+ (rename a into za; rename za into a; zify_unop_core t thm a) ||
+ (* Otherwise, a is a complex term: we alias it. *)
+ (remember a as za; zify_unop_core t thm za).
+
+Ltac zify_unop t thm a :=
+ (* if a is a scalar, we can simply reduce the unop *)
+ let isz := isZcst a in
+ match isz with
+ | true => simpl (t a) in *
+ | _ => zify_unop_var_or_term t thm a
+ end.
+
+Ltac zify_unop_nored t thm a :=
+ (* in this version, we don't try to reduce the unop (that can be (Zplus x)) *)
+ let isz := isZcst a in
+ match isz with
+ | true => zify_unop_core t thm a
+ | _ => zify_unop_var_or_term t thm a
+ end.
+
+Ltac zify_binop t thm a b:=
+ (* works as zify_unop, except that we should be careful when
+ dealing with b, since it can be equal to a *)
+ let isza := isZcst a in
+ match isza with
+ | true => zify_unop (t a) (thm a) b
+ | _ =>
+ let za := fresh "z" in
+ (rename a into za; rename za into a; zify_unop_nored (t a) (thm a) b) ||
+ (remember a as za; match goal with
+ | H : za = b |- _ => zify_unop_nored (t za) (thm za) za
+ | _ => zify_unop_nored (t za) (thm za) b
+ end)
+ end.
+
+Ltac zify_op_1 :=
+ match goal with
+ | |- context [ Zmax ?a ?b ] => zify_binop Zmax Zmax_spec a b
+ | H : context [ Zmax ?a ?b ] |- _ => zify_binop Zmax Zmax_spec a b
+ | |- context [ Zmin ?a ?b ] => zify_binop Zmin Zmin_spec a b
+ | H : context [ Zmin ?a ?b ] |- _ => zify_binop Zmin Zmin_spec a b
+ | |- context [ Zsgn ?a ] => zify_unop Zsgn Zsgn_spec a
+ | H : context [ Zsgn ?a ] |- _ => zify_unop Zsgn Zsgn_spec a
+ | |- context [ Zabs ?a ] => zify_unop Zabs Zabs_spec a
+ | H : context [ Zabs ?a ] |- _ => zify_unop Zabs Zabs_spec a
+ end.
+
+Ltac zify_op := repeat zify_op_1.
+
+
+
+
+
+(** II) Conversion from nat to Z *)
+
+
+Definition Z_of_nat' := Z_of_nat.
+
+Ltac hide_Z_of_nat t :=
+ let z := fresh "z" in set (z:=Z_of_nat t) in *;
+ change Z_of_nat with Z_of_nat' in z;
+ unfold z in *; clear z.
+
+Ltac zify_nat_rel :=
+ match goal with
+ (* I: equalities *)
+ | H : (@eq nat ?a ?b) |- _ => generalize (inj_eq _ _ H); clear H; intro H
+ | |- (@eq nat ?a ?b) => apply (inj_eq_rev a b)
+ | H : context [ @eq nat ?a ?b ] |- _ => rewrite (inj_eq_iff a b) in H
+ | |- context [ @eq nat ?a ?b ] => rewrite (inj_eq_iff a b)
+ (* II: less than *)
+ | H : (lt ?a ?b) |- _ => generalize (inj_lt _ _ H); clear H; intro H
+ | |- (lt ?a ?b) => apply (inj_lt_rev a b)
+ | H : context [ lt ?a ?b ] |- _ => rewrite (inj_lt_iff a b) in H
+ | |- context [ lt ?a ?b ] => rewrite (inj_lt_iff a b)
+ (* III: less or equal *)
+ | H : (le ?a ?b) |- _ => generalize (inj_le _ _ H); clear H; intro H
+ | |- (le ?a ?b) => apply (inj_le_rev a b)
+ | H : context [ le ?a ?b ] |- _ => rewrite (inj_le_iff a b) in H
+ | |- context [ le ?a ?b ] => rewrite (inj_le_iff a b)
+ (* IV: greater than *)
+ | H : (gt ?a ?b) |- _ => generalize (inj_gt _ _ H); clear H; intro H
+ | |- (gt ?a ?b) => apply (inj_gt_rev a b)
+ | H : context [ gt ?a ?b ] |- _ => rewrite (inj_gt_iff a b) in H
+ | |- context [ gt ?a ?b ] => rewrite (inj_gt_iff a b)
+ (* V: greater or equal *)
+ | H : (ge ?a ?b) |- _ => generalize (inj_ge _ _ H); clear H; intro H
+ | |- (ge ?a ?b) => apply (inj_ge_rev a b)
+ | H : context [ ge ?a ?b ] |- _ => rewrite (inj_ge_iff a b) in H
+ | |- context [ ge ?a ?b ] => rewrite (inj_ge_iff a b)
+ end.
+
+Ltac zify_nat_op :=
+ match goal with
+ (* misc type conversions: positive/N/Z to nat *)
+ | H : context [ Z_of_nat (nat_of_P ?a) ] |- _ => rewrite <- (Zpos_eq_Z_of_nat_o_nat_of_P a) in H
+ | |- context [ Z_of_nat (nat_of_P ?a) ] => rewrite <- (Zpos_eq_Z_of_nat_o_nat_of_P a)
+ | H : context [ Z_of_nat (nat_of_N ?a) ] |- _ => rewrite (Z_of_nat_of_N a) in H
+ | |- context [ Z_of_nat (nat_of_N ?a) ] => rewrite (Z_of_nat_of_N a)
+ | H : context [ Z_of_nat (Zabs_nat ?a) ] |- _ => rewrite (inj_Zabs_nat a) in H
+ | |- context [ Z_of_nat (Zabs_nat ?a) ] => rewrite (inj_Zabs_nat a)
+
+ (* plus -> Zplus *)
+ | H : context [ Z_of_nat (plus ?a ?b) ] |- _ => rewrite (inj_plus a b) in H
+ | |- context [ Z_of_nat (plus ?a ?b) ] => rewrite (inj_plus a b)
+
+ (* min -> Zmin *)
+ | H : context [ Z_of_nat (min ?a ?b) ] |- _ => rewrite (inj_min a b) in H
+ | |- context [ Z_of_nat (min ?a ?b) ] => rewrite (inj_min a b)
+
+ (* max -> Zmax *)
+ | H : context [ Z_of_nat (max ?a ?b) ] |- _ => rewrite (inj_max a b) in H
+ | |- context [ Z_of_nat (max ?a ?b) ] => rewrite (inj_max a b)
+
+ (* minus -> Zmax (Zminus ... ...) 0 *)
+ | H : context [ Z_of_nat (minus ?a ?b) ] |- _ => rewrite (inj_minus a b) in H
+ | |- context [ Z_of_nat (minus ?a ?b) ] => rewrite (inj_minus a b)
+
+ (* pred -> minus ... -1 -> Zmax (Zminus ... -1) 0 *)
+ | H : context [ Z_of_nat (pred ?a) ] |- _ => rewrite (pred_of_minus a) in H
+ | |- context [ Z_of_nat (pred ?a) ] => rewrite (pred_of_minus a)
+
+ (* mult -> Zmult and a positivity hypothesis *)
+ | H : context [ Z_of_nat (mult ?a ?b) ] |- _ =>
+ let H:= fresh "H" in
+ assert (H:=Zle_0_nat (mult a b)); rewrite (inj_mult a b) in *
+ | |- context [ Z_of_nat (mult ?a ?b) ] =>
+ let H:= fresh "H" in
+ assert (H:=Zle_0_nat (mult a b)); rewrite (inj_mult a b) in *
+
+ (* O -> Z0 *)
+ | H : context [ Z_of_nat O ] |- _ => simpl (Z_of_nat O) in H
+ | |- context [ Z_of_nat O ] => simpl (Z_of_nat O)
+
+ (* S -> number or Zsucc *)
+ | H : context [ Z_of_nat (S ?a) ] |- _ =>
+ let isnat := isnatcst a in
+ match isnat with
+ | true => simpl (Z_of_nat (S a)) in H
+ | _ => rewrite (inj_S a) in H
+ end
+ | |- context [ Z_of_nat (S ?a) ] =>
+ let isnat := isnatcst a in
+ match isnat with
+ | true => simpl (Z_of_nat (S a))
+ | _ => rewrite (inj_S a)
+ end
+
+ (* atoms of type nat : we add a positivity condition (if not already there) *)
+ | H : context [ Z_of_nat ?a ] |- _ =>
+ match goal with
+ | H' : 0 <= Z_of_nat a |- _ => hide_Z_of_nat a
+ | H' : 0 <= Z_of_nat' a |- _ => fail
+ | _ => let H:= fresh "H" in
+ assert (H:=Zle_0_nat a); hide_Z_of_nat a
+ end
+ | |- context [ Z_of_nat ?a ] =>
+ match goal with
+ | H' : 0 <= Z_of_nat a |- _ => hide_Z_of_nat a
+ | H' : 0 <= Z_of_nat' a |- _ => fail
+ | _ => let H:= fresh "H" in
+ assert (H:=Zle_0_nat a); hide_Z_of_nat a
+ end
+ end.
+
+Ltac zify_nat := repeat zify_nat_rel; repeat zify_nat_op; unfold Z_of_nat' in *.
+
+
+
+
+(* III) conversion from positive to Z *)
+
+Definition Zpos' := Zpos.
+Definition Zneg' := Zneg.
+
+Ltac hide_Zpos t :=
+ let z := fresh "z" in set (z:=Zpos t) in *;
+ change Zpos with Zpos' in z;
+ unfold z in *; clear z.
+
+Ltac zify_positive_rel :=
+ match goal with
+ (* I: equalities *)
+ | H : (@eq positive ?a ?b) |- _ => generalize (Zpos_eq _ _ H); clear H; intro H
+ | |- (@eq positive ?a ?b) => apply (Zpos_eq_rev a b)
+ | H : context [ @eq positive ?a ?b ] |- _ => rewrite (Zpos_eq_iff a b) in H
+ | |- context [ @eq positive ?a ?b ] => rewrite (Zpos_eq_iff a b)
+ (* II: less than *)
+ | H : context [ (?a<?b)%positive ] |- _ => change (a<b)%positive with (Zpos a<Zpos b) in H
+ | |- context [ (?a<?b)%positive ] => change (a<b)%positive with (Zpos a<Zpos b)
+ (* III: less or equal *)
+ | H : context [ (?a<=?b)%positive ] |- _ => change (a<=b)%positive with (Zpos a<=Zpos b) in H
+ | |- context [ (?a<=?b)%positive ] => change (a<=b)%positive with (Zpos a<=Zpos b)
+ (* IV: greater than *)
+ | H : context [ (?a>?b)%positive ] |- _ => change (a>b)%positive with (Zpos a>Zpos b) in H
+ | |- context [ (?a>?b)%positive ] => change (a>b)%positive with (Zpos a>Zpos b)
+ (* V: greater or equal *)
+ | H : context [ (?a>=?b)%positive ] |- _ => change (a>=b)%positive with (Zpos a>=Zpos b) in H
+ | |- context [ (?a>=?b)%positive ] => change (a>=b)%positive with (Zpos a>=Zpos b)
+ end.
+
+Ltac zify_positive_op :=
+ match goal with
+ (* Zneg -> -Zpos (except for numbers) *)
+ | H : context [ Zneg ?a ] |- _ =>
+ let isp := isPcst a in
+ match isp with
+ | true => change (Zneg a) with (Zneg' a) in H
+ | _ => change (Zneg a) with (- Zpos a) in H
+ end
+ | |- context [ Zneg ?a ] =>
+ let isp := isPcst a in
+ match isp with
+ | true => change (Zneg a) with (Zneg' a)
+ | _ => change (Zneg a) with (- Zpos a)
+ end
+
+ (* misc type conversions: nat to positive *)
+ | H : context [ Zpos (P_of_succ_nat ?a) ] |- _ => rewrite (Zpos_P_of_succ_nat a) in H
+ | |- context [ Zpos (P_of_succ_nat ?a) ] => rewrite (Zpos_P_of_succ_nat a)
+
+ (* Pplus -> Zplus *)
+ | H : context [ Zpos (Pplus ?a ?b) ] |- _ => change (Zpos (Pplus a b)) with (Zplus (Zpos a) (Zpos b)) in H
+ | |- context [ Zpos (Pplus ?a ?b) ] => change (Zpos (Pplus a b)) with (Zplus (Zpos a) (Zpos b))
+
+ (* Pmin -> Zmin *)
+ | H : context [ Zpos (Pmin ?a ?b) ] |- _ => rewrite (Zpos_min a b) in H
+ | |- context [ Zpos (Pmin ?a ?b) ] => rewrite (Zpos_min a b)
+
+ (* Pmax -> Zmax *)
+ | H : context [ Zpos (Pmax ?a ?b) ] |- _ => rewrite (Zpos_max a b) in H
+ | |- context [ Zpos (Pmax ?a ?b) ] => rewrite (Zpos_max a b)
+
+ (* Pminus -> Zmax 1 (Zminus ... ...) *)
+ | H : context [ Zpos (Pminus ?a ?b) ] |- _ => rewrite (Zpos_minus a b) in H
+ | |- context [ Zpos (Pminus ?a ?b) ] => rewrite (Zpos_minus a b)
+
+ (* Psucc -> Zsucc *)
+ | H : context [ Zpos (Psucc ?a) ] |- _ => rewrite (Zpos_succ_morphism a) in H
+ | |- context [ Zpos (Psucc ?a) ] => rewrite (Zpos_succ_morphism a)
+
+ (* Ppred -> Pminus ... -1 -> Zmax 1 (Zminus ... - 1) *)
+ | H : context [ Zpos (Ppred ?a) ] |- _ => rewrite (Ppred_minus a) in H
+ | |- context [ Zpos (Ppred ?a) ] => rewrite (Ppred_minus a)
+
+ (* Pmult -> Zmult and a positivity hypothesis *)
+ | H : context [ Zpos (Pmult ?a ?b) ] |- _ =>
+ let H:= fresh "H" in
+ assert (H:=Zgt_pos_0 (Pmult a b)); rewrite (Zpos_mult_morphism a b) in *
+ | |- context [ Zpos (Pmult ?a ?b) ] =>
+ let H:= fresh "H" in
+ assert (H:=Zgt_pos_0 (Pmult a b)); rewrite (Zpos_mult_morphism a b) in *
+
+ (* xO *)
+ | H : context [ Zpos (xO ?a) ] |- _ =>
+ let isp := isPcst a in
+ match isp with
+ | true => change (Zpos (xO a)) with (Zpos' (xO a)) in H
+ | _ => rewrite (Zpos_xO a) in H
+ end
+ | |- context [ Zpos (xO ?a) ] =>
+ let isp := isPcst a in
+ match isp with
+ | true => change (Zpos (xO a)) with (Zpos' (xO a))
+ | _ => rewrite (Zpos_xO a)
+ end
+ (* xI *)
+ | H : context [ Zpos (xI ?a) ] |- _ =>
+ let isp := isPcst a in
+ match isp with
+ | true => change (Zpos (xI a)) with (Zpos' (xI a)) in H
+ | _ => rewrite (Zpos_xI a) in H
+ end
+ | |- context [ Zpos (xI ?a) ] =>
+ let isp := isPcst a in
+ match isp with
+ | true => change (Zpos (xI a)) with (Zpos' (xI a))
+ | _ => rewrite (Zpos_xI a)
+ end
+
+ (* xI : nothing to do, just prevent adding a useless positivity condition *)
+ | H : context [ Zpos xH ] |- _ => hide_Zpos xH
+ | |- context [ Zpos xH ] => hide_Zpos xH
+
+ (* atoms of type positive : we add a positivity condition (if not already there) *)
+ | H : context [ Zpos ?a ] |- _ =>
+ match goal with
+ | H' : Zpos a > 0 |- _ => hide_Zpos a
+ | H' : Zpos' a > 0 |- _ => fail
+ | _ => let H:= fresh "H" in assert (H:=Zgt_pos_0 a); hide_Zpos a
+ end
+ | |- context [ Zpos ?a ] =>
+ match goal with
+ | H' : Zpos a > 0 |- _ => hide_Zpos a
+ | H' : Zpos' a > 0 |- _ => fail
+ | _ => let H:= fresh "H" in assert (H:=Zgt_pos_0 a); hide_Zpos a
+ end
+ end.
+
+Ltac zify_positive :=
+ repeat zify_positive_rel; repeat zify_positive_op; unfold Zpos',Zneg' in *.
+
+
+
+
+
+(* IV) conversion from N to Z *)
+
+Definition Z_of_N' := Z_of_N.
+
+Ltac hide_Z_of_N t :=
+ let z := fresh "z" in set (z:=Z_of_N t) in *;
+ change Z_of_N with Z_of_N' in z;
+ unfold z in *; clear z.
+
+Ltac zify_N_rel :=
+ match goal with
+ (* I: equalities *)
+ | H : (@eq N ?a ?b) |- _ => generalize (Z_of_N_eq _ _ H); clear H; intro H
+ | |- (@eq N ?a ?b) => apply (Z_of_N_eq_rev a b)
+ | H : context [ @eq N ?a ?b ] |- _ => rewrite (Z_of_N_eq_iff a b) in H
+ | |- context [ @eq N ?a ?b ] => rewrite (Z_of_N_eq_iff a b)
+ (* II: less than *)
+ | H : (?a<?b)%N |- _ => generalize (Z_of_N_lt _ _ H); clear H; intro H
+ | |- (?a<?b)%N => apply (Z_of_N_lt_rev a b)
+ | H : context [ (?a<?b)%N ] |- _ => rewrite (Z_of_N_lt_iff a b) in H
+ | |- context [ (?a<?b)%N ] => rewrite (Z_of_N_lt_iff a b)
+ (* III: less or equal *)
+ | H : (?a<=?b)%N |- _ => generalize (Z_of_N_le _ _ H); clear H; intro H
+ | |- (?a<=?b)%N => apply (Z_of_N_le_rev a b)
+ | H : context [ (?a<=?b)%N ] |- _ => rewrite (Z_of_N_le_iff a b) in H
+ | |- context [ (?a<=?b)%N ] => rewrite (Z_of_N_le_iff a b)
+ (* IV: greater than *)
+ | H : (?a>?b)%N |- _ => generalize (Z_of_N_gt _ _ H); clear H; intro H
+ | |- (?a>?b)%N => apply (Z_of_N_gt_rev a b)
+ | H : context [ (?a>?b)%N ] |- _ => rewrite (Z_of_N_gt_iff a b) in H
+ | |- context [ (?a>?b)%N ] => rewrite (Z_of_N_gt_iff a b)
+ (* V: greater or equal *)
+ | H : (?a>=?b)%N |- _ => generalize (Z_of_N_ge _ _ H); clear H; intro H
+ | |- (?a>=?b)%N => apply (Z_of_N_ge_rev a b)
+ | H : context [ (?a>=?b)%N ] |- _ => rewrite (Z_of_N_ge_iff a b) in H
+ | |- context [ (?a>=?b)%N ] => rewrite (Z_of_N_ge_iff a b)
+ end.
+
+Ltac zify_N_op :=
+ match goal with
+ (* misc type conversions: nat to positive *)
+ | H : context [ Z_of_N (N_of_nat ?a) ] |- _ => rewrite (Z_of_N_of_nat a) in H
+ | |- context [ Z_of_N (N_of_nat ?a) ] => rewrite (Z_of_N_of_nat a)
+ | H : context [ Z_of_N (Zabs_N ?a) ] |- _ => rewrite (Z_of_N_abs a) in H
+ | |- context [ Z_of_N (Zabs_N ?a) ] => rewrite (Z_of_N_abs a)
+ | H : context [ Z_of_N (Npos ?a) ] |- _ => rewrite (Z_of_N_pos a) in H
+ | |- context [ Z_of_N (Npos ?a) ] => rewrite (Z_of_N_pos a)
+ | H : context [ Z_of_N N0 ] |- _ => change (Z_of_N N0) with Z0 in H
+ | |- context [ Z_of_N N0 ] => change (Z_of_N N0) with Z0
+
+ (* Nplus -> Zplus *)
+ | H : context [ Z_of_N (Nplus ?a ?b) ] |- _ => rewrite (Z_of_N_plus a b) in H
+ | |- context [ Z_of_N (Nplus ?a ?b) ] => rewrite (Z_of_N_plus a b)
+
+ (* Nmin -> Zmin *)
+ | H : context [ Z_of_N (Nmin ?a ?b) ] |- _ => rewrite (Z_of_N_min a b) in H
+ | |- context [ Z_of_N (Nmin ?a ?b) ] => rewrite (Z_of_N_min a b)
+
+ (* Nmax -> Zmax *)
+ | H : context [ Z_of_N (Nmax ?a ?b) ] |- _ => rewrite (Z_of_N_max a b) in H
+ | |- context [ Z_of_N (Nmax ?a ?b) ] => rewrite (Z_of_N_max a b)
+
+ (* Nminus -> Zmax 0 (Zminus ... ...) *)
+ | H : context [ Z_of_N (Nminus ?a ?b) ] |- _ => rewrite (Z_of_N_minus a b) in H
+ | |- context [ Z_of_N (Nminus ?a ?b) ] => rewrite (Z_of_N_minus a b)
+
+ (* Nsucc -> Zsucc *)
+ | H : context [ Z_of_N (Nsucc ?a) ] |- _ => rewrite (Z_of_N_succ a) in H
+ | |- context [ Z_of_N (Nsucc ?a) ] => rewrite (Z_of_N_succ a)
+
+ (* Nmult -> Zmult and a positivity hypothesis *)
+ | H : context [ Z_of_N (Nmult ?a ?b) ] |- _ =>
+ let H:= fresh "H" in
+ assert (H:=Z_of_N_le_0 (Nmult a b)); rewrite (Z_of_N_mult a b) in *
+ | |- context [ Z_of_N (Nmult ?a ?b) ] =>
+ let H:= fresh "H" in
+ assert (H:=Z_of_N_le_0 (Nmult a b)); rewrite (Z_of_N_mult a b) in *
+
+ (* atoms of type N : we add a positivity condition (if not already there) *)
+ | H : context [ Z_of_N ?a ] |- _ =>
+ match goal with
+ | H' : 0 <= Z_of_N a |- _ => hide_Z_of_N a
+ | H' : 0 <= Z_of_N' a |- _ => fail
+ | _ => let H:= fresh "H" in assert (H:=Z_of_N_le_0 a); hide_Z_of_N a
+ end
+ | |- context [ Z_of_N ?a ] =>
+ match goal with
+ | H' : 0 <= Z_of_N a |- _ => hide_Z_of_N a
+ | H' : 0 <= Z_of_N' a |- _ => fail
+ | _ => let H:= fresh "H" in assert (H:=Z_of_N_le_0 a); hide_Z_of_N a
+ end
+ end.
+
+Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *.
+
+
+
+(** The complete Z-ification tactic *)
+
+Ltac zify :=
+ repeat progress (zify_nat; zify_positive; zify_N); zify_op.
+
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
new file mode 100644
index 00000000..60616845
--- /dev/null
+++ b/plugins/omega/coq_omega.ml
@@ -0,0 +1,1823 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(**************************************************************************)
+(* *)
+(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *)
+(* *)
+(* Pierre Crégut (CNET, Lannion, France) *)
+(* *)
+(**************************************************************************)
+
+(* $Id$ *)
+
+open Util
+open Pp
+open Reduction
+open Proof_type
+open Names
+open Nameops
+open Term
+open Termops
+open Declarations
+open Environ
+open Sign
+open Inductive
+open Tacticals
+open Tacmach
+open Evar_refiner
+open Tactics
+open Clenv
+open Logic
+open Libnames
+open Nametab
+open Contradiction
+
+module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
+open OmegaSolver
+
+(* Added by JCF, 09/03/98 *)
+
+let elim_id id gl = simplest_elim (pf_global gl id) gl
+let resolve_id id gl = apply (pf_global gl id) gl
+
+let timing timer_name f arg = f arg
+
+let display_time_flag = ref false
+let display_system_flag = ref false
+let display_action_flag = ref false
+let old_style_flag = ref false
+
+let read f () = !f
+let write f x = f:=x
+
+open Goptions
+
+let _ =
+ declare_bool_option
+ { optsync = false;
+ optname = "Omega system time displaying flag";
+ optkey = ["Omega";"System"];
+ optread = read display_system_flag;
+ optwrite = write display_system_flag }
+
+let _ =
+ declare_bool_option
+ { optsync = false;
+ optname = "Omega action display flag";
+ optkey = ["Omega";"Action"];
+ optread = read display_action_flag;
+ optwrite = write display_action_flag }
+
+let _ =
+ declare_bool_option
+ { optsync = false;
+ optname = "Omega old style flag";
+ optkey = ["Omega";"OldStyle"];
+ optread = read old_style_flag;
+ optwrite = write old_style_flag }
+
+
+let all_time = timing "Omega "
+let solver_time = timing "Solver "
+let exact_time = timing "Rewrites "
+let elim_time = timing "Elim "
+let simpl_time = timing "Simpl "
+let generalize_time = timing "Generalize"
+
+let new_identifier =
+ let cpt = ref 0 in
+ (fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; id_of_string s)
+
+let new_identifier_state =
+ let cpt = ref 0 in
+ (fun () -> let s = make_ident "State" (Some !cpt) in incr cpt; s)
+
+let new_identifier_var =
+ let cpt = ref 0 in
+ (fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; id_of_string s)
+
+let new_id =
+ let cpt = ref 0 in fun () -> incr cpt; !cpt
+
+let new_var_num =
+ let cpt = ref 1000 in (fun () -> incr cpt; !cpt)
+
+let new_var =
+ let cpt = ref 0 in fun () -> incr cpt; Nameops.make_ident "WW" (Some !cpt)
+
+let display_var i = Printf.sprintf "X%d" i
+
+let intern_id,unintern_id =
+ let cpt = ref 0 in
+ let table = Hashtbl.create 7 and co_table = Hashtbl.create 7 in
+ (fun (name : identifier) ->
+ try Hashtbl.find table name with Not_found ->
+ let idx = !cpt in
+ Hashtbl.add table name idx;
+ Hashtbl.add co_table idx name;
+ incr cpt; idx),
+ (fun idx ->
+ try Hashtbl.find co_table idx with Not_found ->
+ let v = new_var () in
+ Hashtbl.add table v idx; Hashtbl.add co_table idx v; v)
+
+let mk_then = tclTHENLIST
+
+let exists_tac c = constructor_tac false (Some 1) 1 (Rawterm.ImplicitBindings [c])
+
+let generalize_tac t = generalize_time (generalize t)
+let elim t = elim_time (simplest_elim t)
+let exact t = exact_time (Tactics.refine t)
+let unfold s = Tactics.unfold_in_concl [all_occurrences, Lazy.force s]
+
+let rev_assoc k =
+ let rec loop = function
+ | [] -> raise Not_found | (v,k')::_ when k = k' -> v | _ :: l -> loop l
+ in
+ loop
+
+let tag_hypothesis,tag_of_hyp, hyp_of_tag =
+ let l = ref ([]:(identifier * int) list) in
+ (fun h id -> l := (h,id):: !l),
+ (fun h -> try List.assoc h !l with Not_found -> failwith "tag_hypothesis"),
+ (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis")
+
+let hide_constr,find_constr,clear_tables,dump_tables =
+ let l = ref ([]:(constr * (identifier * identifier * bool)) list) in
+ (fun h id eg b -> l := (h,(id,eg,b)):: !l),
+ (fun h -> try List.assoc h !l with Not_found -> failwith "find_contr"),
+ (fun () -> l := []),
+ (fun () -> !l)
+
+(* Lazy evaluation is used for Coq constants, because this code
+ is evaluated before the compiled modules are loaded.
+ To use the constant Zplus, one must type "Lazy.force coq_Zplus"
+ This is the right way to access to Coq constants in tactics ML code *)
+
+open Coqlib
+
+let logic_dir = ["Coq";"Logic";"Decidable"]
+let coq_modules =
+ init_modules @arith_modules @ [logic_dir] @ zarith_base_modules
+ @ [["Coq"; "omega"; "OmegaLemmas"]]
+
+let init_constant = gen_constant_in_modules "Omega" init_modules
+let constant = gen_constant_in_modules "Omega" coq_modules
+
+(* Zarith *)
+let coq_xH = lazy (constant "xH")
+let coq_xO = lazy (constant "xO")
+let coq_xI = lazy (constant "xI")
+let coq_Z0 = lazy (constant "Z0")
+let coq_Zpos = lazy (constant "Zpos")
+let coq_Zneg = lazy (constant "Zneg")
+let coq_Z = lazy (constant "Z")
+let coq_comparison = lazy (constant "comparison")
+let coq_Gt = lazy (constant "Gt")
+let coq_Zplus = lazy (constant "Zplus")
+let coq_Zmult = lazy (constant "Zmult")
+let coq_Zopp = lazy (constant "Zopp")
+let coq_Zminus = lazy (constant "Zminus")
+let coq_Zsucc = lazy (constant "Zsucc")
+let coq_Zgt = lazy (constant "Zgt")
+let coq_Zle = lazy (constant "Zle")
+let coq_Z_of_nat = lazy (constant "Z_of_nat")
+let coq_inj_plus = lazy (constant "inj_plus")
+let coq_inj_mult = lazy (constant "inj_mult")
+let coq_inj_minus1 = lazy (constant "inj_minus1")
+let coq_inj_minus2 = lazy (constant "inj_minus2")
+let coq_inj_S = lazy (constant "inj_S")
+let coq_inj_le = lazy (constant "inj_le")
+let coq_inj_lt = lazy (constant "inj_lt")
+let coq_inj_ge = lazy (constant "inj_ge")
+let coq_inj_gt = lazy (constant "inj_gt")
+let coq_inj_neq = lazy (constant "inj_neq")
+let coq_inj_eq = lazy (constant "inj_eq")
+let coq_fast_Zplus_assoc_reverse = lazy (constant "fast_Zplus_assoc_reverse")
+let coq_fast_Zplus_assoc = lazy (constant "fast_Zplus_assoc")
+let coq_fast_Zmult_assoc_reverse = lazy (constant "fast_Zmult_assoc_reverse")
+let coq_fast_Zplus_permute = lazy (constant "fast_Zplus_permute")
+let coq_fast_Zplus_comm = lazy (constant "fast_Zplus_comm")
+let coq_fast_Zmult_comm = lazy (constant "fast_Zmult_comm")
+let coq_Zmult_le_approx = lazy (constant "Zmult_le_approx")
+let coq_OMEGA1 = lazy (constant "OMEGA1")
+let coq_OMEGA2 = lazy (constant "OMEGA2")
+let coq_OMEGA3 = lazy (constant "OMEGA3")
+let coq_OMEGA4 = lazy (constant "OMEGA4")
+let coq_OMEGA5 = lazy (constant "OMEGA5")
+let coq_OMEGA6 = lazy (constant "OMEGA6")
+let coq_OMEGA7 = lazy (constant "OMEGA7")
+let coq_OMEGA8 = lazy (constant "OMEGA8")
+let coq_OMEGA9 = lazy (constant "OMEGA9")
+let coq_fast_OMEGA10 = lazy (constant "fast_OMEGA10")
+let coq_fast_OMEGA11 = lazy (constant "fast_OMEGA11")
+let coq_fast_OMEGA12 = lazy (constant "fast_OMEGA12")
+let coq_fast_OMEGA13 = lazy (constant "fast_OMEGA13")
+let coq_fast_OMEGA14 = lazy (constant "fast_OMEGA14")
+let coq_fast_OMEGA15 = lazy (constant "fast_OMEGA15")
+let coq_fast_OMEGA16 = lazy (constant "fast_OMEGA16")
+let coq_OMEGA17 = lazy (constant "OMEGA17")
+let coq_OMEGA18 = lazy (constant "OMEGA18")
+let coq_OMEGA19 = lazy (constant "OMEGA19")
+let coq_OMEGA20 = lazy (constant "OMEGA20")
+let coq_fast_Zred_factor0 = lazy (constant "fast_Zred_factor0")
+let coq_fast_Zred_factor1 = lazy (constant "fast_Zred_factor1")
+let coq_fast_Zred_factor2 = lazy (constant "fast_Zred_factor2")
+let coq_fast_Zred_factor3 = lazy (constant "fast_Zred_factor3")
+let coq_fast_Zred_factor4 = lazy (constant "fast_Zred_factor4")
+let coq_fast_Zred_factor5 = lazy (constant "fast_Zred_factor5")
+let coq_fast_Zred_factor6 = lazy (constant "fast_Zred_factor6")
+let coq_fast_Zmult_plus_distr_l = lazy (constant "fast_Zmult_plus_distr_l")
+let coq_fast_Zmult_opp_comm = lazy (constant "fast_Zmult_opp_comm")
+let coq_fast_Zopp_plus_distr = lazy (constant "fast_Zopp_plus_distr")
+let coq_fast_Zopp_mult_distr_r = lazy (constant "fast_Zopp_mult_distr_r")
+let coq_fast_Zopp_eq_mult_neg_1 = lazy (constant "fast_Zopp_eq_mult_neg_1")
+let coq_fast_Zopp_involutive = lazy (constant "fast_Zopp_involutive")
+let coq_Zegal_left = lazy (constant "Zegal_left")
+let coq_Zne_left = lazy (constant "Zne_left")
+let coq_Zlt_left = lazy (constant "Zlt_left")
+let coq_Zge_left = lazy (constant "Zge_left")
+let coq_Zgt_left = lazy (constant "Zgt_left")
+let coq_Zle_left = lazy (constant "Zle_left")
+let coq_new_var = lazy (constant "new_var")
+let coq_intro_Z = lazy (constant "intro_Z")
+
+let coq_dec_eq = lazy (constant "dec_eq")
+let coq_dec_Zne = lazy (constant "dec_Zne")
+let coq_dec_Zle = lazy (constant "dec_Zle")
+let coq_dec_Zlt = lazy (constant "dec_Zlt")
+let coq_dec_Zgt = lazy (constant "dec_Zgt")
+let coq_dec_Zge = lazy (constant "dec_Zge")
+
+let coq_not_Zeq = lazy (constant "not_Zeq")
+let coq_Znot_le_gt = lazy (constant "Znot_le_gt")
+let coq_Znot_lt_ge = lazy (constant "Znot_lt_ge")
+let coq_Znot_ge_lt = lazy (constant "Znot_ge_lt")
+let coq_Znot_gt_le = lazy (constant "Znot_gt_le")
+let coq_neq = lazy (constant "neq")
+let coq_Zne = lazy (constant "Zne")
+let coq_Zle = lazy (constant "Zle")
+let coq_Zgt = lazy (constant "Zgt")
+let coq_Zge = lazy (constant "Zge")
+let coq_Zlt = lazy (constant "Zlt")
+
+(* Peano/Datatypes *)
+let coq_le = lazy (init_constant "le")
+let coq_lt = lazy (init_constant "lt")
+let coq_ge = lazy (init_constant "ge")
+let coq_gt = lazy (init_constant "gt")
+let coq_minus = lazy (init_constant "minus")
+let coq_plus = lazy (init_constant "plus")
+let coq_mult = lazy (init_constant "mult")
+let coq_pred = lazy (init_constant "pred")
+let coq_nat = lazy (init_constant "nat")
+let coq_S = lazy (init_constant "S")
+let coq_O = lazy (init_constant "O")
+
+(* Compare_dec/Peano_dec/Minus *)
+let coq_pred_of_minus = lazy (constant "pred_of_minus")
+let coq_le_gt_dec = lazy (constant "le_gt_dec")
+let coq_dec_eq_nat = lazy (constant "dec_eq_nat")
+let coq_dec_le = lazy (constant "dec_le")
+let coq_dec_lt = lazy (constant "dec_lt")
+let coq_dec_ge = lazy (constant "dec_ge")
+let coq_dec_gt = lazy (constant "dec_gt")
+let coq_not_eq = lazy (constant "not_eq")
+let coq_not_le = lazy (constant "not_le")
+let coq_not_lt = lazy (constant "not_lt")
+let coq_not_ge = lazy (constant "not_ge")
+let coq_not_gt = lazy (constant "not_gt")
+
+(* Logic/Decidable *)
+let coq_eq_ind_r = lazy (constant "eq_ind_r")
+
+let coq_dec_or = lazy (constant "dec_or")
+let coq_dec_and = lazy (constant "dec_and")
+let coq_dec_imp = lazy (constant "dec_imp")
+let coq_dec_iff = lazy (constant "dec_iff")
+let coq_dec_not = lazy (constant "dec_not")
+let coq_dec_False = lazy (constant "dec_False")
+let coq_dec_not_not = lazy (constant "dec_not_not")
+let coq_dec_True = lazy (constant "dec_True")
+
+let coq_not_or = lazy (constant "not_or")
+let coq_not_and = lazy (constant "not_and")
+let coq_not_imp = lazy (constant "not_imp")
+let coq_not_iff = lazy (constant "not_iff")
+let coq_not_not = lazy (constant "not_not")
+let coq_imp_simp = lazy (constant "imp_simp")
+let coq_iff = lazy (constant "iff")
+
+(* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *)
+
+(* For unfold *)
+open Closure
+let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with
+ | Const kn when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) ->
+ EvalConstRef kn
+ | _ -> anomaly ("Coq_omega: "^s^" is not an evaluable constant")
+
+let sp_Zsucc = lazy (evaluable_ref_of_constr "Zsucc" coq_Zsucc)
+let sp_Zminus = lazy (evaluable_ref_of_constr "Zminus" coq_Zminus)
+let sp_Zle = lazy (evaluable_ref_of_constr "Zle" coq_Zle)
+let sp_Zgt = lazy (evaluable_ref_of_constr "Zgt" coq_Zgt)
+let sp_Zge = lazy (evaluable_ref_of_constr "Zge" coq_Zge)
+let sp_Zlt = lazy (evaluable_ref_of_constr "Zlt" coq_Zlt)
+let sp_not = lazy (evaluable_ref_of_constr "not" (lazy (build_coq_not ())))
+
+let mk_var v = mkVar (id_of_string v)
+let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |])
+let mk_times t1 t2 = mkApp (Lazy.force coq_Zmult, [| t1; t2 |])
+let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |])
+let mk_eq t1 t2 = mkApp (build_coq_eq (), [| Lazy.force coq_Z; t1; t2 |])
+let mk_le t1 t2 = mkApp (Lazy.force coq_Zle, [| t1; t2 |])
+let mk_gt t1 t2 = mkApp (Lazy.force coq_Zgt, [| t1; t2 |])
+let mk_inv t = mkApp (Lazy.force coq_Zopp, [| t |])
+let mk_and t1 t2 = mkApp (build_coq_and (), [| t1; t2 |])
+let mk_or t1 t2 = mkApp (build_coq_or (), [| t1; t2 |])
+let mk_not t = mkApp (build_coq_not (), [| t |])
+let mk_eq_rel t1 t2 = mkApp (build_coq_eq (),
+ [| Lazy.force coq_comparison; t1; t2 |])
+let mk_inj t = mkApp (Lazy.force coq_Z_of_nat, [| t |])
+
+let mk_integer n =
+ let rec loop n =
+ if n =? one then Lazy.force coq_xH else
+ mkApp((if n mod two =? zero then Lazy.force coq_xO else Lazy.force coq_xI),
+ [| loop (n/two) |])
+ in
+ if n =? zero then Lazy.force coq_Z0
+ else mkApp ((if n >? zero then Lazy.force coq_Zpos else Lazy.force coq_Zneg),
+ [| loop (abs n) |])
+
+type omega_constant =
+ | Zplus | Zmult | Zminus | Zsucc | Zopp
+ | Plus | Mult | Minus | Pred | S | O
+ | Zpos | Zneg | Z0 | Z_of_nat
+ | Eq | Neq
+ | Zne | Zle | Zlt | Zge | Zgt
+ | Z | Nat
+ | And | Or | False | True | Not | Iff
+ | Le | Lt | Ge | Gt
+ | Other of string
+
+type omega_proposition =
+ | Keq of constr * constr * constr
+ | Kn
+
+type result =
+ | Kvar of identifier
+ | Kapp of omega_constant * constr list
+ | Kimp of constr * constr
+ | Kufo
+
+let destructurate_prop t =
+ let c, args = decompose_app t in
+ match kind_of_term c, args with
+ | _, [_;_;_] when c = build_coq_eq () -> Kapp (Eq,args)
+ | _, [_;_] when c = Lazy.force coq_neq -> Kapp (Neq,args)
+ | _, [_;_] when c = Lazy.force coq_Zne -> Kapp (Zne,args)
+ | _, [_;_] when c = Lazy.force coq_Zle -> Kapp (Zle,args)
+ | _, [_;_] when c = Lazy.force coq_Zlt -> Kapp (Zlt,args)
+ | _, [_;_] when c = Lazy.force coq_Zge -> Kapp (Zge,args)
+ | _, [_;_] when c = Lazy.force coq_Zgt -> Kapp (Zgt,args)
+ | _, [_;_] when c = build_coq_and () -> Kapp (And,args)
+ | _, [_;_] when c = build_coq_or () -> Kapp (Or,args)
+ | _, [_;_] when c = Lazy.force coq_iff -> Kapp (Iff, args)
+ | _, [_] when c = build_coq_not () -> Kapp (Not,args)
+ | _, [] when c = build_coq_False () -> Kapp (False,args)
+ | _, [] when c = build_coq_True () -> Kapp (True,args)
+ | _, [_;_] when c = Lazy.force coq_le -> Kapp (Le,args)
+ | _, [_;_] when c = Lazy.force coq_lt -> Kapp (Lt,args)
+ | _, [_;_] when c = Lazy.force coq_ge -> Kapp (Ge,args)
+ | _, [_;_] when c = Lazy.force coq_gt -> Kapp (Gt,args)
+ | Const sp, args ->
+ Kapp (Other (string_of_id (basename_of_global (ConstRef sp))),args)
+ | Construct csp , args ->
+ Kapp (Other (string_of_id (basename_of_global (ConstructRef csp))), args)
+ | Ind isp, args ->
+ Kapp (Other (string_of_id (basename_of_global (IndRef isp))),args)
+ | Var id,[] -> Kvar id
+ | Prod (Anonymous,typ,body), [] -> Kimp(typ,body)
+ | Prod (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal"
+ | _ -> Kufo
+
+let destructurate_type t =
+ let c, args = decompose_app t in
+ match kind_of_term c, args with
+ | _, [] when c = Lazy.force coq_Z -> Kapp (Z,args)
+ | _, [] when c = Lazy.force coq_nat -> Kapp (Nat,args)
+ | _ -> Kufo
+
+let destructurate_term t =
+ let c, args = decompose_app t in
+ match kind_of_term c, args with
+ | _, [_;_] when c = Lazy.force coq_Zplus -> Kapp (Zplus,args)
+ | _, [_;_] when c = Lazy.force coq_Zmult -> Kapp (Zmult,args)
+ | _, [_;_] when c = Lazy.force coq_Zminus -> Kapp (Zminus,args)
+ | _, [_] when c = Lazy.force coq_Zsucc -> Kapp (Zsucc,args)
+ | _, [_] when c = Lazy.force coq_Zopp -> Kapp (Zopp,args)
+ | _, [_;_] when c = Lazy.force coq_plus -> Kapp (Plus,args)
+ | _, [_;_] when c = Lazy.force coq_mult -> Kapp (Mult,args)
+ | _, [_;_] when c = Lazy.force coq_minus -> Kapp (Minus,args)
+ | _, [_] when c = Lazy.force coq_pred -> Kapp (Pred,args)
+ | _, [_] when c = Lazy.force coq_S -> Kapp (S,args)
+ | _, [] when c = Lazy.force coq_O -> Kapp (O,args)
+ | _, [_] when c = Lazy.force coq_Zpos -> Kapp (Zneg,args)
+ | _, [_] when c = Lazy.force coq_Zneg -> Kapp (Zpos,args)
+ | _, [] when c = Lazy.force coq_Z0 -> Kapp (Z0,args)
+ | _, [_] when c = Lazy.force coq_Z_of_nat -> Kapp (Z_of_nat,args)
+ | Var id,[] -> Kvar id
+ | _ -> Kufo
+
+let recognize_number t =
+ let rec loop t =
+ match decompose_app t with
+ | f, [t] when f = Lazy.force coq_xI -> one + two * loop t
+ | f, [t] when f = Lazy.force coq_xO -> two * loop t
+ | f, [] when f = Lazy.force coq_xH -> one
+ | _ -> failwith "not a number"
+ in
+ match decompose_app t with
+ | f, [t] when f = Lazy.force coq_Zpos -> loop t
+ | f, [t] when f = Lazy.force coq_Zneg -> neg (loop t)
+ | f, [] when f = Lazy.force coq_Z0 -> zero
+ | _ -> failwith "not a number"
+
+type constr_path =
+ | P_APP of int
+ (* Abstraction and product *)
+ | P_BODY
+ | P_TYPE
+ (* Case *)
+ | P_BRANCH of int
+ | P_ARITY
+ | P_ARG
+
+let context operation path (t : constr) =
+ let rec loop i p0 t =
+ match (p0,kind_of_term t) with
+ | (p, Cast (c,k,t)) -> mkCast (loop i p c,k,t)
+ | ([], _) -> operation i t
+ | ((P_APP n :: p), App (f,v)) ->
+ let v' = Array.copy v in
+ v'.(pred n) <- loop i p v'.(pred n); mkApp (f, v')
+ | ((P_BRANCH n :: p), Case (ci,q,c,v)) ->
+ (* avant, y avait mkApp... anyway, BRANCH seems nowhere used *)
+ let v' = Array.copy v in
+ v'.(n) <- loop i p v'.(n); (mkCase (ci,q,c,v'))
+ | ((P_ARITY :: p), App (f,l)) ->
+ appvect (loop i p f,l)
+ | ((P_ARG :: p), App (f,v)) ->
+ let v' = Array.copy v in
+ v'.(0) <- loop i p v'.(0); mkApp (f,v')
+ | (p, Fix ((_,n as ln),(tys,lna,v))) ->
+ let l = Array.length v in
+ let v' = Array.copy v in
+ v'.(n)<- loop (Pervasives.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v')))
+ | ((P_BODY :: p), Prod (n,t,c)) ->
+ (mkProd (n,t,loop (succ i) p c))
+ | ((P_BODY :: p), Lambda (n,t,c)) ->
+ (mkLambda (n,t,loop (succ i) p c))
+ | ((P_BODY :: p), LetIn (n,b,t,c)) ->
+ (mkLetIn (n,b,t,loop (succ i) p c))
+ | ((P_TYPE :: p), Prod (n,t,c)) ->
+ (mkProd (n,loop i p t,c))
+ | ((P_TYPE :: p), Lambda (n,t,c)) ->
+ (mkLambda (n,loop i p t,c))
+ | ((P_TYPE :: p), LetIn (n,b,t,c)) ->
+ (mkLetIn (n,b,loop i p t,c))
+ | (p, _) ->
+ ppnl (Printer.pr_lconstr t);
+ failwith ("abstract_path " ^ string_of_int(List.length p))
+ in
+ loop 1 path t
+
+let occurence path (t : constr) =
+ let rec loop p0 t = match (p0,kind_of_term t) with
+ | (p, Cast (c,_,_)) -> loop p c
+ | ([], _) -> t
+ | ((P_APP n :: p), App (f,v)) -> loop p v.(pred n)
+ | ((P_BRANCH n :: p), Case (_,_,_,v)) -> loop p v.(n)
+ | ((P_ARITY :: p), App (f,_)) -> loop p f
+ | ((P_ARG :: p), App (f,v)) -> loop p v.(0)
+ | (p, Fix((_,n) ,(_,_,v))) -> loop p v.(n)
+ | ((P_BODY :: p), Prod (n,t,c)) -> loop p c
+ | ((P_BODY :: p), Lambda (n,t,c)) -> loop p c
+ | ((P_BODY :: p), LetIn (n,b,t,c)) -> loop p c
+ | ((P_TYPE :: p), Prod (n,term,c)) -> loop p term
+ | ((P_TYPE :: p), Lambda (n,term,c)) -> loop p term
+ | ((P_TYPE :: p), LetIn (n,b,term,c)) -> loop p term
+ | (p, _) ->
+ ppnl (Printer.pr_lconstr t);
+ failwith ("occurence " ^ string_of_int(List.length p))
+ in
+ loop path t
+
+let abstract_path typ path t =
+ let term_occur = ref (mkRel 0) in
+ let abstract = context (fun i t -> term_occur:= t; mkRel i) path t in
+ mkLambda (Name (id_of_string "x"), typ, abstract), !term_occur
+
+let focused_simpl path gl =
+ let newc = context (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
+ convert_concl_no_check newc DEFAULTcast gl
+
+let focused_simpl path = simpl_time (focused_simpl path)
+
+type oformula =
+ | Oplus of oformula * oformula
+ | Oinv of oformula
+ | Otimes of oformula * oformula
+ | Oatom of identifier
+ | Oz of bigint
+ | Oufo of constr
+
+let rec oprint = function
+ | Oplus(t1,t2) ->
+ print_string "("; oprint t1; print_string "+";
+ oprint t2; print_string ")"
+ | Oinv t -> print_string "~"; oprint t
+ | Otimes (t1,t2) ->
+ print_string "("; oprint t1; print_string "*";
+ oprint t2; print_string ")"
+ | Oatom s -> print_string (string_of_id s)
+ | Oz i -> print_string (string_of_bigint i)
+ | Oufo f -> print_string "?"
+
+let rec weight = function
+ | Oatom c -> intern_id c
+ | Oz _ -> -1
+ | Oinv c -> weight c
+ | Otimes(c,_) -> weight c
+ | Oplus _ -> failwith "weight"
+ | Oufo _ -> -1
+
+let rec val_of = function
+ | Oatom c -> mkVar c
+ | Oz c -> mk_integer c
+ | Oinv c -> mkApp (Lazy.force coq_Zopp, [| val_of c |])
+ | Otimes (t1,t2) -> mkApp (Lazy.force coq_Zmult, [| val_of t1; val_of t2 |])
+ | Oplus(t1,t2) -> mkApp (Lazy.force coq_Zplus, [| val_of t1; val_of t2 |])
+ | Oufo c -> c
+
+let compile name kind =
+ let rec loop accu = function
+ | Oplus(Otimes(Oatom v,Oz n),r) -> loop ({v=intern_id v; c=n} :: accu) r
+ | Oz n ->
+ let id = new_id () in
+ tag_hypothesis name id;
+ {kind = kind; body = List.rev accu; constant = n; id = id}
+ | _ -> anomaly "compile_equation"
+ in
+ loop []
+
+let rec decompile af =
+ let rec loop = function
+ | ({v=v; c=n}::r) -> Oplus(Otimes(Oatom (unintern_id v),Oz n),loop r)
+ | [] -> Oz af.constant
+ in
+ loop af.body
+
+let mkNewMeta () = mkMeta (Evarutil.new_meta())
+
+let clever_rewrite_base_poly typ p result theorem gl =
+ let full = pf_concl gl in
+ let (abstracted,occ) = abstract_path typ (List.rev p) full in
+ let t =
+ applist
+ (mkLambda
+ (Name (id_of_string "P"),
+ mkArrow typ mkProp,
+ mkLambda
+ (Name (id_of_string "H"),
+ applist (mkRel 1,[result]),
+ mkApp (Lazy.force coq_eq_ind_r,
+ [| typ; result; mkRel 2; mkRel 1; occ; theorem |]))),
+ [abstracted])
+ in
+ exact (applist(t,[mkNewMeta()])) gl
+
+let clever_rewrite_base p result theorem gl =
+ clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem gl
+
+let clever_rewrite_base_nat p result theorem gl =
+ clever_rewrite_base_poly (Lazy.force coq_nat) p result theorem gl
+
+let clever_rewrite_gen p result (t,args) =
+ let theorem = applist(t, args) in
+ clever_rewrite_base p result theorem
+
+let clever_rewrite_gen_nat p result (t,args) =
+ let theorem = applist(t, args) in
+ clever_rewrite_base_nat p result theorem
+
+let clever_rewrite p vpath t gl =
+ let full = pf_concl gl in
+ let (abstracted,occ) = abstract_path (Lazy.force coq_Z) (List.rev p) full in
+ let vargs = List.map (fun p -> occurence p occ) vpath in
+ let t' = applist(t, (vargs @ [abstracted])) in
+ exact (applist(t',[mkNewMeta()])) gl
+
+let rec shuffle p (t1,t2) =
+ match t1,t2 with
+ | Oplus(l1,r1), Oplus(l2,r2) ->
+ if weight l1 > weight l2 then
+ let (tac,t') = shuffle (P_APP 2 :: p) (r1,t2) in
+ (clever_rewrite p [[P_APP 1;P_APP 1];
+ [P_APP 1; P_APP 2];[P_APP 2]]
+ (Lazy.force coq_fast_Zplus_assoc_reverse)
+ :: tac,
+ Oplus(l1,t'))
+ else
+ let (tac,t') = shuffle (P_APP 2 :: p) (t1,r2) in
+ (clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 1];[P_APP 2;P_APP 2]]
+ (Lazy.force coq_fast_Zplus_permute)
+ :: tac,
+ Oplus(l2,t'))
+ | Oplus(l1,r1), t2 ->
+ if weight l1 > weight t2 then
+ let (tac,t') = shuffle (P_APP 2 :: p) (r1,t2) in
+ clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]]
+ (Lazy.force coq_fast_Zplus_assoc_reverse)
+ :: tac,
+ Oplus(l1, t')
+ else
+ [clever_rewrite p [[P_APP 1];[P_APP 2]]
+ (Lazy.force coq_fast_Zplus_comm)],
+ Oplus(t2,t1)
+ | t1,Oplus(l2,r2) ->
+ if weight l2 > weight t1 then
+ let (tac,t') = shuffle (P_APP 2 :: p) (t1,r2) in
+ clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 1];[P_APP 2;P_APP 2]]
+ (Lazy.force coq_fast_Zplus_permute)
+ :: tac,
+ Oplus(l2,t')
+ else [],Oplus(t1,t2)
+ | Oz t1,Oz t2 ->
+ [focused_simpl p], Oz(Bigint.add t1 t2)
+ | t1,t2 ->
+ if weight t1 < weight t2 then
+ [clever_rewrite p [[P_APP 1];[P_APP 2]]
+ (Lazy.force coq_fast_Zplus_comm)],
+ Oplus(t2,t1)
+ else [],Oplus(t1,t2)
+
+let rec shuffle_mult p_init k1 e1 k2 e2 =
+ let rec loop p = function
+ | (({c=c1;v=v1}::l1) as l1'),(({c=c2;v=v2}::l2) as l2') ->
+ if v1 = v2 then
+ let tac =
+ clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1];
+ [P_APP 1; P_APP 1; P_APP 1; P_APP 2];
+ [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
+ [P_APP 1; P_APP 1; P_APP 2];
+ [P_APP 2; P_APP 1; P_APP 2];
+ [P_APP 1; P_APP 2];
+ [P_APP 2; P_APP 2]]
+ (Lazy.force coq_fast_OMEGA10)
+ in
+ if Bigint.add (Bigint.mult k1 c1) (Bigint.mult k2 c2) =? zero then
+ let tac' =
+ clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
+ (Lazy.force coq_fast_Zred_factor5) in
+ tac :: focused_simpl (P_APP 1::P_APP 2:: p) :: tac' ::
+ loop p (l1,l2)
+ else tac :: loop (P_APP 2 :: p) (l1,l2)
+ else if v1 > v2 then
+ clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1];
+ [P_APP 1; P_APP 1; P_APP 1; P_APP 2];
+ [P_APP 1; P_APP 1; P_APP 2];
+ [P_APP 2];
+ [P_APP 1; P_APP 2]]
+ (Lazy.force coq_fast_OMEGA11) ::
+ loop (P_APP 2 :: p) (l1,l2')
+ else
+ clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1];
+ [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
+ [P_APP 1];
+ [P_APP 2; P_APP 1; P_APP 2];
+ [P_APP 2; P_APP 2]]
+ (Lazy.force coq_fast_OMEGA12) ::
+ loop (P_APP 2 :: p) (l1',l2)
+ | ({c=c1;v=v1}::l1), [] ->
+ clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1];
+ [P_APP 1; P_APP 1; P_APP 1; P_APP 2];
+ [P_APP 1; P_APP 1; P_APP 2];
+ [P_APP 2];
+ [P_APP 1; P_APP 2]]
+ (Lazy.force coq_fast_OMEGA11) ::
+ loop (P_APP 2 :: p) (l1,[])
+ | [],({c=c2;v=v2}::l2) ->
+ clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1];
+ [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
+ [P_APP 1];
+ [P_APP 2; P_APP 1; P_APP 2];
+ [P_APP 2; P_APP 2]]
+ (Lazy.force coq_fast_OMEGA12) ::
+ loop (P_APP 2 :: p) ([],l2)
+ | [],[] -> [focused_simpl p_init]
+ in
+ loop p_init (e1,e2)
+
+let rec shuffle_mult_right p_init e1 k2 e2 =
+ let rec loop p = function
+ | (({c=c1;v=v1}::l1) as l1'),(({c=c2;v=v2}::l2) as l2') ->
+ if v1 = v2 then
+ let tac =
+ clever_rewrite p
+ [[P_APP 1; P_APP 1; P_APP 1];
+ [P_APP 1; P_APP 1; P_APP 2];
+ [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
+ [P_APP 1; P_APP 2];
+ [P_APP 2; P_APP 1; P_APP 2];
+ [P_APP 2; P_APP 2]]
+ (Lazy.force coq_fast_OMEGA15)
+ in
+ if Bigint.add c1 (Bigint.mult k2 c2) =? zero then
+ let tac' =
+ clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
+ (Lazy.force coq_fast_Zred_factor5)
+ in
+ tac :: focused_simpl (P_APP 1::P_APP 2:: p) :: tac' ::
+ loop p (l1,l2)
+ else tac :: loop (P_APP 2 :: p) (l1,l2)
+ else if v1 > v2 then
+ clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]]
+ (Lazy.force coq_fast_Zplus_assoc_reverse) ::
+ loop (P_APP 2 :: p) (l1,l2')
+ else
+ clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1];
+ [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
+ [P_APP 1];
+ [P_APP 2; P_APP 1; P_APP 2];
+ [P_APP 2; P_APP 2]]
+ (Lazy.force coq_fast_OMEGA12) ::
+ loop (P_APP 2 :: p) (l1',l2)
+ | ({c=c1;v=v1}::l1), [] ->
+ clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]]
+ (Lazy.force coq_fast_Zplus_assoc_reverse) ::
+ loop (P_APP 2 :: p) (l1,[])
+ | [],({c=c2;v=v2}::l2) ->
+ clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1];
+ [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
+ [P_APP 1];
+ [P_APP 2; P_APP 1; P_APP 2];
+ [P_APP 2; P_APP 2]]
+ (Lazy.force coq_fast_OMEGA12) ::
+ loop (P_APP 2 :: p) ([],l2)
+ | [],[] -> [focused_simpl p_init]
+ in
+ loop p_init (e1,e2)
+
+let rec shuffle_cancel p = function
+ | [] -> [focused_simpl p]
+ | ({c=c1}::l1) ->
+ let tac =
+ clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1];[P_APP 1; P_APP 2];
+ [P_APP 2; P_APP 2];
+ [P_APP 1; P_APP 1; P_APP 2; P_APP 1]]
+ (if c1 >? zero then
+ (Lazy.force coq_fast_OMEGA13)
+ else
+ (Lazy.force coq_fast_OMEGA14))
+ in
+ tac :: shuffle_cancel p l1
+
+let rec scalar p n = function
+ | Oplus(t1,t2) ->
+ let tac1,t1' = scalar (P_APP 1 :: p) n t1 and
+ tac2,t2' = scalar (P_APP 2 :: p) n t2 in
+ clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]]
+ (Lazy.force coq_fast_Zmult_plus_distr_l) ::
+ (tac1 @ tac2), Oplus(t1',t2')
+ | Oinv t ->
+ [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
+ (Lazy.force coq_fast_Zmult_opp_comm);
+ focused_simpl (P_APP 2 :: p)], Otimes(t,Oz(neg n))
+ | Otimes(t1,Oz x) ->
+ [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]]
+ (Lazy.force coq_fast_Zmult_assoc_reverse);
+ focused_simpl (P_APP 2 :: p)],
+ Otimes(t1,Oz (n*x))
+ | Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products"
+ | (Oatom _ as t) -> [], Otimes(t,Oz n)
+ | Oz i -> [focused_simpl p],Oz(n*i)
+ | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zmult, [| mk_integer n; c |]))
+
+let rec scalar_norm p_init =
+ let rec loop p = function
+ | [] -> [focused_simpl p_init]
+ | (_::l) ->
+ clever_rewrite p
+ [[P_APP 1; P_APP 1; P_APP 1];[P_APP 1; P_APP 1; P_APP 2];
+ [P_APP 1; P_APP 2];[P_APP 2]]
+ (Lazy.force coq_fast_OMEGA16) :: loop (P_APP 2 :: p) l
+ in
+ loop p_init
+
+let rec norm_add p_init =
+ let rec loop p = function
+ | [] -> [focused_simpl p_init]
+ | _:: l ->
+ clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]]
+ (Lazy.force coq_fast_Zplus_assoc_reverse) ::
+ loop (P_APP 2 :: p) l
+ in
+ loop p_init
+
+let rec scalar_norm_add p_init =
+ let rec loop p = function
+ | [] -> [focused_simpl p_init]
+ | _ :: l ->
+ clever_rewrite p
+ [[P_APP 1; P_APP 1; P_APP 1; P_APP 1];
+ [P_APP 1; P_APP 1; P_APP 1; P_APP 2];
+ [P_APP 1; P_APP 1; P_APP 2]; [P_APP 2]; [P_APP 1; P_APP 2]]
+ (Lazy.force coq_fast_OMEGA11) :: loop (P_APP 2 :: p) l
+ in
+ loop p_init
+
+let rec negate p = function
+ | Oplus(t1,t2) ->
+ let tac1,t1' = negate (P_APP 1 :: p) t1 and
+ tac2,t2' = negate (P_APP 2 :: p) t2 in
+ clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]]
+ (Lazy.force coq_fast_Zopp_plus_distr) ::
+ (tac1 @ tac2),
+ Oplus(t1',t2')
+ | Oinv t ->
+ [clever_rewrite p [[P_APP 1;P_APP 1]] (Lazy.force coq_fast_Zopp_involutive)], t
+ | Otimes(t1,Oz x) ->
+ [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]]
+ (Lazy.force coq_fast_Zopp_mult_distr_r);
+ focused_simpl (P_APP 2 :: p)], Otimes(t1,Oz (neg x))
+ | Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products"
+ | (Oatom _ as t) ->
+ let r = Otimes(t,Oz(negone)) in
+ [clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1)], r
+ | Oz i -> [focused_simpl p],Oz(neg i)
+ | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zopp, [| c |]))
+
+let rec transform p t =
+ let default isnat t' =
+ try
+ let v,th,_ = find_constr t' in
+ [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v
+ with _ ->
+ let v = new_identifier_var ()
+ and th = new_identifier () in
+ hide_constr t' v th isnat;
+ [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v
+ in
+ try match destructurate_term t with
+ | Kapp(Zplus,[t1;t2]) ->
+ let tac1,t1' = transform (P_APP 1 :: p) t1
+ and tac2,t2' = transform (P_APP 2 :: p) t2 in
+ let tac,t' = shuffle p (t1',t2') in
+ tac1 @ tac2 @ tac, t'
+ | Kapp(Zminus,[t1;t2]) ->
+ let tac,t =
+ transform p
+ (mkApp (Lazy.force coq_Zplus,
+ [| t1; (mkApp (Lazy.force coq_Zopp, [| t2 |])) |])) in
+ unfold sp_Zminus :: tac,t
+ | Kapp(Zsucc,[t1]) ->
+ let tac,t = transform p (mkApp (Lazy.force coq_Zplus,
+ [| t1; mk_integer one |])) in
+ unfold sp_Zsucc :: tac,t
+ | Kapp(Zmult,[t1;t2]) ->
+ let tac1,t1' = transform (P_APP 1 :: p) t1
+ and tac2,t2' = transform (P_APP 2 :: p) t2 in
+ begin match t1',t2' with
+ | (_,Oz n) -> let tac,t' = scalar p n t1' in tac1 @ tac2 @ tac,t'
+ | (Oz n,_) ->
+ let sym =
+ clever_rewrite p [[P_APP 1];[P_APP 2]]
+ (Lazy.force coq_fast_Zmult_comm) in
+ let tac,t' = scalar p n t2' in tac1 @ tac2 @ (sym :: tac),t'
+ | _ -> default false t
+ end
+ | Kapp((Zpos|Zneg|Z0),_) ->
+ (try ([],Oz(recognize_number t)) with _ -> default false t)
+ | Kvar s -> [],Oatom s
+ | Kapp(Zopp,[t]) ->
+ let tac,t' = transform (P_APP 1 :: p) t in
+ let tac',t'' = negate p t' in
+ tac @ tac', t''
+ | Kapp(Z_of_nat,[t']) -> default true t'
+ | _ -> default false t
+ with e when catchable_exception e -> default false t
+
+let shrink_pair p f1 f2 =
+ match f1,f2 with
+ | Oatom v,Oatom _ ->
+ let r = Otimes(Oatom v,Oz two) in
+ clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zred_factor1), r
+ | Oatom v, Otimes(_,c2) ->
+ let r = Otimes(Oatom v,Oplus(c2,Oz one)) in
+ clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 2]]
+ (Lazy.force coq_fast_Zred_factor2), r
+ | Otimes (v1,c1),Oatom v ->
+ let r = Otimes(Oatom v,Oplus(c1,Oz one)) in
+ clever_rewrite p [[P_APP 2];[P_APP 1;P_APP 2]]
+ (Lazy.force coq_fast_Zred_factor3), r
+ | Otimes (Oatom v,c1),Otimes (v2,c2) ->
+ let r = Otimes(Oatom v,Oplus(c1,c2)) in
+ clever_rewrite p
+ [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2;P_APP 2]]
+ (Lazy.force coq_fast_Zred_factor4),r
+ | t1,t2 ->
+ begin
+ oprint t1; print_newline (); oprint t2; print_newline ();
+ flush Pervasives.stdout; error "shrink.1"
+ end
+
+let reduce_factor p = function
+ | Oatom v ->
+ let r = Otimes(Oatom v,Oz one) in
+ [clever_rewrite p [[]] (Lazy.force coq_fast_Zred_factor0)],r
+ | Otimes(Oatom v,Oz n) as f -> [],f
+ | Otimes(Oatom v,c) ->
+ let rec compute = function
+ | Oz n -> n
+ | Oplus(t1,t2) -> Bigint.add (compute t1) (compute t2)
+ | _ -> error "condense.1"
+ in
+ [focused_simpl (P_APP 2 :: p)], Otimes(Oatom v,Oz(compute c))
+ | t -> oprint t; error "reduce_factor.1"
+
+let rec condense p = function
+ | Oplus(f1,(Oplus(f2,r) as t)) ->
+ if weight f1 = weight f2 then begin
+ let shrink_tac,t = shrink_pair (P_APP 1 :: p) f1 f2 in
+ let assoc_tac =
+ clever_rewrite p
+ [[P_APP 1];[P_APP 2;P_APP 1];[P_APP 2;P_APP 2]]
+ (Lazy.force coq_fast_Zplus_assoc) in
+ let tac_list,t' = condense p (Oplus(t,r)) in
+ (assoc_tac :: shrink_tac :: tac_list), t'
+ end else begin
+ let tac,f = reduce_factor (P_APP 1 :: p) f1 in
+ let tac',t' = condense (P_APP 2 :: p) t in
+ (tac @ tac'), Oplus(f,t')
+ end
+ | Oplus(f1,Oz n) ->
+ let tac,f1' = reduce_factor (P_APP 1 :: p) f1 in tac,Oplus(f1',Oz n)
+ | Oplus(f1,f2) ->
+ if weight f1 = weight f2 then begin
+ let tac_shrink,t = shrink_pair p f1 f2 in
+ let tac,t' = condense p t in
+ tac_shrink :: tac,t'
+ end else begin
+ let tac,f = reduce_factor (P_APP 1 :: p) f1 in
+ let tac',t' = condense (P_APP 2 :: p) f2 in
+ (tac @ tac'),Oplus(f,t')
+ end
+ | Oz _ as t -> [],t
+ | t ->
+ let tac,t' = reduce_factor p t in
+ let final = Oplus(t',Oz zero) in
+ let tac' = clever_rewrite p [[]] (Lazy.force coq_fast_Zred_factor6) in
+ tac @ [tac'], final
+
+let rec clear_zero p = function
+ | Oplus(Otimes(Oatom v,Oz n),r) when n =? zero ->
+ let tac =
+ clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
+ (Lazy.force coq_fast_Zred_factor5) in
+ let tac',t = clear_zero p r in
+ tac :: tac',t
+ | Oplus(f,r) ->
+ let tac,t = clear_zero (P_APP 2 :: p) r in tac,Oplus(f,t)
+ | t -> [],t
+
+let replay_history tactic_normalisation =
+ let aux = id_of_string "auxiliary" in
+ let aux1 = id_of_string "auxiliary_1" in
+ let aux2 = id_of_string "auxiliary_2" in
+ let izero = mk_integer zero in
+ let rec loop t =
+ match t with
+ | HYP e :: l ->
+ begin
+ try
+ tclTHEN
+ (List.assoc (hyp_of_tag e.id) tactic_normalisation)
+ (loop l)
+ with Not_found -> loop l end
+ | NEGATE_CONTRADICT (e2,e1,b) :: l ->
+ let eq1 = decompile e1
+ and eq2 = decompile e2 in
+ let id1 = hyp_of_tag e1.id
+ and id2 = hyp_of_tag e2.id in
+ let k = if b then negone else one in
+ let p_initial = [P_APP 1;P_TYPE] in
+ let tac= shuffle_mult_right p_initial e1.body k e2.body in
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_OMEGA17, [|
+ val_of eq1;
+ val_of eq2;
+ mk_integer k;
+ mkVar id1; mkVar id2 |])]);
+ (mk_then tac);
+ (intros_using [aux]);
+ (resolve_id aux);
+ reflexivity
+ ]
+ | CONTRADICTION (e1,e2) :: l ->
+ let eq1 = decompile e1
+ and eq2 = decompile e2 in
+ let p_initial = [P_APP 2;P_TYPE] in
+ let tac = shuffle_cancel p_initial e1.body in
+ let solve_le =
+ let not_sup_sup = mkApp (build_coq_eq (), [|
+ Lazy.force coq_comparison;
+ Lazy.force coq_Gt;
+ Lazy.force coq_Gt |])
+ in
+ tclTHENS
+ (tclTHENLIST [
+ (unfold sp_Zle);
+ (simpl_in_concl);
+ intro;
+ (absurd not_sup_sup) ])
+ [ assumption ; reflexivity ]
+ in
+ let theorem =
+ mkApp (Lazy.force coq_OMEGA2, [|
+ val_of eq1; val_of eq2;
+ mkVar (hyp_of_tag e1.id);
+ mkVar (hyp_of_tag e2.id) |])
+ in
+ tclTHEN (tclTHEN (generalize_tac [theorem]) (mk_then tac)) (solve_le)
+ | DIVIDE_AND_APPROX (e1,e2,k,d) :: l ->
+ let id = hyp_of_tag e1.id in
+ let eq1 = val_of(decompile e1)
+ and eq2 = val_of(decompile e2) in
+ let kk = mk_integer k
+ and dd = mk_integer d in
+ let rhs = mk_plus (mk_times eq2 kk) dd in
+ let state_eg = mk_eq eq1 rhs in
+ let tac = scalar_norm_add [P_APP 3] e2.body in
+ tclTHENS
+ (cut state_eg)
+ [ tclTHENS
+ (tclTHENLIST [
+ (intros_using [aux]);
+ (generalize_tac
+ [mkApp (Lazy.force coq_OMEGA1,
+ [| eq1; rhs; mkVar aux; mkVar id |])]);
+ (clear [aux;id]);
+ (intros_using [id]);
+ (cut (mk_gt kk dd)) ])
+ [ tclTHENS
+ (cut (mk_gt kk izero))
+ [ tclTHENLIST [
+ (intros_using [aux1; aux2]);
+ (generalize_tac
+ [mkApp (Lazy.force coq_Zmult_le_approx,
+ [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])]);
+ (clear [aux1;aux2;id]);
+ (intros_using [id]);
+ (loop l) ];
+ tclTHENLIST [
+ (unfold sp_Zgt);
+ (simpl_in_concl);
+ reflexivity ] ];
+ tclTHENLIST [ (unfold sp_Zgt); simpl_in_concl; reflexivity ]
+ ];
+ tclTHEN (mk_then tac) reflexivity ]
+
+ | NOT_EXACT_DIVIDE (e1,k) :: l ->
+ let c = floor_div e1.constant k in
+ let d = Bigint.sub e1.constant (Bigint.mult c k) in
+ let e2 = {id=e1.id; kind=EQUA;constant = c;
+ body = map_eq_linear (fun c -> c / k) e1.body } in
+ let eq2 = val_of(decompile e2) in
+ let kk = mk_integer k
+ and dd = mk_integer d in
+ let tac = scalar_norm_add [P_APP 2] e2.body in
+ tclTHENS
+ (cut (mk_gt dd izero))
+ [ tclTHENS (cut (mk_gt kk dd))
+ [tclTHENLIST [
+ (intros_using [aux2;aux1]);
+ (generalize_tac
+ [mkApp (Lazy.force coq_OMEGA4,
+ [| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]);
+ (clear [aux1;aux2]);
+ (unfold sp_not);
+ (intros_using [aux]);
+ (resolve_id aux);
+ (mk_then tac);
+ assumption ] ;
+ tclTHENLIST [
+ (unfold sp_Zgt);
+ simpl_in_concl;
+ reflexivity ] ];
+ tclTHENLIST [
+ (unfold sp_Zgt);
+ simpl_in_concl;
+ reflexivity ] ]
+ | EXACT_DIVIDE (e1,k) :: l ->
+ let id = hyp_of_tag e1.id in
+ let e2 = map_eq_afine (fun c -> c / k) e1 in
+ let eq1 = val_of(decompile e1)
+ and eq2 = val_of(decompile e2) in
+ let kk = mk_integer k in
+ let state_eq = mk_eq eq1 (mk_times eq2 kk) in
+ if e1.kind = DISE then
+ let tac = scalar_norm [P_APP 3] e2.body in
+ tclTHENS
+ (cut state_eq)
+ [tclTHENLIST [
+ (intros_using [aux1]);
+ (generalize_tac
+ [mkApp (Lazy.force coq_OMEGA18,
+ [| eq1;eq2;kk;mkVar aux1; mkVar id |])]);
+ (clear [aux1;id]);
+ (intros_using [id]);
+ (loop l) ];
+ tclTHEN (mk_then tac) reflexivity ]
+ else
+ let tac = scalar_norm [P_APP 3] e2.body in
+ tclTHENS (cut state_eq)
+ [
+ tclTHENS
+ (cut (mk_gt kk izero))
+ [tclTHENLIST [
+ (intros_using [aux2;aux1]);
+ (generalize_tac
+ [mkApp (Lazy.force coq_OMEGA3,
+ [| eq1; eq2; kk; mkVar aux2; mkVar aux1;mkVar id|])]);
+ (clear [aux1;aux2;id]);
+ (intros_using [id]);
+ (loop l) ];
+ tclTHENLIST [
+ (unfold sp_Zgt);
+ simpl_in_concl;
+ reflexivity ] ];
+ tclTHEN (mk_then tac) reflexivity ]
+ | (MERGE_EQ(e3,e1,e2)) :: l ->
+ let id = new_identifier () in
+ tag_hypothesis id e3;
+ let id1 = hyp_of_tag e1.id
+ and id2 = hyp_of_tag e2 in
+ let eq1 = val_of(decompile e1)
+ and eq2 = val_of (decompile (negate_eq e1)) in
+ let tac =
+ clever_rewrite [P_APP 3] [[P_APP 1]]
+ (Lazy.force coq_fast_Zopp_eq_mult_neg_1) ::
+ scalar_norm [P_APP 3] e1.body
+ in
+ tclTHENS
+ (cut (mk_eq eq1 (mk_inv eq2)))
+ [tclTHENLIST [
+ (intros_using [aux]);
+ (generalize_tac [mkApp (Lazy.force coq_OMEGA8,
+ [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]);
+ (clear [id1;id2;aux]);
+ (intros_using [id]);
+ (loop l) ];
+ tclTHEN (mk_then tac) reflexivity]
+
+ | STATE {st_new_eq=e;st_def=def;st_orig=orig;st_coef=m;st_var=v} :: l ->
+ let id = new_identifier ()
+ and id2 = hyp_of_tag orig.id in
+ tag_hypothesis id e.id;
+ let eq1 = val_of(decompile def)
+ and eq2 = val_of(decompile orig) in
+ let vid = unintern_id v in
+ let theorem =
+ mkApp (build_coq_ex (), [|
+ Lazy.force coq_Z;
+ mkLambda
+ (Name vid,
+ Lazy.force coq_Z,
+ mk_eq (mkRel 1) eq1) |])
+ in
+ let mm = mk_integer m in
+ let p_initial = [P_APP 2;P_TYPE] in
+ let tac =
+ clever_rewrite (P_APP 1 :: P_APP 1 :: P_APP 2 :: p_initial)
+ [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1) ::
+ shuffle_mult_right p_initial
+ orig.body m ({c= negone;v= v}::def.body) in
+ tclTHENS
+ (cut theorem)
+ [tclTHENLIST [
+ (intros_using [aux]);
+ (elim_id aux);
+ (clear [aux]);
+ (intros_using [vid; aux]);
+ (generalize_tac
+ [mkApp (Lazy.force coq_OMEGA9,
+ [| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]);
+ (mk_then tac);
+ (clear [aux]);
+ (intros_using [id]);
+ (loop l) ];
+ tclTHEN (exists_tac eq1) reflexivity ]
+ | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l ->
+ let id1 = new_identifier ()
+ and id2 = new_identifier () in
+ tag_hypothesis id1 e1; tag_hypothesis id2 e2;
+ let id = hyp_of_tag e.id in
+ let tac1 = norm_add [P_APP 2;P_TYPE] e.body in
+ let tac2 = scalar_norm_add [P_APP 2;P_TYPE] e.body in
+ let eq = val_of(decompile e) in
+ tclTHENS
+ (simplest_elim (applist (Lazy.force coq_OMEGA19, [eq; mkVar id])))
+ [tclTHENLIST [ (mk_then tac1); (intros_using [id1]); (loop act1) ];
+ tclTHENLIST [ (mk_then tac2); (intros_using [id2]); (loop act2) ]]
+ | SUM(e3,(k1,e1),(k2,e2)) :: l ->
+ let id = new_identifier () in
+ tag_hypothesis id e3;
+ let id1 = hyp_of_tag e1.id
+ and id2 = hyp_of_tag e2.id in
+ let eq1 = val_of(decompile e1)
+ and eq2 = val_of(decompile e2) in
+ if k1 =? one & e2.kind = EQUA then
+ let tac_thm =
+ match e1.kind with
+ | EQUA -> Lazy.force coq_OMEGA5
+ | INEQ -> Lazy.force coq_OMEGA6
+ | DISE -> Lazy.force coq_OMEGA20
+ in
+ let kk = mk_integer k2 in
+ let p_initial =
+ if e1.kind=DISE then [P_APP 1; P_TYPE] else [P_APP 2; P_TYPE] in
+ let tac = shuffle_mult_right p_initial e1.body k2 e2.body in
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]);
+ (mk_then tac);
+ (intros_using [id]);
+ (loop l)
+ ]
+ else
+ let kk1 = mk_integer k1
+ and kk2 = mk_integer k2 in
+ let p_initial = [P_APP 2;P_TYPE] in
+ let tac= shuffle_mult p_initial k1 e1.body k2 e2.body in
+ tclTHENS (cut (mk_gt kk1 izero))
+ [tclTHENS
+ (cut (mk_gt kk2 izero))
+ [tclTHENLIST [
+ (intros_using [aux2;aux1]);
+ (generalize_tac
+ [mkApp (Lazy.force coq_OMEGA7, [|
+ eq1;eq2;kk1;kk2;
+ mkVar aux1;mkVar aux2;
+ mkVar id1;mkVar id2 |])]);
+ (clear [aux1;aux2]);
+ (mk_then tac);
+ (intros_using [id]);
+ (loop l) ];
+ tclTHENLIST [
+ (unfold sp_Zgt);
+ simpl_in_concl;
+ reflexivity ] ];
+ tclTHENLIST [
+ (unfold sp_Zgt);
+ simpl_in_concl;
+ reflexivity ] ]
+ | CONSTANT_NOT_NUL(e,k) :: l ->
+ tclTHEN (generalize_tac [mkVar (hyp_of_tag e)]) Equality.discrConcl
+ | CONSTANT_NUL(e) :: l ->
+ tclTHEN (resolve_id (hyp_of_tag e)) reflexivity
+ | CONSTANT_NEG(e,k) :: l ->
+ tclTHENLIST [
+ (generalize_tac [mkVar (hyp_of_tag e)]);
+ (unfold sp_Zle);
+ simpl_in_concl;
+ (unfold sp_not);
+ (intros_using [aux]);
+ (resolve_id aux);
+ reflexivity
+ ]
+ | _ -> tclIDTAC
+ in
+ loop
+
+let normalize p_initial t =
+ let (tac,t') = transform p_initial t in
+ let (tac',t'') = condense p_initial t' in
+ let (tac'',t''') = clear_zero p_initial t'' in
+ tac @ tac' @ tac'' , t'''
+
+let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) =
+ let p_initial = [P_APP pos ;P_TYPE] in
+ let (tac,t') = normalize p_initial t in
+ let shift_left =
+ tclTHEN
+ (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ])
+ (tclTRY (clear [id]))
+ in
+ if tac <> [] then
+ let id' = new_identifier () in
+ ((id',(tclTHENLIST [ (shift_left); (mk_then tac); (intros_using [id']) ]))
+ :: tactic,
+ compile id' flag t' :: defs)
+ else
+ (tactic,defs)
+
+let destructure_omega gl tac_def (id,c) =
+ if atompart_of_id id = "State" then
+ tac_def
+ else
+ try match destructurate_prop c with
+ | Kapp(Eq,[typ;t1;t2])
+ when destructurate_type (pf_nf gl typ) = Kapp(Z,[]) ->
+ let t = mk_plus t1 (mk_inv t2) in
+ normalize_equation
+ id EQUA (Lazy.force coq_Zegal_left) 2 t t1 t2 tac_def
+ | Kapp(Zne,[t1;t2]) ->
+ let t = mk_plus t1 (mk_inv t2) in
+ normalize_equation
+ id DISE (Lazy.force coq_Zne_left) 1 t t1 t2 tac_def
+ | Kapp(Zle,[t1;t2]) ->
+ let t = mk_plus t2 (mk_inv t1) in
+ normalize_equation
+ id INEQ (Lazy.force coq_Zle_left) 2 t t1 t2 tac_def
+ | Kapp(Zlt,[t1;t2]) ->
+ let t = mk_plus (mk_plus t2 (mk_integer negone)) (mk_inv t1) in
+ normalize_equation
+ id INEQ (Lazy.force coq_Zlt_left) 2 t t1 t2 tac_def
+ | Kapp(Zge,[t1;t2]) ->
+ let t = mk_plus t1 (mk_inv t2) in
+ normalize_equation
+ id INEQ (Lazy.force coq_Zge_left) 2 t t1 t2 tac_def
+ | Kapp(Zgt,[t1;t2]) ->
+ let t = mk_plus (mk_plus t1 (mk_integer negone)) (mk_inv t2) in
+ normalize_equation
+ id INEQ (Lazy.force coq_Zgt_left) 2 t t1 t2 tac_def
+ | _ -> tac_def
+ with e when catchable_exception e -> tac_def
+
+let reintroduce id =
+ (* [id] cannot be cleared if dependent: protect it by a try *)
+ tclTHEN (tclTRY (clear [id])) (intro_using id)
+
+let coq_omega gl =
+ clear_tables ();
+ let tactic_normalisation, system =
+ List.fold_left (destructure_omega gl) ([],[]) (pf_hyps_types gl) in
+ let prelude,sys =
+ List.fold_left
+ (fun (tac,sys) (t,(v,th,b)) ->
+ if b then
+ let id = new_identifier () in
+ let i = new_id () in
+ tag_hypothesis id i;
+ (tclTHENLIST [
+ (simplest_elim (applist (Lazy.force coq_intro_Z, [t])));
+ (intros_using [v; id]);
+ (elim_id id);
+ (clear [id]);
+ (intros_using [th;id]);
+ tac ]),
+ {kind = INEQ;
+ body = [{v=intern_id v; c=one}];
+ constant = zero; id = i} :: sys
+ else
+ (tclTHENLIST [
+ (simplest_elim (applist (Lazy.force coq_new_var, [t])));
+ (intros_using [v;th]);
+ tac ]),
+ sys)
+ (tclIDTAC,[]) (dump_tables ())
+ in
+ let system = system @ sys in
+ if !display_system_flag then display_system display_var system;
+ if !old_style_flag then begin
+ try
+ let _ = simplify (new_id,new_var_num,display_var) false system in
+ tclIDTAC gl
+ with UNSOLVABLE ->
+ let _,path = depend [] [] (history ()) in
+ if !display_action_flag then display_action display_var path;
+ (tclTHEN prelude (replay_history tactic_normalisation path)) gl
+ end else begin
+ try
+ let path = simplify_strong (new_id,new_var_num,display_var) system in
+ if !display_action_flag then display_action display_var path;
+ (tclTHEN prelude (replay_history tactic_normalisation path)) gl
+ with NO_CONTRADICTION -> error "Omega can't solve this system"
+ end
+
+let coq_omega = solver_time coq_omega
+
+let nat_inject gl =
+ let rec explore p t =
+ try match destructurate_term t with
+ | Kapp(Plus,[t1;t2]) ->
+ tclTHENLIST [
+ (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2))
+ ((Lazy.force coq_inj_plus),[t1;t2]));
+ (explore (P_APP 1 :: p) t1);
+ (explore (P_APP 2 :: p) t2)
+ ]
+ | Kapp(Mult,[t1;t2]) ->
+ tclTHENLIST [
+ (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2))
+ ((Lazy.force coq_inj_mult),[t1;t2]));
+ (explore (P_APP 1 :: p) t1);
+ (explore (P_APP 2 :: p) t2)
+ ]
+ | Kapp(Minus,[t1;t2]) ->
+ let id = new_identifier () in
+ tclTHENS
+ (tclTHEN
+ (simplest_elim (applist (Lazy.force coq_le_gt_dec, [t2;t1])))
+ (intros_using [id]))
+ [
+ tclTHENLIST [
+ (clever_rewrite_gen p
+ (mk_minus (mk_inj t1) (mk_inj t2))
+ ((Lazy.force coq_inj_minus1),[t1;t2;mkVar id]));
+ (loop [id,mkApp (Lazy.force coq_le, [| t2;t1 |])]);
+ (explore (P_APP 1 :: p) t1);
+ (explore (P_APP 2 :: p) t2) ];
+ (tclTHEN
+ (clever_rewrite_gen p (mk_integer zero)
+ ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id]))
+ (loop [id,mkApp (Lazy.force coq_gt, [| t2;t1 |])]))
+ ]
+ | Kapp(S,[t']) ->
+ let rec is_number t =
+ try match destructurate_term t with
+ Kapp(S,[t]) -> is_number t
+ | Kapp(O,[]) -> true
+ | _ -> false
+ with e when catchable_exception e -> false
+ in
+ let rec loop p t =
+ try match destructurate_term t with
+ Kapp(S,[t]) ->
+ (tclTHEN
+ (clever_rewrite_gen p
+ (mkApp (Lazy.force coq_Zsucc, [| mk_inj t |]))
+ ((Lazy.force coq_inj_S),[t]))
+ (loop (P_APP 1 :: p) t))
+ | _ -> explore p t
+ with e when catchable_exception e -> explore p t
+ in
+ if is_number t' then focused_simpl p else loop p t
+ | Kapp(Pred,[t]) ->
+ let t_minus_one =
+ mkApp (Lazy.force coq_minus, [| t;
+ mkApp (Lazy.force coq_S, [| Lazy.force coq_O |]) |]) in
+ tclTHEN
+ (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one
+ ((Lazy.force coq_pred_of_minus),[t]))
+ (explore p t_minus_one)
+ | Kapp(O,[]) -> focused_simpl p
+ | _ -> tclIDTAC
+ with e when catchable_exception e -> tclIDTAC
+
+ and loop = function
+ | [] -> tclIDTAC
+ | (i,t)::lit ->
+ begin try match destructurate_prop t with
+ Kapp(Le,[t1;t2]) ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_inj_le, [| t1;t2;mkVar i |]) ]);
+ (explore [P_APP 1; P_TYPE] t1);
+ (explore [P_APP 2; P_TYPE] t2);
+ (reintroduce i);
+ (loop lit)
+ ]
+ | Kapp(Lt,[t1;t2]) ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_inj_lt, [| t1;t2;mkVar i |]) ]);
+ (explore [P_APP 1; P_TYPE] t1);
+ (explore [P_APP 2; P_TYPE] t2);
+ (reintroduce i);
+ (loop lit)
+ ]
+ | Kapp(Ge,[t1;t2]) ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_inj_ge, [| t1;t2;mkVar i |]) ]);
+ (explore [P_APP 1; P_TYPE] t1);
+ (explore [P_APP 2; P_TYPE] t2);
+ (reintroduce i);
+ (loop lit)
+ ]
+ | Kapp(Gt,[t1;t2]) ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_inj_gt, [| t1;t2;mkVar i |]) ]);
+ (explore [P_APP 1; P_TYPE] t1);
+ (explore [P_APP 2; P_TYPE] t2);
+ (reintroduce i);
+ (loop lit)
+ ]
+ | Kapp(Neq,[t1;t2]) ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_inj_neq, [| t1;t2;mkVar i |]) ]);
+ (explore [P_APP 1; P_TYPE] t1);
+ (explore [P_APP 2; P_TYPE] t2);
+ (reintroduce i);
+ (loop lit)
+ ]
+ | Kapp(Eq,[typ;t1;t2]) ->
+ if pf_conv_x gl typ (Lazy.force coq_nat) then
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]);
+ (explore [P_APP 2; P_TYPE] t1);
+ (explore [P_APP 3; P_TYPE] t2);
+ (reintroduce i);
+ (loop lit)
+ ]
+ else loop lit
+ | _ -> loop lit
+ with e when catchable_exception e -> loop lit end
+ in
+ loop (List.rev (pf_hyps_types gl)) gl
+
+let rec decidability gl t =
+ match destructurate_prop t with
+ | Kapp(Or,[t1;t2]) ->
+ mkApp (Lazy.force coq_dec_or, [| t1; t2;
+ decidability gl t1; decidability gl t2 |])
+ | Kapp(And,[t1;t2]) ->
+ mkApp (Lazy.force coq_dec_and, [| t1; t2;
+ decidability gl t1; decidability gl t2 |])
+ | Kapp(Iff,[t1;t2]) ->
+ mkApp (Lazy.force coq_dec_iff, [| t1; t2;
+ decidability gl t1; decidability gl t2 |])
+ | Kimp(t1,t2) ->
+ mkApp (Lazy.force coq_dec_imp, [| t1; t2;
+ decidability gl t1; decidability gl t2 |])
+ | Kapp(Not,[t1]) -> mkApp (Lazy.force coq_dec_not, [| t1;
+ decidability gl t1 |])
+ | Kapp(Eq,[typ;t1;t2]) ->
+ begin match destructurate_type (pf_nf gl typ) with
+ | Kapp(Z,[]) -> mkApp (Lazy.force coq_dec_eq, [| t1;t2 |])
+ | Kapp(Nat,[]) -> mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |])
+ | _ -> errorlabstrm "decidability"
+ (str "Omega: Can't solve a goal with equality on " ++
+ Printer.pr_lconstr typ)
+ end
+ | Kapp(Zne,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zne, [| t1;t2 |])
+ | Kapp(Zle,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zle, [| t1;t2 |])
+ | Kapp(Zlt,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zlt, [| t1;t2 |])
+ | Kapp(Zge,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zge, [| t1;t2 |])
+ | Kapp(Zgt,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zgt, [| t1;t2 |])
+ | Kapp(Le, [t1;t2]) -> mkApp (Lazy.force coq_dec_le, [| t1;t2 |])
+ | Kapp(Lt, [t1;t2]) -> mkApp (Lazy.force coq_dec_lt, [| t1;t2 |])
+ | Kapp(Ge, [t1;t2]) -> mkApp (Lazy.force coq_dec_ge, [| t1;t2 |])
+ | Kapp(Gt, [t1;t2]) -> mkApp (Lazy.force coq_dec_gt, [| t1;t2 |])
+ | Kapp(False,[]) -> Lazy.force coq_dec_False
+ | Kapp(True,[]) -> Lazy.force coq_dec_True
+ | Kapp(Other t,_::_) -> error
+ ("Omega: Unrecognized predicate or connective: "^t)
+ | Kapp(Other t,[]) -> error ("Omega: Unrecognized atomic proposition: "^t)
+ | Kvar _ -> error "Omega: Can't solve a goal with proposition variables"
+ | _ -> error "Omega: Unrecognized proposition"
+
+let onClearedName id tac =
+ (* We cannot ensure that hyps can be cleared (because of dependencies), *)
+ (* so renaming may be necessary *)
+ tclTHEN
+ (tclTRY (clear [id]))
+ (fun gl ->
+ let id = fresh_id [] id gl in
+ tclTHEN (introduction id) (tac id) gl)
+
+let destructure_hyps gl =
+ let rec loop = function
+ | [] -> (tclTHEN nat_inject coq_omega)
+ | (i,body,t)::lit ->
+ begin try match destructurate_prop t with
+ | Kapp(False,[]) -> elim_id i
+ | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit
+ | Kapp(Or,[t1;t2]) ->
+ (tclTHENS
+ (elim_id i)
+ [ onClearedName i (fun i -> (loop ((i,None,t1)::lit)));
+ onClearedName i (fun i -> (loop ((i,None,t2)::lit))) ])
+ | Kapp(And,[t1;t2]) ->
+ tclTHENLIST [
+ (elim_id i);
+ (tclTRY (clear [i]));
+ (fun gl ->
+ let i1 = fresh_id [] (add_suffix i "_left") gl in
+ let i2 = fresh_id [] (add_suffix i "_right") gl in
+ tclTHENLIST [
+ (introduction i1);
+ (introduction i2);
+ (loop ((i1,None,t1)::(i2,None,t2)::lit)) ] gl)
+ ]
+ | Kapp(Iff,[t1;t2]) ->
+ tclTHENLIST [
+ (elim_id i);
+ (tclTRY (clear [i]));
+ (fun gl ->
+ let i1 = fresh_id [] (add_suffix i "_left") gl in
+ let i2 = fresh_id [] (add_suffix i "_right") gl in
+ tclTHENLIST [
+ introduction i1;
+ generalize_tac
+ [mkApp (Lazy.force coq_imp_simp,
+ [| t1; t2; decidability gl t1; mkVar i1|])];
+ onClearedName i1 (fun i1 ->
+ tclTHENLIST [
+ introduction i2;
+ generalize_tac
+ [mkApp (Lazy.force coq_imp_simp,
+ [| t2; t1; decidability gl t2; mkVar i2|])];
+ onClearedName i2 (fun i2 ->
+ loop
+ ((i1,None,mk_or (mk_not t1) t2)::
+ (i2,None,mk_or (mk_not t2) t1)::lit))
+ ])] gl)
+ ]
+ | Kimp(t1,t2) ->
+ if
+ is_Prop (pf_type_of gl t1) &
+ is_Prop (pf_type_of gl t2) &
+ closed0 t2
+ then
+ tclTHENLIST [
+ (generalize_tac [mkApp (Lazy.force coq_imp_simp,
+ [| t1; t2; decidability gl t1; mkVar i|])]);
+ (onClearedName i (fun i ->
+ (loop ((i,None,mk_or (mk_not t1) t2)::lit))))
+ ]
+ else
+ loop lit
+ | Kapp(Not,[t]) ->
+ begin match destructurate_prop t with
+ Kapp(Or,[t1;t2]) ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]);
+ (onClearedName i (fun i ->
+ (loop ((i,None,mk_and (mk_not t1) (mk_not t2)):: lit))))
+ ]
+ | Kapp(And,[t1;t2]) ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_not_and, [| t1; t2;
+ decidability gl t1; mkVar i|])]);
+ (onClearedName i (fun i ->
+ (loop ((i,None,mk_or (mk_not t1) (mk_not t2))::lit))))
+ ]
+ | Kapp(Iff,[t1;t2]) ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_not_iff, [| t1; t2;
+ decidability gl t1; decidability gl t2; mkVar i|])]);
+ (onClearedName i (fun i ->
+ (loop ((i,None,
+ mk_or (mk_and t1 (mk_not t2))
+ (mk_and (mk_not t1) t2))::lit))))
+ ]
+ | Kimp(t1,t2) ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_not_imp, [| t1; t2;
+ decidability gl t1;mkVar i |])]);
+ (onClearedName i (fun i ->
+ (loop ((i,None,mk_and t1 (mk_not t2)) :: lit))))
+ ]
+ | Kapp(Not,[t]) ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_not_not, [| t;
+ decidability gl t; mkVar i |])]);
+ (onClearedName i (fun i -> (loop ((i,None,t)::lit))))
+ ]
+ | Kapp(Zle, [t1;t2]) ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_Znot_le_gt, [| t1;t2;mkVar i|])]);
+ (onClearedName i (fun _ -> loop lit))
+ ]
+ | Kapp(Zge, [t1;t2]) ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_Znot_ge_lt, [| t1;t2;mkVar i|])]);
+ (onClearedName i (fun _ -> loop lit))
+ ]
+ | Kapp(Zlt, [t1;t2]) ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_Znot_lt_ge, [| t1;t2;mkVar i|])]);
+ (onClearedName i (fun _ -> loop lit))
+ ]
+ | Kapp(Zgt, [t1;t2]) ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_Znot_gt_le, [| t1;t2;mkVar i|])]);
+ (onClearedName i (fun _ -> loop lit))
+ ]
+ | Kapp(Le, [t1;t2]) ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_not_le, [| t1;t2;mkVar i|])]);
+ (onClearedName i (fun _ -> loop lit))
+ ]
+ | Kapp(Ge, [t1;t2]) ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_not_ge, [| t1;t2;mkVar i|])]);
+ (onClearedName i (fun _ -> loop lit))
+ ]
+ | Kapp(Lt, [t1;t2]) ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_not_lt, [| t1;t2;mkVar i|])]);
+ (onClearedName i (fun _ -> loop lit))
+ ]
+ | Kapp(Gt, [t1;t2]) ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_not_gt, [| t1;t2;mkVar i|])]);
+ (onClearedName i (fun _ -> loop lit))
+ ]
+ | Kapp(Eq,[typ;t1;t2]) ->
+ if !old_style_flag then begin
+ match destructurate_type (pf_nf gl typ) with
+ | Kapp(Nat,_) ->
+ tclTHENLIST [
+ (simplest_elim
+ (mkApp
+ (Lazy.force coq_not_eq, [|t1;t2;mkVar i|])));
+ (onClearedName i (fun _ -> loop lit))
+ ]
+ | Kapp(Z,_) ->
+ tclTHENLIST [
+ (simplest_elim
+ (mkApp
+ (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|])));
+ (onClearedName i (fun _ -> loop lit))
+ ]
+ | _ -> loop lit
+ end else begin
+ match destructurate_type (pf_nf gl typ) with
+ | Kapp(Nat,_) ->
+ (tclTHEN
+ (convert_hyp_no_check
+ (i,body,
+ (mkApp (Lazy.force coq_neq, [| t1;t2|]))))
+ (loop lit))
+ | Kapp(Z,_) ->
+ (tclTHEN
+ (convert_hyp_no_check
+ (i,body,
+ (mkApp (Lazy.force coq_Zne, [| t1;t2|]))))
+ (loop lit))
+ | _ -> loop lit
+ end
+ | _ -> loop lit
+ end
+ | _ -> loop lit
+ with e when catchable_exception e -> loop lit
+ end
+ in
+ loop (pf_hyps gl) gl
+
+let destructure_goal gl =
+ let concl = pf_concl gl in
+ let rec loop t =
+ match destructurate_prop t with
+ | Kapp(Not,[t]) ->
+ (tclTHEN
+ (tclTHEN (unfold sp_not) intro)
+ destructure_hyps)
+ | Kimp(a,b) -> (tclTHEN intro (loop b))
+ | Kapp(False,[]) -> destructure_hyps
+ | _ ->
+ (tclTHEN
+ (tclTHEN
+ (Tactics.refine
+ (mkApp (Lazy.force coq_dec_not_not, [| t;
+ decidability gl t; mkNewMeta () |])))
+ intro)
+ (destructure_hyps))
+ in
+ (loop concl) gl
+
+let destructure_goal = all_time (destructure_goal)
+
+let omega_solver gl =
+ Coqlib.check_required_library ["Coq";"omega";"Omega"];
+ let result = destructure_goal gl in
+ (* if !display_time_flag then begin text_time ();
+ flush Pervasives.stdout end; *)
+ result
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
new file mode 100644
index 00000000..3bfdce7f
--- /dev/null
+++ b/plugins/omega/g_omega.ml4
@@ -0,0 +1,47 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(**************************************************************************)
+(* *)
+(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *)
+(* *)
+(* Pierre Crégut (CNET, Lannion, France) *)
+(* *)
+(**************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id$ *)
+
+open Coq_omega
+open Refiner
+
+let omega_tactic l =
+ let tacs = List.map
+ (function
+ | "nat" -> Tacinterp.interp <:tactic<zify_nat>>
+ | "positive" -> Tacinterp.interp <:tactic<zify_positive>>
+ | "N" -> Tacinterp.interp <:tactic<zify_N>>
+ | "Z" -> Tacinterp.interp <:tactic<zify_op>>
+ | s -> Util.error ("No Omega knowledge base for type "^s))
+ (Util.list_uniquize (List.sort compare l))
+ in
+ tclTHEN
+ (tclREPEAT (tclPROGRESS (tclTHENLIST tacs)))
+ omega_solver
+
+
+TACTIC EXTEND omega
+| [ "omega" ] -> [ omega_tactic [] ]
+END
+
+TACTIC EXTEND omega'
+| [ "omega" "with" ne_ident_list(l) ] ->
+ [ omega_tactic (List.map Names.string_of_id l) ]
+| [ "omega" "with" "*" ] -> [ omega_tactic ["nat";"positive";"N";"Z"] ]
+END
+
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
new file mode 100644
index 00000000..11ab9c03
--- /dev/null
+++ b/plugins/omega/omega.ml
@@ -0,0 +1,716 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(**************************************************************************)
+(* *)
+(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *)
+(* *)
+(* Pierre Crégut (CNET, Lannion, France) *)
+(* *)
+(* 13/10/2002 : modified to cope with an external numbering of equations *)
+(* and hypothesis. Its use for Omega is not more complex and it makes *)
+(* things much simpler for the reflexive version where we should limit *)
+(* the number of source of numbering. *)
+(**************************************************************************)
+
+open Names
+
+module type INT = sig
+ type bigint
+ val less_than : bigint -> bigint -> bool
+ val add : bigint -> bigint -> bigint
+ val sub : bigint -> bigint -> bigint
+ val mult : bigint -> bigint -> bigint
+ val euclid : bigint -> bigint -> bigint * bigint
+ val neg : bigint -> bigint
+ val zero : bigint
+ val one : bigint
+ val to_string : bigint -> string
+end
+
+let debug = ref false
+
+module MakeOmegaSolver (Int:INT) = struct
+
+type bigint = Int.bigint
+let (<?) = Int.less_than
+let (<=?) x y = Int.less_than x y or x = y
+let (>?) x y = Int.less_than y x
+let (>=?) x y = Int.less_than y x or x = y
+let (=?) = (=)
+let (+) = Int.add
+let (-) = Int.sub
+let ( * ) = Int.mult
+let (/) x y = fst (Int.euclid x y)
+let (mod) x y = snd (Int.euclid x y)
+let zero = Int.zero
+let one = Int.one
+let two = one + one
+let negone = Int.neg one
+let abs x = if Int.less_than x zero then Int.neg x else x
+let string_of_bigint = Int.to_string
+let neg = Int.neg
+
+(* To ensure that polymorphic (<) is not used mistakenly on big integers *)
+(* Warning: do not use (=) either on big int *)
+let (<) = ((<) : int -> int -> bool)
+let (>) = ((>) : int -> int -> bool)
+let (<=) = ((<=) : int -> int -> bool)
+let (>=) = ((>=) : int -> int -> bool)
+
+let pp i = print_int i; print_newline (); flush stdout
+
+let push v l = l := v :: !l
+
+let rec pgcd x y = if y =? zero then x else pgcd y (x mod y)
+
+let pgcd_l = function
+ | [] -> failwith "pgcd_l"
+ | x :: l -> List.fold_left pgcd x l
+
+let floor_div a b =
+ match a >=? zero , b >? zero with
+ | true,true -> a / b
+ | false,false -> a / b
+ | true, false -> (a-one) / b - one
+ | false,true -> (a+one) / b - one
+
+type coeff = {c: bigint ; v: int}
+
+type linear = coeff list
+
+type eqn_kind = EQUA | INEQ | DISE
+
+type afine = {
+ (* a number uniquely identifying the equation *)
+ id: int ;
+ (* a boolean true for an eq, false for an ineq (Sigma a_i x_i >= 0) *)
+ kind: eqn_kind;
+ (* the variables and their coefficient *)
+ body: coeff list;
+ (* a constant *)
+ constant: bigint }
+
+type state_action = {
+ st_new_eq : afine;
+ st_def : afine;
+ st_orig : afine;
+ st_coef : bigint;
+ st_var : int }
+
+type action =
+ | DIVIDE_AND_APPROX of afine * afine * bigint * bigint
+ | NOT_EXACT_DIVIDE of afine * bigint
+ | FORGET_C of int
+ | EXACT_DIVIDE of afine * bigint
+ | SUM of int * (bigint * afine) * (bigint * afine)
+ | STATE of state_action
+ | HYP of afine
+ | FORGET of int * int
+ | FORGET_I of int * int
+ | CONTRADICTION of afine * afine
+ | NEGATE_CONTRADICT of afine * afine * bool
+ | MERGE_EQ of int * afine * int
+ | CONSTANT_NOT_NUL of int * bigint
+ | CONSTANT_NUL of int
+ | CONSTANT_NEG of int * bigint
+ | SPLIT_INEQ of afine * (int * action list) * (int * action list)
+ | WEAKEN of int * bigint
+
+exception UNSOLVABLE
+
+exception NO_CONTRADICTION
+
+let display_eq print_var (l,e) =
+ let _ =
+ List.fold_left
+ (fun not_first f ->
+ print_string
+ (if f.c <? zero then "- " else if not_first then "+ " else "");
+ let c = abs f.c in
+ if c =? one then
+ Printf.printf "%s " (print_var f.v)
+ else
+ Printf.printf "%s %s " (string_of_bigint c) (print_var f.v);
+ true)
+ false l
+ in
+ if e >? zero then
+ Printf.printf "+ %s " (string_of_bigint e)
+ else if e <? zero then
+ Printf.printf "- %s " (string_of_bigint (abs e))
+
+let rec trace_length l =
+ let action_length accu = function
+ | SPLIT_INEQ (_,(_,l1),(_,l2)) ->
+ accu + one + trace_length l1 + trace_length l2
+ | _ -> accu + one in
+ List.fold_left action_length zero l
+
+let operator_of_eq = function
+ | EQUA -> "=" | DISE -> "!=" | INEQ -> ">="
+
+let kind_of = function
+ | EQUA -> "equation" | DISE -> "disequation" | INEQ -> "inequation"
+
+let display_system print_var l =
+ List.iter
+ (fun { kind=b; body=e; constant=c; id=id} ->
+ Printf.printf "E%d: " id;
+ display_eq print_var (e,c);
+ Printf.printf "%s 0\n" (operator_of_eq b))
+ l;
+ print_string "------------------------\n\n"
+
+let display_inequations print_var l =
+ List.iter (fun e -> display_eq print_var e;print_string ">= 0\n") l;
+ print_string "------------------------\n\n"
+
+let sbi = string_of_bigint
+
+let rec display_action print_var = function
+ | act :: l -> begin match act with
+ | DIVIDE_AND_APPROX (e1,e2,k,d) ->
+ Printf.printf
+ "Inequation E%d is divided by %s and the constant coefficient is \
+ rounded by substracting %s.\n" e1.id (sbi k) (sbi d)
+ | NOT_EXACT_DIVIDE (e,k) ->
+ Printf.printf
+ "Constant in equation E%d is not divisible by the pgcd \
+ %s of its other coefficients.\n" e.id (sbi k)
+ | EXACT_DIVIDE (e,k) ->
+ Printf.printf
+ "Equation E%d is divided by the pgcd \
+ %s of its coefficients.\n" e.id (sbi k)
+ | WEAKEN (e,k) ->
+ Printf.printf
+ "To ensure a solution in the dark shadow \
+ the equation E%d is weakened by %s.\n" e (sbi k)
+ | SUM (e,(c1,e1),(c2,e2)) ->
+ Printf.printf
+ "We state %s E%d = %s %s E%d + %s %s E%d.\n"
+ (kind_of e1.kind) e (sbi c1) (kind_of e1.kind) e1.id (sbi c2)
+ (kind_of e2.kind) e2.id
+ | STATE { st_new_eq = e } ->
+ Printf.printf "We define a new equation E%d: " e.id;
+ display_eq print_var (e.body,e.constant);
+ print_string (operator_of_eq e.kind); print_string " 0"
+ | HYP e ->
+ Printf.printf "We define E%d: " e.id;
+ display_eq print_var (e.body,e.constant);
+ print_string (operator_of_eq e.kind); print_string " 0\n"
+ | FORGET_C e -> Printf.printf "E%d is trivially satisfiable.\n" e
+ | FORGET (e1,e2) -> Printf.printf "E%d subsumes E%d.\n" e1 e2
+ | FORGET_I (e1,e2) -> Printf.printf "E%d subsumes E%d.\n" e1 e2
+ | MERGE_EQ (e,e1,e2) ->
+ Printf.printf "E%d and E%d can be merged into E%d.\n" e1.id e2 e
+ | CONTRADICTION (e1,e2) ->
+ Printf.printf
+ "Equations E%d and E%d imply a contradiction on their \
+ constant factors.\n" e1.id e2.id
+ | NEGATE_CONTRADICT(e1,e2,b) ->
+ Printf.printf
+ "Equations E%d and E%d state that their body is at the same time
+ equal and different\n" e1.id e2.id
+ | CONSTANT_NOT_NUL (e,k) ->
+ Printf.printf "Equation E%d states %s = 0.\n" e (sbi k)
+ | CONSTANT_NEG(e,k) ->
+ Printf.printf "Equation E%d states %s >= 0.\n" e (sbi k)
+ | CONSTANT_NUL e ->
+ Printf.printf "Inequation E%d states 0 != 0.\n" e
+ | SPLIT_INEQ (e,(e1,l1),(e2,l2)) ->
+ Printf.printf "Equation E%d is split in E%d and E%d\n\n" e.id e1 e2;
+ display_action print_var l1;
+ print_newline ();
+ display_action print_var l2;
+ print_newline ()
+ end; display_action print_var l
+ | [] ->
+ flush stdout
+
+let default_print_var v = Printf.sprintf "X%d" v (* For debugging *)
+
+(*""*)
+let add_event, history, clear_history =
+ let accu = ref [] in
+ (fun (v:action) -> if !debug then display_action default_print_var [v]; push v accu),
+ (fun () -> !accu),
+ (fun () -> accu := [])
+
+let nf_linear = Sort.list (fun x y -> x.v > y.v)
+
+let nf ((b : bool),(e,(x : int))) = (b,(nf_linear e,x))
+
+let map_eq_linear f =
+ let rec loop = function
+ | x :: l -> let c = f x.c in if c=?zero then loop l else {v=x.v; c=c} :: loop l
+ | [] -> []
+ in
+ loop
+
+let map_eq_afine f e =
+ { id = e.id; kind = e.kind; body = map_eq_linear f e.body;
+ constant = f e.constant }
+
+let negate_eq = map_eq_afine (fun x -> neg x)
+
+let rec sum p0 p1 = match (p0,p1) with
+ | ([], l) -> l | (l, []) -> l
+ | (((x1::l1) as l1'), ((x2::l2) as l2')) ->
+ if x1.v = x2.v then
+ let c = x1.c + x2.c in
+ if c =? zero then sum l1 l2 else {v=x1.v;c=c} :: sum l1 l2
+ else if x1.v > x2.v then
+ x1 :: sum l1 l2'
+ else
+ x2 :: sum l1' l2
+
+let sum_afine new_eq_id eq1 eq2 =
+ { kind = eq1.kind; id = new_eq_id ();
+ body = sum eq1.body eq2.body; constant = eq1.constant + eq2.constant }
+
+exception FACTOR1
+
+let rec chop_factor_1 = function
+ | x :: l ->
+ if abs x.c =? one then x,l else let (c',l') = chop_factor_1 l in (c',x::l')
+ | [] -> raise FACTOR1
+
+exception CHOPVAR
+
+let rec chop_var v = function
+ | f :: l -> if f.v = v then f,l else let (f',l') = chop_var v l in (f',f::l')
+ | [] -> raise CHOPVAR
+
+let normalize ({id=id; kind=eq_flag; body=e; constant =x} as eq) =
+ if e = [] then begin
+ match eq_flag with
+ | EQUA ->
+ if x =? zero then [] else begin
+ add_event (CONSTANT_NOT_NUL(id,x)); raise UNSOLVABLE
+ end
+ | DISE ->
+ if x <> zero then [] else begin
+ add_event (CONSTANT_NUL id); raise UNSOLVABLE
+ end
+ | INEQ ->
+ if x >=? zero then [] else begin
+ add_event (CONSTANT_NEG(id,x)); raise UNSOLVABLE
+ end
+ end else
+ let gcd = pgcd_l (List.map (fun f -> abs f.c) e) in
+ if eq_flag=EQUA & x mod gcd <> zero then begin
+ add_event (NOT_EXACT_DIVIDE (eq,gcd)); raise UNSOLVABLE
+ end else if eq_flag=DISE & x mod gcd <> zero then begin
+ add_event (FORGET_C eq.id); []
+ end else if gcd <> one then begin
+ let c = floor_div x gcd in
+ let d = x - c * gcd in
+ let new_eq = {id=id; kind=eq_flag; constant=c;
+ body=map_eq_linear (fun c -> c / gcd) e} in
+ add_event (if eq_flag=EQUA or eq_flag = DISE then EXACT_DIVIDE(eq,gcd)
+ else DIVIDE_AND_APPROX(eq,new_eq,gcd,d));
+ [new_eq]
+ end else [eq]
+
+let eliminate_with_in new_eq_id {v=v;c=c_unite} eq2
+ ({body=e1; constant=c1} as eq1) =
+ try
+ let (f,_) = chop_var v e1 in
+ let coeff = if c_unite=?one then neg f.c else if c_unite=? negone then f.c
+ else failwith "eliminate_with_in" in
+ let res = sum_afine new_eq_id eq1 (map_eq_afine (fun c -> c * coeff) eq2) in
+ add_event (SUM (res.id,(one,eq1),(coeff,eq2))); res
+ with CHOPVAR -> eq1
+
+let omega_mod a b = a - b * floor_div (two * a + b) (two * b)
+let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 =
+ let e = original.body in
+ let sigma = new_var_id () in
+ let smallest,var =
+ try
+ List.fold_left (fun (v,p) c -> if v >? (abs c.c) then abs c.c,c.v else (v,p))
+ (abs (List.hd e).c, (List.hd e).v) (List.tl e)
+ with Failure "tl" -> display_system print_var [original] ; failwith "TL" in
+ let m = smallest + one in
+ let new_eq =
+ { constant = omega_mod original.constant m;
+ body = {c= neg m;v=sigma} ::
+ map_eq_linear (fun a -> omega_mod a m) original.body;
+ id = new_eq_id (); kind = EQUA } in
+ let definition =
+ { constant = neg (floor_div (two * original.constant + m) (two * m));
+ body = map_eq_linear (fun a -> neg (floor_div (two * a + m) (two * m)))
+ original.body;
+ id = new_eq_id (); kind = EQUA } in
+ add_event (STATE {st_new_eq = new_eq; st_def = definition;
+ st_orig = original; st_coef = m; st_var = sigma});
+ let new_eq = List.hd (normalize new_eq) in
+ let eliminated_var, def = chop_var var new_eq.body in
+ let other_equations =
+ Util.list_map_append
+ (fun e ->
+ normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) l1 in
+ let inequations =
+ Util.list_map_append
+ (fun e ->
+ normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) l2 in
+ let original' = eliminate_with_in new_eq_id eliminated_var new_eq original in
+ let mod_original = map_eq_afine (fun c -> c / m) original' in
+ add_event (EXACT_DIVIDE (original',m));
+ List.hd (normalize mod_original),other_equations,inequations
+
+let rec eliminate_one_equation ((new_eq_id,new_var_id,print_var) as new_ids) (e,other,ineqs) =
+ if !debug then display_system print_var (e::other);
+ try
+ let v,def = chop_factor_1 e.body in
+ (Util.list_map_append
+ (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) other,
+ Util.list_map_append
+ (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) ineqs)
+ with FACTOR1 ->
+ eliminate_one_equation new_ids (banerjee_step new_ids e other ineqs)
+
+let rec banerjee ((_,_,print_var) as new_ids) (sys_eq,sys_ineq) =
+ let rec fst_eq_1 = function
+ (eq::l) ->
+ if List.exists (fun x -> abs x.c =? one) eq.body then eq,l
+ else let (eq',l') = fst_eq_1 l in (eq',eq::l')
+ | [] -> raise Not_found in
+ match sys_eq with
+ [] -> if !debug then display_system print_var sys_ineq; sys_ineq
+ | (e1::rest) ->
+ let eq,other = try fst_eq_1 sys_eq with Not_found -> (e1,rest) in
+ if eq.body = [] then
+ if eq.constant =? zero then begin
+ add_event (FORGET_C eq.id); banerjee new_ids (other,sys_ineq)
+ end else begin
+ add_event (CONSTANT_NOT_NUL(eq.id,eq.constant)); raise UNSOLVABLE
+ end
+ else
+ banerjee new_ids
+ (eliminate_one_equation new_ids (eq,other,sys_ineq))
+
+type kind = INVERTED | NORMAL
+
+let redundancy_elimination new_eq_id system =
+ let normal = function
+ ({body=f::_} as e) when f.c <? zero -> negate_eq e, INVERTED
+ | e -> e,NORMAL in
+ let table = Hashtbl.create 7 in
+ List.iter
+ (fun e ->
+ let ({body=ne} as nx) ,kind = normal e in
+ if ne = [] then
+ if nx.constant <? zero then begin
+ add_event (CONSTANT_NEG(nx.id,nx.constant)); raise UNSOLVABLE
+ end else add_event (FORGET_C nx.id)
+ else
+ try
+ let (optnormal,optinvert) = Hashtbl.find table ne in
+ let final =
+ if kind = NORMAL then begin
+ match optnormal with
+ Some v ->
+ let kept =
+ if v.constant <? nx.constant
+ then begin add_event (FORGET (v.id,nx.id));v end
+ else begin add_event (FORGET (nx.id,v.id));nx end in
+ (Some(kept),optinvert)
+ | None -> Some nx,optinvert
+ end else begin
+ match optinvert with
+ Some v ->
+ let _kept =
+ if v.constant >? nx.constant
+ then begin add_event (FORGET_I (v.id,nx.id));v end
+ else begin add_event (FORGET_I (nx.id,v.id));nx end in
+ (optnormal,Some(if v.constant >? nx.constant then v else nx))
+ | None -> optnormal,Some nx
+ end in
+ begin match final with
+ (Some high, Some low) ->
+ if high.constant <? low.constant then begin
+ add_event(CONTRADICTION (high,negate_eq low));
+ raise UNSOLVABLE
+ end
+ | _ -> () end;
+ Hashtbl.remove table ne;
+ Hashtbl.add table ne final
+ with Not_found ->
+ Hashtbl.add table ne
+ (if kind = NORMAL then (Some nx,None) else (None,Some nx)))
+ system;
+ let accu_eq = ref [] in
+ let accu_ineq = ref [] in
+ Hashtbl.iter
+ (fun p0 p1 -> match (p0,p1) with
+ | (e, (Some x, Some y)) when x.constant =? y.constant ->
+ let id=new_eq_id () in
+ add_event (MERGE_EQ(id,x,y.id));
+ push {id=id; kind=EQUA; body=x.body; constant=x.constant} accu_eq
+ | (e, (optnorm,optinvert)) ->
+ begin match optnorm with
+ Some x -> push x accu_ineq | _ -> () end;
+ begin match optinvert with
+ Some x -> push (negate_eq x) accu_ineq | _ -> () end)
+ table;
+ !accu_eq,!accu_ineq
+
+exception SOLVED_SYSTEM
+
+let select_variable system =
+ let table = Hashtbl.create 7 in
+ let push v c=
+ try let r = Hashtbl.find table v in r := max !r (abs c)
+ with Not_found -> Hashtbl.add table v (ref (abs c)) in
+ List.iter (fun {body=l} -> List.iter (fun f -> push f.v f.c) l) system;
+ let vmin,cmin = ref (-1), ref zero in
+ let var_cpt = ref 0 in
+ Hashtbl.iter
+ (fun v ({contents = c}) ->
+ incr var_cpt;
+ if c <? !cmin or !vmin = (-1) then begin vmin := v; cmin := c end)
+ table;
+ if !var_cpt < 1 then raise SOLVED_SYSTEM;
+ !vmin
+
+let classify v system =
+ List.fold_left
+ (fun (not_occ,below,over) eq ->
+ try let f,eq' = chop_var v eq.body in
+ if f.c >=? zero then (not_occ,((f.c,eq) :: below),over)
+ else (not_occ,below,((neg f.c,eq) :: over))
+ with CHOPVAR -> (eq::not_occ,below,over))
+ ([],[],[]) system
+
+let product new_eq_id dark_shadow low high =
+ List.fold_left
+ (fun accu (a,eq1) ->
+ List.fold_left
+ (fun accu (b,eq2) ->
+ let eq =
+ sum_afine new_eq_id (map_eq_afine (fun c -> c * b) eq1)
+ (map_eq_afine (fun c -> c * a) eq2) in
+ add_event(SUM(eq.id,(b,eq1),(a,eq2)));
+ match normalize eq with
+ | [eq] ->
+ let final_eq =
+ if dark_shadow then
+ let delta = (a - one) * (b - one) in
+ add_event(WEAKEN(eq.id,delta));
+ {id = eq.id; kind=INEQ; body = eq.body;
+ constant = eq.constant - delta}
+ else eq
+ in final_eq :: accu
+ | (e::_) -> failwith "Product dardk"
+ | [] -> accu)
+ accu high)
+ [] low
+
+let fourier_motzkin (new_eq_id,_,print_var) dark_shadow system =
+ let v = select_variable system in
+ let (ineq_out, ineq_low,ineq_high) = classify v system in
+ let expanded = ineq_out @ product new_eq_id dark_shadow ineq_low ineq_high in
+ if !debug then display_system print_var expanded; expanded
+
+let simplify ((new_eq_id,new_var_id,print_var) as new_ids) dark_shadow system =
+ if List.exists (fun e -> e.kind = DISE) system then
+ failwith "disequation in simplify";
+ clear_history ();
+ List.iter (fun e -> add_event (HYP e)) system;
+ let system = Util.list_map_append normalize system in
+ let eqs,ineqs = List.partition (fun e -> e.kind=EQUA) system in
+ let simp_eq,simp_ineq = redundancy_elimination new_eq_id ineqs in
+ let system = (eqs @ simp_eq,simp_ineq) in
+ let rec loop1a system =
+ let sys_ineq = banerjee new_ids system in
+ loop1b sys_ineq
+ and loop1b sys_ineq =
+ let simp_eq,simp_ineq = redundancy_elimination new_eq_id sys_ineq in
+ if simp_eq = [] then simp_ineq else loop1a (simp_eq,simp_ineq)
+ in
+ let rec loop2 system =
+ try
+ let expanded = fourier_motzkin new_ids dark_shadow system in
+ loop2 (loop1b expanded)
+ with SOLVED_SYSTEM ->
+ if !debug then display_system print_var system; system
+ in
+ loop2 (loop1a system)
+
+let rec depend relie_on accu = function
+ | act :: l ->
+ begin match act with
+ | DIVIDE_AND_APPROX (e,_,_,_) ->
+ if List.mem e.id relie_on then depend relie_on (act::accu) l
+ else depend relie_on accu l
+ | EXACT_DIVIDE (e,_) ->
+ if List.mem e.id relie_on then depend relie_on (act::accu) l
+ else depend relie_on accu l
+ | WEAKEN (e,_) ->
+ if List.mem e relie_on then depend relie_on (act::accu) l
+ else depend relie_on accu l
+ | SUM (e,(_,e1),(_,e2)) ->
+ if List.mem e relie_on then
+ depend (e1.id::e2.id::relie_on) (act::accu) l
+ else
+ depend relie_on accu l
+ | STATE {st_new_eq=e;st_orig=o} ->
+ if List.mem e.id relie_on then depend (o.id::relie_on) (act::accu) l
+ else depend relie_on accu l
+ | HYP e ->
+ if List.mem e.id relie_on then depend relie_on (act::accu) l
+ else depend relie_on accu l
+ | FORGET_C _ -> depend relie_on accu l
+ | FORGET _ -> depend relie_on accu l
+ | FORGET_I _ -> depend relie_on accu l
+ | MERGE_EQ (e,e1,e2) ->
+ if List.mem e relie_on then
+ depend (e1.id::e2::relie_on) (act::accu) l
+ else
+ depend relie_on accu l
+ | NOT_EXACT_DIVIDE (e,_) -> depend (e.id::relie_on) (act::accu) l
+ | CONTRADICTION (e1,e2) ->
+ depend (e1.id::e2.id::relie_on) (act::accu) l
+ | CONSTANT_NOT_NUL (e,_) -> depend (e::relie_on) (act::accu) l
+ | CONSTANT_NEG (e,_) -> depend (e::relie_on) (act::accu) l
+ | CONSTANT_NUL e -> depend (e::relie_on) (act::accu) l
+ | NEGATE_CONTRADICT (e1,e2,_) ->
+ depend (e1.id::e2.id::relie_on) (act::accu) l
+ | SPLIT_INEQ _ -> failwith "depend"
+ end
+ | [] -> relie_on, accu
+
+(*
+let depend relie_on accu trace =
+ Printf.printf "Longueur de la trace initiale : %d\n"
+ (trace_length trace + trace_length accu);
+ let rel',trace' = depend relie_on accu trace in
+ Printf.printf "Longueur de la trace simplifiée : %d\n" (trace_length trace');
+ rel',trace'
+*)
+
+let solve (new_eq_id,new_eq_var,print_var) system =
+ try let _ = simplify new_eq_id false system in failwith "no contradiction"
+ with UNSOLVABLE -> display_action print_var (snd (depend [] [] (history ())))
+
+let negation (eqs,ineqs) =
+ let diseq,_ = List.partition (fun e -> e.kind = DISE) ineqs in
+ let normal = function
+ | ({body=f::_} as e) when f.c <? zero -> negate_eq e, INVERTED
+ | e -> e,NORMAL in
+ let table = Hashtbl.create 7 in
+ List.iter (fun e ->
+ let {body=ne;constant=c} ,kind = normal e in
+ Hashtbl.add table (ne,c) (kind,e)) diseq;
+ List.iter (fun e ->
+ assert (e.kind = EQUA);
+ let {body=ne;constant=c},kind = normal e in
+ try
+ let (kind',e') = Hashtbl.find table (ne,c) in
+ add_event (NEGATE_CONTRADICT (e,e',kind=kind'));
+ raise UNSOLVABLE
+ with Not_found -> ()) eqs
+
+exception FULL_SOLUTION of action list * int list
+
+let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system =
+ clear_history ();
+ List.iter (fun e -> add_event (HYP e)) system;
+ (* Initial simplification phase *)
+ let rec loop1a system =
+ negation system;
+ let sys_ineq = banerjee new_ids system in
+ loop1b sys_ineq
+ and loop1b sys_ineq =
+ let dise,ine = List.partition (fun e -> e.kind = DISE) sys_ineq in
+ let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in
+ if simp_eq = [] then dise @ simp_ineq
+ else loop1a (simp_eq,dise @ simp_ineq)
+ in
+ let rec loop2 system =
+ try
+ let expanded = fourier_motzkin new_ids false system in
+ loop2 (loop1b expanded)
+ with SOLVED_SYSTEM -> if !debug then display_system print_var system; system
+ in
+ let rec explode_diseq = function
+ | (de::diseq,ineqs,expl_map) ->
+ let id1 = new_eq_id ()
+ and id2 = new_eq_id () in
+ let e1 =
+ {id = id1; kind=INEQ; body = de.body; constant = de.constant -one} in
+ let e2 =
+ {id = id2; kind=INEQ; body = map_eq_linear neg de.body;
+ constant = neg de.constant - one} in
+ let new_sys =
+ List.map (fun (what,sys) -> ((de.id,id1,true)::what, e1::sys))
+ ineqs @
+ List.map (fun (what,sys) -> ((de.id,id2,false)::what,e2::sys))
+ ineqs
+ in
+ explode_diseq (diseq,new_sys,(de.id,(de,id1,id2))::expl_map)
+ | ([],ineqs,expl_map) -> ineqs,expl_map
+ in
+ try
+ let system = Util.list_map_append normalize system in
+ let eqs,ineqs = List.partition (fun e -> e.kind=EQUA) system in
+ let dise,ine = List.partition (fun e -> e.kind = DISE) ineqs in
+ let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in
+ let system = (eqs @ simp_eq,simp_ineq @ dise) in
+ let system' = loop1a system in
+ let diseq,ineq = List.partition (fun e -> e.kind = DISE) system' in
+ let first_segment = history () in
+ let sys_exploded,explode_map = explode_diseq (diseq,[[],ineq],[]) in
+ let all_solutions =
+ List.map
+ (fun (decomp,sys) ->
+ clear_history ();
+ try let _ = loop2 sys in raise NO_CONTRADICTION
+ with UNSOLVABLE ->
+ let relie_on,path = depend [] [] (history ()) in
+ let dc,_ = List.partition (fun (_,id,_) -> List.mem id relie_on) decomp in
+ let red = List.map (fun (x,_,_) -> x) dc in
+ (red,relie_on,decomp,path))
+ sys_exploded
+ in
+ let max_count sys =
+ let tbl = Hashtbl.create 7 in
+ let augment x =
+ try incr (Hashtbl.find tbl x)
+ with Not_found -> Hashtbl.add tbl x (ref 1) in
+ let eq = ref (-1) and c = ref 0 in
+ List.iter (function
+ | ([],r_on,_,path) -> raise (FULL_SOLUTION (path,r_on))
+ | (l,_,_,_) -> List.iter augment l) sys;
+ Hashtbl.iter (fun x v -> if !v > !c then begin eq := x; c := !v end) tbl;
+ !eq
+ in
+ let rec solve systems =
+ try
+ let id = max_count systems in
+ let rec sign = function
+ | ((id',_,b)::l) -> if id=id' then b else sign l
+ | [] -> failwith "solve" in
+ let s1,s2 =
+ List.partition (fun (_,_,decomp,_) -> sign decomp) systems in
+ let s1' =
+ List.map (fun (dep,ro,dc,pa) -> (Util.list_except id dep,ro,dc,pa)) s1 in
+ let s2' =
+ List.map (fun (dep,ro,dc,pa) -> (Util.list_except id dep,ro,dc,pa)) s2 in
+ let (r1,relie1) = solve s1'
+ and (r2,relie2) = solve s2' in
+ let (eq,id1,id2) = List.assoc id explode_map in
+ [SPLIT_INEQ(eq,(id1,r1),(id2, r2))], eq.id :: Util.list_union relie1 relie2
+ with FULL_SOLUTION (x0,x1) -> (x0,x1)
+ in
+ let act,relie_on = solve all_solutions in
+ snd(depend relie_on act first_segment)
+ with UNSOLVABLE -> snd (depend [] [] (history ()))
+
+end
diff --git a/plugins/omega/omega_plugin.mllib b/plugins/omega/omega_plugin.mllib
new file mode 100644
index 00000000..2b387fdc
--- /dev/null
+++ b/plugins/omega/omega_plugin.mllib
@@ -0,0 +1,4 @@
+Omega
+Coq_omega
+G_omega
+Omega_plugin_mod
diff --git a/plugins/omega/vo.itarget b/plugins/omega/vo.itarget
new file mode 100644
index 00000000..9d9a77a8
--- /dev/null
+++ b/plugins/omega/vo.itarget
@@ -0,0 +1,4 @@
+OmegaLemmas.vo
+OmegaPlugin.vo
+Omega.vo
+PreOmega.vo
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-20 04:54:44 +0000