Noperthedron.SolutionTable.Basic

source

def Pose.getParam (q : Pose) :

Solution.Param → ℝ

Equations

Instances For

source

def Solution.Row.ValidGlobal (_tab : Table) (row : Row) :

Prop

Equations

Solution.Row.ValidGlobal _tab row = (Solution.Checker.checkGlobal row = true)

Instances For

source

instance Solution.instDecidableValidGlobal (_tab : Table) (row : Row) :

Decidable (Row.ValidGlobal _tab row)

Equations

Solution.instDecidableValidGlobal _tab row = inferInstanceAs (Decidable (Solution.Checker.checkGlobal row = true))

source

def Solution.Row.ValidLocal (tab : Table) (row : Row) :

Prop

Equations

Solution.Row.ValidLocal tab row = (row.nodeType = 2 ∧ sorry)

Instances For

source

instance Solution.instDecidableValidLocal (tab : Table) (row : Row) :

Decidable (Row.ValidLocal tab row)

Equations

Solution.instDecidableValidLocal tab row = sorry

source

structure Solution.Row.ValidSplitParam (tab : Table) (row : Row) (param : Param) :

Prop

split : row.split = 1
bound0 : row.ID < row.IDfirstChild
bound1 : row.IDfirstChild < Array.size tab
bound2 : row.IDfirstChild + 1 < Array.size tab
first_child_good : tab[row.IDfirstChild].interval = Interval.lower_half param row.interval
second_child_good : tab[row.IDfirstChild + 1].interval = Interval.upper_half param row.interval

Instances For

source

instance Solution.instDecidableValidSplitParam (tab : Table) (row : Row) (param : Param) :

Decidable (Row.ValidSplitParam tab row param)

Equations

One or more equations did not get rendered due to their size.

source

def Solution.Row.ValidBinarySplit (tab : Table) (row : Row) :

Prop

Equations

One or more equations did not get rendered due to their size.

Instances For

source

instance Solution.Row.instDecidableValidBinarySplit (tab : Table) (row : Row) :

Decidable (ValidBinarySplit tab row)

Equations

Solution.Row.instDecidableValidBinarySplit tab row = instDecidableAnd

source

def Solution.example_interval :

Interval

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Solution.Table.HasIntervals (tab : Table) (start : ℕ) (intervals : List Interval) :

Prop

Equations

tab.HasIntervals start intervals = ∀ (i : Fin intervals.length), ∃ (h : start + ↑i < Array.size tab), tab[start + ↑i].interval = intervals[i]

Instances For

source

instance Solution.Table.instDecidableHasIntervals (tab : Table) (start : ℕ) (intervals : List Interval) :

Decidable (tab.HasIntervals start intervals)

Equations

tab.instDecidableHasIntervals start intervals = Nat.decidableForallFin fun (i : Fin intervals.length) => ∃ (h : start + ↑i < Array.size tab), tab[start + ↑i].interval = intervals[i]

source

def Solution.Row.ValidFullSplit (tab : Table) (row : Row) :

Prop

Equations

One or more equations did not get rendered due to their size.

Instances For

source

instance Solution.Row.instDecidableValidFullSplit (tab : Table) (row : Row) :

Decidable (ValidFullSplit tab row)

Equations

Solution.Row.instDecidableValidFullSplit tab row = instDecidableAnd

source

def Solution.Row.ValidSplit (tab : Table) (row : Row) :

Prop

Equations

Solution.Row.ValidSplit tab row = (row.nodeType = 3 ∧ (Solution.Row.ValidBinarySplit tab row ∨ Solution.Row.ValidFullSplit tab row))

Instances For

source

instance Solution.Row.instDecidableValidSplit (tab : Table) (row : Row) :

Decidable (ValidSplit tab row)

Equations

Solution.Row.instDecidableValidSplit tab row = instDecidableAnd

source

inductive Solution.Row.Valid (tab : Table) (row : Row) :

Prop

