How to resolve a "Application type mismatch" of `._proof_1`

Stream: lean4

[Hirotaka Sato]

I am trying to write formal proofs about deterministic pushdown automata (DPDAs) as defined by Sipser in "Introduction to the Theory of Computation". Its transition function δ comes with a condition that enforces deterministic behavior: ∀ q a x, exactly one of δ(q, some a, some x), δ(q, some a, none), δ(q, none, some x), δ(q, none, none) is some.

Thus, I created a structure Sipser_PreDPDA that has the transition function as its data, and declared that Sipser_DPDA is the pair ofSipser_PreDPDA together with a proof that the condition holds.

The definition of Sipser_DPDA.stepTransition requires that certain path be False.elimed using the condition; however, using this version of definition causes a cryptic motive is not type correct error. To get around this issue, I first decided to define a function in Sipser_PreDPDA, such that does not kill unreachable code paths and instead returns none, and tried to show that this equals Sipser_DPDA.stepTransition for all the possible cases.

However, that attempt resulted in the error messages Case tag 'rhs' not found. and

Application type mismatch: In the application
  Sipser_DPDA.stepTransition._proof_1 M idesc hεε
the argument
  hεε
has type
  some (r, y) = none : Prop
but is expected to have type
  M.pda.transition (idesc.current_state, none, none) = none : Prop

What is the underlying cause, and how can I fix it? The following is a somewhat minimized code that reproduces the issue.

structure Sipser_PreDPDA (Q S Γ) where
  /-
  q0 : Q
  F : Finset Q
  -/
  transition : Q × Option S × Option Γ -> Option (Q × Option Γ)

def exactly_one_some {α}
  (o1 : Option α)
  (o2 : Option α)
  (o3 : Option α)
  (o4 : Option α) := match o1, o2, o3, o4 with
  | some _, none, none, none => true
  | none, some _, none, none => true
  | none, none, some _, none => true
  | none, none, none, some _ => true
  | _, _, _, _ => false

structure Sipser_DPDA(Q S Γ) where
  pda : Sipser_PreDPDA Q S Γ
  deterministic : ∀ q a x,
    exactly_one_some
      (pda.transition (q, some a, some x))
      (pda.transition (q, some a, none))
      (pda.transition (q, none, some x))
      (pda.transition (q, none, none))

structure Sipser_DPDA_IDesc (Q) (S) (Γ) where
  current_state : Q
  remaining_input : List S
  stack : List Γ


-- This is the version that does not depend on the `deterministic` condition.
-- This is intended as a workaround in Lean's `motive is not type correct` error.
def Sipser_PreDPDA.stepTransition {Q S Γ}
  (M: Sipser_PreDPDA Q S Γ)
  (idesc: Sipser_DPDA_IDesc Q S Γ)
  : Option (Sipser_DPDA_IDesc Q S Γ) :=
  match M.transition (idesc.current_state, none, none) with
  | some (r, y) => some ⟨ r, idesc.remaining_input, y.toList ++ idesc.stack ⟩
  | none => match idesc.remaining_input, idesc.stack with
    | [], [] => none
    | [], x :: xs => match M.transition (idesc.current_state, none, some x) with
      | some (r, y) => some ⟨ r, idesc.remaining_input, y.toList ++ xs ⟩
      | none => none
    | a :: ws, [] => match M.transition (idesc.current_state, some a, none) with
      | some (r, y) => some ⟨ r, ws, y.toList ++ idesc.stack ⟩
      | none => none
    | a :: ws, x :: xs => match
        (M.transition (idesc.current_state, some a, some x)),
        (M.transition (idesc.current_state, some a, none)),
        (M.transition (idesc.current_state, none, some x)) with
      | some (r, y), none, none => some ⟨ r, ws, y.toList ++ xs ⟩
      | none, some (r, y), none => some ⟨ r, idesc.remaining_input, y.toList ++ xs ⟩
      | none, none, some (r, y) => some ⟨ r, ws, y.toList ++ idesc.stack ⟩
      | _, _, _ => none -- When the `deterministic` condition holds, this branch should never be reached.


