The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

Your conjecture is wrong:

Lemma wrong: SubPlist (0 :: nil).
Proof.
apply Sub. apply Skip.
  - apply Base.
  - repeat constructor.
Qed.

Jean-Francois

On Fri, Oct 04, 2013 at 10:23:29AM +0200, Fabien Renaud wrote:
> 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.
> >


-- 
Jean-Francois Monin
VERIMAG
Universite de Grenoble 1