Why-provenance is an m-semiring
Lax392996.WhyProvenance · concepts/Lax392996/WhyProvenance.lean · lax-392996
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
For a set , is an m-semiring, where : an element is a family of witness sets, addition is union of families, multiplication is pairwise union of witnesses, and the monus is set difference of families, with the natural order being inclusion. The instance is built here, and the claims pin each operation to the stated one: exhibiting an m-semiring structure on is only half of the proposition, the operations have to be the right ones.
Concept map
Evidence
This concept declares 6 statements. Each proof establishes one of them relative to its assumptions.
1 Why.add_carrier proven
2 Why.isMSemiring proven
3 Why.monus_carrier proven
4 Why.mul_carrier proven
5 Why.one_carrier proven
6 Why.zero_carrier proven
In the paper
Lean source view on GitHub
| 1 | import Mathlib.Data.Set.Basic |
| 2 | import Mathlib.Data.Set.Insert |
| 3 | import Mathlib.Algebra.Ring.Defs |
| 4 | import Lax392996.SemiringsWithMonus |
| 5 | |
| 6 | /-! |
| 7 | --- |
| 8 | title: Why-provenance is an m-semiring |
| 9 | type: theorem |
| 10 | --- |
| 11 | For a set , |
| 12 | is an m-semiring, where : |
| 13 | an element is a family of witness sets, addition is union of families, |
| 14 | multiplication is pairwise union of witnesses, and the monus is set |
| 15 | difference of families, with the natural order being inclusion. The |
| 16 | instance is built here, and the claims pin each operation to the stated |
| 17 | one: exhibiting an m-semiring structure on is only half of the |
| 18 | proposition, the operations have to be the right ones. |
| 19 | -/ |
| 20 | |
| 21 | namespace Lax392996.WhyProvenance |
| 22 | |
| 23 | open Lax392996.SemiringsWithMonus |
| 24 | |
| 25 | variable {α : Type} |
| 26 | |
| 27 | /-- Why-provenance over `α`: a family of sets of witnesses. -/ |
| 28 | @[ext] |
| 29 | structure Why (α: Type) where |
| 30 | carrier : Set (Set α) |
| 31 | |
| 32 | instance instCoeWhySet : Coe (Why α) (Set (Set α)) := ⟨Why.carrier⟩ |
| 33 | |
| 34 | instance instZeroWhy : Zero (Why α) where |
| 35 | zero := ⟨∅⟩ |
| 36 | |
| 37 | instance instAddWhy : Add (Why α) where |
| 38 | add a b := ⟨a ∪ b⟩ |
| 39 | |
| 40 | /-- Pairwise union of witnesses, the multiplication of `Why α`. -/ |
| 41 | def why_mul (a b: Why α) : Why α := |
| 42 | ⟨{ z : Set α | ∃ x y : Set α, x ∈ a.carrier ∧ y ∈ b.carrier ∧ z = x ∪ y}⟩ |
| 43 | |
| 44 | instance instCommSemiringWhy : CommSemiring (Why α) where |
| 45 | one := ⟨{∅}⟩ |
| 46 | mul := why_mul |
| 47 | |
| 48 | add_assoc := by |
| 49 | intro a b c |
| 50 | simp [HAdd.hAdd, Add.add] |
| 51 | exact Set.union_assoc _ _ _ |
| 52 | |
| 53 | zero_add := by |
| 54 | intro a |
| 55 | show ⟨(⟨∅⟩ : Why α).carrier ∪ a.carrier⟩ = a |
| 56 | simp |
| 57 | |
| 58 | add_zero := by |
| 59 | intro a |
| 60 | show ⟨a.carrier ∪ (⟨∅⟩ : Why α).carrier⟩ = a |
| 61 | simp |
| 62 | |
| 63 | add_comm := by |
| 64 | intro a b |
| 65 | simp [HAdd.hAdd, Add.add] |
| 66 | exact Set.union_comm _ _ |
| 67 | |
| 68 | mul_assoc := by |
| 69 | intro a b c |
| 70 | unfold why_mul |
| 71 | ext w |
| 72 | simp [HMul.hMul] |
| 73 | apply Iff.intro |
| 74 | . intro h |
| 75 | obtain ⟨xa, xb, h₁, h₂⟩ := h |
| 76 | obtain ⟨hxa, hxb⟩ := h₁ |
| 77 | obtain ⟨xc, hxc, hw⟩ := h₂ |
| 78 | use xa, hxa, xb, xc |
| 79 | constructor |
| 80 | . use hxb, hxc |
| 81 | . simp[hw, Set.union_assoc] |
| 82 | |
| 83 | . intro h |
| 84 | obtain ⟨xa, hxa, xb, xc, hxbc, hw⟩ := h |
| 85 | use xa, xb |
| 86 | constructor |
| 87 | . use hxa, hxbc.1 |
| 88 | . use xc, hxbc.2 |
| 89 | simp[hw, Set.union_assoc] |
| 90 | |
| 91 | one_mul := by |
| 92 | intro a |
| 93 | show why_mul (⟨{∅}⟩: Why α) a = a |
| 94 | unfold why_mul |
| 95 | simp |
| 96 | |
| 97 | mul_one := by |
| 98 | intro a |
| 99 | show why_mul a (⟨{∅}⟩: Why α) = a |
| 100 | unfold why_mul |
| 101 | simp |
| 102 | |
| 103 | zero_mul := by |
| 104 | intro a |
| 105 | show why_mul (⟨∅⟩: Why α) a = (⟨∅⟩: Why α) |
| 106 | unfold why_mul |
| 107 | simp |
| 108 | |
| 109 | mul_zero := by |
| 110 | intro a |
| 111 | show why_mul a (⟨∅⟩: Why α) = (⟨∅⟩: Why α) |
| 112 | unfold why_mul |
| 113 | simp |
| 114 | |
| 115 | mul_comm := by |
| 116 | intro a b |
| 117 | show why_mul a b = why_mul b a |
| 118 | unfold why_mul |
| 119 | ext z |
| 120 | simp |
| 121 | apply Iff.intro |
| 122 | . intro h |
| 123 | obtain ⟨x, hx, y, hy, hz⟩ := h |
| 124 | use y, hy, x, hx |
| 125 | simp[hz, Set.union_comm] |
| 126 | . intro h |
| 127 | obtain ⟨y, hy, x, hx, hz⟩ := h |
| 128 | use x, hx, y, hy |
| 129 | simp[hz, Set.union_comm] |
| 130 | |
| 131 | left_distrib := by |
| 132 | intro a b c |
| 133 | show why_mul a ⟨b ∪ c⟩ = ⟨(why_mul a b) ∪ (why_mul a c)⟩ |
| 134 | unfold why_mul |
| 135 | ext z |
| 136 | simp |
| 137 | apply Iff.intro |
| 138 | . intro h |
| 139 | obtain ⟨x, hx, y, hy, hz⟩ := h |
| 140 | cases hy with |
| 141 | | inl hy' => |
| 142 | apply Or.inl |
| 143 | use x, hx, y, hy' |
| 144 | | inr hy' => |
| 145 | apply Or.inr |
| 146 | use x, hx, y, hy' |
| 147 | . intro h |
| 148 | cases h with |
| 149 | | inl h' => |
| 150 | obtain ⟨x, hx, y, hy, hz⟩ := h' |
| 151 | use x, hx, y |
| 152 | simp[hy, hz] |
| 153 | | inr h' => |
| 154 | obtain ⟨x, hx, y, hy, hz⟩ := h' |
| 155 | use x, hx, y |
| 156 | simp[hy, hz] |
| 157 | |
| 158 | right_distrib := by |
| 159 | intro a b c |
| 160 | show why_mul ⟨a ∪ b⟩ c = ⟨(why_mul a c) ∪ (why_mul b c)⟩ |
| 161 | unfold why_mul |
| 162 | simp |
| 163 | ext z |
| 164 | simp |
| 165 | apply Iff.intro |
| 166 | . intro h |
| 167 | obtain ⟨x, hx, y, hy, hz⟩ := h |
| 168 | cases hx with |
| 169 | | inl hx' => |
| 170 | apply Or.inl |
| 171 | use x, hx', y, hy |
| 172 | | inr hx' => |
| 173 | apply Or.inr |
| 174 | use x, hx', y, hy |
| 175 | . intro h |
| 176 | cases h with |
| 177 | | inl h' => |
| 178 | obtain ⟨x, hx, y, hy, hz⟩ := h' |
| 179 | use x |
| 180 | simp[hx] |
| 181 | use y |
| 182 | | inr h' => |
| 183 | obtain ⟨x, hx, y, hy, hz⟩ := h' |
| 184 | use x |
| 185 | simp[hx] |
| 186 | use y |
| 187 | |
| 188 | nsmul := nsmulRec |
| 189 | |
| 190 | /-- The support indicator: `𝟘` on the empty family, `𝟙` on any nonempty |
| 191 | one. This is the `δ` of `Why α`. -/ |
| 192 | def Why.deltaInd (a : Why α) : Why α := |
| 193 | ⟨{s | s = ∅ ∧ a.carrier.Nonempty}⟩ |
| 194 | |
| 195 | /-- Why-provenance is a semiring with monus: `∖` is set difference on the outer |
| 196 | level, `2^(2^X)` ordered by inclusion. -/ |
| 197 | instance instSemiringWithMonusWhy : SemiringWithMonus (Why α) where |
| 198 | le a b := a.carrier ⊆ b.carrier |
| 199 | le_refl := by simp |
| 200 | le_trans := by |
| 201 | intro a b c ha hb x hx |
| 202 | exact hb (ha hx) |
| 203 | |
| 204 | le_antisymm := by |
| 205 | intro a b ha hb |
| 206 | ext x |
| 207 | apply Iff.intro |
| 208 | . exact fun a ↦ ha (hb (ha a)) |
| 209 | . exact fun a ↦ hb (ha (hb a)) |
| 210 | |
| 211 | add_le_add_left := by |
| 212 | simp[HAdd.hAdd,Add.add] |
| 213 | intro a b hab c x hx |
| 214 | simp |
| 215 | apply Or.inl |
| 216 | exact hab hx |
| 217 | |
| 218 | add_le_add_right := by |
| 219 | simp[HAdd.hAdd,Add.add] |
| 220 | intro a b hab c x hx |
| 221 | simp |
| 222 | apply Or.inr |
| 223 | exact hab hx |
| 224 | |
| 225 | exists_add_of_le := by |
| 226 | intro a b hab |
| 227 | simp[HAdd.hAdd,Add.add] |
| 228 | use ⟨b.carrier \ a.carrier⟩ |
| 229 | ext x |
| 230 | simp |
| 231 | intro hx |
| 232 | exact hab hx |
| 233 | |
| 234 | le_self_add := by |
| 235 | intro a b x hx |
| 236 | simp[HAdd.hAdd,Add.add] |
| 237 | apply Or.inl |
| 238 | exact hx |
| 239 | |
| 240 | le_add_self := by |
| 241 | intro a b x hx |
| 242 | simp[HAdd.hAdd,Add.add] |
| 243 | apply Or.inr |
| 244 | exact hx |
| 245 | |
| 246 | sub a b := ⟨a.carrier \ b.carrier⟩ |
| 247 | monus_spec := by |
| 248 | intro a b c |
| 249 | simp[HAdd.hAdd,Add.add] |
| 250 | show (⟨a.carrier \ b.carrier⟩: Why α).carrier ⊆ c.carrier ↔ a.carrier ⊆ b.carrier ∪ c.carrier |
| 251 | apply Iff.intro |
| 252 | . intro h x hx |
| 253 | by_cases hx' : x ∈ b.carrier |
| 254 | . apply Or.inl |
| 255 | exact hx' |
| 256 | . apply Or.inr |
| 257 | have h' : x ∈ a.carrier \ b.carrier := by simp[hx, hx'] |
| 258 | exact h h' |
| 259 | . intro h x hx |
| 260 | simp at hx |
| 261 | obtain ⟨ha, hb⟩ := hx |
| 262 | have h' : x ∈ b.carrier ∪ c.carrier := h ha |
| 263 | simp at h' |
| 264 | tauto |
| 265 | |
| 266 | delta := Why.deltaInd |
| 267 | delta_zero := by |
| 268 | ext z |
| 269 | show z ∈ {s | s = ∅ ∧ (∅ : Set (Set α)).Nonempty} ↔ z ∈ (∅ : Set (Set α)) |
| 270 | simp |
| 271 | delta_natCast_pos := by |
| 272 | have hidem : ∀ a : Why α, a + a = a := fun a => by simp [(· + ·), Add.add] |
| 273 | have hone : (1 : Why α) ≠ 0 := by |
| 274 | intro h |
| 275 | have := congrArg Why.carrier h |
| 276 | exact Set.singleton_ne_empty (∅ : Set α) this |
| 277 | have hcast : ∀ {n : ℕ}, 0 < n → (n : Why α) = 1 := by |
| 278 | intro n hn |
| 279 | induction n with |
| 280 | | zero => omega |
| 281 | | succ m ih => |
| 282 | rcases Nat.eq_zero_or_pos m with hm | hm |
| 283 | · rw [hm]; simp |
| 284 | · rw [Nat.cast_succ, ih hm, hidem 1] |
| 285 | have hne : ∀ {a : Why α}, a ≠ 0 → Why.deltaInd a = 1 := by |
| 286 | intro a h |
| 287 | have hnonempty : a.carrier.Nonempty := by |
| 288 | rcases Set.eq_empty_or_nonempty a.carrier with he | hne |
| 289 | · exact absurd (by ext z; rw [he]; exact Iff.rfl) h |
| 290 | · exact hne |
| 291 | ext z |
| 292 | show z ∈ {s | s = ∅ ∧ a.carrier.Nonempty} ↔ z ∈ ({∅} : Set (Set α)) |
| 293 | simp [hnonempty] |
| 294 | intro n hn |
| 295 | rw [hcast hn, hne hone] |
| 296 | delta_absorb := fun a b => by |
| 297 | have hzsf : ∀ {a b : Why α}, a + b = 0 → a = 0 := by |
| 298 | intro a b h |
| 299 | have hc : a.carrier ∪ b.carrier = (∅ : Set (Set α)) := |
| 300 | congrArg Why.carrier h |
| 301 | have hx : a.carrier = ∅ := by |
| 302 | ext w |
| 303 | simp only [Set.mem_empty_iff_false, iff_false] |
| 304 | intro hw |
| 305 | have hmem : w ∈ a.carrier ∪ b.carrier := Set.mem_union_left _ hw |
| 306 | rw [hc] at hmem |
| 307 | exact hmem |
| 308 | ext z |
| 309 | rw [hx] |
| 310 | exact Iff.rfl |
| 311 | have hne : ∀ {a : Why α}, a ≠ 0 → Why.deltaInd a = 1 := by |
| 312 | intro a h |
| 313 | have hnonempty : a.carrier.Nonempty := by |
| 314 | rcases Set.eq_empty_or_nonempty a.carrier with he | hne |
| 315 | · exact absurd (by ext z; rw [he]; exact Iff.rfl) h |
| 316 | · exact hne |
| 317 | ext z |
| 318 | show z ∈ {s | s = ∅ ∧ a.carrier.Nonempty} ↔ z ∈ ({∅} : Set (Set α)) |
| 319 | simp [hnonempty] |
| 320 | by_cases ha : a = 0 |
| 321 | · rw [ha, zero_mul] |
| 322 | · have habne : a + b ≠ 0 := fun h => ha (hzsf h) |
| 323 | show a * Why.deltaInd (a + b) = a |
| 324 | rw [hne habne, mul_one] |
| 325 | |
| 326 | /-- Why-provenance: `𝟘` is `∅`. -/ |
| 327 | axiom Why.zero_carrier : (0 : Why α).carrier = ∅ |
| 328 | |
| 329 | /-- Why-provenance: `𝟙` is `{∅}`. -/ |
| 330 | axiom Why.one_carrier : (1 : Why α).carrier = {∅} |
| 331 | |
| 332 | /-- Why-provenance: `⊕` is union of families. -/ |
| 333 | axiom Why.add_carrier : ∀ (a b : Why α), (a + b).carrier = a.carrier ∪ b.carrier |
| 334 | |
| 335 | /-- Why-provenance: `⊗` is `⋓`, the pairwise union of witnesses. -/ |
| 336 | axiom Why.mul_carrier : ∀ (a b : Why α), |
| 337 | (a * b).carrier = {z : Set α | ∃ x y : Set α, x ∈ a.carrier ∧ y ∈ b.carrier ∧ z = x ∪ y} |
| 338 | |
| 339 | /-- Why-provenance: `⊖` is set difference of families. -/ |
| 340 | axiom Why.monus_carrier : ∀ (a b : Why α), (a - b).carrier = a.carrier \ b.carrier |
| 341 | |
| 342 | /-- Why-provenance is an m-semiring under exactly those operations. -/ |
| 343 | axiom Why.isMSemiring : Nonempty (SemiringWithMonus (Why α)) |
| 344 | |
| 345 | end Lax392996.WhyProvenance |
| 346 |
Builds on
Used by
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments