deep match behind an Option a structure

Stream: lean4

[Ryan Lahfa]

I'm trying to match what a function does, which itself performs matches, but each time I have to match a mk due to the structure definition, or the context is not quite what I wished for:

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

structure KrivineState where
  code: KrivineInstruction
  env: KrivineEnv
  stack: KrivineEnv

def evalKrivineMachine (state: KrivineState): Option KrivineState :=
match state.code, state.env, state.stack with
| KrivineInstruction.Access 0, (KrivineClosure.pair code recEnv :: closures), stack => some $ KrivineState.mk code recEnv stack
| KrivineInstruction.Access n, (KrivineClosure.pair code recEnv :: closures), stack => some $ KrivineState.mk (KrivineInstruction.Access (n - 1)) closures stack
| KrivineInstruction.Push c' c, env, stack => some $ KrivineState.mk c env (KrivineClosure.pair c' env :: stack)
| KrivineInstruction.Grab code, closures, (KrivineClosure.pair c₀ e₀ :: stack) => some $ KrivineState.mk code (KrivineClosure.pair c₀ e₀ :: closures) stack
| _, _, _ => none


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

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

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 1 + depth_env
| 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 (1 + KrivineClosure.depth closure) (depth closures)

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 => C[List.length e₀](compile.leftInv c₀) ∧ (correct e₀ (by admit)) ∧ (correct env (sorry))
)
end KrivineEnv

def KrivineState.correct (state: KrivineState): Prop :=
  C[List.length state.env](compile.leftInv state.code)
  ∧ (KrivineEnv.correct state.env)
  ∧ (KrivineEnv.correct state.stack)

-- here I want to perform case-analysis on (evalKrivineMachine state0) return.
theorem transitionCorrectness (state₀: KrivineState) (state₁: KrivineState)
  (hTransition: evalKrivineMachine state₀ = state₁): KrivineState.correct state₀ -> KrivineState.correct state₁ :=
by match state₀.code, state₀.env, state₀.stack with
| KrivineInstruction.Access 0, (KrivineClosure.pair code recEnv :: closures), stack => exact sorry
| KrivineInstruction.Access n, (KrivineClosure.pair code recEnv :: closures), stack => exact sorry
| KrivineInstruction.Push c' c, env, stack => exact sorry
| KrivineInstruction.Grab code, closures, (KrivineClosure.pair c₀ e₀ :: stack) => exact sorry
| _, _, _ => exact sorry

But, neither approach I use enable me to match properly the return of evalKrivineMachine, BTW, is it expected that evalKrivineMachine state_0 = state_1 is smart enough to know that it is in fact: evalKrivineMachine state_0 = some state_1 (which the context shows!) ?

[Ryan Lahfa]

Ryan Lahfa said:

I'm trying to match what a function does, which itself performs matches, but each time I have to match a mk due to the structure definition, or the context is not quite what I wished for:

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

structure KrivineState where
  code: KrivineInstruction
  env: KrivineEnv
  stack: KrivineEnv

def evalKrivineMachine (state: KrivineState): Option KrivineState :=
match state.code, state.env, state.stack with
| KrivineInstruction.Access 0, (KrivineClosure.pair code recEnv :: closures), stack => some $ KrivineState.mk code recEnv stack
| KrivineInstruction.Access n, (KrivineClosure.pair code recEnv :: closures), stack => some $ KrivineState.mk (KrivineInstruction.Access (n - 1)) closures stack
| KrivineInstruction.Push c' c, env, stack => some $ KrivineState.mk c env (KrivineClosure.pair c' env :: stack)
| KrivineInstruction.Grab code, closures, (KrivineClosure.pair c₀ e₀ :: stack) => some $ KrivineState.mk code (KrivineClosure.pair c₀ e₀ :: closures) stack
| _, _, _ => none


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

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

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 1 + depth_env
| 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 (1 + KrivineClosure.depth closure) (depth closures)

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 => (correct e₀ (by admit)) ∧ (correct env (sorry))
)
end KrivineEnv

def KrivineState.correct (state: KrivineState): Prop :=
   (KrivineEnv.correct state.env)
  ∧ (KrivineEnv.correct state.stack)

-- here I want to perform case-analysis on (evalKrivineMachine state0) return.
theorem transitionCorrectness (state₀: KrivineState) (state₁: KrivineState)
  (hTransition: evalKrivineMachine state₀ = state₁): KrivineState.correct state₀ -> KrivineState.correct state₁ :=
