The Coq mailing list

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