Ssreflect Users Discussion List

[Pierre Jouvelot <>]

Hello Yves,

Sure. I wanted to use

Lemma big_ord_widen_cond n1 n2 (P : pred nat) (F : nat → R) :
     n1 ≤ n2 →
  \big[op/idx]_(i < n1 | P i) F i
      = \big[op/idx]_(i < n2 | P i && (i < n1)) F i.

but, here, F is supposed to take a nat, while my rewritten function is (now) taking an ordinal.

Thanks.

Pierre

On 2 Apr 2020, at 10:51, Yves Bertot <> wrote:

Hello,

Can you post an example?  In particular, can show one of the lemmas from bigop that you find problematic?

Yves

On 4/2/20 10:41 AM, Pierre Jouvelot wrote:

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