# Zulip Chat Archive

## Stream: general

### Topic: Error due to several linear_order on N

#### Rémy Degenne (Jan 17 2021 at 10:36):

In the following code, I have an error at the last line of the lemma. It is apparently due to the two max involved (in `h`

and in the goal) being defined through different `linear_order`

on N. I am not exactly sure of what happens there. How do I go around that difficulty?

```
import data.finset.intervals
local attribute [instance] classical.prop_decidable
/-- A set `s` is sup-closed if for all `t₁, t₂ ∈ s`, `t₁ ⊔ t₂ ∈ s`. -/
def sup_closed {α} [has_sup α] (s : set α) : Prop := ∀ t1 t2, t1 ∈ s → t2 ∈ s → t1 ⊔ t2 ∈ s
lemma sup_closed_tail_finset_set (N : ℕ) :
sup_closed {s : finset ℕ | ∃ r : ℕ, s = finset.Ico N (N+r+1)} :=
begin
rintros s1 s2 ⟨r1, hs1⟩ ⟨r2, hs2⟩,
use (r1 ⊔ r2),
have hr : ∀ r : ℕ, N ≤ N + r + 1,
{ intro r,
rw add_assoc,
nth_rewrite 0 ←add_zero N,
exact add_le_add_left (zero_le _) N, },
rw [finset.sup_eq_union s1 s2, hs1, hs2, sup_eq_max, ←max_add_add_left, ←max_add_add_right],
have h := finset.Ico.union' (hr r1) (hr r2),
rw min_self at h,
exact h, -- error caused by two different linear_order on ℕ
end
```

#### Shing Tak Lam (Jan 17 2021 at 10:38):

The example you posted works for me?

#### Mario Carneiro (Jan 17 2021 at 10:38):

Do you perhaps have `open_locale classical`

in your file?

#### Rémy Degenne (Jan 17 2021 at 10:40):

I added the line that apparently causes the error : `local attribute [instance] classical.prop_decidable`

#### Rémy Degenne (Jan 17 2021 at 10:42):

but if I remove that from my original file, I get errors in many other theorems. Should I add decidable hypotheses to all lemma instead of having that line on top of the file?

#### Sebastien Gouezel (Jan 17 2021 at 10:44):

`open_locale classical`

is better, because it adjusts more carefully the priorities.

#### Sebastien Gouezel (Jan 17 2021 at 10:44):

Your snippet works with `open_locale classical`

, and hopefully the rest of your file should also work.

#### Rémy Degenne (Jan 17 2021 at 10:46):

I get errors at different places, of the same type, like

```
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
semilattice_sup_bot.to_semilattice_sup (finset ℕ)
inferred
semilattice_sup_bot.to_semilattice_sup (finset ℕ)
```

#### Sebastien Gouezel (Jan 17 2021 at 10:48):

#mwe with `open_locale classical`

?

#### Rémy Degenne (Jan 17 2021 at 10:49):

I'll try and make one, but it will take a while. That error is in the middle of a lemma near the end of a big new file with long proofs :)

#### Sebastien Gouezel (Jan 17 2021 at 10:52):

Otherwise, you can post a gist to your file

#### Rémy Degenne (Jan 17 2021 at 10:57):

It's in that file : https://github.com/leanprover-community/mathlib/blob/independence/src/measure_theory/independence.lean

#### Rémy Degenne (Jan 17 2021 at 10:58):

but I'll try and extract something short

#### Kevin Buzzard (Jan 17 2021 at 11:02):

Are the errors like

```
invalid field notation, 'smul_finite' is not a valid "field" because environment does not contain 'measure_theory.measure.smul_finite'
μ
which has type
measure α
```

expected (in `indep2_of_indep2_sets_of_pi_system_aux`

)? Is this related?

#### Rémy Degenne (Jan 17 2021 at 11:03):

That function should exist on that branch. There are two new lemma outside of independence.lean

#### Rémy Degenne (Jan 17 2021 at 11:04):

in measure_space.lean

#### Kevin Buzzard (Jan 17 2021 at 11:04):

Then maybe you should give a mathlib branch to look at and not a gist. It's `independence`

, right?

#### Rémy Degenne (Jan 17 2021 at 11:04):

yes it is

#### Rémy Degenne (Jan 17 2021 at 11:06):

