De Morgan's laws for Pred #2832
Conversation
|
So... I think that all of these things are already covered by |
|
I think you are correct @jamesmckinna . But there must also be something very slightly different about them? Perhaps some subtlety about irrelevance? |
|
The differences, AFAICT, are that the lemmas in 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 = ∀¬⟶¬∃ λ _ → ∀∁PSo... I think this is worth badging as |
|
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 ;-) |
|
I think you're right about all of this being redundant. I think the main remaining point is around findability and naming:
|
|
I broadly agree:
But it's a testament to Stockholm Syndrome that I have come to internalise the |
|
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 |
There was a problem hiding this comment.
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
added
addition
discoverability
| 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) |
There was a problem hiding this comment.
| 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.
| ¬∃⟨P⟩⇒Π[∁P] ¬sat = curry ¬sat | ||
|
|
||
| ¬∃⟨P⟩⇒∀[∁P] : ∀ {P : Pred A ℓ} → ¬ ∃⟨ P ⟩ → ∀[ ∁ P ] | ||
| ¬∃⟨P⟩⇒∀[∁P] ¬sat = curry ¬sat _ |
There was a problem hiding this comment.
Maybe coupling is considered harmful, but given the amount of duplication/repetition/redundancy here, I would prefer to emphasise it by delegation:
| ¬∃⟨P⟩⇒∀[∁P] ¬sat = curry ¬sat _ | |
| ¬∃⟨P⟩⇒∀[∁P] ¬sat = ¬∃⟨P⟩⇒Π[∁P] ¬sat _ |
| ¬∃⟨P⟩⇒∀[∁P] ¬sat = curry ¬sat _ | ||
|
|
||
| ∃⟨∁P⟩⇒¬Π[P] : ∀ {P : Pred A ℓ} → ∃⟨ ∁ P ⟩ → ¬ Π[ P ] | ||
| ∃⟨∁P⟩⇒¬Π[P] (x , ¬Px) ΠP = ¬Px (ΠP x) |
There was a problem hiding this comment.
| ∃⟨∁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
| ∃⟨∁P⟩⇒¬∀[P] (_ , ¬Px) ∀P = ¬Px ∀P | ||
|
|
||
| Π[∁P]⇒¬∃[P] : ∀ {P : Pred A ℓ} → Π[ ∁ P ] → ¬ ∃⟨ P ⟩ | ||
| Π[∁P]⇒¬∃[P] Π∁P (x , Px) = Π∁P x Px |
There was a problem hiding this comment.
| Π[∁P]⇒¬∃[P] Π∁P (x , Px) = Π∁P x Px | |
| Π[∁P]⇒¬∃[P] = uncurry |
suffices!
| Π[∁P]⇒¬∃[P] Π∁P (x , Px) = Π∁P x Px | ||
|
|
||
| ∀[∁P]⇒¬∃[P] : ∀ {P : Pred A ℓ} → ∀[ ∁ P ] → ¬ ∃⟨ P ⟩ | ||
| ∀[∁P]⇒¬∃[P] ∀∁P (_ , Px) = ∀∁P Px |
There was a problem hiding this comment.
| ∀[∁P]⇒¬∃[P] ∀∁P (_ , Px) = ∀∁P Px | |
| ∀[∁P]⇒¬∃[P] = Π[∁P]⇒¬∃[P] (λ _ → ∀∁P) |
again, emphasise the delegation to the explicit version.
|
There are (lots of!?) potential
so perhaps worth lifting out as a new issue? |
Closes #2831