The Coq mailing list

[Benedikt Ahrens <Benedikt.Ahrens AT unice.fr>]

Hi,

On 26.11.2011 16:43, Eric Finster wrote:
> Based on Adam's response (thanks Adam!) I came up with the following:
> 
>    Fixpoint zero_len_eq (A : Type) n (v : Vect A n) :=
>      match v in (Vect _ n) return (match n with O => identity _ _ | S
> _ => unit end) with
>        | VNil => identity_refl (VNil A)
>        | VCons _ _ _ => tt
>      end.
> 
> Which looks like some good progress.
> 
>    Check zero_len_eq.
> 
>    *******
> 
>    zero_len_eq
>         : forall A : Type,
>           forall n : nat,
>           Vect A n
>           → match n with
>             | 0 => identity (VNil A) (VNil A)
>             | S _ => unit
>             end
> 
> But I still cannot seem to use this to prove the lemma as stated.
> 
>    Lemma zero_len_is_nil_prf (A : Type) (v : Vect A 0) : v = VNil A.
>    Proof.
>      apply (zero_len_eq A O v).
> 
>    ********
>    Error: Impossible to unify "identity (VNil A) (VNil A)" with "v = VNil 
> A".
> 
> Am I asking for too much here?


Your predicate should probably depend on the natural number, as follows:

Fixpoint zero_len_is_nil' (A : Type) n : Vect A n -> Prop :=
  match n return Vect A n -> Prop with
  | 0 => fun v => v = VNil A
  | _ => fun _ => True
  end.

Lemma zero_len_is_nil2 A n : forall v, zero_len_is_nil' A n v.
Proof.
  intros.
  destruct v;
  simpl; auto.
Qed.

Lemma zero_len_is_nil_pa (A : Type) (v : Vect A 0) : v = VNil A.
  assert (H:= zero_len_is_nil2 A 0).
  simpl in H.
  auto.
Qed.


It would be nice to have something like a condensed cheat sheet version
of Adam's book...

Greetings,
benedikt