coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Benedikt.AHRENS AT unice.fr
- To: Laurent Th�ry <Laurent.Thery AT sophia.inria.fr>
- Cc: Jeff Vaughan <jeff AT seas.harvard.edu>, Coq List <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] Pattern matching on vectors
- Date: Fri, 09 Oct 2009 19:23:55 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
- [Coq-Club] Pattern matching on vectors, Jeff Vaughan
- Message not available
- Re: [Coq-Club] Pattern matching on vectors, Jeff Vaughan
- Re: [Coq-Club] Pattern matching on vectors, Adam Chlipala
- Re: [Coq-Club] Pattern matching on vectors,
Laurent Théry
- Re: [Coq-Club] Pattern matching on vectors, Benedikt . AHRENS
- Re: [Coq-Club] Pattern matching on vectors, Jeff Vaughan
- Re: [Coq-Club] Pattern matching on vectors, Matthieu Sozeau
- Re: [Coq-Club] Pattern matching on vectors for dummies, Jean-Francois Monin
- Re: [Coq-Club] Pattern matching on vectors, Benedikt . AHRENS
- Re: [Coq-Club] Pattern matching on vectors, Adam Koprowski
- Message not available
Archive powered by MhonArc 2.6.16.