UniTO/tesi/drafts/partial-decomposition-proof.org

# done
Auxiliary operations:

  index family of a constructor
  Idx(K) := [0; arity(K)[

  head of an ordered family (we write x for any object here, value, pattern etc.)
  head((xᵢ)^{i ∈ I}) = x_min(I)

  tail of an ordered family
  tail((xᵢ)^{i ∈ I}) := (xᵢ)^{i ≠ min(I)}

  head constructor of a value or pattern
  constr(K(xᵢ)ⁱ) = K
  constr(_) = ⊥
  constr(x) = ⊥

  first non-⊥ element of an ordered family
  First((xᵢ)ⁱ) := ⊥                   if ∀i, xᵢ = ⊥
  First((xᵢ)ⁱ) := x_min{i | xᵢ ≠ ⊥}   if ∃i, xᵢ ≠ ⊥
# end

Definition of running a pattern row against a (same-size) value vector  (pᵢ)ⁱ(vᵢ)ⁱ
  ∅                   (∅)                  := []
  (_, tail(pᵢ)ⁱ)      (vᵢ)                 := tail(pᵢ)ⁱ(tail(vᵢ)ⁱ)
  (x, tail(pᵢ)ⁱ)      (vᵢ)                 := σ[x↦v₀]        if tail(pᵢ)ⁱ(tail(vᵢ)ⁱ) = σ
  (K(qⱼ)ʲ, tail(pᵢ)ⁱ) (K(v'ⱼ)ʲ,tail(vⱼ)ʲ)  := ((qⱼ)ʲ +++ tail(pᵢ)ⁱ)((v'ⱼ)ʲ +++ tail(vᵢ)ⁱ)
  (K(qⱼ)ʲ, tail(pᵢ)ⁱ) (K'(v'ₗ)ˡ,tail(vⱼ)ʲ) := ⊥              if K ≠ K'
  (q₁|q₂, tail(pᵢ)ⁱ)  (vᵢ)ⁱ                := First((q₁,tail(pᵢ)ⁱ)(vᵢ)ⁱ, (q₂,tail(pᵢ)ⁱ)(vᵢ)ⁱ)

Definition of group decomposition:
  let constrs((pᵢ)^{i ∈ I}) = { K | K = constr(pᵢ), i ∈ I }
  let Groups(m) where m = ((aᵢ)ⁱ ((pᵢⱼ)ⁱ → eⱼ)ⁱʲ) =
    let (Kₖ)ᵏ = constrs(pᵢ₀)ⁱ in
    ( Kₖ →
        ((a₀.ₗ)ˡ +++ tail(aᵢ)ⁱ)
        (
         if pₒⱼ is Kₖ(qₗ) then
            (qₗ)ˡ +++ tail(pᵢⱼ)ⁱ  → eⱼ
         if pₒⱼ is _ then
            (_)ˡ +++ tail(pᵢⱼ)ⁱ   → eⱼ
         else ⊥
        )ʲ
    ), (
      tail(aᵢ)ⁱ, (tail(pᵢⱼ)ⁱ  → eⱼ if p₀ⱼ is _ else ⊥)ʲ
    )

Groups(m) is an auxiliary function that decomposes a matrix m into
submatrices, according to the head constructor of their first pattern.
Groups(m) returns one submatrix m_r for each head constructor K that
occurs on the first row of m, plus one "wildcard submatrix" m_{wild}
that matches on all values that do not start with one of those head
constructors.

Intuitively, m is equivalent to its decomposition in the following
sense: if the first pattern of an input vector (v_i)^i starts with one
of the head constructors Kₖ, then running (v_i)^i against m is the same
as running it against the submatrix m_{Kₖ}; otherwise (its head
constructor is none of the Kₖ) it is equivalent to running it against
the wildcard submatrix.

We formalize this intuition as follows:

Lemma (Groups):
  Let $m$ be a matrix with $Groups(m) = (kᵣ → mᵣ)ᵏ, m_{wild}$.
  For any value vector $(vᵢ)ᴵ$ such that $v₀ = K(v'ₗ)ˡ$ for some
  constructor K,
  we have:
  \[
    if K = Kₖ for some k then
      m(vᵢ)ⁱ = mₖ((v'ₗ)ˡ +++ (vᵢ)^{i∈I\{0}})
    otherwise
      m(vᵢ)ⁱ = m_{wild}(vᵢ)^{i∈I\{0}}
  \]

Proof:

  Let $m$ be a matrix ((aᵢ)ⁱ, ((pᵢⱼ)ⁱ → eⱼ)ʲ) with $Groups(m) = (Kₖ → mₖ)ᵏ, m_{wild}$.

  Below we are going to assume that m is a simplified matrix:

    the first row does not with an or-pattern or a variable

  I think it would be simpler to not consider them at all in the
  formalization. If we do want them, the discrepancy can be fixed
  later by defining a simplification step that explodes
  head-or-patterns and binds variable, and showing that it preserves
  the matrix semantics.

  Let (vᵢ)ⁱ be an input matrix with v₀ = Kᵥ(v'ₗ)ˡ for some constructor Kᵥ.

  We have to show that:
  - if Kₖ = Kᵥ for some Kₖ ∈ constrs(p₀ⱼ)ʲ, then
      m(vᵢ)ⁱ = mₖ((v'ₗ)ˡ +++ tail(vᵢ)ⁱ)
  - otherwise
      m(vᵢ)ⁱ = m_{wild}(tail(vᵢ)ⁱ)

  Let us call (rₖⱼ) the j-th row of the submatrix mₖ, and rⱼ_{wild}
  the j-th row of the wildcard submatrix m_{wild}.

  Our goal contains same-behavior equalities between matrices, for
  a fixed input vector (vᵢ)ⁱ. It suffices to show same-behavior
  equalities between each row of the matrices for this input
  vector. We show that for any j,

  - if Kₖ = Kᵥ for some Kₖ ∈ constrs(p₀ⱼ)ʲ, then
      (pᵢⱼ)ⁱ(vᵢ)ⁱ = rₖⱼ((v'ₗ)ˡ +++ tail(vᵢ)ⁱ
  - otherwise
      (pᵢⱼ)ⁱ(vᵢ)ⁱ = rⱼ_{wild} tail(vᵢ)ⁱ

  In the first case (Kᵥ is Kₖ for some Kₖ ∈ constrs(p₀ⱼ)ʲ), we
  have to prove that

    (pᵢⱼ)ⁱ(vᵢ)ⁱ = rₖⱼ((v'ₗ)ˡ +++ tail(vᵢ)ⁱ

  By definition of mₖ we know that rₖⱼ is equal to
  
    if pₒⱼ is Kₖ(qₗ) then
       (qₗ)ˡ +++ tail(pᵢⱼ)ⁱ  → eⱼ
    if pₒⱼ is _ then
       (_)ˡ +++ tail(pᵢⱼ)ⁱ   → eⱼ
    else ⊥

  By definition of (pᵢ)ⁱ(vᵢ)ⁱ we know that (pᵢⱼ)ⁱ(vᵢ) is equal to

    (K(qⱼ)ʲ, tail(pᵢⱼ)ⁱ) (K(v'ₗ)ˡ,tail(vᵢ)ⁱ)  := ((qⱼ)ʲ +++ tail(pᵢⱼ)ⁱ)((v'ₗ)ˡ +++ tail(vᵢ)ⁱ)
    (_, tail(pᵢⱼ)ⁱ)      (vᵢ)                 := tail(pᵢⱼ)ⁱ(tail(vᵢ)ⁱ)
    (K(qⱼ)ʲ, tail(pᵢⱼ)ⁱ) (K'(v'ₗ)ˡ,tail(vⱼ)ʲ) := ⊥              if K ≠ K'

  We prove this first case by a second case analysis on p₀ⱼ.

    TODO

  In the second case (Kᵥ is distinct from Kₖ for all Kₖ ∈ constrs(pₒⱼ)ʲ),
  we have to prove that

      (pᵢⱼ)ⁱ(vᵢ)ⁱ = rⱼ_{wild} tail(vᵢ)ⁱ

    TODO