Theorem Proving in lean exercise review request

Stream: lean4

[James Sully]

I went a bit crazy doing a version of the expression evaluator exercise from chapter 7 exercise 3 of Theorem Proving.

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.

I've simplified it as much as I know how, does anyone have any suggestions for neatening it?

inductive Expr where
  | const : Nat → Expr
  | var : Nat → Expr
  | plus : Expr → Expr → Expr
  | times : Expr → Expr → Expr

namespace Expr
def varInExpr (n : Nat) (e : Expr) : Prop := match e with
  | const _ => False
  | var m => n = m
  | plus s t => varInExpr n s ∨ varInExpr n t
  | times s t => varInExpr n s ∨ varInExpr n t

def varInEnv (n : Nat) (env : List (Nat × Nat)) : Prop :=
  n ∈ env.map Prod.fst

theorem mem_head_or_tail (x hd : α) (tl : List α) (h : x ∈ hd :: tl)
  : x = hd ∨ x ∈ tl := by
  cases h with
  | head => left; eq_refl
  | tail => right; assumption

def getEnv (key : Nat) (env : List (Nat × Nat)) (ok : varInEnv key env) : Nat :=
  match env with
  | [] => by
    exfalso
    cases ok
  | (key', val) :: rest =>
    have h₂ : key = key' ∨ key ∈ rest.map Prod.fst := by
      exact mem_head_or_tail key key' (List.map Prod.fst rest) ok
    if h₃ : key == key' then
      val
    else
      have ok' : varInEnv key rest := by
        rw [show varInEnv key rest = (key ∈ rest.map Prod.fst) from rfl]
        simp_all
      getEnv key rest ok'

example : varInExpr 3 (var 3) := rfl
example : varInExpr 3 (plus (var 3) (const 10)) := by left; rfl

def eval (env : List (Nat × Nat))
         (expr : Expr)
         (_ : ∀ n, varInExpr n expr → varInEnv n env)
         : Nat :=
  match h₂ : expr with
  | const n => n
  | var i =>
    have : varInExpr i expr := by rw [h₂]; rfl
    have : varInEnv i env := by simp_all only
    getEnv i env ‹varInEnv i env›
  | plus  s t =>
    have sOk : ∀ n, varInExpr n s → varInEnv n env := by
      intro n h₃
      have : varInExpr n (s.plus t) := by left; exact h₃
      simp_all only
    have tOk : ∀ n, varInExpr n t → varInEnv n env := by
      intro n h₃
      have : varInExpr n (s.plus t) := by right; exact h₃
      simp_all only
    eval env s sOk + eval env t tOk
  | times s t =>
    have sOk : ∀ n, varInExpr n s → varInEnv n env := by
      intro n h₃
      have : varInExpr n (s.times t) := by left; exact h₃
      simp_all only
    have tOk : ∀ n, varInExpr n t → varInEnv n env := by
      intro n h₃
      have : varInExpr n (s.times t) := by right; exact h₃
      simp_all only
    eval env s sOk * eval env t tOk

#eval
  let env := [(1, 42)]
  let expr := var 1
  let ok : ∀ n, varInExpr n expr → varInEnv n env := by
    rw [show expr = var 1 from rfl]
    intro n h
    rw [show varInExpr n (var 1) = (n = 1) by rfl] at h
    suffices h₁ : varInEnv n env = (1 ∈ [1]) by rw [h₁]; left
    calc varInEnv n env
      _ = (n ∈ env.map Prod.fst) := rfl
      _ = (n ∈ [1]) := rfl
      _ = (1 ∈ [1]) := by rw [h]

  eval env expr ok

[James Sully]

in particular I'm not happy with the repetition in the plus and times branches of eval

[James Sully]

alternative formulations of varInExpr, varInEnv, or the precondition for eval that make the proofs easier would be welcome as well

[James Sully]

This would obviously be a lot simpler if the env was a Nat -> Nat, or eval returned Option Nat or something, but this is more fun

[Marcus Rossel]

I'm guessing not all of this is relevant to you, but if I wanted to go super fancy I'd do:

import Lean

inductive Expr where
  | const : Nat → Expr
  | var   : Nat → Expr
  | plus  : Expr → Expr → Expr
  | times : Expr → Expr → Expr

namespace Expr

instance : OfNat Expr n where
  ofNat := .const n

prefix:100 "%" => Expr.var

instance : Add Expr where
  add := .plus

instance : Mul Expr where
  mul := .times

def Mem (n : Nat) : Expr → Prop
  | const _            => False
  | %m                 => n = m
  | s + t | .times s t => Mem n s ∨ Mem n t -- We can't use `*` for pattern matching of `.times`: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Mul.20match_pattern

instance : Membership Nat Expr where
  mem := Mem

abbrev Env := List (Nat × Nat)

namespace Env

def Mem (n : Nat) (env : Env) : Prop :=
  n ∈ env.map Prod.fst

instance : Membership Nat Env where
  mem := Env.Mem

theorem Mem.iff_mem (env : Env) : (n ∈ env) ↔ (n ∈ env.map Prod.fst) :=
  Iff.rfl

local macro "get_mem" : tactic => `(tactic| simp_all [Mem.iff_mem])

def get (key : Nat) (env : Env) (_ : key ∈ env := by get_mem) : Nat :=
  let (key', val) :: rest := env
  if _ : key == key' then val else get key rest

def Completes (env : Env) (expr : Expr) : Prop :=
  ∀ n, n ∈ expr → n ∈ env

infixr:50 " ⊢ " => Completes

namespace Completes

theorem var (h : env ⊢ %n) : n ∈ env :=
  h _ rfl

theorem plus_left (h : env ⊢ s + t) : env ⊢ s :=
  fun _ hn => h _ (.inl hn)

theorem plus_right (h : env ⊢ s + t) : env ⊢ t :=
  fun _ hn => h _ (.inr hn)

theorem times_left (h : env ⊢ s * t) : env ⊢ s :=
  fun _ hn => h _ (.inl hn)

theorem times_right (h : env ⊢ s * t) : env ⊢ t :=
  fun _ hn => h _ (.inr hn)

end Completes

end Env

example : 3 ∈ %3 := rfl
example : 3 ∈ %3 + 10 := by left; rfl

local macro "eval_compl" : tactic => `(tactic|
  first
    | simp_all [Env.Completes.plus_left ‹_›]
    | simp_all [Env.Completes.plus_right ‹_›]
    | simp_all [Env.Completes.times_left ‹_›]
    | simp_all [Env.Completes.times_right ‹_›]
)

def eval (env : Env) (expr : Expr) (compl : env ⊢ expr := by eval_compl) : Nat :=
  match expr with
  | const n   => n
  | var i     => env.get i compl.var
  | plus s t  => eval env s + eval env t
  | times s t => eval env s * eval env t

#eval
  let env := [(1, 42)]
  let expr := %1
  eval env expr <| by intro; simp_all [expr, env, (· ∈ ·), Expr.Mem, Env.Mem, List.Mem.head]

[James Sully]

Some good stuff in here, thanks. I especially like iff_mem and get_mem for reducing the definitional rewrites. In the general case I'd probably be worried about a Membership Nat Expr instance for vars bc I might theoretically also want to talk about whether particular consts are in the expression. At that point maybe it'd be worth creating types for Var and Const and having

inductive Expr where
  | const : Const → Expr
  | var   : Var → Expr

[James Sully]

I don't know enough maths to know why ⊢ is an appropriate choice of symbol for this, but it's cool

[Henrik Böving]

Turnstyle has a lot of meanings in the logic world, generally there is always some context on the left ("context" is generally a name for "collection of variables, often with associated types") and then some expression on the right that is considered "valid" in that context. "valid" can mean a lot of things, in this case "all variables are bound" but for example the notation is also common as

\Gamma \turnstyle x : \tau

in type theory where it means "the expression x has type tau in context Gamma

[James Sully]

default argument with a tactic is a cool strategy. I think indexing works that way with get_elem_tactic

[James Sully]

Henrik Böving said:

Turnstyle has a lot of meanings in the logic world, generally there is always some context on the left ("context" is generally a name for "collection of variables, often with associated types") and then some expression on the right that is considered "valid" in that context. "valid" can mean a lot of things, in this case "all variables are bound" but for example the notation is also common as

\Gamma \turnstyle x : \tau

in type theory where it means "the expression x has type tau in context Gamma

That makes sense, the infoview would be an example

[Henrik Böving]

Precisely! The infoview is the dump of the context + expected type at that point and you are constructing the x

[James Sully]

Marcus Rossel said:

def get (key : Nat) (env : Env) (_ : key ∈ env := by get_mem) : Nat :=
  let (key', val) :: rest := env
  if _ : key == key' then val else get key rest

What specifically is the criteria for lean being able to know that a case is inconsistent and can be left out, like the [] case here?

[Marcus Rossel]

@James Sully I'm not sure. But in this case the [] branch could be closed using by contradiction, so perhaps that's one of the things Lean checks.

[James Sully]

I did a quick experiment:

#eval Id.run do
  let myList₁ : List Nat := []

  -- match myList₁ with
  -- | [] => 1
  -- | n :: ns => by contradiction -- "error: tactic 'contradiction' failed"

  match h : myList₁ with
  | [] => 1
  | n :: ns => by contradiction -- ok, since we have `h`

  -- let [] := myList₁ -- "error: missing cases: (List.cons _ _)"

  have : myList₁ = [] := rfl
  let [] := myList₁ -- ok

It's a bit strange to me that the let before the have is an error, it feels like something the system ought to be able to work out.

Could lean not whenever it sees
let x := e
automatically also add an anonymous hypothesis that x = e to the context? I'm sure there's some good reason this isn't done, but I don't immediately see what it is.

[Kevin Buzzard]

let [] := ... surely makes no sense, because you are in no position to say what you want [] to mean; it already means something.

[James Sully]

It's just a pattern match, I can easily switch the whole thing around to use cons instead, it makes no difference. But there would be destructuring bindings, so the statement would have a purpose, if that bothers you.

[James Sully]

here it is the other way around, if that's less distracting

def main : IO Unit := do
  let myList₁ : List Nat := [1]

  -- match myList₁ with
  -- | [] => by contradiction -- error: tactic 'contradiction' failed
  -- | n :: ns => 1

  let _ := match h : myList₁ with
  | [] => by contradiction -- ok, since we have `h`
  | n :: ns => 1

  -- let [n] := myList₁ -- error: missing cases: (List.cons _ (List.cons _ _))
  have : myList₁ = [1] := rfl
  let [n] := myList₁ -- ok

  IO.println n -- prints 1