relay — a product as an assay, on Face
22 receipts inline · 144 lines · pinned a63a5145ded36617 — shasum -a 256 of this file, cut to 16, as pins has it · lake env lean relay.lean prints nothing when every receipt passes
import Face
open Room Face
set_option autoImplicit false
namespace Relay
def stage (σ : List Bool → List Bool) (d : door Nat (List Bool)) : door Nat (List Bool) :=
vertical (fun d => σ (met d)) d
/-- info: 'Relay.stage' does not depend on any axioms -/
#guard_msgs in #print axioms stage
def relay (stages : List (List Bool → List Bool)) : door Nat (List Bool) → door Nat (List Bool)
| d => stages.foldl (fun d σ => stage σ d) d
/-- info: 'Relay.relay' does not depend on any axioms -/
#guard_msgs in #print axioms relay
def erase (s : List Bool) : List Bool := zeros s.length
/-- info: 'Relay.erase' does not depend on any axioms -/
#guard_msgs in #print axioms erase
def signal : List Bool := [true, false, true, true]
/-- info: 'Relay.signal' does not depend on any axioms -/
#guard_msgs in #print axioms signal
def sent : door Nat (List Bool) := atTheDoor (0 : Nat) signal
/-- info: 'Relay.sent' does not depend on any axioms -/
#guard_msgs in #print axioms sent
def throughOdometer : door Nat (List Bool) := relay [inc, inc, inc] sent
/-- info: 'Relay.throughOdometer' does not depend on any axioms -/
#guard_msgs in #print axioms throughOdometer
def recovered : List Bool := again dec 3 (met throughOdometer)
/-- info: 'Relay.recovered' does not depend on any axioms -/
#guard_msgs in #print axioms recovered
def throughErase : door Nat (List Bool) := relay [inc, erase] sent
/-- info: 'Relay.throughErase' does not depend on any axioms -/
#guard_msgs in #print axioms throughErase
def otherSignal : List Bool := [false, false, true, true]
/-- info: 'Relay.otherSignal' does not depend on any axioms -/
#guard_msgs in #print axioms otherSignal
def throughEraseOther : door Nat (List Bool) := relay [inc, erase] (atTheDoor (0 : Nat) otherSignal)
/-- info: 'Relay.throughEraseOther' does not depend on any axioms -/
#guard_msgs in #print axioms throughEraseOther
def faceSent : Nat := face sent
/-- info: 'Relay.faceSent' does not depend on any axioms -/
#guard_msgs in #print axioms faceSent
def faceArrived : Nat := face throughOdometer
#guard faceArrived == faceSent
#guard met throughOdometer != signal
#guard recovered == signal
#guard met throughErase == met throughEraseOther
#guard signal != otherSignal
/-- info: 'Relay.faceArrived' does not depend on any axioms -/
#guard_msgs in #print axioms faceArrived
def helloWorld : List Bool := [true, false, false, true, false, true, true, false]
/-- info: 'Relay.helloWorld' does not depend on any axioms -/
#guard_msgs in #print axioms helloWorld
def playedBack : List Bool := behavior (replayer (ledger Bool)) helloWorld
/-- info: 'Relay.playedBack' does not depend on any axioms -/
#guard_msgs in #print axioms playedBack
def theRouteKept : List Bool := park (replayer (ledger Bool)) [] helloWorld
#guard playedBack == helloWorld
#guard theRouteKept == helloWorld
#guard theRouteKept.length == helloWorld.length
/-- info: 'Relay.theRouteKept' does not depend on any axioms -/
#guard_msgs in #print axioms theRouteKept
theorem the_relay_is_unheard_at_the_face (σ : List Bool → List Bool) (d : door Nat (List Bool)) :
alike (host (originFace Nat) (List Bool)) (stage σ d) d :=
by (intro x; induction x; all_goals ((intros; rfl)))
/-- info: 'Relay.the_relay_is_unheard_at_the_face' does not depend on any axioms -/
#guard_msgs in #print axioms the_relay_is_unheard_at_the_face
theorem the_odometer_stage_has_a_section (s : List Bool) : dec (inc s) = s :=
(by (apply Room.the_tick_unwinds <;> fail))
/-- info: 'Relay.the_odometer_stage_has_a_section' does not depend on any axioms -/
#guard_msgs in #print axioms the_odometer_stage_has_a_section
theorem the_signal_is_recovered : again dec 3 (met throughOdometer) = signal :=
by (intros; (repeat' constructor); all_goals (intros; fail))
/-- info: 'Relay.the_signal_is_recovered' does not depend on any axioms -/
#guard_msgs in #print axioms the_signal_is_recovered
theorem the_erasing_stage_merges : met throughErase = met throughEraseOther ∧ signal ≠ otherSignal :=
by decide
/-- info: 'Relay.the_erasing_stage_merges' does not depend on any axioms -/
#guard_msgs in #print axioms the_erasing_stage_merges
theorem no_section_recovers_the_erased (r : List Bool → List Bool) (hr : ∀ s, r (erase s) = s) : False :=
a_merging_map_has_no_section erase (s := signal) (s' := otherSignal) (by decide) (by decide) r hr
/-- info: 'Relay.no_section_recovers_the_erased' does not depend on any axioms -/
#guard_msgs in #print axioms no_section_recovers_the_erased
theorem the_replayer_parks_the_word {I O : Type} (m : Machine.{0, 0, 0} I O) :
∀ (ws rec : List I), park (replayer m) rec ws = rec ++ ws :=
by
(intro x; induction x;
all_goals
(first
| (intros; (apply ((Room.the_append_rests _)).symm <;> fail))
| (rename_i ih; intros; exact (ih _).trans (by (apply Room.the_appends_regroup <;> fail)))))
/-- info: 'Relay.the_replayer_parks_the_word' does not depend on any axioms -/
#guard_msgs in #print axioms the_replayer_parks_the_word
theorem the_identity_relay_keeps_its_route (w : List Bool) :
behavior (replayer (ledger Bool)) w = behavior (ledger Bool) w ∧ park (replayer (ledger Bool)) [] w = w :=
⟨the_replay_is_the_machine (ledger Bool) w, the_replayer_parks_the_word (ledger Bool) w []⟩
/-- info: 'Relay.the_identity_relay_keeps_its_route' does not depend on any axioms -/
#guard_msgs in #print axioms the_identity_relay_keeps_its_route
end Relay