game — a product as an assay, on Witness

51 receipts inline · 323 lines · pinned 4d0a8f73f91e4307 — shasum -a 256 of this file, cut to 16, as pins has it · lake env lean game.lean prints nothing when every receipt passes

import Witness
open Room Face Witness
set_option autoImplicit false

namespace Game

structure World where
  weight : Nat
  hue : Nat
  heads : Nat

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

def weight : Nat := 0

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

def hue : Nat := 1

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

def heads : Nat := 2

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

def see (w : World) (p : Nat) : Nat :=
  cond (Nat.beq p weight) w.weight (cond (Nat.beq p hue) w.hue (cond (Nat.beq p heads) w.heads 0))

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

def worldFace : Face := ⟨World, Nat, Nat, see⟩

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

def firstGap (x y : World) : List Nat → Option Nat
  | [] => none
  | p :: ps => cond (Nat.beq (see x p) (see y p)) (firstGap x y ps) (some p)

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

def fuelToPart (x y : World) : List Nat → Nat
  | [] => 0
  | p :: ps => cond (Nat.beq (see x p) (see y p)) (fuelToPart x y ps + 1) 1

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

def room : List Nat := [weight, hue, heads]

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

def deaf : List Nat := [weight, heads]

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

def a : World := ⟨3, 5, 1⟩

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

def b : World := ⟨4, 5, 1⟩

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

def c : World := ⟨3, 6, 1⟩

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

def levelOne : door World Nat × door World Nat := (atTheDoor a 7, atTheDoor b 7)

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

def levelTwo : door World Nat × door World Nat := (atTheDoor a 7, atTheDoor a 9)

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

def levelThree : door World Nat × door World Nat := (atTheDoor a 7, atTheDoor a 7)

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

def levelFour : door World Nat × door World Nat := (atTheDoor a 7, atTheDoor c 7)

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

def levelOneGap : Option Nat := firstGap a b room

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

def levelOneFuel : Nat := fuelToPart a b room

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

def levelFourAtTheDeafSeat : Option Nat := firstGap a c deaf

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

def levelFourAtTheRoom : Option Nat := firstGap a c room

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

def levelFourFuel : Nat := fuelToPart a c room

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

def levelTwoAtTheRoom : Option Nat := firstGap a a room

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

def deafReadsA : List Nat := reads worldFace deaf a

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

def deafReadsC : List Nat := reads worldFace deaf c

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

def roomReadsA : List Nat := reads worldFace room a

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

def roomReadsC : List Nat := reads worldFace room c

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

def mirrorOfA : door Nat Nat := turnAbout (atTheDoor (3 : Nat) (3 : Nat))

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

def notAMirror : door Nat Nat := turnAbout (atTheDoor (3 : Nat) (5 : Nat))

#guard levelOneGap == some weight
#guard levelOneFuel == 1
#guard levelTwoAtTheRoom == none
#guard levelFourAtTheDeafSeat == none
#guard levelFourAtTheRoom == some hue
#guard levelFourFuel == 2
#guard deafReadsA == deafReadsC
#guard roomReadsA != roomReadsC
#guard face mirrorOfA == 3 && met mirrorOfA == 3
#guard face notAMirror == 5 && met notAMirror == 3

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

def res3 : Nat → Nat
  | 0 => 0
  | 1 => 1
  | 2 => 2
  | n + 3 => res3 n

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

def tick (d : door World Nat) : door World Nat :=
  atTheDoor ⟨(face d).weight + res3 (met d), (face d).hue, (face d).heads⟩ (met d + 1)

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

def after : Nat → door World Nat → door World Nat
  | 0, d => d
  | k + 1, d => after k (tick d)

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

