halt — a product as an assay, on Counter

12 receipts inline · 97 lines · pinned 22ae9119cccf1109 — shasum -a 256 of this file, cut to 16, as pins has it · lake env lean halt.lean prints nothing when every receipt passes

import Face
import Rest
import Counter
open Room Face Rest Counter
set_option autoImplicit false

namespace Halt

def stuck : room := ([], [(7, [7])])

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

def demo : room := ([], [(1, []), (2, [3]), (3, [])])

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

def seatedAfter (st : room) (k : Nat) : Option (List Nat) := (runs cascade.m cascade.steer cascade.rest st k).map (·.1)

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

def countAt (w : List Unit) (k : Nat) : Option Nat := (haltingGap Unit Nat).obs counting (w, k)

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

def carryAt (w : List Unit) (k : Nat) : Option Nat := (haltingGap Unit Nat).obs carrying (w, k)
#guard countAt [] 3 == some 3
#guard countAt [(), ()] 1 == some 3
#guard countAt [] 2 == none
#guard carryAt [] 3 == some 3
#guard carryAt [] 2 == none
#guard countAt [(), (), (), ()] 0 == carryAt [(), (), (), ()] 0
#guard seatedAfter demo 1 == none
#guard seatedAfter demo 2 == some [2, 3, 1]
#guard seatedAfter stuck 0 == some []
#guard settled stuck
#guard (sweep demo).2.length == 1

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

def countPlan (w : List Unit) (k : Nat) : Option Nat := read counting (plan counting w) k

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

def cascadePlan (w : List Unit) (k : Nat) : Option (List Nat) := (read cascade (plan cascade w) k).map (·.1)

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

def cascadeAt (st : room) (k : Nat) : Option (List Nat) := (read cascade st k).map (·.1)
#guard countPlan [] 3 == countAt [] 3
#guard countPlan [(), ()] 1 == countAt [(), ()] 1
#guard countPlan [] 2 == none
#guard countPlan [] 5 == countPlan [] 3
#guard cascadePlan [] 0 == some []
#guard cascadeAt demo 0 == none
#guard cascadeAt demo 3 == some [2, 3, 1]
#guard cascadeAt demo 9 == cascadeAt demo 3
#guard cascadeAt stuck 0 == some []

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

theorem the_counters_plan_is_read_at_the_gap (w : List Unit) (k : Nat) :
    read counting (plan counting w) k = (haltingGap Unit Nat).obs counting (w, k) :=
  (by (apply Rest.a_plan_is_read_at_the_gap <;> fail))

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

theorem two_readers_of_the_counter_agree (w : List Unit) (o o' : Nat) (f f' : Nat)
    (h : read counting (plan counting w) f = some o) (h' : read counting (plan counting w) f' = some o') : o = o' :=
  (by (apply Rest.every_reader_reads_the_same <;> assumption))

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

theorem the_cascades_replay_reads_its_plan (w : List Unit) (k : Nat) :
    read (replayRunner cascade) (plan (replayRunner cascade) w) k = read cascade (plan cascade w) k :=
  (by (apply Rest.the_replay_reads_the_plan <;> fail))

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

theorem a_plan_read_is_a_meeting_at_a_door (w : List Unit) (k : Nat) :
    read counting (plan counting w) k = walkIn (haltingGap Unit Nat).obs (atTheDoor counting (w, k)) :=
  (by (apply Rest.a_plan_is_read_at_the_gap <;> fail))

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

end Halt

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 Halt["Halt"]
    a_plan_read_is_a_meeting_at_a_door["a_plan_read_is_a_meeting_at_a_door"]
    the_cascades_replay_reads_its_plan["the_cascades_replay_reads_its_plan"]
    the_counters_plan_is_read_at_the_gap["the_counters_plan_is_read_at_the_gap"]
    two_readers_of_the_counter_agree["two_readers_of_the_counter_agree"]
  end
  subgraph Rest["Rest"]
    Rest_a_plan_is_read_at_the_gap["a_plan_is_read_at_the_gap"]
    Rest_every_reader_reads_the_same["every_reader_reads_the_same"]
    Rest_the_replay_reads_the_plan["the_replay_reads_the_plan"]
  end
  the_counters_plan_is_read_at_the_gap --> Rest_a_plan_is_read_at_the_gap
  a_plan_read_is_a_meeting_at_a_door --> Rest_a_plan_is_read_at_the_gap
  the_cascades_replay_reads_its_plan --> Rest_the_replay_reads_the_plan
  two_readers_of_the_counter_agree --> Rest_every_reader_reads_the_same

halt — a product as an assay, on Counter

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)

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)