Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] How to talk about a restricted set of an inductive?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to talk about a restricted set of an inductive?


Chronological Thread 
  • 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>
Hi,

This is the kind of things I want but I actually simplified too much my problem.

Take this inductive:
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')
.

(In my real problem, I cannot as well give a better base case since free duplication can happen).

Now I would to restrict to Plist which are started with an empty left list:
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 to
immediately 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:

A n (l : list A) (x y : NList_ n l), x = y.

Jup. There might be a simpler proof, but here is one:

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\...



Archive powered by MHonArc 2.6.18.

Top of Page