Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg

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