Standardise implicit arguments of cancellation properties.

[FR-vdash-bot]

In Algebra.Definitions

LeftCancellative _•_ = ∀ x {y z} → (x • y) ≈ (x • z) → y ≈ z
RightCancellative _•_ = ∀ {x} y z → (y • x) ≈ (z • x) → y ≈ z
AlmostLeftCancellative e _•_ = ∀ {x} y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z
AlmostRightCancellative e _•_ = ∀ {x} y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z

In Data.Rational.Unnormalised.Properties

+-cancelˡ : ∀ {r p q} → r + p ≃ r + q → p ≃ q
+-cancelʳ : ∀ {r p q} → p + r ≃ q + r → p ≃ q

Perhaps we should make them uniform.

[MatthewDaggitt]

Hey, thanks for the spot! Yup, so for starters the rational proofs should be using the LeftCancellative and RightCancellative types.

As for the AlmostX and X definitions, the reason for the differences in the implicits is Agda's ability to infer them. LeftCancellative and RightCancellative were introduced early on in the library's life and the implicit arguments are slightly broken, see the code below. To fix this I think none of the arguments to those definitions should be implicit. The Almost versions were introduced very recently and I think have the right implicits (x is inferrable from the equality).

open import Data.Rational.Base
open import Algebra.Definitions
open import Relation.Binary.PropositionalEquality.Core

postulate
  rc : RightCancellative _≡_ _+_
  arc : AlmostRightCancellative _≡_ 0ℚ _+_
  x y z : ℚ
  x≢0 : x ≢ 0ℚ
  eq : y + x ≡ z + x

-- Inference error
test : y ≡ z
test = rc y z eq

-- No inference error
test2 : y ≡ z
test2 = arc y z x≢0 eq

Therefore I think the correct definitions are:

LeftCancellative _•_ = ∀ x y z → (x • y) ≈ (x • z) → y ≈ z
RightCancellative _•_ = ∀ x y z → (y • x) ≈ (z • x) → y ≈ z
AlmostLeftCancellative e _•_ = ∀ {x} y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z
AlmostRightCancellative e _•_ = ∀ {x} y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z

but we will need to wait until v2.0 to make such a breaking change.

[FR-vdash-bot]

I have just noticed something similar.

In Data.Nat.Properties

≤-stepsˡ : ∀ {m n} o → m ≤ n → m ≤ o + n
≤-stepsʳ : ∀ {m n} o → m ≤ n → m ≤ n + o
m≤m+n : ∀ m n → m ≤ m + n
m≤n+m : ∀ m n → m ≤ n + m

In Data.Integer.Properties

≤-steps : ∀ {m n} p → m ≤ n → m ≤ + p + n
m≤m+n : ∀ {m} n → m ≤ m + + n
n≤m+n : ∀ m {n} → n ≤ + m + n

In Data.Rational.Unnormalised.Properties

≤-steps : ∀ {p q r} → NonNegative r → p ≤ q → p ≤ r + q
p≤p+q : ∀ {p q} → NonNegative q → p ≤ p + q
p≤q+p : ∀ {p} → NonNegative p → ∀ {q} → q ≤ p + q

[MatthewDaggitt]

Okay so

• we should be explicit everywhere in Algebra.Definitions
• we should change Data.Rational.Properties (and elsewhere) to be use those definitions

[MatthewDaggitt]

We should check that the subsequent inconsistencies in Data.Nat/Integer/Rational.Properties been resolved by the NonZero rewrite everywhere, as their types have changed.

[JacquesCarette]

So there's a problem with using the definitions in Data.Rational.Properties: the notion of NonZero that it uses is different than the notion that AlmostLeftCancellative uses. So I'm not sure we can make that change. To make things consistent, what we'd need to do is to parametrize AlmostLeftCancellative by a "non zero" predicate.

Also, by inconsistencies, do you mean like the ones pointed out above regarding implicit/explicit? For example, in ≤-stepsˡ it does make sense to make them implicit, as they'll always be inferable. So I'm not quite sure what to do for part 2 of this.

[jamesmckinna]

Is there a common resolution available of this issue with (the implied need for non-zeroness distinct from NonZero brought up by) #1562? And #1175?

Eg. see developing branch towards a possible PR...

... where I will shortly push some breaking (and speculative) changes.

[JacquesCarette]

While I'm assigned this (and I don't mind), right now, I'm not quite sure what ought to be done. It feels like enough things have "moved underneath" that I'm not sure what is feasible / outstanding. Especially given some of @jamesmckinna 's work in #1562 , #1579 and #2117 .

[jamesmckinna]

