diff options
| -rw-r--r-- | contrib/omega/coq_omega.ml | 4 | ||||
| -rw-r--r-- | contrib/romega/ReflOmegaCore.v | 33 | ||||
| -rw-r--r-- | contrib/romega/refl_omega.ml | 51 | ||||
| -rw-r--r-- | test-suite/success/Omega0.v | 8 | ||||
| -rw-r--r-- | test-suite/success/ROmega.v | 14 | ||||
| -rw-r--r-- | test-suite/success/ROmega0.v | 35 | ||||
| -rw-r--r-- | test-suite/success/ROmega2.v | 19 |
7 files changed, 112 insertions, 52 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 497fcdb6cb..aa59daf5fa 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -300,6 +300,7 @@ let coq_eq_ind_r = lazy (constant "eq_ind_r") let coq_dec_or = lazy (constant "dec_or") let coq_dec_and = lazy (constant "dec_and") let coq_dec_imp = lazy (constant "dec_imp") +let coq_dec_iff = lazy (constant "dec_iff") let coq_dec_not = lazy (constant "dec_not") let coq_dec_False = lazy (constant "dec_False") let coq_dec_not_not = lazy (constant "dec_not_not") @@ -310,6 +311,7 @@ let coq_not_and = lazy (constant "not_and") let coq_not_imp = lazy (constant "not_imp") let coq_not_not = lazy (constant "not_not") let coq_imp_simp = lazy (constant "imp_simp") +let coq_iff = lazy (constant "iff") (* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *) @@ -386,6 +388,8 @@ let destructurate_prop t = | _, [_;_] when c = Lazy.force coq_Zgt -> Kapp (Zgt,args) | _, [_;_] when c = build_coq_and () -> Kapp (And,args) | _, [_;_] when c = build_coq_or () -> Kapp (Or,args) + | _, [t1;t2] when c = Lazy.force coq_iff -> + Kapp (And,[mkArrow t1 t2;mkArrow t2 t1]) | _, [_] when c = build_coq_not () -> Kapp (Not,args) | _, [] when c = build_coq_False () -> Kapp (False,args) | _, [] when c = build_coq_True () -> Kapp (True,args) diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v index 5583ce4c90..fda18c6cef 100644 --- a/contrib/romega/ReflOmegaCore.v +++ b/contrib/romega/ReflOmegaCore.v @@ -1848,6 +1848,15 @@ Definition exact_divide (k : Z) (body : term) (t : nat) end | false => TrueTerm end + | NeqTerm (Tint Z0) b => + match eq_term (scalar_norm t (body * Tint k)%term) b with + | true => + match eq_Z k 0 with + | true => FalseTerm + | false => NeqTerm (Tint 0) body + end + | false => TrueTerm + end | _ => TrueTerm end. @@ -1858,18 +1867,24 @@ Theorem exact_divide_valid : unfold valid1, exact_divide in |- *; intros k1 k2 t ep e p1; Simplify; simpl in |- *; auto; elim_eq_term (scalar_norm t (k2 * Tint k1)%term) t1; simpl in |- *; auto; elim_eq_Z k1 0; simpl in |- *; - auto; intros H1 H2; elim H2; elim scalar_norm_stable; - simpl in |- *; generalize H1; case (interp_term e k2); + auto; intros H1 H2; elim H2; elim scalar_norm_stable; + simpl in |- *; + [ + generalize H1; case (interp_term e k2); try trivial; (case k1; simpl in |- *; [ intros; absurd (0 = 0); assumption | intros p2 p3 H3 H4; discriminate H4 - | intros p2 p3 H3 H4; discriminate H4 ]). - + | intros p2 p3 H3 H4; discriminate H4 ]) + | + subst k1; rewrite Zmult_comm; simpl in *; intros; absurd (0=0); trivial + | + generalize H1; case (interp_term e k2); + try trivial; intros p2 p3 H3 H4; discriminate H4 + ]. Qed. - (* \paragraph{[O_DIV_APPROX]} La preuve reprend le schéma de la précédente mais on est sur une opération de type valid1 et non sur une opération terminale. *) @@ -1954,7 +1969,7 @@ Definition state (m : Z) (s : step) (prop1 prop2 : proposition) := match prop1 with | EqTerm (Tint Z0) b1 => match prop2 with - | EqTerm (Tint Z0) (b2 + - b3)%term => + | EqTerm b2 b3 => EqTerm (Tint 0) (rewrite s (b1 + (- b3 + b2) * Tint m)%term) | _ => TrueTerm end @@ -1965,10 +1980,8 @@ Theorem state_valid : forall (m : Z) (s : step), valid2 (state m s). unfold valid2 in |- *; intros m s ep e p1 p2; unfold state in |- *; Simplify; simpl in |- *; auto; elim (rewrite_stable s e); simpl in |- *; - intros H1 H2; elim H1; - rewrite (Zplus_comm (- interp_term e t5) (interp_term e t3)); - elim H2; simpl in |- *; reflexivity. - + intros H1 H2; elim H1. + rewrite H2; rewrite Zplus_opp_l; simpl; reflexivity. Qed. (* \subsubsection{Tactiques générant plusieurs but} diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml index 285fc0ca8c..e7e7b3c590 100644 --- a/contrib/romega/refl_omega.ml +++ b/contrib/romega/refl_omega.ml @@ -6,6 +6,10 @@ *************************************************************************) +(* The addition on int, since it while be hidden soon by the one on BigInt *) + +let (+.) = (+) + open Const_omega module OmegaSolver = Omega.MakeOmegaSolver (Bigint) open OmegaSolver @@ -792,6 +796,9 @@ and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c = | Kimp(t1,t2) -> binprop env ctxt (not negated) (not negated) gl (fun i x y -> Pimp(i,x,y)) t1 t2 + | Kapp("iff",[t1;t2]) -> + binprop env ctxt negated negated gl + (fun i x y -> Pand(i,x,y)) (Term.mkArrow t1 t2) (Term.mkArrow t2 t1) | _ -> Pprop c with e when Logic.catchable_exception e -> Pprop c @@ -995,10 +1002,10 @@ let rec equas_of_solution_tree = function list_union (equas_of_solution_tree t1) (equas_of_solution_tree t2) | Leaf s -> s.s_equa_deps - -(* Because of really_useful_prop, decidable formulas such as Pfalse - and Ptrue are moved to Pprop, thus breaking the decidability check - in ReflOmegaCore.concl_to_hyp... *) +(* [really_useful_prop] pushes useless props in a new Pprop variable *) +(* Things get shorter, but may also get wrong, since a Prop is considered + to be undecidable in ReflOmegaCore.concl_to_hyp, whereas for instance + Pfalse is decidable. So should not be used on conclusion (??) *) let really_useful_prop l_equa c = let rec real_of = function @@ -1034,6 +1041,14 @@ let really_useful_prop l_equa c = None -> Pprop (real_of c) | Some t -> t +let rec vars_of_prop = function + | Pequa(_,e) -> vars_of_equations [e] + | Pnot p -> vars_of_prop p + | Por(_,p1,p2) -> list_union (vars_of_prop p1) (vars_of_prop p2) + | Pand(_,p1,p2) -> list_union (vars_of_prop p1) (vars_of_prop p2) + | Pimp(_,p1,p2) -> list_union (vars_of_prop p1) (vars_of_prop p2) + | _ -> [] + let rec display_solution_tree ch = function Leaf t -> output_string ch @@ -1160,10 +1175,15 @@ let replay_history env env_hyp = | CONSTANT_NUL e :: l -> mkApp (Lazy.force coq_s_constant_nul, [| mk_nat (get_hyp env_hyp e) |]) - | NEGATE_CONTRADICT(e1,e2,b) :: l -> + | NEGATE_CONTRADICT(e1,e2,true) :: l -> mkApp (Lazy.force coq_s_negate_contradict, [| mk_nat (get_hyp env_hyp e1.id); mk_nat (get_hyp env_hyp e2.id) |]) + | NEGATE_CONTRADICT(e1,e2,false) :: l -> + mkApp (Lazy.force coq_s_negate_contradict_inv, + [| mk_nat (List.length e2.body); + mk_nat (get_hyp env_hyp e1.id); + mk_nat (get_hyp env_hyp e2.id) |]) | SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: l -> let i = get_hyp env_hyp e.id in let r1 = loop (CCEqua e1 :: env_hyp) l1 in @@ -1254,14 +1274,18 @@ let resolution env full_reified_goal systems_list = let l_hyps = id_concl :: list_remove id_concl l_hyps' in let useful_hyps = List.map (fun id -> List.assoc id full_reified_goal) l_hyps in - let useful_vars = vars_of_equations equations in + let useful_vars = + let really_useful_vars = vars_of_equations equations in + let concl_vars = vars_of_prop (List.assoc id_concl full_reified_goal) in + list_uniq (List.sort compare (really_useful_vars @ concl_vars)) + in (* variables a introduire *) let to_introduce = add_stated_equations env solution_tree in let stated_vars = List.map (fun (v,_,_,_) -> v) to_introduce in let l_generalize_arg = List.map (fun (_,t,_,_) -> t) to_introduce in let hyp_stated_vars = List.map (fun (_,_,_,id) -> CCEqua id) to_introduce in (* L'environnement de base se construit en deux morceaux : - - les variables des équations utiles + - les variables des équations utiles (et de la conclusion) - les nouvelles variables declarées durant les preuves *) let all_vars_env = useful_vars @ stated_vars in let basic_env = @@ -1280,8 +1304,7 @@ let resolution env full_reified_goal systems_list = to_introduce in let reified_concl = match useful_hyps with - (Pnot p) :: _ -> - reified_of_proposition env (really_useful_prop useful_equa_id p) + (Pnot p) :: _ -> reified_of_proposition env p | _ -> reified_of_proposition env Pfalse in let l_reified_terms = (List.map @@ -1301,9 +1324,13 @@ let resolution env full_reified_goal systems_list = [| e.e_trace |] | ((O_left | O_mono) :: l) -> app coq_p_left [| loop l |] | (O_right :: l) -> app coq_p_right [| loop l |] in - app coq_pair_step - [| mk_nat (list_index e.e_origin.o_hyp l_hyps) ; - loop e.e_origin.o_path |] in + let correct_index = + let i = list_index e.e_origin.o_hyp l_hyps in + (* PL: it seems that additionnally introduced hyps are in the way during + normalization, hence this index shifting... *) + if i=0 then 0 else i +. List.length to_introduce + in + app coq_pair_step [| mk_nat correct_index; loop e.e_origin.o_path |] in let normalization_trace = mk_list (Lazy.force coq_h_step) (List.map normalize_equation equations) in diff --git a/test-suite/success/Omega0.v b/test-suite/success/Omega0.v index 4614c90db0..accaec41ed 100644 --- a/test-suite/success/Omega0.v +++ b/test-suite/success/Omega0.v @@ -8,16 +8,16 @@ Lemma test_romega_0 : 0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'. Proof. intros. -(*omega.*) -Admitted. +omega. +Qed. Lemma test_romega_0b : forall m m', 0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'. Proof. intros m m'. -(*omega.*) -Admitted. +omega. +Qed. Lemma test_romega_1 : forall (z z1 z2 : Z), diff --git a/test-suite/success/ROmega.v b/test-suite/success/ROmega.v index 04b666edd3..ff1f57df32 100644 --- a/test-suite/success/ROmega.v +++ b/test-suite/success/ROmega.v @@ -7,8 +7,8 @@ Lemma lem1 : forall x y : Z, (-5 < x < 5)%Z -> (-5 < y)%Z -> (-5 < x + y + 5)%Z. Proof. intros x y. - (*romega.*) -Admitted. +romega. +Qed. (* Proposed by Pierre Crégut *) @@ -22,8 +22,8 @@ Qed. Lemma lem3 : forall x y : Z, x = y -> (x + x)%Z = (y + y)%Z. Proof. intros. - (*romega.*) -Admitted. +romega. +Qed. (* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *) (* internal variable and a section variable (June 2001) *) @@ -68,7 +68,7 @@ Variable n : nat. Variable ap_n : n <> 0. Let delta := f n ap_n. Lemma lem7 : n = n. - (*romega.*) (*ROMEGA CANT DEAL WITH NAT*) + (*romega. ---> ROMEGA CANT DEAL WITH NAT*) Admitted. End C. @@ -76,7 +76,7 @@ End C. Require Import Omega. Lemma lem8 : forall H : 0 = 0 -> 0 = 0, H = H -> 0 = 0. intros. -(* romega.*) (*ROMEGA CANT DEAL WITH NAT*) +(* romega. ---> ROMEGA CANT DEAL WITH NAT*) Admitted. (* Bug that what caused by the use of intro_using in Omega *) @@ -84,7 +84,7 @@ Require Import Omega. Lemma lem9 : forall p q : nat, ~ (p <= q /\ p < q \/ q <= p /\ p < q) -> p < p \/ p <= p. intros. -(* romega.*)(*ROMEGA CANT DEAL WITH NAT*) +(* romega. ---> ROMEGA CANT DEAL WITH NAT*) Admitted. (* Check that the interpretation of mult on nat enforces its positivity *) diff --git a/test-suite/success/ROmega0.v b/test-suite/success/ROmega0.v index 0efca1e13f..86cf49cb5e 100644 --- a/test-suite/success/ROmega0.v +++ b/test-suite/success/ROmega0.v @@ -8,16 +8,16 @@ Lemma test_romega_0 : 0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'. Proof. intros. -(*romega.*) -Admitted. +romega. +Qed. Lemma test_romega_0b : forall m m', 0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'. Proof. intros m m'. -(*romega.*) -Admitted. +romega. +Qed. Lemma test_romega_1 : forall (z z1 z2 : Z), @@ -42,8 +42,8 @@ Lemma test_romega_1b : z >= 0. Proof. intros z z1 z2. -(* romega. *) -Admitted. +romega. +Qed. Lemma test_romega_2 : forall a b c:Z, 0<=a-b<=1 -> b-c<=2 -> a-c<=3. @@ -56,8 +56,8 @@ Lemma test_romega_2b : forall a b c:Z, 0<=a-b<=1 -> b-c<=2 -> a-c<=3. Proof. intros a b c. -(*romega.*) -Admitted. +romega. +Qed. Lemma test_romega_3 : forall a b h hl hr ha hb, 0 <= ha - hl <= 1 -> @@ -115,22 +115,22 @@ Qed. Lemma test_romega_6b : forall z, z>=0 -> 0>z+2 -> False. Proof. intros z. -(*romega. *) -Admitted. +romega. +Qed. Lemma test_romega_7 : forall z, 0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1. Proof. intros. -(*romega.*) -Admitted. +romega. +Qed. Lemma test_romega_7b : forall z, 0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1. Proof. intros. -(*romega.*) -Admitted. +romega. +Qed. (* Magaud #240 *) @@ -144,6 +144,9 @@ intros x y. romega. Qed. +(* Besson #1298 *) - - +Lemma test_romega9 : forall z z':Z, z<>z' -> z'=z -> False. +intros. +romega. +Qed. diff --git a/test-suite/success/ROmega2.v b/test-suite/success/ROmega2.v index 9d47c9f654..a3be2898c1 100644 --- a/test-suite/success/ROmega2.v +++ b/test-suite/success/ROmega2.v @@ -4,6 +4,20 @@ Require Import ZArith ROmega. Open Scope Z_scope. + +(* First a simplified version used during debug of romega on Test46 *) +Lemma Test46_simplified : +forall v1 v2 v5 : Z, +0 = v2 + v5 -> +0 < v5 -> +0 < v2 -> +4*v2 <> 5*v1. +intros. +romega. +Qed. + + +(* The complete problem *) Lemma Test46 : forall v1 v2 v3 v4 v5 : Z, ((2 * v4) + (5)) + (8 * v2) <= ((4 * v4) + (3 * v4)) + (5 * v4) -> @@ -23,6 +37,5 @@ forall v1 v2 v3 v4 v5 : Z, ((7 * v1) + (1 * v3)) + ((2 * v3) + (1 * v3)) >= ((6 * v5) + (4)) + ((1) + (9)) -> False. intros. -(*romega.*) -Admitted. - +romega. +Qed. |