From 72b9a7df489ea47b3e5470741fd39f6100d31676 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Sat, 18 Aug 2007 20:34:57 +0000 Subject: Imported Upstream version 8.1.pl1+dfsg --- contrib/romega/ReflOmegaCore.v | 33 ++++++++++++++++++--------- contrib/romega/refl_omega.ml | 51 ++++++++++++++++++++++++++++++++---------- 2 files changed, 62 insertions(+), 22 deletions(-) (limited to 'contrib/romega') diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v index 83ea5b63..d20cafc1 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 285fc0ca..e7e7b3c5 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 -- cgit v1.2.3