De Morgan's laws for Pred by Taneb · Pull Request #2832 · agda/agda-stdlib

Taneb · 2025-09-26T05:51:50Z

JacquesCarette

Two comments, two requests for change.

Massively surprised this wasn't here already!

jamesmckinna · 2025-09-28T13:54:47Z

So... I think that all of these things are already covered by Relation.Nullary.Negation (including even @JacquesCarette 's observations about curry etc.)? Or not!?

JacquesCarette · 2025-09-28T15:40:53Z

I think you are correct @jamesmckinna . But there must also be something very slightly different about them? Perhaps some subtlety about irrelevance?

jamesmckinna · 2025-09-29T03:16:32Z

The differences, AFAICT, are that the lemmas in Relation.Nullary.Negation only concern the Universal (explicitly quantified) cases, whereas this PR also covers the IUniversal (implicitly quantified) ones as well. But, FTR, using the suggested import:

open import Relation.Nullary.Negation using (¬_; ∃⟶¬∀¬; ∀⟶¬∃¬; ¬∃⟶∀¬; ∀¬⟶¬∃; ∃¬⟶¬∀)
module _ {P : Pred A ℓ} where

  ¬∃⟨P⟩⇒Π[∁P] : ¬ ∃⟨ P ⟩ → Π[ ∁ P ]
  ¬∃⟨P⟩⇒Π[∁P] = ¬∃⟶∀¬

  ¬∃⟨P⟩⇒∀[∁P] : ¬ ∃⟨ P ⟩ → ∀[ ∁ P ]
  ¬∃⟨P⟩⇒∀[∁P] ¬sat = ¬∃⟶∀¬ ¬sat _

  ∃⟨∁P⟩⇒¬Π[P] : ∃⟨ ∁ P ⟩ → ¬ Π[ P ]
  ∃⟨∁P⟩⇒¬Π[P] = ∃¬⟶¬∀

  ∃⟨∁P⟩⇒¬∀[P] : ∃⟨ ∁ P ⟩ → ¬ ∀[ P ]
  ∃⟨∁P⟩⇒¬∀[P] ∃CP ∀P = ∃¬⟶¬∀ ∃CP λ _ → ∀P

  Π[∁P]⇒¬∃[P] : Π[ ∁ P ] → ¬ ∃⟨ P ⟩
  Π[∁P]⇒¬∃[P] = ∀¬⟶¬∃

  ∀[∁P]⇒¬∃[P] : ∀[ ∁ P ] → ¬ ∃⟨ P ⟩
  ∀[∁P]⇒¬∃[P] ∀∁P = ∀¬⟶¬∃ λ _ → ∀∁P

So... I think this is worth badging as status:duplicate or even status:invalid?

jamesmckinna · 2025-10-01T03:22:32Z

Do we want to merge this, or close, and follow up with a rename+deprecate as discussed in #2831 ?

I'm (largely) agnostic/uncommitted on this issue (apart from the redundancy involved), but proofs which differ at all from those versions offered above would be... redundancy too far, IMNSVHO ;-)

JacquesCarette · 2025-10-10T18:52:18Z

I think you're right about all of this being redundant. I think the main remaining point is around findability and naming:

Neither @Taneb nor Sergei were able to find these
Relation.Nullary is a hideous prefix. Are there such things as non-trivial nullary relations? This feels like a horrible hack from ages ago that 3.0 should get rid of.

jamesmckinna · 2025-10-11T07:27:39Z

I broadly agree:

for v2.4, I think we should get the names/namingconvention right see [ deprecate ] names for deMorgan lemmas in Relation.Nullary.Negation #2838
for v3.0, we can indeed revisit these larger-scale modular hierarchies

But it's a testament to Stockholm Syndrome that I have come to internalise the Nullary/Unary/Binary taxonomy ;-)

jamesmckinna · 2025-10-14T08:47:31Z

@Taneb suggest merging your commits here, or my suggestions above, to #2838 so that we can knock this off, at least for v2.4?

Taneb · 2025-10-14T10:04:45Z

Why don't we merge both PRs separately? fwiw I'm (very slightly) against your suggestions: they add a new import to the dependency graph to turn a bunch of one line definitions to a bunch of slightly more abbreviated one line definitions

jamesmckinna · 2025-10-14T11:47:04Z

Why don't we merge both PRs separately? fwiw I'm (very slightly) against your suggestions: they add a new import to the dependency graph to turn a bunch of one line definitions to a bunch of slightly more abbreviated one line definitions

Fair enough, but, pace the discoverability problem (not trying to discount it), I'm not sure the duplication in Unary makes (better?) sense... but for the sake of v2.4 (and the opportunity for a breaking redesign in v3.0), happy to merge this too.

jamesmckinna

Happy to merge this, but I'd push a bit harder on @JacquesCarette 's suggestion to use curry/uncurry where possible... (eg by inlining the definitions given above?)

jamesmckinna

I won't stand in the way of what's here already, but I do think the suggestions I make improve things, but without adding the extra node to the dependency graph, while emphasising the generic/delegation aspects of all these proofs.

jamesmckinna · 2025-10-28T06:27:44Z

 module Relation.Unary.Properties where

-open import Data.Product.Base as Product using (_×_; _,_; swap; proj₁; zip′)
+open import Data.Product.Base as Product using (_×_; _,_; -,_; swap; proj₁; zip′; curry)


Suggested change

open import Data.Product.Base as Product using (_×_; _,_; -,_; swap; proj₁; zip′; curry)

open import Data.Product.Base as Product using (_×_; _,_; -,_; swap; proj₁; zip′; curry; uncurry)

As before, I'd rather use the generic operations where possible.

jamesmckinna · 2025-10-28T06:29:20Z

+¬∃⟨P⟩⇒Π[∁P] ¬sat = curry ¬sat
+
+¬∃⟨P⟩⇒∀[∁P] : ∀ {P : Pred A ℓ} → ¬ ∃⟨ P ⟩ → ∀[ ∁ P ]
+¬∃⟨P⟩⇒∀[∁P] ¬sat = curry ¬sat _


Maybe coupling is considered harmful, but given the amount of duplication/repetition/redundancy here, I would prefer to emphasise it by delegation:

Suggested change

¬∃⟨P⟩⇒∀[∁P] ¬sat = curry ¬sat _

¬∃⟨P⟩⇒∀[∁P] ¬sat = ¬∃⟨P⟩⇒Π[∁P] ¬sat _

jamesmckinna · 2025-10-28T06:30:49Z

+¬∃⟨P⟩⇒∀[∁P] ¬sat = curry ¬sat _
+
+∃⟨∁P⟩⇒¬Π[P] : ∀ {P : Pred A ℓ} → ∃⟨ ∁ P ⟩ → ¬ Π[ P ]
+∃⟨∁P⟩⇒¬Π[P] (x , ¬Px) ΠP = ¬Px (ΠP x)


Suggested change

∃⟨∁P⟩⇒¬Π[P] (x , ¬Px) ΠP = ¬Px (ΠP x)

∃⟨∁P⟩⇒¬Π[P] (_ , ¬Px) ΠP = ¬Px (ΠP _)

using the underscores here:

is more robust (debatable?)

formally mirrors the subsequent lemma

jamesmckinna · 2025-10-28T06:34:54Z

+∃⟨∁P⟩⇒¬∀[P] (_ , ¬Px) ∀P = ¬Px ∀P
+
+Π[∁P]⇒¬∃[P] : ∀ {P : Pred A ℓ} → Π[ ∁ P ] → ¬ ∃⟨ P ⟩
+Π[∁P]⇒¬∃[P] Π∁P (x , Px) = Π∁P x Px


Suggested change

Π[∁P]⇒¬∃[P] Π∁P (x , Px) = Π∁P x Px

Π[∁P]⇒¬∃[P] = uncurry

suffices!

jamesmckinna · 2025-10-28T06:35:08Z

+Π[∁P]⇒¬∃[P] Π∁P (x , Px) = Π∁P x Px
+
+∀[∁P]⇒¬∃[P] : ∀ {P : Pred A ℓ} → ∀[ ∁ P ] → ¬ ∃⟨ P ⟩
+∀[∁P]⇒¬∃[P] ∀∁P (_ , Px) = ∀∁P Px


Suggested change

∀[∁P]⇒¬∃[P] ∀∁P (_ , Px) = ∀∁P Px

∀[∁P]⇒¬∃[P] = Π[∁P]⇒¬∃[P] (λ _ → ∀∁P)

again, emphasise the delegation to the explicit version.

jamesmckinna · 2025-10-28T06:42:47Z

There are (lots of!?) potential library-design issues raised by this PR:

navigability/discoverability, as already noted
redundant recoding as a side effect of the above
finessing implicit vs. explicit function spaces (I find Function.Base.{_$-|λ-} too fiddly in practice to use, but maybe they could be deployed here?)
the Relation.*ary hierarchy, and 'opportunities' to refactor it
...

so perhaps worth lifting out as a new issue?

jamesmckinna · 2025-11-08T11:01:56Z

Do you want the refactoring suggestions, or shall we simply merge as is @Taneb ?

jamesmckinna · 2026-01-22T12:01:27Z

Happy to (re-)consider my suggestions re: delegation/refactoring downstream, so merging now.

* Add De Morgan's law for Pred * Add more of De Morgan's laws * Don't name unused variables * Use curry

Taneb added 2 commits September 26, 2025 07:44

Add De Morgan's law for Pred

d24ce8c

Add more of De Morgan's laws

0a974c5

JacquesCarette requested changes Sep 26, 2025

View reviewed changes

Comment thread src/Relation/Unary/Properties.agda Outdated

Comment thread src/Relation/Unary/Properties.agda Outdated

Comment thread src/Relation/Unary/Properties.agda

Comment thread src/Relation/Unary/Properties.agda Outdated

Don't name unused variables

b406933

Taneb requested a review from JacquesCarette September 27, 2025 20:37

JacquesCarette approved these changes Sep 27, 2025

View reviewed changes

jamesmckinna mentioned this pull request Oct 11, 2025

[ deprecate ] names for deMorgan lemmas in Relation.Nullary.Negation #2838

Merged

jamesmckinna requested changes Oct 14, 2025

View reviewed changes

Use curry

522a0c3

Taneb requested a review from jamesmckinna October 27, 2025 12:38

JacquesCarette approved these changes Oct 27, 2025

View reviewed changes

jamesmckinna added addition discoverability How easy/hard will it be for users to find, within the context of their application? labels Oct 27, 2025

jamesmckinna approved these changes Oct 28, 2025

View reviewed changes

jamesmckinna added this to the v2.4 milestone Oct 28, 2025

jamesmckinna added this pull request to the merge queue Jan 22, 2026

Merged via the queue into master with commit 99167f7 Jan 22, 2026
12 checks passed

plt-amy pushed a commit that referenced this pull request Feb 9, 2026

De Morgan's laws for Pred (#2832)

09e266e

* Add De Morgan's law for Pred * Add more of De Morgan's laws * Don't name unused variables * Use curry

andreasabel mentioned this pull request Apr 18, 2026

Update experimental branch; allow GHC 9.14 #2985

Merged

	open import Data.Product.Base as Product using (_×_; _,_; -,_; swap; proj₁; zip′; curry)
	open import Data.Product.Base as Product using (_×_; _,_; -,_; swap; proj₁; zip′; curry; uncurry)

	¬∃⟨P⟩⇒∀[∁P] ¬sat = curry ¬sat _
	¬∃⟨P⟩⇒∀[∁P] ¬sat = ¬∃⟨P⟩⇒Π[∁P] ¬sat _

	∃⟨∁P⟩⇒¬Π[P] (x , ¬Px) ΠP = ¬Px (ΠP x)
	∃⟨∁P⟩⇒¬Π[P] (_ , ¬Px) ΠP = ¬Px (ΠP _)

	Π[∁P]⇒¬∃[P] Π∁P (x , Px) = Π∁P x Px
	Π[∁P]⇒¬∃[P] = uncurry

	∀[∁P]⇒¬∃[P] ∀∁P (_ , Px) = ∀∁P Px
	∀[∁P]⇒¬∃[P] = Π[∁P]⇒¬∃[P] (λ _ → ∀∁P)

Conversation

Taneb commented Sep 26, 2025

Uh oh!

JacquesCarette left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jamesmckinna commented Sep 28, 2025

Uh oh!

JacquesCarette commented Sep 28, 2025

Uh oh!

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

Uh oh!

Uh oh!

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

Uh oh!

Uh oh!

JacquesCarette commented Oct 10, 2025

Uh oh!

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

Uh oh!

Uh oh!

jamesmckinna commented Oct 14, 2025

Uh oh!

Taneb commented Oct 14, 2025

Uh oh!

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

Uh oh!

Uh oh!

jamesmckinna left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jamesmckinna left a comment

Choose a reason for hiding this comment

Uh oh!

jamesmckinna Oct 28, 2025

Choose a reason for hiding this comment

Uh oh!

jamesmckinna Oct 28, 2025

Choose a reason for hiding this comment

Uh oh!

jamesmckinna Oct 28, 2025

Choose a reason for hiding this comment

Uh oh!

jamesmckinna Oct 28, 2025

Choose a reason for hiding this comment

Uh oh!

jamesmckinna Oct 28, 2025

Choose a reason for hiding this comment

Uh oh!

jamesmckinna commented Oct 28, 2025

Uh oh!

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

Uh oh!

Uh oh!

jamesmckinna commented Jan 22, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

jamesmckinna commented Sep 29, 2025 •

edited

Loading

jamesmckinna commented Oct 1, 2025 •

edited

Loading

jamesmckinna commented Oct 11, 2025 •

edited

Loading

jamesmckinna commented Oct 14, 2025 •

edited

Loading

jamesmckinna left a comment •

edited

Loading

jamesmckinna commented Nov 8, 2025 •

edited

Loading