def Sipser_DPDA.stepTransition {Q S Γ}
  (M: Sipser_DPDA Q S Γ)
  (idesc: Sipser_DPDA_IDesc Q S Γ)
  : Option (Sipser_DPDA_IDesc Q S Γ) :=
  match hεε : M.pda.transition (idesc.current_state, none, none) with
  | some (r, y) => some ⟨ r, idesc.remaining_input, y.toList ++ idesc.stack ⟩
  | none => match idesc.remaining_input, idesc.stack with
    | [], [] => none
    | [], x :: xs => match h2 : M.pda.transition (idesc.current_state, none, some x) with
      | some (r, y) => some ⟨ r, idesc.remaining_input, y.toList ++ xs ⟩
      | none => none
    | a :: ws, [] => match h2 : M.pda.transition (idesc.current_state, some a, none) with
      | some (r, y) => some ⟨ r, ws, y.toList ++ idesc.stack ⟩
      | none => none
    | a :: ws, x :: xs => match
        hax : (M.pda.transition (idesc.current_state, some a, some x)),
        haε : (M.pda.transition (idesc.current_state, some a, none)),
        hεx : (M.pda.transition (idesc.current_state, none, some x)) with
      | some (r, y), none, none => some ⟨ r, ws, y.toList ++ xs ⟩
      | none, some (r, y), none => some ⟨ r, idesc.remaining_input, y.toList ++ xs ⟩
      | none, none, some (r, y) => some ⟨ r, ws, y.toList ++ idesc.stack ⟩
      | some _, some _, some _ => False.elim <| by have h3 := M.deterministic idesc.current_state a x; simp [exactly_one_some, hεε, hax, haε, hεx] at h3
      | some _, some _, none   => False.elim <| by have h3 := M.deterministic idesc.current_state a x; simp [exactly_one_some, hεε, hax, haε, hεx] at h3
      | some _, none, some _   => False.elim <| by have h3 := M.deterministic idesc.current_state a x; simp [exactly_one_some, hεε, hax, haε, hεx] at h3
      | none, some _, some _   => False.elim <| by have h3 := M.deterministic idesc.current_state a x; simp [exactly_one_some, hεε, hax, haε, hεx] at h3
      | none, none, none       => False.elim <| by have h3 := M.deterministic idesc.current_state a x; simp [exactly_one_some, hεε, hax, haε, hεx] at h3



theorem step_in_pre_is_step_in_dpda {Q S Γ}
  (M: Sipser_DPDA Q S Γ)
  (idesc: Sipser_DPDA_IDesc Q S Γ) :
  Sipser_PreDPDA.stepTransition M.pda idesc = M.stepTransition idesc := by
  simp only [Sipser_PreDPDA.stepTransition, Sipser_DPDA.stepTransition]
  match h2 : M.pda.transition (idesc.current_state, none, none) with
  | some (r, y) => sorry
  | none => sorry

[Aaron Liu]

Hirotaka Sato said:

The definition of Sipser_DPDA.stepTransition requires that certain path be False.elimed using the condition

I strongly doubt this is required, there's probably ways around it.

however, using this version of definition causes a cryptic motive is not type correct error.

Did you try reading the error message? The most common one (the one on rw) has a very detailed explanation, if you are on a sufficiently recent version of Lean.

[Hirotaka Sato]

Did you try reading the error message?

The issue arose when I used the following definition to convert a different formulation of DPDAs in to the Sipser format while proving that it satisfies the Sipser condition:

def Predet_DPDA.toSipser {Q S Γ} [DecidableEq Q] (M: Predet_DPDA Q S Γ) : Sipser_DPDA (AugmentOneState Q) S Γ :=
  let ⟨ q0, F, dot_delta ⟩ := M
  let sipser_delta_curried : (Fin 1 ⊕ Q) → Option Γ → Option S → Option (((Fin 1 ⊕ Q)) × Option Γ) := sorry /- a very long definition -/
  let is_deterministic := sorry /- somewhat long proof -/
  ⟨
    ⟨
    Sum.inr q0,
    Finset.image Sum.inr F,
    fun (p, input_consumption, stack_consumption) => sipser_delta_curried p stack_consumption input_consumption
    ⟩,
    is_deterministic
  ⟩

