diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
| commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
| tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /plugins/omega | |
| parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff) | |
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/omega')
| -rw-r--r-- | plugins/omega/OmegaLemmas.v | 38 | ||||
| -rw-r--r-- | plugins/omega/PreOmega.v | 204 | ||||
| -rw-r--r-- | plugins/omega/coq_omega.ml | 622 | ||||
| -rw-r--r-- | plugins/omega/g_omega.ml4 | 10 | ||||
| -rw-r--r-- | plugins/omega/omega.ml | 250 |
5 files changed, 562 insertions, 562 deletions
diff --git a/plugins/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v index fe8fcc924..56a854d6f 100644 --- a/plugins/omega/OmegaLemmas.v +++ b/plugins/omega/OmegaLemmas.v @@ -31,7 +31,7 @@ Qed. Theorem Zred_factor3 : forall n m:Z, n * m + n = n * (1 + m). Proof. intros x y; pattern x at 2 in |- *; rewrite <- (Zmult_1_r x); - rewrite <- Zmult_plus_distr_r; rewrite Zplus_comm; + rewrite <- Zmult_plus_distr_r; rewrite Zplus_comm; trivial with arith. Qed. @@ -53,7 +53,7 @@ Qed. (** Other specific variants of theorems dedicated for the Omega tactic *) Lemma new_var : forall x : Z, exists y : Z, x = y. -intros x; exists x; trivial with arith. +intros x; exists x; trivial with arith. Qed. Lemma OMEGA1 : forall x y : Z, x = y -> 0 <= x -> 0 <= y. @@ -62,7 +62,7 @@ Qed. Lemma OMEGA2 : forall x y : Z, 0 <= x -> 0 <= y -> 0 <= x + y. exact Zplus_le_0_compat. -Qed. +Qed. Lemma OMEGA3 : forall x y k : Z, k > 0 -> x = y * k -> x = 0 -> y = 0. @@ -82,11 +82,11 @@ unfold not in |- *; intros x y z H1 H2 H3; cut (y > 0); [ rewrite H3; unfold Zgt in |- *; simpl in |- *; discriminate | apply Zle_gt_trans with x; [ pattern x at 1 in |- *; rewrite <- (Zplus_0_l x); - apply Zplus_le_compat_r; rewrite Zmult_comm; + apply Zplus_le_compat_r; rewrite Zmult_comm; generalize H4; unfold Zgt in |- *; case y; [ simpl in |- *; intros H7; discriminate H7 | intros p H7; rewrite <- (Zmult_0_r (Zpos p)); - unfold Zle in |- *; rewrite Zcompare_mult_compat; + unfold Zle in |- *; rewrite Zcompare_mult_compat; exact H6 | simpl in |- *; intros p H7; discriminate H7 ] | assumption ] ] @@ -116,7 +116,7 @@ Lemma OMEGA8 : forall x y : Z, 0 <= x -> 0 <= y -> x = - y -> x = 0. intros x y H1 H2 H3; elim (Zle_lt_or_eq 0 x H1); [ intros H4; absurd (0 < x); [ change (0 >= x) in |- *; apply Zle_ge; apply Zplus_le_reg_l with y; - rewrite H3; rewrite Zplus_opp_r; rewrite Zplus_0_r; + rewrite H3; rewrite Zplus_opp_r; rewrite Zplus_0_r; assumption | assumption ] | intros H4; rewrite H4; trivial with arith ]. @@ -143,7 +143,7 @@ Lemma OMEGA11 : (v1 * c1 + l1) * k1 + l2 = v1 * (c1 * k1) + (l1 * k1 + l2). intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r; - repeat rewrite Zmult_assoc; repeat elim Zplus_assoc; + repeat rewrite Zmult_assoc; repeat elim Zplus_assoc; trivial with arith. Qed. @@ -152,7 +152,7 @@ Lemma OMEGA12 : l1 + (v2 * c2 + l2) * k2 = v2 * (c2 * k2) + (l1 + l2 * k2). intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r; - repeat rewrite Zmult_assoc; repeat elim Zplus_assoc; + repeat rewrite Zmult_assoc; repeat elim Zplus_assoc; rewrite Zplus_permute; trivial with arith. Qed. @@ -166,7 +166,7 @@ intros; rewrite Zplus_assoc; rewrite (Zplus_comm (v * Zpos x) l1); rewrite Zplus_opp_r; rewrite Zmult_0_r; rewrite Zplus_0_r; trivial with arith. Qed. - + Lemma OMEGA14 : forall (v l1 l2 : Z) (x : positive), v * Zneg x + l1 + (v * Zpos x + l2) = l1 + l2. @@ -188,14 +188,14 @@ Qed. Lemma OMEGA16 : forall v c l k : Z, (v * c + l) * k = v * (c * k) + l * k. intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r; - repeat rewrite Zmult_assoc; repeat elim Zplus_assoc; + repeat rewrite Zmult_assoc; repeat elim Zplus_assoc; trivial with arith. Qed. Lemma OMEGA17 : forall x y z : Z, Zne x 0 -> y = 0 -> Zne (x + y * z) 0. unfold Zne, not in |- *; intros x y z H1 H2 H3; apply H1; - apply Zplus_reg_l with (y * z); rewrite Zplus_comm; + apply Zplus_reg_l with (y * z); rewrite Zplus_comm; rewrite H3; rewrite H2; auto with arith. Qed. @@ -213,7 +213,7 @@ unfold Zne in |- *; intros x H; elim (Zle_or_lt 0 x); rewrite <- Zsucc_pred; apply Zlt_le_succ; assumption | intros H2; absurd (x = 0); auto with arith ] | intros H1; right; rewrite <- Zopp_eq_mult_neg_1; rewrite Zplus_comm; - apply Zle_left; apply Zsucc_le_reg; simpl in |- *; + apply Zle_left; apply Zsucc_le_reg; simpl in |- *; apply Zlt_le_succ; auto with arith ]. Qed. @@ -229,7 +229,7 @@ Definition fast_Zplus_comm (x y : Z) (P : Z -> Prop) Definition fast_Zplus_assoc_reverse (n m p : Z) (P : Z -> Prop) (H : P (n + (m + p))) := eq_ind_r P H (Zplus_assoc_reverse n m p). -Definition fast_Zplus_assoc (n m p : Z) (P : Z -> Prop) +Definition fast_Zplus_assoc (n m p : Z) (P : Z -> Prop) (H : P (n + m + p)) := eq_ind_r P H (Zplus_assoc n m p). Definition fast_Zplus_permute (n m p : Z) (P : Z -> Prop) @@ -257,7 +257,7 @@ Definition fast_OMEGA13 (v l1 l2 : Z) (x : positive) (P : Z -> Prop) Definition fast_OMEGA14 (v l1 l2 : Z) (x : positive) (P : Z -> Prop) (H : P (l1 + l2)) := eq_ind_r P H (OMEGA14 v l1 l2 x). -Definition fast_Zred_factor0 (x : Z) (P : Z -> Prop) +Definition fast_Zred_factor0 (x : Z) (P : Z -> Prop) (H : P (x * 1)) := eq_ind_r P H (Zred_factor0 x). Definition fast_Zopp_eq_mult_neg_1 (x : Z) (P : Z -> Prop) @@ -272,18 +272,18 @@ Definition fast_Zopp_plus_distr (x y : Z) (P : Z -> Prop) Definition fast_Zopp_involutive (x : Z) (P : Z -> Prop) (H : P x) := eq_ind_r P H (Zopp_involutive x). -Definition fast_Zopp_mult_distr_r (x y : Z) (P : Z -> Prop) +Definition fast_Zopp_mult_distr_r (x y : Z) (P : Z -> Prop) (H : P (x * - y)) := eq_ind_r P H (Zopp_mult_distr_r x y). Definition fast_Zmult_plus_distr_l (n m p : Z) (P : Z -> Prop) (H : P (n * p + m * p)) := eq_ind_r P H (Zmult_plus_distr_l n m p). -Definition fast_Zmult_opp_comm (x y : Z) (P : Z -> Prop) +Definition fast_Zmult_opp_comm (x y : Z) (P : Z -> Prop) (H : P (x * - y)) := eq_ind_r P H (Zmult_opp_comm x y). Definition fast_Zmult_assoc_reverse (n m p : Z) (P : Z -> Prop) (H : P (n * (m * p))) := eq_ind_r P H (Zmult_assoc_reverse n m p). -Definition fast_Zred_factor1 (x : Z) (P : Z -> Prop) +Definition fast_Zred_factor1 (x : Z) (P : Z -> Prop) (H : P (x * 2)) := eq_ind_r P H (Zred_factor1 x). Definition fast_Zred_factor2 (x y : Z) (P : Z -> Prop) @@ -295,8 +295,8 @@ Definition fast_Zred_factor3 (x y : Z) (P : Z -> Prop) Definition fast_Zred_factor4 (x y z : Z) (P : Z -> Prop) (H : P (x * (y + z))) := eq_ind_r P H (Zred_factor4 x y z). -Definition fast_Zred_factor5 (x y : Z) (P : Z -> Prop) +Definition fast_Zred_factor5 (x y : Z) (P : Z -> Prop) (H : P y) := eq_ind_r P H (Zred_factor5 x y). -Definition fast_Zred_factor6 (x : Z) (P : Z -> Prop) +Definition fast_Zred_factor6 (x : Z) (P : Z -> Prop) (H : P (x + 0)) := eq_ind_r P H (Zred_factor6 x). diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 47e22a97f..a5a085a99 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -5,16 +5,16 @@ Open Local Scope Z_scope. (** * zify: the Z-ification tactic *) -(* This tactic searches for nat and N and positive elements in the goal and - translates everything into Z. It is meant as a pre-processor for +(* This tactic searches for nat and N and positive elements in the goal and + translates everything into Z. It is meant as a pre-processor for (r)omega; for instance a positivity hypothesis is added whenever - a multiplication is encountered - an atom is encountered (that is a variable or an unknown construct) Recognized relations (can be handled as deeply as allowed by setoid rewrite): - { eq, le, lt, ge, gt } on { Z, positive, N, nat } - - Recognized operations: + + Recognized operations: - on Z: Zmin, Zmax, Zabs, Zsgn are translated in term of <= < = - on nat: + * - S O pred min max nat_of_P nat_of_N Zabs_nat - on positive: Zneg Zpos xI xO xH + * - Psucc Ppred Pmin Pmax P_of_succ_nat @@ -26,31 +26,31 @@ Open Local Scope Z_scope. (** I) translation of Zmax, Zmin, Zabs, Zsgn into recognized equations *) -Ltac zify_unop_core t thm a := +Ltac zify_unop_core t thm a := (* Let's introduce the specification theorem for t *) - let H:= fresh "H" in assert (H:=thm a); + let H:= fresh "H" in assert (H:=thm a); (* Then we replace (t a) everywhere with a fresh variable *) let z := fresh "z" in set (z:=t a) in *; clearbody z. -Ltac zify_unop_var_or_term t thm a := +Ltac zify_unop_var_or_term t thm a := (* If a is a variable, no need for aliasing *) - let za := fresh "z" in + let za := fresh "z" in (rename a into za; rename za into a; zify_unop_core t thm a) || (* Otherwise, a is a complex term: we alias it. *) (remember a as za; zify_unop_core t thm za). -Ltac zify_unop t thm a := +Ltac zify_unop t thm a := (* if a is a scalar, we can simply reduce the unop *) - let isz := isZcst a in - match isz with + let isz := isZcst a in + match isz with | true => simpl (t a) in * | _ => zify_unop_var_or_term t thm a end. -Ltac zify_unop_nored t thm a := +Ltac zify_unop_nored t thm a := (* in this version, we don't try to reduce the unop (that can be (Zplus x)) *) - let isz := isZcst a in - match isz with + let isz := isZcst a in + match isz with | true => zify_unop_core t thm a | _ => zify_unop_var_or_term t thm a end. @@ -58,20 +58,20 @@ Ltac zify_unop_nored t thm a := Ltac zify_binop t thm a b:= (* works as zify_unop, except that we should be careful when dealing with b, since it can be equal to a *) - let isza := isZcst a in - match isza with + let isza := isZcst a in + match isza with | true => zify_unop (t a) (thm a) b - | _ => - let za := fresh "z" in + | _ => + let za := fresh "z" in (rename a into za; rename za into a; zify_unop_nored (t a) (thm a) b) || - (remember a as za; match goal with + (remember a as za; match goal with | H : za = b |- _ => zify_unop_nored (t za) (thm za) za | _ => zify_unop_nored (t za) (thm za) b end) end. -Ltac zify_op_1 := - match goal with +Ltac zify_op_1 := + match goal with | |- context [ Zmax ?a ?b ] => zify_binop Zmax Zmax_spec a b | H : context [ Zmax ?a ?b ] |- _ => zify_binop Zmax Zmax_spec a b | |- context [ Zmin ?a ?b ] => zify_binop Zmin Zmin_spec a b @@ -93,13 +93,13 @@ Ltac zify_op := repeat zify_op_1. Definition Z_of_nat' := Z_of_nat. -Ltac hide_Z_of_nat t := - let z := fresh "z" in set (z:=Z_of_nat t) in *; - change Z_of_nat with Z_of_nat' in z; +Ltac hide_Z_of_nat t := + let z := fresh "z" in set (z:=Z_of_nat t) in *; + change Z_of_nat with Z_of_nat' in z; unfold z in *; clear z. -Ltac zify_nat_rel := - match goal with +Ltac zify_nat_rel := + match goal with (* I: equalities *) | H : (@eq nat ?a ?b) |- _ => generalize (inj_eq _ _ H); clear H; intro H | |- (@eq nat ?a ?b) => apply (inj_eq_rev a b) @@ -127,8 +127,8 @@ Ltac zify_nat_rel := | |- context [ ge ?a ?b ] => rewrite (inj_ge_iff a b) end. -Ltac zify_nat_op := - match goal with +Ltac zify_nat_op := + match goal with (* misc type conversions: positive/N/Z to nat *) | H : context [ Z_of_nat (nat_of_P ?a) ] |- _ => rewrite <- (Zpos_eq_Z_of_nat_o_nat_of_P a) in H | |- context [ Z_of_nat (nat_of_P ?a) ] => rewrite <- (Zpos_eq_Z_of_nat_o_nat_of_P a) @@ -158,11 +158,11 @@ Ltac zify_nat_op := | |- context [ Z_of_nat (pred ?a) ] => rewrite (pred_of_minus a) (* mult -> Zmult and a positivity hypothesis *) - | H : context [ Z_of_nat (mult ?a ?b) ] |- _ => - let H:= fresh "H" in + | H : context [ Z_of_nat (mult ?a ?b) ] |- _ => + let H:= fresh "H" in assert (H:=Zle_0_nat (mult a b)); rewrite (inj_mult a b) in * - | |- context [ Z_of_nat (mult ?a ?b) ] => - let H:= fresh "H" in + | |- context [ Z_of_nat (mult ?a ?b) ] => + let H:= fresh "H" in assert (H:=Zle_0_nat (mult a b)); rewrite (inj_mult a b) in * (* O -> Z0 *) @@ -170,29 +170,29 @@ Ltac zify_nat_op := | |- context [ Z_of_nat O ] => simpl (Z_of_nat O) (* S -> number or Zsucc *) - | H : context [ Z_of_nat (S ?a) ] |- _ => - let isnat := isnatcst a in - match isnat with + | H : context [ Z_of_nat (S ?a) ] |- _ => + let isnat := isnatcst a in + match isnat with | true => simpl (Z_of_nat (S a)) in H | _ => rewrite (inj_S a) in H end - | |- context [ Z_of_nat (S ?a) ] => - let isnat := isnatcst a in - match isnat with + | |- context [ Z_of_nat (S ?a) ] => + let isnat := isnatcst a in + match isnat with | true => simpl (Z_of_nat (S a)) | _ => rewrite (inj_S a) end - (* atoms of type nat : we add a positivity condition (if not already there) *) - | H : context [ Z_of_nat ?a ] |- _ => - match goal with + (* atoms of type nat : we add a positivity condition (if not already there) *) + | H : context [ Z_of_nat ?a ] |- _ => + match goal with | H' : 0 <= Z_of_nat a |- _ => hide_Z_of_nat a | H' : 0 <= Z_of_nat' a |- _ => fail | _ => let H:= fresh "H" in assert (H:=Zle_0_nat a); hide_Z_of_nat a end - | |- context [ Z_of_nat ?a ] => - match goal with + | |- context [ Z_of_nat ?a ] => + match goal with | H' : 0 <= Z_of_nat a |- _ => hide_Z_of_nat a | H' : 0 <= Z_of_nat' a |- _ => fail | _ => let H:= fresh "H" in @@ -205,18 +205,18 @@ Ltac zify_nat := repeat zify_nat_rel; repeat zify_nat_op; unfold Z_of_nat' in *. -(* III) conversion from positive to Z *) +(* III) conversion from positive to Z *) Definition Zpos' := Zpos. Definition Zneg' := Zneg. -Ltac hide_Zpos t := - let z := fresh "z" in set (z:=Zpos t) in *; - change Zpos with Zpos' in z; +Ltac hide_Zpos t := + let z := fresh "z" in set (z:=Zpos t) in *; + change Zpos with Zpos' in z; unfold z in *; clear z. -Ltac zify_positive_rel := - match goal with +Ltac zify_positive_rel := + match goal with (* I: equalities *) | H : (@eq positive ?a ?b) |- _ => generalize (Zpos_eq _ _ H); clear H; intro H | |- (@eq positive ?a ?b) => apply (Zpos_eq_rev a b) @@ -236,18 +236,18 @@ Ltac zify_positive_rel := | |- context [ (?a>=?b)%positive ] => change (a>=b)%positive with (Zpos a>=Zpos b) end. -Ltac zify_positive_op := - match goal with +Ltac zify_positive_op := + match goal with (* Zneg -> -Zpos (except for numbers) *) - | H : context [ Zneg ?a ] |- _ => - let isp := isPcst a in - match isp with + | H : context [ Zneg ?a ] |- _ => + let isp := isPcst a in + match isp with | true => change (Zneg a) with (Zneg' a) in H | _ => change (Zneg a) with (- Zpos a) in H end - | |- context [ Zneg ?a ] => - let isp := isPcst a in - match isp with + | |- context [ Zneg ?a ] => + let isp := isPcst a in + match isp with | true => change (Zneg a) with (Zneg' a) | _ => change (Zneg a) with (- Zpos a) end @@ -272,45 +272,45 @@ Ltac zify_positive_op := | H : context [ Zpos (Pminus ?a ?b) ] |- _ => rewrite (Zpos_minus a b) in H | |- context [ Zpos (Pminus ?a ?b) ] => rewrite (Zpos_minus a b) - (* Psucc -> Zsucc *) + (* Psucc -> Zsucc *) | H : context [ Zpos (Psucc ?a) ] |- _ => rewrite (Zpos_succ_morphism a) in H | |- context [ Zpos (Psucc ?a) ] => rewrite (Zpos_succ_morphism a) (* Ppred -> Pminus ... -1 -> Zmax 1 (Zminus ... - 1) *) | H : context [ Zpos (Ppred ?a) ] |- _ => rewrite (Ppred_minus a) in H | |- context [ Zpos (Ppred ?a) ] => rewrite (Ppred_minus a) - + (* Pmult -> Zmult and a positivity hypothesis *) - | H : context [ Zpos (Pmult ?a ?b) ] |- _ => - let H:= fresh "H" in + | H : context [ Zpos (Pmult ?a ?b) ] |- _ => + let H:= fresh "H" in assert (H:=Zgt_pos_0 (Pmult a b)); rewrite (Zpos_mult_morphism a b) in * - | |- context [ Zpos (Pmult ?a ?b) ] => - let H:= fresh "H" in + | |- context [ Zpos (Pmult ?a ?b) ] => + let H:= fresh "H" in assert (H:=Zgt_pos_0 (Pmult a b)); rewrite (Zpos_mult_morphism a b) in * (* xO *) - | H : context [ Zpos (xO ?a) ] |- _ => - let isp := isPcst a in - match isp with + | H : context [ Zpos (xO ?a) ] |- _ => + let isp := isPcst a in + match isp with | true => change (Zpos (xO a)) with (Zpos' (xO a)) in H | _ => rewrite (Zpos_xO a) in H end - | |- context [ Zpos (xO ?a) ] => - let isp := isPcst a in - match isp with + | |- context [ Zpos (xO ?a) ] => + let isp := isPcst a in + match isp with | true => change (Zpos (xO a)) with (Zpos' (xO a)) | _ => rewrite (Zpos_xO a) end - (* xI *) - | H : context [ Zpos (xI ?a) ] |- _ => - let isp := isPcst a in - match isp with + (* xI *) + | H : context [ Zpos (xI ?a) ] |- _ => + let isp := isPcst a in + match isp with | true => change (Zpos (xI a)) with (Zpos' (xI a)) in H | _ => rewrite (Zpos_xI a) in H end - | |- context [ Zpos (xI ?a) ] => - let isp := isPcst a in - match isp with + | |- context [ Zpos (xI ?a) ] => + let isp := isPcst a in + match isp with | true => change (Zpos (xI a)) with (Zpos' (xI a)) | _ => rewrite (Zpos_xI a) end @@ -320,38 +320,38 @@ Ltac zify_positive_op := | |- context [ Zpos xH ] => hide_Zpos xH (* atoms of type positive : we add a positivity condition (if not already there) *) - | H : context [ Zpos ?a ] |- _ => - match goal with + | H : context [ Zpos ?a ] |- _ => + match goal with | H' : Zpos a > 0 |- _ => hide_Zpos a | H' : Zpos' a > 0 |- _ => fail | _ => let H:= fresh "H" in assert (H:=Zgt_pos_0 a); hide_Zpos a end - | |- context [ Zpos ?a ] => - match goal with + | |- context [ Zpos ?a ] => + match goal with | H' : Zpos a > 0 |- _ => hide_Zpos a | H' : Zpos' a > 0 |- _ => fail | _ => let H:= fresh "H" in assert (H:=Zgt_pos_0 a); hide_Zpos a end end. -Ltac zify_positive := +Ltac zify_positive := repeat zify_positive_rel; repeat zify_positive_op; unfold Zpos',Zneg' in *. -(* IV) conversion from N to Z *) +(* IV) conversion from N to Z *) Definition Z_of_N' := Z_of_N. -Ltac hide_Z_of_N t := - let z := fresh "z" in set (z:=Z_of_N t) in *; - change Z_of_N with Z_of_N' in z; +Ltac hide_Z_of_N t := + let z := fresh "z" in set (z:=Z_of_N t) in *; + change Z_of_N with Z_of_N' in z; unfold z in *; clear z. -Ltac zify_N_rel := - match goal with +Ltac zify_N_rel := + match goal with (* I: equalities *) | H : (@eq N ?a ?b) |- _ => generalize (Z_of_N_eq _ _ H); clear H; intro H | |- (@eq N ?a ?b) => apply (Z_of_N_eq_rev a b) @@ -378,9 +378,9 @@ Ltac zify_N_rel := | H : context [ (?a>=?b)%N ] |- _ => rewrite (Z_of_N_ge_iff a b) in H | |- context [ (?a>=?b)%N ] => rewrite (Z_of_N_ge_iff a b) end. - -Ltac zify_N_op := - match goal with + +Ltac zify_N_op := + match goal with (* misc type conversions: nat to positive *) | H : context [ Z_of_N (N_of_nat ?a) ] |- _ => rewrite (Z_of_N_of_nat a) in H | |- context [ Z_of_N (N_of_nat ?a) ] => rewrite (Z_of_N_of_nat a) @@ -407,27 +407,27 @@ Ltac zify_N_op := | H : context [ Z_of_N (Nminus ?a ?b) ] |- _ => rewrite (Z_of_N_minus a b) in H | |- context [ Z_of_N (Nminus ?a ?b) ] => rewrite (Z_of_N_minus a b) - (* Nsucc -> Zsucc *) + (* Nsucc -> Zsucc *) | H : context [ Z_of_N (Nsucc ?a) ] |- _ => rewrite (Z_of_N_succ a) in H | |- context [ Z_of_N (Nsucc ?a) ] => rewrite (Z_of_N_succ a) - + (* Nmult -> Zmult and a positivity hypothesis *) - | H : context [ Z_of_N (Nmult ?a ?b) ] |- _ => - let H:= fresh "H" in + | H : context [ Z_of_N (Nmult ?a ?b) ] |- _ => + let H:= fresh "H" in assert (H:=Z_of_N_le_0 (Nmult a b)); rewrite (Z_of_N_mult a b) in * - | |- context [ Z_of_N (Nmult ?a ?b) ] => - let H:= fresh "H" in + | |- context [ Z_of_N (Nmult ?a ?b) ] => + let H:= fresh "H" in assert (H:=Z_of_N_le_0 (Nmult a b)); rewrite (Z_of_N_mult a b) in * - (* atoms of type N : we add a positivity condition (if not already there) *) - | H : context [ Z_of_N ?a ] |- _ => - match goal with + (* atoms of type N : we add a positivity condition (if not already there) *) + | H : context [ Z_of_N ?a ] |- _ => + match goal with | H' : 0 <= Z_of_N a |- _ => hide_Z_of_N a | H' : 0 <= Z_of_N' a |- _ => fail | _ => let H:= fresh "H" in assert (H:=Z_of_N_le_0 a); hide_Z_of_N a end - | |- context [ Z_of_N ?a ] => - match goal with + | |- context [ Z_of_N ?a ] => + match goal with | H' : 0 <= Z_of_N a |- _ => hide_Z_of_N a | H' : 0 <= Z_of_N' a |- _ => fail | _ => let H:= fresh "H" in assert (H:=Z_of_N_le_0 a); hide_Z_of_N a @@ -440,6 +440,6 @@ Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *. (** The complete Z-ification tactic *) -Ltac zify := +Ltac zify := repeat progress (zify_nat; zify_positive; zify_N); zify_op. diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 075188f54..e037ee8bf 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -58,7 +58,7 @@ let write f x = f:=x open Goptions let _ = - declare_bool_option + declare_bool_option { optsync = false; optname = "Omega system time displaying flag"; optkey = ["Omega";"System"]; @@ -66,7 +66,7 @@ let _ = optwrite = write display_system_flag } let _ = - declare_bool_option + declare_bool_option { optsync = false; optname = "Omega action display flag"; optkey = ["Omega";"Action"]; @@ -74,7 +74,7 @@ let _ = optwrite = write display_action_flag } let _ = - declare_bool_option + declare_bool_option { optsync = false; optname = "Omega old style flag"; optkey = ["Omega";"OldStyle"]; @@ -89,16 +89,16 @@ let elim_time = timing "Elim " let simpl_time = timing "Simpl " let generalize_time = timing "Generalize" -let new_identifier = - let cpt = ref 0 in +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 +let new_identifier_state = + let cpt = ref 0 in (fun () -> let s = make_ident "State" (Some !cpt) in incr cpt; s) -let new_identifier_var = - let cpt = ref 0 in +let new_identifier_var = + let cpt = ref 0 in (fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; id_of_string s) let new_id = @@ -115,17 +115,17 @@ let display_var i = Printf.sprintf "X%d" i let intern_id,unintern_id = let cpt = ref 0 in let table = Hashtbl.create 7 and co_table = Hashtbl.create 7 in - (fun (name : identifier) -> - try Hashtbl.find table name with Not_found -> + (fun (name : identifier) -> + try Hashtbl.find table name with Not_found -> let idx = !cpt in - Hashtbl.add table name idx; + Hashtbl.add table name idx; Hashtbl.add co_table idx name; incr cpt; idx), - (fun idx -> - try Hashtbl.find co_table idx with Not_found -> + (fun idx -> + try Hashtbl.find co_table idx with Not_found -> let v = new_var () in Hashtbl.add table v idx; Hashtbl.add co_table idx v; v) - + let mk_then = tclTHENLIST let exists_tac c = constructor_tac false (Some 1) 1 (Rawterm.ImplicitBindings [c]) @@ -134,10 +134,10 @@ let generalize_tac t = generalize_time (generalize t) let elim t = elim_time (simplest_elim t) let exact t = exact_time (Tactics.refine t) let unfold s = Tactics.unfold_in_concl [all_occurrences, Lazy.force s] - + let rev_assoc k = let rec loop = function - | [] -> raise Not_found | (v,k')::_ when k = k' -> v | _ :: l -> loop l + | [] -> raise Not_found | (v,k')::_ when k = k' -> v | _ :: l -> loop l in loop @@ -347,15 +347,15 @@ let mk_eq_rel t1 t2 = mkApp (build_coq_eq (), let mk_inj t = mkApp (Lazy.force coq_Z_of_nat, [| t |]) let mk_integer n = - let rec loop n = - if n =? one then Lazy.force coq_xH else + let rec loop n = + if n =? one then Lazy.force coq_xH else mkApp((if n mod two =? zero then Lazy.force coq_xO else Lazy.force coq_xI), [| loop (n/two) |]) in - if n =? zero then Lazy.force coq_Z0 + if n =? zero then Lazy.force coq_Z0 else mkApp ((if n >? zero then Lazy.force coq_Zpos else Lazy.force coq_Zneg), [| loop (abs n) |]) - + type omega_constant = | Zplus | Zmult | Zminus | Zsucc | Zopp | Plus | Mult | Minus | Pred | S | O @@ -371,7 +371,7 @@ type omega_proposition = | Keq of constr * constr * constr | Kn -type result = +type result = | Kvar of identifier | Kapp of omega_constant * constr list | Kimp of constr * constr @@ -442,18 +442,18 @@ let recognize_number t = | f, [t] when f = Lazy.force coq_xI -> one + two * loop t | f, [t] when f = Lazy.force coq_xO -> two * loop t | f, [] when f = Lazy.force coq_xH -> one - | _ -> failwith "not a number" + | _ -> failwith "not a number" in - match decompose_app t with + match decompose_app t with | f, [t] when f = Lazy.force coq_Zpos -> loop t | f, [t] when f = Lazy.force coq_Zneg -> neg (loop t) | f, [] when f = Lazy.force coq_Z0 -> zero | _ -> failwith "not a number" - + type constr_path = | P_APP of int (* Abstraction and product *) - | P_BODY + | P_BODY | P_TYPE (* Case *) | P_BRANCH of int @@ -461,8 +461,8 @@ type constr_path = | P_ARG let context operation path (t : constr) = - let rec loop i p0 t = - match (p0,kind_of_term t) with + let rec loop i p0 t = + match (p0,kind_of_term t) with | (p, Cast (c,k,t)) -> mkCast (loop i p c,k,t) | ([], _) -> operation i t | ((P_APP n :: p), App (f,v)) -> @@ -493,9 +493,9 @@ let context operation path (t : constr) = (mkLambda (n,loop i p t,c)) | ((P_TYPE :: p), LetIn (n,b,t,c)) -> (mkLetIn (n,b,loop i p t,c)) - | (p, _) -> + | (p, _) -> ppnl (Printer.pr_lconstr t); - failwith ("abstract_path " ^ string_of_int(List.length p)) + failwith ("abstract_path " ^ string_of_int(List.length p)) in loop 1 path t @@ -514,9 +514,9 @@ let occurence path (t : constr) = | ((P_TYPE :: p), Prod (n,term,c)) -> loop p term | ((P_TYPE :: p), Lambda (n,term,c)) -> loop p term | ((P_TYPE :: p), LetIn (n,b,term,c)) -> loop p term - | (p, _) -> + | (p, _) -> ppnl (Printer.pr_lconstr t); - failwith ("occurence " ^ string_of_int(List.length p)) + failwith ("occurence " ^ string_of_int(List.length p)) in loop path t @@ -539,13 +539,13 @@ type oformula = | Oz of bigint | Oufo of constr -let rec oprint = function - | Oplus(t1,t2) -> - print_string "("; oprint t1; print_string "+"; +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 "*"; + | Otimes (t1,t2) -> + print_string "("; oprint t1; print_string "*"; oprint t2; print_string ")" | Oatom s -> print_string (string_of_id s) | Oz i -> print_string (string_of_bigint i) @@ -567,92 +567,92 @@ let rec val_of = function | Oplus(t1,t2) -> mkApp (Lazy.force coq_Zplus, [| val_of t1; val_of t2 |]) | Oufo c -> c -let compile name kind = +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" + | _ -> anomaly "compile_equation" in loop [] -let rec decompile af = +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 + | ({v=v; c=n}::r) -> Oplus(Otimes(Oatom (unintern_id v),Oz n),loop r) + | [] -> Oz af.constant in loop af.body let mkNewMeta () = mkMeta (Evarutil.new_meta()) -let clever_rewrite_base_poly typ p result theorem gl = +let 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 = + let t = applist (mkLambda - (Name (id_of_string "P"), + (Name (id_of_string "P"), mkArrow typ mkProp, mkLambda (Name (id_of_string "H"), applist (mkRel 1,[result]), - mkApp (Lazy.force coq_eq_ind_r, + mkApp (Lazy.force coq_eq_ind_r, [| typ; result; mkRel 2; mkRel 1; occ; theorem |]))), - [abstracted]) + [abstracted]) in exact (applist(t,[mkNewMeta()])) gl -let clever_rewrite_base p result theorem 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 = +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 +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 +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 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) = +let rec shuffle p (t1,t2) = match t1,t2 with | Oplus(l1,r1), Oplus(l2,r2) -> - if weight l1 > weight l2 then + 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]; + (clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]] (Lazy.force coq_fast_Zplus_assoc_reverse) :: tac, Oplus(l1,t')) - else + 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 -> + | Oplus(l1,r1), t2 -> if weight l1 > weight t2 then let (tac,t') = shuffle (P_APP 2 :: p) (r1,t2) in clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]] (Lazy.force coq_fast_Zplus_assoc_reverse) - :: tac, + :: tac, Oplus(l1, t') - else - [clever_rewrite p [[P_APP 1];[P_APP 2]] + else + [clever_rewrite p [[P_APP 1];[P_APP 2]] (Lazy.force coq_fast_Zplus_comm)], Oplus(t2,t1) - | t1,Oplus(l2,r2) -> + | 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]] @@ -664,11 +664,11 @@ let rec shuffle p (t1,t2) = [focused_simpl p], Oz(Bigint.add t1 t2) | t1,t2 -> if weight t1 < weight t2 then - [clever_rewrite p [[P_APP 1];[P_APP 2]] + [clever_rewrite p [[P_APP 1];[P_APP 2]] (Lazy.force coq_fast_Zplus_comm)], Oplus(t2,t1) else [],Oplus(t1,t2) - + let rec shuffle_mult p_init k1 e1 k2 e2 = let rec loop p = function | (({c=c1;v=v1}::l1) as l1'),(({c=c2;v=v2}::l2) as l2') -> @@ -681,13 +681,13 @@ let rec shuffle_mult p_init k1 e1 k2 e2 = [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) + (Lazy.force coq_fast_OMEGA10) in - if Bigint.add (Bigint.mult k1 c1) (Bigint.mult k2 c2) =? zero then - let tac' = + if Bigint.add (Bigint.mult k1 c1) (Bigint.mult k2 c2) =? zero then + let tac' = clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] (Lazy.force coq_fast_Zred_factor5) in - tac :: focused_simpl (P_APP 1::P_APP 2:: p) :: tac' :: + 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 @@ -706,7 +706,7 @@ let rec shuffle_mult p_init k1 e1 k2 e2 = [P_APP 2; P_APP 2]] (Lazy.force coq_fast_OMEGA12) :: loop (P_APP 2 :: p) (l1',l2) - | ({c=c1;v=v1}::l1), [] -> + | ({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]; @@ -714,7 +714,7 @@ let rec shuffle_mult p_init k1 e1 k2 e2 = [P_APP 1; P_APP 2]] (Lazy.force coq_fast_OMEGA11) :: loop (P_APP 2 :: p) (l1,[]) - | [],({c=c2;v=v2}::l2) -> + | [],({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]; @@ -722,10 +722,10 @@ let rec shuffle_mult p_init k1 e1 k2 e2 = [P_APP 2; P_APP 2]] (Lazy.force coq_fast_OMEGA12) :: loop (P_APP 2 :: p) ([],l2) - | [],[] -> [focused_simpl p_init] + | [],[] -> [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') -> @@ -738,14 +738,14 @@ let rec shuffle_mult_right p_init e1 k2 e2 = [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) + (Lazy.force coq_fast_OMEGA15) in - if Bigint.add c1 (Bigint.mult k2 c2) =? zero then - let tac' = + if Bigint.add c1 (Bigint.mult k2 c2) =? zero then + let tac' = clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] - (Lazy.force coq_fast_Zred_factor5) + (Lazy.force coq_fast_Zred_factor5) in - tac :: focused_simpl (P_APP 1::P_APP 2:: p) :: tac' :: + 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 @@ -760,11 +760,11 @@ let rec shuffle_mult_right p_init e1 k2 e2 = [P_APP 2; P_APP 2]] (Lazy.force coq_fast_OMEGA12) :: loop (P_APP 2 :: p) (l1',l2) - | ({c=c1;v=v1}::l1), [] -> + | ({c=c1;v=v1}::l1), [] -> clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]] (Lazy.force coq_fast_Zplus_assoc_reverse) :: loop (P_APP 2 :: p) (l1,[]) - | [],({c=c2;v=v2}::l2) -> + | [],({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]; @@ -772,89 +772,89 @@ let rec shuffle_mult_right p_init e1 k2 e2 = [P_APP 2; P_APP 2]] (Lazy.force coq_fast_OMEGA12) :: loop (P_APP 2 :: p) ([],l2) - | [],[] -> [focused_simpl p_init] + | [],[] -> [focused_simpl p_init] in loop p_init (e1,e2) -let rec shuffle_cancel p = function +let rec shuffle_cancel p = function | [] -> [focused_simpl p] | ({c=c1}::l1) -> - let tac = + 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 2; P_APP 2]; [P_APP 1; P_APP 1; P_APP 2; P_APP 1]] - (if c1 >? zero then - (Lazy.force coq_fast_OMEGA13) - else - (Lazy.force coq_fast_OMEGA14)) + (if c1 >? zero then + (Lazy.force coq_fast_OMEGA13) + else + (Lazy.force coq_fast_OMEGA14)) in tac :: shuffle_cancel p l1 - + let rec scalar p n = function - | Oplus(t1,t2) -> - let tac1,t1' = scalar (P_APP 1 :: p) n t1 and + | Oplus(t1,t2) -> + let tac1,t1' = scalar (P_APP 1 :: p) n t1 and tac2,t2' = scalar (P_APP 2 :: p) n t2 in clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]] - (Lazy.force coq_fast_Zmult_plus_distr_l) :: + (Lazy.force coq_fast_Zmult_plus_distr_l) :: (tac1 @ tac2), Oplus(t1',t2') | Oinv t -> - [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] + [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] (Lazy.force coq_fast_Zmult_opp_comm); focused_simpl (P_APP 2 :: p)], Otimes(t,Oz(neg n)) - | Otimes(t1,Oz x) -> + | Otimes(t1,Oz x) -> [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]] (Lazy.force coq_fast_Zmult_assoc_reverse); - focused_simpl (P_APP 2 :: p)], + focused_simpl (P_APP 2 :: p)], Otimes(t1,Oz (n*x)) | Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products" | (Oatom _ as t) -> [], Otimes(t,Oz n) | Oz i -> [focused_simpl p],Oz(n*i) | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zmult, [| mk_integer n; c |])) - -let rec scalar_norm p_init = + +let rec scalar_norm p_init = let rec loop p = function | [] -> [focused_simpl p_init] - | (_::l) -> + | (_::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 + (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 -> + | _:: l -> clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]] (Lazy.force coq_fast_Zplus_assoc_reverse) :: - loop (P_APP 2 :: p) l + 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 -> + | _ :: 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 + (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 + | Oplus(t1,t2) -> + let tac1,t1' = negate (P_APP 1 :: p) t1 and tac2,t2' = negate (P_APP 2 :: p) t2 in clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]] - (Lazy.force coq_fast_Zopp_plus_distr) :: + (Lazy.force coq_fast_Zopp_plus_distr) :: (tac1 @ tac2), Oplus(t1',t2') | Oinv t -> [clever_rewrite p [[P_APP 1;P_APP 1]] (Lazy.force coq_fast_Zopp_involutive)], t - | Otimes(t1,Oz x) -> + | Otimes(t1,Oz x) -> [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]] (Lazy.force coq_fast_Zopp_mult_distr_r); focused_simpl (P_APP 2 :: p)], Otimes(t1,Oz (neg x)) @@ -864,13 +864,13 @@ let rec negate p = function [clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1)], r | Oz i -> [focused_simpl p],Oz(neg i) | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zopp, [| c |])) - -let rec transform p t = + +let rec transform p t = let default isnat t' = - try + try let v,th,_ = find_constr t' in [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v - with _ -> + with _ -> let v = new_identifier_var () and th = new_identifier () in hide_constr t' v th isnat; @@ -878,12 +878,12 @@ let rec transform p t = in try match destructurate_term t with | Kapp(Zplus,[t1;t2]) -> - let tac1,t1' = transform (P_APP 1 :: p) t1 + 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 = + let tac,t = transform p (mkApp (Lazy.force coq_Zplus, [| t1; (mkApp (Lazy.force coq_Zopp, [| t2 |])) |])) in @@ -893,18 +893,18 @@ let rec transform p t = [| t1; mk_integer one |])) in unfold sp_Zsucc :: tac,t | Kapp(Zmult,[t1;t2]) -> - let tac1,t1' = transform (P_APP 1 :: p) t1 + 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]] + let sym = + clever_rewrite p [[P_APP 1];[P_APP 2]] (Lazy.force coq_fast_Zmult_comm) in let tac,t' = scalar p n t2' in tac1 @ tac2 @ (sym :: tac),t' | _ -> default false t end - | Kapp((Zpos|Zneg|Z0),_) -> + | Kapp((Zpos|Zneg|Z0),_) -> (try ([],Oz(recognize_number t)) with _ -> default false t) | Kvar s -> [],Oatom s | Kapp(Zopp,[t]) -> @@ -914,28 +914,28 @@ let rec transform p t = | Kapp(Z_of_nat,[t']) -> default true t' | _ -> default false t with e when catchable_exception e -> default false t - + let shrink_pair p f1 f2 = match f1,f2 with - | Oatom v,Oatom _ -> + | Oatom v,Oatom _ -> let r = Otimes(Oatom v,Oz two) in clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zred_factor1), r - | Oatom v, Otimes(_,c2) -> + | Oatom v, Otimes(_,c2) -> let r = Otimes(Oatom v,Oplus(c2,Oz one)) in - clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 2]] + clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 2]] (Lazy.force coq_fast_Zred_factor2), r - | Otimes (v1,c1),Oatom v -> + | Otimes (v1,c1),Oatom v -> let r = Otimes(Oatom v,Oplus(c1,Oz one)) in clever_rewrite p [[P_APP 2];[P_APP 1;P_APP 2]] (Lazy.force coq_fast_Zred_factor3), r | Otimes (Oatom v,c1),Otimes (v2,c2) -> let r = Otimes(Oatom v,Oplus(c1,c2)) in - clever_rewrite p + 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 (); + | t1,t2 -> + begin + oprint t1; print_newline (); oprint t2; print_newline (); flush Pervasives.stdout; error "shrink.1" end @@ -948,7 +948,7 @@ let reduce_factor p = function let rec compute = function | Oz n -> n | Oplus(t1,t2) -> Bigint.add (compute t1) (compute t2) - | _ -> error "condense.1" + | _ -> error "condense.1" in [focused_simpl (P_APP 2 :: p)], Otimes(Oatom v,Oz(compute c)) | t -> oprint t; error "reduce_factor.1" @@ -957,31 +957,31 @@ 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 + let assoc_tac = + clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 1];[P_APP 2;P_APP 2]] (Lazy.force coq_fast_Zplus_assoc) in let tac_list,t' = condense p (Oplus(t,r)) in (assoc_tac :: shrink_tac :: tac_list), t' end else begin let tac,f = reduce_factor (P_APP 1 :: p) f1 in - let tac',t' = condense (P_APP 2 :: p) t in - (tac @ tac'), Oplus(f,t') + let tac',t' = condense (P_APP 2 :: p) t in + (tac @ tac'), Oplus(f,t') end - | Oplus(f1,Oz n) -> + | Oplus(f1,Oz n) -> let tac,f1' = reduce_factor (P_APP 1 :: p) f1 in tac,Oplus(f1',Oz n) - | Oplus(f1,f2) -> + | 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') + let tac',t' = condense (P_APP 2 :: p) f2 in + (tac @ tac'),Oplus(f,t') end | Oz _ as t -> [],t - | t -> + | t -> let tac,t' = reduce_factor p t in let final = Oplus(t',Oz zero) in let tac' = clever_rewrite p [[]] (Lazy.force coq_fast_Zred_factor6) in @@ -990,99 +990,99 @@ let rec condense p = function let rec clear_zero p = function | Oplus(Otimes(Oatom v,Oz n),r) when n =? zero -> let tac = - clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] + 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) -> + | 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 replay_history tactic_normalisation = let aux = id_of_string "auxiliary" in let aux1 = id_of_string "auxiliary_1" in let aux2 = id_of_string "auxiliary_2" in let izero = mk_integer zero in let rec loop t = match t with - | HYP e :: l -> - begin - try - tclTHEN - (List.assoc (hyp_of_tag e.id) tactic_normalisation) + | 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 + let eq1 = decompile e1 + and eq2 = decompile e2 in + let id1 = hyp_of_tag e1.id and id2 = hyp_of_tag e2.id in let k = if b then negone else one in let p_initial = [P_APP 1;P_TYPE] in let tac= shuffle_mult_right p_initial e1.body k e2.body in tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_OMEGA17, [| + (generalize_tac + [mkApp (Lazy.force coq_OMEGA17, [| val_of eq1; val_of eq2; - mk_integer k; + mk_integer k; mkVar id1; mkVar id2 |])]); (mk_then tac); (intros_using [aux]); (resolve_id aux); reflexivity ] - | CONTRADICTION (e1,e2) :: l -> - let eq1 = decompile e1 - and eq2 = decompile e2 in + | CONTRADICTION (e1,e2) :: l -> + let eq1 = decompile e1 + and eq2 = decompile e2 in let p_initial = [P_APP 2;P_TYPE] in let tac = shuffle_cancel p_initial e1.body in let solve_le = - let not_sup_sup = mkApp (build_coq_eq (), [| - Lazy.force coq_comparison; + let not_sup_sup = mkApp (build_coq_eq (), [| + Lazy.force coq_comparison; Lazy.force coq_Gt; Lazy.force coq_Gt |]) in - tclTHENS + tclTHENS (tclTHENLIST [ (unfold sp_Zle); (simpl_in_concl); intro; (absurd not_sup_sup) ]) - [ assumption ; reflexivity ] + [ assumption ; reflexivity ] in let theorem = - mkApp (Lazy.force coq_OMEGA2, [| - val_of eq1; val_of eq2; + mkApp (Lazy.force coq_OMEGA2, [| + val_of eq1; val_of eq2; mkVar (hyp_of_tag e1.id); mkVar (hyp_of_tag e2.id) |]) in tclTHEN (tclTHEN (generalize_tac [theorem]) (mk_then tac)) (solve_le) | DIVIDE_AND_APPROX (e1,e2,k,d) :: l -> let id = hyp_of_tag e1.id in - let eq1 = val_of(decompile e1) + let eq1 = val_of(decompile e1) and eq2 = val_of(decompile e2) in - let kk = mk_integer k + 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 + (cut state_eg) [ tclTHENS (tclTHENLIST [ (intros_using [aux]); - (generalize_tac + (generalize_tac [mkApp (Lazy.force coq_OMEGA1, [| eq1; rhs; mkVar aux; mkVar id |])]); (clear [aux;id]); (intros_using [id]); (cut (mk_gt kk dd)) ]) - [ tclTHENS - (cut (mk_gt kk izero)) + [ tclTHENS + (cut (mk_gt kk izero)) [ tclTHENLIST [ (intros_using [aux1; aux2]); - (generalize_tac + (generalize_tac [mkApp (Lazy.force coq_Zmult_le_approx, [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])]); (clear [aux1;aux2;id]); @@ -1095,23 +1095,23 @@ let replay_history tactic_normalisation = tclTHENLIST [ (unfold sp_Zgt); simpl_in_concl; reflexivity ] ]; tclTHEN (mk_then tac) reflexivity ] - + | NOT_EXACT_DIVIDE (e1,k) :: l -> let c = floor_div e1.constant k in let d = Bigint.sub e1.constant (Bigint.mult c k) in - let e2 = {id=e1.id; kind=EQUA;constant = c; + let e2 = {id=e1.id; kind=EQUA;constant = c; body = map_eq_linear (fun c -> c / k) e1.body } in let eq2 = val_of(decompile e2) in - let kk = mk_integer k + let kk = mk_integer k and dd = mk_integer d in let tac = scalar_norm_add [P_APP 2] e2.body in - tclTHENS - (cut (mk_gt dd izero)) - [ tclTHENS (cut (mk_gt kk dd)) + tclTHENS + (cut (mk_gt dd izero)) + [ tclTHENS (cut (mk_gt kk dd)) [tclTHENLIST [ (intros_using [aux2;aux1]); - (generalize_tac - [mkApp (Lazy.force coq_OMEGA4, + (generalize_tac + [mkApp (Lazy.force coq_OMEGA4, [| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]); (clear [aux1;aux2]); (unfold sp_not); @@ -1121,7 +1121,7 @@ let replay_history tactic_normalisation = assumption ] ; tclTHENLIST [ (unfold sp_Zgt); - simpl_in_concl; + simpl_in_concl; reflexivity ] ]; tclTHENLIST [ (unfold sp_Zgt); @@ -1130,18 +1130,18 @@ let replay_history tactic_normalisation = | 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) + let eq1 = val_of(decompile e1) and eq2 = val_of(decompile e2) in let kk = mk_integer k in let state_eq = mk_eq eq1 (mk_times eq2 kk) in if e1.kind = DISE then let tac = scalar_norm [P_APP 3] e2.body in - tclTHENS - (cut state_eq) + tclTHENS + (cut state_eq) [tclTHENLIST [ (intros_using [aux1]); - (generalize_tac - [mkApp (Lazy.force coq_OMEGA18, + (generalize_tac + [mkApp (Lazy.force coq_OMEGA18, [| eq1;eq2;kk;mkVar aux1; mkVar id |])]); (clear [aux1;id]); (intros_using [id]); @@ -1149,14 +1149,14 @@ let replay_history tactic_normalisation = tclTHEN (mk_then tac) reflexivity ] else let tac = scalar_norm [P_APP 3] e2.body in - tclTHENS (cut state_eq) + tclTHENS (cut state_eq) [ - tclTHENS - (cut (mk_gt kk izero)) + tclTHENS + (cut (mk_gt kk izero)) [tclTHENLIST [ (intros_using [aux2;aux1]); - (generalize_tac - [mkApp (Lazy.force coq_OMEGA3, + (generalize_tac + [mkApp (Lazy.force coq_OMEGA3, [| eq1; eq2; kk; mkVar aux2; mkVar aux1;mkVar id|])]); (clear [aux1;aux2;id]); (intros_using [id]); @@ -1169,35 +1169,35 @@ let replay_history tactic_normalisation = | (MERGE_EQ(e3,e1,e2)) :: l -> let id = new_identifier () in tag_hypothesis id e3; - let id1 = hyp_of_tag e1.id + let id1 = hyp_of_tag e1.id and id2 = hyp_of_tag e2 in - let eq1 = val_of(decompile e1) + 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]] + let tac = + clever_rewrite [P_APP 3] [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1) :: - scalar_norm [P_APP 3] e1.body + scalar_norm [P_APP 3] e1.body in - tclTHENS - (cut (mk_eq eq1 (mk_inv eq2))) + tclTHENS + (cut (mk_eq eq1 (mk_inv eq2))) [tclTHENLIST [ (intros_using [aux]); - (generalize_tac [mkApp (Lazy.force coq_OMEGA8, + (generalize_tac [mkApp (Lazy.force coq_OMEGA8, [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]); (clear [id1;id2;aux]); (intros_using [id]); (loop l) ]; tclTHEN (mk_then tac) reflexivity] - + | STATE {st_new_eq=e;st_def=def;st_orig=orig;st_coef=m;st_var=v} :: l -> - let id = new_identifier () + let id = new_identifier () and id2 = hyp_of_tag orig.id in tag_hypothesis id e.id; - let eq1 = val_of(decompile def) + let eq1 = val_of(decompile def) and eq2 = val_of(decompile orig) in let vid = unintern_id v in let theorem = - mkApp (build_coq_ex (), [| + mkApp (build_coq_ex (), [| Lazy.force coq_Z; mkLambda (Name vid, @@ -1206,20 +1206,20 @@ let replay_history tactic_normalisation = in let mm = mk_integer m in let p_initial = [P_APP 2;P_TYPE] in - let tac = - clever_rewrite (P_APP 1 :: P_APP 1 :: P_APP 2 :: p_initial) + let tac = + clever_rewrite (P_APP 1 :: P_APP 1 :: P_APP 2 :: p_initial) [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1) :: shuffle_mult_right p_initial orig.body m ({c= negone;v= v}::def.body) in - tclTHENS - (cut theorem) + tclTHENS + (cut theorem) [tclTHENLIST [ (intros_using [aux]); (elim_id aux); (clear [aux]); (intros_using [vid; aux]); (generalize_tac - [mkApp (Lazy.force coq_OMEGA9, + [mkApp (Lazy.force coq_OMEGA9, [| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]); (mk_then tac); (clear [aux]); @@ -1227,36 +1227,36 @@ let replay_history tactic_normalisation = (loop l) ]; tclTHEN (exists_tac (inj_open eq1)) reflexivity ] | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l -> - let id1 = new_identifier () + 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 + tclTHENS (simplest_elim (applist (Lazy.force coq_OMEGA19, [eq; mkVar id]))) [tclTHENLIST [ (mk_then tac1); (intros_using [id1]); (loop act1) ]; tclTHENLIST [ (mk_then tac2); (intros_using [id2]); (loop act2) ]] | SUM(e3,(k1,e1),(k2,e2)) :: l -> let id = new_identifier () in tag_hypothesis id e3; - let id1 = hyp_of_tag e1.id + let id1 = hyp_of_tag e1.id and id2 = hyp_of_tag e2.id in - let eq1 = val_of(decompile e1) + let eq1 = val_of(decompile e1) and eq2 = val_of(decompile e2) in if k1 =? one & e2.kind = EQUA then let tac_thm = match e1.kind with - | EQUA -> Lazy.force coq_OMEGA5 - | INEQ -> Lazy.force coq_OMEGA6 - | DISE -> Lazy.force coq_OMEGA20 + | EQUA -> Lazy.force coq_OMEGA5 + | INEQ -> Lazy.force coq_OMEGA6 + | DISE -> Lazy.force coq_OMEGA20 in let kk = mk_integer k2 in let p_initial = if e1.kind=DISE then [P_APP 1; P_TYPE] else [P_APP 2; P_TYPE] in let tac = shuffle_mult_right p_initial e1.body k2 e2.body in - tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]); (mk_then tac); @@ -1264,18 +1264,18 @@ let replay_history tactic_normalisation = (loop l) ] else - let kk1 = mk_integer k1 + let kk1 = mk_integer k1 and kk2 = mk_integer k2 in let p_initial = [P_APP 2;P_TYPE] in let tac= shuffle_mult p_initial k1 e1.body k2 e2.body in - tclTHENS (cut (mk_gt kk1 izero)) - [tclTHENS - (cut (mk_gt kk2 izero)) + tclTHENS (cut (mk_gt kk1 izero)) + [tclTHENS + (cut (mk_gt kk2 izero)) [tclTHENLIST [ (intros_using [aux2;aux1]); (generalize_tac - [mkApp (Lazy.force coq_OMEGA7, [| - eq1;eq2;kk1;kk2; + [mkApp (Lazy.force coq_OMEGA7, [| + eq1;eq2;kk1;kk2; mkVar aux1;mkVar aux2; mkVar id1;mkVar id2 |])]); (clear [aux1;aux2]); @@ -1288,11 +1288,11 @@ let replay_history tactic_normalisation = reflexivity ] ]; tclTHENLIST [ (unfold sp_Zgt); - simpl_in_concl; + simpl_in_concl; reflexivity ] ] - | CONSTANT_NOT_NUL(e,k) :: l -> + | CONSTANT_NOT_NUL(e,k) :: l -> tclTHEN (generalize_tac [mkVar (hyp_of_tag e)]) Equality.discrConcl - | CONSTANT_NUL(e) :: l -> + | CONSTANT_NUL(e) :: l -> tclTHEN (resolve_id (hyp_of_tag e)) reflexivity | CONSTANT_NEG(e,k) :: l -> tclTHENLIST [ @@ -1302,43 +1302,43 @@ let replay_history tactic_normalisation = (unfold sp_not); (intros_using [aux]); (resolve_id aux); - reflexivity + reflexivity ] - | _ -> tclIDTAC + | _ -> 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 + 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 + let shift_left = + tclTHEN (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ]) (tclTRY (clear [id])) in if tac <> [] then - let id' = new_identifier () in + let id' = new_identifier () in ((id',(tclTHENLIST [ (shift_left); (mk_then tac); (intros_using [id']) ])) :: tactic, compile id' flag t' :: defs) - else + else (tactic,defs) - + let destructure_omega gl tac_def (id,c) = - if atompart_of_id id = "State" then + if atompart_of_id id = "State" then tac_def else try match destructurate_prop c with - | Kapp(Eq,[typ;t1;t2]) + | Kapp(Eq,[typ;t1;t2]) when destructurate_type (pf_nf gl typ) = Kapp(Z,[]) -> let t = mk_plus t1 (mk_inv t2) in - normalize_equation + 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 @@ -1369,10 +1369,10 @@ let reintroduce id = let coq_omega gl = clear_tables (); - let tactic_normalisation, system = + let tactic_normalisation, system = List.fold_left (destructure_omega gl) ([],[]) (pf_hyps_types gl) in - let prelude,sys = - List.fold_left + let prelude,sys = + List.fold_left (fun (tac,sys) (t,(v,th,b)) -> if b then let id = new_identifier () in @@ -1385,8 +1385,8 @@ let coq_omega gl = (clear [id]); (intros_using [th;id]); tac ]), - {kind = INEQ; - body = [{v=intern_id v; c=one}]; + {kind = INEQ; + body = [{v=intern_id v; c=one}]; constant = zero; id = i} :: sys else (tclTHENLIST [ @@ -1399,17 +1399,17 @@ let coq_omega gl = let system = system @ sys in if !display_system_flag then display_system display_var system; if !old_style_flag then begin - try + try let _ = simplify (new_id,new_var_num,display_var) false system in tclIDTAC gl - with UNSOLVABLE -> + with UNSOLVABLE -> let _,path = depend [] [] (history ()) in if !display_action_flag then display_action display_var path; - (tclTHEN prelude (replay_history tactic_normalisation path)) gl - end else begin + (tclTHEN prelude (replay_history tactic_normalisation path)) gl + end else begin try let path = simplify_strong (new_id,new_var_num,display_var) system in - if !display_action_flag then display_action display_var path; + if !display_action_flag then display_action display_var path; (tclTHEN prelude (replay_history tactic_normalisation path)) gl with NO_CONTRADICTION -> error "Omega can't solve this system" end @@ -1417,10 +1417,10 @@ let coq_omega gl = let coq_omega = solver_time coq_omega let nat_inject gl = - let rec explore p t = + let rec explore p t = try match destructurate_term t with | Kapp(Plus,[t1;t2]) -> - tclTHENLIST [ + tclTHENLIST [ (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2)) ((Lazy.force coq_inj_plus),[t1;t2])); (explore (P_APP 1 :: p) t1); @@ -1436,61 +1436,61 @@ let nat_inject gl = | 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 + (simplest_elim (applist (Lazy.force coq_le_gt_dec, [t2;t1]))) + (intros_using [id])) [ tclTHENLIST [ - (clever_rewrite_gen p + (clever_rewrite_gen p (mk_minus (mk_inj t1) (mk_inj t2)) ((Lazy.force coq_inj_minus1),[t1;t2;mkVar id])); (loop [id,mkApp (Lazy.force coq_le, [| t2;t1 |])]); (explore (P_APP 1 :: p) t1); (explore (P_APP 2 :: p) t2) ]; - (tclTHEN + (tclTHEN (clever_rewrite_gen p (mk_integer zero) ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id])) (loop [id,mkApp (Lazy.force coq_gt, [| t2;t1 |])])) ] | Kapp(S,[t']) -> let rec is_number t = - try match destructurate_term t with + try match destructurate_term t with Kapp(S,[t]) -> is_number t | Kapp(O,[]) -> true | _ -> false - with e when catchable_exception e -> false + with e when catchable_exception e -> false in let rec loop p t = - try match destructurate_term t with + try match destructurate_term t with Kapp(S,[t]) -> - (tclTHEN - (clever_rewrite_gen p + (tclTHEN + (clever_rewrite_gen p (mkApp (Lazy.force coq_Zsucc, [| mk_inj t |])) - ((Lazy.force coq_inj_S),[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 + | _ -> explore p t + with e when catchable_exception e -> explore p t in if is_number t' then focused_simpl p else loop p t | Kapp(Pred,[t]) -> - let t_minus_one = - mkApp (Lazy.force coq_minus, [| t; + let t_minus_one = + mkApp (Lazy.force coq_minus, [| t; mkApp (Lazy.force coq_S, [| Lazy.force coq_O |]) |]) in tclTHEN - (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one + (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one ((Lazy.force coq_pred_of_minus),[t])) - (explore p t_minus_one) + (explore p t_minus_one) | Kapp(O,[]) -> focused_simpl p - | _ -> tclIDTAC - with e when catchable_exception e -> tclIDTAC - + | _ -> tclIDTAC + with e when catchable_exception e -> tclIDTAC + and loop = function | [] -> tclIDTAC - | (i,t)::lit -> - begin try match destructurate_prop t with + | (i,t)::lit -> + begin try match destructurate_prop t with Kapp(Le,[t1;t2]) -> tclTHENLIST [ - (generalize_tac + (generalize_tac [mkApp (Lazy.force coq_inj_le, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); (explore [P_APP 2; P_TYPE] t2); @@ -1499,7 +1499,7 @@ let nat_inject gl = ] | Kapp(Lt,[t1;t2]) -> tclTHENLIST [ - (generalize_tac + (generalize_tac [mkApp (Lazy.force coq_inj_lt, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); (explore [P_APP 2; P_TYPE] t2); @@ -1508,7 +1508,7 @@ let nat_inject gl = ] | Kapp(Ge,[t1;t2]) -> tclTHENLIST [ - (generalize_tac + (generalize_tac [mkApp (Lazy.force coq_inj_ge, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); (explore [P_APP 2; P_TYPE] t2); @@ -1536,7 +1536,7 @@ let nat_inject gl = | Kapp(Eq,[typ;t1;t2]) -> if pf_conv_x gl typ (Lazy.force coq_nat) then tclTHENLIST [ - (generalize_tac + (generalize_tac [mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]); (explore [P_APP 2; P_TYPE] t1); (explore [P_APP 3; P_TYPE] t2); @@ -1545,32 +1545,32 @@ let nat_inject gl = ] else loop lit | _ -> loop lit - with e when catchable_exception e -> loop lit end + with e when catchable_exception e -> loop lit end in loop (List.rev (pf_hyps_types gl)) gl - + let rec decidability gl t = match destructurate_prop t with - | Kapp(Or,[t1;t2]) -> + | Kapp(Or,[t1;t2]) -> mkApp (Lazy.force coq_dec_or, [| t1; t2; decidability gl t1; decidability gl t2 |]) - | Kapp(And,[t1;t2]) -> + | Kapp(And,[t1;t2]) -> mkApp (Lazy.force coq_dec_and, [| t1; t2; decidability gl t1; decidability gl t2 |]) - | Kapp(Iff,[t1;t2]) -> + | Kapp(Iff,[t1;t2]) -> mkApp (Lazy.force coq_dec_iff, [| t1; t2; decidability gl t1; decidability gl t2 |]) - | Kimp(t1,t2) -> + | Kimp(t1,t2) -> mkApp (Lazy.force coq_dec_imp, [| t1; t2; decidability gl t1; decidability gl t2 |]) - | Kapp(Not,[t1]) -> mkApp (Lazy.force coq_dec_not, [| t1; + | Kapp(Not,[t1]) -> mkApp (Lazy.force coq_dec_not, [| t1; decidability gl t1 |]) - | Kapp(Eq,[typ;t1;t2]) -> + | Kapp(Eq,[typ;t1;t2]) -> begin match destructurate_type (pf_nf gl typ) with | Kapp(Z,[]) -> mkApp (Lazy.force coq_dec_eq, [| t1;t2 |]) | Kapp(Nat,[]) -> mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |]) - | _ -> errorlabstrm "decidability" - (str "Omega: Can't solve a goal with equality on " ++ + | _ -> errorlabstrm "decidability" + (str "Omega: Can't solve a goal with equality on " ++ Printer.pr_lconstr typ) end | Kapp(Zne,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zne, [| t1;t2 |]) @@ -1584,7 +1584,7 @@ let rec decidability gl t = | Kapp(Gt, [t1;t2]) -> mkApp (Lazy.force coq_dec_gt, [| t1;t2 |]) | Kapp(False,[]) -> Lazy.force coq_dec_False | Kapp(True,[]) -> Lazy.force coq_dec_True - | Kapp(Other t,_::_) -> error + | Kapp(Other t,_::_) -> error ("Omega: Unrecognized predicate or connective: "^t) | Kapp(Other t,[]) -> error ("Omega: Unrecognized atomic proposition: "^t) | Kvar _ -> error "Omega: Can't solve a goal with proposition variables" @@ -1595,7 +1595,7 @@ let onClearedName id tac = (* so renaming may be necessary *) tclTHEN (tclTRY (clear [id])) - (fun gl -> + (fun gl -> let id = fresh_id [] id gl in tclTHEN (introduction id) (tac id) gl) @@ -1607,7 +1607,7 @@ let destructure_hyps gl = | Kapp(False,[]) -> elim_id i | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit | Kapp(Or,[t1;t2]) -> - (tclTHENS + (tclTHENS (elim_id i) [ onClearedName i (fun i -> (loop ((i,None,t1)::lit))); onClearedName i (fun i -> (loop ((i,None,t2)::lit))) ]) @@ -1615,7 +1615,7 @@ let destructure_hyps gl = tclTHENLIST [ (elim_id i); (tclTRY (clear [i])); - (fun gl -> + (fun gl -> let i1 = fresh_id [] (add_suffix i "_left") gl in let i2 = fresh_id [] (add_suffix i "_right") gl in tclTHENLIST [ @@ -1627,7 +1627,7 @@ let destructure_hyps gl = tclTHENLIST [ (elim_id i); (tclTRY (clear [i])); - (fun gl -> + (fun gl -> let i1 = fresh_id [] (add_suffix i "_left") gl in let i2 = fresh_id [] (add_suffix i "_right") gl in tclTHENLIST [ @@ -1661,16 +1661,16 @@ let destructure_hyps gl = ] else loop lit - | Kapp(Not,[t]) -> - begin match destructurate_prop t with - Kapp(Or,[t1;t2]) -> + | Kapp(Not,[t]) -> + begin match destructurate_prop t with + Kapp(Or,[t1;t2]) -> tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]); (onClearedName i (fun i -> (loop ((i,None,mk_and (mk_not t1) (mk_not t2)):: lit)))) ] - | Kapp(And,[t1;t2]) -> + | Kapp(And,[t1;t2]) -> tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_not_and, [| t1; t2; @@ -1690,8 +1690,8 @@ let destructure_hyps gl = ] | Kimp(t1,t2) -> tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_not_imp, [| t1; t2; + (generalize_tac + [mkApp (Lazy.force coq_not_imp, [| t1; t2; decidability gl t1;mkVar i |])]); (onClearedName i (fun i -> (loop ((i,None,mk_and t1 (mk_not t2)) :: lit)))) @@ -1717,7 +1717,7 @@ let destructure_hyps gl = ] | Kapp(Zlt, [t1;t2]) -> tclTHENLIST [ - (generalize_tac + (generalize_tac [mkApp (Lazy.force coq_Znot_lt_ge, [| t1;t2;mkVar i|])]); (onClearedName i (fun _ -> loop lit)) ] @@ -1752,33 +1752,33 @@ let destructure_hyps gl = (onClearedName i (fun _ -> loop lit)) ] | Kapp(Eq,[typ;t1;t2]) -> - if !old_style_flag then begin + if !old_style_flag then begin match destructurate_type (pf_nf gl typ) with - | Kapp(Nat,_) -> + | Kapp(Nat,_) -> tclTHENLIST [ - (simplest_elim + (simplest_elim (mkApp (Lazy.force coq_not_eq, [|t1;t2;mkVar i|]))); (onClearedName i (fun _ -> loop lit)) ] | Kapp(Z,_) -> tclTHENLIST [ - (simplest_elim + (simplest_elim (mkApp (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|]))); (onClearedName i (fun _ -> loop lit)) ] | _ -> loop lit - end else begin + end else begin match destructurate_type (pf_nf gl typ) with - | Kapp(Nat,_) -> - (tclTHEN + | Kapp(Nat,_) -> + (tclTHEN (convert_hyp_no_check (i,body, (mkApp (Lazy.force coq_neq, [| t1;t2|])))) (loop lit)) | Kapp(Z,_) -> - (tclTHEN + (tclTHEN (convert_hyp_no_check (i,body, (mkApp (Lazy.force coq_Zne, [| t1;t2|])))) @@ -1786,10 +1786,10 @@ let destructure_hyps gl = | _ -> loop lit end | _ -> loop lit - end - | _ -> loop lit + end + | _ -> loop lit with e when catchable_exception e -> loop lit - end + end in loop (pf_hyps gl) gl @@ -1798,19 +1798,19 @@ let destructure_goal gl = let rec loop t = match destructurate_prop t with | Kapp(Not,[t]) -> - (tclTHEN - (tclTHEN (unfold sp_not) intro) + (tclTHEN + (tclTHEN (unfold sp_not) intro) destructure_hyps) | Kimp(a,b) -> (tclTHEN intro (loop b)) | Kapp(False,[]) -> destructure_hyps | _ -> - (tclTHEN + (tclTHEN (tclTHEN - (Tactics.refine + (Tactics.refine (mkApp (Lazy.force coq_dec_not_not, [| t; decidability gl t; mkNewMeta () |]))) - intro) - (destructure_hyps)) + intro) + (destructure_hyps)) in (loop concl) gl @@ -1818,7 +1818,7 @@ let destructure_goal = all_time (destructure_goal) let omega_solver gl = Coqlib.check_required_library ["Coq";"omega";"Omega"]; - let result = destructure_goal gl in - (* if !display_time_flag then begin text_time (); + let result = destructure_goal gl in + (* if !display_time_flag then begin text_time (); flush Pervasives.stdout end; *) result diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index a69f8ef74..3bfdce7fd 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -20,16 +20,16 @@ open Coq_omega open Refiner -let omega_tactic l = - let tacs = List.map - (function +let omega_tactic l = + let tacs = List.map + (function | "nat" -> Tacinterp.interp <:tactic<zify_nat>> | "positive" -> Tacinterp.interp <:tactic<zify_positive>> | "N" -> Tacinterp.interp <:tactic<zify_N>> | "Z" -> Tacinterp.interp <:tactic<zify_op>> | s -> Util.error ("No Omega knowledge base for type "^s)) (Util.list_uniquize (List.sort compare l)) - in + in tclTHEN (tclREPEAT (tclPROGRESS (tclTHENLIST tacs))) omega_solver @@ -40,7 +40,7 @@ TACTIC EXTEND omega END TACTIC EXTEND omega' -| [ "omega" "with" ne_ident_list(l) ] -> +| [ "omega" "with" ne_ident_list(l) ] -> [ omega_tactic (List.map Names.string_of_id l) ] | [ "omega" "with" "*" ] -> [ omega_tactic ["nat";"positive";"N";"Z"] ] END diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index fd774c16d..11ab9c039 100644 --- a/plugins/omega/omega.ml +++ b/plugins/omega/omega.ml @@ -85,13 +85,13 @@ type linear = coeff list type eqn_kind = EQUA | INEQ | DISE -type afine = { +type afine = { (* a number uniquely identifying the equation *) - id: int ; + id: int ; (* a boolean true for an eq, false for an ineq (Sigma a_i x_i >= 0) *) - kind: eqn_kind; + kind: eqn_kind; (* the variables and their coefficient *) - body: coeff list; + body: coeff list; (* a constant *) constant: bigint } @@ -108,7 +108,7 @@ type action = | FORGET_C of int | EXACT_DIVIDE of afine * bigint | SUM of int * (bigint * afine) * (bigint * afine) - | STATE of state_action + | STATE of state_action | HYP of afine | FORGET of int * int | FORGET_I of int * int @@ -126,22 +126,22 @@ exception UNSOLVABLE exception NO_CONTRADICTION let display_eq print_var (l,e) = - let _ = - List.fold_left + let _ = + List.fold_left (fun not_first f -> - print_string + print_string (if f.c <? zero then "- " else if not_first then "+ " else ""); let c = abs f.c in - if c =? one then + if c =? one then Printf.printf "%s " (print_var f.v) - else - Printf.printf "%s %s " (string_of_bigint c) (print_var f.v); + else + Printf.printf "%s %s " (string_of_bigint c) (print_var f.v); true) false l in - if e >? zero then + if e >? zero then Printf.printf "+ %s " (string_of_bigint e) - else if e <? zero then + else if e <? zero then Printf.printf "- %s " (string_of_bigint (abs e)) let rec trace_length l = @@ -151,22 +151,22 @@ let rec trace_length l = | _ -> accu + one in List.fold_left action_length zero l -let operator_of_eq = function +let operator_of_eq = function | EQUA -> "=" | DISE -> "!=" | INEQ -> ">=" let kind_of = function | EQUA -> "equation" | DISE -> "disequation" | INEQ -> "inequation" -let display_system print_var l = - List.iter - (fun { kind=b; body=e; constant=c; id=id} -> +let display_system print_var l = + List.iter + (fun { kind=b; body=e; constant=c; id=id} -> Printf.printf "E%d: " id; display_eq print_var (e,c); Printf.printf "%s 0\n" (operator_of_eq b)) l; print_string "------------------------\n\n" -let display_inequations print_var l = +let display_inequations print_var l = List.iter (fun e -> display_eq print_var e;print_string ">= 0\n") l; print_string "------------------------\n\n" @@ -175,7 +175,7 @@ let sbi = string_of_bigint let rec display_action print_var = function | act :: l -> begin match act with | DIVIDE_AND_APPROX (e1,e2,k,d) -> - Printf.printf + Printf.printf "Inequation E%d is divided by %s and the constant coefficient is \ rounded by substracting %s.\n" e1.id (sbi k) (sbi d) | NOT_EXACT_DIVIDE (e,k) -> @@ -187,28 +187,28 @@ let rec display_action print_var = function "Equation E%d is divided by the pgcd \ %s of its coefficients.\n" e.id (sbi k) | WEAKEN (e,k) -> - Printf.printf + Printf.printf "To ensure a solution in the dark shadow \ the equation E%d is weakened by %s.\n" e (sbi k) - | SUM (e,(c1,e1),(c2,e2)) -> + | SUM (e,(c1,e1),(c2,e2)) -> Printf.printf - "We state %s E%d = %s %s E%d + %s %s E%d.\n" + "We state %s E%d = %s %s E%d + %s %s E%d.\n" (kind_of e1.kind) e (sbi c1) (kind_of e1.kind) e1.id (sbi c2) (kind_of e2.kind) e2.id | STATE { st_new_eq = e } -> - Printf.printf "We define a new equation E%d: " e.id; - display_eq print_var (e.body,e.constant); + Printf.printf "We define a new equation E%d: " e.id; + display_eq print_var (e.body,e.constant); print_string (operator_of_eq e.kind); print_string " 0" - | HYP e -> - Printf.printf "We define E%d: " e.id; - display_eq print_var (e.body,e.constant); + | HYP e -> + Printf.printf "We define E%d: " e.id; + display_eq print_var (e.body,e.constant); print_string (operator_of_eq e.kind); print_string " 0\n" | FORGET_C e -> Printf.printf "E%d is trivially satisfiable.\n" e | FORGET (e1,e2) -> Printf.printf "E%d subsumes E%d.\n" e1 e2 | FORGET_I (e1,e2) -> Printf.printf "E%d subsumes E%d.\n" e1 e2 | MERGE_EQ (e,e1,e2) -> Printf.printf "E%d and E%d can be merged into E%d.\n" e1.id e2 e - | CONTRADICTION (e1,e2) -> + | CONTRADICTION (e1,e2) -> Printf.printf "Equations E%d and E%d imply a contradiction on their \ constant factors.\n" e1.id e2.id @@ -216,20 +216,20 @@ let rec display_action print_var = function Printf.printf "Equations E%d and E%d state that their body is at the same time equal and different\n" e1.id e2.id - | CONSTANT_NOT_NUL (e,k) -> + | CONSTANT_NOT_NUL (e,k) -> Printf.printf "Equation E%d states %s = 0.\n" e (sbi k) - | CONSTANT_NEG(e,k) -> + | CONSTANT_NEG(e,k) -> Printf.printf "Equation E%d states %s >= 0.\n" e (sbi k) | CONSTANT_NUL e -> Printf.printf "Inequation E%d states 0 != 0.\n" e - | SPLIT_INEQ (e,(e1,l1),(e2,l2)) -> + | SPLIT_INEQ (e,(e1,l1),(e2,l2)) -> Printf.printf "Equation E%d is split in E%d and E%d\n\n" e.id e1 e2; display_action print_var l1; print_newline (); display_action print_var l2; print_newline () end; display_action print_var l - | [] -> + | [] -> flush stdout let default_print_var v = Printf.sprintf "X%d" v (* For debugging *) @@ -245,38 +245,38 @@ 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 map_eq_linear f = let rec loop = function | x :: l -> let c = f x.c in if c=?zero then loop l else {v=x.v; c=c} :: loop l - | [] -> [] + | [] -> [] in loop -let map_eq_afine f e = - { id = e.id; kind = e.kind; body = map_eq_linear f e.body; +let map_eq_afine f e = + { id = e.id; kind = e.kind; body = map_eq_linear f e.body; constant = f e.constant } let negate_eq = map_eq_afine (fun x -> neg x) -let rec sum p0 p1 = match (p0,p1) with +let rec sum p0 p1 = match (p0,p1) with | ([], l) -> l | (l, []) -> l - | (((x1::l1) as l1'), ((x2::l2) as l2')) -> + | (((x1::l1) as l1'), ((x2::l2) as l2')) -> if x1.v = x2.v then let c = x1.c + x2.c in if c =? zero then sum l1 l2 else {v=x1.v;c=c} :: sum l1 l2 - else if x1.v > x2.v then + else if x1.v > x2.v then x1 :: sum l1 l2' - else + else x2 :: sum l1' l2 -let sum_afine new_eq_id eq1 eq2 = +let sum_afine new_eq_id eq1 eq2 = { kind = eq1.kind; id = new_eq_id (); body = sum eq1.body eq2.body; constant = eq1.constant + eq2.constant } exception FACTOR1 let rec chop_factor_1 = function - | x :: l -> + | x :: l -> if abs x.c =? one then x,l else let (c',l') = chop_factor_1 l in (c',x::l') | [] -> raise FACTOR1 @@ -287,7 +287,7 @@ let rec chop_var v = function | [] -> raise CHOPVAR let normalize ({id=id; kind=eq_flag; body=e; constant =x} as eq) = - if e = [] then begin + if e = [] then begin match eq_flag with | EQUA -> if x =? zero then [] else begin @@ -310,7 +310,7 @@ let normalize ({id=id; kind=eq_flag; body=e; constant =x} as eq) = end else if gcd <> one then begin let c = floor_div x gcd in let d = x - c * gcd in - let new_eq = {id=id; kind=eq_flag; constant=c; + let new_eq = {id=id; kind=eq_flag; constant=c; body=map_eq_linear (fun c -> c / gcd) e} in add_event (if eq_flag=EQUA or eq_flag = DISE then EXACT_DIVIDE(eq,gcd) else DIVIDE_AND_APPROX(eq,new_eq,gcd,d)); @@ -320,15 +320,15 @@ let normalize ({id=id; kind=eq_flag; body=e; constant =x} as eq) = let eliminate_with_in new_eq_id {v=v;c=c_unite} eq2 ({body=e1; constant=c1} as eq1) = try - let (f,_) = chop_var v e1 in - let coeff = if c_unite=?one then neg f.c else if c_unite=? negone then f.c + let (f,_) = chop_var v e1 in + let coeff = if c_unite=?one then neg f.c else if c_unite=? negone then f.c else failwith "eliminate_with_in" in let res = sum_afine new_eq_id eq1 (map_eq_afine (fun c -> c * coeff) eq2) in add_event (SUM (res.id,(one,eq1),(coeff,eq2))); res with CHOPVAR -> eq1 let omega_mod a b = a - b * floor_div (two * a + b) (two * b) -let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 = +let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 = let e = original.body in let sigma = new_var_id () in let smallest,var = @@ -339,7 +339,7 @@ let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 = let m = smallest + one in let new_eq = { constant = omega_mod original.constant m; - body = {c= neg m;v=sigma} :: + body = {c= neg m;v=sigma} :: map_eq_linear (fun a -> omega_mod a m) original.body; id = new_eq_id (); kind = EQUA } in let definition = @@ -351,11 +351,11 @@ let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 = st_orig = original; st_coef = m; st_var = sigma}); let new_eq = List.hd (normalize new_eq) in let eliminated_var, def = chop_var var new_eq.body in - let other_equations = + let other_equations = Util.list_map_append - (fun e -> + (fun e -> normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) l1 in - let inequations = + let inequations = Util.list_map_append (fun e -> normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) l2 in @@ -364,7 +364,7 @@ let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 = add_event (EXACT_DIVIDE (original',m)); List.hd (normalize mod_original),other_equations,inequations -let rec eliminate_one_equation ((new_eq_id,new_var_id,print_var) as new_ids) (e,other,ineqs) = +let rec eliminate_one_equation ((new_eq_id,new_var_id,print_var) as new_ids) (e,other,ineqs) = if !debug then display_system print_var (e::other); try let v,def = chop_factor_1 e.body in @@ -377,22 +377,22 @@ let rec eliminate_one_equation ((new_eq_id,new_var_id,print_var) as new_ids) (e, let rec banerjee ((_,_,print_var) as new_ids) (sys_eq,sys_ineq) = let rec fst_eq_1 = function - (eq::l) -> + (eq::l) -> if List.exists (fun x -> abs x.c =? one) eq.body then eq,l else let (eq',l') = fst_eq_1 l in (eq',eq::l') | [] -> raise Not_found in match sys_eq with [] -> if !debug then display_system print_var sys_ineq; sys_ineq - | (e1::rest) -> + | (e1::rest) -> let eq,other = try fst_eq_1 sys_eq with Not_found -> (e1,rest) in - if eq.body = [] then + if eq.body = [] then if eq.constant =? zero then begin add_event (FORGET_C eq.id); banerjee new_ids (other,sys_ineq) end else begin add_event (CONSTANT_NOT_NUL(eq.id,eq.constant)); raise UNSOLVABLE end else - banerjee new_ids + banerjee new_ids (eliminate_one_equation new_ids (eq,other,sys_ineq)) type kind = INVERTED | NORMAL @@ -403,37 +403,37 @@ let redundancy_elimination new_eq_id system = | e -> e,NORMAL in let table = Hashtbl.create 7 in List.iter - (fun e -> + (fun e -> let ({body=ne} as nx) ,kind = normal e in if ne = [] then if nx.constant <? zero then begin add_event (CONSTANT_NEG(nx.id,nx.constant)); raise UNSOLVABLE end else add_event (FORGET_C nx.id) else - try + try let (optnormal,optinvert) = Hashtbl.find table ne in let final = if kind = NORMAL then begin - match optnormal with - Some v -> + match optnormal with + Some v -> let kept = - if v.constant <? nx.constant + 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 + match optinvert with Some v -> let _kept = - if v.constant >? nx.constant + 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) -> + (Some high, Some low) -> if high.constant <? low.constant then begin add_event(CONTRADICTION (high,negate_eq low)); raise UNSOLVABLE @@ -442,21 +442,21 @@ let redundancy_elimination new_eq_id system = Hashtbl.remove table ne; Hashtbl.add table ne final with Not_found -> - Hashtbl.add table ne + Hashtbl.add table ne (if kind = NORMAL then (Some nx,None) else (None,Some nx))) system; let accu_eq = ref [] in let accu_ineq = ref [] in Hashtbl.iter - (fun p0 p1 -> match (p0,p1) with + (fun p0 p1 -> match (p0,p1) with | (e, (Some x, Some y)) when x.constant =? y.constant -> let id=new_eq_id () in add_event (MERGE_EQ(id,x,y.id)); push {id=id; kind=EQUA; body=x.body; constant=x.constant} accu_eq | (e, (optnorm,optinvert)) -> - begin match optnorm with + begin match optnorm with Some x -> push x accu_ineq | _ -> () end; - begin match optinvert with + begin match optinvert with Some x -> push (negate_eq x) accu_ineq | _ -> () end) table; !accu_eq,!accu_ineq @@ -465,7 +465,7 @@ exception SOLVED_SYSTEM let select_variable system = let table = Hashtbl.create 7 in - let push v c= + let push v c= try let r = Hashtbl.find table v in r := max !r (abs c) with Not_found -> Hashtbl.add table v (ref (abs c)) in List.iter (fun {body=l} -> List.iter (fun f -> push f.v f.c) l) system; @@ -480,7 +480,7 @@ let select_variable system = !vmin let classify v system = - List.fold_left + List.fold_left (fun (not_occ,below,over) eq -> try let f,eq' = chop_var v eq.body in if f.c >=? zero then (not_occ,((f.c,eq) :: below),over) @@ -493,18 +493,18 @@ let product new_eq_id dark_shadow low high = (fun accu (a,eq1) -> List.fold_left (fun accu (b,eq2) -> - let eq = + let eq = sum_afine new_eq_id (map_eq_afine (fun c -> c * b) eq1) (map_eq_afine (fun c -> c * a) eq2) in add_event(SUM(eq.id,(b,eq1),(a,eq2))); match normalize eq with | [eq] -> let final_eq = - if dark_shadow then + if dark_shadow then let delta = (a - one) * (b - one) in add_event(WEAKEN(eq.id,delta)); - {id = eq.id; kind=INEQ; body = eq.body; - constant = eq.constant - delta} + {id = eq.id; kind=INEQ; body = eq.body; + constant = eq.constant - delta} else eq in final_eq :: accu | (e::_) -> failwith "Product dardk" @@ -519,7 +519,7 @@ let fourier_motzkin (new_eq_id,_,print_var) dark_shadow system = if !debug then display_system print_var expanded; expanded let simplify ((new_eq_id,new_var_id,print_var) as new_ids) dark_shadow system = - if List.exists (fun e -> e.kind = DISE) system then + 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; @@ -528,23 +528,23 @@ let simplify ((new_eq_id,new_var_id,print_var) as new_ids) dark_shadow system = let simp_eq,simp_ineq = redundancy_elimination new_eq_id ineqs in let system = (eqs @ simp_eq,simp_ineq) in let rec loop1a system = - let sys_ineq = banerjee new_ids system in - loop1b sys_ineq + let sys_ineq = banerjee new_ids system in + loop1b sys_ineq and loop1b sys_ineq = let simp_eq,simp_ineq = redundancy_elimination new_eq_id sys_ineq in - if simp_eq = [] then simp_ineq else loop1a (simp_eq,simp_ineq) + if simp_eq = [] then simp_ineq else loop1a (simp_eq,simp_ineq) in let rec loop2 system = try let expanded = fourier_motzkin new_ids dark_shadow system in loop2 (loop1b expanded) with SOLVED_SYSTEM -> - if !debug then display_system print_var system; system + if !debug then display_system print_var system; system in loop2 (loop1a system) let rec depend relie_on accu = function - | act :: l -> + | act :: l -> begin match act with | DIVIDE_AND_APPROX (e,_,_,_) -> if List.mem e.id relie_on then depend relie_on (act::accu) l @@ -555,40 +555,40 @@ let rec depend relie_on accu = function | 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 + | SUM (e,(_,e1),(_,e2)) -> + if List.mem e relie_on then depend (e1.id::e2.id::relie_on) (act::accu) l - else + else depend relie_on accu l | STATE {st_new_eq=e;st_orig=o} -> if List.mem e.id relie_on then depend (o.id::relie_on) (act::accu) l else depend relie_on accu l - | HYP e -> + | 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 + if List.mem e relie_on then depend (e1.id::e2::relie_on) (act::accu) l - else + else depend relie_on accu l | NOT_EXACT_DIVIDE (e,_) -> depend (e.id::relie_on) (act::accu) l - | CONTRADICTION (e1,e2) -> + | 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,_) -> + | NEGATE_CONTRADICT (e1,e2,_) -> depend (e1.id::e2.id::relie_on) (act::accu) l | SPLIT_INEQ _ -> failwith "depend" end | [] -> relie_on, accu (* -let depend relie_on accu trace = - Printf.printf "Longueur de la trace initiale : %d\n" +let depend relie_on accu trace = + Printf.printf "Longueur de la trace initiale : %d\n" (trace_length trace + trace_length accu); let rel',trace' = depend relie_on accu trace in Printf.printf "Longueur de la trace simplifiée : %d\n" (trace_length trace'); @@ -598,20 +598,20 @@ let depend relie_on accu trace = let solve (new_eq_id,new_eq_var,print_var) system = try let _ = simplify new_eq_id false system in failwith "no contradiction" with UNSOLVABLE -> display_action print_var (snd (depend [] [] (history ()))) - + let negation (eqs,ineqs) = let diseq,_ = List.partition (fun e -> e.kind = DISE) ineqs in let normal = function | ({body=f::_} as e) when f.c <? zero -> negate_eq e, INVERTED | e -> e,NORMAL in let table = Hashtbl.create 7 in - List.iter (fun e -> + List.iter (fun e -> let {body=ne;constant=c} ,kind = normal e in Hashtbl.add table (ne,c) (kind,e)) diseq; List.iter (fun e -> assert (e.kind = EQUA); let {body=ne;constant=c},kind = normal e in - try + try let (kind',e') = Hashtbl.find table (ne,c) in add_event (NEGATE_CONTRADICT (e,e',kind=kind')); raise UNSOLVABLE @@ -625,39 +625,39 @@ let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system = (* Initial simplification phase *) let rec loop1a system = negation system; - let sys_ineq = banerjee new_ids system in - loop1b sys_ineq + let sys_ineq = banerjee new_ids system in + loop1b sys_ineq and loop1b sys_ineq = let dise,ine = List.partition (fun e -> e.kind = DISE) sys_ineq in let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in if simp_eq = [] then dise @ simp_ineq - else loop1a (simp_eq,dise @ simp_ineq) + else loop1a (simp_eq,dise @ simp_ineq) in let rec loop2 system = try let expanded = fourier_motzkin new_ids false system in loop2 (loop1b expanded) - with SOLVED_SYSTEM -> if !debug then display_system print_var system; system + with SOLVED_SYSTEM -> if !debug then display_system print_var system; system in - let rec explode_diseq = function + let rec explode_diseq = function | (de::diseq,ineqs,expl_map) -> - let id1 = new_eq_id () + let id1 = new_eq_id () and id2 = new_eq_id () in - let e1 = + let e1 = {id = id1; kind=INEQ; body = de.body; constant = de.constant -one} in - let e2 = - {id = id2; kind=INEQ; body = map_eq_linear neg de.body; + let e2 = + {id = id2; kind=INEQ; body = map_eq_linear neg de.body; constant = neg de.constant - one} in let new_sys = - List.map (fun (what,sys) -> ((de.id,id1,true)::what, e1::sys)) - ineqs @ - List.map (fun (what,sys) -> ((de.id,id2,false)::what,e2::sys)) - ineqs + 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 + | ([],ineqs,expl_map) -> ineqs,expl_map in - try + try let system = Util.list_map_append normalize system in let eqs,ineqs = List.partition (fun e -> e.kind=EQUA) system in let dise,ine = List.partition (fun e -> e.kind = DISE) ineqs in @@ -669,45 +669,45 @@ let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system = let sys_exploded,explode_map = explode_diseq (diseq,[[],ineq],[]) in let all_solutions = List.map - (fun (decomp,sys) -> + (fun (decomp,sys) -> clear_history (); try let _ = loop2 sys in raise NO_CONTRADICTION - with UNSOLVABLE -> + with UNSOLVABLE -> let relie_on,path = depend [] [] (history ()) in let dc,_ = List.partition (fun (_,id,_) -> List.mem id relie_on) decomp in let red = List.map (fun (x,_,_) -> x) dc in (red,relie_on,decomp,path)) - sys_exploded + sys_exploded in - let max_count sys = + let max_count sys = let tbl = Hashtbl.create 7 in - let augment x = - try incr (Hashtbl.find tbl x) + let augment x = + try incr (Hashtbl.find tbl x) with Not_found -> Hashtbl.add tbl x (ref 1) in let eq = ref (-1) and c = ref 0 in - List.iter (function + List.iter (function | ([],r_on,_,path) -> raise (FULL_SOLUTION (path,r_on)) | (l,_,_,_) -> List.iter augment l) sys; Hashtbl.iter (fun x v -> if !v > !c then begin eq := x; c := !v end) tbl; - !eq + !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 + let rec solve systems = + try + let id = max_count systems in + let rec sign = function + | ((id',_,b)::l) -> if id=id' then b else sign l | [] -> failwith "solve" in let s1,s2 = List.partition (fun (_,_,decomp,_) -> sign decomp) systems in - let s1' = + let s1' = List.map (fun (dep,ro,dc,pa) -> (Util.list_except id dep,ro,dc,pa)) s1 in - let s2' = + let s2' = List.map (fun (dep,ro,dc,pa) -> (Util.list_except id dep,ro,dc,pa)) s2 in - let (r1,relie1) = solve s1' + let (r1,relie1) = solve s1' and (r2,relie2) = solve s2' in let (eq,id1,id2) = List.assoc id explode_map in [SPLIT_INEQ(eq,(id1,r1),(id2, r2))], eq.id :: Util.list_union relie1 relie2 - with FULL_SOLUTION (x0,x1) -> (x0,x1) + with FULL_SOLUTION (x0,x1) -> (x0,x1) in let act,relie_on = solve all_solutions in snd(depend relie_on act first_segment) |