Supporting results for pointwise provable equality.

def PointwiseComposition.Nat.natToVec : ℕ → (n : ℕ) → Option (Fin n → ℕ)

The nat To Vec construction in Nat.

Equations

• PointwiseComposition.Nat.natToVec 0 0 = some ![]
• PointwiseComposition.Nat.natToVec e.succ n.succ = Option.map (fun (x : Fin n → ℕ) => (Nat.unpair e).1 :> x) (PointwiseComposition.Nat.natToVec (Nat.unpair e).2 n)
• PointwiseComposition.Nat.natToVec x✝¹ x✝ = none

@[simp]

theorem PointwiseComposition.Nat.natToVec_vecToNat {n : ℕ} (v : Fin n → ℕ) : natToVec (Matrix.vecToNat v) n = some v

theorem PointwiseComposition.Nat.lt_of_eq_natToVec {n e : ℕ} {v : Fin n → ℕ} (h : natToVec e n = some v) (i : Fin n) : v i < e

@[irreducible]

def PointwiseComposition.Nat.natToList : ℕ → List ℕ

List form of Nat.natToVec: the same decoding, with the length out of the type.

Equations

• PointwiseComposition.Nat.natToList 0 = []
• PointwiseComposition.Nat.natToList e.succ = (Nat.unpair e).1 :: PointwiseComposition.Nat.natToList (Nat.unpair e).2

theorem PointwiseComposition.Nat.natToVec_eq_some_iff {e k : ℕ} {v : Fin k → ℕ} : natToVec e k = some v ↔ natToList e = List.ofFn v

theorem PointwiseComposition.Nat.natToVec_eq_none_of_length {e k : ℕ} (h : (natToList e).length ≠ k) : natToVec e k = none

natToVec succeeds exactly when the length-free decoding has the expected length.

theorem PointwiseComposition.Nat.natToVec_isSome_of_length {e k : ℕ} (h : (natToList e).length = k) : ∃ (v : Fin k → ℕ), natToVec e k = some v