Converting Bool to Prop

Stream: lean4

[Shreyas Srinivas]

I have the following example, which I'd like to run:

import Std.Data.List.Basic

structure Stack (α : Type) where
  stuff : List α

def pop [BEq α] (s : Stack α) : Option α × Stack α :=
  if h : s.stuff == [] then
    ⟨none, s⟩
  else
    (some (s.stuff.head h), s.stuff.tail)

List.head requires proof that the list is non empty (s.stuff ≠ [] : Prop) . The type of h is however ¬(s.stuff == []) = true : Prop. What is the quickest way to get there? Is an equation lemma the only way to go?

[Kevin Buzzard]

Can you put h : s.stuff = [] instead? if is expecting a Prop, not a bool.

[Shreyas Srinivas]

Making it a prop means I need to add a decidable instance. I can see why this is true. On the other hand, I don't see why a computable bool can't be converted to a proof of the corresponding prop.

[Shreyas Srinivas]

Specifically , changing to a Prop gives the following error

failed to synthesize instance
  Decidable (s.stuff = [])

[Henrik Böving]

A coomputable bool can be converted to a Prop. It is just that == Does not necessarily have to mean =. The implementation can be completely distinct. The reason the Decidable thing does not work here is that the general decidability function on lists requires decidability to be shown, what you want to do here is add a deriving DecidableEq to your structure (or just making it an abbrev all together) and a [DecidableEq α] argument to your function so it can synthesize.

Alternatively, since there is no need to know that alpha is decidableeq since yoou only want to check for equality to the empty list you might as well simply pattern match:

match h: s.stuff with
| [] => ...
| x :: xs =>

which in general just simplifies your program largely because there is no need for the head and tail stuff anymore in the first place

[Shreyas Srinivas]

Henrik Böving said:

A coomputable bool can be converted to a Prop. It is just that == Does not necessarily have to mean =. The implementation can be completely distinct. The reason the Decidable thing does not work here is that the general decidability function on lists requires decidability to be shown, what you want to do here is add a deriving DecidableEq to your structure (or just making it an abbrev all together) and a [DecidableEq α] argument to your function so it can synthesize.

Alternatively, since there is no need to know that alpha is decidableeq since yoou only want to check for equality to the empty list you might as well simply pattern match:

match h: s.stuff with
| [] => ...
| x :: xs =>

which in general just simplifies your program largely because there is no need for the head and tail stuff anymore in the first place

Ah no this was an #mwe I constructed to express my question on how to reason with conditionals. In each of the respective branches of the conditional if then else, the if condition is either true or false.

[Shreyas Srinivas]

Adding [DecidableEq α] helps in this example

[Shreyas Srinivas]

thanks a lot :)

[Shreyas Srinivas]

I guess a better example would have a condition that is not a pattern match. (something like n > m where n and m are naturals.

[Kyle Miller]

It's worth knowing that you can either stick with the == side of things and use docs4#LawfulBEq, or you can switch to = and use DecidableEq. In both cases you get a decidable equality test that is also meaningful (in that it can either be turned into = or is already =).