Witness — the witnessing, a species beside the storeys, grown from germ/Witness.lean
37 receipts inline · 330 lines · pinned 234e5775d27994fa — shasum -a 256 of this file, cut to 16, as pins has it · lake env lean Witness.lean prints nothing when every receipt passes
import Face
open Room Face
namespace Witness
universe u v w
def seat (F : Face) : Type v := List F.Probe
/-- info: 'Witness.seat' does not depend on any axioms -/
#guard_msgs in #print axioms seat
def reads (F : Face) (s : List F.Probe) (x : F.State) : List F.Ans :=
s.map (F.obs x)
/-- info: 'Witness.reads' does not depend on any axioms -/
#guard_msgs in #print axioms reads
def witnessFace (F : Face) : Face := ⟨F.State, List F.Probe, List F.Ans, fun x s => reads F s x⟩
/-- info: 'Witness.witnessFace' does not depend on any axioms -/
#guard_msgs in #print axioms witnessFace
def hears (F : Face) (s : List F.Probe) (p : F.Probe) : Prop := p ∈ s
/-- info: 'Witness.hears' does not depend on any axioms -/
#guard_msgs in #print axioms hears
def witnessed (F : Face) (seats : List (List F.Probe)) (x y : F.State) : Prop :=
∀ s, s ∈ seats → reads F s x = reads F s y
/-- info: 'Witness.witnessed' does not depend on any axioms -/
#guard_msgs in #print axioms witnessed
def earshot (F : Face) (seats : List (List F.Probe)) : List F.Probe :=
joinMap (fun s => s) seats
/-- info: 'Witness.earshot' does not depend on any axioms -/
#guard_msgs in #print axioms earshot
def covers (F : Face) (seats : List (List F.Probe)) : Prop :=
∀ q, q ∈ earshot F seats
/-- info: 'Witness.covers' does not depend on any axioms -/
#guard_msgs in #print axioms covers
def dark (F : Face) (seats : List (List F.Probe)) (x y : F.State) : Prop :=
∀ q, q ∈ earshot F seats → F.obs x q = F.obs y q
/-- info: 'Witness.dark' does not depend on any axioms -/
#guard_msgs in #print axioms dark
def coversAll (F : Face) (ps : List F.Probe) (seats : List (List F.Probe)) : Prop :=
∀ q, q ∈ ps → q ∈ earshot F seats
/-- info: 'Witness.coversAll' does not depend on any axioms -/
#guard_msgs in #print axioms coversAll
theorem the_alike_read_alike (F : Face) {x y : F.State} (h : alike F x y) :
∀ s : List F.Probe, reads F s x = reads F s y :=
by
(intro x; induction x;
all_goals
(first
| (intros; rfl)
| (intros; (apply Room.map_congr_mem <;> (intros; apply h <;> fail)))))
/-- info: 'Witness.the_alike_read_alike' does not depend on any axioms -/
#guard_msgs in #print axioms the_alike_read_alike
theorem a_wall_hides_the_probe (F : Face) {x y : F.State} {p : F.Probe} (h : differOnly F x y p) :
∀ s : List F.Probe, ¬ hears F s p → reads F s x = reads F s y
| [], _ => rfl
| q :: s, hn => by
show F.obs x q :: reads F s x = F.obs y q :: reads F s y
rw [h q (fun hq => hn (hq ▸ List.Mem.head s)),
a_wall_hides_the_probe F h s (fun hs => hn (List.Mem.tail q hs))]
/-- info: 'Witness.a_wall_hides_the_probe' does not depend on any axioms -/
#guard_msgs in #print axioms a_wall_hides_the_probe
theorem a_narrower_seat_reads_no_more (F : Face) {x y : F.State} (s : List F.Probe)
(h : ∀ q, q ∈ s → F.obs x q = F.obs y q) : reads F s x = reads F s y :=
(by (apply Room.map_congr_mem <;> assumption))
/-- info: 'Witness.a_narrower_seat_reads_no_more' does not depend on any axioms -/
#guard_msgs in #print axioms a_narrower_seat_reads_no_more
theorem the_probe_reads_the_seat (F : Face) {x y : F.State} {q : F.Probe} :
∀ s : List F.Probe, q ∈ s → reads F s x = reads F s y → F.obs x q = F.obs y q
| p :: s, hq, he => by
cases hq with
| head => exact the_first_mark_reads he
| tail _ hs => exact the_probe_reads_the_seat F s hs (the_rest_reads he)
/-- info: 'Witness.the_probe_reads_the_seat' does not depend on any axioms -/
#guard_msgs in #print axioms the_probe_reads_the_seat
theorem the_seat_that_hears_it_reads_it (F : Face) {x y : F.State} {p : F.Probe}
(hp : F.obs x p ≠ F.obs y p) : ∀ s : List F.Probe, hears F s p → reads F s x ≠ reads F s y
| q :: s, hq => fun he => by
cases hq with
| head => exact hp (the_first_mark_reads he)
| tail _ hs =>
exact the_seat_that_hears_it_reads_it F hp s hs (the_rest_reads he)
/-- info: 'Witness.the_seat_that_hears_it_reads_it' does not depend on any axioms -/
#guard_msgs in #print axioms the_seat_that_hears_it_reads_it
theorem the_witness_parts_what_the_face_parts (F : Face) {x y : F.State}
(h : alike (witnessFace F) x y) : alike F x y :=
fun p => the_first_mark_reads (h [p])
/-- info: 'Witness.the_witness_parts_what_the_face_parts' does not depend on any axioms -/
#guard_msgs in #print axioms the_witness_parts_what_the_face_parts
theorem the_sounding_is_the_trails_reading (F : Face) (s : F.State) :
∀ q : Interview F.Probe F.Ans, sound F s q = reads F (trail F s q) s :=
by
(intro x; induction x;
all_goals
(first
| (intros; rfl)
| (rename_i ih; intros; exact congrArg _ (ih _))))
/-- info: 'Witness.the_sounding_is_the_trails_reading' does not depend on any axioms -/
#guard_msgs in #print axioms the_sounding_is_the_trails_reading
theorem a_dark_probe_is_out_of_earshot (F : Face) (seats : List (List F.Probe)) (p : F.Probe)
(h : ∀ s, s ∈ seats → ¬ hears F s p) : ¬ p ∈ earshot F seats :=
fun hp => match mem_joinMap_back seats hp with
| ⟨s, hs, hps⟩ => h s hs hps
/-- info: 'Witness.a_dark_probe_is_out_of_earshot' does not depend on any axioms -/
#guard_msgs in #print axioms a_dark_probe_is_out_of_earshot
theorem out_of_earshot_is_dark (F : Face) (seats : List (List F.Probe)) (p : F.Probe)
(h : ¬ p ∈ earshot F seats) : ∀ s, s ∈ seats → ¬ hears F s p :=
fun _ hs hps => h (mem_joinMap_intro hs hps)
/-- info: 'Witness.out_of_earshot_is_dark' does not depend on any axioms -/
#guard_msgs in #print axioms out_of_earshot_is_dark
theorem the_ceremony_reseats_every_reading (F : Face) {W : Type w} (s : List F.Probe) (x : F.State) (w : W) :
reads (host F W) s (atTheDoor x w) = reads F s x :=
by (intros; (repeat' constructor); all_goals (intros; fail))
/-- info: 'Witness.the_ceremony_reseats_every_reading' does not depend on any axioms -/
#guard_msgs in #print axioms the_ceremony_reseats_every_reading
theorem the_word_at_the_door_is_unread_at_every_seat (F : Face) {W : Type w} (s : List F.Probe) (x : F.State)
(w w' : W) : reads (host F W) s (atTheDoor x w) = reads (host F W) s (atTheDoor x w') :=
by (intros; (repeat' constructor); all_goals (intros; fail))
/-- info: 'Witness.the_word_at_the_door_is_unread_at_every_seat' does not depend on any axioms -/
#guard_msgs in #print axioms the_word_at_the_door_is_unread_at_every_seat
theorem a_word_hidden_in_the_body_is_unheard_in_the_narration (F : Face) {B : Type w} (g : F.Ans → B)
{x y : F.State} {p : F.Probe} (h : differOnly F x y p) (hp : g (F.obs x p) = g (F.obs y p))
(dec : ∀ q : F.Probe, q = p ∨ q ≠ p) : alike (retell F g) x y :=
fun q => match dec q with
| Or.inl hq => by rw [hq]; exact hp
| Or.inr hq => by show g (F.obs x q) = g (F.obs y q); rw [h q hq]
/-- info: 'Witness.a_word_hidden_in_the_body_is_unheard_in_the_narration' does not depend on any axioms -/
#guard_msgs in #print axioms a_word_hidden_in_the_body_is_unheard_in_the_narration
theorem the_witness_is_a_face (F : Face) {x y : F.State} (h : alike F x y) :
alike (witnessFace F) x y :=
fun p => (by (apply Room.map_congr_mem <;> (intros; apply h <;> fail)))
/-- info: 'Witness.the_witness_is_a_face' does not depend on any axioms -/
#guard_msgs in #print axioms the_witness_is_a_face
theorem a_seat_over_a_seat_is_derived (F : Face) (s : List F.Probe) {A : Type u} (g : List F.Ans → A)
(v : A) : Derived F (fun x => g (reads F s x) = v) :=
by
(intros; (try dsimp only [reads, Face.Derived, Face.Face] at *); intros;
(rw [Room.map_congr_mem];
(intros; apply Face.the_sounding_reads_the_alike <;> (apply Face.no_interview_parts_the_alike <;> assumption))))
/-- info: 'Witness.a_seat_over_a_seat_is_derived' does not depend on any axioms -/
#guard_msgs in #print axioms a_seat_over_a_seat_is_derived
theorem a_wider_cone_reads_no_less (F : Face) (s : List F.Probe) (seats : List (List F.Probe)) {x y : F.State}
(hw : witnessed F (s :: seats) x y) : witnessed F seats x y :=
fun t ht => hw t (List.Mem.tail s ht)
/-- info: 'Witness.a_wider_cone_reads_no_less' does not depend on any axioms -/
#guard_msgs in #print axioms a_wider_cone_reads_no_less
theorem a_cover_of_the_room_covers_its_probes (F : Face) (ps : List F.Probe) (seats : List (List F.Probe))
(hc : covers F seats) : coversAll F ps seats :=
by (intro _ y; induction y; all_goals ((intros; (apply hc <;> fail))))
/-- info: 'Witness.a_cover_of_the_room_covers_its_probes' does not depend on any axioms -/
#guard_msgs in #print axioms a_cover_of_the_room_covers_its_probes
theorem a_room_covers_itself_at_one_seat (F : Face) (ps : List F.Probe) : coversAll F ps [ps] :=
fun p =>
(by
(intros;
apply Room.mem_joinMap_intro <;>
first
| exact List.Mem.head _
| assumption))
/-- info: 'Witness.a_room_covers_itself_at_one_seat' does not depend on any axioms -/
#guard_msgs in #print axioms a_room_covers_itself_at_one_seat
theorem the_room_is_the_widest_seat (F : Face) (s : List F.Probe) (x y : F.State)
(h : reads F s x ≠ reads F s y) : ¬ alike F x y :=
fun p => (by (apply h <;> (apply the_alike_read_alike <;> assumption)))
/-- info: 'Witness.the_room_is_the_widest_seat' does not depend on any axioms -/
#guard_msgs in #print axioms the_room_is_the_widest_seat
theorem speak_now (F : Face) {seats : List (List F.Probe)} {x y : F.State}
(hw : witnessed F seats x y) : ∀ q, q ∈ earshot F seats → F.obs x q = F.obs y q := by
intro q hq
obtain ⟨s, hs, hqs⟩ := mem_joinMap_back seats hq
exact the_probe_reads_the_seat F s hqs (hw s hs)
/-- info: 'Witness.speak_now' does not depend on any axioms -/
#guard_msgs in #print axioms speak_now
theorem a_wall_at_the_witness (F : Face) {x y : F.State} {p : F.Probe} (h : differOnly F x y p)
(s : List F.Probe) (hs : ¬ hears F s p) : (witnessFace F).obs x s = (witnessFace F).obs y s :=
(by (apply a_wall_hides_the_probe <;> assumption))
/-- info: 'Witness.a_wall_at_the_witness' does not depend on any axioms -/
#guard_msgs in #print axioms a_wall_at_the_witness
theorem a_probe_no_seat_hears_is_dark (F : Face) {x y : F.State} {p : F.Probe} (h : differOnly F x y p)
(seats : List (List F.Probe)) (hd : ∀ s, s ∈ seats → ¬ hears F s p) : witnessed F seats x y :=
by
(intro x; induction x;
all_goals
(first
| (intros; rfl)
|
(intros;
(apply a_wall_hides_the_probe <;>
first
| assumption
| (apply hd <;> assumption)))))
/-- info: 'Witness.a_probe_no_seat_hears_is_dark' does not depend on any axioms -/
#guard_msgs in #print axioms a_probe_no_seat_hears_is_dark
theorem the_narration_reads_alike_at_every_seat (F : Face) {B : Type w} (g : F.Ans → B)
{x y : F.State} {p : F.Probe} (h : differOnly F x y p) (hp : g (F.obs x p) = g (F.obs y p))
(dec : ∀ q : F.Probe, q = p ∨ q ≠ p) (s : List F.Probe) :
reads (retell F g) s x = reads (retell F g) s y :=
(by (apply the_alike_read_alike <;> (apply a_word_hidden_in_the_body_is_unheard_in_the_narration <;> assumption)))
/-- info: 'Witness.the_narration_reads_alike_at_every_seat' does not depend on any axioms -/
#guard_msgs in #print axioms the_narration_reads_alike_at_every_seat
theorem a_difference_out_of_the_cone_is_dark (F : Face) (seats : List (List F.Probe)) {x y : F.State} {p : F.Probe}
(h : differOnly F x y p) (hp : ¬ p ∈ earshot F seats) : witnessed F seats x y :=
by
(intro x; induction x;
all_goals
(first
| (intros; rfl)
|
(intros;
(apply a_wall_hides_the_probe <;>
first
| assumption
| (apply out_of_earshot_is_dark <;> assumption)))))
/-- info: 'Witness.a_difference_out_of_the_cone_is_dark' does not depend on any axioms -/
#guard_msgs in #print axioms a_difference_out_of_the_cone_is_dark
theorem forever_hold_your_peace (F : Face) {seats : List (List F.Probe)} {x y : F.State}
(hc : covers F seats) (hw : witnessed F seats x y) : alike F x y :=
fun p =>
(by
(apply speak_now <;>
first
| assumption
| (apply hc <;> fail)))
/-- info: 'Witness.forever_hold_your_peace' does not depend on any axioms -/
#guard_msgs in #print axioms forever_hold_your_peace
theorem the_cone_is_earshot (F : Face) (seats : List (List F.Probe)) (x y : F.State) :
witnessed F seats x y ↔ dark F seats x y :=
⟨fun hw => speak_now F hw,
fun hd s hs => a_narrower_seat_reads_no_more F s (fun q hq => hd q (mem_joinMap_intro hs hq))⟩
/-- info: 'Witness.the_cone_is_earshot' does not depend on any axioms -/
#guard_msgs in #print axioms the_cone_is_earshot
theorem a_difference_in_the_cone_is_read (F : Face) (seats : List (List F.Probe)) {x y : F.State} {q : F.Probe}
(hq : q ∈ earshot F seats) (h : F.obs x q ≠ F.obs y q) : ¬ witnessed F seats x y :=
fun p => (by (apply h <;> (apply speak_now <;> assumption)))
/-- info: 'Witness.a_difference_in_the_cone_is_read' does not depend on any axioms -/
#guard_msgs in #print axioms a_difference_in_the_cone_is_read
theorem hold_your_peace_on_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) : ∀ q, q ∈ ps → F.obs x q = F.obs y q :=
(by
(intros;
apply speak_now <;>
first
| assumption
| (apply hc <;> assumption)))
/-- info: 'Witness.hold_your_peace_on_the_room' does not depend on any axioms -/
#guard_msgs in #print axioms hold_your_peace_on_the_room
theorem the_room_at_its_probes_reads_alike (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) : reads F ps x = reads F ps y :=
by
(intros; (try dsimp only [witnessed, reads, Face.Face, coversAll] at *); intros;
(rw [Room.map_congr_mem];
(intros;
apply speak_now <;>
first
| assumption
| (apply hc <;> assumption))))
/-- info: 'Witness.the_room_at_its_probes_reads_alike' does not depend on any axioms -/
#guard_msgs in #print axioms the_room_at_its_probes_reads_alike
end Witness