[ refactor ] make contradiction and friends entirely definitionally proof-irrelevant
#2802
Conversation
| @@ -409,17 +409,17 @@ module Antisymmetry | |||
| length (y ∷ ys₁) ≤⟨ length-mono-≤ ss ⟩ | |||
| length zs ≤⟨ ℕ.n≤1+n (length zs) ⟩ | |||
| length (z ∷ zs) ≤⟨ length-mono-≤ rs ⟩ | |||
| length ys₁ ∎) $ ℕ.<-irrefl ≡.refl | |||
| length ys₁ ∎) (ℕ.<-irrefl ≡.refl) | |||
There was a problem hiding this comment.
perhaps don't roll in such pure, non-breaking style changes in to something breaking and make a separate (if tiny) PR?
There was a problem hiding this comment.
Not a style change; it's yet another 'feature' of irrelevant function spaces: _$_ is no longer well-typed!
| @@ -26,38 +26,48 @@ infix 3 ¬_ | |||
| ¬_ : Set a → Set a | |||
| ¬ A = A → ⊥ | |||
|
|
|||
| -- Note the following use of flip: | |||
| private | |||
| note : (A → ¬ B) → B → ¬ A | |||
There was a problem hiding this comment.
If you're going to bother to move this to the top of the file, maybe also document where the 'note' is useful in reading below?
There was a problem hiding this comment.
Well... for starters, breaking, so code motion ought to be permissible?
Secondly, more importantly, some of the properties in this module (eg _¬-⊎_ and ¬¬-η) are consequences of the minimal logic interpretation of ¬_, and they are conceptually prior to the ones which make genuine use of ex falso ⊥-elim(-irr)... so it made sense to me that they occur first in the module. Cf. #2803
As to the best way to document this separation of concerns, suggestions welcome!
There was a problem hiding this comment.
Maybe one way to resolve this is to interpolate a v2.4 non-breaking PR which reorganises Negation.Core to distinguish
- definition
- consequences/properties per minimal logic:
note,¬¬-η,contra-diagonal... - consequences/properties per use of ex falso
rather than try to do this as part of this PR?
There was a problem hiding this comment.
And/or add some text to #2798 to emphasise the distinction?
|
Thanks @JacquesCarette for the speedy feedback (on a For most of your queries, eta-expansion is needed because there's no (contravariant) subtyping between As for the ones which seemingly contradict #2653 , see #2803 : don't use |
The inevitable
breakingconsequence of #2785 , designed as a 'cleaning of the stables'.Cf. #2346 whose intention it follows.
Currently duplicates functionality from #2803 ; will tidy up once that is merged.
Downstream consequence:
contradictioninternally need eta-expansion (and this may be regarded as a UX failure...?)stdlibthat I can find)TODO:
contradiction-irrintroduced as consequences of [ refactor ] weaken type ofRelation.Nullary.Negation.Core.contradiction-irr#2785Consider also:
Relation.Nullary.Reflectsto make its various arguments definitionally proof-irrelevantRelation.Nullary.Negation.Core._¬-⊎_in favour ofcontradiction₂, or else change its type as well; its one use instdlibis inReflects, so could be refactored in any case via¬-recomputeand inlining...