everyone — a product as an assay, on Witness
46 receipts inline · 302 lines · pinned 592aea676ba2e661 — shasum -a 256 of this file, cut to 16, as pins has it · lake env lean everyone.lean prints nothing when every receipt passes
import Witness
open Room Face Witness
set_option autoImplicit false
namespace Everyone.Treaty
inductive Role where
| couple | helper
/-- info: 'Everyone.Treaty.Role' does not depend on any axioms -/
#guard_msgs in #print axioms Role
def Role.code : Role → Nat
| .couple => 0 | .helper => 1
/-- info: 'Everyone.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: 'Everyone.Treaty.Role.beq' does not depend on any axioms -/
#guard_msgs in #print axioms Role.beq
def roles : List Role := [.couple, .helper]
/-- info: 'Everyone.Treaty.roles' does not depend on any axioms -/
#guard_msgs in #print axioms roles
inductive Page where
| home | seatingChart | guestList | samePage | invoices | budget | guests | site | team | dayOf | tasks | files | guide | profile | vendorChat | mySeason
/-- info: 'Everyone.Treaty.Page' does not depend on any axioms -/
#guard_msgs in #print axioms Page
def Page.code : Page → Nat
| .home => 0 | .seatingChart => 1 | .guestList => 2 | .samePage => 3 | .invoices => 4 | .budget => 5 | .guests => 6 | .site => 7 | .team => 8 | .dayOf => 9 | .tasks => 10 | .files => 11 | .guide => 12 | .profile => 13 | .vendorChat => 14 | .mySeason => 15
/-- info: 'Everyone.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: 'Everyone.Treaty.Page.beq' does not depend on any axioms -/
#guard_msgs in #print axioms Page.beq
def pages : List Page := [.home, .seatingChart, .guestList, .samePage, .invoices, .budget, .guests, .site, .team, .dayOf, .tasks, .files, .guide, .profile, .vendorChat, .mySeason]
/-- info: 'Everyone.Treaty.pages' does not depend on any axioms -/
#guard_msgs in #print axioms pages
inductive Ask where
| guests | headcount | timeline | invoices
/-- info: 'Everyone.Treaty.Ask' does not depend on any axioms -/
#guard_msgs in #print axioms Ask
def Ask.code : Ask → Nat
| .guests => 0 | .headcount => 1 | .timeline => 2 | .invoices => 3
/-- info: 'Everyone.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: 'Everyone.Treaty.Ask.beq' does not depend on any axioms -/
#guard_msgs in #print axioms Ask.beq
def asks : List Ask := [.guests, .headcount, .timeline, .invoices]
/-- info: 'Everyone.Treaty.asks' does not depend on any axioms -/
#guard_msgs in #print axioms asks
structure Room where
guests : List Nat
delivered : List Nat
timeline : List Nat
invoices : List Nat
/-- info: 'Everyone.Treaty.Room' does not depend on any axioms -/
#guard_msgs in #print axioms Room
def readRoom (r : Room) : Ask → List Nat
| .guests => r.guests
| .headcount => r.delivered
| .timeline => r.timeline
| .invoices => r.invoices
/-- info: 'Everyone.Treaty.readRoom' does not depend on any axioms -/
#guard_msgs in #print axioms readRoom
def roomFace : Face := ⟨Room, Ask, List Nat, readRoom⟩
/-- info: 'Everyone.Treaty.roomFace' does not depend on any axioms -/
#guard_msgs in #print axioms roomFace
def seenPaid : Role → List Page
| .couple => [.home, .seatingChart, .guestList, .samePage, .invoices, .budget, .guests, .site, .team, .dayOf, .tasks, .files, .guide, .profile]
| .helper => [.home, .seatingChart, .samePage, .invoices, .team, .dayOf, .tasks, .files, .guide, .profile, .vendorChat]
/-- info: 'Everyone.Treaty.seenPaid' does not depend on any axioms -/
#guard_msgs in #print axioms seenPaid
def seenUnpaid : Role → List Page
| .couple => [.home, .seatingChart, .guestList, .samePage, .invoices, .budget, .guests, .site, .team, .dayOf, .tasks, .files, .guide, .profile]
| .helper => [.home, .seatingChart, .guestList, .samePage, .team, .dayOf, .tasks, .files, .guide, .profile]
/-- info: 'Everyone.Treaty.seenUnpaid' does not depend on any axioms -/
#guard_msgs in #print axioms seenUnpaid
def seen (ρ : Role) (paid : Bool) : List Page := cond paid (seenPaid ρ) (seenUnpaid ρ)
/-- info: 'Everyone.Treaty.seen' does not depend on any axioms -/
#guard_msgs in #print axioms seen
def sees (ρ : Role) (paid : Bool) (p : Page) : Bool := enrolled Page.beq (seen ρ paid) p
/-- info: 'Everyone.Treaty.sees' does not depend on any axioms -/
#guard_msgs in #print axioms sees
def editedPaid : Role → List Page
| .couple => [.home, .seatingChart, .guestList, .samePage, .invoices, .budget, .guests, .site, .team, .dayOf, .tasks, .files, .guide, .profile]
| .helper => [.invoices, .dayOf, .tasks, .files, .profile, .vendorChat]
/-- info: 'Everyone.Treaty.editedPaid' does not depend on any axioms -/
#guard_msgs in #print axioms editedPaid
def editedUnpaid : Role → List Page
| .couple => [.home, .seatingChart, .guestList, .samePage, .invoices, .budget, .guests, .site, .team, .dayOf, .tasks, .files, .guide, .profile]
| .helper => [.seatingChart, .guestList, .dayOf, .tasks, .files, .profile]
/-- info: 'Everyone.Treaty.editedUnpaid' does not depend on any axioms -/
#guard_msgs in #print axioms editedUnpaid
def edited (ρ : Role) (paid : Bool) : List Page := cond paid (editedPaid ρ) (editedUnpaid ρ)
/-- info: 'Everyone.Treaty.edited' does not depend on any axioms -/
#guard_msgs in #print axioms edited
def edits (ρ : Role) (paid : Bool) (p : Page) : Bool := enrolled Page.beq (edited ρ paid) p
/-- info: 'Everyone.Treaty.edits' does not depend on any axioms -/
#guard_msgs in #print axioms edits
def coupleSeat : List Ask := [.guests, .headcount, .timeline, .invoices]
/-- info: 'Everyone.Treaty.coupleSeat' does not depend on any axioms -/
#guard_msgs in #print axioms coupleSeat
def catererSeat : List Ask := [.timeline, .headcount]
/-- info: 'Everyone.Treaty.catererSeat' does not depend on any axioms -/
#guard_msgs in #print axioms catererSeat
def bestManSeat : List Ask := [.timeline]
/-- info: 'Everyone.Treaty.bestManSeat' does not depend on any axioms -/
#guard_msgs in #print axioms bestManSeat
def venueSeat : List Ask := [.timeline, .headcount]
/-- info: 'Everyone.Treaty.venueSeat' does not depend on any axioms -/
#guard_msgs in #print axioms venueSeat
def withGuests (r : Room) (x : List Nat) : Room := { r with guests := x }
/-- info: 'Everyone.Treaty.withGuests' does not depend on any axioms -/
#guard_msgs in #print axioms withGuests
def withTime (r : Room) (x : Nat) : Room := { r with timeline := x :: r.timeline }
/-- info: 'Everyone.Treaty.withTime' does not depend on any axioms -/
#guard_msgs in #print axioms withTime
def withInvoice (r : Room) (x : Nat) : Room := { r with invoices := x :: r.invoices }
/-- info: 'Everyone.Treaty.withInvoice' does not depend on any axioms -/
#guard_msgs in #print axioms withInvoice
def demo : Room := ⟨[2, 3, 1], [], [10, 11, 12], []⟩
/-- info: 'Everyone.Treaty.demo' does not depend on any axioms -/
#guard_msgs in #print axioms demo
def later : Room := withTime demo 9
/-- info: 'Everyone.Treaty.later' does not depend on any axioms -/
#guard_msgs in #print axioms later
def billed : Room := withInvoice demo 1200
/-- info: 'Everyone.Treaty.billed' does not depend on any axioms -/
#guard_msgs in #print axioms billed
def catererInDemo : List (List Nat) := reads roomFace catererSeat demo
#guard catererInDemo == [[10, 11, 12], []]
/-- info: 'Everyone.Treaty.catererInDemo' does not depend on any axioms -/
#guard_msgs in #print axioms catererInDemo
def bestManInLater : List (List Nat) := reads roomFace bestManSeat later
#guard bestManInLater == [[9, 10, 11, 12]]
/-- info: 'Everyone.Treaty.bestManInLater' does not depend on any axioms -/
#guard_msgs in #print axioms bestManInLater
def coupleInLater : List (List Nat) := reads roomFace coupleSeat later
#guard coupleInLater == [[2, 3, 1], [], [9, 10, 11, 12], []]
/-- info: 'Everyone.Treaty.coupleInLater' does not depend on any axioms -/
#guard_msgs in #print axioms coupleInLater
def coupleInBilled : List (List Nat) := reads roomFace coupleSeat billed
#guard coupleInBilled == [[2, 3, 1], [], [10, 11, 12], [1200]]
/-- info: 'Everyone.Treaty.coupleInBilled' does not depend on any axioms -/
#guard_msgs in #print axioms coupleInBilled
def catererInBilled : List (List Nat) := reads roomFace catererSeat billed
#guard catererInBilled == [[10, 11, 12], []]
/-- info: 'Everyone.Treaty.catererInBilled' does not depend on any axioms -/
#guard_msgs in #print axioms catererInBilled
def venueInBilled : List (List Nat) := reads roomFace venueSeat billed
#guard venueInBilled == [[10, 11, 12], []]
/-- info: 'Everyone.Treaty.venueInBilled' does not depend on any axioms -/
#guard_msgs in #print axioms venueInBilled
def bestManInBilled : List (List Nat) := reads roomFace bestManSeat billed
#guard bestManInBilled == [[10, 11, 12]]
#guard sees .helper true .invoices == true
#guard sees .helper false .invoices == false
#guard sees .couple true .invoices == true
#guard sees .couple true .vendorChat == false
#guard sees .helper true .vendorChat == true
#guard sees .helper false .vendorChat == false
#guard sees .couple true .mySeason == false
#guard sees .helper false .mySeason == false
#guard sees .helper false .guests == false
#guard sees .helper false .site == false
#guard sees .helper false .budget == false
#guard sees .helper false .seatingChart == true
#guard sees .helper false .dayOf == true
#guard sees .helper true .invoices == true
#guard sees .helper true .guests == false
#guard sees .helper true .invoices == true
#guard sees .helper true .guests == false
#guard sees .helper true .site == false
#guard sees .helper true .vendorChat == true
#guard sees .helper true .vendorChat == true
#guard sees .helper true .invoices == true
#guard sees .helper true .guests == false
#guard sees .helper true .budget == false
#guard roles.all (fun ρ => edits ρ true .dayOf && edits ρ false .dayOf)
/-- info: 'Everyone.Treaty.bestManInBilled' does not depend on any axioms -/
#guard_msgs in #print axioms bestManInBilled
theorem withGuests_changes_nothing_the_caterer_hears (r : Room) (x : List Nat) :
reads roomFace catererSeat (withGuests r x) = reads roomFace catererSeat r :=
by (intros; (repeat' constructor); all_goals (intros; fail))
/-- info: 'Everyone.Treaty.withGuests_changes_nothing_the_caterer_hears' does not depend on any axioms -/
#guard_msgs in #print axioms withGuests_changes_nothing_the_caterer_hears
theorem withGuests_changes_nothing_the_bestMan_hears (r : Room) (x : List Nat) :
reads roomFace bestManSeat (withGuests r x) = reads roomFace bestManSeat r :=
by (intros; (repeat' constructor); all_goals (intros; fail))
/-- info: 'Everyone.Treaty.withGuests_changes_nothing_the_bestMan_hears' does not depend on any axioms -/
#guard_msgs in #print axioms withGuests_changes_nothing_the_bestMan_hears
theorem withGuests_changes_nothing_the_venue_hears (r : Room) (x : List Nat) :
reads roomFace venueSeat (withGuests r x) = reads roomFace venueSeat r :=
by (intros; (repeat' constructor); all_goals (intros; fail))
/-- info: 'Everyone.Treaty.withGuests_changes_nothing_the_venue_hears' does not depend on any axioms -/
#guard_msgs in #print axioms withGuests_changes_nothing_the_venue_hears
theorem withInvoice_changes_nothing_the_caterer_hears (r : Room) (x : Nat) :
reads roomFace catererSeat (withInvoice r x) = reads roomFace catererSeat r :=
by (intros; (repeat' constructor); all_goals (intros; fail))
/-- info: 'Everyone.Treaty.withInvoice_changes_nothing_the_caterer_hears' does not depend on any axioms -/
#guard_msgs in #print axioms withInvoice_changes_nothing_the_caterer_hears
theorem withInvoice_changes_nothing_the_bestMan_hears (r : Room) (x : Nat) :
reads roomFace bestManSeat (withInvoice r x) = reads roomFace bestManSeat r :=
by (intros; (repeat' constructor); all_goals (intros; fail))
/-- info: 'Everyone.Treaty.withInvoice_changes_nothing_the_bestMan_hears' does not depend on any axioms -/
#guard_msgs in #print axioms withInvoice_changes_nothing_the_bestMan_hears
theorem withInvoice_changes_nothing_the_venue_hears (r : Room) (x : Nat) :
reads roomFace venueSeat (withInvoice r x) = reads roomFace venueSeat r :=
by (intros; (repeat' constructor); all_goals (intros; fail))
/-- info: 'Everyone.Treaty.withInvoice_changes_nothing_the_venue_hears' does not depend on any axioms -/
#guard_msgs in #print axioms withInvoice_changes_nothing_the_venue_hears
end Everyone.Treatythe data-model shadow — every structure a table, every seat a view over the columns its probes read, every wall theorem the policy it licenses (bin/counter schema)
-- the data-model shadow of grown/assays/everyone.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 ask AS ENUM ('guests', 'headcount', 'timeline', 'invoices');
CREATE TYPE role AS ENUM ('couple', 'helper');
CREATE TYPE page AS ENUM ('home', 'seatingChart', 'guestList', 'samePage', 'invoices', 'budget', 'guests', 'site', 'team', 'dayOf', 'tasks', 'files', 'guide', 'profile', 'vendorChat', 'mySeason');
CREATE TABLE room (
id serial PRIMARY KEY,
guests integer[] NOT NULL,
delivered integer[] NOT NULL,
timeline integer[] NOT NULL,
invoices integer[] NOT NULL
);
-- roomFace: a face over room — each probe a column
CREATE FUNCTION room_as_room_face(room_id integer) RETURNS TABLE(guests integer[], headcount integer[], timeline integer[], invoices integer[]) LANGUAGE sql STABLE AS $$
SELECT room.guests, room.delivered, room.timeline, room.invoices FROM room WHERE id = $1 $$;
-- seenUnpaid: a rule over role, derived, never stored
CREATE FUNCTION seen_unpaid(role) RETURNS page[] LANGUAGE sql IMMUTABLE AS $$
SELECT CASE $1 WHEN 'couple' THEN ARRAY['home', 'seatingChart', 'guestList', 'samePage', 'invoices', 'budget', 'guests', 'site', 'team', 'dayOf', 'tasks', 'files', 'guide', 'profile']::page[] WHEN 'helper' THEN ARRAY['home', 'seatingChart', 'guestList', 'samePage', 'team', 'dayOf', 'tasks', 'files', 'guide', 'profile']::page[] END $$;
-- editedUnpaid: a rule over role, derived, never stored
CREATE FUNCTION edited_unpaid(role) RETURNS page[] LANGUAGE sql IMMUTABLE AS $$
SELECT CASE $1 WHEN 'couple' THEN ARRAY['home', 'seatingChart', 'guestList', 'samePage', 'invoices', 'budget', 'guests', 'site', 'team', 'dayOf', 'tasks', 'files', 'guide', 'profile']::page[] WHEN 'helper' THEN ARRAY['seatingChart', 'guestList', 'dayOf', 'tasks', 'files', 'profile']::page[] END $$;
-- edited: a rule over role, derived, never stored
CREATE FUNCTION edited(role, boolean) RETURNS page[] LANGUAGE sql IMMUTABLE AS $$
SELECT (CASE WHEN $2 THEN editedPaid($1) ELSE editedUnpaid($1) END) $$;
-- editedPaid: a rule over role, derived, never stored
CREATE FUNCTION edited_paid(role) RETURNS page[] LANGUAGE sql IMMUTABLE AS $$
SELECT CASE $1 WHEN 'couple' THEN ARRAY['home', 'seatingChart', 'guestList', 'samePage', 'invoices', 'budget', 'guests', 'site', 'team', 'dayOf', 'tasks', 'files', 'guide', 'profile']::page[] WHEN 'helper' THEN ARRAY['invoices', 'dayOf', 'tasks', 'files', 'profile', 'vendorChat']::page[] END $$;
-- seenPaid: a rule over role, derived, never stored
CREATE FUNCTION seen_paid(role) RETURNS page[] LANGUAGE sql IMMUTABLE AS $$
SELECT CASE $1 WHEN 'couple' THEN ARRAY['home', 'seatingChart', 'guestList', 'samePage', 'invoices', 'budget', 'guests', 'site', 'team', 'dayOf', 'tasks', 'files', 'guide', 'profile']::page[] WHEN 'helper' THEN ARRAY['home', 'seatingChart', 'samePage', 'invoices', 'team', 'dayOf', 'tasks', 'files', 'guide', 'profile', 'vendorChat']::page[] END $$;
-- seen: a rule over role, derived, never stored
CREATE FUNCTION seen(role, boolean) RETURNS page[] LANGUAGE sql IMMUTABLE AS $$
SELECT (CASE WHEN $2 THEN seenPaid($1) ELSE seenUnpaid($1) END) $$;
-- readRoom: derived, not yet drawn (data over Everyone.Treaty.Room)
-- withInvoice: a clerk — never a second copy of the row, an update to it
-- described by withInvoice_changes_nothing_the_bestMan_hears, withInvoice_changes_nothing_the_caterer_hears, withInvoice_changes_nothing_the_venue_hears
CREATE FUNCTION with_invoice(room_id integer, arg2 integer) RETURNS void LANGUAGE sql AS $$
UPDATE room SET invoices = array_prepend(arg2, room.invoices) WHERE id = $1 $$;
-- withTime: a clerk — never a second copy of the row, an update to it
CREATE FUNCTION with_time(room_id integer, arg2 integer) RETURNS void LANGUAGE sql AS $$
UPDATE room SET timeline = array_prepend(arg2, room.timeline) WHERE id = $1 $$;
-- withGuests: a clerk — never a second copy of the row, an update to it
-- described by withGuests_changes_nothing_the_bestMan_hears, withGuests_changes_nothing_the_caterer_hears, withGuests_changes_nothing_the_venue_hears
CREATE FUNCTION with_guests(room_id integer, arg2 integer[]) RETURNS void LANGUAGE sql AS $$
UPDATE room SET guests = arg2 WHERE id = $1 $$;
-- sees: a rule over role, derived, never stored
CREATE FUNCTION sees(role, boolean, page) RETURNS boolean LANGUAGE sql IMMUTABLE AS $$
SELECT ($3 = ANY(SELECT unnest(seen($1, $2)))) $$;
-- edits: a rule over role, derived, never stored
CREATE FUNCTION edits(role, boolean, page) RETURNS boolean LANGUAGE sql IMMUTABLE AS $$
SELECT ($3 = ANY(SELECT unnest(edited($1, $2)))) $$;
-- venueSeat: hears timeline, headcount
-- licensed by withGuests_changes_nothing_the_venue_hears, withInvoice_changes_nothing_the_venue_hears
CREATE VIEW room_as_venue_seat AS SELECT room.id, f.timeline, f.headcount FROM room, LATERAL room_as_room_face(room.id) f;
-- bestManSeat: hears timeline
-- licensed by withGuests_changes_nothing_the_bestMan_hears, withInvoice_changes_nothing_the_bestMan_hears
CREATE VIEW room_as_best_man_seat AS SELECT room.id, f.timeline FROM room, LATERAL room_as_room_face(room.id) f;
-- coupleSeat: hears guests, headcount, timeline, invoices
CREATE VIEW room_as_couple_seat AS SELECT room.id, f.guests, f.headcount, f.timeline, f.invoices FROM room, LATERAL room_as_room_face(room.id) f;
-- catererSeat: hears timeline, headcount
-- licensed by withGuests_changes_nothing_the_caterer_hears, withInvoice_changes_nothing_the_caterer_hears
CREATE VIEW room_as_caterer_seat AS SELECT room.id, f.timeline, f.headcount FROM room, LATERAL room_as_room_face(room.id) f;
-- asks: hears guests, headcount, timeline, invoices
CREATE VIEW room_as_asks AS SELECT room.id, f.guests, f.headcount, f.timeline, f.invoices FROM room, LATERAL room_as_room_face(room.id) f;