syntax question

Stream: new members

[Chase Norman]

I'm a new Lean user and I'm trying to write a proposition about lists using an element-wise strategy. The following is a toy example:

def sorted : list ℕ → Prop := λ c : list ℕ, ∀ x : ℕ, x < c.length → list.nth_le c x

nth_le returns a type (x < c.length) → ℕ. How do I use my implication assumption to retrieve the natural number value? By extension, what if I needed the expression (x-1 < c.length)? Thanks.

[Kevin Buzzard]

I think the computer scientists know better ways to say a list is sorted, but you could put \forall (x : nat) (h : x < c.length), ...

[Chase Norman]

Yeah this is a toy example, I understand it's not necessary in this case. However I would like to know how to do it for a more complicated example.

[Kevin Buzzard]

My method scales. Do you know about pi types?

[Kevin Buzzard]

A pi type is more general than a function because the type of the output can depend on the input term. That's all I'm using here

[Chase Norman]

Oh I understand what you're saying now, thanks so much! As a side question, how many potential instances of x < c.length can exist? Are all instances of this Prop equivalent? My guess is that there will be no such element of the type when x >= c.length and 1 such element when x < c.length.

My understanding of pi types is that they are the type of a lambda function that receives the proper input and output types. Is this a correct understanding?

[Kevin Buzzard]

All proofs of a proposition are equal by definition in Lean so there's so issue there. Your guess is the right model. A pi type is exactly what you have here, it's just a statement like "for all n in S, n>=37" where the type n>=37 of the conclusion depends on the input term n