gistfile1.coq

(* Kevin Sullivan <[email protected]>, writing to the Coq-Club: *)
(* 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 ant'_eq : forall (X:Type) f (x:X) n,
  ant' f (f x) n = f (ant' f x n).
Proof.
  intros X f x n.
  generalize dependent x.
  induction n. 
  (* Case n = 0, trivial *) simpl. reflexivity.
  (* Case n = S n *) simpl. intros x.
  rewrite IHn. reflexivity.
Qed.

Theorem equiv: forall (X: Type) (f: X->X) (x: X) (n: nat),
(ant f x n) = (ant' f x n).
Proof.  
  intros X f x. induction n as [|n'].
  (* n = 0 *)
   simpl. reflexivity.
  (* n = S n' *)
   simpl. rewrite IHn'.
   rewrite ant'_eq. reflexivity.
Qed.


(* Jean-Francois Monin <[email protected]>: *)
(* Additional exercise: prove the following stronger version *)

Require Import FunctionalExtensionality. (* aw yeah *)

Theorem identical : forall (X: Type) (f: X->X) n, 
 (fun x => ant f x n) = (fun x => ant' f x n).
Proof.
  intros X f n.
  apply functional_extensionality.
  intros x. apply equiv.
Qed.