The Coq mailing list

[Dimitri Hendriks <diem AT cs.vu.nl>]

I forgot the type parameter A in the definition of get_first,
it should be:


Definition get_first (A : Type) (n:nat) (v : vec A (S n)) : A :=
    match v in (vec _ m) return (m = S n -> A) with
    | Vnil => fun H => False_rect A (disc_O_S n H)
    | Vcons a _ _ => fun _ => a
    end (refl_equal (S n)).



On 28 Mar 2008, at 10:36, Dimitri Hendriks wrote:
> for pattern matching over dependent types you
> have to use an explicit elimination predicate
> to predict the type of the righthand side.
> see ch. 15 of the manual.
>
> if you first define your function with tactics:
>
> Definition get_first (A : Type) (n:nat) (v : vec A (S n)) : A.
> intros A n v.
> inversion v as [ | a m w H ].
> exact a.
> Defined.
>
> and then inspect the built lambda-term:
>
> Print get_first.
>
> you can see what the predicate should look like:
>   (vec m) -> (m = S n -> A)
>
> and this may insprire you to write for instance:
>
> Lemma disc_O_S : forall n, O <> S n.
> intros n H.
> discriminate H.
> Qed.
>
> Definition get_first (n:nat) (v : vec (S n)) : A :=
>   match v in (vec m) return (m = S n -> A) with
>   | Vnil => fun H => False_rect A (disc_O_S n H)
>   | Vcons a _ _ => fun _ => a
>   end (refl_equal (S n)).
>
> dimitri
>
> On 28 Mar 2008, at 09:07, Michael Day wrote:
> > Hi,
> >
> > I have defined a simple vector type and a function to get the  
> > first element of non-empty vectors as follows:
> >
> > Inductive vec (A:Type) : nat -> Type :=
> >     | Vnil : vec A 0
> >     | Vcons : forall (a:A) (n:nat), vec A n -> vec A (S n).
> >
> > Definition get_first (A:Type) (n:nat) (v:vec A (S n))  
> > (default:A) : A :=
> >     match v with
> >     | Vnil => default    (* I want to delete this line *)
> >     | Vcons a _ _ => a
> >     end.
> >
> > Coq prevents me from calling get_first with an empty vector, so  
> > the Vnil case will never be matched and the default value will  
> > never be used. However, Coq does not permit me to omit this case:
> >
> > Error: Non exhaustive pattern-matching: no clause found for  
> > pattern Vnil
> >
> > This is incredibly frustrating. Why does Coq think that "Vnil" is  
> > an inhabitant of "vec (S n)"? After reading Conor McBride's papers  
> > on Epigram I expect the system to understand that 0 <> S n :)
> >
> > The Vhead function in the Bvector module in the standard library  
> > uses the inversion tactic instead, but that seems to generate a  
> > very large and complicated definition for something that should be  
> > quite simple.
> >
> > Best regards,
> >
> > Michael
> >
> > --
> > Print XML with Prince!
> > http://www.princexml.com
> >
> > --------------------------------------------------------
> > Bug reports: http://logical.futurs.inria.fr/coq-bugs
> > Archives: http://pauillac.inria.fr/pipermail/coq-club
> >          http://pauillac.inria.fr/bin/wilma/coq-club
> > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club