The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

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

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

Office 3-605, FIT, Tsinghua University
Haidian District, Beijing 100084, CHINA
Tel: +86 10 62 79 69 79 ext 605
Fax@LIAMA:
 +86 10 6264 7458