Pattern matching on vectors

[Jeff Vaughan]

Hi,

I'm trying to prove some simple theorems using types defined in terms of
vectors.  I'm getting suck because I'm not sure how to destruct a vector
when there are constraints on its length.

Vectors are defined as follows:

   Set Implicit Arguments.

   Inductive vector (A: Type): nat -> Type :=
   | vnil: vector A O
   | vcons: forall len, A -> vector A len -> vector A (S len).
   Implicit Arguments vnil [A].

And I would like to prove, for instance, this lemma:

   Lemma openVector: forall A n (v: vector A (S n)),
     exists a, exists v0, v = vcons a v0.

The problem---as I understand it---is that induction
(elim/destruct/generalized induction...) on v produces goals that are
ill-typed.  For instance,

   exists a, exists v0, vnil = vcons a v0

Note that the left hand side of the equality has type (vector A 0) and
the right hand side has type (vector A (S _)).  I tried using John Major
equality.  This let me take a small step forward, but didn't enable real
progress.

Any tips?

Best,
Jeff Vaughan

--------------------------------------------------------
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

[Jeff Vaughan]

Thanks Ryan!

Matthieu Sozeau just replied off list and suggested using
dependent destruction/induction.  Like your proof these tactics also use
JMeq and import an axiom.

Is there any reason to be wary of the JMeq_eq axiom?  Is it possible to
prove such a theorem without JMeq?

Also, when you suggest a fixpoint based version of vectors, do you mean
something like the following?

Fixpoint vec' (A: Type) (n: nat) : Type :=
   match n with
     O => unit
   | S m => A * vec' A m
   end.

Best,
Jeff

Ryan Wisnesky wrote:

> Personally, I think the real moral of the story here is to avoid
> indexing inductive types with terms.  Here's the first  proof I could
> think of:
>
> Inductive vector (A: Type): nat -> Type :=
>  | vnil: vector A O
>  | vcons: forall len, A -> vector A len -> vector A (S len).
>
> Set Implicit Arguments.
> Require Import JMeq.
>
>  Lemma openVector: forall A n (v: vector A (S n)),
>    exists a, exists v0, v = vcons A n a v0.
>  Proof.
>   intros.
>   refine (match v as v' in vector _ n' return S n = n' -> JMeq v v' ->
>             exists a : A, exists v0 : vector A n, v = vcons A n a v0
>             with
>             | vnil => _
>             | vcons n a v0 => _
>           end (refl_equal (S n)) (JMeq_refl v)).
>   intros. discriminate. (* first case is impossible *)
>   intros. assert (n = n0). congruence. subst. clear H.
>   apply JMeq_eq in H0. (* use jmeq axiom *)
>   eauto.
> Qed.
>
> What's happening here is case analysis on v, just like you wanted, but
> there an "as" and "in" clause that tells Coq explicitly how to handle
> the dependency.  The tactics don't generally deal with this well so you
> may need to write proof terms manually like this.  I'd recommend moving
> to a fixpoint version of vector instead.
>
> On Oct 8, 2009, at 6:20 PM, Jeff Vaughan wrote:
>
>> Hi,
>>
>> I'm trying to prove some simple theorems using types defined in terms
>> of vectors.  I'm getting suck because I'm not sure how to destruct a
>> vector when there are constraints on its length.
>>
>> Vectors are defined as follows:
>>
>>  Set Implicit Arguments.
>>
>>  Inductive vector (A: Type): nat -> Type :=
>>  | vnil: vector A O
>>  | vcons: forall len, A -> vector A len -> vector A (S len).
>>  Implicit Arguments vnil [A].
>>
>> And I would like to prove, for instance, this lemma:
>>
>>  Lemma openVector: forall A n (v: vector A (S n)),
>>    exists a, exists v0, v = vcons a v0.
>>
>> The problem---as I understand it---is that induction
>> (elim/destruct/generalized induction...) on v produces goals that are
>> ill-typed.  For instance,
>>
>>  exists a, exists v0, vnil = vcons a v0
>>
>> Note that the left hand side of the equality has type (vector A 0) and
>> the right hand side has type (vector A (S _)).  I tried using John
>> Major equality.  This let me take a small step forward, but didn't
>> enable real progress.
>>
>> Any tips?
>>
>> Best,
>> Jeff Vaughan
>>
>> --------------------------------------------------------
>> 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

[Adam Chlipala-3]

Jeff Vaughan wrote:

> Vectors are defined as follows:
>
>   Set Implicit Arguments.
>
>   Inductive vector (A: Type): nat -> Type :=
>   | vnil: vector A O
>   | vcons: forall len, A -> vector A len -> vector A (S len).
>   Implicit Arguments vnil [A].
>
> And I would like to prove, for instance, this lemma:
>
>   Lemma openVector: forall A n (v: vector A (S n)),
>     exists a, exists v0, v = vcons a v0.

This is one of my favorite examples, because it's easy to prove directly
with a proof term:

Definition openVector A n (v: vector A (S n))
  : exists a, exists v0, v = vcons a v0 :=
    match v in vector _ N return match N return vector A N -> Prop with
                                   | O => fun _ => True
                                   | S n => fun v => exists a, exists
