Cannot rewrite term being cased on

Stream: lean4

[James Gallicchio]

I've been trying for a while to step through a match expression in a proof, but the rewrite that should be succeeding is not.

Here, I'm trying to rewrite the LazyList.force F to none with h', so that I can step through the match. rw [h'] fails:

tactic 'rewrite' failed, motive is not type correct
τ : Type ?u.3819
F : LazyList τ
F_len : Nat
R : LazyList τ
R_len : Nat
...
h' : LazyList.force F = none
...
⊢ (match LazyList.force F, (_ : LazyList.force F = LazyList.force F) with
    | some (x, F'), h =>
      some (x, LBQueue.balance F' (F_len - 1) R R_len (_ : LazyList.length F' = F_len - 1 ∧ LazyList.length R = R_len))
    | none, h => none) =
    none

Full code is here
(sorry for the not-MWE, I can't figure out how to get this issue to appear elsewhere :sad:)

[James Gallicchio]

I can spend some more time trying to find an MWE if the issue is too unintelligible like this

[Kevin Buzzard]

Try cases h'? In lean 3 this would probably make progress, as would subst h'.

[Mario Carneiro]

I believe split should work in this case. (Lean 4 split is like split_ifs from lean 3 but it also works on matches)

[James Gallicchio]

Ah, cases h' seems to reveal the issue:

dependent elimination failed, failed to solve equation
  none =
    Acc.rec
      (fun x₁ ac₁ ih =>
        (fun x a =>
            PSigma.casesOn (motive := fun x =>
...

Seems like maybe same issue as this topic

[James Gallicchio]

Huh, so even after the other topic was resolved, this is still having trouble. Weirdly if I just case on F.force again (and eliminate one case via contradiction) it works... I just can't directly rewrite into the match, nor split on it

[James Gallicchio]

(Doing cases h' still gives the same dependent elimination failure)

[Mario Carneiro]

can you make a MWE?

[James Gallicchio]

inductive LazyList (α : Type u)
| nil : LazyList α
| cons (hd : α) (tl : LazyList α) : LazyList α
| delayed (t : Thunk (LazyList α)) : LazyList α

namespace LazyList

def force : LazyList α → Option (α × LazyList α)
| delayed as => force as.get
| nil        => none
| cons a as  => some (a,as)

end LazyList


def deq (Q : LazyList τ) : Option (τ × LazyList τ) :=
  match h:Q.force with
  | some (x, F') => some (x, F')
  | none => none

theorem deq_correct (Q : LazyList τ)
  : deq Q = none ↔ Q.force = none
  := by
    cases h':Q.force
    case none =>
      simp [deq]
      cases h'
    sorry

[James Gallicchio]

I think (?) this shows the right behavior

[James Gallicchio]

And this works perfectly fine in replacement of the cases h':

match h'':Q.force with
| none => simp
| some _ =>
  rw [h'] at h''
  contradiction

[James Gallicchio]

wait, no, doing that causes a really strange error at the top level declaration deq_correct ???

[James Gallicchio]

application type mismatch
  deq.match_1 Q fun x h => Option (τ × LazyList τ)
argument has type
  (x : Option (τ × LazyList τ)) → x✝ = x → Type u_1
but function has type
  (motive : (x : Option (τ × LazyList τ)) → LazyList.force Q = x → Type u_1) →
    (x : Option (τ × LazyList τ)) →
      (h : LazyList.force Q = x) →
        ((x : τ) → (F' : LazyList τ) → (h : LazyList.force Q = some (x, F')) → motive (some (x, F')) h) →
          ((h : LazyList.force Q = none) → motive none h) → motive x h

[Leonardo de Moura]

Ideally we would want to write

theorem deq_correct (Q : LazyList τ) : deq Q = none ↔ Q.force = none := by
  simp [deq]
  cases Q.force <;> simp

or

theorem deq_correct (Q : LazyList τ) : deq Q = none ↔ Q.force = none := by
  simp [deq]
  split <;> simp

Both cases Q.force and split fail when trying to generalize Q.force. Auxiliary declarations (deq.match_1 and deq.proof_1) created by Lean are preventing generalize from creating a type correct term. deq.match_1 is an auxiliary declaration used to represent the match expression in deq, and deq.proof_1 is used by Lean when "hiding" all proof terms nested in a definition. We can work around these issues by unfolding these definitions.

theorem deq_correct (Q : LazyList τ) : deq Q = none ↔ Q.force = none := by
  simp [deq]
  unfold deq.match_1
  unfold deq.proof_1
  cases Q.force <;> simp

We will try to improve generalize and how we encode match expressions to avoid these workarounds in the future.

[James Gallicchio]

Trying to apply this workaround in more complicated situations I'm a bit lost again... Here's an MWE that's closer to my actual application:

inductive LazyList (α : Type u)
| nil : LazyList α
| cons (hd : α) (tl : LazyList α) : LazyList α
| delayed (t : Thunk (LazyList α)) : LazyList α

namespace LazyList

def force : LazyList α → Option (α × LazyList α)
| delayed as => force as.get
| nil        => none
| cons a as  => some (a,as)

def length : LazyList α → Nat
| nil        => 0
| cons _ as  => length as + 1
| delayed as => length as.get

theorem F_force_some_len_minus_one {L L' : LazyList α}
  : L.force = some (a, L') → L'.length = L.length - 1
  := sorry

end LazyList

structure LazyBatchQueue (τ) :=
  F : LazyList τ
  F_len : Nat
  h_lens : F.length = F_len


def deq (Q : LazyBatchQueue τ) : Option (τ × LazyBatchQueue τ) :=
  match h:Q.F.force with
  | some (x, F') =>
    some (x,
      ⟨F', Q.F_len - 1,
        by simp [LazyList.F_force_some_len_minus_one h, Q.h_lens]⟩)
  | none => none

theorem deq_correct (Q : LazyBatchQueue τ)
  : deq Q = none ↔ Q.F.force = none
  := by
    simp [deq]
    unfold deq.match_1
    unfold deq.proof_1
    unfold deq.proof_2
    match h':Q.F.force with
    | none => simp
    | some _ => simp

The biggest difference from the last is that now we are carrying around a proof term with the queue structure (so perhaps that's causing other proof-erasing definitions to be generated?).

The same proof as before (which I think should in principle still work) fails with a reference to deq.proof_2, so I tried unfolding that also, but now it generates a type incorrect term because it is generalizing Q.F.force within the proof term from the implementation of deq...

Is there a consistent way to apply this workaround? I can also just leave sorrys until the behavior improves, since it isn't urgent.

[Mario Carneiro]

My old standby for solving this situation in lean 3 still works in lean 4: Write the generalization motive explicitly. It's not pretty but it works when you have messy dependencies

theorem deq_correct (Q : LazyBatchQueue τ)
  : deq Q = none ↔ Q.F.force = none
  := by
    simp [deq]
    suffices ∀ o h, deq.match_1 Q (fun x h => _) o h _ _ = none ↔ _ from this _ rfl
    intros o h
    cases o <;> simp [h]

[James Gallicchio]

Oh boy, okay -- let me try to parse what that's doing

[Mario Carneiro]

the basic idea is that we are simultaneously generalizing Q.F.forceand rfl : Q.F.force = Q.F.force because the rfl proof is what prevents us from generalizing Q.F.force. These two are passed as arguments to deq.match_1, which already states the generalized type of h : Q.F.force = o, so if we introduce them at the same time then we don't get any "motive is not type correct" issues

[Mario Carneiro]

(It helps to set set_option pp.match false to see what the actual match application looks like)

[James Gallicchio]

Sorry for dragging up an old thread — I’m back to trying to figure this out.

[James Gallicchio]

Where are the proof_i terms used in the match encoding? Even with pp.match off and pp.all on they don’t appear anywhere — is it only occurring in the proof of the relevant proposition?

[James Gallicchio]

(Trying to understand why those need to be unfolded/what it’s doing when I unfold those)

[Leonardo de Moura]

@James Gallicchio We discussed this issue in the dev channel. To provide a better experience for users, we have to change how we encode match expressions. This is on our TODO list, but it will not happen in the next two months. We have a tutorial at the end of May, and fixing things and adding missing features for it is our current priority. Here are the notes from the dev channel if you are interested.

---

A user wrote the following function.

def deq (Q : LazyList τ) : Option (τ × LazyList τ) :=
  match h:Q.force with
  | some (x, F') => some (x, F')
  | none         => none

The following auxiliary definition is created

@deq.match_1 :
  -- Parameters
  {τ : Type u_1} →
  (Q : LazyList τ) →
  -- Motive
  (motive : (x : Option (τ × LazyList τ)) → LazyList.force Q = x → Sort u_2) →
  -- Discriminants aka major premises
  (x : Option (τ × LazyList τ)) →
  (h : LazyList.force Q = x) →
  -- Alternatives aka minor premises
  ((x : τ) → (F' : LazyList τ) → (h : LazyList.force Q = some (x, F')) → motive (some (x, F')) h) →
  ((h : LazyList.force Q = none) → motive none h) →
  -- Result type
  motive x h

If the goal contains the term deq.match_1 Q <some-motive> (LazyList.force Q) ..., we cannot generalize LazyList.force Q.
The auxiliary definition above follows the structure of kernel recursors where the motive does not depend on the major premises (aka discriminants), but it prevents us from generalizing effectively. We could work karound this particular issue by using a different encoding where the motive depends on the discriminants

 def deq.match
    (τ : Type u)
    (d₁ : Option (τ × LazyList τ))
    (d₂ : d₁ = d₁)
    (motive : (x' : Option (τ × LazyList τ)) → x' = d₁ → Sort v)
    (h₁ : (x : τ) → (F' : LazyList τ) → (h : some (x, F') = d₁) → motive (some (x, F')) h)
    (h₂ : (h : none = d₁) → motive none h)
    : motive d₁ d₂ := by
  cases d₁
  exact h₂ rfl
  exact h₁ _ _ rfl

BTW, I hit similar problems a few times whenever we have match h:t ... where t is not a variable. This kind of match creates a term that cannot be generalized by tactics such as cases and split. The issue also affects any match where the user manually provides a complex motive by hand + discriminants that are not variables. This second scenario is rare since very few people are willing to write complex motives by hand. The problem with match h:t ... is that it makes it super easy for users to create a nontrivial motive. :sweat_smile:
This issue is bothering me :sweat_smile: Here is another encoding that fixes the problem, but does not change the order: parameter, motive, discriminants, alternatives.

def deq.match {τ : Type u} (Q : LazyList τ) (motive : (x : Option (τ × LazyList τ)) → Sort v)
              (d : Option (τ × LazyList τ))
              (h₁ : (x : τ) → (F' : LazyList τ) → (h : d = some (x, F')) → motive (some (x, F')))
              (h₂ : (h : d = none) → motive none)
              : motive d := by
  cases h:d
  . exact h₂ h
  . exact h₁ _ _ h

It removes rfl as a discriminant. In retrospect, it is a bit pointless to take an argument that is always set with rfl.
This fix also avoids the workaround unfold deq.proof_1.
We would need some extra annotation to make sure we can delaborate this kind of match, but the result will be better.
For example, the deq function

def deq (Q : LazyList τ) : Option (τ × LazyList τ) :=
  match h:Q.force with
  | some (x, F') => some (x, F')
  | none => none

is currently delaborated as

def deq.{u_1} : {τ : Type u_1} → LazyList τ → Option (τ × LazyList τ) :=
fun {τ} Q =>
  match LazyList.force Q, (_ : LazyList.force Q = LazyList.force Q) with
  | some (x, F'), h => some (x, F')
  | none, h => none

The output is correct, but it exposes our encoding for h:.

[Evgeniy Kuznetsov]

@Leonardo de Moura, in case you decide it's worth your attention:

example {n: Nat}: True :=
  match h: n with
  | 0     => True.intro
  | n + 1 => by
    trace_state
    exact True.intro

h has type:

. nightly-2022-04-29: h : n✝ = n + 1
. nightly-2022-04-30: h : n✝ = Nat.succ n

[Leonardo de Moura]

@Evgeniy Kuznetsov Thanks for the reporting the discrepancy. I changed how the h : is encoded in to address the issue in this thread and https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/hypothesis.20can't.20be.20used/near/280252919
In the new encoding, h : <discriminant> = <pattern>. The issues in these threads are not fully resolved, I still have to write a new split tactic that takes into account the new encoding, and add support in simp too.
In your example, the discrepancy is on the <pattern> of h : <discriminant> = <pattern>, because x+1 is a pseudo-pattern, and only becomes a "real" pattern after we reduce it to Nat.succ x. The new behavior seems reasonable to me.
I have also noticed discrepancies on the <discriminant>. In the new encoding, it is exactly the discriminant we typed, and in the previous encoding, the <discriminant> would be "refined" by previous patterns.
We want to make sure we have the final encoding before we make the first official Lean 4 release this summer.

[Leonardo de Moura]

Note that you can still simulate previous encoding by manually providing the "motive" for the match.

theorem ex {n: Nat}: True :=
  match (motive := (n' : Nat) → n = n' → _) n, rfl with
  | 0, h     => True.intro
  | y + 1, h => by
    trace_state -- h : n = y + 1
    exact True.intro

[Leonardo de Moura]

BTW, I will be tweaking with the new encoding in the next few days. So, we may have a few more discrepancies.

[Evgeniy Kuznetsov]

Thank you for a comprehensive answer! Just wanted to make sure this is the expected behavior.