Simple Bool-contradiction lemma?

[andreasabel]

Would there be a place for this simple lemma in the standard library?

Bool-contradiction : ∀ {ℓ} {A : Set ℓ} {b : Bool} → b ≡ true → b ≡ false → A
Bool-contradiction refl ()

I found it convenient when refuting impossible cases concerning functions into Bool.

[jamesmckinna]

In the interests of non-duplication/avoiding redundancy, you could instead write

open import Data.Bool.Properties using (not-¬)

Bool-contradiction : ∀ {ℓ} {A : Set ℓ} {b : Bool} → b ≡ true → b ≡ false → A
Bool-contradiction ≡tt ≡ff with () ← not-¬ ≡tt ≡ff

(or inline with () ← not-¬ ≡tt ≡ff where appropriate in your code?)

But not sure whether that's really the answer to your question?

[andreasabel]

My question is whether it is within the policy to add a new lemma

Bool-contradiction : ∀ {ℓ} {A : Set ℓ} {b : Bool} → b ≡ true → b ≡ false → A

to Data.Bool.Properties. Of course, this lemma can be proven in many ways, and everything than can be proven with the lemma can be proven without it in some other way, but it strikes me as a natural lemma to look for when working with boolean functions.

E.g. here is a proof that the unit type is not isomorphic to the booleans (not using the Iso definition from the standard library):

record _≅_ (A B : Set) : Set where
  constructor iso
  field
    raw : A ⇔ B
  open _⇔_ raw public
  field
    from∘to : ∀{a} → from (to a) ≡ a
    to∘from : ∀{b} → to (from b) ≡ b

¬Unit≅Bool : ¬(⊤ ≅ Bool)
¬Unit≅Bool (iso _ _ _ to∘from) =
  Bool-contradiction (to∘from {b = true}) (to∘from {b = false})

Here, we basically want to combine the two equations f record{} ≡ true and f record{} ≡ false.

Here is another example proving that minimization is deterministic:

  Mu : (f : ℕ → Bool) → ℕ → Set
  Mu f zero    = f zero ≡ true
  Mu f (suc n) = f zero ≡ false × Mu (f ∘ suc) n

  Mu-functional :  ∀ n m → Mu f n → Mu f m → n ≡ m
  Mu-functional zero    zero    _                 _              = refl
  Mu-functional zero    (suc m) f0-true           (f0-false , _) = Bool-contradiction f0-true f0-false
  Mu-functional (suc n) zero    (f0-false , _)    f0-true        = Bool-contradiction f0-true f0-false
  Mu-functional (suc n) (suc m) (f0-false , mu-n) (_ , mu-m)     = cong suc (Mu-functional n m mu-n mu-m)

[jamesmckinna]

So, I'm not surprised by your response, but I'm maybe not the authority to comment on the OP, except to say:

