Setting value of vector

Stream: new members

[Benjamin]

I'm trying to write the following code:

def set_zero (L : Vector Nat n) (i : Nat) : Vector Nat n :=
    if i < n then L.set i 0 else L

I get the following error:

failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid

I have tried to provide a proof that the index is in bounds, but I can't get the syntax right. How can I fix this?

[Kevin Buzzard]

I don't know anything about Vector but does if h : i < n then... help?

[Benjamin]

That does work, thanks. But in my actual application, I have something like if h : i < n && j < n then ..., and it no longer works there.

[Benjamin]

I guess I need a function that transforms i < n && j < nto i < n. If I were using Coq, I would use the Search tactic to find such a function. How can I do this in Lean?

[Benjamin]

I fixed it by replacing && with /\, although I'm not sure why that fixes it.

[Matt Diamond]

do you understand the difference between && and /\?

[Benjamin]

I think I do. Since I'm working with decidable propositions, I figured I should use &&.

[Matt Diamond]

nah, you can use the propositional /\ instead of the boolean &&... if A and B are decidable then A /\ B is decidable

[Matt Diamond]

&& ends up doing some conversion to boolean that you don't need

[Matt Diamond]

I think that's why && didn't work... you end up losing the propositional information and just combining the whole thing into one true value

[Matt Diamond]

on the subject of looking for functions, one method is to use the exact? and apply? tactics

[Matt Diamond]

Loogle is also useful

[Kevin Buzzard]

Lean has a Decidable typeclass, so you can feel free to work with the more powerful Prop universe and still keep track of decidability. For example i < n is a decidable Prop but it's still a Prop and if still works constructively.