properties of finsets

Stream: new members

[Iocta]

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

[Iocta]

How to deal with this?

[Mario Carneiro]

what's up with those decidability assumptions?

[Mario Carneiro]

Just add open_locale classical to the top of the file

[Mario Carneiro]

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

[Mario Carneiro]

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

[Iocta]

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

[Mario Carneiro]

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

[Scott Morrison]

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.

[Mario Carneiro]

I thought this was part of open_locale classical

[Scott Morrison]

Oh! Maybe it is, sorry.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Iocta]

ok

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Iocta]

How do I get a finset from finite s?

[Mario Carneiro]

docs#set.finite.exists_finset

[Iocta]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Iocta]

Oh, oops

[Mario Carneiro]

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