and then tried to prove that a single-step semantics is preserved across the translation of Predet_DPDA into Sipser_DPDA:

theorem Predet_to_Sipser_preserves_semantics_single_step {Q S Γ}
  [Fintype Q] [DecidableEq Q] [Fintype S] [Fintype Γ] [DecidableEq Γ]
  (M: Predet_DPDA Q S Γ) (idesc: Predet_DPDA_IDesc Q S Γ) :
  Predet_DPDA_IDesc.toSipser <$> M.stepTransition idesc = M.toSipser.stepTransition idesc.toSipser := by
  simp [Functor.map,
   Predet_DPDA_IDesc.toSipser,     Predet_DPDA.toSipser,
   Predet_DPDA.stepTransition, Sipser_DPDA.stepTransition,
  ]
  sorry -- this is where I am stuck

Here are the list of things I tried to fill in the location of sorry:

• cases M.transition idesc.current_state with causes tactic 'generalize' failed, result is not type correct
• Writing match (motive := Predet_Judge Q S Γ → Option Γ → Option S → Option ((Fin 1 ⊕ Q) × Option Γ)) M.transition idesc.p with | ...directly within the proof causes a type mismatch error claiming that I am supplying a Option Γ → Option S → Option ((Fin 1 ⊕ Q) × Option Γ)) M.transition idesc.p where a Prop is wanted
• Changing the simp to simp [Functor.map] and continuing on with:

  match h : M.transition idesc.p with
  | Predet_Judge.uncondPush (α, q) =>
    simp [Predet_DPDA_IDesc.toSipser, Predet_DPDA.toSipser, Predet_DPDA.stepTransition, Sipser_DPDA.stepTransition]
    rw [h] -- This is where I got `motive is not type correct`
  | Predet_Judge.popAndDecideWhetherToConsume fΓ_wS => sorry

reports

tactic 'rewrite' failed, motive is not type correct
/-- very, very long definition --/
Error: Application type mismatch: In the application
  Sipser_DPDA.stepTransition._proof_1 M.toSipser idesc.toSipser hεε
the argument
  hεε
has type
/-- very, very long definition --/
but is expected to have type
  M.toSipser.pda.transition (idesc.toSipser.p, AugmentEpsilon.Epsilon, AugmentEpsilon.Epsilon) = none : Prop
Explanation: The rewrite tactic rewrites an expression 'e' using an equality 'a = b' by the following process. First, it looks for all 'a' in 'e'. Second, it tries to abstract these occurrences of 'a' to create a function 'm := fun _a => ...', called the *motive*, with the property that 'm a' is definitionally equal to 'e'. Third, we observe that 'congrArg' implies that 'm a = m b', which can be used with lemmas such as 'Eq.mpr' to change the goal. However, if 'e' depends on specific properties of 'a', then the motive 'm' might not typecheck.

Possible solutions: use rewrite's 'occs' configuration option to limit which occurrences are rewritten, or use 'simp' or 'conv' mode, which have strategies for certain kinds of dependencies (these tactics can handle proofs and 'Decidable' instances whose types depend on the rewritten term, and 'simp' can apply user-defined '@[congr]' theorems as well).
/- very, very long definition -/

Using rw (config := { occs := .pos [1]}) [h] changes nothing; using simp results in simp made no progress. So I guess I should read the documentation of conv?

For the full context, here is the non-minimized code: https://github.com/hsjoihs/dpda-lean/blob/20250706_motive_is_not_type_correct/Dpda/Conversion/PredetToSipser.lean#L221

[Aaron Liu]

I'll see what I can do

[Aaron Liu]

Can you provide a #mwe (or a non-m we) of you problem with "motive is not type correct"?

[Hirotaka Sato]

I have originally sought to resolve the "type mismatch of ._proof_1" (because that one can be reproduced by only using Sipser_DPDA and thus I considered it simpler), so I currently only have the minimized code for "Sipser only". https://github.com/hsjoihs/dpda-lean/blob/minimal_example_sipser_only/Dpda/Definition/Sipser.lean

Unfortunately I have to leave in a few minutes and will be away for a few hours. Minimization of Predet_DPDAto make a MWE for "motive is not type correct" will be after I get back home.

[Aaron Liu]

