How to prove a recursive definition in lean4

Stream: new members

[Shubham Kumar 🦀 (he/him)]

I am looking for a hint as to how I should go about proving a recursive definition, for example I have a recursive definition

  def execute_prog (p : Prog) (prog_len : Nat) (s : Stack) (pc : Nat) : Stack × Nat :=
    if prog_len == pc then (s, pc)
    else
      match p with
      | [] => (s, pc)
      | instr :: instrs =>
        let (s', pc') := execute_instr instr s pc
        execute_prog instrs prog_len s' pc'

it's a function which consumes a program p which is a list of an inductive type so List Instr and it performs operation on the Stack of Ints.

I am able to formalise the theorem statement but the above function is a recursive definition so I am kind of stuck in an unfold hell.
So some pointers on dealing with recursive functions in general would be nice

Thanks and sorry for the stupid question, I'm sure I missed it in TPiL (if it's somewhere addressed in TPiL please point it to me I'll just refer that part)

[Mario Carneiro]

what do you mean proving the definition? A definition is a definition

[Mario Carneiro]

also #mwe if you want people to actually demonstrate with code

[Mario Carneiro]

the short answer is that you theorems about a definition by recursion are proved by induction. You should never have to unfold the recursive definition more than once (in each case)

[Shubham Kumar 🦀 (he/him)]

Mario Carneiro said:

what do you mean proving the definition? A definition is a definition

umm so I phrased that incorrectly I meant proving a theorem statement containing a recursive statement.

Mario Carneiro said:

also #mwe if you want people to actually demonstrate with code

I can give a mwe but I feel guilty when I don't solve it on my own and get a solution but just to not waste anyone's time I'll provide context.

so there is a set of instructions in a list

  def prog_ex : Prog :=
    [
      Instr.dup, -- 0
      Instr.lit 0,  -- 1
      Instr.eq,  -- 2
      Instr.if_ 12, -- 3
      Instr.swap, -- 4
      Instr.lit 1, -- 5
      Instr.add, -- 6
      Instr.swap, -- 7
      Instr.lit 1, -- 8
      Instr.sub, -- 9
      Instr.lit 0, -- 10
      Instr.if_ 0 -- 11
    ]

and the thing I need to prove is that if I pass any stack where m :: n :: stack where m, n >= 0 and stack : List Int
in addition to prog_ex to execute_prog it will always output a stack where the first element is a 0 and second element is (m + n) followed by stack so the result would be 0 :: (m + n) :: stack

so I defined an intermediate definition

  def n_stack (m : Int) (n : Int) (s : Stack) : Stack :=
    Prod.fst $ execute_prog (prog_ex) 12 (m :: n :: s) 0

and this makes the theorem definition easier

  theorem t1
    (s : Stack)
    (m : Int)
    (n : Int)
    (hm : m ≥ 0)
    (hn : n ≥ 0) :
    (0 :: (m + n) :: s) = (n_stack m n s) := by
    unfold n_stack
    match s with
    | [] =>
      unfold execute_prog
      simp
      sorry
    | x :: xs => sorry
    sorry

but unfortunately I couldn't make any progress, sorry if this seems really stupid

[Shubham Kumar 🦀 (he/him)]

when I have tried it with a simple example that usually works but I cannot generalise it

[Mario Carneiro]

I can give a mwe but I feel guilty when I don't solve it on my own and get a solution but just to not waste anyone's time I'll provide context.

An MWE is not your whole problem, it is the part you are stuck on, removed from the context and placed in a self-contained file

[Mario Carneiro]

the difference between providing long explanations as context and providing a short toy version of your problem that compiles is really huge in terms of the speed and volume of responses

[Mario Carneiro]

In order for me to answer your question, I'm going to have to infer the types of all those things you wrote and add sorry everywhere. You can do that much more accurately than I since you have the actual example on hand

[Mario Carneiro]

My impression, from what I can see, is that you shouldn't need to match on s here, you can just simp [n_stack, execute_prog]

[Shubham Kumar 🦀 (he/him)]

Mario Carneiro said:

I can give a mwe but I feel guilty when I don't solve it on my own and get a solution but just to not waste anyone's time I'll provide context.

An MWE is not your whole problem, it is the part you are stuck on, removed from the context and placed in a self-contained file

I'll try to make sure that I am able frame it more precisely, I'm not very good at it. If there are any other resources in addition to mwe that you recommend for framing a precise question please feel free to share, I want to get better at this

[Shubham Kumar 🦀 (he/him)]

Mario Carneiro said:

My impression, from what I can see, is that you shouldn't need to match on s here, you can just simp [n_stack, execute_prog]

I tried simp [n_stack] and when I add simp [n_stack, execute_prog] it crashes my vscode after being non-responsive for a while

I'll try something else

[Shubham Kumar 🦀 (he/him)]

Mario Carneiro said:

In order for me to answer your question, I'm going to have to infer the types of all those things you wrote and add sorry everywhere. You can do that much more accurately than I since you have the actual example on hand

so I can write the types
Stack is List Int
Prog is List Instr
and Instr is an inductive type

  inductive Instr : Type
  | add : Instr
  | sub : Instr
  | eq  : Instr
  | drop : Instr
  | dup  : Instr
  | swap : Instr
  | over : Instr
  | lit  : Int → Instr
  | if_  : Nat → Instr
  deriving Repr

if there are any other types which don't make sense let me know :sweat_smile:

[Shubham Kumar 🦀 (he/him)]

the function execute_instr is

  def execute_instr (i : Instr) (s : Stack) (pc : Nat) : Stack × Nat :=
    match i with
    | Instr.add => nAdd s pc
    | Instr.sub => nSub s pc
    | Instr.eq  => nSub s pc
    | Instr.drop => nDrop s pc
    | Instr.dup => nDup s pc
    | Instr.swap => nSwap s pc
    | Instr.over => nOver s pc
    | Instr.lit i => nLit i s pc
    | Instr.if_ a => nIf a s pc

[Shubham Kumar 🦀 (he/him)]

sorry for making these needlessly complex I kind of feel bad if you want to withdraw from this question I understand :face_with_peeking_eye:

[Kevin Buzzard]

Please please please stop writing text and just post a #mwe if you want an answer. Beginners make all kinds of errors. We need to see fully working code.

[Kevin Buzzard]

Instructions are in the link

[Shubham Kumar 🦀 (he/him)]

yeah I'll try and post a mwe, let me figure it out