The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Saturday, November 26, 2011 08:10:35 AM Benedikt Ahrens wrote:
> 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

I like to construct a general decomposition principle, in the form of a 
*_rect 
function, and then use that.  For example:

Inductive vector (X:Type) : nat -> Type :=
| vector_nil : vector X 0
| vector_cons : forall n:nat,
  X -> vector X n -> vector X (S n).

Implicit Arguments vector_nil [[X]].
Implicit Arguments vector_cons [[X] [n]].

Definition vector_decomp_T {X:Type} (n:nat)
  : (vector X n -> Type) -> vector X n -> Type :=
match n with
| 0 => fun P v => P vector_nil -> P v
| S m => fun P v =>
  (forall (x0:X) (v0:vector X m),
   P (vector_cons x0 v0)) -> P v
end.

Definition vector_decomp {X:Type} {n:nat}
  (v:vector X n) :
  forall P:vector X n -> Type,
    vector_decomp_T n P v :=
match v as v' in (vector _ n')
  return (forall P':vector X n' -> Type,
          vector_decomp_T n' P' v') with
| vector_nil => fun P' Pnil => Pnil
| vector_cons _ x0 v0 => fun P' Pcons => Pcons x0 v0
end.

Definition vector0_rect {X:Type}
  (P:vector X 0 -> Type) (Pnil:P vector_nil)
  (v:vector X 0) : P v :=
vector_decomp v P Pnil.

Definition vectorS_rect {X:Type} {n:nat}
  (P:vector X (S n) -> Type)
  (Pcons:forall (x:X) (v:vector X n),
    P (vector_cons x v))
  (v:vector X (S n)) : P v :=
vector_decomp v P Pcons.

Definition hd {X:Type} {n:nat} (v:vector X (S n)) : X :=
  vectorS_rect (fun _ => X)
  (fun x _ => x) v.

Definition tl {X:Type} {n:nat} (v:vector X (S n)) :
  vector X n :=
  vectorS_rect (fun _ => vector X n)
  (fun _ v => v) v.

Lemma vector0_nil:
  forall (X:Type) (v:vector X 0), v = vector_nil.
Proof.
inversion v using @vector0_rect.
reflexivity.
Qed.

Lemma vectorS_cons_hd_tl:
  forall (X:Type) (n:nat) (v:vector X (S n)),
  v = vector_cons (hd v) (tl v).
Proof.
inversion v using @vectorS_rect.
simpl.
reflexivity.
Qed.

One disadvantage I see for this definition is that the extraction isn't very 
nice.

One minor question I have about this: why does "inversion using" leave 
hypotheses in the goal, while "inversion" and "induction using" both move the 
hypotheses into the proof context?
-- 
Daniel Schepler