Ssreflect Users Discussion List

[Georges Gonthier <>]

  Always generalizing would make it impossible to chain conditional views. 
After using a view lemma v1 :  C -> reflect b P,
on H: b, it would not be possible to use v2 : P -> Q, because the first 
application would have been generalized from elimTF (v1 ?) H : P to
(fun HC => elimTF (v1 HC) H) : C -> P, which no longer has type P. Not 
generalizing avoids this, and indeed makes it possible to use the
view /(_ _) to strip leading quantifiers from an assumption that has been 
generalized. This feature is used extensively in many parts of the FT proof, 
especially with skolemizing views such as all_sig. If you changed this it 
would be a major incompatibility (and loss of functionality).
   Cheers,
Georges

-----Original Message-----
From:  
[] On Behalf Of Enrico Tassi
Sent: 16 September 2014 13:31
To: 
Subject: [ssreflect] Script refactoring and semantics of view chaining

As per section 9.9, the semantics of move/v1;move/v2 and move=>/v1/v2 is 
slightly different.  In short the automatic generalization of unresolved 
implicit arguments is done only at the end of the chain of views.
To break the chain in two single view application one can just write move=> 
/v1 - /v2.

When one refactors a script he may be tempted to glue two lines and if the 
two lines end/begin with a view application he may inadvertently chain the 
views together and incur into a "mysterious" error.

Now, I have completely forgotten why I coded it this way.  I mean, one could 
generalize after every view.  I recall there was a reason, but my memory 
fails me.

Anyone recalls why?
--
Enrico Tassi