v0, v = vcons a v0
                                 end v with
      | vnil => I
      | vcons _ a v0 => ex_intro _ a (ex_intro _ v0 (refl_equal _))
    end.

I could try to "explain" what's going on here, but it's probably better
to treat this code as a koan and come to your own understanding. :)

--------------------------------------------------------
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

[Laurent Théry-2]

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

[Adam Koprowski]

  Dear Jeff,

  I'd just like to point out that the CoLoR library has a rich set of results on vectors (as an extension to Coq's stdlib). You'll also find Vsn_eq there from which your lemma trivially follows. Hope that helps.

  Cheers,
   Adam

On Fri, Oct 9, 2009 at 00:20, Jeff Vaughan <jeff@...> wrote:

Hi,

I'm trying to prove some simple theorems using types defined in terms of vectors.  I'm getting suck because I'm not sure how to destruct a vector when there are constraints on its length.

Vectors are defined as follows:

 Set Implicit Arguments.

 Inductive vector (A: Type): nat -> Type :=
 | vnil: vector A O
 | vcons: forall len, A -> vector A len -> vector A (S len).
 Implicit Arguments vnil [A].

And I would like to prove, for instance, this lemma:

 Lemma openVector: forall A n (v: vector A (S n)),
   exists a, exists v0, v = vcons a v0.

The problem---as I understand it---is that induction (elim/destruct/generalized induction...) on v produces goals that are ill-typed.  For instance,

 exists a, exists v0, vnil = vcons a v0

Note that the left hand side of the equality has type (vector A 0) and the right hand side has type (vector A (S _)).  I tried using John Major equality.  This let me take a small step forward, but didn't enable real progress.

Any tips?

Best,
Jeff Vaughan

--------------------------------------------------------
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

--
=====================================================
Adam.Koprowski@..., http://www.cs.ru.nl/~Adam.Koprowski
The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================

[Benedikt.AHRENS]

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

[Jeff Vaughan]

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@... 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

--------------------------------------------------------
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

[Matthieu Sozeau]

Le 9 oct. 09 à 13:23, Benedikt.AHRENS@... a écrit :

> 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?

Yes, using [dependent destruction] [1]:

<<
Require Import Bvector Program.Equality.

Lemma is_nil: forall A (v:vector A 0),
        v = Vnil A.
Proof.
intros A v. dependent destruction v. reflexivity.
Qed.
 >>

[1] http://coq.inria.fr/refman/Reference-Manual013.html#dependent-induction-example

-- Matthieu

--------------------------------------------------------
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

[Jean-Francois Monin]

Hello,

Both openVector and is_nil can be proved using tactics
and in a similar way, provided you stick to simple ones:
use "case" instead of "dependent inversion".
Note that "destruct as" does not work either.

Explaining a koan.  Using tactics helps to understand what is going on
step by step.

Here is a detailed script.

Definition openVector_when_S
  (A: Type) (n: nat) : vector A n -> Prop :=
  match n return vector A n -> Prop with
    | O => fun _ => True
    | S n => fun v => exists a, exists v0, v = vcons a v0
  end.

Lemma openVector:
  forall A n (v: vector A (S n)), exists a, exists v0, v = vcons a v0.
Proof.
intros A n v. change (openVector_when_S v). case v; clear v n.
  simpl. exact I.
  intros n a v. simpl. exists a; exists v; reflexivity.
Qed.


Definition is_nil_when_0 (A: Type) (n: nat) : vector A n -> Prop :=
  match n return vector A n -> Prop with
    | O => fun v => v = vnil
    | S n => fun _ => True
  end.

Lemma is_nil: forall A (v: vector A 0), v = vnil.
Proof.
intros A v. change (is_nil_when_0 v). case v; clear v; simpl.
  reflexivity.
  intros n a v; exact I.
Qed.


You get exactly the same terms as with direct code
(up to expansion of the auxiliary definitions, which can
be inlined in the script if you want).
By contrast, dependent inversion provides a much more
complicated term.


An interesting, not necessarily better (look at proof terms)
alternative is to prove both lemmas using a common auxiliary
definition.

Definition decompose (A: Type) (n: nat) : vector A n -> Prop :=
  match n return vector A n -> Prop with
    | O => fun v => v = vnil
    | S n => fun v => exists a, exists v0, v = vcons a v0
  end.

Lemma openVector':
  forall A n (v: vector A (S n)), exists a, exists v0, v = vcons a v0.
Proof.
intros A n v. change (decompose v). case v; clear v n; simpl.
  reflexivity.
  intros n a v. exists a; exists v; reflexivity.
Qed.

(* and similarly for is_nil *)

Regards,
  Jean-Francois

On Fri, Oct 09, 2009 at 07:23:55PM +0200, Benedikt.AHRENS@... 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
>
>

--
Jean-Francois Monin
CNRS-LIAMA, Project FORMES  &  Universite de Grenoble 1

Office 3-605, FIT, Tsinghua University
Haidian District, Beijing 100084, CHINA
Tel: [phone] ext 605
Fax@LIAMA: [phone]

--------------------------------------------------------
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