Ssreflect Users Discussion List

[Michael Shulman <>]

Dear Assia,

Thanks very much for your long and thoughtful response.  I see now how
there is a benefit.  I think that for me personally, the disadvantage
in terms of user confusion may outweigh the advantage in terms of
slightly shorter proof scripts; we'll see what the rest of the
HoTT/Coq community thinks.

Best,
Mike

On Mon, Jun 22, 2015 at 4:09 PM, Assia Mahboubi <> 
wrote:
> Hello Mike,
>
> it is great to read you on this list, thanks for posting!
>
> This is a very relevant question. To be honest I have myself felt uneasy at
> first (and more recently while teaching) with this unpleasant variability 
> in the
> display. Yet my own experience is that it is still worth working with it.
>
> Indeed, one thing is to have two objects judgmentally equal (I'll write
> convertible below), and one other is to have the Coq tactics and the 
> heuristic
> algorithms they rely on know about it. And delta-reduction (the name of the
> reduction step consisting in unfolding a definition) is really used as a 
> key in
> several important such algorithms like matching.
>
> Let me try to comment the kind of things that break if you test this 
> approach
> (i.e. posing a definition for ltn, used for the _ < _ notation) in ssrnat.v 
> :
>
> - a proof that n < n.+1 is no longer 'trivial' : you need to unfold the
> definition of _ < _ first (but that's no good reason as you could very well 
> make
> this another Hint Resolve);
>
> - you will need to add a handful of lemmas like :
> Lemma ltn_leq_trans n m p : m < n -> n <= p -> m < p.
>
> which really is an instance of leq_trans, but might now be needed because 
> the
> new head symbol of the conclusion is ltn, not leq (but that could be ok as 
> well
> with a good naming policy, although this is not so trivial a task; for 
> instance
> have a look at ssrnum.v for a taste of the litany of lemmas that should be 
> there
> in that case);
>
> - suppose you want to prove something like (this is a subset of the proof of
> leq_exp2l):
>
> m : nat
> x : nat
> y : nat
> x_gt1 : 1 < x
> ================
> m ^ 0 <= x ^ y
>
> with m, x, y abstract variables.
> In the current version of ssrnat, you can just prove this with the 
> one-liner:
>
>   by rewrite expn_gt0 ltnW.
>
> where
>
> Lemma expn_gt0 m n : (0 < m ^ n) = (0 < m) || (n == 0).
> Lemma ltnW m n : m < n -> m <= n.
>
> because
>
>  i) m ^ 0 is convertible to 1 and therefore the goal is convertible to
>  1 <= x ^ y, which could also be printed 0 < x ^ y. Hence we can rewrite 
> with
> expn_gt0, because the pattern of the rule matches   the goal, which is then
> transformed into
>
> ...
> x_gt1 : 1 < x
> =================
> (0 < x) || (y == 0).
>
>   ii) Now  0 < x is the same as 1 <= x so rewriting with ltnW turns this new
> goal into
>
> ....
> x_gt1 : 1 < x
> =================
> true || (y == 0)
>
> which is itself judgmentally equal to true (up to the is_true coercion 
> inserted
> everywhere), and hence trivially proved.
>
>   iii) Of course a second subgoal has also been generated, requiring a 
> proof that
>
> ....
> x_gt1 : 1 < x
> =================
> 1 < x
>
> which is also trivially proved, hence the success of the prenex 'by' 
> tactical.
>
>
> A script proving this last simple thing is longer if you no more have 
> conversion
> doing the bureaucracy for you and if you need to fiddle with explicit
> folding/unfolding and transitivity steps. And then as the library grows, so 
> does
> the bureaucracy.
>
> One of the design patterns throughout the Mathematical Components library 
> is to
> minimize the size of the script input required from the user in order to 
> prove
> trivial things. And judgmental equality is used pervasively as a small 
> scale,
> on-the-fly, automation device for that purpose. Definitions are thus only 
> added
> when they support a true body of new theory, which is not really the case 
> for
> the strict comparison on nats, compared to the large one.
>
> I agree that S n < m and n <= m are not syntactically equal but I also do 
> not
> think that in this particular case the former expression brings something 
> (in
> terms of properties, theory,...) compared to the later. So you could see 
> this
> variation in the display as a kind of "on the fly normalisation" in the 
> writing.
> Although of course the underlying terms remain the same.
>
> May be other users will have more comments (thanks again for asking on the
> list!). Meanwhile, hope my 5 cents help.
>
> Best,
>
> assia
>
>
>
> Le 22/06/2015 07:32, Michael Shulman a écrit :
>> Hello,
>>
>> In the homotopy type theory Coq library we have started using some of
>> the basic definitions and proofs about natural numbers inspired by
>> SSR.  However there is one thing I am puzzled by: why is "n < m" a
>> Notation for "S n <= m" rather than a Definition?  I appreciate the
>> advantage of having the two be judgmentally equal, but it's not
>> obvious to me why one would want them to be syntactically equal (i.e.
>> without having to unfold a definition).  Moreover, I find it confusing
>> to have hypotheses of the form "S n <= m" automatically transformed
>> into "n < m" (e.g. in the inductive step of an induction on n with a
>> previous hypothesis of "n <= m"); the two are not syntactically equal
>> in my head.  Can someone explain?
>>
>> Thanks!
>> Mike
>>