Ssreflect Users Discussion List

[Frédéric Chyzak <>]

I have a general trouble when facing a notation.  I won't question the need 
for them here, but rather the consistency of choices.


I think I can understand the choices in:

(*       [set x | C] == the A containing the x such that C holds (x is bound  
(*                      in C).                                                
(*     [set x \in D] == the A containing the x in the collective predicate D. 
(* [set x \in D | C] == the A containing the x in D such that C holds.        

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.    
(*     [ \/ P1 , P2 | P3 ] == multiway logical disjunction, up to 4 terms.    
(*        [&& a, b, c & d] == iterated, right associative boolean conjunction 

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


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

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

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


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?

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

Frédéric