diff options
| author |  fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-23 18:00:22 +0000 |
|---|---|---|
| committer | fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-23 18:00:22 +0000 |
| commit | a87b941bcdd0f3de75e18a245cbad4656fa11fe8 (patch) | |
| tree | f8aa894c6013ebdc56c394701370c8e208cf0df8 /plugins/micromega | |
| parent | f1686dbcad2515eee22b26b156fe51f6e9d22857 (diff) | |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14152 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/Psatz.v | 9 | ||||
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 1 |
2 files changed, 10 insertions, 0 deletions
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index 325cc31bb..4fef3d790 100644 --- a/plugins/micromega/Psatz.v +++ b/plugins/micromega/Psatz.v @@ -76,6 +76,15 @@ Ltac psatzl dom := | _ => fail "Unsupported domain" end in tac. + +Ltac lra := + unfold Rdiv in * ; + psatzl_R ; + try (intros __wit __varmap __ff ; + change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; + apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity). + + Ltac lia := cbv delta - [Zplus Zminus Zopp Zmult Zpower Zgt Zge Zle Zlt iff not] ; xlia ; intros __wit __varmap __ff ; diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 69ec518ee..42d451a2d 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1524,6 +1524,7 @@ let rec abstract_wrt_formula f1 f2 = | I(a,_,b) , I(a',x,b') -> I(abstract_wrt_formula a a',x, abstract_wrt_formula b b') | FF , FF -> FF | TT , TT -> TT + | N x , N y -> N(abstract_wrt_formula x y) | _ -> failwith "abstract_wrt_formula" (** |