diff options
| -rw-r--r-- | doc/changelog/04-tactics/13715-lia_implb.rst | 2 | ||||
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 23 | ||||
| -rw-r--r-- | test-suite/micromega/reify_bool.v | 18 |
3 files changed, 36 insertions, 7 deletions
diff --git a/doc/changelog/04-tactics/13715-lia_implb.rst b/doc/changelog/04-tactics/13715-lia_implb.rst new file mode 100644 index 0000000000..dd61872342 --- /dev/null +++ b/doc/changelog/04-tactics/13715-lia_implb.rst @@ -0,0 +1,2 @@ +- **Added:** + :tacn:`lia` supports the boolean operator `Bool.implb` (`#13715 <https://github.com/coq/coq/pull/13715>`_, by Frédéric Besson). diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index e119ceb241..5e138fa3d1 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -930,7 +930,8 @@ let is_prop env sigma term = Sorts.is_prop sort type formula_op = - { op_and : EConstr.t + { op_impl : EConstr.t option (* only for booleans *) + ; op_and : EConstr.t ; op_or : EConstr.t ; op_iff : EConstr.t ; op_not : EConstr.t @@ -939,7 +940,8 @@ type formula_op = let prop_op = lazy - { op_and = Lazy.force coq_and + { op_impl = None (* implication is Prod *) + ; op_and = Lazy.force coq_and ; op_or = Lazy.force coq_or ; op_iff = Lazy.force coq_iff ; op_not = Lazy.force coq_not @@ -948,13 +950,17 @@ let prop_op = let bool_op = lazy - { op_and = Lazy.force coq_andb + { op_impl = Some (Lazy.force coq_implb) + ; op_and = Lazy.force coq_andb ; op_or = Lazy.force coq_orb ; op_iff = Lazy.force coq_eqb ; op_not = Lazy.force coq_negb ; op_tt = Lazy.force coq_true ; op_ff = Lazy.force coq_false } +let is_implb sigma l o = + match o with None -> false | Some c -> EConstr.eq_constr sigma l c + let parse_formula (genv, sigma) parse_atom env tg term = let parse_atom b env tg t = try @@ -970,6 +976,10 @@ let parse_formula (genv, sigma) parse_atom env tg term = match EConstr.kind sigma term with | App (l, rst) -> ( match rst with + | [|a; b|] when is_implb sigma l op.op_impl -> + let f, env, tg = xparse_formula op k env tg a in + let g, env, tg = xparse_formula op k env tg b in + (mkformula_binary k (mkIMPL k) term f g, env, tg) | [|a; b|] when EConstr.eq_constr sigma l op.op_and -> let f, env, tg = xparse_formula op k env tg a in let g, env, tg = xparse_formula op k env tg b in @@ -2075,12 +2085,11 @@ module MakeCache (T : sig val hash_coeff : int -> coeff -> int val eq_prover_option : prover_option -> prover_option -> bool val eq_coeff : coeff -> coeff -> bool -end) : -sig +end) : sig type key = T.prover_option * (T.coeff Mc.pol * Mc.op1) list + val memo_opt : (unit -> bool) -> string -> (key -> 'a) -> key -> 'a -end = -struct +end = struct module E = struct type t = T.prover_option * (T.coeff Mc.pol * Mc.op1) list diff --git a/test-suite/micromega/reify_bool.v b/test-suite/micromega/reify_bool.v new file mode 100644 index 0000000000..501fafc0b3 --- /dev/null +++ b/test-suite/micromega/reify_bool.v @@ -0,0 +1,18 @@ +Require Import ZArith. +Require Import Lia. +Import Z. +Unset Lia Cache. + +Goal forall (x y : Z), + implb (Z.eqb x y) (Z.eqb y x) = true. +Proof. + intros. + lia. +Qed. + +Goal forall (x y :Z), implb (Z.eqb x 0) (Z.eqb y 0) = true <-> + orb (negb (Z.eqb x 0))(Z.eqb y 0) = true. +Proof. + intro. + lia. +Qed. |