The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

On Monday 30 March 2009 15:45:38 James McKinna wrote:
> Dear Edsko, and others,
>
> a simpler example might be to try to show, for example, commutativity of
> addition on natural numbers defined tail-recursively as
>
> plus 0 n = n
> plus (S m) n = plus m (S n)
>
> We discussed this problem (and automatic techniques for solving it, due
> to Andrew Ireland and Alan Bundy in particular) at the Dagstuhl 9350
> meeting in 1995...
>     http://www.dagstuhl.de/en/program/calendar/semhp/?semnr=9530
>
> But I can't find Andrew's paper on it out there in TV-land ("Rippling to
> meet the challenge", I think it was called, given during the last
> session on challenge problems). You might check with him directly...

I couldn't find the paper, but I've been implementing a rippling tactic in 
Coq 
(I hope to release this soon) and it can automatically prove commutativity of 
addition using the tail-recursive definition of plus above. It can do this 
given only the definition of plus and the regular induction principles 
generated by Coq. A manual proof that imitates the proof steps the rippling 
tactic makes in one of its proofs is as follows:

Fixpoint plus_t (m n : nat) {struct m} : nat :=
  match m with
  | 0 => n
  | S p => plus_t p (S n)
  end.

Notation "x +t y" := (plus_t x y) (at level 20).

Theorem add_commute_2 : forall a b, a +t b = b +t a.
intros.
revert a.
induction b.

 simpl.
 induction a.
  reflexivity.
 
  rewrite <- IHa. 
  generalize (a +t 0). intros. clear.
  induction n.
   reflexivity.
 
   simpl.
   rewrite <- IHn.
   generalize 0. intros. clear.
   revert n0.
   induction n.

    reflexivity.
    simpl.
    intros.
    rewrite IHn.
    reflexivity.

 intros.
 simpl.
 rewrite <- IHb.
 reflexivity.
Defined.

The essentially tricks are to make use of "revert" and "generalize" where 
appropriate before performing induction so that the induction hypotheses are 
strong enough in the step cases. I found that the "generalize 0" step in one 
of the subgoals wasn't obvious i.e. n +t 2 = S (S n +t 0) should be 
generalized to n +t S (S n0) = S (S n +t n0) before induction is performed on 
n. There are a couple of papers on my homepage that briefly describe 
automation with rippling in Coq: http://homepages.inf.ed.ac.uk/s0091720/

Regards,

Sean