PrimParser Lawfulness Proofs

Lawful instances for Success, Outcome, and Parser: LawfulFunctor, LawfulGradedFunctor, LawfulGradedApplicative, LawfulGradedMonad.

instance Parser.instLawfulFunctorSuccess {n : ℕ} {gc : Necessity} : LawfulFunctor (Success n gc)

instance Parser.instLawfulFunctorOutcome {ε : Type} {n : ℕ} {gc : Necessity} : LawfulFunctor (Outcome ε n gc)

instance Parser.instLawfulGradedFunctorNecessitySuccess {n : ℕ} : LawfulGradedFunctor (Success n)

instance Parser.instLawfulGradedFunctorGrade {σ τ : Type} [Buffer σ] [Reader σ τ] {ε : Type} : LawfulGradedFunctor (Parser σ τ ε)

theorem Parser.heq {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {g1 g2 : Grade} {p : Parser σ τ ε g1 α} {q : Parser σ τ ε g2 α} (hg : g1 = g2) (h : ∀ {m : ℕ} (t : Input σ m), p.run t ≍ q.run t) : p ≍ q

@[simp]

theorem Parser.Failure.trans_self {ε : Type} {n : ℕ} (e : Failure n ε) (h : n ≤ n) : e.trans h = e

theorem Parser.Success.heq {α : Type} {n : ℕ} {c1 c2 : Necessity} {s1 : Success n c1 α} {s2 : Success n c2 α} (hc : c1 = c2) (hr : s1.result = s2.result := by rfl) (hrs : s1.restSize = s2.restSize := by rfl) : s1 ≍ s2

theorem Parser.Success.seq_assoc {α β γ : Type} {n : ℕ} {gc gc' gc'' : Necessity} {a : Success n gc α} {b : Success a.restSize gc' β} {c : Success b.restSize gc'' γ} : (a.seq b).seq c ≍ a.seq (b.seq c)

@[simp]

theorem Parser.Success.seq_result {α β : Type} {n : ℕ} {gc gc' : Necessity} (a : Success n gc α) (b : Success a.restSize gc' β) : (a.seq b).result = b.result

@[simp]

theorem Parser.Success.seq_restSize {α β : Type} {n : ℕ} {gc gc' : Necessity} (a : Success n gc α) (b : Success a.restSize gc' β) : (a.seq b).restSize = b.restSize

theorem Parser.Outcome.failure_congr {α ε : Type} {n : ℕ} {c1 c2 : Necessity} {f : Failure n ε} (hc : c1 = c2) : failure f ≍ failure f

theorem Parser.Outcome.success_congr {α ε : Type} {n : ℕ} {c1 c2 : Necessity} {s1 : Success n c1 α} {s2 : Success n c2 α} (hc : c1 = c2) (hs : s1 ≍ s2) : success s1 ≍ success s2

theorem Parser.bind_run {σ τ : Type} [Buffer σ] [Reader σ τ] {α β ε : Type} {n : ℕ} {g g' : Grade} (m : Parser σ τ ε g α) (f : α → Parser σ τ ε g' β) (t : Input σ n) : (m.bind f).run t = match m.run t with | failure e => failure e | success x => match (f x.result).run (t.dropTo x.restSize ⋯) with | failure e => failure (e.trans ⋯) | success y => success (x.seq y)

theorem Parser.gpure_gbind {σ τ : Type} [Buffer σ] [Reader σ τ] {α β ε : Type} {j : Grade} (a : α) (f : α → Parser σ τ ε j β) : gpure a >>=ᵍ f ≍ f a

theorem Parser.gbind_gpure {σ τ : Type} [Buffer σ] [Reader σ τ] {α ε : Type} {i : Grade} (p : Parser σ τ ε i α) : p >>=ᵍ gpure ≍ p

theorem Parser.gbind_assoc {σ τ : Type} [Buffer σ] [Reader σ τ] {α β γ ε : Type} {i j k : Grade} (x : Parser σ τ ε i α) (f : α → Parser σ τ ε j β) (g : β → Parser σ τ ε k γ) : x >>=ᵍ f >>=ᵍ g ≍ x >>=ᵍ fun (a : α) => f a >>=ᵍ g

theorem Parser.gmap_gpure {σ τ : Type} [Buffer σ] [Reader σ τ] {α β ε : Type} (G : α → β) (x : α) : G <$>ᵍ gpure x = gpure (G x)

theorem Parser.gpure_gseq {σ τ : Type} [Buffer σ] [Reader σ τ] {α β ε : Type} {i : Grade} (G : α → β) (x : Parser σ τ ε i α) : (gpure G <*>ᵍ fun (x_1 : Unit) => x) ≍ G <$>ᵍ x

theorem Parser.gseq_gpure {σ τ : Type} [Buffer σ] [Reader σ τ] {α β ε : Type} {i : Grade} (u : Parser σ τ ε i (α → β)) (x : α) : (u <*>ᵍ fun (x_1 : Unit) => gpure x) ≍ (fun (x_1 : α → β) => x_1 x) <$>ᵍ u

theorem Parser.gseq_assoc {σ τ : Type} [Buffer σ] [Reader σ τ] {α β γ ε : Type} {i j k : Grade} (u : Parser σ τ ε i (β → γ)) (v : Parser σ τ ε j (α → β)) (w : Parser σ τ ε k α) : ((Function.comp <$>ᵍ u <*>ᵍ fun (x : Unit) => v) <*>ᵍ fun (x : Unit) => w) ≍ u <*>ᵍ fun (x : Unit) => v <*>ᵍ fun (x : Unit) => w

instance Parser.instLawfulGradedApplicativeGrade {σ τ : Type} [Buffer σ] [Reader σ τ] {ε : Type} : LawfulGradedApplicative (Parser σ τ ε)

instance Parser.instLawfulGradedMonadGrade {σ τ : Type} [Buffer σ] [Reader σ τ] {ε : Type} : LawfulGradedMonad (Parser σ τ ε)