coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Cedric Auger <sedrikov AT gmail.com>
- To: Fabien Renaud <Fabien.Renaud AT inria.fr>
- Cc: Jonas Oberhauser <s9joober AT gmail.com>, "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] How to talk about a restricted set of an inductive?
- Date: Fri, 4 Oct 2013 11:05:16 +0200
Once again, I do not see the point in having Plist in Type. For any given m and n, Plist m n is either empty or a singleton.
2013/10/4 Fabien Renaud <Fabien.Renaud AT inria.fr>
Now I would to restrict to Plist which are started with an empty left list:(In my real problem, I cannot as well give a better base case since free duplication can happen).Hi,Take this inductive:
This is the kind of things I want but I actually simplified too much my problem.
Inductive Plist : list nat -> list nat -> Type :=
| Base l : Plist l nil
| Move l x l': Plist (x::l) l' -> x > 10 -> Plist l (x::l')
| Skip l x l': Plist l l' -> x <= 10 -> Plist l (x::l')
.
Inductive SubPlist : list nat -> Type :=
| Sub l : Plist nil l -> SubPlist l.I would like to be able to prove that for all Plist coming from SubPlist,
all the elements are strictly greater than 10.But there is now (wrt to the previous example), no way toimmediately conclude since this is a consequence.
So once again I'm wondering how should I do?
On Fri, Oct 4, 2013 at 4:01 AM, Jonas Oberhauser <s9joober AT gmail.com> wrote:
Am 03.10.2013 14:35, schrieb Cedric Auger:Jup. There might be a simpler proof, but here is one:
A n (l : list A) (x y : NList_ n l), x = y.
Lemma NList_Unique {A} (l : list A) n (y : NList_ n l): match n return NList_ n l -> Prop with
| 0 => fun y => Base l = y
| S n' =>
match l with
| nil => fun y => False
| cons a l' => fun y => exists x : NList_ n' l', Cons n' l' a x = y
end
end y.
induction y ; auto.
exists y ; auto.
Qed.
Goal forall A n (l : list A) (x y : NList_ n l), x = y.
induction x.
apply (NList_Unique l).
intros y.
destruct (NList_Unique (a :: l) (S n) y) as [x' P].
now rewrite IHx with x'.
Qed.
--
.../Sedrikov\...
- Re: [Coq-Club] How to talk about a restricted set of an inductive?, (continued)
- Message not available
- Re: [Coq-Club] How to talk about a restricted set of an inductive?, Fabien Renaud, 10/03/2013
- Re: [Coq-Club] How to talk about a restricted set of an inductive?, Robbert Krebbers, 10/03/2013
- Re: [Coq-Club] How to talk about a restricted set of an inductive?, Robbert Krebbers, 10/03/2013
- Re: [Coq-Club] How to talk about a restricted set of an inductive?, Fabien Renaud, 10/03/2013
- Re: [Coq-Club] How to talk about a restricted set of an inductive?, Rui Baptista, 10/03/2013
- Re: [Coq-Club] How to talk about a restricted set of an inductive?, Fabien Renaud, 10/03/2013
- Message not available
- Re: [Coq-Club] How to talk about a restricted set of an inductive?, Cedric Auger, 10/03/2013
- Re: [Coq-Club] How to talk about a restricted set of an inductive?, Jonas Oberhauser, 10/04/2013
- Re: [Coq-Club] How to talk about a restricted set of an inductive?, Fabien Renaud, 10/04/2013
- Re: [Coq-Club] How to talk about a restricted set of an inductive?, Jean-Francois Monin, 10/04/2013
- Re: [Coq-Club] How to talk about a restricted set of an inductive?, Fabien Renaud, 10/04/2013
- Re: [Coq-Club] How to talk about a restricted set of an inductive?, Cedric Auger, 10/04/2013
Archive powered by MHonArc 2.6.18.