fin n

Stream: new members

[Alex Zhang]

theorem test_1 (n : ℕ) : (∑ i in fin n, 1) = n :=
begin
  sorry
end

Why cannot I apply \sigma\ to fin n ?
The above gives me the error message
image.png

[Alex Zhang]

I am confused...

[Eric Wieser]

∑ i : fin n, 1

[Eric Wieser]

which is short for ∑ i in (finset.univ : finset (fin n)), 1 (docs#finset.univ)

[Alex Zhang]

Thank you, Eric!

[Johan Commelin]

@Alex Zhang the difference is whether you sum over a set (i.e. a subset) or over the full type.
In the first case you use i in s, in the second i : X.

[Alex Zhang]

Thanks for all your kind help above!
This formalization using fin n gives me the error message:
image.png

theorem test_1 (n j: nat)(i : fin n) (h: i <(j+1)): 1=1 :=
begin
  sorry
end

Why does this happen and how can I fix this issue?

[Anne Baanen]

This happens when checking i < j + 1 because Lean does the following to check the types:

• the two sides of < should have the same type
• let's check i: this is a fin n, so the other side should also be a fin n
• let's check j + 1: the two sides of + should have the same type, namely fin n
• j is not a fin n but a ℕ, and there's no coercion from ℕ to fin n, error!

[Anne Baanen]

The solution is to hint that you actually want to compare the two values as natural numbers:

theorem test_1 (n j: nat)(i : fin n) (h: (i : ℕ) < j + 1) : 1=1 :=
begin
  sorry
end

[Anne Baanen]

• the two sides of < should have the same type
• let's check (i : ℕ): this is obviously a ℕ, so the other side should also be a ℕ
• let's check that i is a ℕ: it's actually a fin n, but I know how to convert from fin n to ℕ (docs#fin.fin_to_nat), so apply the coercion
• let's check j + 1: the two sides of + should have the same type, namely ℕ
• ...

[Kevin Buzzard]

@Alex Zhang remember that i : fin n does not mean "$i$ is a natural number, and somewhere in the system there is a proof that $i<n$". It means "i is a pair, consisting of a natural number i.1 and a proof i.2 that i.1 < n". You are confusing i and i.1.

[Kevin Buzzard]

PS I cannot see your screenshots very well at all on my device. Can you just cut and paste errors in between triple quotes like you quote your code? People usually reserve screenshots only for issues which are VS Code specific.

[Alex Zhang]

Anne Baanen said:

The solution is to hint that you actually want to compare the two values as natural numbers:

theorem test_1 (n j: nat)(i : fin n) (h: (i : ℕ) < j + 1) : 1=1 :=
begin
  sorry
end

Cool! I can only fix it by changing the direction of < before..which looks like a silly way.

[Kevin Buzzard]

Yes, because > is illegal :-)

[Alex Zhang]

Kevin Buzzard said:

PS I cannot see your screenshots very well at all on my device. Can you just cut and paste errors in between triple quotes like you quote your code? People usually reserve screenshots only for issues which are VS Code specific.

Got it and no problem!

[Kevin Buzzard]

Either that or I'll have to go and find my glasses :-)