by match state₀.code, state₀.env, state₀.stack with
| KrivineInstruction.Access 0, (KrivineClosure.pair code recEnv :: closures), stack => exact sorry
| KrivineInstruction.Access n, (KrivineClosure.pair code recEnv :: closures), stack => exact sorry
| KrivineInstruction.Push c' c, env, stack => exact sorry
| KrivineInstruction.Grab code, closures, (KrivineClosure.pair c₀ e₀ :: stack) => exact sorry
| _, _, _ => exact sorry

But, neither approach I use enable me to match properly the return of evalKrivineMachine, BTW, is it expected that evalKrivineMachine state_0 = state_1 is smart enough to know that it is in fact: evalKrivineMachine state_0 = some state_1 (which the context shows!) ?

So to answer myself, I can match the mk constructor then rematch the variables.
Though, I'm still running into issues because it looks like Lean 4 is not able to eliminate an match after a simp, I'm getting this in my goal:

some function (match KrivineInstruction.Access 0, KrivineClosure.pair code recEnv :: closures, stack with
            | KrivineInstruction.Access 0, KrivineClosure.pair code recEnv :: closures, stack =>
              some { code := code, env := recEnv, stack := stack }
            | KrivineInstruction.Access n, KrivineClosure.pair code recEnv :: closures, stack =>
              some { code := KrivineInstruction.Access (n - 1), env := closures, stack := stack }
            | KrivineInstruction.Push c' c, env, stack =>
              some { code := c, env := env, stack := KrivineClosure.pair c' env :: stack }
            | KrivineInstruction.Grab code, closures, KrivineClosure.pair c₀ e₀ :: stack =>
              some { code := code, env := KrivineClosure.pair c₀ e₀ :: closures, stack := stack }
            | x, x_1, x_2 => none).code

And I think it can be simplified to some { code := code, env := recEnv, stack := stack } but I'm not sure how to debug this further.

[Ryan Lahfa]

Okay, I have a very simple repro:

inductive A
| A (n: Nat)
| B (n: A)

inductive C
| pair (i: A) (e: List C)

def D := List C

structure S where
  a: A
  b: D
  c: D

def eval (state: S): Option S :=
match state.a, state.b, state.c with
| A.A 0, (C.pair c subExpr :: tail), stack =>
  some $ S.mk c subExpr stack
| A.A (Nat.succ n), (C.pair c subExpr :: tail), stack =>
  some $ S.mk (A.A n) tail stack
| A.B c, env, stack =>
  some $ S.mk c env stack
| _, _, _ =>
  none

def test_0: eval { a := A.A 0, b := [C.pair (A.A 1) []], c := [] } = some { a := A.A 1, b := [], c := []} :=
by
simp [eval]

In my code, I would like to reduce the lhs into rhs, so simp [eval] turns into:

match A.A 0, [C.pair (A.A 1) []], [] with
    | A.A 0, C.pair c subExpr :: tail, stack => some { a := c, b := subExpr, c := stack }
    | A.A (Nat.succ n), C.pair c subExpr :: tail, stack => some { a := A.A n, b := tail, c := stack }
    | A.B c, env, stack => some { a := c, b := env, c := stack }
    | x, x_1, x_2 => none) =
    some { a := A.A 1, b := [], c := [] }

At any moment, this proof can be closed by rfl, but if I'm in a case where I would like to exploit the reduction, I would need to inject have: eval $a = $target := by rfl and use it. Is there any way to reuse simp here?

[Ryan Lahfa]

Ha, have is not working

[Ryan Lahfa]

This:

inductive A
| A (n: Nat)
| B (n: A)

inductive C
| pair (i: A) (e: List C)

def D := List C

structure S where
  a: A
  b: D
  c: D

def eval (state: S): Option S :=
match state.a, state.b, state.c with
| A.A 0, (C.pair c subExpr :: tail), stack =>
  some $ S.mk c subExpr stack
| A.A (Nat.succ n), (C.pair c subExpr :: tail), stack =>
  some $ S.mk (A.A n) tail stack
| A.B c, env, stack =>
  some $ S.mk c env stack
| _, _, _ =>
  none

def test_0: eval { a := A.A 0, b := [C.pair (A.A 1) []], c := [] } = some { a := A.A 1, b := [], c := []} :=
by
have eval { a := A.A 0, b := [C.pair (A.A 1) []], c := [] } = some $ { a := A.A 1, b := [], c := [] } := by rfl
exact this

Context:

unsolved goals
⊢ ?m.1228 = ?m.1228

[Ryan Lahfa]

I don't understand how to debug this kind of issue as it looks like all unification are succeeding:

