An alternative to #1698

[jamesmckinna]

OK... here it is after quite a bit of backtracking and reconsideration. Some possible debating points:

(pro) This PR defines an alternative path to @MatthewDaggitt 's desire for a (much) narrower import dependency for Data.Nat.Induction on Data.Nat.Properties

(pro) That dependency may be localised to a single lemma (so it might be possible to have a 'reduced' version even of this PR)

(pro) The anomalous module Data.Nat.Properties.Core previously required by Data.Fin.Base is now deprecated (and perhaps should have its contents otherwise deleted?)

(pro) Data.Fin.Properties and even Data.Vec.Properties are now (somewhat) improved by using the existing imported pattern matches on the constructors of _≤_ (esp s≤s), making explicit what was previously handled by a destructor-form analysis

(contra) I took some care over this, but the choices I ended up making involve expanding Data.Nat.Base and Data.Nat.Properties with additional (easily) admissible patterns for _<_ (and _<′_) and systematically doing case analysis on proofs of _<_ in terms of those patterns...

(pro) such case analyses are slightly improved over those previously phrased entirely in terms of _≤_, z≤n, and s≤s (and are a more robust basis for change if the definitions in Data.Nat.Base should ever be reconsidered ;-))

(contra) Data.Nat.Properties has grown again, but not by a huge amount, more by way of additional properties of _<_ mirroring those of _≤_, and phrased 'intrinsically' to try to minimise the crosstalk between the at-present coupled definitions of those two concepts

(pro) (?) no deprecations as such (EDITED: besides Data.Nat.Properties.Core obvs.), rather new proofs of old results (plus some resulting knock-on simplifications downstream); so the interface is (broadly) what it was before

(pro/contra?) I have taken the opportunity to experiment with explicitly narrowing the interface of module imports from Dat.Nat.Properties and even Data.Nat.Base in one case which may be more bikeshedding than (strictly) necessary

(contra) the tout ensemble might be regarded as a 'breaking' change, both because of the deprecation; and because it is (somewhat) insistent on drawing attention to the new pattern analyses, even though they were always already there

Oh... and there's probably a ton of work to do with the CHANGELOG... not yet done ;-)

[jamesmckinna]

(contra) I lacked the courage of my convictions to rewrite the proofs of <⇒≤ and ≤⇒< to use the 'new' pattern analysis... which would have involved some redundant recoding

[jamesmckinna]

OK... seems as though I need to remove the definitions from the deprecated module. Makes sense I suppose...

[MatthewDaggitt]

Thanks for this! I've got a paper deadline tomorrow, a talk to write the day after and will need at least a day to recover, but will definitely have a look at this on Friday!

[jamesmckinna]

hmmm... that deprecated module keeps causing a failing test?

[jamesmckinna]

@MatthewDaggitt I, too, have a paper to finish, a talk to give (to you and other people ;-)) on Friday and ... classes to prepare. I made the PR just to take it off/rotate it on my worklist in favour of all the other neglected tasks... so there's no rush here!

[jamesmckinna]

Sorry for the service interruption; I spent last week dealing with a lot of family/personal stuff.
Now I get "Conflicting files" above... what my process in this situation? (agda:master has clearly run ahead of james:pr1698-extended)

[jamesmckinna]

Didn't understand why/how the conflict arose. Appears resolved now.
EDITED: or not...:

[ Violation detected ] src/Codata/Guarded/Stream.agda

Not me, guv'nor. How did this get merged into agda:master?

[jamesmckinna]

So... what's the CHANGELOG idiom for having added pattern synonyms?

[jamesmckinna]

So... now that there is a 'better' proof for <⇒<′, you might very well argue that all of this has been... for nothing, bar the improved proofs of old results available by systematic use of the pattern synonyms. So before considering how best to proceed, is there a way to inline either <⇒<′ or m<1+n⇒m<n∨m≡n so as to removed the dependency on Data.Nat.Properties altogether? That was your original Holy Grail, and it seems like I have taken a very long way around to... not finding it.

[MatthewDaggitt]

So... what's the CHANGELOG idiom for having added pattern synonyms?

I'd just give the whole definition. They're not exactly long.

[MatthewDaggitt]

you might very well argue that all of this has been... for nothing, bar the improved proofs of old results available by systematic use of the pattern synonyms.

I think that's worth it in it's own right 👍

is there a way to inline either <⇒<′ or m<1+n⇒m<n∨m≡n so as to removed the dependency on Data.Nat.Properties altogether? That was your original Holy Grail, and it seems like I have taken a very long way around to... not finding it.

Err none that I can see 😅 but that's okay, grail's aren't traditionally easy to find and I hear that very long journeys are the norm!

[jamesmckinna]

OK, I'll get back to this shortly, if you can clear up two questions:

• which is (to be) the preferred proof of <-WellFounded: via the import of the 'curious lemma', or by appeal to <⇒<′? The 'murder your darlings' heuristic suggests the latter, as does its evident 'naturality'/'desirability'. Any opinions on this?
• I'm genuinely weirded-out by the alleged 'conflict' caused by a file I have not touched: src/Codata/Guarded/Stream.agda, which make test first reported to me as having a whitespace violation,and then pushing it corrected form now seems to generate a conflict over the whitespace. I thought that git's diffing was a tad more sophisticated than that... or has something changed behind the scenes?

[jamesmckinna]

Re: the last point, since when was

<<<<<<< HEAD

=======
>>>>>>> 1798dfce3d2aeb0e0acbddaaba029cc61dc5a31e

a merge conflict???

[jamesmckinna]

Oh... and: removing the old mutual blocks from Data.Nat.Induction?

[jamesmckinna]

Oh, and failing tests for Haskell-CI for ghc-8.2.2 and ghc-8.4.4???

[jamesmckinna]

Hmmm. I think that this Quixotic episode may now be drawing to a close.

[MatthewDaggitt]

which is (to be) the preferred proof of <-WellFounded: via the import of the 'curious lemma', or by appeal to <⇒<′? The 'murder your darlings' heuristic suggests the latter, as does its evident 'naturality'/'desirability'. Any opinions on this?

The former depends on the latter right? So it's much of a muchness. I'd go with the latter.

I'm genuinely weirded-out by the alleged 'conflict' caused by a file I have not touched: src/Codata/Guarded/Stream.agda, which make test first reported to me as having a whitespace violation,and then pushing it corrected form now seems to generate a conflict over the whitespace. I thought that git's diffing was a tad more sophisticated than that... or has something changed behind the scenes?

Git does sometimes flag whitespace changes. I'm not sure why. If it's the only one cropping up then I wouldn't worry too much about it. Thanks for fixing it!

[MatthewDaggitt]

Will merge it in tomorrow if no one has any last thoughts.

[jamesmckinna]

Actually, there are two proofs of the 'curious' lemma; the second proof goes via the equivalence of _<_ and _<′_, but the first is 'purely recursive'. I've left both in, but only noted the first in the CHANGELOG.

[jamesmckinna]

Grrr. Just found some more loose ends from this one. Opened a PR #1734 to resolve.