how to simplify a equality statement

Question

In hypothesis, I have a natural number that cannot be zero.When we add this number to an another function,whose output is also natural number. I have to prove that result of addition of these two values equal to zero is false. I should not dig about f,because addition of anything in non zero term ,become equal to zero is false statement.

`H : (m =? 0) = false

(f+ m =? 0) = false`

Answer 1

Short answer:

Require Import Lia.

rewrite !Nat.eqb_neq; lia.

Long answer:

I feel sorry that this question arises. Historically, most of the reasoning in Coq about equality is done with the eq concept, with the notation m = n, not with the boolean equality, on which you rely here. It is also important to know that Coq has a specific notation for "disequality" or "non-equality" : m <> n stands for ~ (m = n).

So if you add typed the following statement instead, there would be an easy solution:

Require Import Arith Lia.

Lemma example1 f m : m <> 0 -> f + m <> 0.
Proof. lia. Qed.

Unfortunately, this does not work for the way you express your statement:

Lemma example2 f m : (m =? 0) = false -> (f + m =? 0) = false.
Proof. 
Fail lia.

If you call Search with the following pattern, you see that the boolean comparison expression is logically equivalent to basic equality, but only if you use specific theorems to express this:

Search (_ =? _).

Nat.eqb_refl: forall x : nat, (x =? x) = true
beq_nat_refl: forall n : nat, true = (n =? n)
Nat.eqb_sym: forall x y : nat, (x =? y) = (y =? x)
Nat.eqb_spec: forall x y : nat, Bool.reflect (x = y) (x =? y)
beq_nat_eq: forall n m : nat, true = (n =? m) -> n = m
beq_nat_true: forall n m : nat, (n =? m) = true -> n = m
Nat.eqb_eq: forall n m : nat, (n =? m) = true <-> n = m
beq_nat_false: forall n m : nat, (n =? m) = false -> n <> m
Nat.eqb_neq: forall x y : nat, (x =? y) = false <-> x <> y
Nat.pow2_bits_eqb: forall n m : nat, Nat.testbit (2 ^ n) m = (n =? m)
Nat.bit0_eqb: forall a : nat, Nat.testbit a 0 = (a mod 2 =? 1)
Nat.eqb_compare:
  forall x y : nat, (x =? y) = match x ?= y with
                           | Eq => true
                           | _ => false
                           end
Nat.setbit_eqb:
  forall a n m : nat,
  Nat.testbit (Nat.setbit a n) m = ((n =? m) || Nat.testbit a m)%bool
Nat.clearbit_eqb:
  forall a n m : nat,
  Nat.testbit (Nat.clearbit a n) m = (Nat.testbit a m && negb (n =? m))%bool
Nat.testbit_eqb: forall a n : nat, Nat.testbit a n = ((a / 2 ^ n) mod 2 =? 1)

But there is no theorem that expresses the interaction of addition with equality to 0. You can also see this using a more precise pattern.

Search (_ =? _) 0 (_ + _).

This returns nothing.

On the other hand, if you type

Search (_ = _) 0 (_ + _).

You see many theorems, one of which is relevant to your problem.

Nat.eq_add_0: forall n m : nat, n + m = 0 <-> n = 0 /\ m = 0

And this one is enough to solve the problem, if it is expressed with _ = _ instead of _ =? _. So to solve your specific problem, we need first to transform comparisons using _ =? _ into equality statements,and then do logical reasoning using the available theorems. In the first search result, we have the theorem Nat.eqb_neq that is adapted to your situation. Continuing on the proof of example2 above, we can write:

Rewrite !Nat.eqb_neq.

The goal becomes:

f, m : nat
============================
m <> 0 -> f + m <> 0

Now, we could do logical reasoning using the theorem Nat.eq_add_0.

rewrite Nat.eq_add_0.

We can finish the proof by small step like this.

intros mn0 [fis0 mis0]; case mn0; assumption.

we can also ask an automatic tool to finish the proof for us:

tauto.

But going a little backward in time, we can also observe the statement after rewriting with Nat.eqb_neq. This is a statement in linear arithmetic (it contains comparisons, natural numbers, and no product between variables). This statement is in the scope of a tactic for this theory, the one used most often now is lia.