[ add ] injectivity of suc for relation m ≡ n (mod o) for {{NonZero o}}

[jamesmckinna]

Taken from the discussion at https://agda.zulipchat.com/#narrow/channel/264623-stdlib/topic/suc.20injective.20under.20_.25_/with/582024092 :

• introduces definition m ≲%[ o ] n = ∃ λ k → n ≡ m + k * o
• characterises the relation m % o ≡ n % o in terms of (the symmetric closure of) m ≲%[ o ] n
• gives two proofs of 'Carette's Lemma' (suc m) % o ≡ (suc n) % o → m % o ≡ n % o
  • indirect, via the characterisation, using a new lemma about SymClosure
  • direct, via a slick proof due to @alexarice

Possible TODO:

• prove that _≲%[ o ]_ satisfies IsPreorder _≡_, indeed IsPartialOrder _≡_ etc. (decidable, ...)
• relate this to Modular arithmetic in terms of ideals #2729 and friends, esp. Create a version of [m+kn]%n≡m%n for integers #2877

[jamesmckinna]

Last commit tidies up notations etc.
Still can't quite make the proof carettesLemma delegate via a suitable combinator to ≲%[o]⇒≡[o]% ∘ ≲%[o]-suc⁻¹ but this will have to do, I guess. Suggestions welcome!

[alexarice]

I'm unsure if it would actually make anything easier, but an alternative definition here is:

Suggested change

	m ≡%[ o ] n = SymClosure _≲%[ o ]_ m n
	m ≡%[ o ] n = ∃ λ k → ∃ λ k' → m + k * o ≡ n + k' * o

[jamesmckinna]

Nice observation!

(Give relation R, the (relational) composition of R with flip R is automatically symmetric, moreover transitive if flip R . R is contained in the identity , ie R is functional, as in this instance... and then R + flip R being equivalent to flip R . R is a further stronger invariant... but does this help in proving @JacquesCarette 's lemma?)

[jamesmckinna]

Last commit tidies up notations etc. Still can't quite make the proof carettesLemma delegate via a suitable combinator to ≲%[o]⇒≡[o]% ∘ ≲%[o]-suc⁻¹ but this will have to do, I guess. Suggestions welcome!

Can now: by generalising SymClosure.gmap! Final commit closes this last niggle.

[gallais]

What's the mnemonic for the placement of the % sign in this notation vs.
the previous one. I don't think I could predict where it's supposed to go.

Should we have a theory of

_≡[_]_ : ∀ (m : A) (A -> B) (n : A) → Set _
m ≡[ f ] n = (_≡_ on f) m n

and then be this just be _≡[ (_% o) ]_?

[jamesmckinna]

Re: naming.

No, you're absolutely correct that these names are suboptimal! Thank supernatural realms for the review process... and on a more human plane, for your intervention here.

I think I'll try instead

• _≡%[_]_ for m ≡%[ o ] n = m % o ≡ n % o
• _≅%[_]_ for m ≅%[ o ] n = SymClosure _≲%[ o ]_ m n

on the basis that

• ≅ seems like a plausible symbol for the symmetrisation of of a given ≲
• both relations now get % preceding the actual modulus o

Is that any better?

[jamesmckinna]

As for the more general 'quotient by f' equivalence relation, I'm more hesitant to pursue that, for two reasons:

• _% isn't the general f you seek, because of the usual... weirdness about NonZero o witnesses
• @Taneb 's Add ideals and quotient rings #2855 introduces different notation for the quotient relation, and (eventually?) we might see a suitable reconciliation, but I didn't want to prematurely commit to any eventual resolution of those decisions...?

[jamesmckinna]

This proof could be refactored in terms of Relation.Binary.Consequences.wlog, but my first attempt ended up more verbose and harder to read than this version. But perhaps eventually that combinator will be reimplemented, and with it, a suitable refactoring of this lemma.

[jamesmckinna]

Notwithstanding that wlog can be used, I think the above proof is easier to read.

[gallais]

This feels like wlog even more so because _≅%[_]_ is freely symmetric and so it should be (for once!) easy to invoke!

[jamesmckinna]

Well, indeed. But see above... will see what I can do.

[jamesmckinna]

Have done so, but it's a horrible proof, so verbose!
I would really claim it's not an improvement.

[jamesmckinna]

@JacquesCarette hope I've addressed all your feedback
@gallais feel free to insist on the wlog proof, but I think the direct one is better!