Projects.AP.DisjA

source

def AP.State.aWinsDisj (s : State) (fsp : FSP) (st : Strat) :

Prop

Equations

s.aWinsDisj fsp st = ∀ (n : ℕ), ∃ (s₁ : AP.State), AP.sys.simulate st.f s n = (s₁, 0) ∧ ¬fsp.hasLe n s₁.aPos

Instances For

source

def AP.State.aForallWinsDisj (s : State) (fsp : FSP) (a : AStrat) :

Prop

Equations

s.aForallWinsDisj fsp a = ∀ (d : AP.DStrat), d.WF → s.aWinsDisj fsp { a := a, d := d }

Instances For

source

def AP.State.aHwsDisj (s : State) (fsp : FSP) :

Prop

Equations

s.aHwsDisj fsp = ∃ (a : AP.AStrat), a.WF ∧ s.aForallWinsDisj fsp a

Instances For

source

theorem AP.AState.tr_of_aForallWinsDisj {s : State} {fsp : FSP} {a : AStrat} [hs : AState s] (h₁ : s.aForallWinsDisj fsp a) :

∃ (p : PointZ) (s' : State), sys.tr s p = some s' ∧ s'.aForallWinsDisj fsp.next a

source

theorem AP.AState.tr_of_aHwsDisj {s : State} {fsp : FSP} [hs : AState s] (h : s.aHwsDisj fsp) :

∃ (p : PointZ) (s' : State), sys.tr s p = some s' ∧ s'.aHwsDisj fsp.next

source

theorem AP.DState.tr_of_aForallWinsDisj {s s' : State} {p : PointZ} {fsp : FSP} {a : AStrat} [hs : DState s] [ha : a.WF] (h₁ : s.aForallWinsDisj fsp a) (h₂ : sys.tr s p = some s') :

s'.aForallWinsDisj fsp.next a

source

theorem AP.DState.tr_of_aHwsDisj {s s' : State} {p : PointZ} {fsp : FSP} [hs : DState s] (h₁ : s.aHwsDisj fsp) (h₂ : sys.tr s p = some s') :

s'.aHwsDisj fsp.next

source

theorem AP.State.aWinsDisj_iff {s : State} {fsp : FSP} {st : Strat} :

s.aWinsDisj fsp st ↔ s.aWins st ∧ ∀ (n : ℕ), ¬fsp.hasLe n (sys.simulate st.f s n).1.aPos

source

theorem AP.State.aWinsDisj_of_congr {s : State} {fsp₁ fsp₂ : FSP} {st : Strat} (h₁ : s.aWinsDisj fsp₁ st) (h₂ : ∀ (n : ℕ), fsp₂.hasLe n (sys.simulate st.f s n).1.aPos → ∃ (k : ℕ), fsp₁.hasLe k (sys.simulate st.f s k).1.aPos) :

s.aWinsDisj fsp₂ st

source

theorem AP.State.aWinsDisj_insertSet_of_le {s : State} {fsp : FSP} {st : Strat} {ps : Set PointZ} {m n : ℕ} (h₁ : s.aWinsDisj (fsp.insertSet m ps) st) (h₂ : m ≤ n) :

s.aWinsDisj (fsp.insertSet n ps) st

source

theorem AP.State.aWinsDisj_insert_of_le {s : State} {fsp : FSP} {st : Strat} {p : PointZ} {m n : ℕ} (h₁ : s.aWinsDisj (fsp.insert m p) st) (h₂ : m ≤ n) :

s.aWinsDisj (fsp.insert n p) st

source

theorem AP.State.aForallWinsDisj_insertSet_of_le {s : State} {fsp : FSP} {a : AStrat} {ps : Set PointZ} {m n : ℕ} (h₁ : s.aForallWinsDisj (fsp.insertSet m ps) a) (h₂ : m ≤ n) :

s.aForallWinsDisj (fsp.insertSet n ps) a

source

theorem AP.State.aForallWinsDisj_insert_of_le {s : State} {fsp : FSP} {a : AStrat} {p : PointZ} {m n : ℕ} (h₁ : s.aForallWinsDisj (fsp.insert m p) a) (h₂ : m ≤ n) :

s.aForallWinsDisj (fsp.insert n p) a

source

theorem AP.State.aHwsDisj_insertSet_of_le {s : State} {fsp : FSP} {ps : Set PointZ} {m n : ℕ} (h₁ : s.aHwsDisj (fsp.insertSet m ps)) (h₂ : m ≤ n) :

s.aHwsDisj (fsp.insertSet n ps)

source

theorem AP.State.aHwsDisj_insert_of_le {s : State} {fsp : FSP} {p : PointZ} {m n : ℕ} (h₁ : s.aHwsDisj (fsp.insert m p)) (h₂ : m ≤ n) :

s.aHwsDisj (fsp.insert n p)

source

theorem AP.State.aForallWinsDisj_insert_of_mem_taken {s : State} {fsp : FSP} {p : PointZ} {a : AStrat} [hs : sys.WF s] (h₁ : s.aForallWinsDisj fsp a) (h₂ : p ∈ s.taken) :

s.aForallWinsDisj (fsp.insert 0 p) a

source

theorem AP.State.aHwsDisj_insert_of_mem_taken {s : State} {fsp : FSP} {p : PointZ} [hs : sys.WF s] (h₁ : s.aHwsDisj fsp) (h₂ : p ∈ s.taken) :

s.aHwsDisj (fsp.insert 0 p)

source

theorem AP.State.aWinsDisj_of_aWinsDisj_offset {s : State} {st : Strat} {fsp : FSP} {n : ℕ} (h : s.aWinsDisj (fsp.offset n) st) :

s.aWinsDisj fsp st

source

theorem AP.State.aForallWinsDisj_of_aForallWinsDisj_offset {s : State} {a : AStrat} {fsp : FSP} {n : ℕ} (h : s.aForallWinsDisj (fsp.offset n) a) :

s.aForallWinsDisj fsp a

source

theorem AP.State.aHwsDisj_of_aHwsDisj_offset {s : State} {fsp : FSP} {n : ℕ} (h : s.aHwsDisj (fsp.offset n)) :

s.aHwsDisj fsp

source

theorem AP.State.aWinsDisj_of_aWinsDisj_next {s : State} {st : Strat} {fsp : FSP} (h : s.aWinsDisj fsp.next st) :

s.aWinsDisj fsp st

source

theorem AP.State.aForallWinsDisj_of_aForallWinsDisj_next {s : State} {a : AStrat} {fsp : FSP} (h : s.aForallWinsDisj fsp.next a) :

s.aForallWinsDisj fsp a

source

theorem AP.State.aHwsDisj_of_aHwsDisj_next {s : State} {fsp : FSP} (h : s.aHwsDisj fsp.next) :

s.aHwsDisj fsp

source

theorem AP.State.aHwsDisj_setHist_of_aHwsDisj {s : State} {fsp : FSP} {hist : List PointZ} [hs : sys.WF s] [hs' : sys.WF (s.setHist hist)] (h : s.aHwsDisj fsp) :

(s.setHist hist).aHwsDisj fsp

source

@[simp]

theorem AP.State.aHwsDisj_setHist_iff {s : State} {fsp : FSP} {hist : List PointZ} [hs : sys.WF s] [hs' : sys.WF (s.setHist hist)] :

(s.setHist hist).aHwsDisj fsp ↔ s.aHwsDisj fsp

source

theorem AP.State.aPos_not_mem_fsp_get_zero_of_aWinsDisj {s : State} {fsp : FSP} {st : Strat} (h : s.aWinsDisj fsp st) :

s.aPos ∉ fsp.get 0

source

theorem AP.State.aPos_not_mem_fsp_get_zero_of_aForallWinsDisj {s : State} {fsp : FSP} {a : AStrat} (h : s.aForallWinsDisj fsp a) :

s.aPos ∉ fsp.get 0

source

theorem AP.State.aPos_not_mem_fsp_get_zero_of_aHwsDisj {s : State} {fsp : FSP} (h : s.aHwsDisj fsp) :

s.aPos ∉ fsp.get 0

source

theorem AP.State.aWins_of_aWinsDisj {fsp : FSP} {s : State} {a : AStrat} {d : DStrat} (h : s.aWinsDisj fsp { a := a, d := d }) :

s.aWins { a := a, d := d }

source

theorem AP.State.aWins_of_aForallWinsDisj {fsp : FSP} {s : State} {a : AStrat} {d : DStrat} [hd : d.WF] (h : s.aForallWinsDisj fsp a) :

s.aWins { a := a, d := d }

source

theorem AP.State.forall_aWins_of_aForallWinsDisj {fsp : FSP} {s : State} {a : AStrat} (h : s.aForallWinsDisj fsp a) (d : DStrat) [d.WF] :

s.aWins { a := a, d := d }

source

theorem AP.State.aHws_of_aForallWinsDisj {fsp : FSP} {s : State} {a : AStrat} [ha : a.WF] (h : s.aForallWinsDisj fsp a) :

s.aHws

source

structure AP.DisjEraseTaken :

Type

a : AStrat
s : State
p : PointZ
fsp : FSP
n : ℕ

Instances For

source

def AP.aDisjEraseTaken_fa (acc : DisjEraseTaken) :

PointZ × DisjEraseTaken

Equations

AP.aDisjEraseTaken_fa { a := a, s := s, p := p, fsp := fsp, n := n } = (a.f s, { a := a, s := (AP.sys.tr s (a.f s)).get!, p := p, fsp := fsp.next, n := n + 1 })

Instances For

source

def AP.aDisjEraseTaken_fd (p₁ : PointZ) (acc : DisjEraseTaken) :

DisjEraseTaken

Equations

AP.aDisjEraseTaken_fd p₁ { a := a, s := s, p := p, fsp := fsp, n := n } = { a := a, s := (AP.sys.tr s (if p₁ = p then s.chooseDMove else p₁)).get!, p := if p₁ = p then s.chooseDMove else p, fsp := fsp.next, n := n + 1 }

Instances For

source

def AP.aDisjEraseTaken (s s' : State) (p : PointZ) (a : AStrat) (fsp : FSP) :

AStrat

Equations

AP.aDisjEraseTaken s s' p a fsp = AP.AStrat.mkFold s' { a := a, s := s, p := p, fsp := fsp, n := 0 } (fun (x : AP.State) => AP.aDisjEraseTaken_fa) fun (x : AP.State) => AP.aDisjEraseTaken_fd

Instances For

source

theorem AP.AState.validTr_of_aForallWinsDisj {fsp : FSP} {s : State} {a : AStrat} [hsa : AState s] (h : s.aForallWinsDisj fsp a) :

sys.validTr s (a.f s)

source

@[simp]

instance AP.instWFADisjEraseTaken {s s' : State} {p : PointZ} {a : AStrat} {fsp : FSP} :

(aDisjEraseTaken s s' p a fsp).WF

source

structure AP.DisjEraseTaken.Cnd (w₀ w : DisjEraseTaken) (s' s₁' : State) (n : ℕ) :

Prop

h₁ : s₁'.hist.length - s'.hist.length = n
h₂ : w.n = n
h₃ : ∃ (d : DStrat), d.WF ∧ sys.simulate { a := w.a, d := d }.f w₀.s n = (w.s, 0)
h₄ : w.p ∈ w.s.taken
h₅ : s₁' = let __src := w.s; { pw := __src.pw, taken := w.s.taken.erase w.p, aPos := __src.aPos, aTurn := __src.aTurn, hist := s₁'.hist }
h₆ : w.s.aForallWinsDisj w.fsp w.a
h₈ : w.a = w₀.a
h₉ : w.fsp = w₀.fsp.offset n

Instances For

source

theorem AP.DisjEraseTaken.Cnd.state_eq_symm {w₀ w : DisjEraseTaken} {s' s₁' : State} {n : ℕ} (h : w₀.Cnd w s' s₁' n) :

w.s = { pw := s₁'.pw, taken := s₁'.taken.insert w.p, aPos := s₁'.aPos, aTurn := s₁'.aTurn, hist := w.s.hist }

source

theorem AP.State.aWinsDisj_insert_taken_of_aWinsDisj {fsp : FSP} {s : State} {st : Strat} [hs : sys.WF s] (h : s.aWinsDisj fsp st) :

s.aWinsDisj (fsp.insertSet 0 s.taken.toSet) st

source

theorem AP.State.aForallWinsDisj_insert_taken_of_aForallWinsDisj {fsp : FSP} {s : State} {a : AStrat} [hs : sys.WF s] (h : s.aForallWinsDisj fsp a) :

s.aForallWinsDisj (fsp.insertSet 0 s.taken.toSet) a

source

theorem AP.State.aHwsDisj_insert_taken_of_aHwsDisj {fsp : FSP} {s : State} [hs : sys.WF s] (h : s.aHwsDisj fsp) :

s.aHwsDisj (fsp.insertSet 0 s.taken.toSet)

source

theorem AP.State.aWinsDisj_of_aWinsDisj_insertSet {fsp : FSP} {s : State} {k : ℕ} {ps : Set PointZ} {st : Strat} (h : s.aWinsDisj (fsp.insertSet k ps) st) :

s.aWinsDisj fsp st

source

theorem AP.State.aForallWinsDisj_of_aForallWinsDisj_insertSet {fsp : FSP} {s : State} {k : ℕ} {ps : Set PointZ} {a : AStrat} (h : s.aForallWinsDisj (fsp.insertSet k ps) a) :

s.aForallWinsDisj fsp a

source

theorem AP.State.aHwsDisj_of_aHwsDisj_insertSet {fsp : FSP} {s : State} {k : ℕ} {ps : Set PointZ} (h : s.aHwsDisj (fsp.insertSet k ps)) :

s.aHwsDisj fsp

source

theorem AP.State.aWinsDisj_of_aWinsDisj_insert {fsp : FSP} {s : State} {k : ℕ} {p : PointZ} {st : Strat} (h : s.aWinsDisj (fsp.insert k p) st) :

s.aWinsDisj fsp st

source

theorem AP.State.aForallWinsDisj_of_aForallWinsDisj_insert {fsp : FSP} {s : State} {k : ℕ} {p : PointZ} {a : AStrat} (h : s.aForallWinsDisj (fsp.insert k p) a) :

s.aForallWinsDisj fsp a

source

theorem AP.State.aHwsDisj_of_aHwsDisj_insert {fsp : FSP} {s : State} {k : ℕ} {p : PointZ} (h : s.aHwsDisj (fsp.insert k p)) :

s.aHwsDisj fsp

source

theorem AP.State.aHwsDisj_erase_taken {fsp : FSP} {s s' : State} {p : PointZ} [hs : sys.WF s] [hs' : sys.WF s'] (h : s.aHwsDisj fsp) (hpw : s'.pw = s.pw) (ht : s'.aTurn = s.aTurn) (hpa : s'.aPos = s.aPos) (hp : s'.taken = s.taken.erase p) (h₁ : p ∈ s.taken) :

s'.aHwsDisj (fsp.insert 0 p)

source

theorem AP.State.aHwsDisj_erase_taken' {fsp : FSP} {s s' : State} {p : PointZ} [hs : sys.WF s] [hs' : sys.WF s'] (h : s.aHwsDisj fsp) (hpw : s'.pw = s.pw) (ht : s'.aTurn = s.aTurn) (hpa : s'.aPos = s.aPos) (hp : s'.taken = s.taken.erase p) (h₁ : p ∈ s.taken) :

s'.aHwsDisj fsp

source

theorem AP.State.aHwsDisj_of_taken_subset {fsp : FSP} {s s' : State} [hs : sys.WF s] [hs' : sys.WF s'] (h : s.aHwsDisj fsp) (hpw : s'.pw = s.pw) (ht : s'.aTurn = s.aTurn) (hpa : s'.aPos = s.aPos) (h₁ : s'.taken ⊆ s.taken) :

s'.aHwsDisj (fsp.insertSet 0 s.taken.toSet)

source

theorem AP.State.aHwsDisj_of_taken_subset' {fsp : FSP} {s s' : State} [hs : sys.WF s] [hs' : sys.WF s'] (h : s.aHwsDisj fsp) (hpw : s'.pw = s.pw) (ht : s'.aTurn = s.aTurn) (hpa : s'.aPos = s.aPos) (h₁ : s'.taken ⊆ s.taken) :

s'.aHwsDisj fsp

source

noncomputable def AP.dChooseFromSet (ps : Set' PointZ) :

DStrat

Equations

AP.dChooseFromSet ps = AP.DStrat.mk fun (sd : AP.State) => choose? fun (p : PointZ) => p ∈ ps ∧ p ∉ sd.taken ∧ p ≠ sd.aPos

Instances For

source

instance AP.instWFDChooseFromSet {ps : Set' PointZ} :

(dChooseFromSet ps).WF

source

theorem AP.State.eventually_simulate_dChooseFromSet_subset_taken {s : State} {ps : Set' PointZ} {a : AStrat} [hs : sys.WF s] [ha : a.WF] :

eventually fun (n : ℕ) => ∀ (s' : State), sys.simulate { a := a, d := dChooseFromSet ps }.f s n = (s', 0) → ps ⊆ s'.taken

source

theorem AP.State.eventually_simulate_dChooseFromSet_aPos_not_mem {s : State} {ps : Set' PointZ} {a : AStrat} [hs : sys.WF s] [ha : a.WF] :

eventually fun (n : ℕ) => ∀ (s' : State), sys.simulate { a := a, d := dChooseFromSet ps }.f s n = (s', 0) → s'.aPos ∉ ps

source

theorem AP.State.aTurn_of_tr_aPos_ne {s s' : State} {p : PointZ} [hs : sys.WF s] (h₁ : sys.tr s p = some s') (h₂ : s'.aPos ≠ s.aPos) :

s.aTurn = true

source

theorem AP.AState.of_tr_aPos_ne {s s' : State} {p : PointZ} [hs : sys.WF s] (h₁ : sys.tr s p = some s') (h₂ : s'.aPos ≠ s.aPos) :

AState s

source

theorem AP.State.aForallWinsDisj_of_simulate_eq {fsp : FSP} {s s' : State} {r n : ℕ} {a : AStrat} {d : DStrat} [hs : sys.WF s] [ha : a.WF] [hd : d.WF] (h₁ : s.aForallWinsDisj fsp a) (h₂ : sys.simulate { a := a, d := d }.f s n = (s', r)) :

s'.aForallWinsDisj (fsp.offset n) a

source

theorem AP.State.aForallWinsDisj_insertSet_zero_of {s : State} {set : Set PointZ} {a : AStrat} {fsp : FSP} (h₁ : s.aForallWinsDisj fsp a) (h₂ : ∀ (d : DStrat) [d.WF] (n : ℕ) (s₁ : State), sys.simulate { a := a, d := d }.f s n = (s₁, 0) → s₁.aPos ∉ set) :

s.aForallWinsDisj (fsp.insertSet 0 set) a

source

@[simp]

theorem AP.State.aWinsDisj_empty {s : State} {st : Strat} :

s.aWinsDisj ∅ st ↔ s.aWins st

source

@[simp]

theorem AP.State.aForallWinsDisj_empty {s : State} {a : AStrat} :

s.aForallWinsDisj ∅ a ↔ ∀ (d : DStrat), d.WF → s.aWins { a := a, d := d }

source

@[simp]

theorem AP.State.aHwsDisj_empty {s : State} :

s.aHwsDisj ∅ ↔ s.aHws

source

theorem AP.State.aHws_of_taken_subset {s s' : State} [hs : sys.WF s] [hs' : sys.WF s'] (h₁ : s.aHws) (hpw : s'.pw = s.pw) (h₂ : s'.aTurn = s.aTurn) (h₃ : s'.aPos = s.aPos) (h₄ : s'.taken ⊆ s.taken) :

s'.aHws

source

theorem AP.State.dHws_of_taken_subset {s s' : State} [hs : sys.WF s] [hs' : sys.WF s'] (h₁ : s.dHws) (hpw : s'.pw = s.pw) (h₂ : s'.aTurn = s.aTurn) (h₃ : s'.aPos = s.aPos) (h₄ : s.taken ⊆ s'.taken) :

s'.dHws