Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[micromega] Add missing support for implb #13715

Merged
merged 1 commit into from Jan 7, 2021
Merged

[micromega] Add missing support for implb #13715

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
2 changes: 2 additions & 0 deletions doc/changelog/04-tactics/13715-lia_implb.rst
View file
Open in desktop
@@ -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).
23 changes: 16 additions & 7 deletions plugins/micromega/coq_micromega.ml
View file
Open in desktop
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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

Expand Down
18 changes: 18 additions & 0 deletions test-suite/micromega/reify_bool.v
View file
Open in desktop
@@ -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.