diff options
| author | Frédéric Besson | 2020-04-30 10:03:46 +0200 |
|---|---|---|
| committer | Frédéric Besson | 2020-04-30 14:46:57 +0200 |
| commit | 5d514890669296e5d25a342c15aa930595f3af10 (patch) | |
| tree | b4eb670f22ec51187f2243ce3ffed1f59d1fe24f | |
| parent | d436c45a19de2f91aad94f492b547225f8c5b305 (diff) | |
[zify] add support for Nat.le, Nat.lt and Nat.eq
Nat.le, Nat.lt and Nat.eq are aliased to le, lt and @eq nat.
The required declarations are now added in ZifyInst.
| -rw-r--r-- | doc/changelog/04-tactics/12213-zify-Nat.rst | 3 | ||||
| -rw-r--r-- | test-suite/micromega/bug_12210.v | 19 | ||||
| -rw-r--r-- | theories/micromega/ZifyInst.v | 9 |
3 files changed, 31 insertions, 0 deletions
diff --git a/doc/changelog/04-tactics/12213-zify-Nat.rst b/doc/changelog/04-tactics/12213-zify-Nat.rst new file mode 100644 index 0000000000..8b744cd193 --- /dev/null +++ b/doc/changelog/04-tactics/12213-zify-Nat.rst @@ -0,0 +1,3 @@ +- **Added:** + The :tacn:`zify` tactic is now aware of `Nat.le`, `Nat.lt` and `Nat.eq` + (`#12213 <https://github.com/coq/coq/pull/12213>`_, by Frédéric Besson; fixes `#12210 <https://github.com/coq/coq/issues/12210>`_). diff --git a/test-suite/micromega/bug_12210.v b/test-suite/micromega/bug_12210.v new file mode 100644 index 0000000000..ca011def09 --- /dev/null +++ b/test-suite/micromega/bug_12210.v @@ -0,0 +1,19 @@ +Require Import PeanoNat Lia. + +Goal forall x, Nat.le x x. +Proof. +intros. +lia. +Qed. + +Goal forall x, Nat.lt x x -> False. +Proof. +intros. +lia. +Qed. + +Goal forall x, Nat.eq x x. +Proof. +intros. +lia. +Qed. diff --git a/theories/micromega/ZifyInst.v b/theories/micromega/ZifyInst.v index 521ac61e18..5b15dc072a 100644 --- a/theories/micromega/ZifyInst.v +++ b/theories/micromega/ZifyInst.v @@ -42,6 +42,9 @@ Instance Op_lt : BinRel lt := {| TR := Z.lt; TRInj := Nat2Z.inj_lt |}. Add BinRel Op_lt. +Instance Op_Nat_lt : BinRel Nat.lt := Op_lt. +Add BinRel Op_Nat_lt. + Instance Op_gt : BinRel gt := {| TR := Z.gt; TRInj := Nat2Z.inj_gt |}. Add BinRel Op_gt. @@ -50,10 +53,16 @@ Instance Op_le : BinRel le := {| TR := Z.le; TRInj := Nat2Z.inj_le |}. Add BinRel Op_le. +Instance Op_Nat_le : BinRel Nat.le := Op_le. +Add BinRel Op_Nat_le. + Instance Op_eq_nat : BinRel (@eq nat) := {| TR := @eq Z ; TRInj := fun x y : nat => iff_sym (Nat2Z.inj_iff x y) |}. Add BinRel Op_eq_nat. +Instance Op_Nat_eq : BinRel (Nat.eq) := Op_eq_nat. +Add BinRel Op_Nat_eq. + (* zify_nat_op *) Instance Op_plus : BinOp Nat.add := {| TBOp := Z.add; TBOpInj := Nat2Z.inj_add |}. |