[ refactor ] (more) decidable `Data.Fin.Properties` #2744

jamesmckinna · 2025-06-23T09:34:14Z

This PR refactors some proofs about Decidable predicates on Fin n, to clarify some, and to add others, including some additional syntax, around a independently interesting minimisation principle from which certain others follow.

A downstream refactoring might reconsider these things in terms of specialisation of lemmas in Induction.InfiniteDescent.

Outstanding issue: could be more systematic about use of variables to clean the whole module up?

src/Data/Fin/Properties.agda

jamesmckinna · 2025-06-25T10:31:47Z

Thanks @MatthewDaggitt for the feedback:

regarding lifting out these properties to a new module, that does seem like a good idea
regarding naming/(use of) syntax, indeed there are lots of stylistic questions about the current version.

I'll move to DRAFT for the time being, and remove from v2.3, while I reconsider things.

… module

JacquesCarette

All the code seems fine. Only issues are that things seem to have moved without a good reason to.

src/Data/Fin/Relation/Unary/Decidable.agda

jamesmckinna · 2025-06-26T18:57:18Z

Hmmm... @JacquesCarette the code motion was in response to earlier review comments from @MatthewDaggitt , but maybe I misunderstood his intention. Nevertheless, the Quantification section is necessary for the subsequent decFinSubset and all?/any? definitions... so it seemed cognate to keep them together (esp. given the public re-export in Data.Fin.Properties...)

JacquesCarette · 2025-06-26T19:08:17Z

I had seen some of the conversation. This is why maybe a larger break up (Data.Fin.Properties.Quantification too?) might make more sense. Same with the Effectful stuff, it most definitely does not belong in .Properties.Decidable. The main code motion does make a lot of sense, it just has knock-on consequences.

jamesmckinna · 2025-06-27T07:53:02Z

Last addition: dual version of searchMin so that client use doesn't have to figure out the DNE...

jamesmckinna · 2025-06-29T07:59:13Z

@JacquesCarette If you are happy with the revisions, then we could add this to the v2.3 docket?

JacquesCarette

Not thrilled with where the Effectful have ended up, but not a hill I'm willing to die on.

src/Data/Fin/Relation/Unary/Decidable.agda

MatthewDaggitt · 2025-07-02T07:45:15Z

src/Data/Fin/Relation/Unary/Base.agda

+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Fin.Relation.Unary.Base where


Why do we need this Base module?

MatthewDaggitt · 2025-07-02T07:48:45Z

src/Data/Fin/Relation/Unary/Decidable.agda

+
+------------------------------------------------------------------------
+-- search
+-- a Decidable predicate is either always true, or has a smallest counterexample


Capitalisation and formatting of this header could be better?

MatthewDaggitt · 2025-07-02T07:56:18Z

src/Data/Fin/Relation/Unary/Decidable.agda

+syntax Universal< (λ j → P) i = ∀[ j < i ] P
+
+ExistsMinimalCounterexample : (P : Pred (Fin n) p) → Set p
+ExistsMinimalCounterexample P = ∃[ i ] ¬ P i × ∀[ j < i ] P j


We could just call this MinimalCounterexample? Making this a record with named fields would make it easier to read as well?

Using a record not a bad idea...

MatthewDaggitt · 2025-07-02T07:58:50Z

src/Data/Fin/Relation/Unary/Decidable.agda

+ExistsMinimalCounterexample : (P : Pred (Fin n) p) → Set p
+ExistsMinimalCounterexample P = ∃[ i ] ¬ P i × ∀[ j < i ] P j
+
+syntax ExistsMinimalCounterexample P = μ⟨¬ P ⟩


I'm still kind of against this for readability reasons, but why does this have to be a syntax declaration rather than an ordinary infix declaration?

MatthewDaggitt · 2025-07-02T08:01:34Z

src/Data/Fin/Properties.agda

+
+------------------------------------------------------------------------
+-- Fin
+------------------------------------------------------------------------


Is there a reason this and Bundles have been moved? To be they logically make sense to live at the top of the file as they related to the type itself, rather than functions or relations over it.

MatthewDaggitt · 2025-07-02T08:01:50Z

src/Data/Fin/Properties.agda

+------------------------------------------------------------------------
+
+open import Data.Fin.Relation.Unary.Base public
+open import Data.Fin.Relation.Unary.Decidable public


I'm not convinced about this direction of dependencies.

MatthewDaggitt · 2025-07-02T08:03:39Z

src/Data/Fin/Relation/Unary/Decidable.agda

+
+
+Universal< : Pred (Fin n) p → Pred (Fin n) p
+Universal< P i = (j : Fin′ i) → P (inject j)


Why do we use Fin' and inject here rather than an explicit j < i proof? Generally Fin' is quite difficult to work with.

This is pure legacy! The refactoring here was designed to make an existing (however poorly expressed) statement derivable from something stronger...

MatthewDaggitt · 2025-07-02T08:06:21Z

src/Data/Fin/Relation/Unary/Decidable.agda

+
+syntax ExistsMinimalCounterexample P = μ⟨¬ P ⟩
+
+searchMin : Decidable P → (∀ i → P i) ⊎ ∃[ i ] ¬ P i × ∀[ j < i ] P j


How about calling this searchForCounterexample and the one below searchForWitness?

MatthewDaggitt · 2025-07-03T06:04:40Z

Again has merge conflicts, no one waiting on it particularly and @jamesmckinna is away so bumping to v2.4

jamesmckinna · 2025-07-03T07:16:17Z

