Dependent props

Stream: new members

[uwagjaynoi]

I have a function that iterates over an array of bool and returns some index or none (using number n) which finds any index of bool.tt.
I want to prove that either all elements are ff, or it get "some" index, and this index is correct(tt).
However, I have to prove idx < n first to call array.read.
In brief, I want to prove two Props that one depends on the other.
Should I use dependent type like what I have written? or it there better way to express it?
(I know there's array.read', but it's more a general question.)
Thanks!

noncomputable theory
constants (n:ℕ)
def func: array n bool → fin n.succ := sorry
theorem th(ar: array n bool): (∀u, ar.read u = ff) ∨ (∃(h:(func ar).1 < n), ar.read ⟨(func ar).1,h⟩ = tt):= sorry

[Eric Wieser]

Using Exists like that is fairly reasonable

[uwagjaynoi]

Thank you!

[Notification Bot]

uwagjaynoi has marked this topic as resolved.

[Notification Bot]

uwagjaynoi has marked this topic as unresolved.