The Coq mailing list

[Jeff Vaughan <jeff AT seas.harvard.edu>]

I haven't tried this yet, but Frederic Blanqui and Adam Koprowski 
pointed me to the CoLoR library which has lemmas and tactics for 
unfolding vectors 
(http://color.inria.fr/doc/CoLoR.Util.Vector.VecUtil.html#VSntac).  You 
may be able to write tactic based on theirs which handles both theorems.


Best,
Jeff

Benedikt.AHRENS AT unice.fr
 wrote:
> Hello,
>
> for the complementary theorem about vectors of length 0 (code at the
> bottom), Adam's suggestion can be adopted [1], whereas a proof similar
> to Laurent's [2] fails, since the abstraction in the inversion step
> gives an ill-typed term.
> Is there a way to prove the lemma by tactics anyway?
>
> Greetings
> ben
>
> [1]
> Definition is_vnil (A:Set) (v:vector A 0):
>            v = vnil :=
> match v in vector _ N return
>              match N return vector A N -> Prop with
>              | 0 => fun v0 => v0 = vnil
>              | S p => fun _ => True
>              end v with
> | vnil => refl_equal _
> | vcons _ _ _ => I
> end.
>
> [2]
> Lemma is_nil: forall A (v:vector A 0),
>         v = vnil.
> Proof.
> intros A v.
> change (
>    (fun n => match n as n1 return vector A n1 -> Prop with
>             | 0 => fun v => v = vnil
>             | S p => fun _ => True
>             end) 0 v).
> dependent inversion v.
>
> (*
> Error: Abstracting over the terms "0" and "v" leads to a term
> "fun (n : nat) (v : vector A n) =>
>  (fun n0 : nat =>
>   match n0 as n1 return (vector A n1 -> Prop) with
>   | 0 => fun v0 : vector A n => v0 = vnil
>   | S p => fun _ : vector A (S p) => True
>   end) n v" which is ill-typed.
> *)
>
>
>
> Laurent Théry wrote:
> > Hi,
> >
> > yep you have to break the dependance in the equality.
> > Adam's idea but with tactic:
> >
> > Lemma openVector: forall A n (v: vector A (S n)),
> >    exists a, exists v0, v = vcons a v0.
> > intros A n v.
> > change
> > ((fun n: nat => match n return vector A n -> Prop with
> >   O => fun _ => True (* what you want *)
> > | S n1 => fun v =>
> >      exists a : A, exists v0 : vector A n1, v = vcons a v0
> > end) (S n) v).
> > dependent inversion v as [|n1 a1 v1].
> > exists a1; exists v1; auto.
> > Qed.
> >
> >
> > --------------------------------------------------------
> > Bug reports: http://logical.saclay.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.saclay.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