Как доказать х + у - г = х + (у - г) в Coq

Question

Я хочу, чтобы доказать это:

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

Это выглядит тривиальным, но запутать меня много, и мне это нужно другое доказательство.

Спасибо.

Answer 1

То, что вы пытаетесь доказать, не выполняется, если y < = z, потому что с nat a-b равно нулю, если < = b.

Omega - полезная тактика, используемая для неравенства и простой арифметики над nat.

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

Однако, ваша личность, конечно, справедливо и для целых Z.

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