The Coq mailing list

[Leonardo Rodriguez <leonardomatiasrodriguez AT gmail.com>]

i'm glad for your answer to my first post,   because i'm reading your book about program certification . I hope understand the magic of omega and "crush" tactic in a near future. Your solution with the "replace" tactic was interesting too. Thank you.

2011/6/22 Adam Chlipala <adam AT chlipala.net>

leonardomatiasrodriguez@gmail.com wrote:

I'm just learning Coq, and i'm proving a simple theorem:
Theorem le_minus_minus : forall n m , n<= m ->  m - (m - n) = n.
My idea is to replace the first occurrence of "m" in "m - (m - n)"  by "n + (m
- n)" using
le_plus_minus
     : forall n m : nat, n<= m ->  m = n + (m - n)
and then prove another lemma
      forall n p : nat,  (n+p) - p = n.
to conclude ( n + (m - n) ) - (m - n) = n.
 

I see you got an answer to your question, but I'd like to point out another tactic that may make your life easier in the future.  The [rewrite] syntax, suggested by Evgeny and used in your posted solution, requires you to keep track of the argument orders of various lemmas.  By using the [replace] tactic instead, you can avoid that need.  Here's an alternate script using [replace] (see the manual for documentation of unfamiliar tactics):

Goal forall n m , n <= m -> m - (m - n) = n.
 intros.
 pattern m at 1.
 replace m with (n + (m - n)).
 apply other_lemma.
 symmetry; apply le_plus_minus; assumption.
Qed.

P.S.: I wouldn't recommend using such an unwieldy proof script in a real development, since this proof script also works (after you have run "Require Import Omega."):
   intros; omega.