Ssreflect Users Discussion List

[Assia Mahboubi <>]

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
>