Library Coq.micromega.Ztac
Tactics for doing arithmetic proofs.
Useful to bootstrap lia.
Require Import ZArithRing.
Require Import ZArith_base.
Local Open Scope Z_scope.
Lemma eq_incl :
forall (
x y:
Z),
x = y -> x <= y /\ y <= x.
Lemma elim_concl_eq :
forall x y,
(x < y \/ y < x -> False) -> x = y.
Lemma elim_concl_le :
forall x y,
(y < x -> False) -> x <= y.
Lemma elim_concl_lt :
forall x y,
(y <= x -> False) -> x < y.
Lemma Zlt_le_add_1 :
forall n m :
Z,
n < m -> n + 1
<= m.
Ltac normZ :=
repeat
match goal with
|
H :
_ < _ |-
_ =>
apply Zlt_le_add_1 in H
|
H : ?
Y <= _ |-
_ =>
lazymatch Y with
| 0 =>
fail
|
_ =>
apply Zle_minus_le_0 in H
end
|
H :
_ >= _ |-
_ =>
apply Z.ge_le in H
|
H :
_ > _ |-
_ =>
apply Z.gt_lt in H
|
H :
_ = _ |-
_ =>
apply eq_incl in H ;
destruct H
| |- @
eq Z _ _ =>
apply elim_concl_eq ;
let H :=
fresh "HZ"
in intros [
H|
H]
| |-
_ <= _ =>
apply elim_concl_le ;
intros
| |-
_ < _ =>
apply elim_concl_lt ;
intros
| |-
_ >= _ =>
apply Z.le_ge
end.
Inductive proof :=
|
Hyp (
e :
Z) (
prf : 0
<= e)
|
Add (
p1 p2:
proof)
|
Mul (
p1 p2:
proof)
|
Cst (
c :
Z)
.
Lemma add_le :
forall e1 e2, 0
<= e1 -> 0
<= e2 -> 0
<= e1+e2.
Lemma mul_le :
forall e1 e2, 0
<= e1 -> 0
<= e2 -> 0
<= e1*e2.
Fixpoint eval_proof (
p :
proof) :
{ e : Z | 0
<= e} :=
match p with
|
Hyp e prf =>
exist _ e prf
|
Add p1 p2 =>
let (
e1,
p1) :=
eval_proof p1 in
let (
e2,
p2) :=
eval_proof p2 in
exist _ _ (
add_le _ _ p1 p2)
|
Mul p1 p2 =>
let (
e1,
p1) :=
eval_proof p1 in
let (
e2,
p2) :=
eval_proof p2 in
exist _ _ (
mul_le _ _ p1 p2)
|
Cst c =>
match Z_le_dec 0
c with
|
left prf =>
exist _ _ prf
|
_ =>
exist _ _ Z.le_0_1
end
end.
Ltac lia_step p :=
let H :=
fresh in
let prf := (
eval cbn - [
Z.le Z.mul Z.opp Z.sub Z.add]
in (
eval_proof p))
in
match prf with
| @
exist _ _ _ ?
P =>
pose proof P as H
end ;
ring_simplify in H.
Ltac lia_contr :=
match goal with
|
H : 0
<= - (Zpos _) |-
_ =>
rewrite <-
Z.leb_le in H;
compute in H ;
discriminate
|
H : 0
<= (Zneg _) |-
_ =>
rewrite <-
Z.leb_le in H;
compute in H ;
discriminate
end.
Ltac lia p :=
lia_step p ;
lia_contr.
Ltac slia H1 H2 :=
normZ ;
lia (
Add (
Hyp _ H1) (
Hyp _ H2)).