The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

Le Thu, 19 Jan 2012 16:00:23 -0800,
Daniel Schepler 
<dschepler AT gmail.com>
 a écrit :

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

I guess the following is not an option, but well…
✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ 
Definition ignore {A B:Type} (x:A) (y:B) := y.
Notation "… y …" := (ignore _ y).
 (*Don't bother with inputing '…', since it will only be used
   for printing and not parsing; this kind of notation is really
   not convenient as the printed term won't be reparsable.
   If you need to keep reparsable, deactivate this notation.*)

Definition vector_hd {X:Type} {n:nat}
  (v:vector X (S n)) : X :=
vectorS_match v as v' return (ignore (v':vector X _)) X with
| vector_cons h t => (ignore t) h (*oh! the ugly trick occurs here*)
end.

Definition vector_tl {X:Type} {n:nat}
  (v:vector X (S n)) : vector X n :=
vectorS_match v as v' return (ignore v') (vector X n) with
| vector_cons h t => (ignore h) t (*and also here*)
end.

(*A haskell '$' notation would be useful here for 'ignore';
  that is allow to write "ignore a $ ignore b $ term"
  instead of "ignore a (ignore b (term))"*)

Print vector_hd.
Print vector_tl.

(*Note also that "simpl" may break the system, as it may reduce
  the "ignore" calls, and thus reintroduce the "_".
  So it may be better to make it opaque*)
✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ 

By the way, I remember that some months (year?) ago, you said that
you never had problems with the "inversion" tactic. Did you changed
your mind, or do you just want to write terms to compute without using
the tactic system?