[Meta.isDefEq]
    [Meta.isDefEq.step] ?m.1157 =?= ?m.1157
    [Meta.isDefEq] ?m.1157 =?= ?m.1157 ... success
  [Meta.isDefEq]
    [Meta.isDefEq.step] eval { a := A.A 0, b := [C.pair (A.A 1) []] } =
      some { a := A.A 1, b := [] } =?= eval { a := A.A 0, b := [C.pair (A.A 1) []] } = some { a := A.A 1, b := [] }
    [Meta.isDefEq] eval { a := A.A 0, b := [C.pair (A.A 1) []] } =
      some
        { a := A.A 1,
          b := [] } =?= eval { a := A.A 0, b := [C.pair (A.A 1) []] } = some { a := A.A 1, b := [] } ... success
[Meta.isDefEq]
  [Meta.isDefEq.step] eval { a := A.A 0, b := [C.pair (A.A 1) []] } =
    some { a := A.A 1, b := [] } =?= eval { a := A.A 0, b := [C.pair (A.A 1) []] } = some { a := A.A 1, b := [] }
  [Meta.isDefEq] eval { a := A.A 0, b := [C.pair (A.A 1) []] } =
    some
      { a := A.A 1,
        b := [] } =?= eval { a := A.A 0, b := [C.pair (A.A 1) []] } = some { a := A.A 1, b := [] } ... success
invalid pattern
[Meta.isDefEq]
    [Meta.isDefEq.step] ?m.1157 =?= ?m.1164 = ?m.1164
    [Meta.isDefEq] ?m.1157 [assignable] =?= ?m.1164 = ?m.1164 [nonassignable]
      [Meta.isDefEq.assign]
        [Meta.isDefEq.assign] ?m.1157 := ?m.1164 = ?m.1164
        [Meta.isDefEq.assign.beforeMkLambda] ?m.1157 [] := ?m.1164 = ?m.1164
        [Meta.isDefEq.assign.checkTypes]
          [Meta.isDefEq.step] Sort ?u.1156 =?= Prop
          [Meta.isDefEq.assign.final] ?m.1157 := ?m.1164 = ?m.1164
    [Meta.isDefEq] ?m.1164 = ?m.1164 =?= ?m.1164 = ?m.1164 ... success
[Meta.isDefEq]
  [Meta.isDefEq.step] ?m.1164 = ?m.1164 =?= ?m.1164 = ?m.1164
  [Meta.isDefEq] ?m.1164 = ?m.1164 =?= ?m.1164 = ?m.1164 ... success

[Ryan Lahfa]

Elaborator traces seems to show:

[Elab.app.args] explicit: false, rfl : ∀ {α : Sort ?u.1162} {a : α}, a = a
  [Elab.app.finalize] rfl
  [Elab.app.finalize] after etaArgs, rfl : ?m.1164 = ?m.1164
  [Elab.app.finalize] expected type: ?m.1157

So if I understand well, ?m.1164 is α ?

[Mac]

Shouldn't:

have eval { a := A.A 0, b := [C.pair (A.A 1) []] } = some { a := A.A 1, b := [] } := by rfl

be:

have : eval { a := A.A 0, b := [C.pair (A.A 1) []] } = some { a := A.A 1, b := [] } := by rfl

That is, with a colon (and maybe with a name for the hypothesis) -- or I am missing something? I would think that is why you are getting "invalid pattern".

[Ryan Lahfa]

Mac said:

Shouldn't:

have eval { a := A.A 0, b := [C.pair (A.A 1) []] } = some { a := A.A 1, b := [] } := by rfl

be:

have : eval { a := A.A 0, b := [C.pair (A.A 1) []] } = some { a := A.A 1, b := [] } := by rfl

That is, with a colon (and maybe with a name for the hypothesis) -- or I am missing something? I would think that is why you are getting "invalid pattern".

In Lean 4, it is not AFAIK.
Your addition creates expected identifier error

[Mac]

It might need to be named in Lean 4? That is:

have h : eval { a := A.A 0, b := [C.pair (A.A 1) []] } = some { a := A.A 1, b := [] } := by rfl

That's what I would expect from the "expected identifier" error.

[Ryan Lahfa]

Mac said:

It might need to be named in Lean 4? That is:

have h : eval { a := A.A 0, b := [C.pair (A.A 1) []] } = some { a := A.A 1, b := [] } := by rfl

That's what I would expect from the "expected identifier" error.

Surprisingly, it works, but I do not understand why the "no name" version fails as it has worked at some other points. Though, that indeed solves most of my issues.

I can also do have $type from $proof to have a this local decl.