The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

Thanks for your answer which is consistent with your enthousiasm. I
shall retain two issues:

- Dependent types: use of indices vs subset types

At the current stage of the history, it is still painful to program in
the large with datatypes whose constructors carry strong types (such
as "Fin.t n" or "Vector.t A n") rather than with simply-typed
datatypes equipped with side-conditions (such as {m:nat&m<n} or
{l:list A&|l|=n}), and this even though it is more than 15 years ago
that emerged the idea of truly dependently-typed programming (dating
it to Cayenne).

One reason: equality is undecidable, and type theory as it is designed
nowadays only supports the decision of an "intensional" equality, what
amounts to a very limited subset of equality. This is to me a
challenge for the type-theory-based proof assistants to come, here and
elsewhere, to support the automation of larger fragments of
(extensional) equality, whether it is done natively in the logical
foundations (as e.g. was experimented in CoqMT), or as syntactic sugar
(to be thought e.g. as an extension of Sozeau's Equations plugin).

Let me incidentally advocate the exploit of Chung-Kil Hur who
developed his Heq library for the purpose of methodologically reason
with cascades of richly dependent types.

- Methodology: yes, it is important to write robust and fluid scripts,

The ssreflect methodology is not the only approach to come with such
an objective, but it has the advantage to be well-documented,
well-organized, ready-to-use, and to have led to a couple of very
impressive exploits. It deserves to be experimented.

Hugo Herbelin

On Sat, Jul 11, 2015 at 04:57:14PM -0700, John Wiegley wrote:
> >>>>> Hugo Herbelin 
> >>>>> <Hugo.Herbelin AT inria.fr>
> >>>>>  writes:
> 
> > Are you however really sure that the "Search" and the "let:" in the
> > ssreflect package behave essentially differently from the "Search" and the
> > "let '" in current standard Coq?
> 
> I think "Search" in ssreflect can be emulated using SearchAbout, SearchIsos,
> SearchRewrite, etc. I like that Search brings them together into one 
> command,
> which I've bound in Proof General to C-a C-s C-s. For example:
> 
>     (_ = _)                theorems that result in an equality
>     _ (_ = _)              resulting in, or making use of, equality
>     "eq" (_ = _)           " " " with eq in the name
> 
> I've been using Search for long enough now, I can't comment anymore on 
> whether
> standard Coq can do these searches just as easily or not...
> 
> > In any case, I'm curious to know what you exactly intend by "wonderful"!
> 
> It's wonderful because of how versatile it is.  Some examples, from real 
> code:
> 
>   rewrite [(z; H)]lock /range_ltn map_comp (last_map rend) /= last_map 
> -lock /=.
>   rewrite -subn1 -addnBA // leq_plus //.
>   rewrite ![LHS]andbA and_swap !andbA andbC -!andbA
>   rewrite [all]lock -{1}lock /= -lock IHys /= -!andbA.
> 
> I find myself using rewrite quite often, and the many forms of it made
> possible by ssreflect feel very natural and fluid.
> 
> > - strictly speaking, a formalisation methodology: small scale
> >   reflection, and in particular the reflection of decidable
> >   propositions to bool
> 
> Using ssreflect convinced me to use computable bool predicates wherever
> possible, avoiding Prop if unnecessary, and using reflection to move between
> the two as necessary. The only instance of `reflect` I needed to prove 
> myself
> was:
> 
>   reflect (List.Forall a s) (all a s).
> 
> (In order to work with the StronglySorted type from the Coq stdlib).
> 
> > - an extensive library based on this methodology and intensively using
> >   a number of Coq features such as canonical structures for type
> >   inference (more appropriately called nowadays "MathComp" library)
> 
> I don't use MathComp, but I do use seq, fintype, ssrnat, and ssrfun quite a
> bit. The ssreflect "way" convinced me to use a concept of vectors not based 
> on
> constructors, for example, which made some proofs I was having difficulty 
> with
> much simpler. I was later told about n-tuple's in MathComp, but haven't 
> moved
> over to them yet.
> 
> For example, the Fin type in Coq's stdlib gave me all sorts of problems 
> when I
> tried to use it extensively, whereas ssreflect's Ordinal (which simply 
> pairs a
> nat with a predicate) has been far easier, both in proof, and in code where 
> I
> mainly care about the number.
> 
> > - a set of tactics incorporating a number of "cool" original features
> 
> > Would you be kind to clarify for each of these points how they
> > contribute to have "many scenarios which were complex or laborious
> > before have become much simpler to reason about"? I think this would
> > be of interest for the list.
> 
> I'm not sure I have many precise examples to give off-hand. The code I'm
> thinking of as I write this has changed so significantly since switching to
> ssreflect, it's hard to argue that the increase in ease is due solely to 
> that
> one choice. It could also have been due to improvements in thinking induced 
> by
> studying the ssreflect methodology.
> 
> Whatever the reason, I remember -- as a new Coq user -- feeling like I was
> swimming through molasses before I met ssreflect, and then after it became
> simply water: still needing effort and patience, but not too much.
> 
> Lastly, I pretty much ignored context management before ssreflect, relying 
> on
> generated names and having my proofs break constantly. ssreflect makes such
> management a primary task, and gives very convenient tools for doing so, 
> which
> cured that particular problem. It may simply be little things like this, and
> changes in perspective, which have led to this general impression.
> 
> John