The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Is this really stronger? I do not have 8.4 installed but I believe this 
compiles (in 8.4):

Lemma equalsto : (forall (X: Type) (f: X->X) n, (fun x => ant f x n) = 
(fun x => ant' f x n))
  = (forall (X: Type) (f: X->X) (n: nat) (x: X), (ant f x n) = (ant' f 
x n)).
reflexivity. Qed.

In 8.3, I don't seem to be able to prove "equalsto" even if I assume this:

Axiom eta : forall X Y (f : X -> Y), f = (fun x => f x).

Coq doesn't allow me to rewrite beneath the quantifiers when I need the 
quantified variables :( Is there a way around this?

Am 11.11.2012 17:28, schrieb Jean-Francois Monin:
> Additional exercise: prove the following stronger version
>
> Theorem identical : forall (X: Type) (f: X->X) n,
>    (fun x => ant f x n) = (fun x => ant' f x n).
>
> This can be done without axiom (in Coq 8.4).
> Warning: there is a funny trick to use somewhere, so to speak.
>
> The above statement is somewhat weird. It is better to consider:
>
> Theorem identical2 : forall (X: Type) (f: X->X) n,
>    ant2' f n = ant2 f n.
>
> with obvious definitions for ant2 and ant2' such that
> ant2 f n   =  fun x => ant f x n
> ant2' f n  =  fun x => ant' f x n
>
>
> JF
>
>
> On Sat, Nov 10, 2012 at 02:54:57PM +0100, 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.