Error due to several linear_order on N

Stream: general

[Rémy Degenne]

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]

The example you posted works for me?

[Mario Carneiro]

Do you perhaps have open_locale classical in your file?

[Rémy Degenne]

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

[Rémy Degenne]

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]

open_locale classical is better, because it adjusts more carefully the priorities.

[Sebastien Gouezel]

Your snippet works with open_locale classical, and hopefully the rest of your file should also work.

[Rémy Degenne]

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]

#mwe with open_locale classical?

[Rémy Degenne]

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]

Otherwise, you can post a gist to your file

[Rémy Degenne]

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

[Rémy Degenne]

but I'll try and extract something short

[Kevin Buzzard]

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]

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

[Rémy Degenne]

in measure_space.lean

[Kevin Buzzard]

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

[Rémy Degenne]

yes it is

[Rémy Degenne]

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]

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]

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]

      { 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]

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]

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]

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

[Kevin Buzzard]

This is just a trick I've seen before.

[Rémy Degenne]

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

[Kevin Buzzard]

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

[Rémy Degenne]

no, the others are fine.

[Kevin Buzzard]

OK I pushed -- independence.lean is compiling again with open_locale classical.

[Rémy Degenne]

Thanks!

[Kevin Buzzard]

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