De Morgan's laws for Pred

[Taneb]

Closes #2831

[jamesmckinna]

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]

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

[jamesmckinna]

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]

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]

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

1. Neither @Taneb nor Sergei were able to find these
2. 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]

I broadly agree:

• for v2.4, I think we should get the names/namingconvention right see #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]

@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]

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]

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]

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]

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