It doesn't really need to be "minimal"

[Aaron Liu]

I just need something I can paste into a file and have it work

[Aaron Liu]

but of course more minimal is better

[Hirotaka Sato]

Somewhat minimized (retains the same error)

https://github.com/hsjoihs/dpda-lean/blob/motive_is_not_type_correct_minimal/Dpda/Main.lean

universe u_

structure Predet_DPDA (Q: Type u_) (S: Type u_) (Γ: Type u_) where
  transition : Q → (Γ × Q) ⊕ Fin 42

def Predet_DPDA.stepTransition {Q: Type u_} {S: Type u_} {Γ: Type u_}
  (M: Predet_DPDA Q S Γ)
  (pwβ: (Q × List S × List Γ))
  : Option ((Q × List S × List Γ)) := match M.transition pwβ.1 with
  | Sum.inl (γ, q) => some ⟨q, pwβ.2.1, γ :: pwβ.2.2⟩
  | Sum.inr f => sorry

def exactly_one_some {α}
  (o1 : Option α)
  (o2 : Option α)
  (o3 : Option α)
  (o4 : Option α) := match o1, o2, o3, o4 with
  | some _, none, none, none => true
  | none, some _, none, none => true
  | none, none, some _, none => true
  | none, none, none, some _ => true
  | _, _, _, _ => false

structure Sipser_DPDA(Q S Γ) where
  pda_transition : Q × Option S × Option Γ -> Option (Q × Option Γ)
  deterministic : ∀ q a x,
    exactly_one_some
      (pda_transition (q, some a, some x))
      (pda_transition (q, some a, none))
      (pda_transition (q, none, some x))
      (pda_transition (q, none, none))

def Sipser_DPDA.stepTransition {Q S Γ} (M: Sipser_DPDA Q S Γ) (pwβ: (Q × List S × List Γ)) : Option ((Q × List S × List Γ)) :=
  match hεε : M.pda_transition (pwβ.1, none, none) with
  | some (r, y) => some ⟨ r, pwβ.2.1, y.toList ++ pwβ.2.2 ⟩
  | none =>
    match pwβ.2.1, pwβ.2.2 with
    | [], [] => sorry
    | [], x :: xs => sorry
    | a :: ws, [] => sorry
    | a :: ws, x :: xs =>
      match
        hax : (M.pda_transition (pwβ.1, some a, some x)),
        haε : (M.pda_transition (pwβ.1, some a, none)),
        hεx : (M.pda_transition (pwβ.1, none, some x)) with
      | some (r, y), none, none => some ⟨ r, ws, y.toList ++ xs ⟩
      | none, some (r, y), none => some ⟨ r, pwβ.2.1, y.toList ++ xs ⟩
      | none, none, some (r, y) => some ⟨ r, ws, y.toList ++ pwβ.2.2 ⟩
      | some _, some _, some _ => False.elim <| by have h3 := M.deterministic pwβ.1 a x; simp [exactly_one_some, hεε, hax, haε, hεx] at h3
      | some _, some _, none   => False.elim <| by have h3 := M.deterministic pwβ.1 a x; simp [exactly_one_some, hεε, hax, haε, hεx] at h3
      | some _, none, some _   => False.elim <| by have h3 := M.deterministic pwβ.1 a x; simp [exactly_one_some, hεε, hax, haε, hεx] at h3
      | none, some _, some _   => False.elim <| by have h3 := M.deterministic pwβ.1 a x; simp [exactly_one_some, hεε, hax, haε, hεx] at h3
      | none, none, none       => False.elim <| by have h3 := M.deterministic pwβ.1 a x; simp [exactly_one_some, hεε, hax, haε, hεx] at h3

def Predet_DPDA.toSipser {Q S Γ} [DecidableEq Q] (M: Predet_DPDA Q S Γ) : Sipser_DPDA (Option Q) S Γ :=
  let sipser_delta_curried : (Option Q) → Option Γ → Option S → Option (Option Q × Option Γ) :=
    fun p_ => match p_ with
     | none => sorry
     | some p =>
       match M.transition p with
        | Sum.inl (α, q) => sorry
        | Sum.inr fΓ_wS => sorry
  let is_deterministic := sorry
  ⟨
    fun (p, input_consumption, stack_consumption) => sipser_delta_curried p stack_consumption input_consumption
    ,
    is_deterministic
  ⟩

theorem Predet_to_Sipser_preserves_semantics_single_step {Q S Γ}
  [DecidableEq Q] [DecidableEq Γ]
  (M: Predet_DPDA Q S Γ) (idesc: (Q × List S × List Γ)) :
  (fun ⟨ p, w, β ⟩ => ⟨ some p, w, β ⟩) <$> M.stepTransition idesc = M.toSipser.stepTransition (idesc |> fun ⟨ p, w, β ⟩ => ⟨ some p, w, β ⟩) := by
  simp [Functor.map]
  match h : M.transition idesc.1 with
  | Sum.inl (α, q) =>
    simp [Predet_DPDA.toSipser, Predet_DPDA.stepTransition, Sipser_DPDA.stepTransition]
    rw [h] -- This is where I got `motive is not type correct`
  | Sum.inr fΓ_wS => sorry

[Aaron Liu]

I changed rw [h] to simp only [h] and it worked

[Hirotaka Sato]

Hmm maybe then I minimized it too much. Let me bisect and see where that strategy becomes unusable

[Hirotaka Sato]

The following is a single-file version in which simp only [h] makes no progress.

https://github.com/hsjoihs/dpda-lean/tree/motive_is_not_type_correct_and_simp_also_fails

[Hirotaka Sato]

commit 570543074eb9fff0e3cccd391e36e41080497402 still fails to adopt simp only [h]

https://github.com/hsjoihs/dpda-lean/blob/570543074eb9fff0e3cccd391e36e41080497402/Dpda/Main.lean

[Hirotaka Sato]

Commit dced8e5ce64dd174bbefe70374d674986317599f is the best I was able to minimize while retaining both rw's "motive is not type correct" and simp's "no progress.

https://github.com/hsjoihs/dpda-lean/blob/dced8e5ce64dd174bbefe70374d674986317599f/Dpda/Main.lean

universe u_

abbrev Predet_Transition (Q: Type u_) (S: Type u_) (Γ: Type u_) := Q → (Γ × Q) ⊕ Fin 42

structure Predet_DPDA (Q: Type u_) (S: Type u_) (Γ: Type u_) where
  q0 : Q
  transition : Q → (Γ × Q) ⊕ Fin 42

def Predet_Transition.stepTransition {Q: Type u_} {S: Type u_} {Γ: Type u_}
  (transition: Q → (Γ × Q) ⊕ Fin 42)
  (pwβ: (Q × List S × List Γ))
  : Option ((Q × List S × List Γ)) := match transition pwβ.1 with
  | Sum.inl (γ, q) => some ⟨q, pwβ.2.1, γ :: pwβ.2.2⟩
  | Sum.inr f => sorry

def Predet_DPDA.stepTransition {Q: Type u_} {S: Type u_} {Γ: Type u_}
  (M: Predet_DPDA Q S Γ)
  (pwβ: (Q × List S × List Γ))
  : Option ((Q × List S × List Γ)) :=
  Predet_Transition.stepTransition M.transition pwβ

structure Sipser_PreDPDA (Q S Γ) where
  q0 : Q
  transition : Q × Option S × Option Γ -> Option (Q × Option Γ)

def exactly_one_some {α}
  (o1 : Option α)
  (o2 : Option α)
  (o3 : Option α)
  (o4 : Option α) := match o1, o2, o3, o4 with
  | some _, none, none, none => true
  | none, some _, none, none => true
  | none, none, some _, none => true
  | none, none, none, some _ => true
  | _, _, _, _ => false

structure Sipser_DPDA(Q S Γ) where
  pda : Sipser_PreDPDA Q S Γ
  deterministic : ∀ q a x,
    exactly_one_some
      (pda.transition (q, some a, some x))
      (pda.transition (q, some a, none))
      (pda.transition (q, none, some x))
      (pda.transition (q, none, none))

