189 receipts inline · 1485 lines · pinned 15a8e142dc13d6e1 — shasum -a 256 of this file, cut to 16, as pins has it · lake env lean eih.lean prints nothing when every receipt passes
import Witness import Roster open Room Face Witness Roster set_option autoImplicit false namespace Eih.Treaty structure Request where channel : Nat audience : List Nat sender : Nat confirmed : List Nat /-- info: 'Eih.Treaty.Request' does not depend on any axioms -/ #guard_msgs in #print axioms Request def asked (q : Request) : List Nat := q.audience.filter (fun m => !(Nat.beq m q.sender)) /-- info: 'Eih.Treaty.asked' does not depend on any axioms -/ #guard_msgs in #print axioms asked def tally (q : Request) : Nat := (q.confirmed.filter (enrolled Nat.beq (asked q))).length /-- info: 'Eih.Treaty.tally' does not depend on any axioms -/ #guard_msgs in #print axioms tally def heardBy (q : Request) (m : Nat) : List Nat := cond (enrolled Nat.beq q.audience m) q.confirmed [] /-- info: 'Eih.Treaty.heardBy' does not depend on any axioms -/ #guard_msgs in #print axioms heardBy def confirm (q : Request) (m : Nat) : Request := { q with confirmed := m :: q.confirmed } /-- info: 'Eih.Treaty.confirm' does not depend on any axioms -/ #guard_msgs in #print axioms confirm def settled (q : Request) : Bool := everyone Nat.beq (asked q) q.confirmed /-- info: 'Eih.Treaty.settled' does not depend on any axioms -/ #guard_msgs in #print axioms settled def unanswered (qs : List Request) : List Request := qs.filter (fun q => !(settled q)) /-- info: 'Eih.Treaty.unanswered' does not depend on any axioms -/ #guard_msgs in #print axioms unanswered def inChannel (qs : List Request) (ch : Nat) : List Nat := joinMap (fun q => q.confirmed) (qs.filter (fun q => Nat.beq q.channel ch)) /-- info: 'Eih.Treaty.inChannel' does not depend on any axioms -/ #guard_msgs in #print axioms inChannel structure Room where guests : List Party delivered : List Nat ledger : List (Nat × Nat × Nat) timeline : List Nat bach : List Nat requests : List Request /-- info: 'Eih.Treaty.Room' does not depend on any axioms -/ #guard_msgs in #print axioms Room def deliver (r : Room) : Room := { r with delivered := sheet r.guests } /-- info: 'Eih.Treaty.deliver' does not depend on any axioms -/ #guard_msgs in #print axioms deliver def withGuests (r : Room) (gl : List Party) : Room := { r with guests := gl } /-- info: 'Eih.Treaty.withGuests' does not depend on any axioms -/ #guard_msgs in #print axioms withGuests def withBach (r : Room) (b : List Nat) : Room := { r with bach := b } /-- info: 'Eih.Treaty.withBach' does not depend on any axioms -/ #guard_msgs in #print axioms withBach def confirmIn (r : Room) (ch m : Nat) : Room := { r with requests := r.requests.map (fun q => cond (Nat.beq q.channel ch) (confirm q m) q) } /-- info: 'Eih.Treaty.confirmIn' does not depend on any axioms -/ #guard_msgs in #print axioms confirmIn def ask (r : Room) (ch : Nat) (audience : List Nat) (sender : Nat) : Room := { r with requests := ⟨ch, audience, sender, []⟩ :: r.requests } /-- info: 'Eih.Treaty.ask' does not depend on any axioms -/ #guard_msgs in #print axioms ask def withLine (r : Room) (e : Nat × Nat × Nat) : Room := { r with ledger := e :: r.ledger } /-- info: 'Eih.Treaty.withLine' does not depend on any axioms -/ #guard_msgs in #print axioms withLine def allClear (r : Room) : Prop := r.delivered = sheet r.guests ∧ unanswered r.requests = [] /-- info: 'Eih.Treaty.allClear' does not depend on any axioms -/ #guard_msgs in #print axioms allClear inductive Ask where | guests | sheet | ledger | timeline | bach | confirmed | vendorRoom /-- info: 'Eih.Treaty.Ask' does not depend on any axioms -/ #guard_msgs in #print axioms Ask def Ask.code : Ask → Nat | .guests => 0 | .sheet => 1 | .ledger => 2 | .timeline => 3 | .bach => 4 | .confirmed => 5 | .vendorRoom => 6 /-- info: 'Eih.Treaty.Ask.code' does not depend on any axioms -/ #guard_msgs in #print axioms Ask.code def Ask.beq (a b : Ask) : Bool := Nat.beq a.code b.code /-- info: 'Eih.Treaty.Ask.beq' does not depend on any axioms -/ #guard_msgs in #print axioms Ask.beq def readRoom (r : Room) : Ask → List Nat | .guests => r.guests.map (·.name) | .sheet => r.delivered | .ledger => r.ledger.map (·.2.2) | .timeline => r.timeline | .bach => r.bach | .confirmed => inChannel r.requests 0 | .vendorRoom => inChannel r.requests 1 /-- info: 'Eih.Treaty.readRoom' does not depend on any axioms -/ #guard_msgs in #print axioms readRoom def roomFace : Face := ⟨Room, Ask, List Nat, readRoom⟩ /-- info: 'Eih.Treaty.roomFace' does not depend on any axioms -/ #guard_msgs in #print axioms roomFace def roomSeat : List Ask := [.guests, .sheet, .ledger, .timeline, .bach, .confirmed, .vendorRoom] /-- info: 'Eih.Treaty.roomSeat' does not depend on any axioms -/ #guard_msgs in #print axioms roomSeat def coupleSeat : List Ask := [.guests, .sheet, .ledger, .timeline, .confirmed] /-- info: 'Eih.Treaty.coupleSeat' does not depend on any axioms -/ #guard_msgs in #print axioms coupleSeat def lindaSeat : List Ask := [.guests, .timeline, .confirmed] /-- info: 'Eih.Treaty.lindaSeat' does not depend on any axioms -/ #guard_msgs in #print axioms lindaSeat def bestManSeat : List Ask := [.timeline, .bach, .confirmed] /-- info: 'Eih.Treaty.bestManSeat' does not depend on any axioms -/ #guard_msgs in #print axioms bestManSeat def catererSeat : List Ask := [.timeline, .sheet, .confirmed, .vendorRoom] /-- info: 'Eih.Treaty.catererSeat' does not depend on any axioms -/ #guard_msgs in #print axioms catererSeat def humanSeats : List (List Ask) := [coupleSeat, lindaSeat, bestManSeat, catererSeat] /-- info: 'Eih.Treaty.humanSeats' does not depend on any axioms -/ #guard_msgs in #print axioms humanSeats def coupleSideSeats : List (List Ask) := [coupleSeat, lindaSeat, bestManSeat] /-- info: 'Eih.Treaty.coupleSideSeats' does not depend on any axioms -/ #guard_msgs in #print axioms coupleSideSeats inductive VendorAsk where | timeline | mine /-- info: 'Eih.Treaty.VendorAsk' does not depend on any axioms -/ #guard_msgs in #print axioms VendorAsk def vendorFace (v : Nat) : Face := ⟨Room, VendorAsk, List Nat, fun r q => match q with | .timeline => r.timeline | .mine => (r.ledger.filter (fun e => Nat.beq e.1 v)).map (·.2.2)⟩ /-- info: 'Eih.Treaty.vendorFace' does not depend on any axioms -/ #guard_msgs in #print axioms vendorFace def makerFace : Face := ⟨Room, Unit, Nat, fun r _ => r.guests.length⟩ /-- info: 'Eih.Treaty.makerFace' does not depend on any axioms -/ #guard_msgs in #print axioms makerFace structure Channel where audience : List Nat /-- info: 'Eih.Treaty.Channel' does not depend on any axioms -/ #guard_msgs in #print axioms Channel structure File where channel : Channel /-- info: 'Eih.Treaty.File' does not depend on any axioms -/ #guard_msgs in #print axioms File def visible (f : File) (m : Nat) : Prop := m ∈ f.channel.audience /-- info: 'Eih.Treaty.visible' does not depend on any axioms -/ #guard_msgs in #print axioms visible def canSee (f : File) (m : Nat) : Bool := enrolled Nat.beq f.channel.audience m /-- info: 'Eih.Treaty.canSee' does not depend on any axioms -/ #guard_msgs in #print axioms canSee inductive Role where | couple | planner | vendor | venue | party /-- info: 'Eih.Treaty.Role' does not depend on any axioms -/ #guard_msgs in #print axioms Role def Role.code : Role → Nat | .couple => 0 | .planner => 1 | .vendor => 2 | .venue => 3 | .party => 4 /-- info: 'Eih.Treaty.Role.code' does not depend on any axioms -/ #guard_msgs in #print axioms Role.code def Role.beq (a b : Role) : Bool := Nat.beq a.code b.code /-- info: 'Eih.Treaty.Role.beq' does not depend on any axioms -/ #guard_msgs in #print axioms Role.beq def joinsFree : Role → Bool := fun _ => true /-- info: 'Eih.Treaty.joinsFree' does not depend on any axioms -/ #guard_msgs in #print axioms joinsFree def pays : Role → Bool | .couple => true | .vendor => true | .planner => true | .venue => true | .party => false /-- info: 'Eih.Treaty.pays' does not depend on any axioms -/ #guard_msgs in #print axioms pays def samePage (qs : List Request) (v : Nat) : Nat := ((qs.filter (fun q => enrolled Nat.beq q.audience v)).map tally).sum /-- info: 'Eih.Treaty.samePage' does not depend on any axioms -/ #guard_msgs in #print axioms samePage inductive Thing where | wedding | season /-- info: 'Eih.Treaty.Thing' does not depend on any axioms -/ #guard_msgs in #print axioms Thing def owner : Thing → Role | .wedding => .couple | .season => .vendor /-- info: 'Eih.Treaty.owner' does not depend on any axioms -/ #guard_msgs in #print axioms owner structure Bill where thing : Thing payer : Role /-- info: 'Eih.Treaty.Bill' does not depend on any axioms -/ #guard_msgs in #print axioms Bill def lawful (b : Bill) : Bool := Role.beq b.payer (owner b.thing) || (Role.beq b.payer .vendor && Role.beq (owner b.thing) .couple) /-- info: 'Eih.Treaty.lawful' does not depend on any axioms -/ #guard_msgs in #print axioms lawful inductive Page where | floorPlan | guestList | samePage | invoices | budget | guests | site | team | dayOf | tasks /-- info: 'Eih.Treaty.Page' does not depend on any axioms -/ #guard_msgs in #print axioms Page def Page.code : Page → Nat | .floorPlan => 0 | .guestList => 1 | .samePage => 2 | .invoices => 3 | .budget => 4 | .guests => 5 | .site => 6 | .team => 7 | .dayOf => 8 | .tasks => 9 /-- info: 'Eih.Treaty.Page.code' does not depend on any axioms -/ #guard_msgs in #print axioms Page.code def Page.beq (a b : Page) : Bool := Nat.beq a.code b.code /-- info: 'Eih.Treaty.Page.beq' does not depend on any axioms -/ #guard_msgs in #print axioms Page.beq def roles : List Role := [.couple, .planner, .vendor, .venue, .party] /-- info: 'Eih.Treaty.roles' does not depend on any axioms -/ #guard_msgs in #print axioms roles def pages : List Page := [.floorPlan, .guestList, .samePage, .invoices, .budget, .guests, .site, .team, .dayOf, .tasks] /-- info: 'Eih.Treaty.pages' does not depend on any axioms -/ #guard_msgs in #print axioms pages def seen : Role → List Page | .couple => pages | .planner => [.floorPlan, .guestList, .samePage, .invoices, .team, .dayOf, .tasks] | .vendor => [.floorPlan, .samePage, .invoices, .team, .dayOf, .tasks] | .venue => [.floorPlan, .samePage, .invoices, .team, .dayOf, .tasks] | .party => [.floorPlan, .guestList, .samePage, .team, .dayOf, .tasks] /-- info: 'Eih.Treaty.seen' does not depend on any axioms -/ #guard_msgs in #print axioms seen def edited : Role → List Page | .couple => pages | .planner => [.floorPlan, .guestList, .invoices, .team, .dayOf, .tasks] | .vendor => [.invoices, .dayOf, .tasks] | .venue => [.floorPlan, .invoices, .dayOf, .tasks] | .party => [.floorPlan, .guestList, .dayOf, .tasks] /-- info: 'Eih.Treaty.edited' does not depend on any axioms -/ #guard_msgs in #print axioms edited def sees (ρ : Role) (p : Page) : Bool := enrolled Page.beq (seen ρ) p /-- info: 'Eih.Treaty.sees' does not depend on any axioms -/ #guard_msgs in #print axioms sees def edits (ρ : Role) (p : Page) : Bool := enrolled Page.beq (edited ρ) p /-- info: 'Eih.Treaty.edits' does not depend on any axioms -/ #guard_msgs in #print axioms edits def withinSight : Bool := roles.all (fun ρ => pages.all (fun p => !(edits ρ p) || sees ρ p)) /-- info: 'Eih.Treaty.withinSight' does not depend on any axioms -/ #guard_msgs in #print axioms withinSight structure Member where user : Nat role : Role kind : Nat dayLane : Bool arrival : Nat phone : Nat /-- info: 'Eih.Treaty.Member' does not depend on any axioms -/ #guard_msgs in #print axioms Member def vendorSide (m : Member) : Bool := Role.beq m.role .vendor || (Role.beq m.role .venue || Role.beq m.role .planner) /-- info: 'Eih.Treaty.vendorSide' does not depend on any axioms -/ #guard_msgs in #print axioms vendorSide def vendorRoomMembers (roster : List Member) : List Member := roster.filter vendorSide /-- info: 'Eih.Treaty.vendorRoomMembers' does not depend on any axioms -/ #guard_msgs in #print axioms vendorRoomMembers def vendorRoomAudience (roster : List Member) : List Nat := (vendorRoomMembers roster).map (·.user) /-- info: 'Eih.Treaty.vendorRoomAudience' does not depend on any axioms -/ #guard_msgs in #print axioms vendorRoomAudience def channelAudience (roster : List Member) (p : Member → Bool) : List Nat := (roster.filter p).map (·.user) /-- info: 'Eih.Treaty.channelAudience' does not depend on any axioms -/ #guard_msgs in #print axioms channelAudience def vendorRoomRequestOf (roster : List Member) (sender : Nat) (confirmed : List Nat) : Request := ⟨1, vendorRoomAudience roster, sender, confirmed⟩ /-- info: 'Eih.Treaty.vendorRoomRequestOf' does not depend on any axioms -/ #guard_msgs in #print axioms vendorRoomRequestOf structure Task where owner : Nat assignee : Nat done : Bool /-- info: 'Eih.Treaty.Task' does not depend on any axioms -/ #guard_msgs in #print axioms Task def mayClose (m : Member) (t : Task) : Bool := Nat.beq m.user t.owner || (Role.beq m.role .couple || Role.beq m.role .planner) /-- info: 'Eih.Treaty.mayClose' does not depend on any axioms -/ #guard_msgs in #print axioms mayClose def close (t : Task) : Task := { t with done := true } /-- info: 'Eih.Treaty.close' does not depend on any axioms -/ #guard_msgs in #print axioms close def assign (t : Task) (to : Nat) : Task := { t with assignee := to } /-- info: 'Eih.Treaty.assign' does not depend on any axioms -/ #guard_msgs in #print axioms assign def mayOpen (_ : Member) : Bool := true /-- info: 'Eih.Treaty.mayOpen' does not depend on any axioms -/ #guard_msgs in #print axioms mayOpen def memberSees (m : Member) (p : Page) : Bool := sees m.role p && !(m.dayLane && Page.beq p .tasks) /-- info: 'Eih.Treaty.memberSees' does not depend on any axioms -/ #guard_msgs in #print axioms memberSees def memberEdits (m : Member) (p : Page) : Bool := edits m.role p && memberSees m p /-- info: 'Eih.Treaty.memberEdits' does not depend on any axioms -/ #guard_msgs in #print axioms memberEdits def dayOfIsEveryones : Bool := roles.all (fun ρ => !(sees ρ .dayOf) || edits ρ .dayOf) /-- info: 'Eih.Treaty.dayOfIsEveryones' does not depend on any axioms -/ #guard_msgs in #print axioms dayOfIsEveryones structure DayOfEdit where who : Nat row : Nat before : Nat after : Nat /-- info: 'Eih.Treaty.DayOfEdit' does not depend on any axioms -/ #guard_msgs in #print axioms DayOfEdit def dayOfLog : Machine DayOfEdit (List DayOfEdit) := ledger DayOfEdit /-- info: 'Eih.Treaty.dayOfLog' does not depend on any axioms -/ #guard_msgs in #print axioms dayOfLog def undo : List Nat → List Nat | [] => [] | [_] => [] | x :: y :: w => x :: undo (y :: w) /-- info: 'Eih.Treaty.undo' does not depend on any axioms -/ #guard_msgs in #print axioms undo structure Table where shape : Nat occupants : List Nat /-- info: 'Eih.Treaty.Table' does not depend on any axioms -/ #guard_msgs in #print axioms Table def venueTable (t : Table) : Nat × Nat := (t.shape, t.occupants.length) /-- info: 'Eih.Treaty.venueTable' does not depend on any axioms -/ #guard_msgs in #print axioms venueTable def venueChart (c : List Table) : List (Nat × Nat) := c.map venueTable /-- info: 'Eih.Treaty.venueChart' does not depend on any axioms -/ #guard_msgs in #print axioms venueChart def seasonView (rs : List Room) (v : Nat) : List (List Nat) := rs.map (fun r => (vendorFace v).obs r .mine) /-- info: 'Eih.Treaty.seasonView' does not depend on any axioms -/ #guard_msgs in #print axioms seasonView def seasonOwed (rs : List Room) (v : Nat) : Nat := (joinMap (fun r => (vendorFace v).obs r .mine) rs).sum /-- info: 'Eih.Treaty.seasonOwed' does not depend on any axioms -/ #guard_msgs in #print axioms seasonOwed def rose : Party := ⟨1, true, [2, 3]⟩ /-- info: 'Eih.Treaty.rose' does not depend on any axioms -/ #guard_msgs in #print axioms rose def linda : Party := ⟨2, true, [1]⟩ /-- info: 'Eih.Treaty.linda' does not depend on any axioms -/ #guard_msgs in #print axioms linda def cousin : Party := ⟨3, false, [1, 1]⟩ /-- info: 'Eih.Treaty.cousin' does not depend on any axioms -/ #guard_msgs in #print axioms cousin def guestList : List Party := [linda, cousin, rose] /-- info: 'Eih.Treaty.guestList' does not depend on any axioms -/ #guard_msgs in #print axioms guestList def everyoneChannel : Request := ⟨0, [1, 2, 7, 8, 9], 1, [7, 8]⟩ /-- info: 'Eih.Treaty.everyoneChannel' does not depend on any axioms -/ #guard_msgs in #print axioms everyoneChannel def vendorRoomRequest : Request := ⟨1, [7, 8, 9], 9, [7]⟩ /-- info: 'Eih.Treaty.vendorRoomRequest' does not depend on any axioms -/ #guard_msgs in #print axioms vendorRoomRequest def demo : Room := ⟨guestList, [], [(7, 1, 900), (8, 1, 1200)], [10, 11, 12], [42], [everyoneChannel, vendorRoomRequest]⟩ #guard readRoom demo .confirmed == [7, 8] #guard readRoom demo .vendorRoom == [7] #guard sheet guestList == [1, 2, 3] #guard heads guestList == 3 #guard (deliver demo).delivered == [1, 2, 3] #guard demo.delivered == [] #guard readRoom (deliver demo) .sheet == [1, 2, 3] #guard readRoom demo .guests == [2, 3, 1] /-- info: 'Eih.Treaty.demo' does not depend on any axioms -/ #guard_msgs in #print axioms demo def floristSees : List Nat := (vendorFace 7).obs demo .mine #guard floristSees == [900] /-- info: 'Eih.Treaty.floristSees' does not depend on any axioms -/ #guard_msgs in #print axioms floristSees def djSees : List Nat := (vendorFace 8).obs demo .mine #guard djSees == [1200] /-- info: 'Eih.Treaty.djSees' does not depend on any axioms -/ #guard_msgs in #print axioms djSees def catererSees : List (List Nat) := reads roomFace catererSeat (deliver demo) #guard catererSees == [[10, 11, 12], [1, 2, 3], [7, 8], [7]] /-- info: 'Eih.Treaty.catererSees' does not depend on any axioms -/ #guard_msgs in #print axioms catererSees def lindaSees : List (List Nat) := reads roomFace lindaSeat demo #guard lindaSees == [[2, 3, 1], [10, 11, 12], [7, 8]] /-- info: 'Eih.Treaty.lindaSees' does not depend on any axioms -/ #guard_msgs in #print axioms lindaSees def bestManSees : List (List Nat) := reads roomFace bestManSeat demo #guard bestManSees == [[10, 11, 12], [42], [7, 8]] /-- info: 'Eih.Treaty.bestManSees' does not depend on any axioms -/ #guard_msgs in #print axioms bestManSees def coupleSees : List (List Nat) := reads roomFace coupleSeat demo #guard coupleSees == [[2, 3, 1], [], [900, 1200], [10, 11, 12], [7, 8]] /-- info: 'Eih.Treaty.coupleSees' does not depend on any axioms -/ #guard_msgs in #print axioms coupleSees def roomSees : List (List Nat) := reads roomFace roomSeat demo #guard roomSees.length == 7 /-- info: 'Eih.Treaty.roomSees' does not depend on any axioms -/ #guard_msgs in #print axioms roomSees def makerSees : Nat := makerFace.obs demo () #guard makerSees == 3 #guard joinsFree .party && !(pays .party) /-- info: 'Eih.Treaty.makerSees' does not depend on any axioms -/ #guard_msgs in #print axioms makerSees def moreGuests : Room := withGuests demo (rose :: guestList) /-- info: 'Eih.Treaty.moreGuests' does not depend on any axioms -/ #guard_msgs in #print axioms moreGuests def makerSeesMore : Nat := makerFace.obs moreGuests () #guard makerSeesMore == 4 /-- info: 'Eih.Treaty.makerSeesMore' does not depend on any axioms -/ #guard_msgs in #print axioms makerSeesMore def catererSeesMore : List (List Nat) := reads roomFace catererSeat moreGuests #guard catererSeesMore == reads roomFace catererSeat demo /-- info: 'Eih.Treaty.catererSeesMore' does not depend on any axioms -/ #guard_msgs in #print axioms catererSeesMore def newBach : Room := withBach demo [43] /-- info: 'Eih.Treaty.newBach' does not depend on any axioms -/ #guard_msgs in #print axioms newBach def bestManSeesNew : List (List Nat) := reads roomFace bestManSeat newBach #guard bestManSeesNew == [[10, 11, 12], [43], [7, 8]] /-- info: 'Eih.Treaty.bestManSeesNew' does not depend on any axioms -/ #guard_msgs in #print axioms bestManSeesNew def coupleSeesNew : List (List Nat) := reads roomFace coupleSeat newBach #guard coupleSeesNew == coupleSees /-- info: 'Eih.Treaty.coupleSeesNew' does not depend on any axioms -/ #guard_msgs in #print axioms coupleSeesNew def allConfirmed : Room := confirmIn (confirmIn demo 0 2) 0 9 #guard readRoom allConfirmed .confirmed == [9, 2, 7, 8] /-- info: 'Eih.Treaty.allConfirmed' does not depend on any axioms -/ #guard_msgs in #print axioms allConfirmed def roomSeesConfirmed : List (List Nat) := reads roomFace roomSeat allConfirmed #guard roomSeesConfirmed != roomSees /-- info: 'Eih.Treaty.roomSeesConfirmed' does not depend on any axioms -/ #guard_msgs in #print axioms roomSeesConfirmed def lindaSeesConfirmed : List (List Nat) := reads roomFace lindaSeat allConfirmed #guard lindaSeesConfirmed != lindaSees /-- info: 'Eih.Treaty.lindaSeesConfirmed' does not depend on any axioms -/ #guard_msgs in #print axioms lindaSeesConfirmed def vendorConfirmed : Room := confirmIn demo 1 8 #guard readRoom vendorConfirmed .vendorRoom == [8, 7] /-- info: 'Eih.Treaty.vendorConfirmed' does not depend on any axioms -/ #guard_msgs in #print axioms vendorConfirmed def lindaSeesVendorConfirmed : List (List Nat) := reads roomFace lindaSeat vendorConfirmed #guard lindaSeesVendorConfirmed == lindaSees /-- info: 'Eih.Treaty.lindaSeesVendorConfirmed' does not depend on any axioms -/ #guard_msgs in #print axioms lindaSeesVendorConfirmed def coupleSeesVendorConfirmed : List (List Nat) := reads roomFace coupleSeat vendorConfirmed #guard coupleSeesVendorConfirmed == coupleSees /-- info: 'Eih.Treaty.coupleSeesVendorConfirmed' does not depend on any axioms -/ #guard_msgs in #print axioms coupleSeesVendorConfirmed def catererSeesDemo : List (List Nat) := reads roomFace catererSeat demo /-- info: 'Eih.Treaty.catererSeesDemo' does not depend on any axioms -/ #guard_msgs in #print axioms catererSeesDemo def catererSeesVendorConfirmed : List (List Nat) := reads roomFace catererSeat vendorConfirmed #guard catererSeesVendorConfirmed != catererSeesDemo #guard settled everyoneChannel == false #guard settled (confirm (confirm everyoneChannel 2) 9) #guard (unanswered demo.requests).length == 2 #guard (unanswered allConfirmed.requests).length == 1 #guard (unanswered (confirmIn allConfirmed 1 8).requests).length == 0 /-- info: 'Eih.Treaty.catererSeesVendorConfirmed' does not depend on any axioms -/ #guard_msgs in #print axioms catererSeesVendorConfirmed def withInvoice : Room := withLine demo (9, 1, 300) /-- info: 'Eih.Treaty.withInvoice' does not depend on any axioms -/ #guard_msgs in #print axioms withInvoice def lindaSeesInvoice : List (List Nat) := reads roomFace lindaSeat withInvoice #guard lindaSeesInvoice == lindaSees /-- info: 'Eih.Treaty.lindaSeesInvoice' does not depend on any axioms -/ #guard_msgs in #print axioms lindaSeesInvoice def humanEars : List Ask := earshot roomFace humanSeats #guard humanEars.length == 15 #guard enrolled Ask.beq humanEars .confirmed == true #guard enrolled Ask.beq humanEars .ledger == true #guard enrolled Ask.beq humanEars .vendorRoom == true /-- info: 'Eih.Treaty.humanEars' does not depend on any axioms -/ #guard_msgs in #print axioms humanEars def coupleSideEars : List Ask := earshot roomFace coupleSideSeats #guard enrolled Ask.beq coupleSideEars .vendorRoom == false #guard everyone Nat.beq (asked everyoneChannel) (confirm (confirm everyoneChannel 2) 9).confirmed #guard !(everyone Nat.beq (asked everyoneChannel) everyoneChannel.confirmed) /-- info: 'Eih.Treaty.coupleSideEars' does not depend on any axioms -/ #guard_msgs in #print axioms coupleSideEars def maya : Nat := 1 /-- info: 'Eih.Treaty.maya' does not depend on any axioms -/ #guard_msgs in #print axioms maya def jordan : Nat := 7 #guard asked everyoneChannel == [2, 7, 8, 9] #guard tally everyoneChannel == 2 #guard heardBy everyoneChannel jordan == [7, 8] #guard heardBy everyoneChannel maya == [7, 8] #guard heardBy vendorRoomRequest maya == [] #guard heardBy vendorRoomRequest jordan == [7] #guard tally (confirm everyoneChannel 2) == 3 #guard samePage [everyoneChannel, vendorRoomRequest] maya == 2 #guard samePage [everyoneChannel, vendorRoomRequest] jordan == 3 /-- info: 'Eih.Treaty.jordan' does not depend on any axioms -/ #guard_msgs in #print axioms jordan def coveredWedding : Bill := ⟨.wedding, .vendor⟩ /-- info: 'Eih.Treaty.coveredWedding' does not depend on any axioms -/ #guard_msgs in #print axioms coveredWedding def ownWedding : Bill := ⟨.wedding, .couple⟩ /-- info: 'Eih.Treaty.ownWedding' does not depend on any axioms -/ #guard_msgs in #print axioms ownWedding def strayBill : Bill := ⟨.season, .couple⟩ #guard lawful coveredWedding && lawful ownWedding && !(lawful strayBill) #guard Role.beq (owner coveredWedding.thing) .couple #guard withinSight #guard sees .venue .floorPlan && edits .venue .floorPlan && !(sees .venue .guestList) #guard sees .vendor .floorPlan && !(edits .vendor .floorPlan) #guard pays .venue && joinsFree .venue && !(pays .party) /-- info: 'Eih.Treaty.strayBill' does not depend on any axioms -/ #guard_msgs in #print axioms strayBill def vendorRoomChannel : Channel := ⟨[7, 8, 9]⟩ /-- info: 'Eih.Treaty.vendorRoomChannel' does not depend on any axioms -/ #guard_msgs in #print axioms vendorRoomChannel def vendorRoomFile : File := ⟨vendorRoomChannel⟩ #guard !(canSee vendorRoomFile maya) #guard canSee vendorRoomFile jordan /-- info: 'Eih.Treaty.vendorRoomFile' does not depend on any axioms -/ #guard_msgs in #print axioms vendorRoomFile def mayaM : Member := ⟨1, .couple, 0, false, 15, 0⟩ /-- info: 'Eih.Treaty.mayaM' does not depend on any axioms -/ #guard_msgs in #print axioms mayaM def lindaM : Member := ⟨2, .party, 0, true, 14, 0⟩ /-- info: 'Eih.Treaty.lindaM' does not depend on any axioms -/ #guard_msgs in #print axioms lindaM def jordanM : Member := ⟨7, .vendor, 1, false, 12, 0⟩ /-- info: 'Eih.Treaty.jordanM' does not depend on any axioms -/ #guard_msgs in #print axioms jordanM def djM : Member := ⟨8, .vendor, 2, false, 13, 0⟩ /-- info: 'Eih.Treaty.djM' does not depend on any axioms -/ #guard_msgs in #print axioms djM def sofiaM : Member := ⟨9, .vendor, 3, false, 11, 0⟩ /-- info: 'Eih.Treaty.sofiaM' does not depend on any axioms -/ #guard_msgs in #print axioms sofiaM def roster : List Member := [mayaM, lindaM, jordanM, djM, sofiaM] #guard vendorRoomAudience roster == [7, 8, 9] #guard !(enrolled Nat.beq (vendorRoomAudience roster) 1) #guard !(enrolled Nat.beq (vendorRoomAudience roster) 2) #guard (vendorRoomRequestOf roster 9 [7]).audience == vendorRoomRequest.audience #guard vendorRoomAudience [mayaM, lindaM, jordanM] == [7] /-- info: 'Eih.Treaty.roster' does not depend on any axioms -/ #guard_msgs in #print axioms roster def loadIn : Task := ⟨7, 7, false⟩ #guard mayClose jordanM loadIn && mayClose mayaM loadIn && !(mayClose sofiaM loadIn) #guard (close loadIn).done #guard (assign loadIn 9).assignee == 9 #guard mayOpen sofiaM && mayOpen lindaM #guard !(memberSees lindaM .tasks) && memberSees lindaM .dayOf && memberEdits lindaM .dayOf #guard memberSees jordanM .tasks && memberEdits jordanM .tasks #guard !(memberEdits lindaM .tasks) #guard pages.all (fun p => !(memberSees lindaM p) || sees .party p) #guard dayOfIsEveryones #guard undo [1, 2, 3] == [1, 2] #guard undo [1] == [] /-- info: 'Eih.Treaty.loadIn' does not depend on any axioms -/ #guard_msgs in #print axioms loadIn def firstEdit : DayOfEdit := ⟨9, 3, 100, 130⟩ /-- info: 'Eih.Treaty.firstEdit' does not depend on any axioms -/ #guard_msgs in #print axioms firstEdit def secondEdit : DayOfEdit := ⟨7, 5, 600, 615⟩ #guard (behavior dayOfLog [firstEdit, secondEdit]).length == 2 #guard (behavior dayOfLog [firstEdit, secondEdit]).map (·.who) == [9, 7] /-- info: 'Eih.Treaty.secondEdit' does not depend on any axioms -/ #guard_msgs in #print axioms secondEdit def headTable : Table := ⟨0, [1, 2, 3]⟩ /-- info: 'Eih.Treaty.headTable' does not depend on any axioms -/ #guard_msgs in #print axioms headTable def table2 : Table := ⟨1, [4]⟩ #guard venueChart [headTable, table2] == [(0, 3), (1, 1)] #guard venueChart [⟨0, [4, 5, 6]⟩, table2] == venueChart [headTable, table2] #guard seasonView [demo, withInvoice] 7 == [[900], [900]] #guard seasonView [demo, withInvoice] 9 == [[], [300]] #guard seasonOwed [demo, withInvoice] 7 == 1800 #guard seasonOwed [demo, withInvoice] 9 == 300 /-- info: 'Eih.Treaty.table2' does not depend on any axioms -/ #guard_msgs in #print axioms table2 theorem the_delivery_is_the_sheet (r : Room) : (deliver r).delivered = sheet r.guests := by (intros; (repeat' constructor); all_goals (intros; fail)) /-- info: 'Eih.Treaty.the_delivery_is_the_sheet' does not depend on any axioms -/ #guard_msgs in #print axioms the_delivery_is_the_sheet theorem the_delivery_moves_no_guest (r : Room) : (deliver r).guests = r.guests := by (intros; (repeat' constructor); all_goals (intros; fail)) /-- info: 'Eih.Treaty.the_delivery_moves_no_guest' does not depend on any axioms -/ #guard_msgs in #print axioms the_delivery_moves_no_guest theorem everyone_clear_means_every_request_settled (r : Room) (h : allClear r) : ∀ q, q ∈ r.requests → settled q = true := fun q hq => by cases hs : settled q with | true => rfl | false => have hm : q ∈ unanswered r.requests := mem_filter_intro r.requests hq (by show (!(settled q)) = true; rw [hs]; rfl) rw [h.2] at hm exact nomatch hm /-- info: 'Eih.Treaty.everyone_clear_means_every_request_settled' does not depend on any axioms -/ #guard_msgs in #print axioms everyone_clear_means_every_request_settled theorem a_line_touches_only_the_ledger (r : Room) (e : Nat × Nat × Nat) : differOnly roomFace (withLine r e) r .ledger := fun q hq => by cases q <;> first | rfl | exact absurd rfl hq /-- info: 'Eih.Treaty.a_line_touches_only_the_ledger' does not depend on any axioms -/ #guard_msgs in #print axioms a_line_touches_only_the_ledger theorem the_bach_touches_only_the_bach (r : Room) (b : List Nat) : differOnly roomFace (withBach r b) r .bach := fun q hq => by cases q <;> first | rfl | exact absurd rfl hq /-- info: 'Eih.Treaty.the_bach_touches_only_the_bach' does not depend on any axioms -/ #guard_msgs in #print axioms the_bach_touches_only_the_bach theorem a_confirmation_elsewhere_leaves_a_channel (ch ch' m : Nat) (h : Nat.beq ch ch' = false) : ∀ qs : List Request, (qs.map (fun q => cond (Nat.beq q.channel ch) (confirm q m) q)).filter (fun q => Nat.beq q.channel ch') = qs.filter (fun q => Nat.beq q.channel ch') | [] => rfl | q :: qs => by show (cond (Nat.beq q.channel ch) (confirm q m) q :: qs.map (fun q => cond (Nat.beq q.channel ch) (confirm q m) q)).filter (fun q => Nat.beq q.channel ch') = (q :: qs).filter (fun q => Nat.beq q.channel ch') cases hc : Nat.beq q.channel ch with | true => have hq : q.channel = ch := eq_of_beq _ _ hc have hn : Nat.beq q.channel ch' = false := by rw [hq]; exact h show (confirm q m :: qs.map (fun q => cond (Nat.beq q.channel ch) (confirm q m) q)).filter (fun q => Nat.beq q.channel ch') = (q :: qs).filter (fun q => Nat.beq q.channel ch') rw [List.filter_cons_of_neg (p := fun q => Nat.beq q.channel ch') (a := confirm q m) (ne_true_of_eq_false hn), List.filter_cons_of_neg (p := fun q => Nat.beq q.channel ch') (a := q) (ne_true_of_eq_false hn)] exact a_confirmation_elsewhere_leaves_a_channel ch ch' m h qs | false => show (q :: qs.map (fun q => cond (Nat.beq q.channel ch) (confirm q m) q)).filter (fun q => Nat.beq q.channel ch') = (q :: qs).filter (fun q => Nat.beq q.channel ch') cases hc' : Nat.beq q.channel ch' with | true => rw [List.filter_cons_of_pos (p := fun q => Nat.beq q.channel ch') (a := q) hc', List.filter_cons_of_pos (p := fun q => Nat.beq q.channel ch') (a := q) hc', a_confirmation_elsewhere_leaves_a_channel ch ch' m h qs] | false => rw [List.filter_cons_of_neg (p := fun q => Nat.beq q.channel ch') (a := q) (ne_true_of_eq_false hc'), List.filter_cons_of_neg (p := fun q => Nat.beq q.channel ch') (a := q) (ne_true_of_eq_false hc'), a_confirmation_elsewhere_leaves_a_channel ch ch' m h qs] /-- info: 'Eih.Treaty.a_confirmation_elsewhere_leaves_a_channel' does not depend on any axioms -/ #guard_msgs in #print axioms a_confirmation_elsewhere_leaves_a_channel theorem the_guests_touch_only_the_guests (r : Room) (gl : List Party) : differOnly roomFace (withGuests r gl) r .guests := fun q hq => by cases q <;> first | exact absurd rfl hq | rfl /-- info: 'Eih.Treaty.the_guests_touch_only_the_guests' does not depend on any axioms -/ #guard_msgs in #print axioms the_guests_touch_only_the_guests theorem a_vendor_never_sees_anothers_invoice (v w : Nat) (hvw : Nat.beq w v = false) (r : Room) (amount to : Nat) : alike (vendorFace v) (withLine r (w, to, amount)) r := by intro q cases q with | timeline => rfl | mine => show ((( w, to, amount) :: r.ledger).filter (fun e => Nat.beq e.1 v)).map (·.2.2) = (r.ledger.filter (fun e => Nat.beq e.1 v)).map (·.2.2) rw [List.filter, hvw] /-- info: 'Eih.Treaty.a_vendor_never_sees_anothers_invoice' does not depend on any axioms -/ #guard_msgs in #print axioms a_vendor_never_sees_anothers_invoice theorem an_ask_reads_itself : ∀ q : Ask, Ask.beq q q = true := by (intro x; induction x; all_goals ((intros; rfl))) /-- info: 'Eih.Treaty.an_ask_reads_itself' does not depend on any axioms -/ #guard_msgs in #print axioms an_ask_reads_itself theorem a_vendor_sees_only_their_own (v : Nat) (r : Room) : (vendorFace v).obs r .mine = (r.ledger.filter (fun e => Nat.beq e.1 v)).map (·.2.2) := rfl /-- info: 'Eih.Treaty.a_vendor_sees_only_their_own' does not depend on any axioms -/ #guard_msgs in #print axioms a_vendor_sees_only_their_own theorem linda_never_sees_the_ledger (r : Room) (e : Nat × Nat × Nat) : reads roomFace lindaSeat (withLine r e) = reads roomFace lindaSeat r := (by (apply Witness.a_narrower_seat_reads_no_more <;> (intros; apply Witness.the_probe_reads_the_seat <;> first | assumption | rfl))) /-- info: 'Eih.Treaty.linda_never_sees_the_ledger' does not depend on any axioms -/ #guard_msgs in #print axioms linda_never_sees_the_ledger theorem the_caterer_never_sees_the_ledger (r : Room) (e : Nat × Nat × Nat) : reads roomFace catererSeat (withLine r e) = reads roomFace catererSeat r := (by (apply Witness.a_narrower_seat_reads_no_more <;> (intros; apply Witness.the_probe_reads_the_seat <;> first | assumption | rfl))) /-- info: 'Eih.Treaty.the_caterer_never_sees_the_ledger' does not depend on any axioms -/ #guard_msgs in #print axioms the_caterer_never_sees_the_ledger theorem the_caterer_never_sees_the_guests (r : Room) (gl : List Party) : reads roomFace catererSeat (withGuests r gl) = reads roomFace catererSeat r := (by (apply Witness.a_narrower_seat_reads_no_more <;> (intros; apply Witness.the_probe_reads_the_seat <;> first | assumption | rfl))) /-- info: 'Eih.Treaty.the_caterer_never_sees_the_guests' does not depend on any axioms -/ #guard_msgs in #print axioms the_caterer_never_sees_the_guests theorem the_bach_parts_the_best_man (r : Room) (b : List Nat) (hb : b ≠ r.bach) : reads roomFace bestManSeat (withBach r b) ≠ reads roomFace bestManSeat r := (by (apply Witness.the_seat_that_hears_it_reads_it (p := Ask.bach) <;> first | assumption | (apply List.Mem.tail; exact List.Mem.head _))) /-- info: 'Eih.Treaty.the_bach_parts_the_best_man' does not depend on any axioms -/ #guard_msgs in #print axioms the_bach_parts_the_best_man theorem a_confirmation_parts_the_audience (r : Room) (m : Nat) (h : readRoom (confirmIn r 0 m) .confirmed ≠ readRoom r .confirmed) : reads roomFace coupleSeat (confirmIn r 0 m) ≠ reads roomFace coupleSeat r := (by (apply Witness.the_seat_that_hears_it_reads_it (p := Ask.confirmed) <;> first | assumption | (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; exact List.Mem.head _)))))) /-- info: 'Eih.Treaty.a_confirmation_parts_the_audience' does not depend on any axioms -/ #guard_msgs in #print axioms a_confirmation_parts_the_audience theorem the_room_covers_itself : covers roomFace [roomSeat] := by (intro x; induction x; all_goals (first | (intros; (apply Witness.a_room_covers_itself_at_one_seat <;> exact List.Mem.head _)) | (intros; (apply Witness.a_room_covers_itself_at_one_seat <;> (apply List.Mem.tail; exact List.Mem.head _))) | (intros; (apply Witness.a_room_covers_itself_at_one_seat <;> (apply List.Mem.tail; (apply List.Mem.tail; exact List.Mem.head _)))) | (intros; (apply Witness.a_room_covers_itself_at_one_seat <;> (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; exact List.Mem.head _))))) | (intros; (apply Witness.a_room_covers_itself_at_one_seat <;> (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; exact List.Mem.head _)))))) | (intros; (apply Witness.a_room_covers_itself_at_one_seat <;> (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; exact List.Mem.head _))))))) | (intros; (apply Witness.a_room_covers_itself_at_one_seat <;> (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; exact List.Mem.head _)))))))))) /-- info: 'Eih.Treaty.the_room_covers_itself' does not depend on any axioms -/ #guard_msgs in #print axioms the_room_covers_itself theorem the_room_witnesses_the_license (x y : Room) (hw : witnessed roomFace [roomSeat] x y) : alike roomFace x y := by (intro x; induction x; all_goals (first | (intros; (apply Witness.speak_now <;> first | assumption | exact List.Mem.head _)) | (intros; (apply Witness.speak_now <;> first | assumption | (apply List.Mem.tail; exact List.Mem.head _))) | (intros; (apply Witness.speak_now <;> first | assumption | (apply List.Mem.tail; (apply List.Mem.tail; exact List.Mem.head _)))) | (intros; (apply Witness.speak_now <;> first | assumption | (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; exact List.Mem.head _))))) | (intros; (apply Witness.speak_now <;> first | assumption | (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; exact List.Mem.head _)))))) | (intros; (apply Witness.speak_now <;> first | assumption | (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; exact List.Mem.head _))))))) | (intros; (apply Witness.speak_now <;> first | assumption | (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; exact List.Mem.head _)))))))))) /-- info: 'Eih.Treaty.the_room_witnesses_the_license' does not depend on any axioms -/ #guard_msgs in #print axioms the_room_witnesses_the_license theorem the_caterer_reads_the_delivery (r : Room) : readRoom (deliver r) .sheet = sheet r.guests := by (intros; (repeat' constructor); all_goals (intros; fail)) /-- info: 'Eih.Treaty.the_caterer_reads_the_delivery' does not depend on any axioms -/ #guard_msgs in #print axioms the_caterer_reads_the_delivery theorem a_file_is_never_wider_than_its_channel (f : File) (m : Nat) : visible f m ↔ m ∈ f.channel.audience := by (intros; (repeat' constructor); all_goals (intros; (apply Room.perm_mem <;> first | rfl | assumption))) /-- info: 'Eih.Treaty.a_file_is_never_wider_than_its_channel' does not depend on any axioms -/ #guard_msgs in #print axioms a_file_is_never_wider_than_its_channel theorem a_vendor_room_file_is_absent_from_the_couples_files (f : File) (couple : Nat) (h : canSee f couple = false) : ¬ visible f couple := the_unenrolled_are_no_member Nat.beq beq_self f.channel.audience couple h /-- info: 'Eih.Treaty.a_vendor_room_file_is_absent_from_the_couples_files' does not depend on any axioms -/ #guard_msgs in #print axioms a_vendor_room_file_is_absent_from_the_couples_files by (intro x; induction x; all_goals ((intros; rfl))) /-- info: 'Eih.Treaty.join_and_pay_are_unrelated' does not depend on any axioms -/ #guard_msgs in #print axioms join_and_pay_are_unrelated theorem the_party_never_pays : pays .party = false := by (intros; (repeat' constructor); all_goals (intros; fail)) /-- info: 'Eih.Treaty.the_party_never_pays' does not depend on any axioms -/ #guard_msgs in #print axioms the_party_never_pays theorem lanes_shrink_never_lock (m : Member) (p : Page) (h : memberSees m p = true) : sees m.role p = true := (and_reads _ _ h).1 /-- info: 'Eih.Treaty.lanes_shrink_never_lock' does not depend on any axioms -/ #guard_msgs in #print axioms lanes_shrink_never_lock theorem the_day_lane_sees_no_task_list (m : Member) (h : m.dayLane = true) : memberSees m .tasks = false := by show (sees m.role .tasks && !(m.dayLane && Page.beq .tasks .tasks)) = false rw [h] cases sees m.role .tasks <;> rfl /-- info: 'Eih.Treaty.the_day_lane_sees_no_task_list' does not depend on any axioms -/ #guard_msgs in #print axioms the_day_lane_sees_no_task_list theorem the_day_lane_keeps_the_day_of_sheet (m : Member) (h : m.role = .party) : memberSees m .dayOf = true := by show (sees m.role .dayOf && !(m.dayLane && Page.beq .dayOf .tasks)) = true rw [h] cases m.dayLane <;> rfl /-- info: 'Eih.Treaty.the_day_lane_keeps_the_day_of_sheet' does not depend on any axioms -/ #guard_msgs in #print axioms the_day_lane_keeps_the_day_of_sheet theorem an_edit_is_within_the_lane (m : Member) (p : Page) (h : memberEdits m p = true) : memberSees m p = true := (and_reads _ _ h).2 /-- info: 'Eih.Treaty.an_edit_is_within_the_lane' does not depend on any axioms -/ #guard_msgs in #print axioms an_edit_is_within_the_lane theorem the_maker_sees_shape_not_content (r : Room) (gl gl' : List Party) (h : gl.length = gl'.length) : alike makerFace (withGuests r gl) (withGuests r gl') := by (intro x; induction x; all_goals ((intros; (apply h <;> fail)))) /-- info: 'Eih.Treaty.the_maker_sees_shape_not_content' does not depend on any axioms -/ #guard_msgs in #print axioms the_maker_sees_shape_not_content theorem everyone_clear_means_rose_ate (r : Room) (h : allClear r) {p : Party} (hp : p ∈ r.guests) (hr : p.rsvp = true) {m : Nat} (hm : m ∈ p.meals) : m ∈ r.delivered := by rw [h.1] exact a_yes_reaches_the_sheet hp hr hm /-- info: 'Eih.Treaty.everyone_clear_means_rose_ate' does not depend on any axioms -/ #guard_msgs in #print axioms everyone_clear_means_rose_ate theorem the_audience_hears_the_receipt_by_name (q : Request) (m : Nat) (h : enrolled Nat.beq q.audience m = true) : heardBy q m = q.confirmed := by show cond (enrolled Nat.beq q.audience m) q.confirmed [] = q.confirmed rw [h] exact rfl /-- info: 'Eih.Treaty.the_audience_hears_the_receipt_by_name' does not depend on any axioms -/ #guard_msgs in #print axioms the_audience_hears_the_receipt_by_name theorem outside_the_audience_hears_no_receipt (q : Request) (m x : Nat) (h : enrolled Nat.beq q.audience m = false) : heardBy (confirm q x) m = heardBy q m := by show cond (enrolled Nat.beq q.audience m) (x :: q.confirmed) [] = cond (enrolled Nat.beq q.audience m) q.confirmed [] rw [h] exact rfl /-- info: 'Eih.Treaty.outside_the_audience_hears_no_receipt' does not depend on any axioms -/ #guard_msgs in #print axioms outside_the_audience_hears_no_receipt theorem the_sender_is_never_asked (q : Request) : ¬ q.sender ∈ asked q := by intro h have hq := filter_holds q.audience h have hs : (!(Nat.beq q.sender q.sender)) = true := hq rw [beq_self] at hs exact nomatch hs /-- info: 'Eih.Treaty.the_sender_is_never_asked' does not depend on any axioms -/ #guard_msgs in #print axioms the_sender_is_never_asked theorem the_same_page_counts_only_within_earshot (q : Request) (qs : List Request) (v : Nat) (h : enrolled Nat.beq q.audience v = false) : samePage (q :: qs) v = samePage qs v := by show (((q :: qs).filter (fun q => enrolled Nat.beq q.audience v)).map tally).sum = ((qs.filter (fun q => enrolled Nat.beq q.audience v)).map tally).sum rw [List.filter_cons_of_neg (p := fun q => enrolled Nat.beq q.audience v) (a := q) (ne_true_of_eq_false h)] /-- info: 'Eih.Treaty.the_same_page_counts_only_within_earshot' does not depend on any axioms -/ #guard_msgs in #print axioms the_same_page_counts_only_within_earshot theorem the_same_page_hears_its_own_earshot (q : Request) (qs : List Request) (v : Nat) (h : enrolled Nat.beq q.audience v = true) : samePage (q :: qs) v = tally q + samePage qs v := by show (((q :: qs).filter (fun q => enrolled Nat.beq q.audience v)).map tally).sum = tally q + ((qs.filter (fun q => enrolled Nat.beq q.audience v)).map tally).sum rw [List.filter_cons_of_pos (p := fun q => enrolled Nat.beq q.audience v) (a := q) h] exact rfl /-- info: 'Eih.Treaty.the_same_page_hears_its_own_earshot' does not depend on any axioms -/ #guard_msgs in #print axioms the_same_page_hears_its_own_earshot theorem a_covered_wedding_is_still_the_couples (b : Bill) (h : b.thing = .wedding) : owner b.thing = .couple := by rw [h] rfl /-- info: 'Eih.Treaty.a_covered_wedding_is_still_the_couples' does not depend on any axioms -/ #guard_msgs in #print axioms a_covered_wedding_is_still_the_couples theorem the_payer_is_the_owner_or_the_host (b : Bill) (h : lawful b = true) : Role.beq b.payer (owner b.thing) = true ∨ (Role.beq b.payer .vendor = true ∧ Role.beq (owner b.thing) .couple = true) := by cases hp : Role.beq b.payer (owner b.thing) with | true => exact Or.inl rfl | false => have h' : (Role.beq b.payer (owner b.thing) || (Role.beq b.payer .vendor && Role.beq (owner b.thing) .couple)) = true := h rw [hp] at h' exact Or.inr (and_reads _ _ h') /-- info: 'Eih.Treaty.the_payer_is_the_owner_or_the_host' does not depend on any axioms -/ #guard_msgs in #print axioms the_payer_is_the_owner_or_the_host theorem edit_is_within_sight : withinSight = true := (by (apply ((Room.not_not _)).symm <;> fail)) /-- info: 'Eih.Treaty.edit_is_within_sight' does not depend on any axioms -/ #guard_msgs in #print axioms edit_is_within_sight theorem the_venue_edits_the_floor_and_never_sees_the_list : edits .venue .floorPlan = true ∧ sees .venue .guestList = false := ⟨rfl, rfl⟩ /-- info: 'Eih.Treaty.the_venue_edits_the_floor_and_never_sees_the_list' does not depend on any axioms -/ #guard_msgs in #print axioms the_venue_edits_the_floor_and_never_sees_the_list theorem a_vendor_sees_the_floor_and_edits_nothing_there : sees .vendor .floorPlan = true ∧ edits .vendor .floorPlan = false := by (intros; (repeat' constructor); all_goals (intros; fail)) /-- info: 'Eih.Treaty.a_vendor_sees_the_floor_and_edits_nothing_there' does not depend on any axioms -/ #guard_msgs in #print axioms a_vendor_sees_the_floor_and_edits_nothing_there theorem the_couple_is_never_in_the_vendor_room (roster : List Member) (m : Member) (hc : m.role = .couple) : ¬ m ∈ vendorRoomMembers roster := fun h => by have hp : vendorSide m = true := filter_holds roster h have hf : vendorSide m = false := by cases m with | mk u r k l a p => cases r with | couple => rfl | planner => exact nomatch hc | vendor => exact nomatch hc | venue => exact nomatch hc | party => exact nomatch hc exact nomatch (hf.symm.trans hp) /-- info: 'Eih.Treaty.the_couple_is_never_in_the_vendor_room' does not depend on any axioms -/ #guard_msgs in #print axioms the_couple_is_never_in_the_vendor_room theorem the_wedding_party_is_never_in_the_vendor_room (roster : List Member) (m : Member) (hc : m.role = .party) : ¬ m ∈ vendorRoomMembers roster := fun h => by have hp : vendorSide m = true := filter_holds roster h have hf : vendorSide m = false := by cases m with | mk u r k l a p => cases r with | couple => exact nomatch hc | planner => exact nomatch hc | vendor => exact nomatch hc | venue => exact nomatch hc | party => rfl exact nomatch (hf.symm.trans hp) /-- info: 'Eih.Treaty.the_wedding_party_is_never_in_the_vendor_room' does not depend on any axioms -/ #guard_msgs in #print axioms the_wedding_party_is_never_in_the_vendor_room theorem a_vendor_is_in_the_vendor_room (roster : List Member) (m : Member) (hm : m ∈ roster) (hv : m.role = .vendor) : m ∈ vendorRoomMembers roster := mem_filter_intro roster hm (by cases m with | mk u r k l a p => cases r with | couple => exact nomatch hv | planner => exact nomatch hv | vendor => rfl | venue => exact nomatch hv | party => exact nomatch hv) /-- info: 'Eih.Treaty.a_vendor_is_in_the_vendor_room' does not depend on any axioms -/ #guard_msgs in #print axioms a_vendor_is_in_the_vendor_room theorem the_vendor_room_is_derived_from_the_roster (roster : List Member) : vendorRoomAudience roster = channelAudience roster vendorSide := by (intros; (repeat' constructor); all_goals (intros; fail)) /-- info: 'Eih.Treaty.the_vendor_room_is_derived_from_the_roster' does not depend on any axioms -/ #guard_msgs in #print axioms the_vendor_room_is_derived_from_the_roster theorem an_audience_is_members (roster : List Member) (p : Member → Bool) (u : Nat) (h : u ∈ channelAudience roster p) : ∃ m, m ∈ roster ∧ m.user = u := by obtain ⟨m, hm, he⟩ := mem_map_back (roster.filter p) h exact ⟨m, mem_of_mem_filter roster hm, he⟩ /-- info: 'Eih.Treaty.an_audience_is_members' does not depend on any axioms -/ #guard_msgs in #print axioms an_audience_is_members theorem the_owner_may_close (m : Member) (t : Task) (h : Nat.beq m.user t.owner = true) : mayClose m t = true := by show (Nat.beq m.user t.owner || (Role.beq m.role .couple || Role.beq m.role .planner)) = true rw [h] exact rfl /-- info: 'Eih.Treaty.the_owner_may_close' does not depend on any axioms -/ #guard_msgs in #print axioms the_owner_may_close theorem the_couple_may_close (m : Member) (t : Task) (h : m.role = .couple) : mayClose m t = true := by show (Nat.beq m.user t.owner || (Role.beq m.role .couple || Role.beq m.role .planner)) = true rw [h] cases Nat.beq m.user t.owner <;> rfl /-- info: 'Eih.Treaty.the_couple_may_close' does not depend on any axioms -/ #guard_msgs in #print axioms the_couple_may_close theorem a_vendor_may_not_close_anothers (m : Member) (t : Task) (h1 : Nat.beq m.user t.owner = false) (h2 : m.role = .vendor) : mayClose m t = false := by show (Nat.beq m.user t.owner || (Role.beq m.role .couple || Role.beq m.role .planner)) = false rw [h1, h2] exact rfl /-- info: 'Eih.Treaty.a_vendor_may_not_close_anothers' does not depend on any axioms -/ #guard_msgs in #print axioms a_vendor_may_not_close_anothers theorem anyone_may_open_a_task (m : Member) : mayOpen m = true := by (intros; (repeat' constructor); all_goals (intros; fail)) /-- info: 'Eih.Treaty.anyone_may_open_a_task' does not depend on any axioms -/ #guard_msgs in #print axioms anyone_may_open_a_task theorem the_day_of_sheet_is_everyones_to_edit : dayOfIsEveryones = true := (by (apply ((Room.not_not _)).symm <;> fail)) /-- info: 'Eih.Treaty.the_day_of_sheet_is_everyones_to_edit' does not depend on any axioms -/ #guard_msgs in #print axioms the_day_of_sheet_is_everyones_to_edit theorem every_edit_is_kept (w : List DayOfEdit) : behavior dayOfLog w = w := the_ledger_parks_the_word w [] /-- info: 'Eih.Treaty.every_edit_is_kept' does not depend on any axioms -/ #guard_msgs in #print axioms every_edit_is_kept theorem the_last_edit_undoes (e : Nat) : ∀ w : List Nat, undo (w ++ [e]) = w | [] => rfl | [_] => rfl | x :: y :: w => congrArg (x :: ·) (the_last_edit_undoes e (y :: w)) /-- info: 'Eih.Treaty.the_last_edit_undoes' does not depend on any axioms -/ #guard_msgs in #print axioms the_last_edit_undoes theorem the_venue_reads_counts_not_names (t : Table) (occ occ' : List Nat) (h : occ.length = occ'.length) : venueTable { t with occupants := occ } = venueTable { t with occupants := occ' } := by show (t.shape, occ.length) = (t.shape, occ'.length) rw [h] /-- info: 'Eih.Treaty.the_venue_reads_counts_not_names' does not depend on any axioms -/ #guard_msgs in #print axioms the_venue_reads_counts_not_names theorem a_season_reads_each_room_as_the_vendor (rs : List Room) (v : Nat) : seasonView rs v = rs.map (fun r => (vendorFace v).obs r .mine) := by (intros; (repeat' constructor); all_goals (intros; fail)) /-- info: 'Eih.Treaty.a_season_reads_each_room_as_the_vendor' does not depend on any axioms -/ #guard_msgs in #print axioms a_season_reads_each_room_as_the_vendor theorem the_seasons_sum_is_over_my_own_invoices (rs : List Room) (v : Nat) : seasonOwed rs v = (joinMap (fun r => (vendorFace v).obs r .mine) rs).sum := by (intros; (repeat' constructor); all_goals (intros; fail)) /-- info: 'Eih.Treaty.the_seasons_sum_is_over_my_own_invoices' does not depend on any axioms -/ #guard_msgs in #print axioms the_seasons_sum_is_over_my_own_invoices theorem a_confirmation_touches_only_its_channel (r : Room) (m : Nat) : differOnly roomFace (confirmIn r 0 m) r .confirmed := fun q hq => by cases q with | vendorRoom => show joinMap (fun q => q.confirmed) ((r.requests.map (fun q => cond (Nat.beq q.channel 0) (confirm q m) q)).filter (fun q => Nat.beq q.channel 1)) = joinMap (fun q => q.confirmed) (r.requests.filter (fun q => Nat.beq q.channel 1)) rw [a_confirmation_elsewhere_leaves_a_channel 0 1 m rfl r.requests] | confirmed => exact absurd rfl hq | guests => rfl | sheet => rfl | ledger => rfl | timeline => rfl | bach => rfl /-- info: 'Eih.Treaty.a_confirmation_touches_only_its_channel' does not depend on any axioms -/ #guard_msgs in #print axioms a_confirmation_touches_only_its_channel theorem a_vendor_room_confirmation_touches_only_the_vendor_room (r : Room) (m : Nat) : differOnly roomFace (confirmIn r 1 m) r .vendorRoom := fun q hq => by cases q with | confirmed => show joinMap (fun q => q.confirmed) ((r.requests.map (fun q => cond (Nat.beq q.channel 1) (confirm q m) q)).filter (fun q => Nat.beq q.channel 0)) = joinMap (fun q => q.confirmed) (r.requests.filter (fun q => Nat.beq q.channel 0)) rw [a_confirmation_elsewhere_leaves_a_channel 1 0 m rfl r.requests] | vendorRoom => exact absurd rfl hq | guests => rfl | sheet => rfl | ledger => rfl | timeline => rfl | bach => rfl /-- info: 'Eih.Treaty.a_vendor_room_confirmation_touches_only_the_vendor_room' does not depend on any axioms -/ #guard_msgs in #print axioms a_vendor_room_confirmation_touches_only_the_vendor_room theorem a_quiet_seat_does_not_hear_it (s : List Ask) (p : Ask) (h : enrolled Ask.beq s p = false) : ¬ hears roomFace s p := (by (apply Room.the_unenrolled_are_no_member <;> first | (apply an_ask_reads_itself <;> fail) | assumption)) /-- info: 'Eih.Treaty.a_quiet_seat_does_not_hear_it' does not depend on any axioms -/ #guard_msgs in #print axioms a_quiet_seat_does_not_hear_it theorem the_bach_wall (r : Room) (b : List Nat) (hb : b ≠ r.bach) : reads roomFace coupleSeat (withBach r b) = reads roomFace coupleSeat r ∧ reads roomFace bestManSeat (withBach r b) ≠ reads roomFace bestManSeat r := by (intros; (repeat' constructor); all_goals (intros; (apply the_bach_parts_the_best_man <;> assumption))) /-- info: 'Eih.Treaty.the_bach_wall' does not depend on any axioms -/ #guard_msgs in #print axioms the_bach_wall theorem no_couple_side_seat_hears_the_vendor_room : ¬ hears roomFace (earshot roomFace coupleSideSeats) .vendorRoom := (by (apply a_quiet_seat_does_not_hear_it <;> rfl)) /-- info: 'Eih.Treaty.no_couple_side_seat_hears_the_vendor_room' does not depend on any axioms -/ #guard_msgs in #print axioms no_couple_side_seat_hears_the_vendor_room theorem the_vendor_room_holds_its_own_receipt (r : Room) (m : Nat) : reads roomFace coupleSeat (confirmIn r 1 m) = reads roomFace coupleSeat r ∧ reads roomFace lindaSeat (confirmIn r 1 m) = reads roomFace lindaSeat r ∧ reads roomFace bestManSeat (confirmIn r 1 m) = reads roomFace bestManSeat r := ⟨a_wall_hides_the_probe roomFace (a_vendor_room_confirmation_touches_only_the_vendor_room r m) coupleSeat (a_quiet_seat_does_not_hear_it coupleSeat .vendorRoom rfl), a_wall_hides_the_probe roomFace (a_vendor_room_confirmation_touches_only_the_vendor_room r m) lindaSeat (a_quiet_seat_does_not_hear_it lindaSeat .vendorRoom rfl), a_wall_hides_the_probe roomFace (a_vendor_room_confirmation_touches_only_the_vendor_room r m) bestManSeat (a_quiet_seat_does_not_hear_it bestManSeat .vendorRoom rfl)⟩ /-- info: 'Eih.Treaty.the_vendor_room_holds_its_own_receipt' does not depend on any axioms -/ #guard_msgs in #print axioms the_vendor_room_holds_its_own_receipt theorem the_couple_side_witnesses_no_vendor_room_license (r : Room) (m : Nat) : witnessed roomFace coupleSideSeats (confirmIn r 1 m) r := fun s hs => a_wall_hides_the_probe roomFace (a_vendor_room_confirmation_touches_only_the_vendor_room r m) s (fun hp => no_couple_side_seat_hears_the_vendor_room (mem_joinMap_intro hs hp)) /-- info: 'Eih.Treaty.the_couple_side_witnesses_no_vendor_room_license' does not depend on any axioms -/ #guard_msgs in #print axioms the_couple_side_witnesses_no_vendor_room_license theorem everyone_is_here (r : Room) (h : allClear r) {p : Party} (hp : p ∈ r.guests) (hr : p.rsvp = true) {m : Nat} (hm : m ∈ p.meals) (x : Nat) {gl gl' : List Party} (hperm : gl.Perm gl') : m ∈ r.delivered ∧ (∀ q, q ∈ r.requests → settled q = true) ∧ (sheet r.guests).length = heads r.guests ∧ heads gl = heads gl' ∧ witnessed roomFace coupleSideSeats (confirmIn r 1 x) r ∧ reads roomFace coupleSeat (confirmIn r 1 x) = reads roomFace coupleSeat r := ⟨everyone_clear_means_rose_ate r h hp hr hm, everyone_clear_means_every_request_settled r h, the_sheet_counts_the_heads r.guests, reseating_keeps_the_heads hperm, the_couple_side_witnesses_no_vendor_room_license r x, (the_vendor_room_holds_its_own_receipt r x).1⟩ /-- info: 'Eih.Treaty.everyone_is_here' does not depend on any axioms -/ #guard_msgs in #print axioms everyone_is_here end Eih.Treaty
nothing waits.
-- the vestibule of EVERYONE IS HERE: the disagreements between the product as its team describes it -- and the treaty as it stands, each a statement in the assay's own terms and the darkness it waits on. -- a held statement seats when what it waits on arrives: the customer's word, a carrier, a reach of the -- drawer's fragment, or a seating in the treaty's translator. read by bin/counter book. -- the first round (2026-09-04, Abe's answers through isaac) seated six statements into the assay -- (the_audience_hears_the_receipt_by_name, outside_the_audience_hears_no_receipt, the_sender_is_never_asked, -- the_same_page_counts_only_within_earshot, the_payer_is_the_owner_or_the_host, edit_is_within_sight and -- its two instances), refuted one (a member is a Membership; guests are never members; who can be asked is -- the audience of the channel minus the sender), and left these. -- Abe, in the room (2026-09-04): the day-of sheet is everyone's to edit with a memory, anyone opens a task and -- only its owner, the couple, or the planner closes it — "yep that's great" — seated as -- anyone_may_open_a_task and the_day_of_sheet_is_everyones_to_edit; the day lane's exclusion from tasks -- still waits on lanes as a carrier, below. -- the sixth round (the house's turn): Same page is a drawn sum — stated as a sum (List.sum over the -- requests the viewer hears, mapped through tally) and read by the drawer as an aggregate, its two laws -- re-proved over the filter; the season's total the same way, a face applied inside a lambda read as a -- call to the face's function. a structural recursion (undo) and a pair-valued reading (venueTable) stay -- beyond, and a list of lists (seasonView) is held as undrawn: the shadow holds no jagged array. -- the seventh round (the house's turn): a lane is a member's sub-seat over the pages — memberSees subtracts -- and never adds (lanes_shrink_never_lock, restated at the member), the day lane sees no task list and keeps -- the day-of sheet, an edit is within the lane; the two page-number lists the assay carried since its first -- day retired for the real thing. -- the vestibule is empty (2026-09-04, isaac's move): the business, parked by Abe until a studio arrives, -- cleared — if it is needed it comes back by being asked for; the repo does not remember on his behalf. -- a held statement here is a disagreement between the customer's word and the treaty; today there is none. -- the eighth round (2026-09-08, Abe between turns at league night, through isaac): the first one-liner -- of the feature file, "a Role is one of: couple, planner, vendor, venue, party", refused at the first -- word — "planner is vendor, or planner is couple." held: a planner is not a Role; a planner is a vendor -- or the couple. waits on a carrier (the Role enum, and Member.kind, which may be where it already -- lives) and on Abe's word for which one, when. the feature (assays/sheet.feature) follows him now. -- the same round, his second word: "venue is a vendor. couple / vendor / helper (mother in law, wedding -- party member, etc)." held: the venue is not a Role, it is a vendor; and the Role called party is a -- helper, wider than the wedding party — a mother-in-law is one. so the Roles are three: couple, vendor, -- helper. waits on the same carrier (the Role enum) and on the rules that hand each Role its pages, which -- the treaty states for five and he states for three. the feature follows him. -- his third word: "is a vendor a helper who gets paid? — yep." held: a vendor is not a Role; a vendor is -- a helper with a truth, paid. so the Roles are two, couple and helper, and the pages a paid helper is -- handed (the invoices, among them) are a rule over the role and the truth together. waits on a carrier -- (paid, a truth on Member) and on a rule shape the feature grammar does not yet have — a sentence like -- "a vendor is a helper who is paid" compiling to the retirement of a constructor and the minting of a -- field. the feature keeps vendor as its own constructor until the grammar can say what he said. -- his fourth word, on the pages: "yes. look at the demo. might be more but those are some." held: the -- ten pages are a floor, not the list; the list waits on the demo. an enum is closed by construction, so -- a page the demo has and the treaty lacks is a carrier waiting to be minted, and every rule over pages -- widens when it lands. the sheet keeps the ten and says so. -- his sixth word: "and Vendor Pro — they don't see any pages that have to do with just the vendor. My -- season is only for season pass vendors." held: My season is a page (the demo's twelfth), seen by no -- couple and by no unpaid helper, and by a paid helper only with the season pass — a SECOND truth on a -- helper, pro, beside paid. the treaty has the season as a Thing the vendor owns (owner .season = .vendor, -- seasonView, the_seasons_sum_is_over_my_own_invoices) and no truth for the pass; the sheet's grammar -- has one truth per model tonight. waits on a carrier (pro) and on the grammar's sentence for a second -- truth. the sheet keeps the page, keeps the couple and the unpaid out of it, and says nothing yet about -- the paid helper there. -- his seventh word came through his Claude, reading the demo: the mother of the bride is the wedding -- party role, and what she sees depends on her LANE — the planning lane (home, the channels she is in, -- tasks, same page, day-of, planning team, the seating chart with the guest names, editable, files, the -- guide, her profile) or the helping-with-the-day lane (home, chats, same page, day-of, the chart, her -- profile: tasks, team, files, and the guide drop away; the view shrinks, it doesn't lock). never: guests, -- site, invoices and budget, the vendor room, my season, the who-can-edit panel. the treaty has the lane -- (Member.dayLane, the_day_lane_sees_no_task_list, lanes_shrink_never_lock) and not files, guide, or team -- dropping in the day lane; the sheet has one truth per model and cannot say the lane yet. held: the lane -- as a third truth beside paid and pro, and five more pages on the floor — home, channels, files, the -- guide, my profile — and the seating chart as floor plan and guest names in one page. and a fact for the -- log: their walls table said invoices was off for the wedding party while the demo sidebar showed it; the -- table won and the demo was fixed the same hour. -- his eighth word: "what room?" — and "no bachelor party stuff. there's already an app for that." the -- room is his word (one room for the whole wedding) and the sentence was the house's: a room is not -- asked for anything, it has things. the bachelor party is a carrier the treaty holds — bach, withBach, -- the_bach_wall, the_bach_parts_the_best_man, the best man's seat hearing it — that he refuses whole. -- held: the treaty cuts a carrier the day this seats, and the best man's seat keeps the timeline. the -- sheet has already let it go. -- his ninth word, frame five: "the room has: the guests, the sheet, the timeline — it also has the seating -- chart, the tasks, planning team, files, invoices." held: the treaty keeps an Ask (what the room holds as -- data: guests, sheet, ledger, timeline, confirmed, vendorRoom) and a Page (the sidebar) as two lists, and -- in his mouth they are one list — the room has the pages. and isaac's reading at the table: roles are a -- payor (sponsor) and help, paid or not; a page's scope is who is handed it; the scopes he sees are -- payor-only, payor-and-all-help, paid-help-only. a scope is a column's pattern in the grid, so the -- drawer prints the scopes as a census rather than the treaty minting a type. waits on the treaty joining -- Ask and Page, and on Abe's word for "sponsor" against "couple." -- his tenth word, frames nine and ten: "the couple slot always needs to pay to have access to EIH, paid for -- by themselves or the vendor" — and isaac's reading, "a room needs to be paid to be opened, doesn't matter -- by who, just by someone": yup. a CONFIRMATION, not a hold: the treaty's lawful (the payer is the owner, -- or a vendor paying for their couple), its rows ownWedding, coveredWedding, strayBill, and -- the_payer_is_the_owner_or_the_host, seated on the fourth. and vendors pay for a season pass, which is -- the season as a Thing the vendor owns. named at the table as a LAW OF ROOMS across three products -- (softer's payment tier, yours' second day, EIH's couple slot): a room opens on a payment; the payment is -- for the room and not for the occupant; the payer need not be the one who sits. a species candidate — -- it knows no product's name — for Room's germ when the turn gets there. -- his eleventh word: "the caterer sees: the timeline, the sheet" — "what sheet." the sheet is Roster's word -- (the per-head meal sheet the room delivers, sheet gl) and the assay's probe; his sidebar says HEADCOUNT -- and his day-of page is the day-of sheet. held: the probe's name waits on his word; the feature file that -- was named for the wrong word twice is assays/everyone.feature now, his product's first word. -- his thirteenth and fourteenth words: the best man, an unpaid helper who gets the timeline on top — -- yep. the couple gets the guests, the headcount, and the timeline from the room — "yep and other -- things." the treaty's coupleSeat hears the ledger and the confirmations too; the sheet's room holds -- only guests, headcount, and timeline as data. held: the room's other things, in his words, when he -- names them; the treaty's guess is the invoices and the confirmations. -- his fifteenth word, a screenshot of the couple's sidebar, answering "what else does the room hold for -- the couple": CHANNELS — #Everyone, and a private chat per vendor (Photography; Bloom & Vine Florals) the -- couple is in, beside the vendor room they are not — and the BADGES: Guests 1 waiting (unanswered), Same -- page 2/6 (samePage, the tally), Tasks 4, Invoices 2, Files 4 (lengths), Wedding site DRAFT (a state on -- a page, which nothing in the treaty holds). the treaty has the channels (Channel.audience, visible, -- inChannel, vendorRoomAudience, a_file_is_never_wider_than_its_channel) and the readings; the sheet's -- grammar has neither channels nor a page's state. held: a sentence for a channel and its audience, a -- sentence for a badge as a reading, and the draft as a truth on a page. -- his sixteenth and seventeenth words. a private chat: "so far it's couples and one vendor. but I will -- make group chats available." held: a private chat's audience is the couple and one vendor today — the -- treaty's Channel.audience holds it as a list, which already affords the group chat he intends, so the -- carrier waits on nothing and the rule (who may be added) waits on his word. the wedding site's DRAFT: -- "idk?" — held with the darkness typed in his own vocabulary: UNKNOWN, the maintainer's own. an answer -- of "I don't know" is an answer; the ask is covered, and the row waits on the demo (which may have -- invented the badge) or on a day he decides. the first row of the night that waits on nobody's word -- but the future's. -- the door's first arrival (2026-09-09, Abe's Claude, by git; the chair fable-abe under fable at ../counter): the house -- regrown whole on a two-core sandbox through the chair — every gate silent and green, every treaty vector identical, -- 1994 of Witness's candidates answered by the memo and 0 judged. then the feature, in Abe's sentences with the dates -- he said yes on: a venue is a vendor (his second word, now a line); a planner is a vendor (two prices, not three, -- 2026-09-08); an invoice is an Ask the room holds, heard by the couple, and three walls that nobody else hears it land -- (withInvoice_changes_nothing_the_caterer/bestMan/venue_hears — regrown by the_append_rests, the prepend door's own -- law); and the decided rule as a wall: withGuests changes nothing the venue hears. six walls, six receipts, thirty-one -- guards. held, by the same hand: the planner's walls beyond paid (guest names on the chart, assigns tasks — one truth -- per model); the lane as a third truth (the mother of the bride's two sidebars, above); pro, for My season; and the -- rule the door itself made necessary, from Ian's question the same day: nobody has to log in to be reached — a member -- reached by text and replying YES is confirmed, which is a second kind of member the treaty does not yet type.
graph LR
subgraph Eih_Treaty["Eih.Treaty"]
a_confirmation_elsewhere_leaves_a_channel["a_confirmation_elsewhere_leaves_a_channel"]
a_confirmation_parts_the_audience["a_confirmation_parts_the_audience"]
a_confirmation_touches_only_its_channel["a_confirmation_touches_only_its_channel"]
a_covered_wedding_is_still_the_couples["a_covered_wedding_is_still_the_couples"]
a_file_is_never_wider_than_its_channel["a_file_is_never_wider_than_its_channel"]
a_line_touches_only_the_ledger["a_line_touches_only_the_ledger"]
a_quiet_seat_does_not_hear_it["a_quiet_seat_does_not_hear_it"]
a_season_reads_each_room_as_the_vendor["a_season_reads_each_room_as_the_vendor"]
a_vendor_is_in_the_vendor_room["a_vendor_is_in_the_vendor_room"]
a_vendor_may_not_close_anothers["a_vendor_may_not_close_anothers"]
a_vendor_never_sees_anothers_invoice["a_vendor_never_sees_anothers_invoice"]
a_vendor_room_confirmation_touches_only_the_vendor_room["a_vendor_room_confirmation_touches_only_the_vendor_room"]
a_vendor_room_file_is_absent_from_the_couples_files["a_vendor_room_file_is_absent_from_the_couples_files"]
a_vendor_sees_only_their_own["a_vendor_sees_only_their_own"]
a_vendor_sees_the_floor_and_edits_nothing_there["a_vendor_sees_the_floor_and_edits_nothing_there"]
an_ask_reads_itself["an_ask_reads_itself"]
an_audience_is_members["an_audience_is_members"]
an_edit_is_within_the_lane["an_edit_is_within_the_lane"]
anyone_may_open_a_task["anyone_may_open_a_task"]
edit_is_within_sight["edit_is_within_sight"]
every_edit_is_kept["every_edit_is_kept"]
everyone_clear_means_every_request_settled["everyone_clear_means_every_request_settled"]
everyone_clear_means_rose_ate["everyone_clear_means_rose_ate"]
everyone_is_here["everyone_is_here"]
join_and_pay_are_unrelated["join_and_pay_are_unrelated"]
lanes_shrink_never_lock["lanes_shrink_never_lock"]
linda_never_sees_the_ledger["linda_never_sees_the_ledger"]
no_couple_side_seat_hears_the_vendor_room["no_couple_side_seat_hears_the_vendor_room"]
outside_the_audience_hears_no_receipt["outside_the_audience_hears_no_receipt"]
the_audience_hears_the_receipt_by_name["the_audience_hears_the_receipt_by_name"]
the_bach_parts_the_best_man["the_bach_parts_the_best_man"]
the_bach_touches_only_the_bach["the_bach_touches_only_the_bach"]
the_bach_wall["the_bach_wall"]
the_caterer_never_sees_the_guests["the_caterer_never_sees_the_guests"]
the_caterer_never_sees_the_ledger["the_caterer_never_sees_the_ledger"]
the_caterer_reads_the_delivery["the_caterer_reads_the_delivery"]
the_couple_is_never_in_the_vendor_room["the_couple_is_never_in_the_vendor_room"]
the_couple_may_close["the_couple_may_close"]
the_couple_side_witnesses_no_vendor_room_license["the_couple_side_witnesses_no_vendor_room_license"]
the_day_lane_keeps_the_day_of_sheet["the_day_lane_keeps_the_day_of_sheet"]
the_day_lane_sees_no_task_list["the_day_lane_sees_no_task_list"]
the_day_of_sheet_is_everyones_to_edit["the_day_of_sheet_is_everyones_to_edit"]
the_delivery_is_the_sheet["the_delivery_is_the_sheet"]
the_delivery_moves_no_guest["the_delivery_moves_no_guest"]
the_guests_touch_only_the_guests["the_guests_touch_only_the_guests"]
the_last_edit_undoes["the_last_edit_undoes"]
the_maker_sees_shape_not_content["the_maker_sees_shape_not_content"]
the_owner_may_close["the_owner_may_close"]
the_party_never_pays["the_party_never_pays"]
the_payer_is_the_owner_or_the_host["the_payer_is_the_owner_or_the_host"]
the_room_covers_itself["the_room_covers_itself"]
the_room_witnesses_the_license["the_room_witnesses_the_license"]
the_same_page_counts_only_within_earshot["the_same_page_counts_only_within_earshot"]
the_same_page_hears_its_own_earshot["the_same_page_hears_its_own_earshot"]
the_seasons_sum_is_over_my_own_invoices["the_seasons_sum_is_over_my_own_invoices"]
the_sender_is_never_asked["the_sender_is_never_asked"]
the_vendor_room_holds_its_own_receipt["the_vendor_room_holds_its_own_receipt"]
the_vendor_room_is_derived_from_the_roster["the_vendor_room_is_derived_from_the_roster"]
the_venue_edits_the_floor_and_never_sees_the_list["the_venue_edits_the_floor_and_never_sees_the_list"]
the_venue_reads_counts_not_names["the_venue_reads_counts_not_names"]
the_wedding_party_is_never_in_the_vendor_room["the_wedding_party_is_never_in_the_vendor_room"]
end
subgraph Witness["Witness"]
Witness_a_narrower_seat_reads_no_more["a_narrower_seat_reads_no_more"]
Witness_a_room_covers_itself_at_one_seat["a_room_covers_itself_at_one_seat"]
Witness_a_wall_hides_the_probe["a_wall_hides_the_probe"]
Witness_speak_now["speak_now"]
Witness_the_probe_reads_the_seat["the_probe_reads_the_seat"]
Witness_the_seat_that_hears_it_reads_it["the_seat_that_hears_it_reads_it"]
end
subgraph Roster["Roster"]
Roster_a_yes_reaches_the_sheet["a_yes_reaches_the_sheet"]
Roster_reseating_keeps_the_heads["reseating_keeps_the_heads"]
Roster_the_sheet_counts_the_heads["the_sheet_counts_the_heads"]
end
the_caterer_never_sees_the_ledger --> Witness_a_narrower_seat_reads_no_more
the_caterer_never_sees_the_ledger --> Witness_the_probe_reads_the_seat
a_confirmation_parts_the_audience --> Witness_the_seat_that_hears_it_reads_it
linda_never_sees_the_ledger --> Witness_a_narrower_seat_reads_no_more
linda_never_sees_the_ledger --> Witness_the_probe_reads_the_seat
no_couple_side_seat_hears_the_vendor_room --> a_quiet_seat_does_not_hear_it
the_bach_wall --> the_bach_parts_the_best_man
the_room_witnesses_the_license --> Witness_speak_now
everyone_clear_means_rose_ate --> Roster_a_yes_reaches_the_sheet
the_bach_parts_the_best_man --> Witness_the_seat_that_hears_it_reads_it
a_quiet_seat_does_not_hear_it --> an_ask_reads_itself
a_confirmation_touches_only_its_channel --> a_confirmation_elsewhere_leaves_a_channel
the_room_covers_itself --> Witness_a_room_covers_itself_at_one_seat
a_vendor_room_confirmation_touches_only_the_vendor_room --> a_confirmation_elsewhere_leaves_a_channel
everyone_is_here --> the_couple_side_witnesses_no_vendor_room_license
everyone_is_here --> everyone_clear_means_every_request_settled
everyone_is_here --> the_vendor_room_holds_its_own_receipt
everyone_is_here --> everyone_clear_means_rose_ate
everyone_is_here --> Roster_the_sheet_counts_the_heads
everyone_is_here --> Roster_reseating_keeps_the_heads
the_couple_side_witnesses_no_vendor_room_license --> no_couple_side_seat_hears_the_vendor_room
the_couple_side_witnesses_no_vendor_room_license --> Witness_a_wall_hides_the_probe
the_couple_side_witnesses_no_vendor_room_license --> a_vendor_room_confirmation_touches_only_the_vendor_room
the_caterer_never_sees_the_guests --> Witness_a_narrower_seat_reads_no_more
the_caterer_never_sees_the_guests --> Witness_the_probe_reads_the_seat
the_vendor_room_holds_its_own_receipt --> a_quiet_seat_does_not_hear_it
the_vendor_room_holds_its_own_receipt --> Witness_a_wall_hides_the_probe
the_vendor_room_holds_its_own_receipt --> a_vendor_room_confirmation_touches_only_the_vendor_room
-- the data-model shadow of grown/assays/eih.lean, read from the kernel (bin/counter schema)
-- every foreign key is a field; every policy is a theorem; nothing here that the treaty does not need
CREATE TYPE page AS ENUM ('floorPlan', 'guestList', 'samePage', 'invoices', 'budget', 'guests', 'site', 'team', 'dayOf', 'tasks');
CREATE TYPE ask AS ENUM ('guests', 'sheet', 'ledger', 'timeline', 'bach', 'confirmed', 'vendorRoom');
CREATE TYPE vendor_ask AS ENUM ('timeline', 'mine');
CREATE TYPE role AS ENUM ('couple', 'planner', 'vendor', 'venue', 'party');
CREATE TYPE thing AS ENUM ('wedding', 'season');
CREATE TABLE member (
id serial PRIMARY KEY,
user_ integer NOT NULL,
role role NOT NULL,
kind integer NOT NULL,
day_lane boolean NOT NULL,
arrival integer NOT NULL,
phone integer NOT NULL
);
CREATE TABLE request (
id serial PRIMARY KEY,
channel integer NOT NULL,
audience integer[] NOT NULL,
sender integer NOT NULL,
confirmed integer[] NOT NULL
);
CREATE TABLE party (
id serial PRIMARY KEY,
name integer NOT NULL,
rsvp boolean NOT NULL,
meals integer[] NOT NULL
);
CREATE TABLE day_of_edit (
id serial PRIMARY KEY,
who integer NOT NULL,
row integer NOT NULL,
before integer NOT NULL,
after integer NOT NULL
);
CREATE TABLE channel (
id serial PRIMARY KEY,
audience integer[] NOT NULL
);
CREATE TABLE task (
id serial PRIMARY KEY,
owner integer NOT NULL,
assignee integer NOT NULL,
done boolean NOT NULL
);
CREATE TABLE file (
id serial PRIMARY KEY,
channel integer NOT NULL REFERENCES channel(id)
);
CREATE TABLE bill (
id serial PRIMARY KEY,
thing thing NOT NULL,
payer role NOT NULL
);
CREATE TABLE table_ (
id serial PRIMARY KEY,
shape integer NOT NULL,
occupants integer[] NOT NULL
);
CREATE TABLE room (
id serial PRIMARY KEY,
delivered integer[] NOT NULL,
timeline integer[] NOT NULL,
bach integer[] NOT NULL
);
CREATE TABLE room_guests (
room_id integer NOT NULL REFERENCES room(id),
position integer NOT NULL,
party_id integer NOT NULL REFERENCES party(id)
);
CREATE TABLE room_ledger (
room_id integer NOT NULL REFERENCES room(id),
position integer NOT NULL,
c0 integer NOT NULL,
c1 integer NOT NULL,
c2 integer NOT NULL
);
CREATE TABLE room_requests (
room_id integer NOT NULL REFERENCES room(id),
position integer NOT NULL,
request_id integer NOT NULL REFERENCES request(id)
);
-- makerFace: a face over room — each probe a column
CREATE FUNCTION room_as_maker_face(room_id integer) RETURNS TABLE(unit integer) LANGUAGE sql STABLE AS $$
SELECT cardinality((SELECT array_agg(party_id ORDER BY position) FROM room_guests c WHERE c.room_id = room.id)) FROM room WHERE id = $1 $$;
-- roomFace: a face over room — each probe a column
CREATE FUNCTION room_as_room_face(room_id integer) RETURNS TABLE(guests integer[], sheet integer[], ledger integer[], timeline integer[], bach integer[], confirmed integer[], vendor_room integer[]) LANGUAGE sql STABLE AS $$
SELECT ARRAY(SELECT (SELECT name FROM party WHERE id = x) FROM unnest((SELECT array_agg(party_id ORDER BY position) FROM room_guests c WHERE c.room_id = room.id)) WITH ORDINALITY AS u(x, o) ORDER BY o), room.delivered, ARRAY(SELECT (x).c2 FROM unnest((SELECT array_agg(c ORDER BY position) FROM room_ledger c WHERE c.room_id = room.id)) AS x ORDER BY (x).position), room.timeline, room.bach, ARRAY(SELECT m FROM unnest(ARRAY(SELECT x FROM unnest((SELECT array_agg(request_id ORDER BY position) FROM room_requests c WHERE c.room_id = room.id)) WITH ORDINALITY AS u(x, o) WHERE ((SELECT channel FROM request WHERE id = x) = 0) ORDER BY o)) WITH ORDINALITY AS u(x, o), unnest((SELECT confirmed FROM request WHERE id = x)) WITH ORDINALITY AS v(m, i) ORDER BY o, i), ARRAY(SELECT m FROM unnest(ARRAY(SELECT x FROM unnest((SELECT array_agg(request_id ORDER BY position) FROM room_requests c WHERE c.room_id = room.id)) WITH ORDINALITY AS u(x, o) WHERE ((SELECT channel FROM request WHERE id = x) = 1) ORDER BY o)) WITH ORDINALITY AS u(x, o), unnest((SELECT confirmed FROM request WHERE id = x)) WITH ORDINALITY AS v(m, i) ORDER BY o, i) FROM room WHERE id = $1 $$;
-- vendorFace: a face over room, parameterized (1) — each probe a column
CREATE FUNCTION room_as_vendor_face(room_id integer, p1 integer) RETURNS TABLE(timeline integer[], mine integer[]) LANGUAGE sql STABLE AS $$
SELECT room.timeline, ARRAY(SELECT (x).c2 FROM unnest(ARRAY(SELECT x FROM unnest((SELECT array_agg(c ORDER BY position) FROM room_ledger c WHERE c.room_id = room.id)) AS x WHERE ((x).c0 = $2) ORDER BY (x).position)) AS x ORDER BY (x).position) FROM room WHERE id = $1 $$;
-- joinsFree: a rule over role, derived, never stored
CREATE FUNCTION joins_free(role) RETURNS boolean LANGUAGE sql IMMUTABLE AS $$
SELECT CASE $1 WHEN 'couple' THEN true WHEN 'planner' THEN true WHEN 'vendor' THEN true WHEN 'venue' THEN true WHEN 'party' THEN true END $$;
-- edited: a rule over role, derived, never stored
CREATE FUNCTION edited(role) RETURNS page[] LANGUAGE sql IMMUTABLE AS $$
SELECT CASE $1 WHEN 'couple' THEN ARRAY['floorPlan', 'guestList', 'samePage', 'invoices', 'budget', 'guests', 'site', 'team', 'dayOf', 'tasks']::page[] WHEN 'planner' THEN ARRAY['floorPlan', 'guestList', 'invoices', 'team', 'dayOf', 'tasks']::page[] WHEN 'vendor' THEN ARRAY['invoices', 'dayOf', 'tasks']::page[] WHEN 'venue' THEN ARRAY['floorPlan', 'invoices', 'dayOf', 'tasks']::page[] WHEN 'party' THEN ARRAY['floorPlan', 'guestList', 'dayOf', 'tasks']::page[] END $$;
-- seen: a rule over role, derived, never stored
CREATE FUNCTION seen(role) RETURNS page[] LANGUAGE sql IMMUTABLE AS $$
SELECT CASE $1 WHEN 'couple' THEN ARRAY['floorPlan', 'guestList', 'samePage', 'invoices', 'budget', 'guests', 'site', 'team', 'dayOf', 'tasks']::page[] WHEN 'planner' THEN ARRAY['floorPlan', 'guestList', 'samePage', 'invoices', 'team', 'dayOf', 'tasks']::page[] WHEN 'vendor' THEN ARRAY['floorPlan', 'samePage', 'invoices', 'team', 'dayOf', 'tasks']::page[] WHEN 'venue' THEN ARRAY['floorPlan', 'samePage', 'invoices', 'team', 'dayOf', 'tasks']::page[] WHEN 'party' THEN ARRAY['floorPlan', 'guestList', 'samePage', 'team', 'dayOf', 'tasks']::page[] END $$;
-- pays: a rule over role, derived, never stored
CREATE FUNCTION pays(role) RETURNS boolean LANGUAGE sql IMMUTABLE AS $$
SELECT CASE $1 WHEN 'couple' THEN true WHEN 'planner' THEN true WHEN 'vendor' THEN true WHEN 'venue' THEN true WHEN 'party' THEN false END $$;
-- owner: a rule over thing, derived, never stored
CREATE FUNCTION owner(thing) RETURNS role LANGUAGE sql IMMUTABLE AS $$
SELECT (CASE $1 WHEN 'wedding' THEN 'couple' WHEN 'season' THEN 'vendor' END)::role $$;
-- vendorRoomRequestOf: derived, not yet drawn (data over List Eih.Treaty.Member)
-- heardBy: derived, never stored
-- described by outside_the_audience_hears_no_receipt, the_audience_hears_the_receipt_by_name
CREATE FUNCTION heard_by(request_id integer, arg2 integer) RETURNS integer[] LANGUAGE sql STABLE AS $$
SELECT (CASE WHEN (arg2 = ANY(SELECT unnest(request.audience))) THEN request.confirmed ELSE ARRAY[]::integer[] END) FROM request WHERE id = $1 $$;
-- channelAudience: derived, not yet drawn (data over List Eih.Treaty.Member)
-- inChannel: derived, never stored
CREATE FUNCTION in_channel(request_ids integer[], arg2 integer) RETURNS integer[] LANGUAGE sql STABLE AS $$
SELECT ARRAY(SELECT m FROM unnest(ARRAY(SELECT x FROM unnest($1) WITH ORDINALITY AS u(x, o) WHERE ((SELECT channel FROM request WHERE id = x) = arg2) ORDER BY o)) WITH ORDINALITY AS u(x, o), unnest((SELECT confirmed FROM request WHERE id = x)) WITH ORDINALITY AS v(m, i) ORDER BY o, i) $$;
-- asked: derived, never stored
-- described by the_sender_is_never_asked
CREATE FUNCTION asked(request_id integer) RETURNS integer[] LANGUAGE sql STABLE AS $$
SELECT ARRAY(SELECT x FROM unnest(request.audience) WITH ORDINALITY AS u(x, o) WHERE (NOT (x = request.sender)) ORDER BY o) FROM request WHERE id = $1 $$;
-- readRoom: derived, not yet drawn (data over Eih.Treaty.Room)
-- seasonView: derived, not yet drawn (a list of lists — the shadow holds no jagged array)
-- venue_chart: derived, not yet drawn (calls venue_table, beyond the fragment)
-- venueTable: derived, not yet drawn (data over Eih.Treaty.Table)
-- sheet: derived, never stored
-- described by everyone_is_here, the_caterer_reads_the_delivery, the_delivery_is_the_sheet
CREATE FUNCTION sheet(party_ids integer[]) RETURNS integer[] LANGUAGE sql STABLE AS $$
SELECT (SELECT array_agg(m ORDER BY g.position) FROM unnest($1) WITH ORDINALITY AS g(elem_id, position) JOIN party p ON p.id = g.elem_id, unnest(p.meals) m WHERE p.rsvp) $$;
-- visible: a check, derived, never stored
-- described by a_file_is_never_wider_than_its_channel, a_vendor_room_file_is_absent_from_the_couples_files
CREATE FUNCTION visible(file_id integer, arg2 integer) RETURNS boolean LANGUAGE sql STABLE AS $$
SELECT (arg2 = ANY(SELECT unnest((SELECT audience FROM channel WHERE id = file.channel)))) FROM file WHERE id = $1 $$;
-- canSee: a check, derived, never stored
-- described by a_vendor_room_file_is_absent_from_the_couples_files
CREATE FUNCTION can_see(file_id integer, arg2 integer) RETURNS boolean LANGUAGE sql STABLE AS $$
SELECT (arg2 = ANY(SELECT unnest((SELECT audience FROM channel WHERE id = file.channel)))) FROM file WHERE id = $1 $$;
-- mayClose: a check, derived, never stored
-- described by a_vendor_may_not_close_anothers, the_couple_may_close, the_owner_may_close
CREATE FUNCTION may_close(member_id integer, arg2 integer) RETURNS boolean LANGUAGE sql STABLE AS $$
SELECT ((member.user_ = (SELECT owner FROM task WHERE id = arg2)) OR ((member.role = 'couple') OR (member.role = 'planner'))) FROM member WHERE id = $1 $$;
-- vendorSide: a check, derived, never stored
-- described by the_vendor_room_is_derived_from_the_roster
CREATE FUNCTION vendor_side(member_id integer) RETURNS boolean LANGUAGE sql STABLE AS $$
SELECT ((member.role = 'vendor') OR ((member.role = 'venue') OR (member.role = 'planner'))) FROM member WHERE id = $1 $$;
-- mayOpen: a check, derived, never stored
-- described by anyone_may_open_a_task
CREATE FUNCTION may_open(member_id integer) RETURNS boolean LANGUAGE sql STABLE AS $$
SELECT true FROM member WHERE id = $1 $$;
-- withBach: a clerk — never a second copy of the row, an update to it
-- described by the_bach_parts_the_best_man, the_bach_touches_only_the_bach, the_bach_wall
CREATE FUNCTION with_bach(room_id integer, arg2 integer[]) RETURNS void LANGUAGE sql AS $$
UPDATE room SET bach = arg2 WHERE id = $1 $$;
-- ask: a clerk over a has-many field (requests) — not yet drawn
-- withLine: a clerk over the has-many ledger — a prepend: shift the child rows, insert at zero
-- described by a_line_touches_only_the_ledger, a_vendor_never_sees_anothers_invoice, linda_never_sees_the_ledger, the_caterer_never_sees_the_ledger
CREATE FUNCTION with_line(room_id integer, arg2 integer[]) RETURNS void LANGUAGE sql AS $$
UPDATE room_ledger SET position = position + 1 WHERE room_id = $1;
INSERT INTO room_ledger (room_id, position, c0, c1, c2) VALUES ($1, 0, $2[1], $2[2], $2[3]) $$;
-- confirm: a clerk — never a second copy of the row, an update to it
-- described by a_confirmation_elsewhere_leaves_a_channel, outside_the_audience_hears_no_receipt
CREATE FUNCTION confirm(request_id integer, arg2 integer) RETURNS void LANGUAGE sql AS $$
UPDATE request SET confirmed = array_prepend(arg2, request.confirmed) WHERE id = $1 $$;
-- close: a clerk — never a second copy of the row, an update to it
CREATE FUNCTION close(task_id integer) RETURNS void LANGUAGE sql AS $$
UPDATE task SET done = true WHERE id = $1 $$;
-- withGuests: a clerk over the has-many guests — a replacement: delete, then insert in order
-- described by the_caterer_never_sees_the_guests, the_guests_touch_only_the_guests, the_maker_sees_shape_not_content
CREATE FUNCTION with_guests(room_id integer, arg2 integer[]) RETURNS void LANGUAGE sql AS $$
DELETE FROM room_guests WHERE room_id = $1;
INSERT INTO room_guests (room_id, position, party_id) SELECT $1, ordinality - 1, id FROM unnest($2) WITH ORDINALITY AS u(id, ordinality) $$;
-- assign: a clerk — never a second copy of the row, an update to it
CREATE FUNCTION assign(task_id integer, arg2 integer) RETURNS void LANGUAGE sql AS $$
UPDATE task SET assignee = arg2 WHERE id = $1 $$;
-- undo: derived, not yet drawn (a function over List Nat)
-- edits: a rule over role, derived, never stored
CREATE FUNCTION edits(role, page) RETURNS boolean LANGUAGE sql IMMUTABLE AS $$
SELECT ($2 = ANY(SELECT unnest(edited($1)))) $$;
-- sees: a rule over role, derived, never stored
CREATE FUNCTION sees(role, page) RETURNS boolean LANGUAGE sql IMMUTABLE AS $$
SELECT ($2 = ANY(SELECT unnest(seen($1)))) $$;
-- seasonOwed: derived, never stored
-- described by the_seasons_sum_is_over_my_own_invoices
CREATE FUNCTION season_owed(room_ids integer[], arg2 integer) RETURNS integer LANGUAGE sql STABLE AS $$
SELECT (SELECT coalesce(sum(x), 0) FROM unnest(ARRAY(SELECT m FROM unnest($1) WITH ORDINALITY AS u(x, o), unnest((SELECT mine FROM room_as_vendor_face(x, arg2))) WITH ORDINALITY AS v(m, i) ORDER BY o, i)) AS x) $$;
-- vendorRoomMembers: derived, never stored
-- described by a_vendor_is_in_the_vendor_room, the_couple_is_never_in_the_vendor_room, the_wedding_party_is_never_in_the_vendor_room
CREATE FUNCTION vendor_room_members(member_ids integer[]) RETURNS integer[] LANGUAGE sql STABLE AS $$
SELECT ARRAY(SELECT x FROM unnest($1) WITH ORDINALITY AS u(x, o) WHERE vendor_side(x) ORDER BY o) $$;
-- tally: derived, never stored
-- described by the_same_page_hears_its_own_earshot
CREATE FUNCTION tally(request_id integer) RETURNS integer LANGUAGE sql STABLE AS $$
SELECT cardinality(ARRAY(SELECT x FROM unnest(request.confirmed) WITH ORDINALITY AS u(x, o) WHERE (x = ANY(SELECT unnest(asked(request.id)))) ORDER BY o)) FROM request WHERE id = $1 $$;
-- heads: derived, never stored
-- described by (drawn by the_sheet_counts_the_heads), everyone_is_here
CREATE FUNCTION heads(party_ids integer[]) RETURNS integer LANGUAGE sql STABLE AS $$
SELECT cardinality(sheet($1)) $$;
-- lawful: a check, derived, never stored
-- described by the_payer_is_the_owner_or_the_host
CREATE FUNCTION lawful(bill_id integer) RETURNS boolean LANGUAGE sql STABLE AS $$
SELECT ((bill.payer = owner(bill.thing)) OR ((bill.payer = 'vendor') AND (owner(bill.thing) = 'couple'))) FROM bill WHERE id = $1 $$;
-- settled: a check, derived, never stored
-- described by everyone_clear_means_every_request_settled, everyone_is_here
CREATE FUNCTION settled(request_id integer) RETURNS boolean LANGUAGE sql STABLE AS $$
SELECT (asked(request.id) <@ request.confirmed) FROM request WHERE id = $1 $$;
-- deliver: a clerk — never a second copy of the row, an update to it
-- described by the_caterer_reads_the_delivery, the_delivery_is_the_sheet, the_delivery_moves_no_guest
CREATE FUNCTION deliver(room_id integer) RETURNS void LANGUAGE sql AS $$
UPDATE room SET delivered = sheet((SELECT array_agg(party_id ORDER BY position) FROM room_guests c WHERE c.room_id = room.id)) WHERE id = $1 $$;
-- confirmIn: a clerk over the has-many requests — the element's clerk confirm run on each child the condition selects
-- described by a_confirmation_parts_the_audience, a_confirmation_touches_only_its_channel, a_vendor_room_confirmation_touches_only_the_vendor_room, everyone_is_here, the_couple_side_witnesses_no_vendor_room_license, the_vendor_room_holds_its_own_receipt
CREATE FUNCTION confirm_in(room_id integer, arg2 integer, arg3 integer) RETURNS void LANGUAGE sql AS $$
SELECT confirm(c.request_id, arg3) FROM room_requests c WHERE c.room_id = $1 AND ((SELECT channel FROM request WHERE id = c.request_id) = arg2) $$;
-- samePage: derived, never stored
-- described by the_same_page_counts_only_within_earshot, the_same_page_hears_its_own_earshot
CREATE FUNCTION same_page(request_ids integer[], arg2 integer) RETURNS integer LANGUAGE sql STABLE AS $$
SELECT (SELECT coalesce(sum(x), 0) FROM unnest(ARRAY(SELECT tally(x) FROM unnest(ARRAY(SELECT x FROM unnest($1) WITH ORDINALITY AS u(x, o) WHERE (arg2 = ANY(SELECT unnest((SELECT audience FROM request WHERE id = x)))) ORDER BY o)) WITH ORDINALITY AS u(x, o) ORDER BY o)) AS x) $$;
-- unanswered: derived, never stored
CREATE FUNCTION unanswered(request_ids integer[]) RETURNS integer[] LANGUAGE sql STABLE AS $$
SELECT ARRAY(SELECT x FROM unnest($1) WITH ORDINALITY AS u(x, o) WHERE (NOT settled(x)) ORDER BY o) $$;
-- vendorRoomAudience: derived, never stored
-- described by the_vendor_room_is_derived_from_the_roster
CREATE FUNCTION vendor_room_audience(member_ids integer[]) RETURNS integer[] LANGUAGE sql STABLE AS $$
SELECT ARRAY(SELECT (SELECT user_ FROM member WHERE id = x) FROM unnest(vendor_room_members($1)) WITH ORDINALITY AS u(x, o) ORDER BY o) $$;
-- memberSees: a check, derived, never stored
-- described by an_edit_is_within_the_lane, lanes_shrink_never_lock, the_day_lane_keeps_the_day_of_sheet, the_day_lane_sees_no_task_list
CREATE FUNCTION member_sees(member_id integer, arg2 page) RETURNS boolean LANGUAGE sql STABLE AS $$
SELECT (sees(member.role, arg2) AND (NOT (member.day_lane AND (arg2 = 'tasks')))) FROM member WHERE id = $1 $$;
-- allClear: a check, derived, never stored
-- described by everyone_clear_means_every_request_settled, everyone_clear_means_rose_ate, everyone_is_here
CREATE FUNCTION all_clear(room_id integer) RETURNS boolean LANGUAGE sql STABLE AS $$
SELECT ((room.delivered = sheet((SELECT array_agg(party_id ORDER BY position) FROM room_guests c WHERE c.room_id = room.id))) AND (unanswered((SELECT array_agg(request_id ORDER BY position) FROM room_requests c WHERE c.room_id = room.id)) = ARRAY[]::integer[])) FROM room WHERE id = $1 $$;
-- memberEdits: a check, derived, never stored
-- described by an_edit_is_within_the_lane
CREATE FUNCTION member_edits(member_id integer, arg2 page) RETURNS boolean LANGUAGE sql STABLE AS $$
SELECT (edits(member.role, arg2) AND member_sees(member.id, arg2)) FROM member WHERE id = $1 $$;
-- catererSeat: hears timeline, sheet, confirmed, vendorRoom
-- licensed by the_caterer_never_sees_the_guests, the_caterer_never_sees_the_ledger
CREATE VIEW room_as_caterer_seat AS SELECT room.id, f.timeline, f.sheet, f.confirmed, f.vendor_room FROM room, LATERAL room_as_room_face(room.id) f;
-- roomSeat: hears guests, sheet, ledger, timeline, bach, confirmed, vendorRoom
-- licensed by the_room_covers_itself, the_room_witnesses_the_license
CREATE VIEW room_as_room_seat AS SELECT room.id, f.guests, f.sheet, f.ledger, f.timeline, f.bach, f.confirmed, f.vendor_room FROM room, LATERAL room_as_room_face(room.id) f;
-- lindaSeat: hears guests, timeline, confirmed
-- licensed by everyone_is_here, linda_never_sees_the_ledger, the_vendor_room_holds_its_own_receipt
CREATE VIEW room_as_linda_seat AS SELECT room.id, f.guests, f.timeline, f.confirmed FROM room, LATERAL room_as_room_face(room.id) f;
-- coupleSeat: hears guests, sheet, ledger, timeline, confirmed
-- licensed by a_confirmation_parts_the_audience, everyone_is_here, the_bach_wall, the_vendor_room_holds_its_own_receipt
CREATE VIEW room_as_couple_seat AS SELECT room.id, f.guests, f.sheet, f.ledger, f.timeline, f.confirmed FROM room, LATERAL room_as_room_face(room.id) f;
-- pages: hears floorPlan, guestList, samePage, invoices, budget, guests, site, team, dayOf, tasks
CREATE VIEW member_as_pages AS SELECT id, role AS floor_plan, role AS guest_list, role AS same_page, role AS invoices, role AS budget, role AS guests, role AS site, role AS team, role AS day_of, role AS tasks FROM member;
-- bestManSeat: hears timeline, bach, confirmed
-- licensed by everyone_is_here, the_bach_parts_the_best_man, the_bach_wall, the_vendor_room_holds_its_own_receipt
CREATE VIEW room_as_best_man_seat AS SELECT room.id, f.timeline, f.bach, f.confirmed FROM room, LATERAL room_as_room_face(room.id) f;