# Proving with non-structural recursion in Lean4

I've defined a function (foldMem below) that Lean compiles into a brecOn eliminator. I need to reason with it later on, so I'm trying to prove a couple of lemmas to do so, but I'm stuck trying to prove the recursion lemma (foldMem.step).

The equation compiler generates such theorems internally. They are not meant to be used directly by the user; rather, the simp tactic is configured to use them when necessary.

but simp does not work for me with foldMem

import Std.Data.AssocList
open Std (AssocList)

namespace Std.AssocList

inductive Mem : α → β → AssocList α β → Prop
| head (k : α) (v : β) (tail : AssocList α β) : AssocList.Mem k v $$AssocList.cons k v tail | tail (k : α) (v : β) {k2 : α} {v2 : β} {tail : AssocList α β} (pf : AssocList.Mem k v tail) : AssocList.Mem k v$$ AssocList.cons k2 v2 tail

def Folder (as : AssocList α β) (δ : Type) := δ → (a : α) → (b : β) → AssocList.Mem a b as → δ

def foldMem (as : AssocList α β) (f : Folder as δ) (init : δ) : δ :=
let rec go : (xs : AssocList α β) → δ → ({a : α} → {b : β} → AssocList.Mem a b xs → AssocList.Mem a b as) → δ
| AssocList.nil, acc, _ => acc
| AssocList.cons a b tail, acc, pf => go tail (f acc a b (pf $$AssocList.Mem.head ..)) (λ mem => pf$$ AssocList.Mem.tail _ _ mem)
go as init id

def foldMem.init (f : @Folder α β nil δ) (init : δ) : foldMem nil f init = init :=
by simp [foldMem, go]

def foldMem.step (as : AssocList α β) (k : α) (v : β) (f : Folder (cons k v as) δ) (init : δ) :
(foldMem (cons k v as) f init) =
(foldMem as (λ d a b mem => f d a b <| Mem.tail a b mem) (f init k v <| Mem.head k v as)) :=
by sorry

end Std.AssocList

• Tip: Try to make a complete MWE, including where all the imports are given. There should be no errors except the ones you are asking about. (See leanprover-community.github.io/mwe.html for examples.) Commented Nov 16, 2022 at 0:48
• Thanks. Updated with imports + namespace -- the sorry should now be the only error in lean4 Commented Nov 17, 2022 at 1:11

This isn't a complete solution, but here is how I would think of this. First, your example is a bit complicated (and doesn't compile). I simplified it a bit by just using a List:

inductive Mem : α → List α → Prop
| head (k : α) (tail : List α) : Mem k $$List.cons k tail | tail (k : α) {k2 : α} {tail : List α} (pf : Mem k tail) : Mem k$$ List.cons k2 tail

def Folder (as : List α) (δ : Type) := δ → (a : α) → Mem a as → δ

def foldMem (as : List α) (f : Folder as δ) (init : δ) : δ :=
let rec go : (xs : List α) → δ → ({a : α} → Mem a xs → Mem a as) → δ
| List.nil, acc, _ => acc
| List.cons a tail, acc, pf => go tail (f acc a (pf $$Mem.head ..)) (λ mem => pf$$ Mem.tail _ mem)
go as init id

def foldMem.init (f : @Folder α List.nil δ) (init : δ) : foldMem List.nil f init = init :=
by simp [foldMem, foldMem.go]

def foldMem.step (as : List α) (k : α) (f : Folder (List.cons k as) δ) (init : δ) :
(foldMem (List.cons k as) f init) =
(foldMem as (λ d a mem => f d a <| Mem.tail a mem) (f init k <| Mem.head k as)) :=
by sorry


The helper lemmas for foldMem.go don't get created right away. But since I used foldMem.go in a proof above, now I can see four lemmas associated with foldMem.go:

#check foldMem.go.
-- foldMem.go._eq_1
-- foldMem.go._eq_2
-- foldMem.go.proof_1
-- foldMem.go.proof_2


The first two are what you are looking for, especially _eq_2.

#print foldMem.go._eq_2
-- private theorem foldMem.go._eq_2.{u_1} : ∀ {α : Type u_1} {δ : Type} (as : List α) (f : Folder as δ) (_fun_discr : δ)
--   (a : α) (tail : List α) (pf : ∀ {a_1 : α}, Mem a_1 (a :: tail) → Mem a_1 as),
--   foldMem.go as f (a :: tail) _fun_discr pf =
--     foldMem.go as f tail (f _fun_discr a (_ : Mem a as)) (_ : ∀ {a : α}, Mem a tail → Mem a as)


(See the note at the bottom of this answer about the _s.) You should never call go._eq_2 directly, but it is good to at least know what it says. As for your lemma, let's look at it again after we apply simp to strip away the foldMem:

