Omega now aware of context variables with bodies (in type Z or nat) (fix bug 148)

 For compatibility, this extra feature of omega could be disabled via
  Unset Omega UseLocalDefs.

 Caveat : for now, real let-ins inside goals or hyps aren't handled, use
 some "cbv zeta" reduction if you want to get rid of them. And context
 definitions whose types aren't Z or nat are ignored, some manual "unfold"
 are still mandatory if expanding these definitions will help omega.

1 files changed, 31 insertions, 9 deletions

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index ae1a563be..ff69ddefb 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -50,6 +50,7 @@ let display_time_flag = ref false
 let display_system_flag = ref false
 let display_action_flag = ref false
 let old_style_flag = ref false
+let letin_flag = ref true
 
 (* Should we reset all variable labels between two runs of omega ? *)
 
@@ -100,6 +101,14 @@ let _ =
       optread  = read reset_flag;
       optwrite = write reset_flag }
 
+let _ =
+  declare_bool_option
+    { optdepr  = false;
+      optname  = "Omega takes advantage of context variables with body";
+      optkey   = ["Omega";"UseLocalDefs"];
+      optread  = read letin_flag;
+      optwrite = write letin_flag }
+
 let intref, reset_all_references =
   let refs = ref [] in
   (fun n -> let r = ref n in refs := (r,n) :: !refs; r),
@@ -376,16 +385,15 @@ let mk_var v = mkVar (Id.of_string v)
 let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |])
 let mk_times t1 t2 = mkApp (Lazy.force coq_Zmult, [| t1; t2 |])
 let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |])
-let mk_eq t1 t2 = mkApp (Lazy.force coq_eq,
-			 [| Lazy.force coq_Z; t1; t2 |])
+let mk_gen_eq ty t1 t2 = mkApp (Lazy.force coq_eq, [| ty; t1; t2 |])
+let mk_eq t1 t2 = mk_gen_eq (Lazy.force coq_Z) t1 t2
 let mk_le t1 t2 = mkApp (Lazy.force coq_Zle, [| t1; t2 |])
 let mk_gt t1 t2 = mkApp (Lazy.force coq_Zgt, [| t1; t2 |])
 let mk_inv t = mkApp (Lazy.force coq_Zopp, [| t |])
 let mk_and t1 t2 =  mkApp (Lazy.force coq_and, [| t1; t2 |])
 let mk_or t1 t2 =  mkApp (Lazy.force coq_or, [| t1; t2 |])
 let mk_not t = mkApp (Lazy.force coq_not, [| t |])
-let mk_eq_rel t1 t2 = mkApp (Lazy.force coq_eq,
-			     [| Lazy.force coq_comparison; t1; t2 |])
+let mk_eq_rel t1 t2 = mk_gen_eq (Lazy.force coq_comparison) t1 t2
 let mk_inj t = mkApp (Lazy.force coq_Z_of_nat, [| t |])
 
 let mk_integer n =
@@ -1778,11 +1786,25 @@ let destructure_hyps =
   let type_of = Tacmach.New.pf_unsafe_type_of gl in
   let decidability = decidability gl in
   let pf_nf = pf_nf gl in
-    let rec loop = function
-      | [] -> (tclTHEN nat_inject coq_omega)
-      | decl::lit ->
-          let i = NamedDecl.get_id decl in
-          Proofview.tclEVARMAP >>= fun sigma ->
+  let rec loop = function
+    | [] -> (tclTHEN nat_inject coq_omega)
+    | LocalDef (i,body,typ) :: lit when !letin_flag ->
+       Proofview.tclEVARMAP >>= fun sigma ->
+       begin
+         try
+           match destructurate_type sigma (pf_nf typ) with
+           | Kapp(Nat,_) | Kapp(Z,_) ->
+              let hid = fresh_id Id.Set.empty (add_suffix i "_eqn") gl in
+              let hty = mk_gen_eq typ (mkVar i) body in
+              tclTHEN
+                (assert_by (Name hid) hty reflexivity)
+                (loop (LocalAssum (hid, hty) :: lit))
+           | _ -> loop lit
+         with e when catchable_exception e -> loop lit
+       end
+    | decl :: lit -> (* variable without body (or !letin_flag isn't set) *)
+       let i = NamedDecl.get_id decl in
+       Proofview.tclEVARMAP >>= fun sigma ->
 	  begin try match destructurate_prop sigma (NamedDecl.get_type decl) with
 	  | Kapp(False,[]) -> elim_id i
           | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit