diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-04-28 17:55:54 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-04-28 17:55:54 +0000 |
| commit | 44d578b40ec699ea8bbd4b387c2cf7155bf1d1fe (patch) | |
| tree | 967ad41944c572fc1252b31369aa0af498f14832 /contrib/omega | |
| parent | bd182166d8a97de81b6abdb3aa434cc32d95a9dc (diff) | |
mise sous CVS d'Omega
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@380 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/omega')
| -rwxr-xr-x | contrib/omega/Omega.v | 41 | ||||
| -rw-r--r-- | contrib/omega/OmegaSyntax.v | 26 | ||||
| -rw-r--r-- | contrib/omega/Zcomplements.v | 313 | ||||
| -rw-r--r-- | contrib/omega/Zlogarithm.v | 267 | ||||
| -rw-r--r-- | contrib/omega/Zpower.v | 396 | ||||
| -rw-r--r-- | contrib/omega/coq_omega.ml | 1878 | ||||
| -rwxr-xr-x | contrib/omega/omega.ml | 652 |
7 files changed, 3573 insertions, 0 deletions
diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v new file mode 100755 index 000000000..185a85969 --- /dev/null +++ b/contrib/omega/Omega.v @@ -0,0 +1,41 @@ +(**************************************************************************) +(* *) +(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) +(* *) +(* Pierre Crégut (CNET, Lannion, France) *) +(* *) +(**************************************************************************) + +Require Export ZArith. +(* The constant minus is required in coq_omega.ml *) +Require Export Minus. + +Declare ML Module "equality". +Declare ML Module "omega". +Declare ML Module "coq_omega". + +Require Export OmegaSyntax. + +Hint eq_nat_Omega : zarith := Extern 10 (eq nat ? ?) Abstract Omega. +Hint le_Omega : zarith := Extern 10 (le ? ?) Abstract Omega. +Hint lt_Omega : zarith := Extern 10 (lt ? ?) Abstract Omega. +Hint ge_Omega : zarith := Extern 10 (ge ? ?) Abstract Omega. +Hint gt_Omega : zarith := Extern 10 (gt ? ?) Abstract Omega. + +Hint not_eq_nat_Omega : zarith := Extern 10 ~(eq nat ? ?) Abstract Omega. +Hint not_le_Omega : zarith := Extern 10 ~(le ? ?) Abstract Omega. +Hint not_lt_Omega : zarith := Extern 10 ~(lt ? ?) Abstract Omega. +Hint not_ge_Omega : zarith := Extern 10 ~(ge ? ?) Abstract Omega. +Hint not_gt_Omega : zarith := Extern 10 ~(gt ? ?) Abstract Omega. + +Hint eq_Z_Omega : zarith := Extern 10 (eq Z ? ?) Abstract Omega. +Hint Zle_Omega : zarith := Extern 10 (Zle ? ?) Abstract Omega. +Hint Zlt_Omega : zarith := Extern 10 (Zlt ? ?) Abstract Omega. +Hint Zge_Omega : zarith := Extern 10 (Zge ? ?) Abstract Omega. +Hint Zgt_Omega : zarith := Extern 10 (Zgt ? ?) Abstract Omega. + +Hint not_eq_nat_Omega : zarith := Extern 10 ~(eq Z ? ?) Abstract Omega. +Hint not_Zle_Omega : zarith := Extern 10 ~(Zle ? ?) Abstract Omega. +Hint not_Zlt_Omega : zarith := Extern 10 ~(Zlt ? ?) Abstract Omega. +Hint not_Zge_Omega : zarith := Extern 10 ~(Zge ? ?) Abstract Omega. +Hint not_Zgt_Omega : zarith := Extern 10 ~(Zgt ? ?) Abstract Omega. diff --git a/contrib/omega/OmegaSyntax.v b/contrib/omega/OmegaSyntax.v new file mode 100644 index 000000000..dccfc5e89 --- /dev/null +++ b/contrib/omega/OmegaSyntax.v @@ -0,0 +1,26 @@ +(**************************************************************************) +(* *) +(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) +(* *) +(* Pierre Crégut (CNET, Lannion, France) *) +(* *) +(**************************************************************************) + +Grammar vernac vernac := + omega_sett [ "Set" "Omega" "Time" "." ] -> [(OmegaFlag "+time")] +| omega_sets [ "Set" "Omega" "System" "." ] -> [(OmegaFlag "+system")] +| omega_seta [ "Set" "Omega" "Action" "." ] -> [(OmegaFlag "+action")] +| omega_unst [ "Unset" "Omega" "Time" "." ] -> [(OmegaFlag "-time")] +| omega_unss [ "Unset" "Omega" "System" "." ] -> [(OmegaFlag "-system")] +| omega_unsa [ "Unset" "Omega" "Action" "." ] -> [(OmegaFlag "-action")] +| omega_swit [ "Switch" "Omega" "Time" "." ] -> [(OmegaFlag "time")] +| omega_swis [ "Switch" "Omega" "System" "." ] -> [(OmegaFlag "system")] +| omega_swia [ "Switch" "Omega" "Action" "." ] -> [(OmegaFlag "action")] +| omega_set [ "Set" "Omega" stringarg($id) "." ] -> [(OmegaFlag $id)]. + + +Grammar tactic simple_tactic := + omega [ "Omega" ] -> [(Omega)]. + +Syntax tactic level 0: + omega [(Omega)] -> ["Omega"]. diff --git a/contrib/omega/Zcomplements.v b/contrib/omega/Zcomplements.v new file mode 100644 index 000000000..6bf081781 --- /dev/null +++ b/contrib/omega/Zcomplements.v @@ -0,0 +1,313 @@ +(****************************************************************************) +(* The Calculus of Inductive Constructions *) +(* *) +(* Projet Coq *) +(* *) +(* INRIA LRI-CNRS ENS-CNRS *) +(* Rocquencourt Orsay Lyon *) +(* *) +(* Coq V6.3 *) +(* July 1st 1999 *) +(* *) +(****************************************************************************) +(* Zcomplements.v *) +(****************************************************************************) + +Require Omega. +Require Wf_nat. + +(* Multiplication by a number >0 preserves Zcompare. It also perserves + Zle, Zlt, Zge, Zgt *) + +Implicit Arguments On. + +Lemma Zmult_zero : (x,y:Z)`x*y=0` -> `x=0` \/ `y=0`. +Destruct x; Destruct y; Auto. +Simpl; Intros; Discriminate H. +Simpl; Intros; Discriminate H. +Simpl; Intros; Discriminate H. +Simpl; Intros; Discriminate H. +Save. + +Lemma Zeq_Zminus : (x,y:Z)x=y -> `x-y = 0`. +Intros; Omega. +Save. + +Lemma Zminus_Zeq : (x,y:Z)`x-y=0` -> x=y. +Intros; Omega. +Save. + +Lemma Zmult_Zminus_distr_l : (x,y,z:Z)`(x-y)*z = x*z - y*z`. +Intros; Unfold Zminus. +Rewrite <- Zopp_Zmult. +Apply Zmult_plus_distr_l. +Save. + +Lemma Zmult_Zminus_distr_r : (x,y,z:Z)`z*(x-y) = z*x - z*y`. +Intros; Rewrite (Zmult_sym z `x-y`). +Rewrite (Zmult_sym z x). +Rewrite (Zmult_sym z y). +Apply Zmult_Zminus_distr_l. +Save. + +Lemma Zmult_reg_left : (x,y,z:Z)`z>0` -> `z*x=z*y` -> x=y. +Intros. +Generalize (Zeq_Zminus H0). +Intro. +Apply Zminus_Zeq. +Rewrite <- (Zmult_Zminus_distr_r x y z) in H1. +Elim (Zmult_zero H1). +Omega. +Trivial. +Save. + +Lemma Zmult_reg_right : (x,y,z:Z)`z>0` -> `x*z=y*z` -> x=y. +Intros x y z Hz. +Rewrite (Zmult_sym x z). +Rewrite (Zmult_sym y z). +Intro; Apply Zmult_reg_left with z; Assumption. +Save. + +Lemma Zgt0_le_pred : (y:Z) `y > 0` -> `0 <= (Zpred y)`. +Intro; Unfold Zpred; Omega. +Save. + +Lemma Zlt_Zplus : + (x1,x2,y1,y2:Z)`x1 < x2` -> `y1 < y2` -> `x1 + y1 < x2 + y2`. +Intros; Omega. +Save. + +Lemma Zlt_Zmult_right : (x,y,z:Z)`z>0` -> `x < y` -> `x*z < y*z`. + +Intros; Rewrite (Zs_pred z); Generalize (Zgt0_le_pred H); Intro; +Apply natlike_ind with P:=[z:Z]`x*(Zs z) < y*(Zs z)`; +[ Simpl; Do 2 (Rewrite Zmult_n_1); Assumption +| Unfold Zs; Intros x0 Hx0; Do 6 (Rewrite Zmult_plus_distr_r); + Repeat (Rewrite Zmult_n_1); + Intro; Apply Zlt_Zplus; Assumption +| Assumption ]. +Save. + +Lemma Zlt_Zmult_right2 : (x,y,z:Z)`z>0` -> `x*z < y*z` -> `x < y`. +Intros x y z H; Rewrite (Zs_pred z). +Apply natlike_ind with P:=[z:Z]`x*(Zs z) < y*(Zs z)`->`x < y`. +Simpl; Do 2 Rewrite Zmult_n_1; Auto 1. +Unfold Zs. +Intros x0 Hx0; Repeat (Rewrite Zmult_plus_distr_r). +Repeat Rewrite Zmult_n_1. +Auto with zarith. +Unfold Zpred; Omega. +Save. + +Lemma Zle_Zmult_right : (x,y,z:Z)`z>0` -> `x <= y` -> `x*z <= y*z`. +Intros x y z Hz Hxy. +Elim (Zle_lt_or_eq x y Hxy). +Intros; Apply Zlt_le_weak. +Apply Zlt_Zmult_right; Trivial. +Intros; Apply Zle_refl. +Rewrite H; Trivial. +Save. + +Lemma Zle_Zmult_right2 : (x,y,z:Z)`z>0` -> `x*z <= y*z` -> `x <= y`. +Intros x y z Hz Hxy. +Elim (Zle_lt_or_eq `x*z` `y*z` Hxy). +Intros; Apply Zlt_le_weak. +Apply Zlt_Zmult_right2 with z; Trivial. +Intros; Apply Zle_refl. +Apply Zmult_reg_right with z; Trivial. +Save. + +Lemma Zgt_Zmult_right : (x,y,z:Z)`z>0` -> `x > y` -> `x*z > y*z`. + +Intros; Apply Zlt_gt; Apply Zlt_Zmult_right; +[ Assumption | Apply Zgt_lt ; Assumption ]. +Save. + +Lemma Zlt_Zmult_left : (x,y,z:Z)`z>0` -> `x < y` -> `z*x < z*y`. + +Intros; +Rewrite (Zmult_sym z x); Rewrite (Zmult_sym z y); +Apply Zlt_Zmult_right; Assumption. +Save. + +Lemma Zgt_Zmult_left : (x,y,z:Z)`z>0` -> `x > y` -> `z*x > z*y`. +Intros; +Rewrite (Zmult_sym z x); Rewrite (Zmult_sym z y); +Apply Zgt_Zmult_right; Assumption. +Save. + +Theorem Zcompare_Zmult_right : (x,y,z:Z)` z>0` -> `x ?= y`=`x*z ?= y*z`. + +Intros; Apply Zcompare_egal_dec; +[ Intros; Apply Zlt_Zmult_right; Trivial +| Intro Hxy; Apply [a,b:Z](let (t1,t2)=(Zcompare_EGAL a b) in t2); + Rewrite ((let (t1,t2)=(Zcompare_EGAL x y) in t1) Hxy); Trivial +| Intros; Apply Zgt_Zmult_right; Trivial +]. +Save. + +Theorem Zcompare_Zmult_left : (x,y,z:Z)`z>0` -> `x ?= y`=`z*x ?= z*y`. +Intros; +Rewrite (Zmult_sym z x); +Rewrite (Zmult_sym z y); +Apply Zcompare_Zmult_right; Assumption. +Save. + + +Section diveucl. + +Lemma two_or_two_plus_one : (x:Z) { y:Z | `x = 2*y`}+{ y:Z | `x = 2*y+1`}. +Destruct x. +Left ; Split with ZERO; Reflexivity. + +Destruct p. +Right ; Split with (POS p0); Reflexivity. + +Left ; Split with (POS p0); Reflexivity. + +Right ; Split with ZERO; Reflexivity. + +Destruct p. +Right ; Split with (NEG (add xH p0)). +Rewrite NEG_xI. +Rewrite NEG_add. +Omega. + +Left ; Split with (NEG p0); Reflexivity. + +Right ; Split with `-1`; Reflexivity. +Save. + +(* The biggest power of 2 that is stricly less than a *) +(* Easy to compute : replace all "1" of the binary representation by + "0", except the first "1" (or the first one :-) *) +Fixpoint floor_pos [a : positive] : positive := + Cases a of + | xH => xH + | (xO a') => (xO (floor_pos a')) + | (xI b') => (xO (floor_pos b')) + end. + +Definition floor := [a:positive](POS (floor_pos a)). + +Lemma floor_gt0 : (x:positive) `(floor x) > 0`. +Intro. +Compute. +Trivial. +Save. + +Lemma floor_ok : (a:positive) + `(floor a) <= (POS a) < 2*(floor a)`. +Unfold floor. +Induction a. + +Intro p; Simpl. +Repeat Rewrite POS_xI. +Rewrite (POS_xO (xO (floor_pos p))). +Rewrite (POS_xO (floor_pos p)). +Omega. + +Intro p; Simpl. +Repeat Rewrite POS_xI. +Rewrite (POS_xO (xO (floor_pos p))). +Rewrite (POS_xO (floor_pos p)). +Rewrite (POS_xO p). +Omega. + +Simpl; Omega. +Save. + +Lemma Zdiv_eucl_POS : (b:Z)`b > 0` -> (p:positive) + { qr:Z*Z | let (q,r)=qr in `(POS p)=b*q+r` /\ `0 <= r < b` }. + +Induction p. + +(* p => (xI p) *) +(* Notez l'utilisation des nouveaux patterns Intro *) +Intros p' ((q,r), (Hrec1, Hrec2)). +Elim (Z_lt_ge_dec `2*r+1` b); +[ Exists `(2*q, 2*r+1)`; + Rewrite POS_xI; + Rewrite Hrec1; + Split; + [ Rewrite Zmult_Zplus_distr; + Rewrite Zplus_assoc_l; + Rewrite (Zmult_permute b `2`); + Reflexivity + | Omega ] +| Exists `(2*q+1, 2*r+1-b)`; + Rewrite POS_xI; + Rewrite Hrec1; + Split; + [ Do 2 Rewrite Zmult_Zplus_distr; + Unfold Zminus; + Do 2 Rewrite Zplus_assoc_l; + Rewrite <- (Zmult_permute `2` b); + Generalize `b*q`; Intros; Omega + | Omega ] +]. + +(* p => (xO p) *) +Intros p' ((q,r), (Hrec1, Hrec2)). +Elim (Z_lt_ge_dec `2*r` b); +[ Exists `(2*q,2*r)`; + Rewrite POS_xO; + Rewrite Hrec1; + Split; + [ Rewrite Zmult_Zplus_distr; + Rewrite (Zmult_permute b `2`); + Reflexivity + | Omega ] +| Exists `(2*q+1, 2*r-b)`; + Rewrite POS_xO; + Rewrite Hrec1; + Split; + [ Do 2 Rewrite Zmult_Zplus_distr; + Unfold Zminus; + Rewrite <- (Zmult_permute `2` b); + Generalize `b*q`; Intros; Omega + | Omega ] +]. +(* xH *) +Elim (Z_le_gt_dec `2` b); +[ Exists `(0,1)`; Omega +| Exists `(1,0)`; Omega +]. +Save. + +Theorem Zdiv_eucl : (b:Z)`b > 0` -> (a:Z) + { qr:Z*Z | let (q,r)=qr in `a=b*q+r` /\ `0 <= r < b` }. +Destruct a; + +[ (* a=0 *) Exists `(0,0)`; Omega +| (* a = (POS p) *) Intros; Apply Zdiv_eucl_POS; Auto +| (* a = (NEG p) *) Intros; Elim (Zdiv_eucl_POS H p); + Intros (q,r) (Hp1, Hp2); + Elim (Z_le_gt_dec r `0`); + [ Exists `(-q,0)`; Split; + [ Apply Zopp_intro; Simpl; Rewrite Hp1; + Rewrite Zero_right; + Rewrite <- Zopp_Zmult; + Rewrite Zmult_Zopp_Zopp; + Generalize `b*q`; Intro; Omega + | Omega + ] + | Exists `(-(q+1),b-r)`; Split; + [ Apply Zopp_intro; + Unfold Zminus; Simpl; Rewrite Hp1; + Repeat Rewrite Zopp_Zplus; + Repeat Rewrite <- Zopp_Zmult; + Rewrite Zmult_Zplus_distr; + Rewrite Zmult_Zopp_Zopp; + Rewrite Zplus_assoc_r; + Apply f_equal with f:=[c:Z]`b*q+c`; + Omega + | Omega ] + ] +]. +Save. + +End diveucl. + +(* $Id$ *) + diff --git a/contrib/omega/Zlogarithm.v b/contrib/omega/Zlogarithm.v new file mode 100644 index 000000000..87f1f87c5 --- /dev/null +++ b/contrib/omega/Zlogarithm.v @@ -0,0 +1,267 @@ +(****************************************************************************) +(* The Calculus of Inductive Constructions *) +(* *) +(* Projet Coq *) +(* *) +(* INRIA LRI-CNRS ENS-CNRS *) +(* Rocquencourt Orsay Lyon *) +(* *) +(* Coq V6.3 *) +(* July 1st 1999 *) +(* *) +(****************************************************************************) +(* Zlogarithm.v *) +(****************************************************************************) + +(****************************************************************************) +(* The integer logarithms with base 2. There are three logarithms, *) +(* depending on the rounding of the real 2-based logarithm : *) +(* *) +(* Log_inf : y = (Log_inf x) iff 2^y <= x < 2^(y+1) *) +(* Log_sup : y = (Log_sup x) iff 2^(y-1) < x <= 2^y *) +(* Log_nearest : y= (Log_nearest x) iff 2^(y-1/2) < x <= 2^(y+1/2) *) +(* *) +(* (Log_inf x) is the biggest integer that is smaller than (Log x) *) +(* (Log_inf x) is the smallest integer that is bigger than (Log x) *) +(* (Log_nearest x) is the integer nearest from (Log x). *) +(****************************************************************************) + +Require Omega. +Require Zcomplements. +Require Zpower. + +Section Log_pos. (* Log of positive integers *) + +(* First we build log_inf and log_sup *) + +Fixpoint log_inf [p:positive] : Z := + Cases p of + xH => `0` (* 1 *) + | (xO q) => (Zs (log_inf q)) (* 2n *) + | (xI q) => (Zs (log_inf q)) (* 2n+1 *) + end. +Fixpoint log_sup [p:positive] : Z := + Cases p of + xH => `0` (* 1 *) + | (xO n) => (Zs (log_sup n)) (* 2n *) + | (xI n) => (Zs (Zs (log_inf n))) (* 2n+1 *) + end. + +Hints Unfold log_inf log_sup. + +(* Then we give the specifications of log_inf and log_sup + and prove their validity *) + +(* Hints Resolve ZERO_le_S : zarith. *) +Hints Resolve Zle_trans : zarith. + +Theorem log_inf_correct : (x:positive) ` 0 <= (log_inf x)` /\ + ` (two_p (log_inf x)) <= (POS x) < (two_p (Zs (log_inf x)))`. +Induction x; Intros; Simpl; +[ Elim H; Intros Hp HR; Clear H; Split; + [ Auto with zarith + | Rewrite (two_p_S (Zs (log_inf p)) (Zle_le_S `0` (log_inf p) Hp)); + Rewrite (two_p_S (log_inf p) Hp); + Rewrite (two_p_S (log_inf p) Hp) in HR; + Rewrite (POS_xI p); Omega ] +| Elim H; Intros Hp HR; Clear H; Split; + [ Auto with zarith + | Rewrite (two_p_S (Zs (log_inf p)) (Zle_le_S `0` (log_inf p) Hp)); + Rewrite (two_p_S (log_inf p) Hp); + Rewrite (two_p_S (log_inf p) Hp) in HR; + Rewrite (POS_xO p); Omega ] +| Unfold two_power_pos; Unfold shift_pos; Simpl; Omega +]. +Save. + +Definition log_inf_correct1 := + [p:positive](proj1 ? ? (log_inf_correct p)). +Definition log_inf_correct2 := + [p:positive](proj2 ? ? (log_inf_correct p)). + +Opaque log_inf_correct1 log_inf_correct2. +Hints Resolve log_inf_correct1 log_inf_correct2 : zarith. + +Lemma log_sup_correct1 : (p:positive)` 0 <= (log_sup p)`. +Induction p; Intros; Simpl; Auto with zarith. +Save. + +(* For every p, either p is a power of two and (log_inf p)=(log_sup p) + either (log_sup p)=(log_inf p)+1 *) + +Theorem log_sup_log_inf : (p:positive) + either (POS p)=(two_p (log_inf p)) + and_then (POS p)=(two_p (log_sup p)) + or_else ` (log_sup p)=(Zs (log_inf p))`. + +Induction p; Intros; +[ Elim H; Right; Simpl; + Rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0)); + Rewrite POS_xI; Unfold Zs; Omega +| Elim H; Clear H; Intro Hif; + [ Left; Simpl; + Rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0)); + Rewrite (two_p_S (log_sup p0) (log_sup_correct1 p0)); + Rewrite <- (proj1 ? ? Hif); Rewrite <- (proj2 ? ? Hif); + Auto + | Right; Simpl; + Rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0)); + Rewrite POS_xO; Unfold Zs; Omega ] +| Left; Auto ]. +Save. + +Theorem log_sup_correct2 : (x:positive) + ` (two_p (Zpred (log_sup x))) < (POS x) <= (two_p (log_sup x))`. + +Intro. +Elim (log_sup_log_inf x). +(* x is a power of two and log_sup = log_inf *) +Intros (E1,E2); Rewrite E2. +Split ; [ Apply two_p_pred; Apply log_sup_correct1 | Apply Zle_n ]. +Intros (E1,E2); Rewrite E2. +Rewrite <- (Zpred_Sn (log_inf x)). +Generalize (log_inf_correct2 x); Omega. +Save. + +Lemma log_inf_le_log_sup : + (p:positive) `(log_inf p) <= (log_sup p)`. +Induction p; Simpl; Intros; Omega. +Save. + +Lemma log_sup_le_Slog_inf : + (p:positive) `(log_sup p) <= (Zs (log_inf p))`. +Induction p; Simpl; Intros; Omega. +Save. + +(* Now it's possible to specify and build the Log rounded to the nearest *) + +Fixpoint log_near[x:positive] : Z := + Cases x of + xH => `0` + | (xO xH) => `1` + | (xI xH) => `2` + | (xO y) => (Zs (log_near y)) + | (xI y) => (Zs (log_near y)) + end. + +Theorem log_near_correct1 : (p:positive)` 0 <= (log_near p)`. +Induction p; Simpl; Intros; +[Elim p0; Auto with zarith | Elim p0; Auto with zarith | Trivial with zarith ]. +Intros; Apply Zle_le_S. +Generalize H0; Elim p1; Intros; Simpl; + [ Tauto | Tauto | Apply ZERO_le_POS ]. +Intros; Apply Zle_le_S. +Generalize H0; Elim p1; Intros; Simpl; + [ Tauto | Tauto | Apply ZERO_le_POS ]. +Save. + +Theorem log_near_correct2: (p:positive) + (log_near p)=(log_inf p) +\/(log_near p)=(log_sup p). +Induction p. +Intros p0 [Einf|Esup]. +Simpl. Rewrite Einf. +Case p0; [Left | Left | Right]; Reflexivity. +Simpl; Rewrite Esup. +Elim (log_sup_log_inf p0). +Generalize (log_inf_le_log_sup p0). +Generalize (log_sup_le_Slog_inf p0). +Case p0; Auto with zarith. +Intros; Omega. +Case p0; Intros; Auto with zarith. +Intros p0 [Einf|Esup]. +Simpl. +Repeat Rewrite Einf. +Case p0; Intros; Auto with zarith. +Simpl. +Repeat Rewrite Esup. +Case p0; Intros; Auto with zarith. +Auto. +Save. + +(******************* +Theorem log_near_correct: (p:positive) + `| (two_p (log_near p)) - (POS p) | <= (POS p)-(two_p (log_inf p))` + /\`| (two_p (log_near p)) - (POS p) | <= (two_p (log_sup p))-(POS p)`. +Intro. +Induction p. +Intros p0 [(Einf1,Einf2)|(Esup1,Esup2)]. +Unfold log_near log_inf log_sup. Fold log_near log_inf log_sup. +Rewrite Einf1. +Repeat Rewrite two_p_S. +Case p0; [Left | Left | Right]. + +Split. +Simpl. +Rewrite E1; Case p0; Try Reflexivity. +Compute. +Unfold log_near; Fold log_near. +Unfold log_inf; Fold log_inf. +Repeat Rewrite E1. +Split. +***********************************) + +End Log_pos. + +Section divers. + +(* Number of significative digits. *) + +Definition N_digits := + [x:Z]Cases x of + (POS p) => (log_inf p) + | (NEG p) => (log_inf p) + | ZERO => `0` + end. + +Lemma ZERO_le_N_digits : (x:Z) ` 0 <= (N_digits x)`. +Induction x; Simpl; +[ Apply Zle_n +| Exact log_inf_correct1 +| Exact log_inf_correct1]. +Save. + +Lemma log_inf_shift_nat : + (n:nat)(log_inf (shift_nat n xH))=(inject_nat n). +Induction n; Intros; +[ Try Trivial +| Rewrite -> inj_S; Rewrite <- H; Reflexivity]. +Save. + +Lemma log_sup_shift_nat : + (n:nat)(log_sup (shift_nat n xH))=(inject_nat n). +Induction n; Intros; +[ Try Trivial +| Rewrite -> inj_S; Rewrite <- H; Reflexivity]. +Save. + +(* (Is_power p) means that p is a power of two *) +Fixpoint Is_power[p:positive] : Prop := + Cases p of + xH => True + | (xO q) => (Is_power q) + | (xI q) => False + end. + +Lemma Is_power_correct : + (p:positive) (Is_power p) <-> (Ex [y:nat](p=(shift_nat y xH))). + +Split; +[ Elim p; + [ Simpl; Tauto + | Simpl; Intros; Generalize (H H0); Intro H1; Elim H1; Intros y0 Hy0; + Exists (S y0); Rewrite Hy0; Reflexivity + | Intro; Exists O; Reflexivity] +| Intros; Elim H; Intros; Rewrite -> H0; Elim x; Intros; Simpl; Trivial]. +Save. + +Lemma Is_power_or : (p:positive) (Is_power p)\/~(Is_power p). +Induction p; +[ Intros; Right; Simpl; Tauto +| Intros; Elim H; + [ Intros; Left; Simpl; Exact H0 + | Intros; Right; Simpl; Exact H0] +| Left; Simpl; Trivial]. +Save. + +End divers. diff --git a/contrib/omega/Zpower.v b/contrib/omega/Zpower.v new file mode 100644 index 000000000..475638ce2 --- /dev/null +++ b/contrib/omega/Zpower.v @@ -0,0 +1,396 @@ +(****************************************************************************) +(* The Calculus of Inductive Constructions *) +(* *) +(* Projet Coq *) +(* *) +(* INRIA LRI-CNRS ENS-CNRS *) +(* Rocquencourt Orsay Lyon *) +(* *) +(* Coq V6.3 *) +(* July 1st 1999 *) +(* *) +(****************************************************************************) +(* Zpower.v *) +(****************************************************************************) + +Require Omega. +Require Zcomplements. + +Section section1. + +(* (Zpower_nat z n) is the n-th power of x when n is an unary + integer (type nat) and z an signed integer (type Z) *) + +Definition Zpower_nat := + [z:Z][n:nat] (iter_nat n Z ([x:Z]` z * x `) `1`). + +(* Zpower_nat_is_exp says Zpower_nat is a morphism for + plus : nat->nat and Zmult : Z->Z *) + +Lemma Zpower_nat_is_exp : + (n,m:nat)(z:Z) + `(Zpower_nat z (plus n m)) = (Zpower_nat z n)*(Zpower_nat z m)`. + +Intros; Elim n; +[ Simpl; Elim (Zpower_nat z m); Auto with zarith +| Unfold Zpower_nat; Intros; Simpl; Rewrite H; + Apply Zmult_assoc]. +Save. + +(* (Zpower_nat z n) is the n-th power of x when n is an binary + integer (type positive) and z an signed integer (type Z) *) + +Definition Zpower_pos := + [z:Z][n:positive] (iter_pos n Z ([x:Z]`z * x`) `1`). + +(* This theorem shows that powers of unary and binary integers + are the same thing, modulo the function convert : positive -> nat *) + +Theorem Zpower_pos_nat : + (z:Z)(p:positive)(Zpower_pos z p) = (Zpower_nat z (convert p)). + +Intros; Unfold Zpower_pos; Unfold Zpower_nat; Apply iter_convert. +Save. + +(* Using the theorem Zpower_pos_nat and the lemma Zpower_nat_is_exp we + deduce that the function [n:positive](Zpower_pos z n) is a morphism + for add : positive->positive and Zmult : Z->Z *) + +Theorem Zpower_pos_is_exp : + (n,m:positive)(z:Z) + ` (Zpower_pos z (add n m)) = (Zpower_pos z n)*(Zpower_pos z m)`. + +Intros. +Rewrite -> (Zpower_pos_nat z n). +Rewrite -> (Zpower_pos_nat z m). +Rewrite -> (Zpower_pos_nat z (add n m)). +Rewrite -> (convert_add n m). +Apply Zpower_nat_is_exp. +Save. + +Definition Zpower := + [x,y:Z]Cases y of + (POS p) => (Zpower_pos x p) + | ZERO => `1` + | (NEG p) => `0` + end. + +Hints Immediate Zpower_nat_is_exp : zarith. +Hints Immediate Zpower_pos_is_exp : zarith. +Hints Unfold Zpower_pos : zarith. +Hints Unfold Zpower_nat : zarith. + +Lemma Zpower_exp : (x:Z)(n,m:Z) + `n >= 0` -> `m >= 0` -> `(Zpower x (n+m))=(Zpower x n)*(Zpower x m)`. +Destruct n; Destruct m; Auto with zarith. +Simpl; Intros; Apply Zred_factor0. +Simpl; Auto with zarith. +Intros; Compute in H0; Absurd INFERIEUR=INFERIEUR; Auto with zarith. +Intros; Compute in H0; Absurd INFERIEUR=INFERIEUR; Auto with zarith. +Save. + +End section1. + +Hints Immediate Zpower_nat_is_exp : zarith. +Hints Immediate Zpower_pos_is_exp : zarith. +Hints Unfold Zpower_pos : zarith. +Hints Unfold Zpower_nat : zarith. + +Section Powers_of_2. + +(* For the powers of two, that will be widely used, a more direct + calculus is possible. We will also prove some properties such + as (x:positive) x < 2^x that are true for all integers bigger + than 2 but more difficult to prove and useless. *) + +(* shift n m computes 2^n * m, or m shifted by n positions *) + +Definition shift_nat := + [n:nat][z:positive](iter_nat n positive xO z). +Definition shift_pos := + [n:positive][z:positive](iter_pos n positive xO z). +Definition shift := + [n:Z][z:positive] + Cases n of + ZERO => z + | (POS p) => (iter_pos p positive xO z) + | (NEG p) => z + end. + +Definition two_power_nat := [n:nat] (POS (shift_nat n xH)). +Definition two_power_pos := [x:positive] (POS (shift_pos x xH)). + +Lemma two_power_nat_S : + (n:nat)` (two_power_nat (S n)) = 2*(two_power_nat n)`. +Intro; Simpl; Apply refl_equal. +Save. + +Lemma shift_nat_plus : + (n,m:nat)(x:positive) + (shift_nat (plus n m) x)=(shift_nat n (shift_nat m x)). + +Intros; Unfold shift_nat; Apply iter_nat_plus. +Save. + +Theorem shift_nat_correct : + (n:nat)(x:positive)(POS (shift_nat n x))=`(Zpower_nat 2 n)*(POS x)`. + +Unfold shift_nat; Induction n; +[ Simpl; Trivial with zarith +| Intros; Simpl; +Replace (Zpower_nat `2` (S n0)) with `2 * (Zpower_nat 2 n0)`; +[ Replace (POS (xO (iter_nat n0 positive xO x))) + with `2 * (POS (iter_nat n0 positive xO x))`; + [ Rewrite -> (H x); Apply Zmult_assoc + | Auto with zarith ] +| Auto with zarith ] +]. +Save. + +Theorem two_power_nat_correct : + (n:nat)(two_power_nat n)=(Zpower_nat `2` n). + +Intro n. +Unfold two_power_nat. +Rewrite -> (shift_nat_correct n). +Omega. +Save. + +(* Second we show that two_power_pos and two_power_nat are the same *) +Lemma shift_pos_nat : (p:positive)(x:positive) + (shift_pos p x)=(shift_nat (convert p) x). + +Unfold shift_pos. +Unfold shift_nat. +Intros; Apply iter_convert. +Save. + +Lemma two_power_pos_nat : + (p:positive) (two_power_pos p)=(two_power_nat (convert p)). + +Intro; Unfold two_power_pos; Unfold two_power_nat. +Apply f_equal with f:=POS. +Apply shift_pos_nat. +Save. + +(* Then we deduce that two_power_pos is also correct *) + +Theorem shift_pos_correct : + (p,x:positive) ` (POS (shift_pos p x)) = (Zpower_pos 2 p) * (POS x)`. + +Intros. +Rewrite -> (shift_pos_nat p x). +Rewrite -> (Zpower_pos_nat `2` p). +Apply shift_nat_correct. +Save. + +Theorem two_power_pos_correct : + (x:positive) (two_power_pos x)=(Zpower_pos `2` x). + +Intro. +Rewrite -> two_power_pos_nat. +Rewrite -> Zpower_pos_nat. +Apply two_power_nat_correct. +Save. + +(* Some consequences *) + +Theorem two_power_pos_is_exp : + (x,y:positive) (two_power_pos (add x y)) + =(Zmult (two_power_pos x) (two_power_pos y)). +Intros. +Rewrite -> (two_power_pos_correct (add x y)). +Rewrite -> (two_power_pos_correct x). +Rewrite -> (two_power_pos_correct y). +Apply Zpower_pos_is_exp. +Save. + +(* The exponentiation z -> 2^z for z a signed integer. *) +(* For convenience, we assume that 2^z = 0 for all z <0 *) +(* We could also define a inductive type Log_result with *) +(* 3 contructors Zero | Pos positive -> | minus_infty *) +(* but it's more complexe and not so useful. *) + +Definition two_p := + [x:Z]Cases x of + ZERO => `1` + | (POS y) => (two_power_pos y) + | (NEG y) => `0` + end. + +Theorem two_p_is_exp : + (x,y:Z) ` 0 <= x` -> ` 0 <= y` -> + ` (two_p (x+y)) = (two_p x)*(two_p y)`. +Induction x; +[ Induction y; Simpl; Auto with zarith +| Induction y; + [ Unfold two_p; Rewrite -> (Zmult_sym (two_power_pos p) `1`); + Rewrite -> (Zmult_one (two_power_pos p)); Auto with zarith + | Unfold Zplus; Unfold two_p; + Intros; Apply two_power_pos_is_exp + | Intros; Unfold Zle in H0; Unfold Zcompare in H0; + Absurd SUPERIEUR=SUPERIEUR; Trivial with zarith + ] +| Induction y; + [ Simpl; Auto with zarith + | Intros; Unfold Zle in H; Unfold Zcompare in H; + Absurd (SUPERIEUR=SUPERIEUR); Trivial with zarith + | Intros; Unfold Zle in H; Unfold Zcompare in H; + Absurd (SUPERIEUR=SUPERIEUR); Trivial with zarith + ] +]. +Save. + +Lemma two_p_gt_ZERO : (x:Z) ` 0 <= x` -> ` (two_p x) > 0`. +Induction x; Intros; +[ Simpl; Omega +| Simpl; Unfold two_power_pos; Apply POS_gt_ZERO +| Absurd ` 0 <= (NEG p)`; + [ Simpl; Unfold Zle; Unfold Zcompare; + Do 2 Unfold not; Auto with zarith + | Assumption ] +]. +Save. + +Lemma two_p_S : (x:Z) ` 0 <= x` -> + `(two_p (Zs x)) = 2 * (two_p x)`. +Intros; Unfold Zs. +Rewrite (two_p_is_exp x `1` H (ZERO_le_POS xH)). +Apply Zmult_sym. +Save. + +Lemma two_p_pred : + (x:Z)` 0 <= x` -> ` (two_p (Zpred x)) < (two_p x)`. +Intros; Apply natlike_ind +with P:=[x:Z]` (two_p (Zpred x)) < (two_p x)`; +[ Simpl; Unfold Zlt; Auto with zarith +| Intros; Elim (Zle_lt_or_eq `0` x0 H0); + [ Intros; + Replace (two_p (Zpred (Zs x0))) + with (two_p (Zs (Zpred x0))); + [ Rewrite -> (two_p_S (Zpred x0)); + [ Rewrite -> (two_p_S x0); + [ Omega + | Assumption] + | Apply Zlt_ZERO_pred_le_ZERO; Assumption] + | Rewrite <- (Zs_pred x0); Rewrite <- (Zpred_Sn x0); Trivial with zarith] + | Intro Hx0; Rewrite <- Hx0; Simpl; Unfold Zlt; Auto with zarith] +| Assumption]. +Save. + +Lemma Zlt_lt_double : (x,y:Z) ` 0 <= x < y` -> ` x < 2*y`. +Intros; Omega. Save. + +End Powers_of_2. + +Hints Resolve two_p_gt_ZERO : zarith. +Hints Immediate two_p_pred two_p_S : zarith. + +Section power_div_with_rest. + +(* Division by a power of two + To n:Z and p:positive q,r are associated such that + n = 2^p.q + r and 0 <= r < 2^p *) + +(* Invariant : d*q + r = d'*q + r /\ d' = 2*d /\ 0<= r < d /\ 0 <= r' < d' *) +Definition Zdiv_rest_aux := + [qrd:(Z*Z)*Z] + let (qr,d)=qrd in let (q,r)=qr in + (Cases q of + ZERO => ` (0, r)` + | (POS xH) => ` (0, d + r)` + | (POS (xI n)) => ` ((POS n), d + r)` + | (POS (xO n)) => ` ((POS n), r)` + | (NEG xH) => ` (-1, d + r)` + | (NEG (xI n)) => ` ((NEG n) - 1, d + r)` + | (NEG (xO n)) => ` ((NEG n), r)` + end, ` 2*d`). + +Definition Zdiv_rest := + [x:Z][p:positive]let (qr,d)=(iter_pos p ? Zdiv_rest_aux ((x,`0`),`1`)) in qr. + +Lemma Zdiv_rest_correct1 : + (x:Z)(p:positive) + let (qr,d)=(iter_pos p ? Zdiv_rest_aux ((x,`0`),`1`)) in d=(two_power_pos p). + +Intros x p; +Rewrite (iter_convert p ? Zdiv_rest_aux ((x,`0`),`1`)); +Rewrite (two_power_pos_nat p); +Elim (convert p); Simpl; +[ Trivial with zarith +| Intro n; Rewrite (two_power_nat_S n); + Unfold 2 Zdiv_rest_aux; + Elim (iter_nat n (Z*Z)*Z Zdiv_rest_aux ((x,`0`),`1`)); + Destruct y; Intros; Apply f_equal with f:=[z:Z]`2*z`; Assumption ]. +Save. + +Lemma Zdiv_rest_correct2 : + (x:Z)(p:positive) + let (qr,d)=(iter_pos p ? Zdiv_rest_aux ((x,`0`),`1`)) in + let (q,r)=qr in + ` x=q*d + r` /\ ` 0 <= r < d`. + +Intros; Apply iter_pos_invariant with + f:=Zdiv_rest_aux + Inv:=[qrd:(Z*Z)*Z]let (qr,d)=qrd in let (q,r)=qr in + ` x=q*d + r` /\ ` 0 <= r < d`; +[ Intro x0; Elim x0; Intro y0; Elim y0; + Intros q r d; Unfold Zdiv_rest_aux; + Elim q; + [ Omega + | Destruct p0; + [ Intro; Rewrite POS_xI; Intro; Elim H; Intros; Split; + [ Rewrite H0; Rewrite Zplus_assoc; + Rewrite Zmult_plus_distr_l; + Rewrite Zmult_1_n; Rewrite Zmult_assoc; + Rewrite (Zmult_sym (POS p1) `2`); Apply refl_equal + | Omega ] + | Intro; Rewrite POS_xO; Intro; Elim H; Intros; Split; + [ Rewrite H0; + Rewrite Zmult_assoc; Rewrite (Zmult_sym (POS p1) `2`); + Apply refl_equal + | Omega ] + | Omega ] + | Destruct p0; + [ Intro; Rewrite NEG_xI; Unfold Zminus; Intro; Elim H; Intros; Split; + [ Rewrite H0; Rewrite Zplus_assoc; + Apply f_equal with f:=[z:Z]`z+r`; + Do 2 (Rewrite Zmult_plus_distr_l); + Rewrite Zmult_assoc; + Rewrite (Zmult_sym (NEG p1) `2`); + Rewrite <- Zplus_assoc; + Apply f_equal with f:=[z:Z]`2 * (NEG p1) * d + z`; + Omega + | Omega ] + | Intro; Rewrite NEG_xO; Unfold Zminus; Intro; Elim H; Intros; Split; + [ Rewrite H0; + Rewrite Zmult_assoc; Rewrite (Zmult_sym (NEG p1) `2`); + Apply refl_equal + | Omega ] + | Omega ] ] +| Omega]. +Save. + +Inductive Set Zdiv_rest_proofs[x:Z; p:positive] := + Zdiv_rest_proof : (q:Z)(r:Z) + `x = q * (two_power_pos p) + r` + -> `0 <= r` + -> `r < (two_power_pos p)` + -> (Zdiv_rest_proofs x p). + +Lemma Zdiv_rest_correct : + (x:Z)(p:positive)(Zdiv_rest_proofs x p). +Intros x p. +Generalize (Zdiv_rest_correct1 x p); Generalize (Zdiv_rest_correct2 x p). +Elim (iter_pos p (Z*Z)*Z Zdiv_rest_aux ((x,`0`),`1`)). +Induction y. +Intros. +Elim H; Intros H1 H2; Clear H. +Rewrite -> H0 in H1; Rewrite -> H0 in H2; +Elim H2; Intros; +Apply Zdiv_rest_proof with q:=y0 r:=y1; Assumption. +Save. + +End power_div_with_rest. + + diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml new file mode 100644 index 000000000..9fb2f918b --- /dev/null +++ b/contrib/omega/coq_omega.ml @@ -0,0 +1,1878 @@ +(**************************************************************************) +(* *) +(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) +(* *) +(* Pierre Crégut (CNET, Lannion, France) *) +(* *) +(**************************************************************************) + +(* $Id$ *) + +open Util +open Pp +open Reduction +open Proof_trees +open Ast +open Names +open Generic +open Term +open Sign +open Inductive +open Tacmach +open Tactics +open Clenv +open Logic +open Omega + +(* 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 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" !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 rec mk_then = + function [t] -> t | (t::l) -> (tclTHEN (t) (mk_then l)) | [] -> tclIDTAC + +let collect_com lbind = + map_succeed (function (Com,c)->c | _ -> failwith "Com") lbind + +(*** EST-CE QUE CES FONCTIONS NE SONT PAS AILLEURS DANS LE CODE ?? *) + +let make_clenv_binding_apply wc (c,t) lbind = + let largs = collect_com lbind in + let lcomargs = List.length largs in + if lcomargs = List.length lbind then + let clause = mk_clenv_from wc (c,t) in + clenv_constrain_missing_args largs clause + else if lcomargs = 0 then + let clause = mk_clenv_rename_from wc (c,t) in + clenv_match_args lbind clause + else + errorlabstrm "make_clenv_bindings" + [<'sTR "Cannot mix bindings and free associations">] + +let resolve_with_bindings_tac (c,lbind) gl = + let (wc,kONT) = startWalk gl in + let t = w_hnf_constr wc (w_type_of wc c) in + let clause = make_clenv_binding_apply wc (c,t) lbind in + res_pf kONT clause gl + +let reduce_to_mind gl t = + let rec elimrec t l = match whd_castapp_stack t [] with + | (DOPN(MutInd (x0,x1),_) as mind,_) -> (mind,prod_it t l) + | (DOPN(Const _,_),_) -> + (try + let t' = pf_nf_betaiota gl (pf_one_step_reduce gl t) in elimrec t' l + with e when catchable_exception e -> + errorlabstrm "tactics__reduce_to_mind" + [< 'sTR"Not an inductive product" >]) + | (DOPN(MutCase _,_),_) -> + (try + let t' = pf_nf_betaiota gl (pf_one_step_reduce gl t) in elimrec t' l + with e when catchable_exception e -> + errorlabstrm "tactics__reduce_to_mind" + [< 'sTR"Not an inductive product" >]) + | (DOP2(Cast,c,_),[]) -> elimrec c l + | (DOP2(Prod,ty,DLAM(n,t')),[]) -> elimrec t' ((n,ty)::l) + | _ -> error "Not an inductive product" + in + elimrec t [] + +let constructor_tac nconstropt i lbind gl = + let cl = pf_concl gl in + let (mind, redcl) = reduce_to_mind gl cl in + let ((x0,x1),args) as mindspec= destMutInd mind in + let nconstr = Global.mind_nconstr mindspec + and sigma = project gl in + (match nconstropt with + | Some expnconstr -> + if expnconstr <> nconstr then + error "Not the expected number of constructors" + | _ -> ()); + if i > nconstr then error "Not enough Constructors"; + let c = DOPN(MutConstruct((x0,x1),i),args) in + let resolve_tac = resolve_with_bindings_tac (c,lbind) in + (tclTHEN (tclTHEN (change_in_concl redcl) intros) resolve_tac) gl + +let exists_tac c= constructor_tac (Some 1) 1 [Com,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 [[], s] + +(*** fin de EST-CE QUE CES FONCTIONS NE SONT PAS AILLEURS DANS LE CODE ?? *) +(****************************************************************) + +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) + +let get_applist = + let rec loop accu = function + | DOPN(AppL,cl) -> + begin match Array.to_list cl with + | h :: l -> loop (l @ accu) h + | [] -> failwith "get_applist" end + | DOP2(Cast,c,t) -> loop accu c + | t -> t,accu + in + loop [] + +exception Destruct + +let dest_const_apply t = + let f,args = get_applist t in + match f with + | DOPN((Const _ | MutConstruct _ | MutInd _) as s,_) -> + Global.id_of_global s,args + | _ -> raise Destruct + +type result = + | Kvar of string + | Kapp of string * constr list + | Kimp of constr * constr + | Kufo + +let destructurate t = + match get_applist t with + | DOPN ((Const _ | MutConstruct _ | MutInd _) as c,_),args -> + Kapp (string_of_id (Global.id_of_global c),args) + | VAR id,[] -> Kvar(string_of_id id) + | DOP2(Prod,typ,DLAM(Anonymous,body)),[] -> Kimp(typ,body) + | DOP2(Prod,_,DLAM(Name _,_)),[] -> + error "Omega: Not a quantifier-free goal" + | _ -> Kufo + +let recognize_number t = + let rec loop t = + let f,l = dest_const_apply t in + match string_of_id f,l with + | "xI",[t] -> 1 + 2 * loop t + | "xO",[t] -> 2 * loop t + | "xH",[] -> 1 + | _ -> failwith "not a number" + in + let f,l = dest_const_apply t in + match string_of_id f,l with + | "POS",[t] -> loop t | "NEG",[t] -> - (loop t) | "ZERO",[] -> 0 + | _ -> failwith "not a number" + +(* 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 *) + +let constant sp id = + Declare.global_sp_reference (path_of_string sp) (id_of_string id) + +(* fast_integer *) +let coq_xH = lazy (constant "#fast_integer#positive.cci" "xH") +let coq_xO = lazy (constant "#fast_integer#positive.cci" "xO") +let coq_xI = lazy (constant "#fast_integer#positive.cci" "xI") +let coq_ZERO = lazy (constant "#fast_integer#Z.cci" "ZERO") +let coq_POS = lazy (constant "#fast_integer#Z.cci" "POS") +let coq_NEG = lazy (constant "#fast_integer#Z.cci" "NEG") +let coq_Z = lazy (constant "#fast_integer#Z.cci" "Z") +let coq_relation = lazy (constant "#fast_integer#relation.cci" "relation") +let coq_SUPERIEUR = lazy (constant "#fast_integer#relation.cci" "SUPERIEUR") +let coq_INFEEIEUR = lazy (constant "#fast_integer#relation.cci" "INFERIEUR") +let coq_EGAL = lazy (constant "#fast_integer#relation.cci" "EGAL") +let coq_Zplus = lazy (constant "#fast_integer#Zplus.cci" "Zplus") +let coq_Zmult = lazy (constant "#fast_integer#Zmult.cci" "Zmult") +let coq_Zopp = lazy (constant "#fast_integer#Zopp.cci" "Zopp") + +(* zarith_aux *) +let coq_Zminus = lazy (constant "#zarith_aux#Zminus.cci" "Zminus") +let coq_Zs = lazy (constant "#zarith_aux#Zs.cci" "Zs") +let coq_Zgt = lazy (constant "#zarith_aux#Zgt.cci" "Zgt") +let coq_Zle = lazy (constant "#zarith_aux#Zle.cci" "Zle") +let coq_inject_nat = lazy (constant "#zarith_aux#inject_nat.cci" "inject_nat") + +(* auxiliary *) +let coq_inj_plus = lazy (constant "#auxiliary#inj_plus.cci" "inj_plus") +let coq_inj_mult = lazy (constant "#auxiliary#inj_mult.cci" "inj_mult") +let coq_inj_minus1 = lazy (constant "#auxiliary#inj_minus1.cci" "inj_minus1") +let coq_inj_minus2 = lazy (constant "#auxiliary#inj_minus2.cci" "inj_minus2") +let coq_inj_S = lazy (constant "#auxiliary#inj_S.cci" "inj_S") +let coq_inj_le = lazy (constant "#auxiliary#inj_le.cci" "inj_le") +let coq_inj_lt = lazy (constant "#auxiliary#inj_lt.cci" "inj_lt") +let coq_inj_ge = lazy (constant "#auxiliary#inj_ge.cci" "inj_ge") +let coq_inj_gt = lazy (constant "#auxiliary#inj_gt.cci" "inj_gt") +let coq_inj_neq = lazy (constant "#auxiliary#inj_neq.cci" "inj_neq") +let coq_inj_eq = lazy (constant "#auxiliary#inj_eq.cci" "inj_eq") +let coq_pred_of_minus = + lazy (constant "#auxiliary#pred_of_minus.cci" "pred_of_minus") +let coq_fast_Zplus_assoc_r = + lazy (constant "#auxiliary#fast_Zplus_assoc_r.cci" "fast_Zplus_assoc_r") +let coq_fast_Zplus_assoc_l = + lazy (constant "#auxiliary#fast_Zplus_assoc_l.cci" "fast_Zplus_assoc_l") +let coq_fast_Zmult_assoc_r = + lazy (constant "#auxiliary#fast_Zmult_assoc_r.cci" "fast_Zmult_assoc_r") +let coq_fast_Zplus_permute = + lazy (constant "#auxiliary#fast_Zplus_permute.cci" "fast_Zplus_permute") +let coq_fast_Zplus_sym = + lazy (constant "#auxiliary#fast_Zplus_sym.cci" "fast_Zplus_sym") +let coq_fast_Zmult_sym = + lazy (constant "#auxiliary#fast_Zmult_sym.cci" "fast_Zmult_sym") +let coq_Zmult_le_approx = + lazy (constant "#auxiliary#Zmult_le_approx.cci" "Zmult_le_approx") +let coq_OMEGA1 = lazy (constant "#auxiliary#OMEGA1.cci" "OMEGA1") +let coq_OMEGA2 = lazy (constant "#auxiliary#OMEGA2.cci" "OMEGA2") +let coq_OMEGA3 = lazy (constant "#auxiliary#OMEGA3.cci" "OMEGA3") +let coq_OMEGA4 = lazy (constant "#auxiliary#OMEGA4.cci" "OMEGA4") +let coq_OMEGA5 = lazy (constant "#auxiliary#OMEGA5.cci" "OMEGA5") +let coq_OMEGA6 = lazy (constant "#auxiliary#OMEGA6.cci" "OMEGA6") +let coq_OMEGA7 = lazy (constant "#auxiliary#OMEGA7.cci" "OMEGA7") +let coq_OMEGA8 = lazy (constant "#auxiliary#OMEGA8.cci" "OMEGA8") +let coq_OMEGA9 = lazy (constant "#auxiliary#OMEGA9.cci" "OMEGA9") +let coq_fast_OMEGA10 = + lazy (constant "#auxiliary#fast_OMEGA10.cci" "fast_OMEGA10") +let coq_fast_OMEGA11 = + lazy (constant "#auxiliary#fast_OMEGA11.cci" "fast_OMEGA11") +let coq_fast_OMEGA12 = + lazy (constant "#auxiliary#fast_OMEGA12.cci" "fast_OMEGA12") +let coq_fast_OMEGA13 = + lazy (constant "#auxiliary#fast_OMEGA13.cci" "fast_OMEGA13") +let coq_fast_OMEGA14 = + lazy (constant "#auxiliary#fast_OMEGA14.cci" "fast_OMEGA14") +let coq_fast_OMEGA15 = + lazy (constant "#auxiliary#fast_OMEGA15.cci" "fast_OMEGA15") +let coq_fast_OMEGA16 = + lazy (constant "#auxiliary#fast_OMEGA16.cci" "fast_OMEGA16") +let coq_OMEGA17 = lazy (constant "#auxiliary#OMEGA17.cci" "OMEGA17") +let coq_OMEGA18 = lazy (constant "#auxiliary#OMEGA18.cci" "OMEGA18") +let coq_OMEGA19 = lazy (constant "#auxiliary#OMEGA19.cci" "OMEGA19") +let coq_OMEGA20 = lazy (constant "#auxiliary#OMEGA20.cci" "OMEGA20") +let coq_fast_Zred_factor0 = + lazy (constant "#auxiliary#fast_Zred_factor0.cci" "fast_Zred_factor0") +let coq_fast_Zred_factor1 = + lazy (constant "#auxiliary#fast_Zred_factor1.cci" "fast_Zred_factor1") +let coq_fast_Zred_factor2 = + lazy (constant "#auxiliary#fast_Zred_factor2.cci" "fast_Zred_factor2") +let coq_fast_Zred_factor3 = + lazy (constant "#auxiliary#fast_Zred_factor3.cci" "fast_Zred_factor3") +let coq_fast_Zred_factor4 = + lazy (constant "#auxiliary#fast_Zred_factor4.cci" "fast_Zred_factor4") +let coq_fast_Zred_factor5 = + lazy (constant "#auxiliary#fast_Zred_factor5.cci" "fast_Zred_factor5") +let coq_fast_Zred_factor6 = + lazy (constant "#auxiliary#fast_Zred_factor6.cci" "fast_Zred_factor6") +let coq_fast_Zmult_plus_distr = + lazy + (constant "#auxiliary#fast_Zmult_plus_distr.cci" "fast_Zmult_plus_distr") +let coq_fast_Zmult_Zopp_left = + lazy (constant "#auxiliary#fast_Zmult_Zopp_left.cci" "fast_Zmult_Zopp_left") +let coq_fast_Zopp_Zplus = + lazy (constant "#auxiliary#fast_Zopp_Zplus.cci" "fast_Zopp_Zplus") +let coq_fast_Zopp_Zmult_r = + lazy (constant "#auxiliary#fast_Zopp_Zmult_r.cci" "fast_Zopp_Zmult_r") +let coq_fast_Zopp_one = + lazy (constant "#auxiliary#fast_Zopp_one.cci" "fast_Zopp_one") +let coq_fast_Zopp_Zopp = + lazy (constant "#auxiliary#fast_Zopp_Zopp.cci" "fast_Zopp_Zopp") +let coq_Zegal_left = lazy (constant "#auxiliary#Zegal_left.cci" "Zegal_left") +let coq_Zne_left = lazy (constant "#auxiliary#Zne_left.cci" "Zne_left") +let coq_Zlt_left = lazy (constant "#auxiliary#Zlt_left.cci" "Zlt_left") +let coq_Zge_left = lazy (constant "#auxiliary#Zge_left.cci" "Zge_left") +let coq_Zgt_left = lazy (constant "#auxiliary#Zgt_left.cci" "Zgt_left") +let coq_Zle_left = lazy (constant "#auxiliary#Zle_left.cci" "Zle_left") +let coq_eq_ind_r = lazy (constant "#auxiliary#eq_ind_r.cci" "eq_ind_r") +let coq_new_var = lazy (constant "#auxiliary#new_var.cci" "new_var") +let coq_intro_Z = lazy (constant "#auxiliary#intro_Z.cci" "intro_Z") +let coq_dec_or = lazy (constant "#auxiliary#dec_or.cci" "dec_or") +let coq_dec_and = lazy (constant "#auxiliary#dec_and.cci" "dec_and") +let coq_dec_imp = lazy (constant "#auxiliary#dec_imp.cci" "dec_imp") +let coq_dec_not = lazy (constant "#auxiliary#dec_not.cci" "dec_not") +let coq_dec_eq_nat = lazy (constant "#auxiliary#dec_eq_nat.cci" "dec_eq_nat") +let coq_dec_eq = lazy (constant "#auxiliary#dec_eq.cci" "dec_eq") +let coq_dec_Zne = lazy (constant "#auxiliary#dec_Zne.cci" "dec_Zne") +let coq_dec_Zle = lazy (constant "#auxiliary#dec_Zle.cci" "dec_Zle") +let coq_dec_Zlt = lazy (constant "#auxiliary#dec_Zlt.cci" "dec_Zlt") +let coq_dec_Zgt = lazy (constant "#auxiliary#dec_Zgt.cci" "dec_Zgt") +let coq_dec_Zge = lazy (constant "#auxiliary#dec_Zge.cci" "dec_Zge") +let coq_dec_le = lazy (constant "#auxiliary#dec_le.cci" "dec_le") +let coq_dec_lt = lazy (constant "#auxiliary#dec_lt.cci" "dec_lt") +let coq_dec_ge = lazy (constant "#auxiliary#dec_ge.cci" "dec_ge") +let coq_dec_gt = lazy (constant "#auxiliary#dec_gt.cci" "dec_gt") +let coq_dec_False = lazy (constant "#auxiliary#dec_False.cci" "dec_False") +let coq_dec_not_not = + lazy (constant "#auxiliary#dec_not_not.cci" "dec_not_not") +let coq_dec_True = lazy (constant "#auxiliary#dec_True.cci" "dec_True") +let coq_not_Zeq = lazy (constant "#auxiliary#not_Zeq.cci" "not_Zeq") +let coq_not_Zle = lazy (constant "#auxiliary#not_Zle.cci" "not_Zle") +let coq_not_Zlt = lazy (constant "#auxiliary#not_Zlt.cci" "not_Zlt") +let coq_not_Zge = lazy (constant "#auxiliary#not_Zge.cci" "not_Zge") +let coq_not_Zgt = lazy (constant "#auxiliary#not_Zgt.cci" "not_Zgt") +let coq_not_le = lazy (constant "#auxiliary#not_le.cci" "not_le") +let coq_not_lt = lazy (constant "#auxiliary#not_lt.cci" "not_lt") +let coq_not_ge = lazy (constant "#auxiliary#not_ge.cci" "not_ge") +let coq_not_gt = lazy (constant "#auxiliary#not_gt.cci" "not_gt") +let coq_not_eq = lazy (constant "#auxiliary#not_eq.cci" "not_eq") +let coq_not_or = lazy (constant "#auxiliary#not_or.cci" "not_or") +let coq_not_and = lazy (constant "#auxiliary#not_and.cci" "not_and") +let coq_not_imp = lazy (constant "#auxiliary#not_imp.cci" "not_imp") +let coq_not_not = lazy (constant "#auxiliary#not_not.cci" "not_not") +let coq_imp_simp = lazy (constant "#auxiliary#imp_simp.cci" "imp_simp") +let coq_neq = lazy (constant "#auxiliary#neq.cci" "neq") +let coq_Zne = lazy (constant "#auxiliary#Zne.cci" "Zne") + +(* Compare_dec *) +let coq_le_gt_dec = lazy (constant "#Compare_dec#le_gt_dec.cci" "le_gt_dec") + +(* Peano *) +let coq_le = lazy (constant "#Peano#le.cci" "le") +let coq_gt = lazy (constant "#Peano#gt.cci" "gt") + +(* Datatypes *) +let coq_nat = lazy (constant "#Datatypes#nat.cci" "nat") +let coq_S = lazy (constant "#Datatypes#nat.cci" "S") +let coq_O = lazy (constant "#Datatypes#nat.cci" "O") + +(* Minus *) +let coq_minus = lazy (constant "#Minus#minus.cci" "minus") + +(* Logic *) +let coq_eq = lazy (constant "#Logic#eq.cci" "eq") +let coq_and = lazy (constant "#Logic#and.cci" "and") +let coq_not = lazy (constant "#Logic#not.cci" "not") +let coq_or = lazy (constant "#Logic#or.cci" "or") +let coq_ex = lazy (constant "#Logic#ex.cci" "ex") + +(* Section paths for unfold *) +let sp_Zs = path_of_string "#zarith_aux#Zs.cci" +let sp_Zminus = path_of_string "#zarith_aux#Zminus.cci" +let sp_Zle = path_of_string "#zarith_aux#Zle.cci" +let sp_Zgt = path_of_string "#zarith_aux#Zgt.cci" +let sp_Zge = path_of_string "#zarith_aux#Zge.cci" +let sp_Zlt = path_of_string "#zarith_aux#Zlt.cci" +let sp_not = path_of_string "#Logic#not.cci" + +let mk_var v = VAR(id_of_string v) +let mk_plus t1 t2 = mkAppL [| Lazy.force coq_Zplus; t1; t2 |] +let mk_times t1 t2 = mkAppL [| Lazy.force coq_Zmult; t1; t2 |] +let mk_minus t1 t2 = mkAppL [| Lazy.force coq_Zminus ; t1;t2 |] +let mk_eq t1 t2 = mkAppL [| Lazy.force coq_eq; Lazy.force coq_Z; t1; t2 |] +let mk_le t1 t2 = mkAppL [| Lazy.force coq_Zle; t1; t2 |] +let mk_gt t1 t2 = mkAppL [| Lazy.force coq_Zgt; t1; t2 |] +let mk_inv t = mkAppL [| Lazy.force coq_Zopp; t |] +let mk_and t1 t2 = mkAppL [| Lazy.force coq_and; t1; t2 |] +let mk_or t1 t2 = mkAppL [| Lazy.force coq_or; t1; t2 |] +let mk_not t = mkAppL [| Lazy.force coq_not; t |] +let mk_eq_rel t1 t2 = mkAppL [| Lazy.force coq_eq; + Lazy.force coq_relation; t1; t2 |] +let mk_inj t = mkAppL [| Lazy.force coq_inject_nat; t |] + +let mk_integer n = + let rec loop n = + if n=1 then Lazy.force coq_xH else + mkAppL [| 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 mkAppL [| if n > 0 then Lazy.force coq_POS else Lazy.force coq_NEG; + loop (abs n) |] + +type constr_path = + | P_APP of int + (* Abstraction and product *) + | P_BODY + | P_TYPE + (* Mutcase *) + | P_BRANCH of int + | P_ARITY + | P_ARG + +let context operation path (t:constr) = + let rec loop i p0 p1 = + match (p0,p1) with + | (p, (DOP2(Cast,c,t))) -> DOP2(Cast,loop i p c,t) + | ([], t) -> operation i t + | (p, (DLAM(n,t))) -> DLAM(n,loop (i+1) p t) + | ((P_APP n :: p), (DOPN(AppL,v) as t)) -> + let f,l = get_applist t in + let v' = Array.of_list (f::l) in + v'.(n) <- loop i p v'.(n); (DOPN(AppL,v')) + | ((P_BRANCH n :: p), (DOPN(MutCase _,_) as t)) -> + let (_,_,_,v) = destCase t in + v.(n) <- loop i p v.(n); (DOPN(AppL,v)) + | ((P_ARITY :: p), (DOPN(AppL,v))) -> + let v' = Array.copy v in + v'.(0) <- loop i p v.(0); (DOPN(AppL,v')) + | ((P_ARG :: p), (DOPN(AppL,v))) -> + let v' = Array.copy v in + v'.(1) <- loop i p v.(1); (DOPN(AppL,v')) + | (p, (DOPN(Fix(_,n) as f,v))) -> + let v' = Array.copy v in + let l = Array.length v - 1 in + v'.(l) <- loop i (P_BRANCH n :: p) v.(l); (DOPN(f,v')) + | ((P_BRANCH n :: p), (DLAMV(name,v))) -> + let v' = Array.copy v in + v'.(n) <- loop (i+1) p v.(n); DLAMV(name,v') + | ((P_BODY :: p), (DOP2((Prod | Lambda) as k, t,c))) -> + (DOP2(k,t,loop i p c)) + | ((P_TYPE :: p), (DOP2((Prod | Lambda) as k, term,c))) -> + (DOP2(k,loop i p term, c)) + | (p, t) -> + 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 p1 = match (p0,p1) with + | (p, (DOP2(Cast,c,t))) -> loop p c + | ([], t) -> t + | (p, (DLAM(n,t))) -> loop p t + | ((P_APP n :: p), (DOPN(AppL,v) as t)) -> + let f,l = get_applist t in loop p v.(n) + | ((P_BRANCH n :: p), (DOPN(MutCase _,_) as t)) -> + let (_,_,_,v) = destCase t in loop p v.(n) + | ((P_ARITY :: p), (DOPN(AppL,v))) -> loop p v.(0) + | ((P_ARG :: p), (DOPN(AppL,v))) -> loop p v.(1) + | (p, (DOPN(Fix(_,n) as f,v))) -> + let l = Array.length v - 1 in loop (P_BRANCH n :: p) v.(l) + | ((P_BRANCH n :: p), (DLAMV(name,v))) -> loop p v.(n) + | ((P_BODY :: p), (DOP2((Prod | Lambda) as k, t,c))) -> loop p c + | ((P_TYPE :: p), (DOP2((Prod | Lambda) as k, term,c))) -> loop p term + | (p, t) -> + 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 (Rel 0) in + let abstract = context (fun i t -> term_occur:= t; Rel 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 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 string + | 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 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 -> (VAR (id_of_string c)) + | Oz c -> mk_integer c + | Oinv c -> mkAppL [| Lazy.force coq_Zopp; val_of c |] + | Otimes (t1,t2) -> mkAppL [| Lazy.force coq_Zmult; val_of t1; val_of t2 |] + | Oplus(t1,t2) -> mkAppL [| 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 (Environ.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 (Rel 1,[result])) + (mkAppL [| Lazy.force coq_eq_ind_r; + typ; result; Rel 2; Rel 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 (mkAppL [| Lazy.force coq_Zmult; mk_integer n |]) + +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 (mkAppL [| Lazy.force coq_Zopp; c |]) + +let rec transform p t = + let default () = + try + let v,th,_ = find_constr t in + [clever_rewrite_base p (VAR v) (VAR th)], Oatom (string_of_id v) + with _ -> + let v = new_identifier_var () + and th = new_identifier () in + hide_constr t v th false; + [clever_rewrite_base p (VAR v) (VAR th)], Oatom (string_of_id v) + in + try match destructurate 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 (mkAppL [| Lazy.force coq_Zplus; t1; + (mkAppL [| Lazy.force coq_Zopp; t2 |]) |]) in + unfold sp_Zminus :: tac,t + | Kapp("Zs",[t1]) -> + let tac,t = transform p (mkAppL [| 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 (VAR v) (VAR th)],Oatom(string_of_id v) + with _ -> + let v = new_identifier_var () and th = new_identifier () in + hide_constr t' v th true; + [clever_rewrite_base p (VAR v) (VAR th)], Oatom (string_of_id 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 + tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (generalize_tac + [mkAppL [| Lazy.force coq_OMEGA17; + val_of eq1; + val_of eq2; + mk_integer k; + VAR id1; VAR 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 = mkAppL [| Lazy.force coq_eq; + Lazy.force coq_relation; + Lazy.force coq_SUPERIEUR; + Lazy.force coq_SUPERIEUR |] + in + tclTHENS + (tclTHEN + (tclTHEN + (tclTHEN + (unfold sp_Zle) + (simpl_in_concl)) + intro) + (absurd not_sup_sup)) + [ assumption ; reflexivity ] + in + let theorem = + mkAppL [| Lazy.force coq_OMEGA2; + val_of eq1; val_of eq2; + VAR (hyp_of_tag e1.id); + VAR (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 + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (intros_using [aux]) + (generalize_tac + [mkAppL [| + Lazy.force coq_OMEGA1; + eq1; rhs; VAR aux; VAR id |]])) + (clear [aux;id])) + (intros_using [id])) + (cut (mk_gt kk dd))) + [ tclTHENS + (cut (mk_gt kk zero)) + [ tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (intros_using [aux1; aux2]) + (generalize_tac + [mkAppL [| + Lazy.force coq_Zmult_le_approx; + kk;eq2;dd;VAR aux1;VAR aux2; + VAR id |]])) + (clear [aux1;aux2;id])) + (intros_using [id])) + (loop l); + tclTHEN + (tclTHEN + (unfold sp_Zgt) + (simpl_in_concl)) + reflexivity ]; + tclTHEN + (tclTHEN (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)) + [tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (intros_using [aux2;aux1]) + (generalize_tac + [mkAppL [| Lazy.force coq_OMEGA4; + dd;kk;eq2;VAR aux1; + VAR aux2 |]])) + (clear [aux1;aux2])) + (unfold sp_not)) + (intros_using [aux])) + (resolve_id aux)) + (mk_then tac)) + assumption; + tclTHEN + (tclTHEN + (unfold sp_Zgt) + simpl_in_concl) + reflexivity ]; + tclTHEN + (tclTHEN + (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 1] e2.body in + tclTHENS + (cut state_eq) + [tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (intros_using [aux1]) + (generalize_tac + [mkAppL [| + Lazy.force coq_OMEGA18; + eq1;eq2;kk;VAR aux1; VAR 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)) + [tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (intros_using [aux2;aux1]) + (generalize_tac + [mkAppL [| Lazy.force coq_OMEGA3; + eq1; eq2; kk; VAR aux2; + VAR aux1;VAR id|]])) + (clear [aux1;aux2;id])) + (intros_using [id])) + (loop l); + tclTHEN + (tclTHEN (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))) + [tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (intros_using [aux]) + (generalize_tac [mkAppL [| + Lazy.force coq_OMEGA8; + eq1;eq2;VAR id1;VAR id2; + VAR 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 v = unintern_id sigma in + let vid = id_of_string v in + let theorem = + mkAppL [| Lazy.force coq_ex; + Lazy.force coq_Z; + mkLambda (Name(id_of_string v)) (Lazy.force coq_Z) + (mk_eq (Rel 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 (VAR 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) + [tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (intros_using [aux]) + (elim_id aux)) + (clear [aux])) + (intros_using [vid; aux])) + (generalize_tac + [mkAppL [| Lazy.force coq_OMEGA9; + VAR vid;eq2;eq1;mm; + VAR id2;VAR 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; VAR id]))) + [tclTHEN (tclTHEN (mk_then tac1) (intros_using [id1])) + (loop act1); + tclTHEN (tclTHEN (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 + tclTHEN + (tclTHEN + (tclTHEN + (generalize_tac [mkAppL [| tac_thm; eq1; eq2; + kk; VAR id1; VAR 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)) + [tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (intros_using [aux2;aux1]) + (generalize_tac + [mkAppL [| Lazy.force coq_OMEGA7; + eq1;eq2;kk1;kk2; + VAR aux1;VAR aux2; + VAR id1;VAR id2 |] ])) + (clear [aux1;aux2])) + (mk_then tac)) + (intros_using [id])) + (loop l); + tclTHEN + (tclTHEN (unfold sp_Zgt) simpl_in_concl) + reflexivity ]; + tclTHEN + (tclTHEN (unfold sp_Zgt) simpl_in_concl) + reflexivity ] + | CONSTANT_NOT_NUL(e,k) :: l -> + tclTHEN (generalize_tac [VAR (hyp_of_tag e)]) Equality.discrConcl + | CONSTANT_NUL(e) :: l -> + tclTHEN (resolve_id (hyp_of_tag e)) reflexivity + | CONSTANT_NEG(e,k) :: l -> + tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (generalize_tac [VAR (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 [mkAppL [| theorem; t1; t2; VAR id |] ]) + (clear [id]) + in + if tac <> [] then + ((id,((tclTHEN ((tclTHEN (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 c with + | Kapp("eq",[typ;t1;t2]) + when destructurate (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 coq_omega gl = + clear_tables (); + let tactic_normalisation, system = + it_sign (destructure_omega gl) ([],[]) (pf_untyped_hyps 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; + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (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 (string_of_id v); c=1}]; + constant = 0; id = i} :: sys + else + (tclTHEN + (tclTHEN + (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 hyps = pf_untyped_hyps gl in + let rec explore p t = + try match destructurate t with + | Kapp("plus",[t1;t2]) -> + (tclTHEN + ((tclTHEN + (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]) -> + (tclTHEN + (tclTHEN + (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])) + [ + (tclTHEN + (tclTHEN + (tclTHEN + (clever_rewrite_gen p + (mk_minus (mk_inj t1) (mk_inj t2)) + ((Lazy.force coq_inj_minus1),[t1;t2;VAR id])) + (loop [id] [mkAppL [| 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;VAR id])) + (loop [id] [mkAppL [| Lazy.force coq_gt; t2;t1 |]])) + ] + | Kapp("S",[t']) -> + let rec is_number t = + try match destructurate 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 t with + Kapp("S",[t]) -> + (tclTHEN + (clever_rewrite_gen p + (mkAppL [| 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 = + mkAppL [| Lazy.force coq_minus ; t; + mkAppL [| 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 p0 p1 = + match (p0,p1) with + | ([], []) -> tclIDTAC + | ((i::li),(t::lt)) -> + begin try match destructurate t with + Kapp("le",[t1;t2]) -> + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (generalize_tac + [mkAppL [| Lazy.force coq_inj_le; + t1;t2;VAR i |] ]) + (explore [P_APP 1; P_TYPE] t1)) + (explore [P_APP 2; P_TYPE] t2)) + (clear [i])) + (intros_using [i])) + (loop li lt)) + | Kapp("lt",[t1;t2]) -> + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (generalize_tac + [mkAppL [| Lazy.force coq_inj_lt; + t1;t2;VAR i |] ]) + (explore [P_APP 1; P_TYPE] t1)) + (explore [P_APP 2; P_TYPE] t2)) + (clear [i])) + (intros_using [i])) + (loop li lt)) + | Kapp("ge",[t1;t2]) -> + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (generalize_tac + [mkAppL [| Lazy.force coq_inj_ge; + t1;t2;VAR i |] ]) + (explore [P_APP 1; P_TYPE] t1)) + (explore [P_APP 2; P_TYPE] t2)) + (clear [i])) + (intros_using [i])) + (loop li lt)) + | Kapp("gt",[t1;t2]) -> + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (generalize_tac + [mkAppL [| Lazy.force coq_inj_gt; + t1;t2;VAR i |] ]) + (explore [P_APP 1; P_TYPE] t1)) + (explore [P_APP 2; P_TYPE] t2)) + (clear [i])) + (intros_using [i])) + (loop li lt)) + | Kapp("neq",[t1;t2]) -> + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (generalize_tac + [mkAppL [| Lazy.force coq_inj_neq; + t1;t2;VAR i |] ]) + (explore [P_APP 1; P_TYPE] t1)) + (explore [P_APP 2; P_TYPE] t2)) + (clear [i])) + (intros_using [i])) + (loop li lt)) + | Kapp("eq",[typ;t1;t2]) -> + if pf_conv_x gl typ (Lazy.force coq_nat) then + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (tclTHEN + (generalize_tac + [mkAppL [| Lazy.force coq_inj_eq; + t1;t2;VAR i |] ]) + (explore [P_APP 2; P_TYPE] t1)) + (explore [P_APP 3; P_TYPE] t2)) + (clear [i])) + (intros_using [i])) + (loop li lt)) + else loop li lt + | _ -> loop li lt + with e when catchable_exception e -> loop li lt end + | (_, _) -> failwith "nat_inject" + in + loop (List.rev (ids_of_sign hyps)) (List.rev (vals_of_sign hyps)) gl + +let rec decidability gl t = + match destructurate t with + | Kapp("or",[t1;t2]) -> + mkAppL [| Lazy.force coq_dec_or; t1; t2; + decidability gl t1; decidability gl t2 |] + | Kapp("and",[t1;t2]) -> + mkAppL [| Lazy.force coq_dec_and; t1; t2; + decidability gl t1; decidability gl t2 |] + | Kimp(t1,t2) -> + mkAppL [| Lazy.force coq_dec_imp; t1; t2; + decidability gl t1; decidability gl t2 |] + | Kapp("not",[t1]) -> mkAppL [| Lazy.force coq_dec_not; t1; + decidability gl t1 |] + | Kapp("eq",[typ;t1;t2]) -> + begin match destructurate (pf_nf gl typ) with + | Kapp("Z",[]) -> mkAppL [| Lazy.force coq_dec_eq; t1;t2 |] + | Kapp("nat",[]) -> mkAppL [| 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]) -> mkAppL [| Lazy.force coq_dec_Zne; t1;t2 |] + | Kapp("Zle",[t1;t2]) -> mkAppL [| Lazy.force coq_dec_Zle; t1;t2 |] + | Kapp("Zlt",[t1;t2]) -> mkAppL [| Lazy.force coq_dec_Zlt; t1;t2 |] + | Kapp("Zge",[t1;t2]) -> mkAppL [| Lazy.force coq_dec_Zge; t1;t2 |] + | Kapp("Zgt",[t1;t2]) -> mkAppL [| Lazy.force coq_dec_Zgt; t1;t2 |] + | Kapp("le", [t1;t2]) -> mkAppL [| Lazy.force coq_dec_le; t1;t2 |] + | Kapp("lt", [t1;t2]) -> mkAppL [| Lazy.force coq_dec_lt; t1;t2 |] + | Kapp("ge", [t1;t2]) -> mkAppL [| Lazy.force coq_dec_ge; t1;t2 |] + | Kapp("gt", [t1;t2]) -> mkAppL [| Lazy.force coq_dec_gt; t1;t2 |] + | Kapp("False",[]) -> Lazy.force coq_dec_False + | Kapp("True",[]) -> Lazy.force coq_dec_True + | Kapp(t,_::_) -> error ("Omega: Unrecognized predicate or connective: " + ^ t) + | Kapp(t,[]) -> error ("Omega: Unrecognized atomic proposition: "^ t) + | Kvar _ -> error "Omega: Can't solve a goal with proposition variables" + | _ -> error "Omega: Unrecognized proposition" + +let destructure_hyps gl = + let hyp = pf_untyped_hyps gl in + let rec loop evbd p0 p1 = match (p0,p1) with + | ([], []) -> (tclTHEN nat_inject coq_omega) + | ((i::li), (t::lt)) -> + begin try match destructurate t with + | Kapp(("Zle"|"Zge"|"Zgt"|"Zlt"|"Zne"),[t1;t2]) -> loop evbd li lt + | Kapp("or",[t1;t2]) -> + (tclTHENS ((tclTHEN ((tclTHEN (elim_id i) (clear [i]))) + (intros_using [i]))) + ([ loop evbd (i::li) (t1::lt); loop evbd (i::li) (t2::lt) ])) + | Kapp("and",[t1;t2]) -> + let i1 = id_of_string (string_of_id i ^ "_left") in + let i2 = id_of_string (string_of_id i ^ "_right") in + (tclTHEN + (tclTHEN + (tclTHEN (elim_id i) (clear [i])) + (intros_using [i1;i2])) + (loop (i1::i2::evbd) (i1::i2::li) (t1::t2::lt))) + | Kimp(t1,t2) -> + if isprop (pf_type_of gl t1) & closed0 t2 then begin + (tclTHEN + (tclTHEN + (tclTHEN + (generalize_tac [mkAppL [| Lazy.force coq_imp_simp; + t1; t2; + decidability gl t1; + VAR i|]]) + (clear [i])) + (intros_using [i])) + (loop evbd (i::li) (mk_or (mk_not t1) t2 :: lt))) + end else loop evbd li lt + | Kapp("not",[t]) -> + begin match destructurate t with + Kapp("or",[t1;t2]) -> + (tclTHEN + (tclTHEN + (tclTHEN + (generalize_tac [mkAppL [| Lazy.force coq_not_or; + t1; t2; VAR i |]]) + (clear [i])) + (intros_using [i])) + (loop evbd (i::li) + (mk_and (mk_not t1) (mk_not t2) :: lt))) + | Kapp("and",[t1;t2]) -> + (tclTHEN + (tclTHEN + (tclTHEN + (generalize_tac + [mkAppL [| Lazy.force coq_not_and; t1; t2; + decidability gl t1;VAR i|]]) + (clear [i])) + (intros_using [i])) + (loop evbd (i::li) + (mk_or (mk_not t1) (mk_not t2) :: lt))) + | Kimp(t1,t2) -> + (tclTHEN + (tclTHEN + (tclTHEN + (generalize_tac + [mkAppL [| Lazy.force coq_not_imp; t1; t2; + decidability gl t1;VAR i |]]) + (clear [i])) + (intros_using [i])) + (loop evbd (i::li) (mk_and t1 (mk_not t2) :: lt))) + | Kapp("not",[t]) -> + (tclTHEN + (tclTHEN + (tclTHEN + (generalize_tac + [mkAppL [| Lazy.force coq_not_not; t; + decidability gl t; VAR i |]]) + (clear [i])) + (intros_using [i])) + (loop evbd (i::li) (t :: lt))) + | Kapp("Zle", [t1;t2]) -> + (tclTHEN + (tclTHEN + (tclTHEN + (generalize_tac [mkAppL [| Lazy.force coq_not_Zle; + t1;t2;VAR i|]]) + (clear [i])) + (intros_using [i])) + (loop evbd li lt)) + | Kapp("Zge", [t1;t2]) -> + (tclTHEN + (tclTHEN + (tclTHEN + (generalize_tac [mkAppL [| Lazy.force coq_not_Zge; + t1;t2;VAR i|]]) + (clear [i])) + (intros_using [i])) + (loop evbd li lt)) + | Kapp("Zlt", [t1;t2]) -> + (tclTHEN + (tclTHEN + (tclTHEN + (generalize_tac [mkAppL [| Lazy.force coq_not_Zlt; + t1;t2;VAR i|]]) + (clear [i])) + (intros_using [i])) + (loop evbd li lt)) + | Kapp("Zgt", [t1;t2]) -> + (tclTHEN + (tclTHEN + (tclTHEN + (generalize_tac [mkAppL [| Lazy.force coq_not_Zgt; + t1;t2;VAR i|]]) + (clear [i])) + (intros_using [i])) + (loop evbd li lt)) + | Kapp("le", [t1;t2]) -> + (tclTHEN + (tclTHEN + (tclTHEN + (generalize_tac [mkAppL [| Lazy.force coq_not_le; + t1;t2;VAR i|]]) + (clear [i])) + (intros_using [i])) + (loop evbd li lt)) + | Kapp("ge", [t1;t2]) -> + (tclTHEN + (tclTHEN + (tclTHEN + (generalize_tac [mkAppL [| Lazy.force coq_not_ge; + t1;t2;VAR i|]]) + (clear [i])) + (intros_using [i])) + (loop evbd li lt)) + | Kapp("lt", [t1;t2]) -> + (tclTHEN + (tclTHEN + (tclTHEN + (generalize_tac [mkAppL [| Lazy.force coq_not_lt; + t1;t2;VAR i|]]) + (clear [i])) + (intros_using [i])) + (loop evbd li lt)) + | Kapp("gt", [t1;t2]) -> + (tclTHEN + (tclTHEN + (tclTHEN + (generalize_tac [mkAppL [| Lazy.force coq_not_gt; + t1;t2;VAR i|]]) + (clear [i])) + (intros_using [i])) + (loop evbd li lt)) + | Kapp("eq",[typ;t1;t2]) -> + if !old_style_flag then begin + match destructurate (pf_nf gl typ) with + | Kapp("nat",_) -> + (tclTHEN + (tclTHEN + (tclTHEN + (simplest_elim + (applist + (Lazy.force coq_not_eq, + [t1;t2;VAR i]))) + (clear [i])) + (intros_using [i])) + (loop evbd li lt)) + | Kapp("Z",_) -> + (tclTHEN + (tclTHEN + (tclTHEN + (simplest_elim + (applist + (Lazy.force coq_not_Zeq, + [t1;t2;VAR i]))) + (clear [i])) + (intros_using [i])) + (loop evbd li lt)) + | _ -> loop evbd li lt + end else begin + match destructurate (pf_nf gl typ) with + | Kapp("nat",_) -> + (tclTHEN + (convert_hyp i + (mkAppL [| Lazy.force coq_neq; t1;t2|])) + (loop evbd li lt)) + | Kapp("Z",_) -> + (tclTHEN + (convert_hyp i + (mkAppL [| Lazy.force coq_Zne; t1;t2|])) + (loop evbd li lt)) + | _ -> loop evbd li lt + end + | _ -> loop evbd li lt + end + | _ -> loop evbd li lt + with e when catchable_exception e -> loop evbd li lt + end + | (_, _) -> anomaly "destructurate_hyps" + in + loop (ids_of_sign hyp) (ids_of_sign hyp) (vals_of_sign hyp) gl + +let destructure_goal gl = + let concl = pf_concl gl in + let rec loop t = + match destructurate t with + | Kapp("not",[t1;t2]) -> + (tclTHEN + (tclTHEN (unfold sp_not) intro) + destructure_hyps) + | Kimp(a,b) -> (tclTHEN intro (loop b)) + | Kapp("False",[]) -> destructure_hyps + | _ -> + (tclTHEN + (tclTHEN + (Tactics.refine + (mkAppL [| 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 = + let result = destructure_goal gl in + (* if !display_time_flag then begin text_time (); + flush Pervasives.stdout end; *) + result + +let omega = hide_atomic_tactic "Omega" omega_solver + + diff --git a/contrib/omega/omega.ml b/contrib/omega/omega.ml new file mode 100755 index 000000000..c06a4cb8c --- /dev/null +++ b/contrib/omega/omega.ml @@ -0,0 +1,652 @@ +(**************************************************************************) +(* *) +(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) +(* *) +(* Pierre Crégut (CNET, Lannion, France) *) +(* *) +(**************************************************************************) + +(* $Id$ *) + +open Util +open Hashtbl + +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; "WW" ^ string_of_int !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:string) -> + 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 " (unintern_id f.v) + else + Printf.printf "%d %s " c (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 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 ())) |