In short, the situation is that all was working well until I merged master into the branch a few days ago. And now I am trying to understand what changed.

#### Kevin Buzzard (Jan 17 2021 at 11:14):

The issue seems to be that because `finset`

is constructive (i.e. often wants a proof of decidable equality), and your finite sets of naturals sometimes seem to sometimes have the actual proof of decidable equality and sometimes the magic (classical) one. Her's a fix for `aux_t1_inter_t2`

:

```
lemma aux_t1_inter_t2 {α} (N r : ℕ) (f1 f2 : ℕ → set α) (p1 p2 : finset ℕ)
(hp1 : p1 = finset.range N) (hp2 : p2 = finset.Ico N (N + r + 1)) :
((⋂ (i : ℕ) (hp : i ∈ p1), f1 i) ∩ ⋂ (i : ℕ) (hp : i ∈ p2), f2 i)
= ⋂ (i : ℕ) (h_le : i ∈ finset.range (N + r + 1)),
(ite (i ∈ p1) (f1 i) set.univ ∩ ite (i ∈ p2) (f2 i) set.univ) :=
begin
rw finset.Inter_inter_Inter_eq_Inter_ite,
have h_congr : p1 ∪ p2 = finset.range (N + r + 1),
{ rw [hp1, hp2, ←finset.Ico.zero_bot, ←finset.Ico.zero_bot],
have h_le : N ≤ N + r + 1,
{ rw add_assoc,
nth_rewrite 0 ←add_zero N,
exact add_le_add_left (zero_le _) N, },
rw ←finset.Ico.union_consecutive (zero_le N) h_le },
congr,
ext1 i,
congr,
{ convert h_congr, },
ext1 x,
{ congr', convert h_congr, },
exact λ a a' haa', by congr',
end
```

but I am not offering an explanation as to what has changed, just a workaround.

#### Kevin Buzzard (Jan 17 2021 at 11:15):

I am changing `refl`

to `congr'`

and `exact`

to `convert`

because these tactics know that by proof irrelevance it often doesn't matter which algorithm we are using (the concrete one or the one that doesn't actually exist).

#### Kevin Buzzard (Jan 17 2021 at 11:16):

```
{ convert @is_measurable.ite α (s i) _ _ _ (hf1m i) (λ _, @is_measurable.univ α (s i)), },
{ convert @is_measurable.ite α (s i) _ _ _ (hf2m i) (λ _, @is_measurable.univ α (s i)), }, },
```

fixes `head_n_indep_tail_n_pi_systems`

. This is a very impressive looking piece of work by the way! Many thanks!

#### Rémy Degenne (Jan 17 2021 at 11:17):

Thanks a lot for the help! I never used `convert`

until now. I'll read its doc. There are so many tactics I am still not aware of.

#### Kevin Buzzard (Jan 17 2021 at 11:18):

and adding `by convert`

fixes your last error:

```
have h_pi_head : is_pi_system p_head,
from is_pi_system_pi_system_Union_Inter (λ n, (s n).is_measurable') h_pi {finset.range N}
(by convert sup_closed_singleton (finset.range N)),
...
have h_pi_tail : is_pi_system p_tail,
from is_pi_system_pi_system_Union_Inter (λ n, (s n).is_measurable') h_pi S_tail
(by convert sup_closed_tail_finset_set N),
```

#### Kevin Buzzard (Jan 17 2021 at 11:18):

Shall I just push to the branch? I am not answering your question, I am just solving the problem at hand.

#### Kevin Buzzard (Jan 17 2021 at 11:18):

This is just a trick I've seen before.

#### Rémy Degenne (Jan 17 2021 at 11:19):

Yes if you could push these, that would be great!

#### Kevin Buzzard (Jan 17 2021 at 11:19):

Are there errors in other files? I didn't check.

#### Rémy Degenne (Jan 17 2021 at 11:19):

no, the others are fine.

#### Kevin Buzzard (Jan 17 2021 at 11:20):

OK I pushed -- `independence.lean`

is compiling again with `open_locale classical`

.

#### Rémy Degenne (Jan 17 2021 at 11:21):

Thanks!

#### Kevin Buzzard (Jan 17 2021 at 11:21):

Many thanks for this work! This looks like a very impressive addition to mathlib. I'm happy to help!

Last updated: May 14 2021 at 00:42 UTC