Chapter 7 Exercise 3 Theorem Proving in Lean4

Stream: new members

[Ram]

Hello everyone, I'm following the "Theorem Proving in Lean4" book and I got pretty stuck on an exercise.

Define an inductive data type consisting of terms built up from the following constructors: const n, a constant denoting the natural number n var n, a variable, numbered n plus s t, denoting the sum of s and t times s t, denoting the product of s and t Recursively define a function that evaluates any such term with respect to an assignment of values to the variables.

Here is what I have so far:

inductive Expr : (vars: List Nat) → Type u
  | const (n : Nat) : Expr []
  | var (n : Nat) : Expr [n]
  | plus (s : Expr vars₁) (t : Expr vars₂) : Expr (vars₁ ++ vars₂)
  | times (s : Expr vars₁) (t : Expr vars₂) : Expr (vars₁ ++ vars₂)

def eval
  {vars : List Nat}
  (expr : Expr vars)
  (assignment : List Nat)
  (h : vars.length = assignment.length) : Nat :=
  match expr with
  | Expr.const n => n
  | Expr.var n =>
    let h₁ : assignment ≠ [] := by
      intro h₁
      rw [List.eq_nil_iff_length_eq_zero, ←h] at h₁
      contradiction
    assignment.head h₁
  | @Expr.plus vars₁ vars₂ s t =>
    let assignment₁ : List Nat := List.take vars₁.length assignment
    let assignment₂ : List Nat := List.drop vars₁.length assignment
    let h₁ : vars₁.length = assignment₁.length := sorry
    let h₂ : vars₂.length = assignment₂.length := sorry
    (eval s assignment₁ h₁) + (eval t assignment₂ h₂)
  | @Expr.times vars₁ vars₂ s t =>
    let assignment₁ : List Nat := List.take vars₁.length assignment
    let assignment₂ : List Nat := List.drop vars₁.length assignment
    let h₁ : vars₁.length = assignment₁.length := sorry
    let h₂ : vars₂.length = assignment₂.length := sorry
    (eval s assignment₁ h₁) + (eval t assignment₂ h₂)

I don't know how to prevent double reassignment to variables without a "Set" type. I would like to refrain from importing it from Mathlib if possible.
In general advice and feedback on the code would be appreciated

[Henrik Böving]

The task does not have any variable assignments, the idea is to use a mapping Nat -> Nat and carry it through without modifications. There is also no need to make your type indexed over anything.

[Ram]

Thank you!