# 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)
| 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)).

Arguments Hyp {_} prf.