diff options
Diffstat (limited to 'contrib/omega')
| -rwxr-xr-x | contrib/omega/Omega.v | 57 | ||||
| -rw-r--r-- | contrib/omega/OmegaLemmas.v | 269 | ||||
| -rw-r--r-- | contrib/omega/coq_omega.ml | 1783 | ||||
| -rw-r--r-- | contrib/omega/g_omega.ml4 | 24 | ||||
| -rwxr-xr-x | contrib/omega/omega.ml | 663 |
5 files changed, 2796 insertions, 0 deletions
diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v new file mode 100755 index 00000000..e72dcec2 --- /dev/null +++ b/contrib/omega/Omega.v @@ -0,0 +1,57 @@ +(************************************************************************) +(* 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: Omega.v,v 1.10.2.1 2004/07/16 19:30:12 herbelin Exp $ *) + +(* We do not require [ZArith] anymore, but only what's necessary for Omega *) +Require Export ZArith_base. +Require Export OmegaLemmas. + +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/contrib/omega/OmegaLemmas.v b/contrib/omega/OmegaLemmas.v new file mode 100644 index 00000000..6f0ea2c6 --- /dev/null +++ b/contrib/omega/OmegaLemmas.v @@ -0,0 +1,269 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id: OmegaLemmas.v,v 1.4.2.1 2004/07/16 19:30:12 herbelin Exp $ i*) + +Require Import ZArith_base. + +(** These are 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)%Z -> (0 <= y)%Z. +intros x y H; rewrite H; auto with arith. +Qed. + +Lemma OMEGA2 : forall x y:Z, (0 <= x)%Z -> (0 <= y)%Z -> (0 <= x + y)%Z. +exact Zplus_le_0_compat. +Qed. + +Lemma OMEGA3 : + forall x y k:Z, (k > 0)%Z -> x = (y * k)%Z -> x = 0%Z -> y = 0%Z. + +intros x y k H1 H2 H3; apply (Zmult_integral_l k); + [ unfold not in |- *; intros H4; absurd (k > 0)%Z; + [ rewrite H4; unfold Zgt in |- *; simpl in |- *; discriminate + | assumption ] + | rewrite <- H2; assumption ]. +Qed. + +Lemma OMEGA4 : forall x y z:Z, (x > 0)%Z -> (y > x)%Z -> (z * y + x)%Z <> 0%Z. + +unfold not in |- *; intros x y z H1 H2 H3; cut (y > 0)%Z; + [ intros H4; cut (0 <= z * y + x)%Z; + [ intros H5; generalize (Zmult_le_approx y z x H4 H2 H5); intros H6; + absurd (z * y + x > 0)%Z; + [ 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%Z -> y = 0%Z -> (x + y * z)%Z = 0%Z. + +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)%Z -> y = 0%Z -> (0 <= x + y * z)%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)%Z -> + (t > 0)%Z -> (0 <= x)%Z -> (0 <= y)%Z -> (0 <= x * z + y * t)%Z. + +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)%Z -> (0 <= y)%Z -> x = (- y)%Z -> x = 0%Z. + +intros x y H1 H2 H3; elim (Zle_lt_or_eq 0 x H1); + [ intros H4; absurd (0 < x)%Z; + [ change (0 >= x)%Z 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%Z -> x = z -> (y + (- x + z) * t)%Z = 0%Z. + +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)%Z = + (v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2))%Z. + +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)%Z = (v1 * (c1 * k1) + (l1 * k1 + l2))%Z. + +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)%Z = (v2 * (c2 * k2) + (l1 + l2 * k2))%Z. + +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))%Z = (l1 + l2)%Z. + +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))%Z = (l1 + l2)%Z. + +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)%Z = + (v * (c1 + c2 * k2) + (l1 + l2 * k2))%Z. + +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)%Z = (v * (c * k) + l * k)%Z. + +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%Z -> 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)%Z; rewrite Zplus_comm; + rewrite H3; rewrite H2; auto with arith. +Qed. + +Lemma OMEGA18 : forall x y k:Z, x = (y * k)%Z -> 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)%Z \/ (0 <= x * -1 + -1)%Z. + +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)%Z in |- *; apply Zsucc_le_reg; + rewrite <- Zsucc_pred; apply Zlt_le_succ; assumption + | intros H2; absurd (x = 0%Z); 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%Z -> 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_sym (x y:Z) (P:Z -> Prop) (H:P (y + x)%Z) := + eq_ind_r P H (Zplus_comm x y). + +Definition fast_Zplus_assoc_r (n m p:Z) (P:Z -> Prop) + (H:P (n + (m + p))%Z) := eq_ind_r P H (Zplus_assoc_reverse n m p). + +Definition fast_Zplus_assoc_l (n m p:Z) (P:Z -> Prop) + (H:P (n + m + p)%Z) := 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))%Z) := 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))%Z) := + 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))%Z) := + 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))%Z) := + 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))%Z) := + 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)%Z) := 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)%Z) := 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)%Z) := eq_ind_r P H (OMEGA14 v l1 l2 x). +Definition fast_Zred_factor0 (x:Z) (P:Z -> Prop) (H:P (x * 1)%Z) := + eq_ind_r P H (Zred_factor0 x). + +Definition fast_Zopp_one (x:Z) (P:Z -> Prop) (H:P (x * -1)%Z) := + eq_ind_r P H (Zopp_eq_mult_neg_1 x). + +Definition fast_Zmult_sym (x y:Z) (P:Z -> Prop) (H:P (y * x)%Z) := + eq_ind_r P H (Zmult_comm x y). + +Definition fast_Zopp_Zplus (x y:Z) (P:Z -> Prop) (H:P (- x + - y)%Z) := + eq_ind_r P H (Zopp_plus_distr x y). + +Definition fast_Zopp_Zopp (x:Z) (P:Z -> Prop) (H:P x) := + eq_ind_r P H (Zopp_involutive x). + +Definition fast_Zopp_Zmult_r (x y:Z) (P:Z -> Prop) + (H:P (x * - y)%Z) := eq_ind_r P H (Zopp_mult_distr_r x y). + +Definition fast_Zmult_plus_distr (n m p:Z) (P:Z -> Prop) + (H:P (n * p + m * p)%Z) := eq_ind_r P H (Zmult_plus_distr_l n m p). +Definition fast_Zmult_Zopp_left (x y:Z) (P:Z -> Prop) + (H:P (x * - y)%Z) := eq_ind_r P H (Zmult_opp_comm x y). + +Definition fast_Zmult_assoc_r (n m p:Z) (P:Z -> Prop) + (H:P (n * (m * p))%Z) := eq_ind_r P H (Zmult_assoc_reverse n m p). + +Definition fast_Zred_factor1 (x:Z) (P:Z -> Prop) (H:P (x * 2)%Z) := + eq_ind_r P H (Zred_factor1 x). + +Definition fast_Zred_factor2 (x y:Z) (P:Z -> Prop) + (H:P (x * (1 + y))%Z) := eq_ind_r P H (Zred_factor2 x y). +Definition fast_Zred_factor3 (x y:Z) (P:Z -> Prop) + (H:P (x * (1 + y))%Z) := 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))%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)%Z) := + eq_ind_r P H (Zred_factor6 x). diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml new file mode 100644 index 00000000..7a20aeb6 --- /dev/null +++ b/contrib/omega/coq_omega.ml @@ -0,0 +1,1783 @@ +(************************************************************************) +(* 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: coq_omega.ml,v 1.59.2.3 2004/07/16 19:30:12 herbelin Exp $ *) + +open Util +open Pp +open Reduction +open Proof_type +open Ast +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 Omega +open Contradiction + +(* 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 + +(* Obsolete, subsumed by Time Omega +let _ = + declare_bool_option + { optsync = false; + optname = "Omega time displaying flag"; + optkey = SecondaryTable ("Omega","Time"); + optread = read display_time_flag; + optwrite = write display_time_flag } +*) + +let _ = + declare_bool_option + { optsync = false; + optname = "Omega system time displaying flag"; + optkey = SecondaryTable ("Omega","System"); + optread = read display_system_flag; + optwrite = write display_system_flag } + +let _ = + declare_bool_option + { optsync = false; + optname = "Omega action display flag"; + optkey = SecondaryTable ("Omega","Action"); + optread = read display_action_flag; + optwrite = write display_action_flag } + +let _ = + declare_bool_option + { optsync = false; + optname = "Omega old style flag"; + optkey = SecondaryTable ("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 mk_then = tclTHENLIST + +let exists_tac c = constructor_tac (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 [[], 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 @ [logic_dir] @ arith_modules @ zarith_base_modules + @ [["Coq"; "omega"; "OmegaLemmas"]] + +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_ZERO = lazy (constant (if !Options.v7 then "ZERO" else "Z0")) +let coq_POS = lazy (constant (if !Options.v7 then "POS" else "Zpos")) +let coq_NEG = lazy (constant (if !Options.v7 then "NEG" else "Zneg")) +let coq_Z = lazy (constant "Z") +let coq_relation = lazy (constant (if !Options.v7 then "relation" else "comparison")) +let coq_SUPERIEUR = lazy (constant "SUPERIEUR") +let coq_INFEEIEUR = lazy (constant "INFERIEUR") +let coq_EGAL = lazy (constant "EGAL") +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_Zs = lazy (constant "Zs") +let coq_Zgt = lazy (constant "Zgt") +let coq_Zle = lazy (constant "Zle") +let coq_inject_nat = lazy (constant "inject_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_r = lazy (constant "fast_Zplus_assoc_r") +let coq_fast_Zplus_assoc_l = lazy (constant "fast_Zplus_assoc_l") +let coq_fast_Zmult_assoc_r = lazy (constant "fast_Zmult_assoc_r") +let coq_fast_Zplus_permute = lazy (constant "fast_Zplus_permute") +let coq_fast_Zplus_sym = lazy (constant "fast_Zplus_sym") +let coq_fast_Zmult_sym = lazy (constant "fast_Zmult_sym") +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 = lazy (constant "fast_Zmult_plus_distr") +let coq_fast_Zmult_Zopp_left = lazy (constant "fast_Zmult_Zopp_left") +let coq_fast_Zopp_Zplus = lazy (constant "fast_Zopp_Zplus") +let coq_fast_Zopp_Zmult_r = lazy (constant "fast_Zopp_Zmult_r") +let coq_fast_Zopp_one = lazy (constant "fast_Zopp_one") +let coq_fast_Zopp_Zopp = lazy (constant "fast_Zopp_Zopp") +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_not_Zle = lazy (constant "not_Zle") +let coq_not_Zlt = lazy (constant "not_Zlt") +let coq_not_Zge = lazy (constant "not_Zge") +let coq_not_Zgt = lazy (constant "not_Zgt") +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 (constant "le") +let coq_lt = lazy (constant "lt") +let coq_ge = lazy (constant "ge") +let coq_gt = lazy (constant "gt") +let coq_minus = lazy (constant "minus") +let coq_plus = lazy (constant "plus") +let coq_mult = lazy (constant "mult") +let coq_pred = lazy (constant "pred") +let coq_nat = lazy (constant "nat") +let coq_S = lazy (constant "S") +let coq_O = lazy (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_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_not = lazy (constant "not_not") +let coq_imp_simp = lazy (constant "imp_simp") + +(* 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_Zs = lazy (evaluable_ref_of_constr "Zs" coq_Zs) +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_relation; t1; t2 |]) +let mk_inj t = mkApp (Lazy.force coq_inject_nat, [| t |]) + +let mk_integer n = + let rec loop n = + if n=1 then Lazy.force coq_xH else + mkApp ((if n mod 2 = 0 then Lazy.force coq_xO else Lazy.force coq_xI), + [| loop (n/2) |]) + in + if n = 0 then Lazy.force coq_ZERO + else mkApp ((if n > 0 then Lazy.force coq_POS else Lazy.force coq_NEG), + [| loop (abs n) |]) + +type omega_constant = + | Zplus | Zmult | Zminus | Zs | Zopp + | Plus | Mult | Minus | Pred | S | O + | POS | NEG | ZERO | Inject_nat + | Eq | Neq + | Zne | Zle | Zlt | Zge | Zgt + | Z | Nat + | And | Or | False | True | Not + | 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 = 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 (id_of_global (ConstRef sp))),args) + | Construct csp , args -> + Kapp (Other (string_of_id (id_of_global (ConstructRef csp))), args) + | Ind isp, args -> + Kapp (Other (string_of_id (id_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_Zs -> Kapp (Zs,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_POS -> Kapp (NEG,args) + | _, [_] when c = Lazy.force coq_NEG -> Kapp (POS,args) + | _, [] when c = Lazy.force coq_ZERO -> Kapp (ZERO,args) + | _, [_] when c = Lazy.force coq_inject_nat -> Kapp (Inject_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 -> 1 + 2 * loop t + | f, [t] when f = Lazy.force coq_xO -> 2 * loop t + | f, [] when f = Lazy.force coq_xH -> 1 + | _ -> failwith "not a number" + in + match decompose_app t with + | f, [t] when f = Lazy.force coq_POS -> loop t + | f, [t] when f = Lazy.force coq_NEG -> - (loop t) + | f, [] when f = Lazy.force coq_ZERO -> 0 + | _ -> 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,t)) -> mkCast (loop i p c,t) + | ([], _) -> operation i t + | ((P_APP n :: p), App (f,v)) -> +(* let f,l = get_applist t in NECESSAIRE ?? + let v' = Array.of_list (f::l) in *) + let v' = Array.copy v in + v'.(n-1) <- loop i p v'.(n-1); 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 (i+l) p v.(n); (mkFix (ln,(tys,lna,v'))) + | ((P_BODY :: p), Prod (n,t,c)) -> + (mkProd (n,t,loop (i+1) p c)) + | ((P_BODY :: p), Lambda (n,t,c)) -> + (mkLambda (n,t,loop (i+1) p c)) + | ((P_BODY :: p), LetIn (n,b,t,c)) -> + (mkLetIn (n,b,t,loop (i+1) 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.prterm 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,t)) -> loop p c + | ([], _) -> t + | ((P_APP n :: p), App (f,v)) -> loop p v.(n-1) + | ((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.prterm 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 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 int + | 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_int 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 (Clenv.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_r) + :: 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_r) + :: tac, + Oplus(l1, t') + else + [clever_rewrite p [[P_APP 1];[P_APP 2]] + (Lazy.force coq_fast_Zplus_sym)], + 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(t1+t2) + | t1,t2 -> + if weight t1 < weight t2 then + [clever_rewrite p [[P_APP 1];[P_APP 2]] + (Lazy.force coq_fast_Zplus_sym)], + 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 k1*c1 + k2 * c2 = 0 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 c1 + k2 * c2 = 0 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_r) :: + 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_r) :: + 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 > 0 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) :: + (tac1 @ tac2), Oplus(t1',t2') + | Oinv t -> + [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] + (Lazy.force coq_fast_Zmult_Zopp_left); + focused_simpl (P_APP 2 :: p)], Otimes(t,Oz(-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_r); + 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_r) :: + 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_Zplus) :: + (tac1 @ tac2), + Oplus(t1',t2') + | Oinv t -> + [clever_rewrite p [[P_APP 1;P_APP 1]] (Lazy.force coq_fast_Zopp_Zopp)], 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_Zmult_r); + focused_simpl (P_APP 2 :: p)], Otimes(t1,Oz (-x)) + | Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products" + | (Oatom _ as t) -> + let r = Otimes(t,Oz(-1)) in + [clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zopp_one)], r + | Oz i -> [focused_simpl p],Oz(-i) + | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zopp, [| c |])) + +let rec transform p t = + let default () = + 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 false; + [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(Zs,[t1]) -> + let tac,t = transform p (mkApp (Lazy.force coq_Zplus, + [| t1; mk_integer 1 |])) in + unfold sp_Zs :: 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_sym) in + let tac,t' = scalar p n t2' in tac1 @ tac2 @ (sym :: tac),t' + | _ -> default () + end + | Kapp((POS|NEG|ZERO),_) -> + (try ([],Oz(recognize_number t)) with _ -> default ()) + | 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(Inject_nat,[t']) -> + begin 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 true; + [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v + end + | _ -> default () + with e when catchable_exception e -> default () + +let shrink_pair p f1 f2 = + match f1,f2 with + | Oatom v,Oatom _ -> + let r = Otimes(Oatom v,Oz 2) 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 1)) 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 1)) 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 1) 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) -> 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_l) 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) as t -> + 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 0) 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 0),r) -> + 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 zero = mk_integer 0 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 (-1) else 1 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 superieur = Lazy.force coq_SUPERIEUR in + let not_sup_sup = mkApp (build_coq_eq (), [| + Lazy.force coq_relation; + Lazy.force coq_SUPERIEUR; + Lazy.force coq_SUPERIEUR |]) + 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 zero)) + [ 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 id = hyp_of_tag e1.id in + let c = floor_div e1.constant k in + let d = e1.constant - c * k in + let e2 = {id=e1.id; kind=EQUA;constant = c; + body = map_eq_linear (fun c -> c / k) e1.body } 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_eq = mk_eq eq1 rhs in + let tac = scalar_norm_add [P_APP 2] e2.body in + tclTHENS + (cut (mk_gt dd zero)) + [ 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 zero)) + [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_one) :: + 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(new_eq,def,orig,m,sigma) :: l -> + let id = new_identifier () + and id2 = hyp_of_tag orig.id in + tag_hypothesis id new_eq.id; + let eq1 = val_of(decompile def) + and eq2 = val_of(decompile orig) in + let vid = unintern_id sigma 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 r = mk_plus eq2 (mk_times (mk_plus (mk_inv (mkVar vid)) eq1) mm) in + let tac = + clever_rewrite (P_APP 1 :: P_APP 1 :: P_APP 2 :: p_initial) + [[P_APP 1]] (Lazy.force coq_fast_Zopp_one) :: + shuffle_mult_right p_initial + orig.body m ({c= -1;v=sigma}::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 = 1 & 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 zero)) + [tclTHENS + (cut (mk_gt kk2 zero)) + [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 (-1))) (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 (-1))) (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=1}]; + constant = 0; 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 system; + if !old_style_flag then begin + try let _ = simplify false system in tclIDTAC gl + with UNSOLVABLE -> + let _,path = depend [] [] (history ()) in + if !display_action_flag then display_action path; + (tclTHEN prelude (replay_history tactic_normalisation path)) gl + end else begin + try + let path = simplify_strong system in + if !display_action_flag then display_action 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 aux = id_of_string "auxiliary" in + let table = Hashtbl.create 7 in + 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 0) + ((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_Zs, [| 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 |]) + | 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.prterm 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) + ] + | 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)))) + ] + | 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_not_Zle, [| t1;t2;mkVar i|])]); + (onClearedName i (fun _ -> loop lit)) + ] + | Kapp(Zge, [t1;t2]) -> + tclTHENLIST [ + (generalize_tac + [mkApp (Lazy.force coq_not_Zge, [| t1;t2;mkVar i|])]); + (onClearedName i (fun _ -> loop lit)) + ] + | Kapp(Zlt, [t1;t2]) -> + tclTHENLIST [ + (generalize_tac + [mkApp (Lazy.force coq_not_Zlt, [| t1;t2;mkVar i|])]); + (onClearedName i (fun _ -> loop lit)) + ] + | Kapp(Zgt, [t1;t2]) -> + tclTHENLIST [ + (generalize_tac + [mkApp (Lazy.force coq_not_Zgt, [| 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 = + Library.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/contrib/omega/g_omega.ml4 b/contrib/omega/g_omega.ml4 new file mode 100644 index 00000000..726cf8bc --- /dev/null +++ b/contrib/omega/g_omega.ml4 @@ -0,0 +1,24 @@ +(************************************************************************) +(* 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: g_omega.ml4,v 1.1.12.1 2004/07/16 19:30:13 herbelin Exp $ *) + +open Coq_omega + +TACTIC EXTEND Omega + [ "Omega" ] -> [ omega_solver ] +END diff --git a/contrib/omega/omega.ml b/contrib/omega/omega.ml new file mode 100755 index 00000000..f2eeb5fe --- /dev/null +++ b/contrib/omega/omega.ml @@ -0,0 +1,663 @@ +(************************************************************************) +(* 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: omega.ml,v 1.7.2.1 2004/07/16 19:30:13 herbelin Exp $ *) + +open Util +open Hashtbl +open Names + +let flat_map f = + let rec flat_map_f = function + | [] -> [] + | x :: l -> f x @ flat_map_f l + in + flat_map_f + +let pp i = print_int i; print_newline (); flush stdout + +let debug = ref false + +let filter = List.partition + +let push v l = l := v :: !l + +let rec pgcd x y = if y = 0 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 >=0 , b > 0 with + | true,true -> a / b + | false,false -> a / b + | true, false -> (a-1) / b - 1 + | false,true -> (a+1) / b - 1 + +let new_id = + let cpt = ref 0 in fun () -> incr cpt; ! cpt + +let new_var = + let cpt = ref 0 in fun () -> incr cpt; Nameops.make_ident "WW" (Some !cpt) + +let new_var_num = + let cpt = ref 1000 in (fun () -> incr cpt; !cpt) + +type coeff = {c: int ; 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: int } + +type action = + | DIVIDE_AND_APPROX of afine * afine * int * int + | NOT_EXACT_DIVIDE of afine * int + | FORGET_C of int + | EXACT_DIVIDE of afine * int + | SUM of int * (int * afine) * (int * afine) + | STATE of afine * afine * afine * int * int + | 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 * int + | CONSTANT_NUL of int + | CONSTANT_NEG of int * int + | SPLIT_INEQ of afine * (int * action list) * (int * action list) + | WEAKEN of int * int + +exception UNSOLVABLE + +exception NO_CONTRADICTION + +let intern_id,unintern_id = + let cpt = ref 0 in + let table = create 7 and co_table = create 7 in + (fun (name : identifier) -> + try find table name with Not_found -> + let idx = !cpt in + add table name idx; add co_table idx name; incr cpt; idx), + (fun idx -> + try find co_table idx with Not_found -> + let v = new_var () in add table v idx; add co_table idx v; v) + +let display_eq (l,e) = + let _ = + List.fold_left + (fun not_first f -> + print_string + (if f.c < 0 then "- " else if not_first then "+ " else ""); + let c = abs f.c in + if c = 1 then + Printf.printf "%s " (string_of_id (unintern_id f.v)) + else + Printf.printf "%d %s " c (string_of_id (unintern_id f.v)); + true) + false l + in + if e > 0 then + Printf.printf "+ %d " e + else if e < 0 then + Printf.printf "- %d " (abs e) + +let operator_of_eq = function + | EQUA -> "=" | DISE -> "!=" | INEQ -> ">=" + +let kind_of = function + | EQUA -> "equation" | DISE -> "disequation" | INEQ -> "inequation" + +let display_system l = + List.iter + (fun { kind=b; body=e; constant=c; id=id} -> + print_int id; print_string ": "; + display_eq (e,c); print_string (operator_of_eq b); + print_string "0\n") + l; + print_string "------------------------\n\n" + +let display_inequations l = + List.iter (fun e -> display_eq e;print_string ">= 0\n") l; + print_string "------------------------\n\n" + +let rec display_action = function + | act :: l -> begin match act with + | DIVIDE_AND_APPROX (e1,e2,k,d) -> + Printf.printf + "Inequation E%d is divided by %d and the constant coefficient is \ + rounded by substracting %d.\n" e1.id k d + | NOT_EXACT_DIVIDE (e,k) -> + Printf.printf + "Constant in equation E%d is not divisible by the pgcd \ + %d of its other coefficients.\n" e.id k + | EXACT_DIVIDE (e,k) -> + Printf.printf + "Equation E%d is divided by the pgcd \ + %d of its coefficients.\n" e.id k + | WEAKEN (e,k) -> + Printf.printf + "To ensure a solution in the dark shadow \ + the equation E%d is weakened by %d.\n" e k + | SUM (e,(c1,e1),(c2,e2)) -> + Printf.printf + "We state %s E%d = %d %s E%d + %d %s E%d.\n" + (kind_of e1.kind) e c1 (kind_of e1.kind) e1.id c2 + (kind_of e2.kind) e2.id + | STATE (e,_,_,x,_) -> + Printf.printf "We define a new equation %d :" e.id; + display_eq (e.body,e.constant); + print_string (operator_of_eq e.kind); print_string " 0\n" + | HYP e -> + Printf.printf "We define %d :" e.id; + display_eq (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 implie a contradiction on their \ + constant factors.\n" e1.id e2.id + | NEGATE_CONTRADICT(e1,e2,b) -> + Printf.printf + "Eqations 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 %d=0.\n" e k + | CONSTANT_NEG(e,k) -> + Printf.printf "equation E%d states %d >= 0.\n" e 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 l1; + print_newline (); + display_action l2; + print_newline () + end; display_action l + | [] -> + flush stdout + +(*""*) + +let add_event, history, clear_history = + let accu = ref [] in + (fun (v : action) -> if !debug then display_action [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=0 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 -> -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 = 0 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 eq1 eq2 = + { kind = eq1.kind; id = new_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 = 1 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 =0 then [] else begin + add_event (CONSTANT_NOT_NUL(id,x)); raise UNSOLVABLE + end + | DISE -> + if x <> 0 then [] else begin + add_event (CONSTANT_NUL id); raise UNSOLVABLE + end + | INEQ -> + if x >= 0 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 <> 0 then begin + add_event (NOT_EXACT_DIVIDE (eq,gcd)); raise UNSOLVABLE + end else if eq_flag=DISE & x mod gcd <> 0 then begin + add_event (FORGET_C eq.id); [] + end else if gcd <> 1 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 {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=1 then -f.c else if c_unite= -1 then f.c + else failwith "eliminate_with_in" in + let res = sum_afine eq1 (map_eq_afine (fun c -> c * coeff) eq2) in + add_event (SUM (res.id,(1,eq1),(coeff,eq2))); res + with CHOPVAR -> eq1 + +let omega_mod a b = a - b * floor_div (2 * a + b) (2 * b) +let banerjee_step original l1 l2 = + let e = original.body in + let sigma = new_var_num () 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 [original] ; failwith "TL" in + let m = smallest + 1 in + let new_eq = + { constant = omega_mod original.constant m; + body = {c= -m;v=sigma} :: + map_eq_linear (fun a -> omega_mod a m) original.body; + id = new_id (); kind = EQUA } in + let definition = + { constant = - floor_div (2 * original.constant + m) (2 * m); + body = map_eq_linear (fun a -> - floor_div (2 * a + m) (2 * m)) + original.body; + id = new_id (); kind = EQUA } in + add_event (STATE (new_eq,definition,original,m,sigma)); + let new_eq = List.hd (normalize new_eq) in + let eliminated_var, def = chop_var var new_eq.body in + let other_equations = + flat_map (fun e -> normalize (eliminate_with_in eliminated_var new_eq e)) + l1 in + let inequations = + flat_map (fun e -> normalize (eliminate_with_in eliminated_var new_eq e)) + l2 in + let original' = eliminate_with_in 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 (e,other,ineqs) = + if !debug then display_system (e::other); + try + let v,def = chop_factor_1 e.body in + (flat_map (fun e' -> normalize (eliminate_with_in v e e')) other, + flat_map (fun e' -> normalize (eliminate_with_in v e e')) ineqs) + with FACTOR1 -> eliminate_one_equation (banerjee_step e other ineqs) + +let rec banerjee (sys_eq,sys_ineq) = + let rec fst_eq_1 = function + (eq::l) -> + if List.exists (fun x -> abs x.c = 1) 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 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 = 0 then begin + add_event (FORGET_C eq.id); banerjee (other,sys_ineq) + end else begin + add_event (CONSTANT_NOT_NUL(eq.id,eq.constant)); raise UNSOLVABLE + end + else banerjee (eliminate_one_equation (eq,other,sys_ineq)) +type kind = INVERTED | NORMAL +let redundancy_elimination system = + let normal = function + ({body=f::_} as e) when f.c < 0 -> negate_eq e, INVERTED + | e -> e,NORMAL in + let table = create 7 in + List.iter + (fun e -> + let ({body=ne} as nx) ,kind = normal e in + if ne = [] then + if nx.constant < 0 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) = 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; + remove table ne; + add table ne final + with Not_found -> + 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 + iter + (fun p0 p1 -> match (p0,p1) with + | (e, (Some x, Some y)) when x.constant = y.constant -> + let id=new_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 = create 7 in + let push v c= + try let r = find table v in r := max !r (abs c) + with Not_found -> 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 0 in + let var_cpt = ref 0 in + 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 >= 0 then (not_occ,((f.c,eq) :: below),over) + else (not_occ,below,((-f.c,eq) :: over)) + with CHOPVAR -> (eq::not_occ,below,over)) + ([],[],[]) system + +let product dark_shadow low high = + List.fold_left + (fun accu (a,eq1) -> + List.fold_left + (fun accu (b,eq2) -> + let eq = + sum_afine (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 - 1) * (b - 1) 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 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 dark_shadow ineq_low ineq_high in + if !debug then display_system expanded; expanded + +let simplify 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 = flat_map normalize system in + let eqs,ineqs = filter (fun e -> e.kind=EQUA) system in + let simp_eq,simp_ineq = redundancy_elimination ineqs in + let system = (eqs @ simp_eq,simp_ineq) in + let rec loop1a system = + let sys_ineq = banerjee system in + loop1b sys_ineq + and loop1b sys_ineq = + let simp_eq,simp_ineq = redundancy_elimination 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 dark_shadow system in + loop2 (loop1b expanded) + with SOLVED_SYSTEM -> if !debug then display_system 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 (e,_,_,_,_) -> + if List.mem e.id relie_on then depend 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 solve system = + try let _ = simplify false system in failwith "no contradiction" + with UNSOLVABLE -> display_action (snd (depend [] [] (history ()))) + +let negation (eqs,ineqs) = + let diseq,_ = filter (fun e -> e.kind = DISE) ineqs in + let normal = function + | ({body=f::_} as e) when f.c < 0 -> negate_eq e, INVERTED + | e -> e,NORMAL in + let table = create 7 in + List.iter (fun e -> + let {body=ne;constant=c} ,kind = normal e in + add table (ne,c) (kind,e)) diseq; + List.iter (fun e -> + if e.kind <> EQUA then pp 9999; + let {body=ne;constant=c},kind = normal e in + try + let (kind',e') = 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 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 system in + loop1b sys_ineq + and loop1b sys_ineq = + let dise,ine = filter (fun e -> e.kind = DISE) sys_ineq in + let simp_eq,simp_ineq = redundancy_elimination 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 false system in + loop2 (loop1b expanded) + with SOLVED_SYSTEM -> if !debug then display_system system; system + in + let rec explode_diseq = function + | (de::diseq,ineqs,expl_map) -> + let id1 = new_id () + and id2 = new_id () in + let e1 = + {id = id1; kind=INEQ; body = de.body; constant = de.constant - 1} in + let e2 = + {id = id2; kind=INEQ; body = map_eq_linear (fun x -> -x) de.body; + constant = - de.constant - 1} 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 = flat_map normalize system in + let eqs,ineqs = filter (fun e -> e.kind=EQUA) system in + let dise,ine = filter (fun e -> e.kind = DISE) ineqs in + let simp_eq,simp_ineq = redundancy_elimination ine in + let system = (eqs @ simp_eq,simp_ineq @ dise) in + let system' = loop1a system in + let diseq,ineq = filter (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,_ = filter (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 = create 7 in + let augment x = + try incr (find tbl x) with Not_found -> 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; + 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 = filter (fun (_,_,decomp,_) -> sign decomp) systems in + let s1' = + List.map (fun (dep,ro,dc,pa) -> (list_except id dep,ro,dc,pa)) s1 in + let s2' = + List.map (fun (dep,ro,dc,pa) -> (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 :: 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 ())) |