[ question ] differences between `Reasoning.Binary.Preorder` and `Reasoning.Binary.PartialOrder`?

[jamesmckinna]

All of this infrastructure predates me joining the project, so I'm maybe missing lore about the design, but I'm struck by two (at least!) thoughts/questions about it:

• how, if at all, does PartialOrder reasoning actually operationalise appeals to antisym in order to prove equalities x ≈ y by showing x ≤ y and y ≤ x, specifically, in a _≈⟨ ... ⟩_ step in the middle of a chain of steps?
• are there reasons how/why Preorder reasoning should not be able to support begin-strict-style proofs?

To turn these questions into a feature/refactoring issue/request:

• can/should we refactor Preorder reasoning to be able to support begin-strict syntax?
• can/should we refactor PartialOrder reasoning to support 'antisym reasoning'?

[JacquesCarette]

git blame of those files and (more aptly) the ones it uses (Base/Double and Base/Triple) have largely @MatthewDaggitt 's name all over.

[jamesmckinna]

Thanks @JacquesCarette it was good to be reminded to be less lazy and do some archaeology for myself. I think I'm now clearer about the answer to my first question

* can/should we refactor `Preorder` reasoning to be able to support `begin-strict` syntax?

being: no (though it's a bit of brainworm for me that the NonStrictToStrict relation _<_ derived from an ordering _≤_ somehow ought to have some/enough nice properties to be able to prove instances x < y in a 'chained' way...? UPDATED cf. #1179 and

agda-stdlib/src/Relation/Binary/Construct/StrictToNonStrict.agda

Lines 7 to 9 in d178d4b

	-- Possible TODO: Prove that a conversion ≤ → < → ≤ returns a
	-- relation equivalent to the original one (and similarly for
	-- < → ≤ → <).

While to the second:

* can/should we refactor `PartialOrder` reasoning to support '`antisym` reasoning'? 

Namely to

... operationalise appeals to antisym in order to prove equalities x ≈ y by showing x ≤ y and y ≤ x, specifically, in a _≈⟨ ... ⟩_ step in the middle of a chain of steps?

That seems to require a whole additional piece of design for the syntax/semantics/pragmatics of such a feature.

Is it worth pursuing such a goal? eg to make up a syntax on the spot

...
x ≈⟨ y ≤ x ⟨ x ≤ y ⟩ -- by antisym
y ...

trying to respect the existing polarities of current symbology: the 'backward' step goes in the left-hand placeholder, the 'forward' in the right...

[JacquesCarette]

That seems to require a whole additional piece of design for the syntax/semantics/pragmatics of such a feature.

Indeed it does.

Syntax suggestion (I most definitely do not like the syntax above):

x ≈⟨ y ≤ x && x ≤ y ⟩ -- by antisym
y ...

Whether it is worth doing depends on the actual amount of effort.

[jamesmckinna]

It's a shame that people seem not to like my obviously well-thought-out suggestions for syntax declarations ;-)

Of course, I'm still smarting from the rejection of my earlier suggestion for #1138/ #2160 that in

agda-stdlib/src/Relation/Binary/Reasoning/Syntax.agda

Lines 260 to 266 in d178d4b

	-- Setoid equality syntax
	module ≈-syntax where
	infixr 2 step-≈-⟩ step-≈-⟨
	step-≈-⟩ = forward
	step-≈-⟨ = backward
	syntax step-≈-⟩ x yRz x≈y = x ≈⟨ x≈y ⟩ yRz
	syntax step-≈-⟨ x yRz y≈x = x ≈⟨ y≈x ⟨ yRz

the syntax for 'forward'/'backward' rewriting/reasoning should instead be

      syntax step-≈-⟩ x yRz x≈y = x ≈⟩ x≈y ⟩ yRz
      syntax step-≈-⟨ x yRz y≈x = x ≈⟨ y≈x ⟨ yRz

so that the direction of the angle bracket would cue the direction of reasoning. (BTW: this is a design mistake we can rectify for v3.0 ;-), and if need be, retain the old x ≈⟨ x≈y ⟩ yRz syntax for backwards compatibility UPDATED or even insist that it only be available as syntax when the relation at-hand is symmetric)

Then we could have had (for a suitable defn of antisym-step-≈ in terms of antisym...) a cognate syntax of the form

      syntax antisym-step-≈ x yRz y≈x x≈y = x ≈⟨ y≈x ⟨⟩ x≈y ⟩ yRz

But then again, Wadler's 'minimum ink' design heuristic is perhaps itself A Bit Much to rely on in all circumstances.

[MatthewDaggitt]

So I think the general pattern of the proposed syntax is great, but that we should have a symmetric symbol in the middle. I don't have strong preferences between &&, <> or | etc...

[JacquesCarette]

While I visually like |, it is too easy to mis-interpret it as 'or'. Anything that suggests 'and' is fine with me.

[jamesmckinna]

Quick experiment seems to cause the parser to fall over for my syntax. Boo!

[JC: reverted to original text -- edit was a mistake. A million apologies!]

[jamesmckinna]

I didn't write that last comment!? Boo to whom ever you may be!

[JacquesCarette]

Oh, that is so weird! I wrote that last comment. Why on earth would it attribute it to you? At least the 'Last edited' credits me.

[JacquesCarette]

I'm guessing what happened might be that I mistakenly edited your comment rather than replied to it. Now I need to figure out how to revert that. Clearly never my intent to do that.

[jamesmckinna]

Thanks! All is forgiven. I have been finding recently that I hit Edit instead of Quote reply, and then find myself rapidly trying to reverse out of that awkward spot...

[jamesmckinna]

Anyway, I tried instead:

antisym-step-≈-⟩ : ∀ x {y z} → y IsRelatedTo z → y ≤ x → x ≤ y → x IsRelatedTo z
antisym-step-≈-⟩ x yRz y≤x x≤y = step-≈-⟩ x yRz (antisym x≤y y≤x)

antisym-step-≈-⟨ : ∀ x {y z} → y IsRelatedTo z → x ≤ y → y ≤ x → x IsRelatedTo z
antisym-step-≈-⟨ x yRz x≤y y≤x = step-≈-⟩ x yRz (antisym x≤y y≤x)

syntax antisym-step-≈-⟩ x yRz y≤x x≤y = x ≈⟨ y≤x [] x≤y ⟩ yRz
syntax antisym-step-≈-⟨ x yRz y≤x x≤y = x ≈⟨ x≤y ][ y≤x ⟩ yRz

as possible candidate solutions, after x ≈⟨ y≤x ⟨⟩ x≤y ⟩ yRz and x ≈⟨ x≤y ⟩⟨ y≤x ⟩ yRz were both rejected, and...
... got the same 'unable to parse...' error message.

It seems as though the parser, because it already has ... ≈⟨ ... ⟩ ... as a template to match against, can't entertain the more refined version as a distinct possible parse (and this seems irrespective of the inner 'conjunction-like' symbol we introduce...).

So instead, I tried extending Relation.Binary.Reasoning.PartialOrder with the following

antisym-syntax = antisym
syntax antisym-syntax x≤y y≤x = x≤y ⟨⟩ y≤x

and... bingo!

Still some things to iron out, but see #3057 ... followups there please!