[ refactor ] Restate, and use, the definitions of Monotonic etc. operations
#2580
Conversation
|
Thanks - these already are easier to understand. |
|
How do I remove #1579 from the |
Not sure how you did it, but it's gone for me 🎉 |
| mono⇒cong sym reflexive antisym mono x≈y = antisym | ||
| (mono (reflexive x≈y)) | ||
| (mono (reflexive (sym x≈y))) | ||
|
|
||
| antimono⇒cong : Symmetric ≈₁ → ≈₁ ⇒ ≤₁ → Antisymmetric ≈₂ ≤₂ → | ||
| ∀ {f} → f Preserves ≤₁ ⟶ (flip ≤₂) → f Preserves ≈₁ ⟶ ≈₂ | ||
| ∀ {f} → f Preserves ≤₁ ⟶ (flip ≤₂) → Monotonic₁ ≈₁ ≈₂ f |
There was a problem hiding this comment.
This unfortunately is stated so as not to be able to exploit the refactoring redefinition of Antitonic₁ in Relation.Binary.Definitions below (wrong relation gets flipped!). Downstream refactoring?
|
Now that the abstract definitions are mostly in place, can look at the instantiations in |
|
Remark: all of the |
|
So this should now be ready, modulo:
|
src/Data/Nat/Properties.agda
Outdated
| *-monoʳ-≤ : ∀ n → (n *_) Preserves _≤_ ⟶ _≤_ | ||
| *-monoʳ-≤ n m≤o = *-mono-≤ (≤-refl {n}) m≤o | ||
| *-monoʳ-≤ : LeftMonotonic _≤_ _≤_ _*_ | ||
| *-monoʳ-≤ = mono₂⇒monoˡ {≤₁ = _≤_} {≤₂ = _≤_} {≤₃ = _≤_} ≤-refl *-mono-≤ |
There was a problem hiding this comment.
This providing of implicits is annoying. Suggests that some of them should be explicit in the proof?
There was a problem hiding this comment.
Yes, I've been scratching my head over how it might be avoided... without a conclusion yet.
There was a problem hiding this comment.
So if you make all 3 underscores, which ones are yellow? I notice that the previous proof provided the n explicitly, might that work here as well?
There was a problem hiding this comment.
It seems that only {≤₃ = _≤_} is required here...
There was a problem hiding this comment.
Aaargh: there's a difference depending on whether we consider left or right, presumably because of the left-biased implementations. Will need to investigate further. Sigh.
*-monoˡ-≤ : RightMonotonic _≤_ _≤_ _*_
*-monoˡ-≤ = mono₂⇒monoʳ {≤₃ = _≤_} ≤-refl *-mono-≤
*-monoʳ-≤ : LeftMonotonic _≤_ _≤_ _*_
*-monoʳ-≤ = mono₂⇒monoˡ {≤₁ = _≤_} {≤₂ = _≤_} {≤₃ = _≤_} ≤-refl *-mono-≤
src/Data/Nat/Properties.agda
Outdated
| +-monoʳ-≤ : ∀ n → (n +_) Preserves _≤_ ⟶ _≤_ | ||
| +-monoʳ-≤ n m≤o = +-mono-≤ (≤-refl {n}) m≤o | ||
| +-monoʳ-≤ : LeftMonotonic _≤_ _≤_ _+_ | ||
| +-monoʳ-≤ = mono₂⇒monoˡ {≤₃ = _≤_} ≤-refl +-mono-≤ |
There was a problem hiding this comment.
But here just 1 suffices:
+-monoˡ-≤ : RightMonotonic _≤_ _≤_ _+_
+-monoˡ-≤ = mono₂⇒monoʳ {≤₃ = _≤_} ≤-refl +-mono-≤
+-monoʳ-≤ : LeftMonotonic _≤_ _≤_ _+_
+-monoʳ-≤ = mono₂⇒monoˡ {≤₃ = _≤_} ≤-refl +-mono-≤
|
I'll resolve the merge conflict later, meanwhile tricky questions above needing more thought... ;-)... so have converted back to DRAFT. |
| sel⇒idem sel x = reduce (sel x x) | ||
|
|
||
| module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where | ||
| module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) (open Definitions _≈_) where |
There was a problem hiding this comment.
why put the open Definitions in the module telescope instead of on the line below?
There was a problem hiding this comment.
Because in each case, my conviction is:
- it's easier to read the hypotheses and statements, without the noise of the additional
_≈_arguments - that this is further weight towards my proposed refactoring in Refactor
Algebra.Consequences.*? #2502 / [ refactor ] Add equality as a parameter toAlgebra.Consequences.Base#2572
with the latter being on the model of how Algebra.Definitions is imported instantiated by _≈_ in Algebra.Structures etc.
There was a problem hiding this comment.
I think you misunderstood my point. I want that open there, just inside the module instead of in the telescope!
There was a problem hiding this comment.
OK, but I had been maintaining consistency with the other two, where the open declaration is required in the module telescope, in order to be able to state the hypotheses without reference to equality...
src/Data/Nat/Properties.agda
Outdated
| *-monoʳ-≤ : ∀ n → (n *_) Preserves _≤_ ⟶ _≤_ | ||
| *-monoʳ-≤ n m≤o = *-mono-≤ (≤-refl {n}) m≤o | ||
| *-monoʳ-≤ : LeftMonotonic _≤_ _≤_ _*_ | ||
| *-monoʳ-≤ = mono₂⇒monoˡ {≤₁ = _≤_} {≤₂ = _≤_} {≤₃ = _≤_} ≤-refl *-mono-≤ |
There was a problem hiding this comment.
So if you make all 3 underscores, which ones are yellow? I notice that the previous proof provided the n explicitly, might that work here as well?
Aim: towards tackling #1579
TODO:
Data.Nat.*UPDATED: unsolved metas suggest some more revision is necessary :-(Data.Integer.*Data.Rational.*breakingchanges (v3.0: separate PR once the rest is done?)