• my understanding of the library design is that we don't typically want/accept redundant repetition/recoding, unless there's a strong argument on its behalf... (I'm not clear how compelling your examples are, and I personally would avoid adding your lemma)
• ... negotiating between having a lemma applicable on the RHS of definitions, rather than a refutation on the left via with () ← ... remains an active discussion topic (eg #2123 ) so maybe my counter-proposal isn't welcome, either...
• discoverability/naming/deprecation: is your definition preferable to existing properties under Data.Bool? eg should we rewrite not-¬ in your terms, given that the latter lemma is 'hard to find' (it has morally the same proof as you give; that's why I used it to remove the need for Bool-contradiction... but I did have to search to find it)
• #2653 argues for Relation.Nullary.Negation.Core.contradiction as the 'universal' appeal to ⊥-elim (we're trying to standardise); so would it be better to rephrase the proof of your lemma in simpler terms via contradiction p ¬p where p would be the proof of true ≡ false available in the scope of your hypotheses, and the obvious proof ¬p : ¬(true ≡ false) given by ¬p ()... ie morally again what you have, but wrapped in the 'blessed' abstract wrapper contradiction...

Etc.

Others should offer their opinions!

[JacquesCarette]

I'm personally on the side of preferring findability over minimalism, as long as it does not incur a (predictable) non-trivial maintenance burden.

In more detail: the 'core' of the library aimed at library maintainers should have different design criteria than user-facing aspects. Core embeds fundamental knowledge that might need a high level of sophistication to understand; user-facing should be optimized to let users get their own work done.

More pithily: fancy innards, shiny UI. This is true for large libraries too.

[jamesmckinna]

@JacquesCarette writes:

More pithily: fancy innards, shiny UI. This is true for large libraries too.

Less pithily: are you arguing that eg Data.Bool, as the 'user-facing' module, should declare @andreasabel 's lemma, and that we should implement it using the/a 'core' lemma in Data.Bool.Properties? or some other refactoring based on an as-yet-only-implicitly-defined separation of stdlib modules into 'user-facing' and 'core'?

This seems to be yet-another variation on the 'wide' vs. 'narrow API discussions which recur from time to time... and for which I don't think we (yet) have 'policy' as such, beyond a general bias from the core admin team towards 'narrow'?

[jamesmckinna]

Re: the OP One reason I don't like the lemma is that it reintroduces/reiterates the pattern of <contradictory hypotheses> -> Whatever which is (characterised by) the ex falso quodlibet property ⊥-elim, which, in turn, given the intricacies of the current versions of Data.Empty{.*} (something I never wish to expose as 'user-facing'...), are further encapsulated in contradiction.

So for me it goes too far towards ad hoc maximalism/ a 'wide' API, for the sake of a result which, with a ('narrow'-minded) developer's hat on, I can 'easily' see to be expressible in terms of existing functionality... so the broader issue is perhaps one of: 'ergonomics of ex falso'...?

[JacquesCarette]

are you arguing that eg Data.Bool, as the 'user-facing' module [...]

Indeed, I would accept @andreasabel 's lemma in Data.Bool. It could have a direct or indirect proof - I don't care as much about that, given how simple it is.

ergonomics of ex falso

I agree that if contradiction were easy to deploy for this case, the lemma would not be worth it. But I don't think that's the case.

[jamesmckinna]

Experimenting by implementing #2853 makes me wonder where we stop? Do we 'need' corresponding Discriminate-like inversion lemmas generated for all data definitions? (Is this a UX failure for pattern-matching? One that perhaps requires a generic, Reflection-based, solution instead?)

[jamesmckinna]

@andreasabel What's your take on #2853 ?

[JacquesCarette]

One big benefit of inductive types is "no junk no confusion" to re-use Goguen's nice phrasing. So if "no confusion" is not cheap, there is definitely a problem to be addressed. Absolutely "no confusion" is provable for each such type - but why does it need a proof?

[jamesmckinna]

One big benefit of inductive types is "no junk no confusion" to re-use Goguen's nice phrasing. So if "no confusion" is not cheap, there is definitely a problem to be addressed. Absolutely "no confusion" is provable for each such type - but why does it need a proof?

Well, it seems as though the 'vanilla' "no confusion" is cheap (pattern-matching makes the proof of contradiction easy), but packaging it as an ex false principle, and even the need for such a thing explicitly, is what seems (more) costly...

[Taneb]

I'm not at all convinced that something like this should be added. I think @andreasabel's example in particular is better expressed as the following:

Mu-functional :  ∀ n m → Mu f n → Mu f m → n ≡ m
Mu-functional zero    zero    _                 _              = refl
Mu-functional zero    (suc m) f0-true           (f0-false , _) with () ← trans (sym f0-true) f0-false
Mu-functional (suc n) zero    (f0-false , _)    f0-true        with () ← trans (sym f0-true) f0-false
Mu-functional (suc n) (suc m) (f0-false , mu-n) (_ , mu-m)     = cong suc (Mu-functional n m mu-n mu-m)

Or

Mu-functional :  ∀ n m → Mu f n → Mu f m → n ≡ m
Mu-functional zero    zero    _                 _              = refl
Mu-functional zero    (suc m) f0-true           (f0-false , _) rewrite f0-true with () ← f0-false
Mu-functional (suc n) zero    (f0-false , _)    f0-true        rewrite f0-false with () ← f0-true
Mu-functional (suc n) (suc m) (f0-false , mu-n) (_ , mu-m)     = cong suc (Mu-functional n m mu-n mu-m)

I don't think we should be adding more "explosion" principles at all.

[jamesmckinna]

Thanks @Taneb ! I started from the same place as you (cashed out slightly differently), and so one reason I wrote #2853 was to challenge my own preconceptions on this issue (and why the lemma ends up in Data.Bool as a 'user-facing' lemma).

I think this is very tricky to adjudicate! On reason for seeking input from everyone, esp. from the author of the OP... ;-)