Zulip Chat Archive

Stream: new members

Topic: syntax question


Chase Norman (Sep 29 2020 at 05:47):

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 (Sep 29 2020 at 06:02):

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 (Sep 29 2020 at 06:05):

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 (Sep 29 2020 at 06:06):

My method scales. Do you know about pi types?

Kevin Buzzard (Sep 29 2020 at 06:07):

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 (Sep 29 2020 at 06:13):

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 (Sep 29 2020 at 06:17):

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


Last updated: Dec 20 2023 at 11:08 UTC