Happy to bump! There was enough feedback/pushback on some of the choices I'd made that this one deserves a bit more time/energy/thought.

jamesmckinna · 2025-07-23T08:37:05Z

I'm going to close this one for now, not least because, as is usual for me, the PR tries to do too many things at once:

refactor existing proofs via an intermediate result with 'better' constructive content (disjunction vs. implication from negated antecedent);
introduce new definitions to package such reasoning: bounded quantifiers on Fin (should be introduced separately), with searchForWitness and searchForCounterexample as derived forms;
syntax declarations for the above, by analogy with existing forms under Relation.Unary (but this seems to be more controversial)
code-motion to try to sort out the dependency cycles which attempting all of the above seemed to entail.

It's a mess that I don't quite feel like untangling, except as separate PRs for each of the above, and certainly not now.

JacquesCarette · 2025-08-01T19:46:40Z

(Oops, didn't notice it was subsequently closed before commenting.)

jamesmckinna added 6 commits June 23, 2025 10:00

refactor: avoid indirection via decFinSubset

906c0f6

cosmetic: clarify type

fde3f60

refactor: clarify proof

6832038

add: new definitions

b92e1a9

cosmetic: clarify type

498db73

refactor: clarify proof

53a8d00

jamesmckinna added this to the v2.3 milestone Jun 23, 2025

jamesmckinna added addition refactoring cosmetic labels Jun 23, 2025

jamesmckinna changed the title ~~[ refactor ] decidable Data.Fin.Properties~~ [ refactor ] (more) decidable Data.Fin.Properties Jun 24, 2025

MatthewDaggitt reviewed Jun 25, 2025

View reviewed changes

jamesmckinna marked this pull request as draft June 25, 2025 11:21

add: whitespace

824ccbf

MatthewDaggitt removed this from the v2.3 milestone Jun 25, 2025

jamesmckinna mentioned this pull request Jun 26, 2025

Proved sorted permutations are equal #2748

Merged

jamesmckinna added 6 commits June 26, 2025 12:08

refactor: code motion

c7961fc

refactor: lift out Core properties, ahead of adding new Decidable…

38245f7

… module

refactor: Core not actually needed!

47ccbf5

refactor: lift out properties of Decidable predicates

ce5efba

refactor: code motion and new module

d7b30f2

refactor: update CHANGELOG

c5aebff

JacquesCarette requested changes Jun 26, 2025

View reviewed changes

src/Data/Fin/Relation/Unary/Decidable.agda Outdated Show resolved Hide resolved

src/Data/Fin/Relation/Unary/Decidable.agda Outdated Show resolved Hide resolved

fix: cosmetic tweaks

2a77e81

jamesmckinna added 3 commits June 27, 2025 06:09

refactor: better module structure?

23d252d

refactor: turn with into let

56f3b78

refactor: clarify types

e8e4772

add: dual version of searchMin

355eb56

jamesmckinna marked this pull request as ready for review June 27, 2025 07:53

JacquesCarette approved these changes Jun 30, 2025

View reviewed changes

JacquesCarette added this to the v2.3 milestone Jun 30, 2025

Merge branch 'master' into refactor-decidable-Fin

1470a95

MatthewDaggitt reviewed Jul 2, 2025

View reviewed changes

MatthewDaggitt modified the milestones: v2.3, v2.4 Jul 3, 2025

jamesmckinna marked this pull request as draft July 3, 2025 07:16

jamesmckinna closed this Jul 23, 2025

jamesmckinna removed this from the v2.4 milestone Jul 25, 2025

jamesmckinna mentioned this pull request Jul 30, 2025

[ refactor ] Data.Fin.Properties.decFinSubset #2793

Merged

jamesmckinna mentioned this pull request Aug 2, 2025

Add Data.Nat.Bounded #2257

Closed

jamesmckinna deleted the refactor-decidable-Fin branch August 2, 2025 10:36

jamesmckinna mentioned this pull request Aug 2, 2025

[ add ] clean version of Data.Fin.Properties.searchMinimalCounterexample #2801

Merged


		{-# OPTIONS --cubical-compatible --safe #-}

		module Data.Fin.Relation.Unary.Base where



		Universal< : Pred (Fin n) p → Pred (Fin n) p
		Universal< P i = (j : Fin′ i) → P (inject j)


		syntax ExistsMinimalCounterexample P = μ⟨¬ P ⟩

		searchMin : Decidable P → (∀ i → P i) ⊎ ∃[ i ] ¬ P i × ∀[ j < i ] P j

[ refactor ] (more) decidable Data.Fin.Properties #2744

[ refactor ] (more) decidable Data.Fin.Properties #2744

Uh oh!

Conversation

jamesmckinna commented Jun 23, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jamesmckinna commented Jun 25, 2025

Uh oh!

JacquesCarette left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

jamesmckinna commented Jun 26, 2025

Uh oh!

JacquesCarette commented Jun 26, 2025

Uh oh!

jamesmckinna commented Jun 27, 2025

Uh oh!

jamesmckinna commented Jun 29, 2025

Uh oh!

JacquesCarette left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

MatthewDaggitt commented Jul 3, 2025

Uh oh!

jamesmckinna commented Jul 3, 2025

Uh oh!

jamesmckinna commented Jul 23, 2025

Uh oh!

JacquesCarette commented Aug 1, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

[ refactor ] (more) decidable `Data.Fin.Properties` #2744

[ refactor ] (more) decidable `Data.Fin.Properties` #2744

jamesmckinna commented Jun 23, 2025 •

edited

Loading