Beginner questions about equalities

Stream: lean4

[Tom]

This will be long, I am sorry for the wall of text. I started tonight trying to figure out how to use List.head. After some searching, this is what I wrote (Note that I'm aware of the other versions of head*, this is just for learning purposes)

def test (xs: List α): Option α :=
  if h1: xs != [] then
    some (xs.head h1)
  else
    none

However, this doesn't work because != is expecting a BEq instance. I searched the Lean code and came across the typeclass. So I did

def test (xs: List α) [BEq α]: Option α :=
  if h1: xs != [] then
    some (xs.head h1)
  else
    none

However, now the error is

  h1
has type
  (xs != []) = true : Prop
but is expected to have type
  xs ≠ [] : Prop

Now, this made me think that BEq is not the right typeclass here; so I tried using DecidableEq instead but still no luck. The error actually stays the same. Then I noticed that the error is not using != but ≠ (\ne). Switching to that, I was able to get the function to typecheck and #eval.

I've been scouring the documentation for DecidableEq and BEq and the two operators (!= vs ≠) but have had no luck. So my first question is: Could someone please shed some light on the differences? Looking at BEq it just seems like it's for supporting boolean equality. But the few examples here on Zulip and in the documentation I was able to find do both

structure ...
deriving BEq/DecidableEq

and I can't see any reason to use one over the other.
Upon reflection, it seems that DecidableEq is for creating Props (with = and \ne), while BEq is for creating (runtime) Bool comparisons using == and != but I'm not sure. However, it also seems that DecidableEq works for all my examples instead of BEq; any examples for picking on over the other?

Thank you.

[James Gallicchio]

Yeah, this isn't super straightforward...

• If a prop P is decidable (e.g. there is an instance of the typeclass Decidable P) then we can decide P to get a boolean value for P's truthiness
• DecidableEq A basically means Decidable (a = b) for any a b : A. So, given two elements of the type, we can decide whether they are equal or not
• Lean will coerce decidable Props to Bools if the expected type is a bool. So, here, you write the proposition xs \ne [], but since it expects a Bool it rewrites the if condition as decide (xs \ne []), which is fine since DecidableEq (List α)

[Chris Lovett]

You can just use head? which is defined like this:

def head? : List α → Option α
  | []   => none
  | a::_ => some a

[James Gallicchio]

As for BEq A, this class seems to mean "there is a function A -> A -> Boolthat we call boolean equality" in the same way that Mul A means "there is a function A -> A -> A that we call multiplication" i.e. there's no propositional meaning to it.

I'm not really sure when you'd want to use BEq over decidable equality (which, for most types is equivalent to the BEq instance, just with some propositional content). I think there might be built-in types that have BEq instances but not DecidableEq instances on purpose (i.e. floats? i think?)

[James Gallicchio]

But this is definitely something that should be addressed in beginner tutorials, because most programmers automatically reach for == and != when learning a new language, even though it's rarely what you want to use in Lean.

[James Gallicchio]

Oh, and as a general note in line with what Chris said, pattern matching is almost always the way to go in Lean, even more so than non-dependently-typed functional languages. Eq terms can lead to messy type dependencies that Lean doesn't know how to solve, whereas pattern matching rarely makes a mess :)

[Tom]

Thanks @James Gallicchio !

What does the "Decidable Prop" refer to here? Is it decidable as in the "theory of computation/Turing Machine" decidable? For basic computations, when would something not be decidable? Since lean's functions (at least those which are not partial) are total and hence terminating... right?

Or is it "decidable" in the sense that I have a Prop and I don't have a proof (or have a proof that it's not decidable, as per Goedel's incompleteness; or something like the independence of the AoC from ZF)?

[Tom]

Thanks @Chris Lovett

This is purely a learning exercise. (I am aware of head?, head! and headD); I mostly trying to get to better grips with the interaction between programs with proofs and especially trying to figure out how to use head.

For example, it doesn't seem that pattern matching provides the proof that's required to use head (that is to say, I don't know how to do it). For example, modifying your example, this doesn't type check even though clearly the type in the second branch could be narrowed to l \ne []

def test : List α → Option α
  | []   => none
  | l@(a::_) => some (List.head l)

[Kevin Buzzard]

Decidable just means there's an algorithm for deciding if it's true or false. An example of an undecidable prop would be claiming that two real numbers were equal because there is no algorithm for deciding this in general.

[James Gallicchio]

Tom said:

Or is it "decidable" in the sense that I have a Prop and I don't have a proof

Exactly this; given an arbitrary P : Prop you don't have a proof of P. But if Decidable P then there is some algorithm to give you a proof of P or a proof of not P

[James Gallicchio]

Tom said:

For example, it doesn't seem that pattern matching provides the proof that's required to use head (that is to say, I don't know how to do it). For example, modifying your example, this doesn't type check even though clearly the type in the second branch could be narrowed to l \ne []

Yeah, if you use a @ pattern I'm not sure what information Lean exposes to you about the relationship between the left and right hand sides.

A more standard way to use pattern matching in this kind of situation is to pattern match on a term which appears in some proof term that you need to dispatch. For example:

def Vector (α n) := Fin n → α

def head? : {n : Nat} → Vector α n → Option α
| 0, _    => none
| _+1, i  => some (i ⟨0, Nat.succ_le_succ (Nat.zero_le _)⟩)

Here we are pattern matching on n, which changes the proposition we need to prove from 0 < n (not provable) to 0 < ?n + 1 (provable)

[James Gallicchio]

When you pattern match on a term, the term gets replaced everywhere, including in types that depend on it (e.g. in propositions you need to prove).

The same is not true when you do something like if h : n = 0 ...; you get a proof that h : n = 0 in the positive branch, but it doesn't replace n with zero in the positive branch's context.

[Tom]

@James Gallicchio

Cool, thanks! I was able to make it work using pattern matching:

def test (xs: List α) {he: xs ≠ []} : Option α :=
  match xs, he with
  | [], _   => none
  | l, r    => some (List.head l r)