Fair enough! Plus I have mentally timed out on a lot of this issue since those PRs, and more importantly, the post-v2.0 cycle of development I'm currently working on...

Ping me on Zulip if you want me to try to page this back in...

[jamesmckinna]

[Summarising comments I made to @JacquesCarette on Zulip]

• I think Numeric non-zero equivalents/Redesign of Almost* properties in Algebra.Definitions #2117 was a bit too ambitious in trying to reconcile the Monotone and Cancellative families of properties, so that should be abandoned (until at least v3.0 if not beyond...)
• I agree with the (existing) approach of having the Almost* properties defined in terms of the (negation of the) underlying equality, and hence with any agreed version of what the implicit/explicit quantification should be, as discussed above

But that said, I think that the concrete arithmetic datatypes present a different challenge, namely that the corresponding Almost* properties (probably) also need separate versions where the ¬ x ≈ e precondition is replaced by .{{ NonZero x }}... because

• the mode-of-use of NonZero for the numeric types is typically as an (irrelevant) instance (eg paradigmatically for this issue the already-defined *-cancelʳ-≡ : ∀ m n o .{{_ : NonZero o}} → m * o ≡ n * o → m ≡ n in Data.Nat.Properties)
• Agda, AFAIK, doesn't admit a form of property statement which would allow the above, and ∀ m n o → o ≢ 0 → m * o ≡ n * o → m ≡ n to be specific instantiations of some hypothetical common AlmostRightCancellativeP : Pred A _ → Op₂ A → Set _ AlmostRightCancellativeP P _•_ = ∀ x y z → P x → (y • x) ≈ (z • x) → y ≈ z, because of the instance brackets... (the irrelevance annotation can be handled separately via recompute; see below)

So: it seems as though two parallel strands of definitions are required, one with the quantified instance, one with the _ ≉ 0# precondition... which does seems annoying, even if we prove a lemma (in Algebra.Consequences) of the form relating the two definitions when there is an ambient proof that NonZero x → x ≉ 0#... as is the case for all the concrete datatypes (cf. Biased implementations in the Algebra hierarchy)

Worse (as regards duplication) it is going to be typically again the case that the .{{ NonZero ... }} version will be the one that clients will want to use for the concrete types, in order to exploit instance-based reasoning for 'boring' predicates such as NonZero... but from which behaviour abstract algebraic structures won't be able to profit.

The only conceivable (to me, at least ;-)) unification (in terms of a hypothetical AlmostRightCancellativeP as above) might be to take P = NonZero for the concrete datatypes, and then use Relation.Nullary.Decidable.Core.recompute gymnastics to turn such instantiations into the corresponding irrelevant instance-based statement, because all the relevant concrete NonZero predicates are decidable.

But that still doesn't solve the problem of such derived statements nevertheless needing a consistent form... and we are/seem to be back to duplication of the statement (template) again... sigh.

[jamesmckinna]

