The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

I've defined an induction-like principle for decomposing vectors of positive 
length (just a single decomposition), and I'm trying to define a match-like 
notation to make functions using the principle prettier.  In the attached 
code, the parsing of the notation goes just fine, and the definition of 
vector_decomp gets pretty-printed using the notation.  However, as of Coq 
8.3pl3, the definitions of vector_hd and vector_tl don't get pretty-printed 
using the notation.  I think maybe the difference is that vector_hd and 
vector_tl have some of the notation's "ident" variables unused in their 
corresponding functions.  It doesn't help to use dummy names for the unused 
variables instead of "_", though.

Is there some way I could define the notation so that it would be used for 
printing in all cases?

Also, is there any way to split the notation and format strings onto multiple 
lines?  I didn't see anything like that in chapter 12 of the manual, or in 
the 
definition of string format in chapter 1.

(I'm going to attach the file, to make sure my mailer doesn't wrap the long 
lines, but I'll also mark it for inline display for mail readers that support 
that feature.)
-- 
Daniel Schepler
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 vector0_inv {X:Type} (P:vector X 0 -> Type)
  (Pnil:P vector_nil) (v:vector X 0) : P v :=
match v as v' in (vector _ m) return
(match m with
 | 0 => True
 | S _ => False
 end ->
 match m as m' return (vector X m' -> Type) with
 | 0 => P
 | S _ => fun _ => Empty_set
 end v') with
| vector_nil => fun _:True => Pnil
| vector_cons _ _ _ => False_rect Empty_set
end I.

Definition vectorS_inv {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 :=
match v as v' in (vector _ m) return
  (forall P':vector X m -> Type,
   match m as m' return
      ((vector X m'->Type) -> Type) with
   | 0 => fun _ => Empty_set
   | S m'' => fun P'' =>
     (forall (h:X) (t:vector X m''),
       P'' (vector_cons h t))
   end P' -> P' v') with
| vector_nil => fun (P:vector X 0 -> Type) (e:Empty_set) =>
    match e return (P vector_nil) with end
| vector_cons n h t => fun (P:vector X (S n) -> Type)
    (Pcons:forall (h':X) (t':vector X n),
       P (vector_cons h' t')) => Pcons h t
end P Pcons.

Lemma vector0_singleton:
  forall (X:Type) (v:vector X 0), v = vector_nil.
Proof.
intros.
induction v using vector0_inv.
reflexivity.
Qed.

Notation "'vector0_match' v 'as' v' 'return' P 'with' | 'vector_nil' => Pnil 
'end'" :=
  (vector0_inv (fun v' => P) Pnil v)
  (v' ident,
   format "'[v' 'vector0_match'  v  'as'  v'  'return'  P  'with' '/' |  
'vector_nil'  =>  Pnil '/' 'end' ']'").

Print vector0_singleton.

Notation "'vectorS_match' v 'as' v' 'return' P 'with' | 'vector_cons' h t => 
Pcons 'end'" :=
  (vectorS_inv (fun v' => P) (fun h t => Pcons) v)
  ( v' ident, h ident, t ident,
   format "'[v' 'vectorS_match'  v  'as'  v'  'return'  P  'with' '/' |  
'vector_cons'  h  t  =>  Pcons '/' 'end' ']'").

Definition vector_hd {X:Type} {n:nat}
  (v:vector X (S n)) : X :=
vectorS_match v as _ return X with
| vector_cons h _ => h
end.

Definition vector_tl {X:Type} {n:nat}
  (v:vector X (S n)) : vector X n :=
vectorS_match v as _ return (vector X n) with
| vector_cons _ t => t
end.

Print vector_hd.
Print vector_tl.

Definition vector_decomp {X:Type} {n:nat}
  (v:vector X (S n)) : { p:X * vector X n |
      let (h,t):=p in vector_cons h t = v } :=
vectorS_match v as v' return
  { p:X * vector X n |
    let (h,t):=p in vector_cons h t = v' } with
| vector_cons h t => exist _ (h, t) (eq_refl _)
end.

Print vector_decomp.

Section compute_tests.

Variables (X:Type) (n:nat) (h:X) (t:vector X n).
Compute (vector_hd (vector_cons h t)).
Compute (vector_tl (vector_cons h t)).
Compute (proj1_sig (vector_decomp (vector_cons h t))).

End compute_tests.

Require Import ExtrOcamlBasic.
Extraction Inline vector0_inv vectorS_inv.
Recursive Extraction vector_hd vector_tl vector_decomp.