diff options
Diffstat (limited to 'plugins')
| -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" (** |