One possible alternative statement, but which then still requires some specialisation for the concrete case, would be to rephrase AlmostCancellative in 'positive' constructive style, viz. as ∀ x y z → (x ≈ e) ⊎ (x • y) ≈ (x • z) → y ≈ z (and thereby avoiding @JacquesCarette 's aversion to negated Setoid equality as a code smell)... but that still doesn't seem to avoid the duplication problem...

[jamesmckinna]

Unless, perhaps, we...

• either bite the bullet, and only accept AlmostCancellative statements for concrete algebras (seems bad)
• or, introduce new Algebra.Structures... (apologies for the sketchiness of the sketch)

record NonZero (0# : A) : Set _ where
  field
    NonZero : Pred A _
    nonZero-≢ : NonZero ⇒ (_≉ 0#)
    nonZero-≢⁻¹ : (_≉ 0#) ⇒ NonZero

record DecNonZero (0# : A) : Set _ where
  field
    nonZero : NonZero 0#
    nonZero? : Unary.Decidable NonZero

record AlmostCancellative (_∙_ : Op₂ A) : Set _ where
  field
    cancellative : AlmostCancellative _∙_

module NonZeroCancellative (NZ : NonZero 0#) where

  record AlmostCancellativeNZ (_∙_ : Op₂ A) : Set _ where
    field
      cancellative : AlmostCancellativeNZ _∙_ -- '.{{NonZero x}} version'

    almostCancellative : AlmostCancellative _∙_
    almostCancellative = ...

etc. ? (Modulo better choices of names... apologies for any unintended confusion potentially introduced by poor choice of names above... TL;DR: instead of Consequences, introduced a record which reified possession of a sound-and-complete NonZero implementation, plus a record which witnesses each kind of the AlmostCancellable property, with one having a Biased-style implementation of the other...)

[MatthewDaggitt]

Yes, I think at this point I don't see how to avoid duplication... It's all very unsatisfying and I feel that we're missing something. As a hunch, I would say we're running up into the lack of ability to be generic over modalities (e.g. irrelevance)....

[JacquesCarette]

So I'm going to take myself off of this issue. It seemed straightforward when I put my name down, but clearly it isn't. Right now, I really don't think there is anything that could be done for v2.2. I'm not even sure there is something sensible we can do for v3.0!

[jamesmckinna]

Commiserations @JacquesCarette ! This does seem a 'wicked' problem... so I wonder if one way to "show the fly the way out of the bottle" would be to separate concerns:

• rectify the types/quantification in the Cancellative properties (should be easy?)
• punt the question of how best to formalise the abstract AlmostCancellative (more discussion required as a separate issue; I'd favour the constructively stronger formulation with disjunction, and then for Decidable (_≈ e) show equivalence with the existing property, but that's moot), and not even try to rephrase the .{{NonZero _}} versions for concrete datatypes in terms of the abstract? (Besides making the implicit/explicit quantification consistent?)

[jamesmckinna]

After the discussion above, and following recent discussion on #2554 I'd propose doubling down on my suggestion(s) above, and have

• AlmostLeftCancellative = ∀ x y z → (x ≈ e) ⊎ (x • y) ≈ (x • z) → y ≈ z (resp. Right etc.)
• define the corresponding .{{NonZero x}} versions for the concrete numeric types (as Matthew points out, the duplication seems inevitable?)
• prove the equivalence(s)

The only real question would then be where would such proofs be given? generically, under Algebra.Consequences (or wherever such things should end up... #2502 ), or 'locally' in each Data.*.Properties? I guess the former, to avoid DRY?

[MatthewDaggitt]

I really like the purely algebraic formulation 👍

[jamesmckinna]

Here's my current thinking/a possible re-design/PR route map:

• Define (naming suggestions welcome!), because we will want this for several P (non-zero; positive; negative; ...) in Algebra.Definitions:
  • CancellativeAt x • = ∀ y z → (x • y) ≈ (x • z) → y ≈ z
  • P _-AlmostCancellative_ • = ∀ x → P x ⊎ CancellativeAt x
  • Except_Cancellative_ P • = ∀ {x} → ¬ (P x) → CancellativeAt x
• Prove (in Algebra.Consequences?)
  • P -AlmostCancellative • → Except P Cancellative •
  • Decidable P → Except P Cancellative • → P -AlmostCancellative •
• For Decidable P, we already have .{{P x}} → P x by Relation.Nullary.Decidable.Core.recompute, so we'll use that in place to fix up the generically-stated results for Data.* in terms of the irrelevant instance versions...
• Define
  • AlmostCancellative e = (_≈ e) -AlmostCancellative_
  • (Also? NonZeroCancellative e = Except (_≈ e) Cancellative_ not sure this even needed in view of the above?)
• Prove, for each of the Data.*.Properties, the corresponding generic P -AlmostCancellative •/AlmostCancellative 0# properties, as now, directly by induction/equational reasoning (noting that the case analyses corresponding to the existing versions will 'fall out' of the pattern-matching analysis?), and then redefine the old versions (with deprecations?) in terms of the generic results and recompute as above.

Does that sound plausible, or too elaborate?

And, for Monotonic, #1579 , the corresponding analyses, with Congruent rather than Cancellative?

PR #2573 attempts to implement the above design, but I still feel a sense of ... defeat wrt the level of abstraction obtained there.
UPDATED: PR makes x explicit even in Except_*Cancellative_ (via the new helper, Provided_*Cancellative_, but perhaps it can/should remain implicit (not always confident that at call-sites, instance inference will fill in the correct argument, so in the spirit of 'being explicit everywhere', have ... done so!)

[jamesmckinna]

Indeed, if #2566 were to get merged, then we could even pull all the _-Almost_*/Except_*_ analysis back to Relation.Binary.Definitions? One day...

[JacquesCarette]

This seems quite reasonable to me. Yes, I can see how this does have a "too elaborate" flavour to it, but the only thing that seems 'extra' is Except_Cancellative_. And I'm not even sure that it is extra.

[jamesmckinna]

As noted on the (new) PR, which tackles only the equational cancellation properties, the generalisations to inversion principles for orderings wrt operations should probably be a separate issue, though clearly one derived from this one. It's a big headache trying to develop a Swiss Army knife generalisation covering all the cases described above... so have abandoned that ambition for the time being.