The Coq mailing list

[Guillaume Brunerie <guillaume.brunerie AT gmail.com>]

2011/5/28 Paul Tarau <paul.tarau AT gmail.com>

I would like Coq to reason along the following equations:

    p (s (i b)) = p (o (s b)) = i (p (s b)) = i b

where I want to use, as an inductive hypothesis, that p (s b) = b holds.

I tried "apply psi_os" (that I just proved) but it seems to want both sides

of an equation - is there any way to make it just rewrite p (s (i b)) as

p (o (s b)) according to Lemma psi_os?

The answer is in the question :-)
The tactic you want is called 'rewrite', if you use 'rewrite psi_os' instead of 'apply psi_os', this will work (the tactic 'apply' try to match the current goal with the conclusion, here this is not what you want).
In order to do an induction, you will first need to use 'induction n' at the beginning of the proof, and prove the two other (easy) cases of the induction.

Guillaume