Zulip Chat Archive

Stream: new members

Topic: properties of finsets


view this post on Zulip Iocta (Aug 19 2020 at 03:17):

import data.set.basic
import data.set.finite
import data.nat.basic

def p (s: set  ) [decidable (finite s)]:  := if finite s then 0 else 1

lemma p_finitely_additive :
 ¬ ( (a b : set  ) [decidable (finite a)] [decidable (finite b)] [decidable (finite (a  b))], p (a  b)  p a + p b ) :=
begin
    cases a.finite,
-- expected type:
-- a: set ℕ
-- b: set ℕ
-- _inst_1: decidable a.finite
-- _inst_2: decidable b.finite
-- _inst_3: decidable (a ∪ b).finite
-- ⊢ ℕ
-- Messages (3)
-- my2.lean:527:97
-- failed to synthesize type class instance for
-- a b : set ℕ,
-- _inst_1 : decidable a.finite,
-- _inst_2 : decidable b.finite,
-- _inst_3 : decidable (a ∪ b).finite
-- ⊢ decidable (a ∪ b).finite
-- my2.lean:527:109
-- failed to synthesize type class instance for
-- a b : set ℕ,
-- _inst_1 : decidable a.finite,
-- _inst_2 : decidable b.finite,
-- _inst_3 : decidable (a ∪ b).finite
-- ⊢ decidable a.finite
-- my2.lean:527:115
-- failed to synthesize type class instance for
-- a b : set ℕ,
-- _inst_1 : decidable a.finite,
-- _inst_2 : decidable b.finite,
-- _inst_3 : decidable (a ∪ b).finite
-- ⊢ decidable b.finite

end

view this post on Zulip Iocta (Aug 19 2020 at 03:17):

How to deal with this?

view this post on Zulip Mario Carneiro (Aug 19 2020 at 03:18):

what's up with those decidability assumptions?

view this post on Zulip Mario Carneiro (Aug 19 2020 at 03:18):

Just add open_locale classical to the top of the file

view this post on Zulip Mario Carneiro (Aug 19 2020 at 03:18):

it's not like that sort of property is actually computable in practice

view this post on Zulip Mario Carneiro (Aug 19 2020 at 03:21):

import data.set.basic
import data.set.finite
import data.nat.basic

noncomputable theory
open_locale classical
open set

def p (s: set ) :  := if finite s then 0 else 1

lemma p_finitely_additive : ¬ ( (a b : set ), p (a  b)  p a + p b) :=
begin
  push_neg,
  use [, ], simp [p],
end

view this post on Zulip Iocta (Aug 19 2020 at 03:39):

I don't have the intuition of when I need [decidable _] or noncomputable

view this post on Zulip Mario Carneiro (Aug 19 2020 at 03:45):

use noncomputable theory and then you don't have to worry about the noncomputable marker

view this post on Zulip Scott Morrison (Aug 19 2020 at 03:45):

If you're doing constructive mathematics, or something explicitly algorithmic, use decidable. Otherwise throw in open_locale classical at the first sign of trouble. After that, only add noncomputable if you see an error message telling you to. If you find yourself writing noncomputable more than once or twice in a file, add noncomputable theory at the top of the file.

view this post on Zulip Mario Carneiro (Aug 19 2020 at 03:46):

I thought this was part of open_locale classical

view this post on Zulip Scott Morrison (Aug 19 2020 at 03:46):

Oh! Maybe it is, sorry.

view this post on Zulip Mario Carneiro (Aug 19 2020 at 03:46):

it's not, at least if my test above is any indication

view this post on Zulip Mario Carneiro (Aug 19 2020 at 03:49):

here's a way to abuse the localized command to make it work:

localized "attribute [instance, priority 9] classical.prop_decidable
  noncomputable theory" in classical

open_locale classical
open set

def p (s: set ) :  := if finite s then 0 else 1

view this post on Zulip Iocta (Aug 19 2020 at 03:59):

ok

view this post on Zulip Kenny Lau (Aug 19 2020 at 06:44):

@Iocta the format is (s : set ℕ), i.e. spaces around the colon and no spaces near the brackets

view this post on Zulip Kenny Lau (Aug 19 2020 at 06:45):

and what is it with the double negation in your statement?

view this post on Zulip Kenny Lau (Aug 19 2020 at 06:49):

import data.set.basic
import data.set.finite
import data.nat.basic
import data.nat.parity

noncomputable theory
open_locale classical

open set

def p (s : set ) :  := if s.finite then 0 else 1

lemma not_p_union_eq_p_add_p : ¬∀ (a b : set ), p (a  b) = p a + p b :=
begin
  intro h, specialize h { n | n % 2 = 0 } {n | n % 2 = 1}, unfold p at h,
  rw [if_neg, if_neg, if_neg] at h, cases h,
  { sorry }, -- ¬{n : ℕ | n % 2 = 1}.finite
  { sorry }, -- ¬{n : ℕ | n % 2 = 0}.finite
  { sorry }  -- ¬({n : ℕ | n % 2 = 0} ∪ {n : ℕ | n % 2 = 1}).finite
end

view this post on Zulip Iocta (Aug 19 2020 at 20:20):

How do I get a finset from finite s?

view this post on Zulip Mario Carneiro (Aug 19 2020 at 20:22):

docs#set.finite.exists_finset

view this post on Zulip Iocta (Aug 19 2020 at 20:44):

How do I make evens_not_finite visible inside cases h?

import analysis.normed_space.indicator_function
import measure_theory.set_integral
import analysis.specific_limits
import data.real.basic
import data.nat.basic
import algebra.geom_sum
import tactic.fin_cases
import data.set.basic
import set_theory.cardinal_ordinal


