coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: AUGER Cédric <sedrikov AT gmail.com>
- To: Laurent Théry <Laurent.Thery AT inria.fr>
- Cc: Kevin Sullivan <sullivan.kevinj AT gmail.com>, coq-club AT inria.fr
- Subject: Re: [Coq-Club] An interated composition puzzle
- Date: Sat, 10 Nov 2012 16:00:49 +0100
Le Sat, 10 Nov 2012 16:37:44 +0100,
Laurent Théry
<Laurent.Thery AT inria.fr>
a écrit :
> On 11/10/2012 02:54 PM, Kevin Sullivan wrote:
> > 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.
> You can prove it directly with two inductions, or only one induction
> using an intermediate lemme
> f (ant' f x n) = ant' f (f x) n (that is proved by induction)
>
> Hint: don' t forget to generalize your goal before doing the
> induction!
>
> --
> Laurent
>
>
The way I do it is by proving:
forall m n, ant0 X f x (m+n) = ant0' X f (ant0 X f x m) n).
Showing that with the lemmas "n+0=n" and "(S m)+n=m+(S n)" requires
only one induction.
But I prefer to have:
Definition ant {X: Type} (f: X->X) (x: X) :=
fix ant (n: nat) : X :=
match n with
| O => x
| S n' => f (ant n')
end.
and
Definition ant' {X: Type} (f: X->X) :=
fix (x: X) (n: nat) : X :=
match n with
| O => x
| S n' => ant' (f x) n'
end.
To minimize needs of generalization.
- [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.