coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jean-Francois Monin <jean-francois.monin AT imag.fr>
- To: Kevin Sullivan <sullivan.kevinj AT gmail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] An interated composition puzzle
- Date: Mon, 12 Nov 2012 00:28:03 +0800
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.
>
>
--
Jean-Francois Monin
- [Coq-Club] An interated composition puzzle, Kevin Sullivan, 11/10/2012
- Re: [Coq-Club] An interated composition puzzle, Adam Chlipala, 11/10/2012
- Re: [Coq-Club] An interated composition puzzle, Laurent Théry, 11/10/2012
- Re: [Coq-Club] An interated composition puzzle, AUGER Cédric, 11/10/2012
- Re: [Coq-Club] An interated composition puzzle, Jean-Francois Monin, 11/11/2012
- Re: [Coq-Club] An interated composition puzzle, Jonas Oberhauser, 11/11/2012
- Re: [Coq-Club] An interated composition puzzle, AUGER Cédric, 11/11/2012
- Re: [Coq-Club] An interated composition puzzle, Jonas Oberhauser, 11/11/2012
- Re: [Coq-Club] An interated composition puzzle, AUGER Cédric, 11/11/2012
- Re: [Coq-Club] An interated composition puzzle, Jonas Oberhauser, 11/11/2012
Archive powered by MHonArc 2.6.18.