def Sipser_DPDA.stepTransition {Q S Γ} (M: Sipser_DPDA Q S Γ) (pwβ: (Q × List S × List Γ)) : Option ((Q × List S × List Γ)) :=
  match hεε : M.pda.transition (pwβ.1, none, none) with
  | some (r, y) => some ⟨ r, pwβ.2.1, y.toList ++ pwβ.2.2 ⟩
  | none =>
    match pwβ.2.1, pwβ.2.2 with
    | [], [] => none
    | [], x :: xs =>
      match h2 : M.pda.transition (pwβ.1, none, some x) with
      | some (r, y) => some ⟨ r, pwβ.2.1, y.toList ++ xs ⟩
      | none => none
    | a :: ws, [] =>
      match h2 : M.pda.transition (pwβ.1, some a, none) with
      | some (r, y) => some ⟨ r, ws, y.toList ++ pwβ.2.2 ⟩
      | none => none
    | a :: ws, x :: xs =>
      match
        hax : (M.pda.transition (pwβ.1, some a, some x)),
        haε : (M.pda.transition (pwβ.1, some a, none)),
        hεx : (M.pda.transition (pwβ.1, none, some x)) with
      | some (r, y), none, none => some ⟨ r, ws, y.toList ++ xs ⟩
      | none, some (r, y), none => some ⟨ r, pwβ.2.1, y.toList ++ xs ⟩
      | none, none, some (r, y) => some ⟨ r, ws, y.toList ++ pwβ.2.2 ⟩
      | some _, some _, some _ => False.elim <| by have h3 := M.deterministic pwβ.1 a x; simp [exactly_one_some, hεε, hax, haε, hεx] at h3
      | some _, some _, none   => False.elim <| by have h3 := M.deterministic pwβ.1 a x; simp [exactly_one_some, hεε, hax, haε, hεx] at h3
      | some _, none, some _   => False.elim <| by have h3 := M.deterministic pwβ.1 a x; simp [exactly_one_some, hεε, hax, haε, hεx] at h3
      | none, some _, some _   => False.elim <| by have h3 := M.deterministic pwβ.1 a x; simp [exactly_one_some, hεε, hax, haε, hεx] at h3
      | none, none, none       => False.elim <| by have h3 := M.deterministic pwβ.1 a x; simp [exactly_one_some, hεε, hax, haε, hεx] at h3

def Predet_DPDA.toSipser {Q S Γ} [DecidableEq Q] (M: Predet_DPDA Q S Γ) : Sipser_DPDA (Option Q) S Γ :=
  let ⟨ q0, dot_delta ⟩ := M
  let sipser_delta_curried : (Option Q) → Option Γ → Option S → Option (Option Q × Option Γ) :=
    fun p_ => match p_ with
     | none => sorry
     | some p =>
       match dot_delta p with
        | Sum.inl (α, q) => sorry
        | Sum.inr fΓ_wS => sorry
  let is_deterministic := sorry
  ⟨
    ⟨
    some q0,
    fun (p, input_consumption, stack_consumption) => sipser_delta_curried p stack_consumption input_consumption
    ⟩,
    is_deterministic
  ⟩

theorem Predet_to_Sipser_preserves_semantics_single_step {Q S Γ}
  [DecidableEq Q] [DecidableEq Γ]
  (M: Predet_DPDA Q S Γ) (idesc: (Q × List S × List Γ)) :
  (fun ⟨ p, w, β ⟩ => ⟨ some p, w, β ⟩) <$> M.stepTransition idesc = M.toSipser.stepTransition (idesc |> fun ⟨ p, w, β ⟩ => ⟨ some p, w, β ⟩) := by
  simp [Functor.map]
  match h : M.transition idesc.1 with
  | Sum.inl (α, q) =>
    simp [Predet_DPDA.toSipser, Predet_DPDA.stepTransition, Sipser_DPDA.stepTransition]
    rw [h] -- This is where I got `motive is not type correct`
  | Sum.inr fΓ_wS => sorry

[Aaron Liu]

Maybe try split and then invalidate the .inr case?

[Hirotaka Sato]

I was able to make progress with split. Thank you!!!

https://github.com/hsjoihs/dpda-lean/blob/7ba5801fd9dd3bc7d67f3cb52d3aa87358d5e99a/Dpda/Conversion/PredetToSipser.lean#L221-L238