The Coq mailing list

[Benedikt.AHRENS AT unice.fr]

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