def foldMem.step (as : List α) (k : α) (f : Folder (List.cons k as) δ) (init : δ) :
(foldMem (List.cons k as) f init) =
(foldMem as (λ d a mem => f d a <| Mem.tail a mem) (f init k <| Mem.head k as)) :=
by
simp [foldMem]
-- α: Type ?u.2152
-- δ: Type
-- as: List α
-- k: α
-- f: Folder (k :: as) δ
-- init: δ
-- ⊢ go (k :: as) f (k :: as) init (_ : ∀ {a : α}, Mem a (k :: as) → Mem a (k :: as)) =
--   go as (fun d a mem => f d a (_ : Mem a (k :: as))) as (f init k (_ : Mem k (k :: as)))
--     (_ : ∀ {a : α}, Mem a as → Mem a as)


You can start to see subtle differences between your lemma and the automatic go._eq_2. I didn't take the time to see if your lemma is correct, or if it can be easily modified into go._eq_2, but if your lemma is correct then it should be provable by induction, possibly with some additional helper lemmas to get you started. You will have to massage the theorem to be of the right form to apply the automatic go._eq_2 theorem. Here is how to start the induction on your lemma:

def foldMem.step (as : List α) (k : α) (f : Folder (List.cons k as) δ) (init : δ) :
(foldMem (List.cons k as) f init) =
(foldMem as (λ d a mem => f d a <| Mem.tail a mem) (f init k <| Mem.head k as)) :=
by
induction as with
| nil => rfl
| cons head tail ih =>
-- case cons
-- α: Type ?u.1797
-- δ: Type
-- k: α
-- init: δ
-- tail: List α
-- ih: ∀ (f : Folder (k :: tail) δ),
--   foldMem (k :: tail) f init =
--     foldMem tail (fun d a mem => f d a (_ : Mem a (k :: tail))) (f init k (_ : Mem k (k :: tail)))
-- f: Folder (k :: head :: tail) δ
-- ⊢ foldMem (k :: head :: tail) f init =
--   foldMem (head :: tail) (fun d a mem => f d a (_ : Mem a (k :: head :: tail)))
--     (f init k (_ : Mem k (k :: head :: tail)))


If it was me, I would find the "step" theorem most closely matching the automatic go lemmas, and then use that to prove other useful theorems. (Also, I might even just move go outside the definition to make it easier to work with directly, but of course your question is specifically how to work with it if it is inside the definition.)

Edit: In this particular example, proofs inside definitions are involved. Sometimes the Lean pretty printer hides proofs as in, e.g. (_ : Mem a (k :: tail))) above. To see the proof that _ refers to, use set_option pp.proofs true.

Edit 2: I'm not actually sure induction is needed since your step function is already supposed to be the induction/recursion step, but I haven't thought it through.

Edit 3: The foldMem.init is actually just provable with by rfl and I wonder if the "correct" foldMem.step lemma would be as well. In that case, you wouldn't need to mention the internal go auxiliary function at all.

Thanks to Jason Rute's suggestions, I was able to solve the issue. The challenge I was running into was that go closed over f and as, and my step lemma was trying to to 'throw away' the outer values. By moving go into an auxiliary definition and rejiggering the recursion, I got rid of the closure and the proof did indeed go through with just rfl

import Std.Data.AssocList
open Std (AssocList)

namespace Std.AssocList

inductive Mem : α → β → AssocList α β → Prop
| head (k : α) (v : β) (tail : AssocList α β) : AssocList.Mem k v $$AssocList.cons k v tail | tail (k : α) (v : β) {k2 : α} {v2 : β} {tail : AssocList α β} (pf : AssocList.Mem k v tail) : AssocList.Mem k v$$ AssocList.cons k2 v2 tail

def Folder (as : AssocList α β) (δ : Type) := δ → (a : α) → (b : β) → AssocList.Mem a b as → δ

def foldMem.aux (xs: AssocList α β) (acc: δ) (g: δ → (a : α) → (b : β) → AssocList.Mem a b xs → δ): δ :=
match xs with
| AssocList.nil => acc
| AssocList.cons a b tail => foldMem.aux tail (g acc a b <| AssocList.Mem.head ..)
(λ acc' a' b' mem' => g acc' a' b' <| AssocList.Mem.tail _ _ mem')

def foldMem (as : AssocList α β) (f : Folder as δ) (init : δ) : δ :=
foldMem.aux as init f

def foldMem.init (f : @Folder α β nil δ) (init : δ) : foldMem nil f init = init :=
by rfl

def foldMem.step (as : AssocList α β) (headk : α) (headv : β) (f : Folder (cons headk headv as) δ) (init : δ) :