The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 11/10/2012 08:54 AM, Kevin Sullivan wrote:
> My students presented two solutions to the simple problem of applying a
> function f n times to an argument x (iterated composition). The first says
> apply f to the result of applying f n-1 times to x; the second,  apply f n-1
> times to the result of applying f to x. I challenged one student to prove that
> the programs are equivalent. This ought to be pretty easy based on the
> associativity of composition. Your best solution?
>
> Fixpoint ant {X: Type} (f: X->X) (x: X) (n: nat) : X :=
> match n with
> | O =>  x
> | S n' =>  f (ant f x n')
> end.
>
> Fixpoint ant' {X: Type} (f: X->X) (x: X) (n: nat) : X :=
> match n with
> | O =>  x
> | S n' =>  ant' f (f x) n'
> end.
>
> Theorem equiv: forall (X: Type) (f: X->X) (x: X) (n: nat),
> (ant f x n) = (ant' f x n).
> Proof.  admit.
>    

Here's a pretty short solution:

Section ant.
  Variable X : Type.
  Variable f : X -> X.

  Fixpoint ant (n : nat) (x : X) : X :=
    match n with
      | O => x
      | S n' => f (ant n' x)
    end.

  Fixpoint ant' (n : nat) (x : X) : X :=
    match n with
      | O => x
      | S n' => ant' n' (f x)
    end.

  Ltac t := simpl; intuition (try autorewrite with core; auto).
  Hint Extern 1 (_ = _) => progress f_equal.

  Lemma ant'_fwd : forall n x,
    ant' n (f x) = f (ant' n x).
    induction n; t.
  Qed.

  Hint Rewrite ant'_fwd.

  Theorem equiv: forall n x,
    ant n x = ant' n x.
    induction n; t.
  Qed.
End ant.