def partsAt (d d' : door World Nat) (k : Nat) : Bool :=
  !(Nat.beq (see (face (after k d)) weight) (see (face (after k d')) weight))

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

def crossingWithin (d d' : door World Nat) : Nat → Nat → Option Nat
  | _, 0 => none
  | k, fuel + 1 => cond (partsAt d d' k) (some k) (crossingWithin d d' (k + 1) fuel)

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

def levelFive : door World Nat × door World Nat := (atTheDoor a 7, atTheDoor a 9)

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

def levelSix : door World Nat × door World Nat := (atTheDoor a 7, atTheDoor a 10)

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

def levelFiveCrossing : Option Nat := crossingWithin (atTheDoor a 7) (atTheDoor a 9) 0 12

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

def levelSixCrossing : Option Nat := crossingWithin (atTheDoor a 7) (atTheDoor a 10) 0 12

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

def levelFiveWeights : Nat × Nat := ((face (after 1 (atTheDoor a 7))).weight, (face (after 1 (atTheDoor a 9))).weight)

#guard levelFiveCrossing == some 1
#guard levelSixCrossing == none
#guard levelFiveWeights == (4, 3)
#guard partsAt (atTheDoor a 7) (atTheDoor a 10) 5 == false
#guard met (after 4 (atTheDoor a 7)) == 11

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

theorem level_one_is_timelike : ¬ alike worldFace a b :=
  fun h => absurd (h weight) (by show ¬ (see a weight = see b weight); decide)

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

theorem level_two_is_lightlike :
    alike (host worldFace Nat) (atTheDoor a 7) (atTheDoor a 9) ∧ ¬ alike (widen worldFace Nat) (atTheDoor a 7) (atTheDoor a 9) :=
  ⟨the_host_merges_the_guests worldFace Nat a 7 9, a_wider_seat_reads_the_remainder worldFace a (by decide)⟩

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

theorem level_three_is_spacelike : alike (widen worldFace Nat) (atTheDoor a 7) (atTheDoor a 7) :=
  by (intro x; induction x; all_goals ((intros; rfl)))

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

theorem level_four_is_a_wall_at_the_deaf_seat : reads worldFace deaf a = reads worldFace deaf c :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

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

theorem level_four_is_read_at_the_room : reads worldFace room a ≠ reads worldFace room c :=
  fun h => absurd (the_first_mark_reads (the_rest_reads h)) (by show ¬ (see a hue = see c hue); decide)

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

theorem the_engine_agrees_or_names_the_gap (x y : World) (seat : List Nat) :
    (∀ p, p ∈ seat → Nat.beq (see x p) (see y p) = true) ∨ ∃ p, p ∈ seat ∧ Nat.beq (see x p) (see y p) = false :=
  the_window_agrees_or_names_the_gap worldFace Nat.beq x y seat

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

theorem the_mirror (d : door Nat Nat) : turnAbout d = d ↔ met d = face d :=
  (by (apply Face.the_yield_fixes_the_agreed <;> fail))

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

theorem level_five_parts_at_the_first_tick : partsAt (atTheDoor a 7) (atTheDoor a 9) 1 = true :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

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

theorem level_six_is_in_step_to_twelve : crossingWithin (atTheDoor a 7) (atTheDoor a 10) 0 12 = none :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

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

theorem the_two_secrets_are_alike_at_the_door : alike (host worldFace Nat) (atTheDoor a 7) (atTheDoor a 10) :=
  by (intro x; induction x; all_goals ((intros; rfl)))

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

theorem the_tick_hears_the_secret_only_as_a_residue (w : World) (s : Nat) :
    face (tick (atTheDoor w s)) = face (tick (atTheDoor w (s + 3))) :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

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

theorem the_three_fates :
    ¬ alike worldFace a b
      ∧ (alike (host worldFace Nat) (atTheDoor a 7) (atTheDoor a 9) ∧ ¬ alike (widen worldFace Nat) (atTheDoor a 7) (atTheDoor a 9))
      ∧ alike (widen worldFace Nat) (atTheDoor a 7) (atTheDoor a 7) :=
  by
    (intros; (repeat' constructor);
      all_goals
        (intros;
          first
          | (apply level_one_is_timelike <;> fail)
          | (apply the_two_secrets_are_alike_at_the_door <;> fail)
          | (apply ((level_two_is_lightlike)).2 <;> fail)
          | (apply level_three_is_spacelike <;> fail)))

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

end Game

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 Game["Game"]
    level_five_parts_at_the_first_tick["level_five_parts_at_the_first_tick"]
    level_four_is_a_wall_at_the_deaf_seat["level_four_is_a_wall_at_the_deaf_seat"]
    level_four_is_read_at_the_room["level_four_is_read_at_the_room"]
    level_one_is_timelike["level_one_is_timelike"]
    level_six_is_in_step_to_twelve["level_six_is_in_step_to_twelve"]
    level_three_is_spacelike["level_three_is_spacelike"]
    level_two_is_lightlike["level_two_is_lightlike"]
    the_engine_agrees_or_names_the_gap["the_engine_agrees_or_names_the_gap"]
    the_mirror["the_mirror"]
    the_three_fates["the_three_fates"]
    the_tick_hears_the_secret_only_as_a_residue["the_tick_hears_the_secret_only_as_a_residue"]
    the_two_secrets_are_alike_at_the_door["the_two_secrets_are_alike_at_the_door"]
  end
  the_three_fates --> the_two_secrets_are_alike_at_the_door
  the_three_fates --> level_one_is_timelike
  the_three_fates --> level_two_is_lightlike
  the_three_fates --> level_three_is_spacelike

the 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/game.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 TABLE world (
  id serial PRIMARY KEY,
  weight integer NOT NULL,
  hue integer NOT NULL,
  heads integer NOT NULL
);

-- worldFace: a face over world whose probes are names — one reading, of the row and the probe
CREATE FUNCTION world_as_world_face(world_id integer, probe integer) RETURNS integer LANGUAGE sql STABLE AS $$
  SELECT ⟨unread⟩ FROM world WHERE id = $1 $$;

-- firstGap: derived, not yet drawn (data over Game.World)

-- fuelToPart: derived, not yet drawn (data over Game.World)

-- see: derived, not yet drawn (data over Game.World)

-- res3: derived, not yet drawn (a function over Nat)