coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Frédéric Besson <frederic.besson AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Induction question
- Date: Tue, 19 Jul 2016 09:51:30 +0200
Hello,
Using remember is a good start.
To get a stronger induction hypothesis you need to generalise hypotheses.
Here do a:
revert m n Heqt.
before doing induction.
—
Frédéric
PS: This is actually a FAQ...
> On 19 Jul 2016, at 01:19, Francisco Ferreira
> <fco AT 42nd.ca>
> wrote:
>
> Hello everybody,
> I defined the following data type
> Inductive Acc (A : Set) (R : A -> A -> Prop) (t : A): Prop :=
> inj : (forall t': A, R t t' -> Acc A R t') -> Acc A R t.
> and I am trying to prove a lemma by induction on it. For example, it has
> the following shape.
> Lemma test: forall m n, Acc nat gt (m + n) -> Acc nat gt m.
> Trying to do induction on (Acc nat gt (m + n)) leads us to an hypothesis
> H0 : forall t' : nat, t > t' -> Acc nat gt m
> where t has no relation with m and n.
> Trying to use the remember tactics
> intros.
> remember (m + n) as t.
> induction H.
> leads us to an induction hypothesis
> H0 : forall t' : nat, t > t' -> t' = m + n -> Acc nat gt m
> but the clause t' = m + n is unsatisfiable for any t' < t.
> How I can use induction on Acc in such a way that the induction
> hypothesis preserves the information and is still usable?
> Thanks,
> Francisco
> <coq-question.v>
- [Coq-Club] Induction question, Francisco Ferreira, 07/19/2016
- Re: [Coq-Club] Induction question, Frédéric Besson, 07/19/2016
- Re: [Coq-Club] Induction question, Dominique Larchey-Wendling, 07/19/2016
- Re: [Coq-Club] Induction question, Francisco Ferreira, 07/19/2016
Archive powered by MHonArc 2.6.18.