IsSetRing to CommRing

Stream: new members

[Iocta]

I tried to fill this where and it complains but I can't understand what it's talking about.

import Mathlib
import Mathlib.Data.Set.SymmDiff

namespace MeasureTheory

open MeasurableSpace

variable {α : Type}  {s : Set (Set α)} {m : MeasurableSpace α}



theorem symmDiff_zero (s : Set α) : symmDiff s ∅ = s := by
  exact symmDiff_eq_left.mpr rfl

theorem zero_symmDiff (s : Set α) : symmDiff ∅ s = s := by
  exact symmDiff_eq_right.mpr rfl



instance IsSetRing_CommRing (hs : IsSetRing s) : CommRing (Set α) where
  add := symmDiff
  add_assoc := symmDiff_assoc
  zero := ∅
  zero_add s := by {
    reduce
    simp only [imp_false, false_and, false_or]
    ext a
    constructor
    · intro h
      exact h.1
    · intro h
      constructor
      · exact h
      exact fun a ↦ a
  }
  add_zero := by {
    reduce
    simp
    intro s
    ext a
    constructor
    . intro h
      exact h.1
    intro ha
    constructor
    . exact ha
    . exact fun a ↦ a
  }
  nsmul n a := a
  add_comm := symmDiff_comm
  mul := Set.inter
  left_distrib := Set.inter_symmDiff_distrib_left
  right_distrib := Set.inter_symmDiff_distrib_right
  zero_mul := Set.empty_inter
  mul_zero := Set.inter_empty
  mul_assoc := Set.inter_assoc
  one := Set.univ
  one_mul := Set.univ_inter
  mul_one := Set.inter_univ
  neg := id
  zsmul z a := a
  neg_add_cancel := symmDiff_self
  mul_comm := Set.inter_comm


/-

α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
x✝ : Set α
⊢ (fun n a ↦ a) 0 x✝ = 0
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
x✝ : Set α
⊢ (fun n a ↦ a) 0 x✝ = 0
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
x✝ : Set α
⊢ (fun n a ↦ a) 0 x✝ = 0
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
n✝ : ℕ
x✝ : Set α
⊢ (fun n a ↦ a) (n✝ + 1) x✝ = (fun n a ↦ a) n✝ x✝ + x✝
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
n✝ : ℕ
x✝ : Set α
⊢ (fun n a ↦ a) (n✝ + 1) x✝ = (fun n a ↦ a) n✝ x✝ + x✝
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
n✝ : ℕ
x✝ : Set α
⊢ (fun n a ↦ a) (n✝ + 1) x✝ = (fun n a ↦ a) n✝ x✝ + x✝
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
⊢ NatCast.natCast 0 = 0
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
⊢ NatCast.natCast 0 = 0
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
n✝ : ℕ
⊢ NatCast.natCast (n✝ + 1) = NatCast.natCast n✝ + 1
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
n✝ : ℕ
⊢ NatCast.natCast (n✝ + 1) = NatCast.natCast n✝ + 1
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
x✝ : Set α
⊢ npowRecAuto 0 x✝ = 1
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
x✝ : Set α
⊢ npowRecAuto 0 x✝ = 1
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
n✝ : ℕ
x✝ : Set α
⊢ npowRecAuto (n✝ + 1) x✝ = npowRecAuto n✝ x✝ * x✝
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
n✝ : ℕ
x✝ : Set α
⊢ npowRecAuto (n✝ + 1) x✝ = npowRecAuto n✝ x✝ * x✝
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
a✝ b✝ : Set α
⊢ a✝ - b✝ = a✝ + -b✝
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
a✝ b✝ : Set α
⊢ a✝ - b✝ = a✝ + -b✝
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
a✝ : Set α
⊢ (fun z a ↦ a) 0 a✝ = 0
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
a✝ : Set α
⊢ (fun z a ↦ a) 0 a✝ = 0
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
a✝ : Set α
⊢ (fun z a ↦ a) 0 a✝ = 0
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
n✝ : ℕ
a✝ : Set α
⊢ (fun z a ↦ a) (↑n✝.succ) a✝ = (fun z a ↦ a) (↑n✝) a✝ + a✝
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
n✝ : ℕ
a✝ : Set α
⊢ (fun z a ↦ a) (↑n✝.succ) a✝ = (fun z a ↦ a) (↑n✝) a✝ + a✝
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
n✝ : ℕ
a✝ : Set α
⊢ (fun z a ↦ a) (↑n✝.succ) a✝ = (fun z a ↦ a) (↑n✝) a✝ + a✝
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
n✝ : ℕ
a✝ : Set α
⊢ (fun z a ↦ a) (Int.negSucc n✝) a✝ = -(fun z a ↦ a) (↑n✝.succ) a✝
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
n✝ : ℕ
a✝ : Set α
⊢ (fun z a ↦ a) (Int.negSucc n✝) a✝ = -(fun z a ↦ a) (↑n✝.succ) a✝
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
n✝ : ℕ
⊢ IntCast.intCast ↑n✝ = ↑n✝
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
n✝ : ℕ
⊢ IntCast.intCast ↑n✝ = ↑n✝
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
n✝ : ℕ
⊢ IntCast.intCast (Int.negSucc n✝) = -↑(n✝ + 1)
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
n✝ : ℕ
⊢ IntCast.intCast (Int.negSucc n✝) = -↑(n✝ + 1)
Messages (6)
01.lean:22:66
could not synthesize default value for field 'nsmul_zero' of 'AddMonoid' using tactics
01.lean:22:66
tactic 'rfl' failed, the left-hand side
  (fun n a ↦ a) 0 x✝
