Interaction of Bool and Prop

Stream: lean4

[Avi Craimer]

In principle I understand the difference between Bool and Prop, but I'm still struggling to do fairly simple things with them.

Like suppose I want to have an if then else block where the if checks a condition and then calls a function that requires a proof in the then block. How do I convert the boolean check to the necessary proof term?

Here's an example. I've previously defined a custom null constructor.

def getByIndex (list: List α ) (i: Nat) :=  If i < list.length then  list.get i else null

Of course this doesn't work because list.get requires and argument of type Fin (List.length list) which is a dependent pair where the second item in the pair is a proof that the nat in the first place is less than length. It seems like it should be possible to construct this here since I've done the check in the if, but I can't figure out the syntax.

---

Update: thinking about it a bit more I solved my problem using a local definition with pattern matching to define a get function in the context of my definition.

 (instanciation:
  let get := fun (list: List El) (i:Nat) =>
    match list.get? i with
    | Option.none => nothing
    | Option.some el => el
  ∀ (r x:El), r ≠ x ∧ x ∈ inst r → ∀ (y:El), ∀(i:Nat), y = get (connect x) i  ↔ y ∈  inst (get (connect r ) i)
  )

It works! Not sure if there is a better way to do it.

[Thomas Murrills]

I think the syntax you’re looking for in the first part may be

if h : i < list.length then
  body1
else
  body2

There are many other cases of this sort of pattern (where we want a hypothesis in a context we’ve created) and “put h : before the appropriate part of the syntax” is usually the way to get it into the local context :) (other examples include for and match)

[Avi Craimer]

Thanks Thomas! That is great, so obvious in hindsight.

Here is my example re-worked a bit.

def getWithCustomNull (null: α) (list:List α) (i:Nat) :=
if h : i < list.length then
  list.get ⟨i, h⟩
else
  null

But it leads to another question. How does Lean know whether h exists? Does this only work for decidable propositions? Otherwise, you'd need to provide h as an argument to the function right?

[Kyle Miller]

Yes, if p then x else y needs Decidable p in general

[Kyle Miller]

The underlying functions for if notation are docs#ite for the non-dependent if-then-else and docs#dite for the dependent if-then-else.

[Eric Wieser]

Otherwise, you'd need to provide h as an argument to the function right?

If your function uses if h : P then ... else ... and P is not decidable apriori, then you usually add [Decidable P] to your function.

[Eric Wieser]

(Unless you know that P is undecidable, in which case you should add letI := Classical.dec P to the definition instead)

[Kyle Miller]

(that's assuming you're not writing programs you intend to execute -- it's good for math definitions)

[Kyle Miller]

@Avi Craimer By the way, do you know about docs#List.getD ? This appears to be the function you've written.