Roster — parties with per-head meals, grown from germ/Roster.lean

7 receipts inline · 78 lines · pinned cd39e9677e0f44d1 — shasum -a 256 of this file, cut to 16, as pins has it · lake env lean Roster.lean prints nothing when every receipt passes

import Room
open Room

namespace Roster

structure Party where
  name : Nat
  rsvp : Bool
  meals : List Nat

/-- info: 'Roster.Party' does not depend on any axioms -/
#guard_msgs in #print axioms Party

def sheet : List Party → List Nat :=
  joinMap (fun p => cond p.rsvp p.meals [])

/-- info: 'Roster.sheet' does not depend on any axioms -/
#guard_msgs in #print axioms sheet

def heads : List Party → Nat
  | [] => 0
  | p :: gl => cond p.rsvp p.meals.length 0 + heads gl

/-- info: 'Roster.heads' does not depend on any axioms -/
#guard_msgs in #print axioms heads

theorem the_sheet_counts_the_heads : ∀ gl : List Party, (sheet gl).length = heads gl
  | [] => rfl
  | p :: gl => by
      show (cond p.rsvp p.meals [] ++ sheet gl).length = cond p.rsvp p.meals.length 0 + heads gl
      cases h : p.rsvp with
      | true =>
          show (p.meals ++ sheet gl).length = p.meals.length + heads gl
          rw [lengths_add, the_sheet_counts_the_heads gl]
      | false =>
          show (sheet gl).length = 0 + heads gl
          rw [zero_add, the_sheet_counts_the_heads gl]

/-- info: 'Roster.the_sheet_counts_the_heads' does not depend on any axioms -/
#guard_msgs in #print axioms the_sheet_counts_the_heads

theorem a_yes_reaches_the_sheet {p : Party} {gl : List Party} (hp : p ∈ gl)
    (hr : p.rsvp = true) {m : Nat} (hm : m ∈ p.meals) : m ∈ sheet gl :=
  mem_joinMap_intro hp (by show m ∈ cond p.rsvp p.meals []; rw [hr]; exact hm)

/-- info: 'Roster.a_yes_reaches_the_sheet' does not depend on any axioms -/
#guard_msgs in #print axioms a_yes_reaches_the_sheet

theorem reseating_keeps_the_heads {gl gl' : List Party} (h : gl.Perm gl') : heads gl = heads gl' := by
  induction h with
  | nil => rfl
  | cons a _ ih => exact congrArg (cond a.rsvp a.meals.length 0 + ·) ih
  | swap a b l =>
      show cond b.rsvp b.meals.length 0 + (cond a.rsvp a.meals.length 0 + heads l)
        = cond a.rsvp a.meals.length 0 + (cond b.rsvp b.meals.length 0 + heads l)
      exact Nat.add_left_comm _ _ _
  | trans _ _ ih₁ ih₂ => exact ih₁.trans ih₂

/-- info: 'Roster.reseating_keeps_the_heads' does not depend on any axioms -/
#guard_msgs in #print axioms reseating_keeps_the_heads

theorem reseating_keeps_the_sheets_count {gl gl' : List Party} (h : gl.Perm gl') :
    (sheet gl).length = (sheet gl').length :=
  by
    (intros; (try dsimp only [sheet, Party] at *); intros;
      (apply
            ((the_sheet_counts_the_heads _)).trans
              (by
                (apply
                      ((reseating_keeps_the_heads _)).trans
                        (by (apply ((the_sheet_counts_the_heads _)).symm <;> fail)) <;>
                    assumption)) <;>
          fail))

/-- info: 'Roster.reseating_keeps_the_sheets_count' does not depend on any axioms -/
#guard_msgs in #print axioms reseating_keeps_the_sheets_count

end Roster

the map of relations — every law a node, an arrow for each citation the elaborator reads (bin/counter chart; without --laws the carriers join the map)

graph LR
  subgraph Roster["Roster"]
    a_yes_reaches_the_sheet["a_yes_reaches_the_sheet"]
    reseating_keeps_the_heads["reseating_keeps_the_heads"]
    reseating_keeps_the_sheets_count["reseating_keeps_the_sheets_count"]
    the_sheet_counts_the_heads["the_sheet_counts_the_heads"]
  end
  subgraph Room["Room"]
    Room_lengths_add["lengths_add"]
    Room_mem_joinMap_intro["mem_joinMap_intro"]
    Room_zero_add["zero_add"]
  end
  reseating_keeps_the_sheets_count --> the_sheet_counts_the_heads
  reseating_keeps_the_sheets_count --> reseating_keeps_the_heads
  the_sheet_counts_the_heads --> Room_zero_add
  the_sheet_counts_the_heads --> Room_lengths_add
  a_yes_reaches_the_sheet --> Room_mem_joinMap_intro