tape — a product as an assay, on Rest

19 receipts inline · 166 lines · pinned ce1b6d74f0e8af48 — shasum -a 256 of this file, cut to 16, as pins has it · lake env lean tape.lean prints nothing when every receipt passes

import Face
import Rest
open Room Face Rest
set_option autoImplicit false

namespace Tape

universe w

def tended : Machine Nat Nat := tend adder (0 : Nat) recordTheState

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

def taped : Machine Nat Nat := tape adder (0 : Nat) recordTheState readThrough

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

def untended : Nat := behavior adder [1, 1, 1]

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

def tendedRuns : Nat := behavior tended [1, 1, 1]

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

def tapedRuns : Nat := behavior taped [1, 1, 1]

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

def tapeAfterTwo : Nat := met (park tended (atTheDoor (0 : Nat) (0 : Nat)) [1, 1])

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

def stateAfterTwo : Nat := face (park tended (atTheDoor (0 : Nat) (0 : Nat)) [1, 1])

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

def unreadTape : Nat := behavior (tape adder (0 : Nat) recordTheState (fun _ i => i)) [1, 1, 1]

#guard untended == 3
#guard tendedRuns == 3
#guard tapedRuns == 4
#guard tapeAfterTwo == 1
#guard stateAfterTwo == 2
#guard unreadTape == untended

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

def rememberedAdder : Machine Nat Nat := remembering adder

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

def adderRemembers : List Nat := met (park rememberedAdder (atTheDoor (0 : Nat) ([] : List Nat)) [1, 1, 1])

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

def adderForgets : door Nat (List Nat) :=
  unstep adder (unstep adder (unstep adder (park rememberedAdder (atTheDoor (0 : Nat) ([] : List Nat)) [1, 1, 1])))

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

def rememberedRuns : Nat := behavior rememberedAdder [1, 1, 1]

#guard adderRemembers == [2, 1, 0]
#guard face adderForgets == 0
#guard met adderForgets == []
#guard rememberedRuns == untended

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

def visited {I O : Type} (m : Machine.{0, 0, w} I O) : m.S → List I → List m.S
  | _, [] => []
  | s, i :: u => s :: visited m (m.step s i) u

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

def backwards {A : Type w} : List A → List A
  | [] => []
  | x :: xs => backwards xs ++ [x]

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

def adderVisited : List Nat := visited adder (0 : Nat) [1, 1, 1]
#guard adderVisited == [0, 1, 2]
#guard adderRemembers == backwards adderVisited

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

theorem the_tape_is_the_route_reversed {I O : Type} (m : Machine.{0, 0, w} I O) :
    ∀ (u : List I) (s : m.S) (h : List m.S), met (park (remembering m) (atTheDoor s h) u) = backwards (visited m s u) ++ h
  | [], _, _ => rfl
  | i :: u, s, h => by
      show met (park (remembering m) (atTheDoor (m.step s i) (s :: h)) u) = (backwards (visited m (m.step s i) u) ++ [s]) ++ h
      rw [the_tape_is_the_route_reversed m u (m.step s i) (s :: h), the_appends_regroup]
      exact rfl

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

theorem a_wait_is_a_still_plan_on_its_own_tape {I O : Type} (R : Runner.{0, 0, w} I O) (hstill : ∀ s, R.m.step s (R.steer s) = s)
    (n : Nat) (s : R.m.S) (m : Machine.{0, 0, w} I O) (d : door m.S (List m.S)) (i : I) (u : List I) :
    runs R.m R.steer R.rest s n = cond (R.rest s) (some (R.m.out s)) none
      ∧ (readable R s ↔ R.rest s = true)
      ∧ unstep m ((remembering m).step d i) = d
      ∧ (met (park (remembering m) d u)).length = (met d).length + u.length :=
  ⟨a_still_runner_rests_where_it_stands R hstill n s, the_still_plan_is_readable_iff_at_rest R hstill s,
   the_remembering_step_retracts m d i, the_bill_is_the_word m u d⟩

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

