∸-suc lemma for natural numbers

[pmbittner]

These lemmata wereThis lemma was useful in inductive proofs involving ∸ and ≤ and it seems these two lemmata are this lemma is not yet part of the standard library.

[jamesmckinna]

Thanks for this.
Please remove the duplicate lemma, and fix the other one.

[jamesmckinna]

This might better be called suc-∸ (we tend to favour L-R reading order for lemmas about composition of functions).

Also, following the style-guide precepts about alphabetical mention of specimen names, esp. those bound in variable declarations, the (name and) type of this lemma should probably be

Suggested change

	∸-suc : n ≤ m → suc m ∸ n ≡ suc (m ∸ n)
	suc-∸ : m ≤ n → suc n ∸ m ≡ suc (n ∸ m)

[pmbittner]

I chose ∸-suc as a symmetric name to +-suc and *-suc which look quite similar. I have no problem with a renaming though.

Sorry for getting the variable names wrong, fixed now.

[jamesmckinna]

Let's see what our colleagues say about names!

[JacquesCarette]

Tricky: I prefer James' suggestion, but it's also true that this is consistent with pre-existing names! So I don't know.

[jamesmckinna]

Yes,... maybe I was being too doctrinaire, moreover for a doctrine which is more often honoured in the breach... sigh.

[pmbittner]

I rebased onto master and now an internal CI error occurred (i.e., something in the pipeline, not the agda standard library failed).

[pmbittner]

It seems that ∸-suc is already part of the standard library in terms of +-∸-assoc 1 as well. Sometimes it is not easy to spot whether a theorem you need is already there.... 😅

[jamesmckinna]

It seems that ∸-suc is already part of the standard library in terms of +-∸-assoc 1 as well. Sometimes it is not easy to spot whether a theorem you need is already there.... 😅

Ah! Yes! Good catch.but indeed the combination you describe us a common case, so I'm wondering if it is worth the Fairbairn threshold penalty to include your version as precisely thus instantiating the general case? Not sure, but suggest we perhaps in any case push to c2.4 to allow us all more time to discuss?

[jamesmckinna]

Suggestion:

• we add your lemma (under whatever name ;-))
• we refactor the subsequent proof of +-∸-assoc as follows:

  +-∸-assoc : ∀ m {n o} → o ≤ n → (m + n) ∸ o ≡ m + (n ∸ o)
  +-∸-assoc zero    {n = _} {o = _} _  = refl
  +-∸-assoc (suc m) {n = n} {o = o} le = begin-equality
    suc (m + n) ∸ o   ≡⟨ ∸-suc (m≤n⇒m≤o+n m le) ⟩
    suc ((m + n) ∸ o) ≡⟨ cong suc (+-∸-assoc m le) ⟩
    suc (m + (n ∸ o)) ∎

  which I think is a modest improvement, and the instantiation at m = 1 which occurs twice elsewhere in Data.Nat.Properties can be refactored to use your new lemma.