The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

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).

> 
> 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).

I did the proof in 8.4 and I am pretty sure not to have used any of the
8.4 which weren't in the 8.3. So I am pretty sure this is provable in
8.3.

> 
> 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.

to get:

(λ x, (λ x, G x n) (f x)) = (λ x, f (G x n))
-----→
(λ x, G (f x) n) = (λ x, f (G x n))

with F=ant f and G=ant' f

So you can almost always rewrite, but you have to do some manual stuff.
Maybe the 'pattern' tactic could help. But here again, you would have
to give full expression to factorize. rewrite is not clever enough to
do 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.
> >>
> >>
>