contradiction on bools

Stream: lean4

[James Gallicchio]

I expected contradiction to be able to close this goal -- is this something it should handle?

example (b : Bool) (h₁ : b = true) (h₂ : b = false) : False
  := by contradiction

Or more generally, any time when there are two hypotheses that have the same expression equal to different constructors

[Kyle Miller]

I'm not sure what contradiction should or shouldn't do, but you can add in subst_vars to help contradiction out:

example (b : Bool) (h₁ : b = true) (h₂ : b = false) : False
  := by subst_vars; contradiction

[James Gallicchio]

ooooooh, never seen that tactic before, thanks!

[James Gallicchio]

I now realize this doesn't quite work for my use case, which is more like

example (f : α → Bool) (a : α) (h₁ : f a = true) (h₂ : f a = false) : False
  := by sorry

but I think it's probably easiest to just wait for cc to be implemented

[Kevin Buzzard]

You can just rewrite and then use cases

[Marcus Rossel]

James Gallicchio said:

I now realize this doesn't quite work for my use case, which is more like

example (f : α → Bool) (a : α) (h₁ : f a = true) (h₂ : f a = false) : False
  := by sorry

but I think it's probably easiest to just wait for cc to be implemented

example (f : α → Bool) (a : α) (h₁ : f a = true) (h₂ : f a = false) : False := by
  have := h₁.symm.trans h₂ -- establishes `true = false`
  contradiction

[Mario Carneiro]

or cases h₁ ▸ h₂

[James Gallicchio]

For a single case doing it manually is perfectly fine, but I have a proof where there are a handful of cases that would almost all be solved by cc. So right now I manually go through the cases and name the hypotheses and construct the proof terms, but doing <;> (fst | cc | simp; assumption) instead would be really nice

[James Gallicchio]

Actually, is somebody working on reimplementing cc yet? I've been looking for metaprogramming projects to try out

[Leonardo de Moura]

James Gallicchio said:

Actually, is somebody working on reimplementing cc yet? I've been looking for metaprogramming projects to try out

Nobody is currently working on cc, and would be great to have someone helping with it.

[James Gallicchio]

Ok, I'll give it a shot! :smile: Should it live in core or mathlib?

[Leonardo de Moura]

It should be in the lean4 repo.