Numeric non-zero equivalents/Redesign of Almost* properties in Algebra.Definitions
#2117
Conversation
|
Oops, pushed before |
| -- `Relation.Binary.Core` use *implicit* quantification... so there is | ||
| -- plenty of potential for later/downstream refactoring of this design | ||
|
|
||
| module Monotonicity {ℓ₁ ℓ₂} (_≤₁_ : Rel A ℓ₁) (_≤₂_ : Rel A ℓ₂) where |
There was a problem hiding this comment.
You've probably realized this, but so it doesn't get forgotten: these definitions don't use _≈_ but are passed it anyway. We should have files Algebra.Definitions.Monotonicity and Algebra.Definitions.Cancellativity to avoid this if we keep these
There was a problem hiding this comment.
Good point, and I had, indeed, overlooked this aspect of the design, in favour of trying to work out in eg Data.Rational.Properties how to selectively instantiate Definitions at various points with relations other than equality... on the analogy with *-Reasoning modules...
| Monotone₁ f = ∀ x y → x ≤₁ y → (_≤₂_ on f) x y | ||
|
|
||
| Monotone₂ : Op₂ A → Set _ | ||
| Monotone₂ _∙_ = ∀ x y u v → x ≤₁ y → u ≤₁ v → (x ∙ u) ≤₂ (y ∙ v) |
There was a problem hiding this comment.
This looks very similar to Congruent₂ to me. I wonder if there's something there.
There was a problem hiding this comment.
Well, you're correct, of course, but this is precisely because the Congruent*/Relation.Binary.Preserves* properties use implicit quantification (because the relation instances can be inferred by the typechecker), distinct from the design decision made in issue #1436 to make the Cancellative properties take explicit arguments. I chose Monotone etc. because at one stage I was trying to have a single design in which both the Monotone and Cancellative definitions could be derived from a single family. But it required a fair amount of _on_ gymnastics, plus redundant uses of id, so then I decided to inline everything by hand.
But the general point: we almost never use Congruent*, but definitely do use Monotone a lot, still stands.
So I would pleased if this specimen design prompts a wider rethink. There are a number of outstanding issues even in the v2.0 milestone which I think could be tackled with a design along these lines, if we could only think about it enough and agree... so this contribution is offered up towards such an end.
…gda-stdlib into NumericNonZeroEquivalents
| @@ -183,6 +183,12 @@ nonNegative : ∀ {i} → i ≥ 0ℤ → NonNegative i | |||
| nonNegative {+0} _ = _ | |||
| nonNegative {+[1+ n ]} _ = _ | |||
|
|
|||
| -- Destructors -- mostly see `Data.Integer.Properties` | |||
|
|
|||
| ≢-nonZero⁻¹ : ∀ i → .{{NonZero i}} → i ≢ 0ℤ | |||
There was a problem hiding this comment.
Should i be implicit here? (ditto. all the subsequent lemmas of related form)
| ≢-nonZero⁻¹ : ∀ p → .{{NonZero p}} → p ≢ 0ℚ | ||
| ≢-nonZero⁻¹ _ ⦃ () ⦄ refl |
There was a problem hiding this comment.
This is a good example of why/how p could/should be implicit?
| ≄-nonZero⁻¹ : ∀ p → .{{NonZero p}} → ¬ (p ≃ 0ℚ) | ||
| ≄-nonZero⁻¹ p eq = ≢-nonZero⁻¹ p (≃⇒≡ eq) |
There was a problem hiding this comment.
Infectively so.
| ≢-nonZero⁻¹ : ∀ p → .{{NonZero p}} → p ≢ 0ℚᵘ | ||
| ≢-nonZero⁻¹ _ ⦃ () ⦄ refl |
| ≢-nonZero⁻¹ +0 ⦃ () ⦄ | ||
| ≢-nonZero⁻¹ +[1+ n ] () |
There was a problem hiding this comment.
This being the only instance where there is more than one clause to consider...
| @@ -523,14 +526,6 @@ Non-backwards compatible changes | |||
| - From: `∀ {x} y z → (y • x) ≈ (z • x) → y ≈ z` | |||
| - To: `∀ x y z → (y • x) ≈ (z • x) → y ≈ z` | |||
|
|
|||
There was a problem hiding this comment.
I've removed the existing text regarding Almost*Cancellative, in the absence of a stable story emerging about how it should be replaced. But this comment is a placeholder TODO so...
DRAFT: for discussion.
See my recent comments on/regarding #1175 #1436 #1562 #1579...
... with the usual caveat that I'm trying to do two things in one with this, and should step back and factor them out.
TODO: plenty!
NB: breaking change in types of
Cancellativeproperties, due to slightly unorthodox, non-prenex as regardsCarrierelements, quantifier order...