match don't rewrite context

Stream: lean4

[Ryan Lahfa]

In this example, I expect that match will rewrite correct signature to change argument by A.pair a b :: q, but it didn't, is that expected?

inductive KrivineInstruction
| Access (n: Nat)
| Grab (next: KrivineInstruction)
| Push (next: KrivineInstruction) (continuation: KrivineInstruction)

inductive KrivineClosure
| pair (i: KrivineInstruction) (e: List KrivineClosure)

def KrivineEnv := List KrivineClosure

def List.max: List Nat → Nat
| [] => 0
| x :: q => Nat.max x (max q)

partial def KrivineClosure.depthUnsafe: KrivineClosure -> Nat
| KrivineClosure.pair i env => List.max (List.map depthUnsafe env) + 1

set_option codegen false in
@[implementedBy KrivineClosure.depthUnsafe]
def KrivineClosure.depth: KrivineClosure -> Nat :=
fun closure => by induction closure with
| pair i env depth_env => exact depth_env + 1
| nil => exact 0
| cons head tail head_depth tail_depth => exact Nat.max head_depth tail_depth

namespace KrivineEnv
def depth: KrivineEnv -> Nat
| [] => 0
| closure :: closures => Nat.max (KrivineClosure.depth closure + 1) (depth closures + 1)

def depth_spec₁: ∀ (c: KrivineInstruction) (x: KrivineEnv) (q: KrivineEnv),
  measure depth q (KrivineClosure.pair c x :: q) :=
fun c x q => by admit
def depth_spec₂: ∀ (c: KrivineInstruction) (x: KrivineEnv) (q: KrivineEnv),
  measure depth x (KrivineClosure.pair c x :: q) :=
fun c x q => by admit

def depth_rel: KrivineEnv -> KrivineEnv -> Prop := measure depth
def depth_wf: WellFounded (measure depth) := measureWf depth

def correct: KrivineEnv -> Prop :=
WellFounded.fix depth_wf (fun e correct =>
match e with
  | [] => true
  | KrivineClosure.pair c₀ e₀ :: env =>
    have e = KrivineClosure.pair c₀ e₀ :: env := by admit -- here, how can I recover this proposition, or how can I ensure that correct sig is correct?
    (correct e₀ (by rw this; exact depth_spec₂ _ _ _))
    ∧ (correct env (by rw this; exact depth_spec₁ _ _ _))
)
end KrivineEnv

The context under by admit for the e equality.

e : KrivineEnv
correct : (y : KrivineEnv) → measure depth y e → Prop
c₀ : KrivineInstruction
e₀ env : List KrivineClosure
⊢ e = KrivineClosure.pair c₀ e₀ :: env

[Ryan Lahfa]

It looks like a bug, as this correct version works just fine:

def correct: KrivineEnv -> Prop :=
WellFounded.fix depth_wf (fun e =>
match e with
  | [] => (fun _ => true)
  | KrivineClosure.pair c₀ e₀ :: env =>
    fun correct =>
    (correct e₀ (exact depth_spec₂ _ _ _))
    ∧ (correct env (exact depth_spec₁ _ _ _))
)

I'm not sure what is going on, as I would expect introducing e, correct at the same time and then matching over e should rewrite the local context, including correct signature?

[Sebastian Ullrich]

See https://github.com/leanprover/lean4/commit/157ef80c5aa1fb1e3974f75dd9d948c9f803a07f#diff-ab25ed83c2ea2848f158b341863db96230c15bc28f09930a28095b0e2c4d1b15R905-R906

match (generalizing := true) e with

[Ryan Lahfa]

Sebastian Ullrich said:

See https://github.com/leanprover/lean4/commit/157ef80c5aa1fb1e3974f75dd9d948c9f803a07f#diff-ab25ed83c2ea2848f158b341863db96230c15bc28f09930a28095b0e2c4d1b15R905-R906

match (generalizing := true) e with

Ah