boolean inequality to prop inequality

Stream: lean4

[Bhakti Shah]

there has to be a simple way to do this but i havent found it yet -- how do i go from a != b = true as a goal to a = b -> False? most boolean -> prop coercions ive dealt with have happened automatically so far

[Martin Dvořák]

Please post #mwe. It seems to me there should be parentheses like (a != b) = true probably. Also maybe #xy.

[Marcus Rossel]

@Bhakti Shah I think in general (a != b) = true doesn't imply a = b -> False. You can only go from Prop to Bool but not necessarily the other way around (unless you have LawfulBEq).

[Yuyang Zhao]

We have docs#LawfulBEq.eq_of_beq, docs#ne_of_beq_false, docs#beq_false_of_ne, docs#beq_eq_false_iff_ne. But seems there are almost no lemmas about docs#bne.

[Yuyang Zhao]

You may apply docs#Bool.not_eq_true' on a != b = true first.

[Leonardo de Moura]

Yes, we are currently missing

@[simp] theorem bne_iff_ne [BEq α] [LawfulBEq α] (a b : α) : a != b ↔ a ≠ b := by
  simp [bne]; rw [← beq_iff_eq a b]; simp [-beq_iff_eq]

@Bhakti Shah The [simp] rule above (or similar) should be added to the library. In the meantime, you can add it to your project.

[Bhakti Shah]

Martin Dvořák said:

Please post #mwe. It seems to me there should be parentheses like (a != b) = true probably. Also maybe #xy.

sorry about that i didn't actually expect someone to try to prove it since i thought it would be in a library somewhere :)

[Bhakti Shah]

Leonardo de Moura said:

Yes, we are currently missing

@[simp] theorem bne_iff_ne [BEq α] [LawfulBEq α] (a b : α) : a != b ↔ a ≠ b := by
  simp [bne]; rw [← beq_iff_eq a b]; simp [-beq_iff_eq]

Bhakti Shah The [simp] rule above (or similar) should be added to the library. In the meantime, you can add it to your project.

thanks! I looked on that page and couldn't find it, so i wasn't sure if i was missing something. i did manage to prove it with some similar chaining of lemmas

[Bhakti Shah]

@[simp] theorem bne_iff_ne [BEq α] [LawfulBEq α] (a b : α) : a != b ↔ a ≠ b := by this seems to resolve for me by just simp [bne].

[Leonardo de Moura]

@Bhakti Shah Nice. You should have other [simp] theorems already installed in your environment. The definition above only depends on the core library.