Ssreflect Users Discussion List

[Pierre Jouvelot <>]

Hello all,

I'm trying to clean up a proof based on nats by using ordinals; my proof 
relies in part on big_nat_cond. 

When moving to ordinals, I noticed that most lemmas in bigop for ordinals use 
an F with a nat domain instead of the ordinal one I expected, which is making 
the translation less easy than I thought. 

I have two questions:
- What is the rationale for that, since the index (i < n) do use ordinals?
- How can I proceed, since my cleaned-up function F takes ordinals now (it 
used to take nats)?

Thanks for your advice.

Bye,

Pierre

> On 31 Mar 2020, at 11:07, Yves Bertot 
> <>
>  wrote:
> 
> When manipulating ordinals, it is often convenient to only consider the 
> result through the "val" function, this way you go back to working on 
> natural numbers.  When comparing two ordinals of the same type, val_inj 
> will be handy, so that you only have to compare the natural number values.
> 
> When you want to construct an ordinal and delay the need for the proof for 
> later, you can use the function inord.
> 
> (inord k : 'I_n.+1) has value k if (k < n.+1) and 0 otherwise.  If you 
> write a formula that contains inord, you will need to perform proofs at the 
> time you want to reason about the formula, not at the time you write the 
> formula.
> 
> My personal opinion is that using too much of inord is sloppy programming,  
> but this may help in difficult cases.
> 
> With my best,
> 
> Yves
> 
> 
> On 3/31/20 10:40 AM, Pierre Jouvelot wrote:
>> Thanks a lot, Yves, for the explanation.
>> 
>> I note, though, that the use of ordinals ends up sometimes making life a 
>> bit similar to what you mention ;)
>> 
>> Pierre
>> 
>>> On 31 Mar 2020, at 08:54, Yves Bertot 
>>> <>
>>>  wrote:
>>> 
>>> It is a general design principle in many Coq developments to prefer 
>>> functions with exceptional behavior (like subraction with the right hand 
>>> side larger than left hand side returning 0 or division by 0 returning 0) 
>>> to functions that have the usual mathematical meaning, but take an extra 
>>> proof as argument.
>>> 
>>> Functions with proofs as argument are unwieldy in large developments, 
>>> because if you need to write a large expression with several subractions 
>>> in it, you need to show that all subractions are legit even before you 
>>> can start to write the formula.  The fact that you cannot write a formula 
>>> quickly will prevent you from using you mathematical intuition: by the 
>>> time you can write the formula, your mind is already exhausted.
>>> 
>>> In math-components, for the subn function, it has been accepted that 
>>> subtraction has this irregular behavior,  It is documented in most 
>>> cancelation theorems (where the side condition is present, e.g. subnK), 
>>> and the irregular behavior is even used to define the "<=" order on 
>>> natural numbers.
>>> 
>>> Yves
>>> 
>>> 
>>> On 3/25/20 10:34 AM, Pierre Jouvelot wrote:
>>>> Hi everyone,
>>>> 
>>>> When using subtraction on nats, one has to be careful about its 
>>>> "underflow" property, which destroys "distinctness": 1-3 is equal to 1-4 
>>>> (namely 0), and so even though 3 and 4 are distinct, 1-3 and 1-4 are not 
>>>> anymore.
>>>> 
>>>> A "safer" way to handle subtraction, for me, would be something like:
>>>> 
>>>> Definition safe_subn (m n : nat) (_ : n <= m) := m - n.
>>>> 
>>>> My question is: if one only uses safe_subn in one's lemmas, is the 
>>>> "safety" property maintained by all the rewrite rules in ssrnat, i.e., 
>>>> am I assured that no "apparently distinct" terms will end up being 
>>>> equal? I look at some of the rules, and this seems the case, but this is 
>>>> not a foolproof approach :)
>>>> 
>>>> I'm assuming this is what the comment about nosimpl tag in the header of 
>>>> ssrnat.html is about, but I'd like to be sure.
>>>> 
>>>> Thanks in advance for help.
>>>> 
>>>> Bye,
>>>> 
>>>> Pierre