Threshold — where Rest and Witness meet, grown from germ/Threshold.lean

8 receipts inline · 104 lines · pinned f7da54dac965a650 — shasum -a 256 of this file, cut to 16, as pins has it · lake env lean Threshold.lean prints nothing when every receipt passes

import Rest
import Witness
open Room Face Rest Witness

namespace Threshold

universe u v w u' v' w' u''

def threshold (F : Face) (seats : List (List F.Probe)) {I : Type u'} {O : Type v'} (R : Runner.{u', v', w'} I O)
    (s : R.m.S) : Prop :=
  covers F seats ∧ R.rest s = true

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

def thresholdAt (F : Face) (ps : List F.Probe) (seats : List (List F.Probe)) {I : Type u'} {O : Type v'}
    (R : Runner.{u', v', w'} I O) (s : R.m.S) : Prop :=
  coversAll F ps seats ∧ R.rest s = true

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

theorem the_crossing_is_licensed (F : Face) {seats : List (List F.Probe)} {x y : F.State}
    (hc : covers F seats) (hw : witnessed F seats x y) {W : Type v'} (w w' : W) :
    alike (host F W) (atTheDoor x w) (atTheDoor y w') :=
  (by (apply Witness.forever_hold_your_peace <;> assumption))

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

theorem the_threshold {I : Type u'} (F : Face.{u, v, w}) (seats : List (List F.Probe))
    (R : Runner.{u', u, w'} I F.State) (s : R.m.S) (t : threshold F seats R s)
    {W : Type u} (w w' : W) (sl : List F.Probe) :
    alike (host F W) (atTheDoor (R.m.out s) w) (atTheDoor (R.m.out s) w')
      ∧ reads (host F W) sl (atTheDoor (R.m.out s) w) = reads F sl (R.m.out s)
      ∧ (∀ y, witnessed F seats (R.m.out s) y → alike F (R.m.out s) y)
      ∧ runs R.m R.steer R.rest s 0 = some (R.m.out s) :=
  ⟨the_host_merges_the_guests F W (R.m.out s) w w',
    (by (apply Witness.the_word_at_the_door_is_unread_at_every_seat <;> assumption)), fun _ hw =>
    (by
      (apply Witness.forever_hold_your_peace <;>
          first
          | (apply ((t)).1 <;> fail)
          | assumption)),
    by
    show cond (R.rest s) (some (R.m.out s)) none = some (R.m.out s)
    rw [t.2]
    rfl⟩

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

theorem the_route_is_shed {I : Type u} {O : Type v} (R : Runner.{u, v, u} I O) :
    alike (haltingGap.{u, v, u} I O) R (replayRunner R) :=
  by (intro x; induction x; all_goals ((intros; (apply Rest.the_record_rests_where_the_machine_rests <;> fail))))

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

theorem the_crossing_is_licensed_at_the_room (F : Face) (ps : List F.Probe) {seats : List (List F.Probe)}
    {x y : F.State} (hc : coversAll F ps seats) (hw : witnessed F seats x y) {W : Type v'} (w w' : W) :
    reads (host F W) ps (atTheDoor x w) = reads (host F W) ps (atTheDoor y w') :=
  (by (apply Witness.the_room_at_its_probes_reads_alike <;> assumption))

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

theorem the_threshold_at_the_room {I : Type u'} (F : Face.{u, v, w}) (ps : List F.Probe) (seats : List (List F.Probe))
    (R : Runner.{u', u, w'} I F.State) (s : R.m.S) (t : thresholdAt F ps seats R s)
    {W : Type u} (w w' : W) (sl : List F.Probe) :
    alike (host F W) (atTheDoor (R.m.out s) w) (atTheDoor (R.m.out s) w')
      ∧ reads (host F W) sl (atTheDoor (R.m.out s) w) = reads F sl (R.m.out s)
      ∧ (∀ y, witnessed F seats (R.m.out s) y → reads F ps (R.m.out s) = reads F ps y)
      ∧ runs R.m R.steer R.rest s 0 = some (R.m.out s) :=
  ⟨the_host_merges_the_guests F W (R.m.out s) w w',
    (by (apply Witness.the_word_at_the_door_is_unread_at_every_seat <;> assumption)), fun _ hw =>
    (by
      (apply Witness.the_room_at_its_probes_reads_alike <;>
          first
          | (apply ((t)).1 <;> fail)
          | assumption)),
    by
    show cond (R.rest s) (some (R.m.out s)) none = some (R.m.out s)
    rw [t.2]
    rfl⟩

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

theorem a_threshold_is_a_threshold_at_every_room (F : Face) (ps : List F.Probe) (seats : List (List F.Probe))
    {I : Type u'} {O : Type v'} (R : Runner.{u', v', w'} I O) (s : R.m.S) (t : threshold F seats R s) :
    thresholdAt F ps seats R s :=
  by
    (intros; (repeat' constructor);
      all_goals
        (intros;
          first
          | (apply Witness.a_cover_of_the_room_covers_its_probes <;> (apply ((t)).1 <;> fail))
          | (apply ((t)).2 <;> fail)))

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

end Threshold

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 Threshold["Threshold"]
    a_threshold_is_a_threshold_at_every_room["a_threshold_is_a_threshold_at_every_room"]
    the_crossing_is_licensed["the_crossing_is_licensed"]
    the_crossing_is_licensed_at_the_room["the_crossing_is_licensed_at_the_room"]
    the_route_is_shed["the_route_is_shed"]
    the_threshold["the_threshold"]
    the_threshold_at_the_room["the_threshold_at_the_room"]
  end
  subgraph Rest["Rest"]
    Rest_the_record_rests_where_the_machine_rests["the_record_rests_where_the_machine_rests"]
  end
  subgraph Witness["Witness"]
    Witness_a_cover_of_the_room_covers_its_probes["a_cover_of_the_room_covers_its_probes"]
    Witness_forever_hold_your_peace["forever_hold_your_peace"]
    Witness_the_room_at_its_probes_reads_alike["the_room_at_its_probes_reads_alike"]
    Witness_the_word_at_the_door_is_unread_at_every_seat["the_word_at_the_door_is_unread_at_every_seat"]
  end
  the_route_is_shed --> Rest_the_record_rests_where_the_machine_rests
  the_threshold_at_the_room --> Witness_the_room_at_its_probes_reads_alike
  the_threshold_at_the_room --> Witness_the_word_at_the_door_is_unread_at_every_seat
  the_threshold --> Witness_the_word_at_the_door_is_unread_at_every_seat
  the_threshold --> Witness_forever_hold_your_peace
  the_crossing_is_licensed --> Witness_forever_hold_your_peace
  the_crossing_is_licensed_at_the_room --> Witness_the_room_at_its_probes_reads_alike
  a_threshold_is_a_threshold_at_every_room --> Witness_a_cover_of_the_room_covers_its_probes