asSplit {tab : Table} {row : Row} : ValidSplit tab row → Valid tab row
asGlobal {tab : Table} {row : Row} : ValidGlobal tab row → Valid tab row
asLocal {tab : Table} {row : Row} : ValidLocal tab row → Valid tab row

Instances For

source

instance Solution.instDecidableValid (tab : Table) (row : Row) :

Decidable (Row.Valid tab row)

Equations

Solution.instDecidableValid tab row = decidable_of_iff (Solution.Row.ValidSplit tab row ∨ Solution.Row.ValidGlobal tab row ∨ Solution.Row.ValidLocal tab row) ⋯

source

def Solution.Row.ValidIx (tab : Table) (i : ℕ) (row : Row) :

Prop

Equations

Solution.Row.ValidIx tab i row = (row.ID = i ∧ Solution.Row.Valid tab row ∧ row.ID < Array.size tab)

Instances For

source

instance Solution.Row.instDecidableValidIx (tab : Table) (i : ℕ) (row : Row) :

Decidable (ValidIx tab i row)

Equations

Solution.Row.instDecidableValidIx tab i row = instDecidableAnd

source

def Solution.Table.Valid (tab : Table) :

Prop

Equations

tab.Valid = ∀ (i : Fin (Array.size tab)), Solution.Row.ValidIx tab (↑i) tab[i]

Instances For

source

instance Solution.Table.instDecidableValid (tab : Table) :

Decidable tab.Valid

Equations

tab.instDecidableValid = Nat.decidableForallFin fun (i : Fin (Array.size tab)) => Solution.Row.ValidIx tab (↑i) tab[i]

source

theorem Solution.Table.Valid.valid_at {tab : Table} (htab : tab.Valid) {i : ℕ} (hi : i < Array.size tab) :

Row.ValidIx tab i tab[i]

source

def Solution.Table.valid_decidable (tab : Table) :

Decidable tab.Valid

Equations

tab.valid_decidable = inferInstance

Instances For

source

def Solution.DENOM :

ℝ

The common denominator of θ₁, θ₂, φ₁, φ₂, α rational representation in the table. See [SY25 §7.2]

Equations

Solution.DENOM = 15360000

Instances For

source

noncomputable def Solution.Interval.toPoseInterval (iv : Interval) :

PoseInterval

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def Solution.Row.toPoseInterval (row : Row) :

PoseInterval

Equations

row.toPoseInterval = row.interval.toPoseInterval

Instances For

source

instance Solution.instCoeIntervalSetPose :

Coe Interval (Set Pose)

Equations

Solution.instCoeIntervalSetPose = { coe := fun (iv : Solution.Interval) => {q : Pose | q ∈ iv.toPoseInterval} }

source

theorem Solution.cube_fold_nonempty_aux {α β : Type} {fs : List (α → β → β)} (hfs : fs ≠ []) (b : β) (as : List α) :

0 < (cubeFold fs b as).length

source

theorem Solution.cube_fold_nonempty {α β : Type} {fs : List (α → β → β)} (hfs : fs ≠ []) (b : β) (as : List α) :

1 ≤ (cubeFold fs b as).length

source

theorem Solution.cube_fold_halves (h : Param) (tl : List Param) (iv : Interval) (lower upper : Param → Interval → Interval) :

cubeFold [lower, upper] iv (h :: tl) = cubeFold [lower, upper] (lower h iv) tl ++ cubeFold [lower, upper] (upper h iv) tl

source

theorem Solution.has_intervals_start_in_table (tab : Table) (n : ℕ) (ivs : List Interval) (hivs : 1 ≤ ivs.length) (hi : tab.HasIntervals n ivs) :

n < Array.size tab

source

theorem Solution.has_intervals_concat (tab : Table) (start : ℕ) (ivs1 ivs2 : List Interval) :

tab.HasIntervals start (ivs1 ++ ivs2) ↔ tab.HasIntervals start ivs1 ∧ tab.HasIntervals (start + ivs1.length) ivs2