theorem the_symmetry_is_over_the_guest (F : Face.{0, 0, 0}) {W : Type} (σ : door F.State W → W) (d : door F.State W)
    (s : F.State) {g g' : W} (hw : g ≠ g') {I O : Type} (m : Machine.{0, 0, w} I O) (u : List I) (d' : door m.S (List m.S)) :
    alike (host F W) (vertical σ d) d
      ∧ ¬ alike (widen F W) (atTheDoor s g) (atTheDoor s g')
      ∧ (met (park (remembering m) d' u)).length = (met d').length + u.length :=
  by
    (intros; (repeat' constructor);
      all_goals
        (intros;
          first
          | (apply Face.a_guest_mover_is_unheard <;> fail)
          | (apply Face.a_wider_seat_reads_the_remainder <;> assumption)
          | (apply Face.the_bill_is_the_word <;> fail)))

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

theorem the_horizon_radiates {I O : Type} {W : Type} (m : Machine.{0, 0, 0} I O) (w0 : W) (σ : door m.S W → W)
    (u : List I) (n : Machine.{0, 0, w} I O) (d : door n.S (List n.S)) (v : List I) :
    behavior (tend m w0 σ) u = behavior m u
      ∧ (behavior (tape adder (0 : Nat) recordTheState readThrough) [1, 1, 1] = (4 : Nat)
          ∧ behavior adder [1, 1, 1] = (3 : Nat) ∧ (4 : Nat) ≠ 3)
      ∧ (met (park (remembering n) d v)).length = (met d).length + v.length :=
  by
    (intros; (repeat' constructor);
      all_goals
        (intros;
          first
          | (apply Face.the_tending_is_unheard_at_the_gap <;> fail)
          |
            (apply Room.ne_of_beq_no <;>
                first
                | (apply Room.ble_refl <;> fail)
                | rfl)
          | (apply Face.the_bill_is_the_word <;> fail)))

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

end Tape

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 Tape["Tape"]
    a_wait_is_a_still_plan_on_its_own_tape["a_wait_is_a_still_plan_on_its_own_tape"]
    the_horizon_radiates["the_horizon_radiates"]
    the_symmetry_is_over_the_guest["the_symmetry_is_over_the_guest"]
    the_tape_is_the_route_reversed["the_tape_is_the_route_reversed"]
  end
  subgraph Face["Face"]
    Face_a_guest_mover_is_unheard["a_guest_mover_is_unheard"]
    Face_a_wider_seat_reads_the_remainder["a_wider_seat_reads_the_remainder"]
    Face_the_bill_is_the_word["the_bill_is_the_word"]
    Face_the_remembering_step_retracts["the_remembering_step_retracts"]
    Face_the_tending_is_unheard_at_the_gap["the_tending_is_unheard_at_the_gap"]
  end
  subgraph Rest["Rest"]
    Rest_a_still_runner_rests_where_it_stands["a_still_runner_rests_where_it_stands"]
    Rest_the_still_plan_is_readable_iff_at_rest["the_still_plan_is_readable_iff_at_rest"]
  end
  a_wait_is_a_still_plan_on_its_own_tape --> Face_the_bill_is_the_word
  a_wait_is_a_still_plan_on_its_own_tape --> Rest_the_still_plan_is_readable_iff_at_rest
  a_wait_is_a_still_plan_on_its_own_tape --> Rest_a_still_runner_rests_where_it_stands
  a_wait_is_a_still_plan_on_its_own_tape --> Face_the_remembering_step_retracts
  the_horizon_radiates --> Face_the_bill_is_the_word
  the_horizon_radiates --> Face_the_tending_is_unheard_at_the_gap
  the_symmetry_is_over_the_guest --> Face_the_bill_is_the_word
  the_symmetry_is_over_the_guest --> Face_a_wider_seat_reads_the_remainder
  the_symmetry_is_over_the_guest --> Face_a_guest_mover_is_unheard

tape — a product as an assay, on Rest

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)