List/BEq diamond

Stream: Is there code for X?

[Heather Macbeth]

Couldn't find something like this in the library ... did I miss it?

theorem beq_list_diamond [DecidableEq α] (l1 l2 : List α) :
    decide (l1 = l2) = List.beq l1 l2 := by
  sorry

[Yury G. Kudryashov]

AFAIR, there were plans to redefine docs#Decidable to prevent diamonds like this (going from a boolean to Decidable and back again is not defeq). I don't know what happened to these plans.

[Eric Wieser]

I think the plans were Gabriel's, and MSR losing interest in Lean seems to have caused them to go on hold

[Eric Wieser]

lean4#2038 has a trial implementation

[Yury G. Kudryashov]

That's a huge diff

[Yury G. Kudryashov]

@Gabriel Ebner Do you plan working on lean4#2038? If not, then I'll see if I can pick it up next week.

[Kyle Miller]

@Yury G. Kudryashov Something I noticed and mentioned in this PR comment is that there seems to be a lower-impact change to Decidable (and one that seems to have nicer definitional equalities). I got as far as seeing it'll take also looking through assumptions about Decidable that are hard-coded into the compiler.

Here's the possible re-definition reproduced here:

class Decidable (p : Prop) where
  /-- The truth value of the proposition `p` as a `Bool`.
  If `true` then `p` is true, and if `false` then `p` is false. -/
  decide : Bool
  /-- `decide p` evaluates to the Boolean `true` if and only if `p` is a true proposition.  -/
  cond_decide : cond decide p (Not p)

/-- Prove that `p` is decidable by supplying a proof of `p` -/
@[match_pattern] def Decidable.isTrue {p : Prop} (h : p) : Decidable p where
  decide := true
  cond_decide := h

/-- Prove that `p` is decidable by supplying a proof of `¬p` -/
@[match_pattern] def Decidable.isFalse {p : Prop} (h : Not p) : Decidable p where
  decide := false
  cond_decide := h

[Kyle Miller]

I'm not sure where adjusting Decidable is on the Lean roadmap. It would be good figuring that out before you spend a lot of time on this -- though if it can be carried out in a low-impact way without a huge diff, that would be great to know.

[Henrik Böving]

Kyle Miller said:

Yury G. Kudryashov Something I noticed and mentioned in this PR comment is that there seems to be a lower-impact change to Decidable (and one that seems to have nicer definitional equalities). I got as far as seeing it'll take also looking through assumptions about Decidable that are hard-coded into the compiler.

Here's the possible re-definition reproduced here:

class Decidable (p : Prop) where
  /-- The truth value of the proposition `p` as a `Bool`.
  If `true` then `p` is true, and if `false` then `p` is false. -/
  decide : Bool
  /-- `decide p` evaluates to the Boolean `true` if and only if `p` is a true proposition.  -/
  cond_decide : cond decide p (Not p)

/-- Prove that `p` is decidable by supplying a proof of `p` -/
@[match_pattern] def Decidable.isTrue {p : Prop} (h : p) : Decidable p where
  decide := true
  cond_decide := h

/-- Prove that `p` is decidable by supplying a proof of `¬p` -/
@[match_pattern] def Decidable.isFalse {p : Prop} (h : Not p) : Decidable p where
  decide := false
  cond_decide := h

With this definition a Decidable instance would end up being an unboxed bool by our natural FFI definitions I think. That should make it rather easy to handle in the compiler, maybe even without special casing?

[Kyle Miller]

@Henrik Böving There are some assumptions about Decidable here and there. I got some assertion violations in erase_irrelevant.cpp in particular.

[Henrik Böving]

Right but the code in erase_irrelevant.cpp that deals with decidables is concerned with turning decidable things into Bool things. But since that would just naturally happen with the FFI rules I would hope we might just be able to get rid of it without performance penalty?

[Henrik Böving]

But that's just a hope, I don't know for sure of course

[Kyle Miller]

Oh, ok, I thought you were saying something else. It'd be neat if all we'd need to do to make this work is rip out the special casing.

[Henrik Böving]

If you do rip it out you might also want to either do that or add a note in the new compiler directory which deals with this as well but is disabled right now.

[Yaël Dillies]

Yury G. Kudryashov said:

That's a huge diff

It's not that huge once you ignore everything under stage0.

[Gabriel Ebner]

@Yury G. Kudryashov Unfortunately I don't have time to resume work on that PR. IIRC the Lean PR was technically finished, but it wasn't merged because it would cause work for the mathlib port.

[Gabriel Ebner]

I like Kyle's proposal. It should be enough to just make that change on top of my PR. I'd already ripped out all the special casing in the compiler.

[Yury G. Kudryashov]

I will read instructions on bootstrapping Lean 4 tomorrow.