Seek — the compiler's search, grown from germ/Seek.lean

11 receipts inline · 106 lines · pinned 7746a94afc19b5f1 — shasum -a 256 of this file, cut to 16, as pins has it · lake env lean Seek.lean prints nothing when every receipt passes

import Face
open Room Face

namespace Seek

def seeker (close : Nat → Bool) : Machine Nat (List Nat) :=
  ⟨List Nat, [], fun t m => cond (close m) (t ++ [m]) t, fun t => t⟩

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

def replay (close : Nat → Bool) : Machine Nat (List Nat) :=
  replayer (seeker close)

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

theorem a_failed_move_leaves_no_trace (close : Nat → Bool) (t : List Nat) (m : Nat)
    (h : close m = false) : park (seeker close) t [m] = t :=
  by (intros; (try dsimp only [seeker, Face.park] at *); intros; (rw [h]; rfl))

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

theorem a_closing_move_is_recorded (close : Nat → Bool) (t : List Nat) (m : Nat)
    (h : close m = true) : park (seeker close) t [m] = t ++ [m] :=
  by (intros; (try dsimp only [seeker, Face.park] at *); intros; (rw [h]; rfl))

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

theorem the_trace_is_the_closing_moves (close : Nat → Bool) :
    ∀ (w t : List Nat), park (seeker close) t w = t ++ w.filter close
  | [], t => (the_append_rests t).symm
  | m :: w, t => by
      show park (seeker close) (cond (close m) (t ++ [m]) t) w = t ++ List.filter close (m :: w)
      cases h : close m with
      | true =>
          show park (seeker close) (t ++ [m]) w = t ++ List.filter close (m :: w)
          rw [the_trace_is_the_closing_moves close w (t ++ [m]), the_appends_regroup]
          show t ++ (m :: List.filter close w) = t ++ List.filter close (m :: w)
          rw [List.filter, h]
      | false =>
          show park (seeker close) t w = t ++ List.filter close (m :: w)
          rw [the_trace_is_the_closing_moves close w t]
          show t ++ List.filter close w = t ++ List.filter close (m :: w)
          rw [List.filter, h]

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

theorem the_replay_is_the_search (close : Nat → Bool) (w : List Nat) :
    behavior (replay close) w = behavior (seeker close) w :=
  (by (apply Face.the_replay_is_the_machine <;> fail))

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

theorem the_search_is_the_replay (close : Nat → Bool) (w : List Nat) :
    behavior (seeker close) w = behavior (replay close) w :=
  (by (apply ((Face.the_replay_is_the_machine _ _)).symm <;> fail))

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

theorem the_audition_cannot_part_them (close : Nat → Bool) :
    ∀ q, sound (airGap Nat (List Nat)) (seeker close) q = sound (airGap Nat (List Nat)) (replay close) q :=
  by
    (intro x; induction x;
      all_goals
        (first
          | (intros; rfl)
          |
            (intros;
              (apply ((Face.the_interview_crosses_the_carrier _ _ _ _ _ _)).symm <;>
                  (apply Face.the_replay_is_the_machine <;> fail)))))

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

theorem the_search_starts_empty (close : Nat → Bool) : (seeker close).s0 = [] :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

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

theorem the_search_and_its_replay_are_alike (close : Nat → Bool) :
    alike (airGap Nat (List Nat)) (seeker close) (replay close) :=
  by
    (intro x; induction x;
      all_goals
        (first
          | (intros; rfl)
          | (intros; (apply ((the_replay_is_the_search _ _)).symm <;> fail))))

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

theorem the_search_has_no_memory (close : Nat → Bool) (w : List Nat) :
    behavior (seeker close) w = w.filter close :=
  (by (apply the_trace_is_the_closing_moves <;> fail))

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

end Seek

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 Seek["Seek"]
    a_closing_move_is_recorded["a_closing_move_is_recorded"]
    a_failed_move_leaves_no_trace["a_failed_move_leaves_no_trace"]
    the_audition_cannot_part_them["the_audition_cannot_part_them"]
    the_replay_is_the_search["the_replay_is_the_search"]
    the_search_and_its_replay_are_alike["the_search_and_its_replay_are_alike"]
    the_search_has_no_memory["the_search_has_no_memory"]
    the_search_is_the_replay["the_search_is_the_replay"]
    the_search_starts_empty["the_search_starts_empty"]
    the_trace_is_the_closing_moves["the_trace_is_the_closing_moves"]
  end
  subgraph Face["Face"]
    Face_the_interview_crosses_the_carrier["the_interview_crosses_the_carrier"]
    Face_the_replay_is_the_machine["the_replay_is_the_machine"]
  end
  the_search_has_no_memory --> the_trace_is_the_closing_moves
  the_replay_is_the_search --> Face_the_replay_is_the_machine
  the_search_and_its_replay_are_alike --> the_replay_is_the_search
  the_search_is_the_replay --> Face_the_replay_is_the_machine
  the_audition_cannot_part_them --> Face_the_interview_crosses_the_carrier
  the_audition_cannot_part_them --> Face_the_replay_is_the_machine