example : ¬∀ (a b : set ),  p (a  b) = p a + p b :=
-- XXX Should also require (distinct: a ≠  b).
begin
  intro h,
  let evens := { n | n % 2 = 0 },
  let odds := { n | n % 2 = 1 },
  specialize h evens odds,
  have: evens  odds,
  {
    have zero_even: 0  evens, sorry,
    have zero_not_odd: 0  odds, sorry,
    intro h',
    sorry,
  },
  unfold p at h,
  rw [if_neg, if_neg, if_neg] at h,
  have odds_not_finite: ¬odds.finite,
  {
    intro h',
    have exists_finset_odds:  fset: finset  ,  x, (x  fset  x  odds ),
    {        exact finite.exists_finset h',    },
    cases exists_finset_odds with finset_odds hfinset_odds,
    have finset_odds_bdd_above:  m: nat,  n  finset_odds, n  m, {exact finset.exists_le finset_odds,},
    cases finset_odds_bdd_above with m hm,
    have hodd_max: m + 2  finset_odds  m + 1  finset_odds, sorry,
    cases hodd_max,
    {
        specialize hm (m + 2) hodd_max,
        finish,
    },
    {
        specialize hm (m + 1) hodd_max,
        finish,
    }
  },
  have evens_not_finite: ¬ evens.finite,
  {
      intro h',
      sorry,
  },
  cases h,
  {
    -- exact odds_not_finite, -- unknown identifier
    sorry,
  },
  {
    -- exact evens_not_finite, -- unknown identifier
    sorry,
  },
  {
    show ¬(evens  odds).finite,
    intro h',
    -- Union of infinite sets is infinite, combining previous two results.
    sorry,
  }
end

view this post on Zulip Mario Carneiro (Aug 19 2020 at 20:55):

your formatting does not make it clear that the rw [if_neg, if_neg, if_neg] at h line produces 4 subgoals

view this post on Zulip Mario Carneiro (Aug 19 2020 at 20:58):

here it is again with better braces:

example : ¬∀ (a b : set ),  p (a  b) = p a + p b :=
-- XXX Should also require (distinct: a ≠  b).
begin
  intro h,
  let evens := { n | n % 2 = 0 },
  let odds := { n | n % 2 = 1 },
  specialize h evens odds,
  have: evens  odds,
  { have zero_even: 0  evens, sorry,
    have zero_not_odd: 0  odds, sorry,
    intro h',
    sorry },
  unfold p at h,
  rw [if_neg, if_neg, if_neg] at h,
  { have odds_not_finite: ¬odds.finite,
    { intro h',
      have exists_finset_odds:  fset: finset  ,  x, (x  fset  x  odds ),
      { exact finite.exists_finset h' },
      cases exists_finset_odds with finset_odds hfinset_odds,
      have finset_odds_bdd_above:  m: nat,  n  finset_odds, n  m, {exact finset.exists_le finset_odds,},
      cases finset_odds_bdd_above with m hm,
      have hodd_max: m + 2  finset_odds  m + 1  finset_odds, sorry,
      cases hodd_max,
      { specialize hm (m + 2) hodd_max,
        finish },
      { specialize hm (m + 1) hodd_max,
        finish } },
    have evens_not_finite: ¬ evens.finite,
    { intro h',
      sorry },
    cases h },
  { -- exact odds_not_finite, -- unknown identifier
    sorry },
  { -- exact evens_not_finite, -- unknown identifier
    sorry },
  { show ¬(evens  odds).finite,
    intro h',
    -- Union of infinite sets is infinite, combining previous two results.
    sorry }
end

view this post on Zulip Mario Carneiro (Aug 19 2020 at 20:59):

the problem should now be clear: you did all the haves inside a pointless branch that was proving h : 1 = 1 + 1 |- false, before finishing it with cases h

view this post on Zulip Iocta (Aug 19 2020 at 21:01):

Oh, oops

view this post on Zulip Mario Carneiro (Aug 19 2020 at 21:01):

and here it is with the subgoals appropriately distributed:

example : ¬∀ (a b : set ),  p (a  b) = p a + p b :=
-- XXX Should also require (distinct: a ≠  b).
begin
  intro h,
  let evens := { n | n % 2 = 0 },
  let odds := { n | n % 2 = 1 },
  specialize h evens odds,
  have: evens  odds,
  { have zero_even: 0  evens, sorry,
    have zero_not_odd: 0  odds, sorry,
    intro h',
    sorry },
  unfold p at h,
  rw [if_neg, if_neg, if_neg] at h,
  { cases h },
  { show ¬ odds.finite,
    intro h',
    have exists_finset_odds:  fset: finset  ,  x, (x  fset  x  odds ),
    { exact finite.exists_finset h' },
    cases exists_finset_odds with finset_odds hfinset_odds,
    have finset_odds_bdd_above:  m: nat,  n  finset_odds, n  m, {exact finset.exists_le finset_odds,},
    cases finset_odds_bdd_above with m hm,
    have hodd_max: m + 2  finset_odds  m + 1  finset_odds, sorry,
    cases hodd_max,
    { specialize hm (m + 2) hodd_max,
      finish },
    { specialize hm (m + 1) hodd_max,
      finish } },
  { show ¬ evens.finite,
    intro h',
    sorry },
  { show ¬(evens  odds).finite,
    intro h',
    -- Union of infinite sets is infinite, combining previous two results.
    sorry }
end

Last updated: May 18 2021 at 17:44 UTC