IndisputableMonolith.Causality.Reach

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Causality
   5
   6variable {α : Type}
   7
   8structure Kinematics (α : Type) where
   9  step : α → α → Prop
  10
  11inductive ReachN (K : Kinematics α) : Nat → α → α → Prop
  12| zero {x} : ReachN K 0 x x
  13| succ {n x y z} : ReachN K n x y → K.step y z → ReachN K (n+1) x z
  14
  15def inBall (K : Kinematics α) (x : α) (n : Nat) (y : α) : Prop :=
  16  ∃ k ≤ n, ReachN K k x y
  17
  18lemma reach_in_ball {K : Kinematics α} {x y : α} {n : Nat}
  19  (h : ReachN K n x y) : inBall K x n y := ⟨n, le_rfl, h⟩
  20
  21lemma reach_le_in_ball {K : Kinematics α} {x y : α} {k n : Nat}
  22  (hk : k ≤ n) (h : ReachN K k x y) : inBall K x n y := ⟨k, hk, h⟩
  23
  24def Reaches (K : Kinematics α) (x y : α) : Prop := ∃ n, ReachN K n x y
  25
  26lemma reaches_of_reachN {K : Kinematics α} {x y : α} {n : Nat}
  27  (h : ReachN K n x y) : Reaches K x y := ⟨n, h⟩
  28
  29lemma inBall_mono {K : Kinematics α} {x y : α} {n m : Nat}
  30  (hnm : n ≤ m) : inBall K x n y → inBall K x m y := by
  31  intro ⟨k, hk, hkreach⟩
  32  exact ⟨k, le_trans hk hnm, hkreach⟩
  33
  34def ballP (K : Kinematics α) (x : α) : Nat → α → Prop
  35| 0, y => y = x
  36| Nat.succ n, y => ballP K x n y ∨ ∃ z, ballP K x n z ∧ K.step z y
  37
  38lemma ballP_mono {K : Kinematics α} {x : α} {n m : Nat}
  39  (hnm : n ≤ m) : {y | ballP K x n y} ⊆ {y | ballP K x m y} := by
  40  induction hnm with
  41  | refl => intro y hy; simpa using hy
  42  | @step m hm ih =>
  43      intro y hy
  44      exact Or.inl (ih hy)
  45
  46lemma reach_mem_ballP {K : Kinematics α} {x y : α} :
  47  ∀ {n}, ReachN K n x y → ballP K x n y := by
  48  intro n h; induction h with
  49  | zero => simp [ballP]
  50  | @succ n x y z hxy hyz ih =>
  51      exact Or.inr ⟨y, ih, hyz⟩
  52
  53lemma inBall_subset_ballP {K : Kinematics α} {x y : α} {n : Nat} :
  54  inBall K x n y → ballP K x n y := by
  55  intro ⟨k, hk, hreach⟩
  56  have : ballP K x k y := reach_mem_ballP (K:=K) (x:=x) (y:=y) hreach
  57  have mono := ballP_mono (K:=K) (x:=x) hk
  58  exact mono this
  59
  60lemma ballP_subset_inBall {K : Kinematics α} {x y : α} :
  61  ∀ {n}, ballP K x n y → inBall K x n y := by
  62  intro n
  63  induction n generalizing y with
  64  | zero =>
  65      intro hy; rcases hy with rfl
  66      exact ⟨0, le_rfl, ReachN.zero⟩
  67  | succ n ih =>
  68      intro hy
  69      cases hy with
  70      | inl hy' =>
  71          rcases ih hy' with ⟨k, hk, hkreach⟩
  72          exact ⟨k, Nat.le_trans hk (Nat.le_succ _), hkreach⟩
  73      | inr h' =>
  74          rcases h' with ⟨z, hz, hstep⟩
  75          rcases ih hz with ⟨k, hk, hkreach⟩
  76          exact ⟨k + 1, Nat.succ_le_succ hk, ReachN.succ hkreach hstep⟩
  77
  78end Causality
  79end IndisputableMonolith
  80