Ssreflect Users Discussion List

[Georges Gonthier <>]

  I'll answer those...

    But why is it needed to have a final "&" or "|" (instead of a comma) in 
the 
    following?

    (*     [ /\ P1 , P2 & P3 ] == multiway logical conjunction, up to 5 
terms.    

   Is there any technical need, or is there anything to understand?

This is purely a workaround for technical limitations of the coq parsing 
technology.

  Another case that I do not understand is:

   (* Purely for aesthetics, we provide two subtypes of collecttive predictes 
   
  (*   qualifier n T == a pred T pretty-printing wrapper. An A : qualifier n 
T  *)
  (*                    coerces to pred_class and thus behaves as a 
collective 
  (*                    predicate, but x \in A and x \notin A are displayed 
as: 
  (*             x \is A and x \isn't A when n = 0,                           
  
  (*         x \is a A and x \isn't a A when n = 1,                           
  
  (*       x \is an A and x \isn't an A when n = 2, respectively.             
  

  Are the different n's just meaningless values to enumerate cases, with no 
  indication of the display (\is vs \is a vs \is an) ?

Mostly, though note that n is the number of letters inserted after the is...
Also, one normally defines such "qualifiers" using the constructors 
documented below,
e.g, Definition monic := [qualify p | lead_coef p == 1].
so the "n" only appears in the type inferred by Coq (but I do try to give 
thorough documentation).

  Do these choices not prevent one from using a/an as a variable name used in 
  place of A?

Not really, you could write x \is (a). But this feature is intended to let 
you use global constants with a cuter syntax, and you should not call a 
global constant "a" or "an".

  (And, by ignorance of Coq: is there no way to use an enumerated type of 
  symbolic constants instead of 0, 1, 2 ?)

There is, but then I'd have to document the type, its constants, worry about 
name clashes with other constants in the library... this seemed overkill for 
a simple tag that the user rarely sees or cares about.

  By the way, I don't understand the definition:

   CoInductive qualifier (q : nat) T := Qualifier of predPredType T.
  How does the information about q remain associated with the defined value?  
I 
  would have understood something like
    ... := Qualifier of predPredType q T
   or
   ... := Qualifier of predPredtype (q, T)
  Does the definition make T depend on q?  If so, how?
  Or, is it that, in Coq, any value stores its type?

T does not depend on q, but qualifier q T does... And yes, the polymorphism 
in Coq is always explicit, so in addition to the predPredType T argument the 
Qualifier constructor also takes the two parameters of the type as arguments. 
T can be inferred from the last argument so will be mad implicit, but q would 
remain explicit. So you could write Qualifier 0 (fun p => lead_coef p == 1) 
for the definition of monic above.

  (Sorry, the definition of predPredType, with Eval hnf in ..., does not 
speak to me.)

Well, it should, to some extent. It's obviously a record, which is being here 
used as a type, so you know you should try again your Eval with a cast:
  Eval hnf in (predPredType nat : Type)
prints
   nat -> bool
which should clarify things. The name itself is actually a pretty good clue 
that predPredType is a (canonical) instance of the predType interface 
structure, for the pred T type. Both pred and predType are documented in the 
header, with further documentation mid-file.
   You should not be overly surprised to find things that are hard to 
understand when you dive straight into the technical code without reading the 
explanatory text, especially in foundation files like ssrbool that must 
fiddle the fine points of the Coq system in order to set things up properly 
for the rest of the library. It's a bit like trying to understand how to use 
your computer by reading the assembly code of the BIOS...

    Good night,
Georges