Zulip Chat Archive

Stream: general

Topic: Error due to several linear_order on N


view this post on Zulip 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

view this post on Zulip Shing Tak Lam (Jan 17 2021 at 10:38):

The example you posted works for me?

view this post on Zulip Mario Carneiro (Jan 17 2021 at 10:38):

Do you perhaps have open_locale classical in your file?

view this post on Zulip Rémy Degenne (Jan 17 2021 at 10:40):

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

view this post on Zulip 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?

view this post on Zulip Sebastien Gouezel (Jan 17 2021 at 10:44):

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

view this post on Zulip 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.

view this post on Zulip 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 )

view this post on Zulip Sebastien Gouezel (Jan 17 2021 at 10:48):

#mwe with open_locale classical?

view this post on Zulip 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 :)

view this post on Zulip Sebastien Gouezel (Jan 17 2021 at 10:52):

Otherwise, you can post a gist to your file

view this post on Zulip 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

view this post on Zulip Rémy Degenne (Jan 17 2021 at 10:58):

but I'll try and extract something short

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Rémy Degenne (Jan 17 2021 at 11:04):

in measure_space.lean

view this post on Zulip 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?

view this post on Zulip Rémy Degenne (Jan 17 2021 at 11:04):

yes it is

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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),

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 17 2021 at 11:18):

This is just a trick I've seen before.

view this post on Zulip Rémy Degenne (Jan 17 2021 at 11:19):

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

view this post on Zulip Kevin Buzzard (Jan 17 2021 at 11:19):

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

view this post on Zulip Rémy Degenne (Jan 17 2021 at 11:19):

no, the others are fine.

view this post on Zulip Kevin Buzzard (Jan 17 2021 at 11:20):

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

view this post on Zulip Rémy Degenne (Jan 17 2021 at 11:21):

Thanks!

view this post on Zulip 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