Counter — the compiler's own conduct, grown from germ/Counter.lean
34 receipts inline · 242 lines · pinned 50eb093128ce9af0 — shasum -a 256 of this file, cut to 16, as pins has it · lake env lean Counter.lean prints nothing when every receipt passes
import Face
import Rest
open Room Face Rest
set_option autoImplicit false
universe u v w
namespace Counter
def sighting : Type := Nat × List Nat
/-- info: 'Counter.sighting' does not depend on any axioms -/
#guard_msgs in #print axioms sighting
def room : Type := List Nat × List sighting
/-- info: 'Counter.room' does not depend on any axioms -/
#guard_msgs in #print axioms room
def empty : room := ([], [])
/-- info: 'Counter.empty' does not depend on any axioms -/
#guard_msgs in #print axioms empty
def offer (st : room) (a : sighting) : room := welcome Nat.beq st a
/-- info: 'Counter.offer' does not depend on any axioms -/
#guard_msgs in #print axioms offer
def round (st : room) (w : List sighting) : room := intake Nat.beq st w
/-- info: 'Counter.round' does not depend on any axioms -/
#guard_msgs in #print axioms round
def seated (st : room) (n : Nat) : Bool := enrolled Nat.beq st.1 n
/-- info: 'Counter.seated' does not depend on any axioms -/
#guard_msgs in #print axioms seated
def weight (st : room) (needs : List Nat) : Nat := lacking Nat.beq st.1 needs
/-- info: 'Counter.weight' does not depend on any axioms -/
#guard_msgs in #print axioms weight
def shadow {S B A : Type u} (read : B → List A) (t : List (S × B)) : List (S × List A) :=
t.map (fun o => (o.1, read o.2))
/-- info: 'Counter.shadow' does not depend on any axioms -/
#guard_msgs in #print axioms shadow
def gateFace (S B A : Type u) (read : B → List A) : Face :=
⟨List (S × B), Unit, List (S × List A), fun t _ => shadow read t⟩
/-- info: 'Counter.gateFace' does not depend on any axioms -/
#guard_msgs in #print axioms gateFace
def conductive {S A : Type u} : List (S × List A) → Bool
| [] => true
| r :: rs => r.2.isEmpty && conductive rs
/-- info: 'Counter.conductive' does not depend on any axioms -/
#guard_msgs in #print axioms conductive
def gate {S B A : Type u} (read : B → List A) (t : List (S × B)) : Bool :=
conductive (shadow read t)
/-- info: 'Counter.gate' does not depend on any axioms -/
#guard_msgs in #print axioms gate
def rebody {S B : Type u} (m : B → B) (t : List (S × B)) : List (S × B) :=
t.map (fun o => (o.1, m o.2))
/-- info: 'Counter.rebody' does not depend on any axioms -/
#guard_msgs in #print axioms rebody
def sweep (st : room) : room := round (st.1, []) st.2
/-- info: 'Counter.sweep' does not depend on any axioms -/
#guard_msgs in #print axioms sweep
def settled (st : room) : Bool := Nat.beq (sweep st).1.length st.1.length
/-- info: 'Counter.settled' does not depend on any axioms -/
#guard_msgs in #print axioms settled
def cascade : Runner Unit room := ⟨⟨room, empty, fun st _ => sweep st, fun st => st⟩, fun _ => (), settled⟩
/-- info: 'Counter.cascade' does not depend on any axioms -/
#guard_msgs in #print axioms cascade
theorem a_name_reads_itself (y : Nat) : Nat.beq y y = true :=
(by (apply Room.beq_self <;> fail))
/-- info: 'Counter.a_name_reads_itself' does not depend on any axioms -/
#guard_msgs in #print axioms a_name_reads_itself
theorem the_first_sighting_is_free (st : room) (n : Nat) : offer st (n, []) = (n :: st.1, st.2) :=
(by (apply Room.the_backed_are_seated <;> rfl))
/-- info: 'Counter.the_first_sighting_is_free' does not depend on any axioms -/
#guard_msgs in #print axioms the_first_sighting_is_free
theorem a_backed_sighting_seats (st : room) (a : sighting) (hb : backed Nat.beq st.1 a.2 = true) :
offer st a = (a.1 :: st.1, st.2) :=
(by (apply Room.the_backed_are_seated <;> assumption))
/-- info: 'Counter.a_backed_sighting_seats' does not depend on any axioms -/
#guard_msgs in #print axioms a_backed_sighting_seats
theorem an_unbacked_sighting_waits (st : room) (a : sighting) (hb : backed Nat.beq st.1 a.2 = false) :
offer st a = (st.1, a :: st.2) :=
(by (apply Room.the_unbacked_wait <;> assumption))
/-- info: 'Counter.an_unbacked_sighting_waits' does not depend on any axioms -/
#guard_msgs in #print axioms an_unbacked_sighting_waits
theorem the_seated_stay_seated (st : room) (a : sighting) (n : Nat) (h : seated st n = true) :
seated (offer st a) n = true :=
(by (apply Room.the_enrolled_stay_enrolled <;> assumption))
/-- info: 'Counter.the_seated_stay_seated' does not depend on any axioms -/
#guard_msgs in #print axioms the_seated_stay_seated
theorem the_held_name_what_they_wait_on (st : room) (needs : List Nat)
(h : backed Nat.beq st.1 needs = false) : ∃ n, n ∈ needs ∧ seated st n = false :=
(by (apply Room.the_held_name_their_darkness <;> assumption))
/-- info: 'Counter.the_held_name_what_they_wait_on' does not depend on any axioms -/
#guard_msgs in #print axioms the_held_name_what_they_wait_on
theorem weight_zero_is_backed (st : room) (needs : List Nat) :
weight st needs = 0 ↔ backed Nat.beq st.1 needs = true :=
(by (apply Room.the_weight_is_zero_at_the_door <;> fail))
/-- info: 'Counter.weight_zero_is_backed' does not depend on any axioms -/
#guard_msgs in #print axioms weight_zero_is_backed
theorem a_sighting_that_cites_only_itself_never_seats (x : Nat) (w : List sighting) (st : room)
(hd : seated st x = false) (hs : ∀ a, a ∈ w → Nat.beq a.1 x = true → x ∈ a.2) :
seated (round st w) x = false :=
(by (apply Room.no_mark_lights_itself <;> assumption))
/-- info: 'Counter.a_sighting_that_cites_only_itself_never_seats' does not depend on any axioms -/
#guard_msgs in #print axioms a_sighting_that_cites_only_itself_never_seats
theorem two_sightings_that_cite_each_other_stay_dark (x y : Nat) (w : List sighting) (st : room)
(hx : seated st x = false) (hy : seated st y = false)
(hcx : ∀ a, a ∈ w → Nat.beq a.1 x = true → y ∈ a.2)
(hcy : ∀ a, a ∈ w → Nat.beq a.1 y = true → x ∈ a.2) :
seated (round st w) x = false ∧ seated (round st w) y = false :=
(by (apply Room.the_circle_stays_dark <;> assumption))
/-- info: 'Counter.two_sightings_that_cite_each_other_stay_dark' does not depend on any axioms -/
#guard_msgs in #print axioms two_sightings_that_cite_each_other_stay_dark
theorem the_key_is_cut_from_the_room (st : room) (needs : List Nat) (h : weight st needs = 1) :
∃ k, k ∈ needs ∧ seated st k = false ∧ backed Nat.beq (k :: st.1) needs = true :=
(by
(apply Room.the_key_is_cut_from_the_room <;>
first
| (apply Room.beq_self <;> fail)
| assumption))
/-- info: 'Counter.the_key_is_cut_from_the_room' does not depend on any axioms -/
#guard_msgs in #print axioms the_key_is_cut_from_the_room
theorem the_gate_hears_only_the_receipt {S B A : Type u} (read : B → List A) :
Derived (gateFace S B A read) (fun t => gate read t = true) :=
a_role_read_at_a_probe_is_derived (gateFace S B A read) () (fun rs => conductive rs = true)
/-- info: 'Counter.the_gate_hears_only_the_receipt' does not depend on any axioms -/
#guard_msgs in #print axioms the_gate_hears_only_the_receipt
theorem the_shadow_survives_a_receipt_keeping_rebody {S B A : Type u} (read : B → List A) (m : B → B)
(h : ∀ b, read (m b) = read b) : ∀ t : List (S × B), shadow read (rebody m t) = shadow read t
| [] => rfl
| o :: t => by
show (o.1, read (m o.2)) :: shadow read (rebody m t) = (o.1, read o.2) :: shadow read t
rw [h o.2, the_shadow_survives_a_receipt_keeping_rebody read m h t]
/-- info: 'Counter.the_shadow_survives_a_receipt_keeping_rebody' does not depend on any axioms -/
#guard_msgs in #print axioms the_shadow_survives_a_receipt_keeping_rebody
theorem the_gate_reads_no_body {S B A : Type u} (read : B → List A) (t t' : List (S × B))
(h : shadow read t = shadow read t') : gate read t = gate read t' :=
congrArg conductive h
/-- info: 'Counter.the_gate_reads_no_body' does not depend on any axioms -/
#guard_msgs in #print axioms the_gate_reads_no_body
theorem the_vow_is_the_empty_receipt {S A : Type u} :
∀ rs : List (S × List A), conductive rs = true → ∀ r, r ∈ rs → r.2 = []
| [], _, _, h => nomatch h
| (_, []) :: rs, hc, r, hr => by
cases hr with
| head => rfl
| tail _ h' => exact the_vow_is_the_empty_receipt rs hc r h'
| (_, _ :: _) :: _, hc, _, _ => by
have h : false = true := hc
exact nomatch h
/-- info: 'Counter.the_vow_is_the_empty_receipt' does not depend on any axioms -/
#guard_msgs in #print axioms the_vow_is_the_empty_receipt
theorem a_rest_is_drained_or_stuck (st : room) (h : settled st = true) :
∀ a, a ∈ st.2 → backed Nat.beq st.1 a.2 = false :=
a_sweep_that_seats_no_one_waited_everyone Nat.beq st.2 (st.1, []) (eq_of_beq _ _ h)
/-- info: 'Counter.a_rest_is_drained_or_stuck' does not depend on any axioms -/
#guard_msgs in #print axioms a_rest_is_drained_or_stuck
theorem the_cascade_and_its_record_rest_alike : alike (haltingGap Unit room) cascade (replayRunner cascade) :=
(by (apply Rest.the_record_rests_where_the_machine_rests <;> fail))
/-- info: 'Counter.the_cascade_and_its_record_rest_alike' does not depend on any axioms -/
#guard_msgs in #print axioms the_cascade_and_its_record_rest_alike
theorem a_sighting_is_load_bearing_in_the_same_round (st : room) (a : sighting)
(hb : backed Nat.beq st.1 a.2 = true) : seated (offer st a) a.1 = true :=
(by
(apply Room.the_seat_is_load_bearing_in_the_same_click <;>
first
| (apply a_name_reads_itself <;> fail)
| assumption))
/-- info: 'Counter.a_sighting_is_load_bearing_in_the_same_round' does not depend on any axioms -/
#guard_msgs in #print axioms a_sighting_is_load_bearing_in_the_same_round
theorem a_receipt_keeping_rebody_is_unheard {S B A : Type u} (read : B → List A) (m : B → B)
(h : ∀ b, read (m b) = read b) : unheard (gateFace S B A read) (rebody m) :=
by (intro _ y; induction y; all_goals ((intros; (apply the_shadow_survives_a_receipt_keeping_rebody <;> assumption))))
/-- info: 'Counter.a_receipt_keeping_rebody_is_unheard' does not depend on any axioms -/
#guard_msgs in #print axioms a_receipt_keeping_rebody_is_unheard
theorem the_verdict_survives_the_rebody {S B A : Type u} (read : B → List A) (m : B → B)
(h : ∀ b, read (m b) = read b) (t : List (S × B)) : gate read (rebody m t) = gate read t :=
(by (apply the_gate_reads_no_body <;> (apply the_shadow_survives_a_receipt_keeping_rebody <;> assumption)))
/-- info: 'Counter.the_verdict_survives_the_rebody' does not depend on any axioms -/
#guard_msgs in #print axioms the_verdict_survives_the_rebody
end Counter