Ssreflect Users Discussion List

[Cyril Cohen <>]

While I'm here,

On 28/03/2012 00:57, Frédéric Chyzak wrote:
> 1. I understand the name oapp, but not odflt, obind, and omap.  What is the 
> intuition behind those names?

- odflt (dflt : T) (ox : option T) : T
turns an ox of type option T into an element of type T by extracting the 
content
of the option if there is one, or returning a default element dlft.
So odflt is a shorthand for Option.default.

- obind is the "bind" monadic operator on the "option" monad.

- You can understand the name omap by replacing "option" by "list" in its 
type.

> 2. Where is the meaning of Variables sufficiently described to compare the 
> definitions of pcancel and ocancel:
> 
> Variables (rT aT : Type) (f : aT -> rT).
> 
> Definition pcancel g := forall x, g (f x) = Some x.
> 
> Definition ocancel (g : aT -> option rT) h := forall x, oapp h x (g x) = x.
> 
> The signatures of these constants (as obtained by About) suggest me that 
> variables declared by Variables are added to the signature of the 
> definition if 
> they explicitly appear or are made necessary by type inference.  Is this 
> right?
> 
> Is this the wanted behaviour?

Yes, "Section" "Variables" are abstracted out when you "End" a section.
This generalization is calculated definition by definition, and lemma by 
lemma,
and generalizes only over variables that occur in the term. By the way it is
standard Coq and it is briefly documented here :
http://coq.inria.fr/refman/Reference-Manual004.html#@command47

For example you see that pcancel uses f (and thus aT and rT) so it get
generalized over all the section variables when you end the section.
However ocancel uses aT and rT but not f, so there is no unused "f" argument 
in
its definition when you end the section.


> 3. I tried to understand the proof of can_pcan (to try and clarify the 
> implicit nature of f in some but not all definitions).  Seemingly, the 
> source 
> type of f is counter-intuitively named x, which in the beginning of the 
> file is 
> rather the variable at which f is applied.

No, the source type of f is aT. But in this proof you introduce an x which 
happen
to belong to aT, (because it is the x that corresponds to the first argument 
of
the elements of the (pcancel g) type).

Good night this time,
-- 
Cyril