summaryrefslogtreecommitdiff
path: root/contrib/romega
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-08-18 20:34:57 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-08-18 20:34:57 +0000
commit72b9a7df489ea47b3e5470741fd39f6100d31676 (patch)
tree60108a573d2a80d2dd4e3833649890e32427ff8d /contrib/romega
parent55ce117e8083477593cf1ff2e51a3641c7973830 (diff)
Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg
Diffstat (limited to 'contrib/romega')
-rw-r--r--contrib/romega/ReflOmegaCore.v33
-rw-r--r--contrib/romega/refl_omega.ml51
2 files changed, 62 insertions, 22 deletions
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