Search code examples
coqproof

How to prove x + y - z = x + (y - z) in Coq

I want to prove this :

1 subgoals
x : nat
y : nat
z : nat
______________________________________(1/1)
x + y - z = x + (y - z)

It looks trivial, but it confuse me a lot, and I need it for another proof.

Thanks.

Solution

  • What you're trying to prove doesn't hold if y <= z, because with nat a-b is zero if a <= b.

    Omega is a useful tactic to use for inequalities and simple arithmetic over nat.

    Require Import Omega.
Theorem foo:
    forall x y z:nat, (x = 0 \/ z <= y) <->  x + y - z = x + (y - z).
    intros; omega.
Qed.

    However, your identity of course holds for the integers Z.

    Require Import ZArith.
Open Scope Z.
Theorem fooZ:
    forall x y z:Z, x + y - z = x + (y - z).
    intros; omega.
Qed.