The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 11.11.2012 20:36, schrieb AUGER Cédric:
> Le Sun, 11 Nov 2012 20:00:25 +0100,
> Jonas Oberhauser 
> <s9joober AT gmail.com>
>  a écrit :
>
> > 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.
> Your belief is wrong.
>
> ∀ X (f:X→X) n, (λ x, ant f x n) = (λ x, ant' f x n)
>
> and
>
> ∀ X (f:X→X) n x, ant f x n = ant' f x n
>
> are not unifiable (or so do I hope).

Ahhh I misread. No wonder was I confused. I agree that they are not 
convertible : ) I thought all that happened was an eta expansion (which 
looked weird to me), but this time we prove that the procedures are the 
same, not just the outcomes. I can see how that is a stronger result.

> > Coq doesn't allow me to rewrite beneath the quantifiers when I need
> > the quantified variables :( Is there a way around this?
> Yes and no.
>
> More precisely, in the proofs, I had something like:
>
> H:(λ x, F x n) = (λ x, G x n)
>
> and needed to prove
>
> (λ x, F (f x) n) = (λ x, f (G x n))
>
> what I did was a:
>
> change (λ x, F (f x) n) with (λ x, (λ x, F x n) (f x)).
>
> Then I could do
>
> rewrite H.

I see...
Do you think this should be provable:

Lemma simpleexample X f g : (forall x : X, f x = g x) -> (forall x : X, 
f x = x) = (forall x : X, g x = x).

Obviously I can prove that the two propositions are equivalent, but I 
want to prove that they are equal. If equality means convertibility, I 
certainly think this is true.
Kind regards, Jonas
> > 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.