coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Francisco Ferreira <fco AT 42nd.ca>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Induction question
- Date: Mon, 18 Jul 2016 19:19:49 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fco AT 42nd.ca; spf=Pass smtp.mailfrom=fco AT 42nd.ca; spf=None smtp.helo=postmaster AT mail-it0-f48.google.com
- Ironport-phdr: 9a23:nU9p7R9QXDIEq/9uRHKM819IXTAuvvDOBiVQ1KB90e0cTK2v8tzYMVDF4r011RmSDN2dtqoP0bCempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47AblHf6ke/8SQVUk2mc1EkfqKoQsWI1Yye7KObw9XreQJGhT6wM/tZDS6dikHvjPQQmpZoMa0ryxHE8TNicuVSwn50dxrIx06vrpT4wJk2+CNJ/vkl6sRoUKPgfq1+Q6YLIi4hNjUb/sTtvhjYRgzHyHYGSGgXiBMAVwbO6zmmBJH99CDz4LkukBKGNNH7GOhnEQ+p6L1mHUfl
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
Attachment:
coq-question.v
Description: Binary data
- [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.