The Coq mailing list

[Paul Tarau <paul.tarau AT gmail.com>]

Thanks for you help - the following did it:

Lemma sp_inv : forall n:B, p (s n) = n.

Proof.

induction n.

intros;firstorder.

trivial.

rewrite psi_os.

rewrite pos_ips.

f_equal. trivial.

Qed.

Paul

On May 28, 2011, at 1:14 PM, Guillaume Brunerie wrote:

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