is not definitionally equal to the right-hand side
  0
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
x✝ : Set α
⊢ (fun n a ↦ a) 0 x✝ = 0
01.lean:22:66
could not synthesize default value for field 'nsmul_succ' of 'AddMonoid' using tactics
01.lean:22:66
tactic 'rfl' failed, the left-hand side
  (fun n a ↦ a) (n✝ + 1) x✝
is not definitionally equal to the right-hand side
  (fun n a ↦ a) n✝ x✝ + x✝
α : Type
s : Set (Set α)
m : MeasurableSpace α
hs : IsSetRing s
n✝ : ℕ
x✝ : Set α
⊢ (fun n a ↦ a) (n✝ + 1) x✝ = (fun n a ↦ a) n✝ x✝ + x✝
01.lean:22:66
could not synthesize default value for field 'zsmul_zero'' of 'Ring' using tactics
01.lean:22:66
could not synthesize default value for field 'zsmul_succ'' of 'Ring' using tactics
 -/

[Matt Diamond]

Huh, that's kind of weird... I went to add a proof for nsmul_zero and it said there were 26 goals. Not sure what's going on.

Maybe those are for other fields in the structure.

I mean you do have to prove ∀ x, nsmul 0 x = 0, and you defined it as nsmul n a := a, so I think that proposition is false. Maybe you need to change the definition of nsmul.

[Matt Diamond]

Lean provides docs#nsmulRec and docs#zsmulRec for defining nsmul and zsmul

[Daniel Weber]

This is a known bug which was fixed at lean#6408. Are you able to update your Lean version?

[Matt Diamond]

Ah, so the extra goals is a Lean bug, gotcha. I think there's also a separate problem with the definition, which is that nsmul and zsmul aren't defined correctly. (Though that might've been more obvious without the extra goals.)

@Iocta you can define nsmul as nsmulRec and define zsmul as zsmulRec. You might need to add Zero, Add, and Neg instances for Set α beforehand.

[Matt Diamond]

You could also define Set α as a BooleanRing via the existing BooleanAlgebra instance on Set α and docs#BooleanAlgebra.toBooleanRing. Then you automatically get a CommRing via BooleanRing.toCommRing and I believe it's the same structure you're trying to define? (+ is symm diff, * is intersection, etc.)

[Matt Diamond]

import Mathlib

variable {α : Type}

instance : BooleanRing (Set α) := BooleanAlgebra.toBooleanRing

#synth CommRing (Set α)

[Matt Diamond]

(though if what you're really trying to prove is that s is a CommRing, then that won't be sufficient)

[Matt Diamond]

in that case maybe you could construct a docs#Subring using the proof of IsSetRing and then you'll get the CommRing via docs#Subring.toCommRing

(Edit: Okay that might not work since s would need to contain 1 i.e. Set.univ...)