The Coq mailing list

[Cédric <sedrikov AT gmail.com>]

Le Wed, 13 Aug 2014 02:42:21 +0200, Jinfang Wang <wang AT math.s.chiba-u.ac.jp> a écrit:

Dear All,

I am a statistician and am (very) new to Coq/SSReflect.

I am asking a shamefully simple question, namely, what kind of tactics should I use to cancel a common factor from both sides of an equation? In its simplest form, I what to know how to prove the following fact:

Fact Cancellation_Law: forall x y z, x + z = y + z -> x=y.

Thanks a lot for your help.

Jinfang Wang

Chiba University, Japan

What is your '+'? Is it the one on natural numbers (ie. the one defined without requiring any library)?

If so, (nat, 0, +, *) is not a group, still your cancellation law is valid.

If so, you can use:

Require Import Omega.

Fact Cancellation_Law: forall x y z, x + z = y + z -> x=y.
Proof.
  intros.
  omega.

Qed.

Omega is a tactic designed to solve many arithmetic problems. It is not the only one tactic, there is also the "ring" tactic. I think there is also a "lia" tactic (linear arithmetic), but I never tried it.

But using it will not teach you much on how to use Coq. For that there is some documentation you should start with (CPDT, or Software Foundations for example).

--

---
Cédric AUGER