Trying to understand Theorem Proving in Lean 4 exercise 7.3

Stream: new members

[debord]

I'm attempting to do question 3 in chapter 7 of Theorem Proving in Lean 4 and I'm having a lot of trouble even understanding the question. My understanding of inductive types is that they represent all of the possibilites of what can be a something of a specific type, and you can define how these things are corresponding to your own intuitive idea of what that is. So for example a List can be empty, or it can be populated with an arbitrary amount of elements of any type, which the inductive definition of List says. And then I can define the properties of Lists corresponding to my intuition of what I'm trying to define in the case of when a list is empty, and recursively when its populated. But what exactly is the type that I'm being asked to construct in 7.3? I first define it as

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

which would be that Calc.const/var or Calc.plus/times take either just n or n and m to produce a "Calc" according to the rules I set in the 'evaluator' definition. But I'm struggling to understand what it's asking me to do to "Recursively define a function that evaluates any such term with respect to an assignment of values to the variables." This makes me think to make a definition that takes two natural numbers and somehow turns them into things of type Calc. So then

def Calc_eval (a b : Nat) : Calc :=
  match a with
  | zero =>

but here I'm confused. If a is zero, then what exactly am I even trying to say about Calc? Calc.const 0 would just be the
natural number zero, Calc.var 0 would be creating a new variable with name 0, Calc.add 0 x would be x, etc, but I don't know how exactly I can articulate that here. Can I use cases on the Calc itself that I'm trying to output somehow so that I can explicitly tell it what the Calc is supposed to evaluate to in each instance? Is this even how the function is supposed to go? Is it supposed to take into a Calc and then return the natural numbers that it is 'encoded' with so that it would instead be something like

def Calc_eval (a  : Calc) : Nat :=
  match a with
  | const => /- somehow extract the value associated with 'const' here. Calc.const a ? -/
  | var => /- initialze a variable? variable (n: Nat)? Doesn't seem to be very happy about me trying to do this. -/

Or is it supposed to take in an (a b : Calc) and then produce another Calc, like a lot of the other definitions do. What would that even be at all without the natural number inputs as shown in the function itself? I'm pretty confused on this one and I'd appreciate some guidance. Thanks for your time.

[Arien Malec]

You want something like

inductive Calc where
  | const (n : Nat) :  Calc
  | var (n: Nat): Calc
  | plus (c: Calc) (c: Calc):  Calc
  | times (c: Calc) (c: Calc): Calc

[debord]

Huh, I never got the idea that plus and times would be operating on Calc as well. I suppose that gives more context as to what 'const' and 'var' are, so that we can use Calc to add and multiply on a number and a variable that we somehow assign to. That makes me think we need two constructors for var, like var_init and var_call or something, where Calc.var_init 1 5 would initialize the variable named 1 to the number 5 and Calc.var_call 1 would then be a kind of substitute for Calc.var.const 5. I cannot figure out at all how to implement this. Or is it that an expression like Calc.plus (Calc.const 1) (Calc.var 1) should evaluate to "1 + n"? But then what is var at all? I really wish I could make a new variable with variable (n : Nat) in the evaluator definition but I can't seem to do that without an error.

Edit: This is now my best attempt with this which doesn't work at all:

inductive Calc where
  | const (n : Nat) : Calc
  | var (n : Nat) : Calc
  | plus (c : Calc) (c : Calc) : Calc
  | times (c : Calc) (c : Calc) : Calc

def Calc_eval (a b : Nat) {c : Calc} {n : Nat} : Calc :=
  match a with
  | Nat.zero => by cases c with
    | const => exact Calc.const a
    | var => exact Calc.const n
    | plus => exact Calc.const b
    | times => exact Calc.const 0
  | Nat.succ a => by cases c with
    | const => exact Calc.const (Nat.succ a)
    | var => exact Calc.const n
    | plus => exact Calc.const ((Nat.succ a) + b)
    | times => exact Calc.const ((Nat.succ a) * b)

I still have no real clue what the question is even asking with "Recursively define a function that evaluates any such term with respect to an assignment of values to the variables." Evaluates naturals into Calcs? If so then you have to match the cases of a natural number, zero and successor, and then do something to produce the four cases of a Calc in each case of a Nat. Trying to do the next exercise after makes me realize that I just have no clue how this inductive type thing works actually, at least when it comes to defining my own.

[Bulhwi Cha]

Try filling in the sorry placeholders below. In the definition of eval, the function v : Nat → Nat is an assignment of the natural numbers to the variables of Calc.

inductive Calc : Type where
  | const (n : Nat)
  | var   (n : Nat)
  | plus  (c1 c2 : Calc)
  | times (c1 c2 : Calc)

namespace Calc

def eval (v : Nat → Nat) (c : Calc) : Nat :=
  match c with
  | const (n : Nat) => sorry
  | var   (n : Nat) => sorry
  | plus  (c1 : Calc) (c2 : Calc) => sorry
  | times (c1 : Calc) (c2 : Calc) => sorry

def v1 := fun n : Nat => n - 2
/-
#eval eval v1 (const 3) -- output: 3
#eval eval v1 (var 6)   -- 4
#eval eval v1 (plus (const 3) (var 6))  -- 7
#eval eval v1 (times (const 3) (var 6)) -- 12
#eval eval v1 (times (plus (const 2) (const 3)) (var 6)) -- 20
-/
end Calc

Solution

inductive Data : Type where
  | const (n : Nat)
  | var   (n : Nat)
  | plus  (s t : Data)
  | times (s t : Data)

namespace Data

def eval (v : Nat → Nat) (d : Data) : Nat :=
  match d with
  | const (n : Nat) => n
  | var   (n : Nat) => v n
  | plus  (s : Data) (t : Data) => eval v s + eval v t
  | times (s : Data) (t : Data) => eval v s * eval v t

def v1 := fun n : Nat => n - 2

#eval eval v1 (const 3) -- output: 3
#eval eval v1 (var 6)   -- 4
#eval eval v1 (plus (const 3) (var 6))  -- 7
#eval eval v1 (times (const 3) (var 6)) -- 12
#eval eval v1 (times (plus (const 2) (const 3)) (var 6)) -- 20

end Data

[Bulhwi Cha]

debord said:

Trying to do the next exercise after makes me realize that I just have no clue how this inductive type thing works actually, at least when it comes to defining my own.

These resources will help you:

• Chapter 4 of "Logic and Mechanized Reasoning"
• Implementing propositional logic
• A definition of partial truth assignments

[Arien Malec]

I'd start with thinking about var as another label for const, and getting eval working.

As an exercise, you might then want to think about assigning all the vars as above. Then you can get fancy with labeled vars. E.g., you might think about:

inductive Calc where
  | const (n : Nat) : Calc
  | var (l: String) (n: Nat): Calc
  | plus (s: Calc) (t: Calc):  Calc
  | times (s: Calc) (t: Calc): Calc

def eval (c: Calc) : Nat := sorry

def assign (c: Calc) (l: String) (n: Nat) : Calc  := sorry

[Arien Malec]

If you want to get really fancy, you can then think about error handling, which leads to monads and such...

[Arien Malec]

The non-monadic version of assign above just updates var if the labels match, and leaves them alone if not...

[Kevin Buzzard]

I don't have a CS background but I got a good understanding of questions like this from reading the beginning of Adam Chlipala's book and translating the Coq to Lean (this was one of the first lean exercises I ever did)

[debord]

I first tried to attack the problem with Arien's approach, as it most closely corresponded to my initial idea, but assign proved to be a pretty tough function. I like Bulhwi's approach as well, but my issue with it is that it makes it so that Calc can only be evaluated in terms of another function. This makes Calc more general, but my idea of Calc was just a two-function calculator that works on constants and variables and nothing more. While browsing through the Lean library, I found List.get! and had the realization that the nth number in a list could be var n. So that I get:

inductive Calc where
  | const (n : Nat) : Calc
  | var (n : Nat) : Calc
  | plus (c : Calc) (c : Calc) : Calc
  | times (c : Calc) (c : Calc) : Calc

def eval (l : List Nat) (c : Calc) : Nat :=
  match c with
  | const n => n
  | var n => List.get! l n
  | plus c1 c2 => (eval l c1) + (eval l c2)
  | times c1 c2 => (eval l c1) * (eval l c2)

#eval eval [0, 5, 4, 2, 1, 3] (Calc.const 3) -- 3
#eval eval [0, 5, 4, 2, 1, 3] (Calc.var 6) -- produces an error
#eval eval [0, 5, 4, 2, 1, 3] (Calc.var 5) -- 3
#eval eval [0, 5, 4, 2, 1, 3] (Calc.plus (Calc.const 3) (Calc.var 5)) -- 6
#eval eval [0, 5, 4, 2, 1, 3] (Calc.times (Calc.plus (Calc.const 2) (Calc.const 3)) (Calc.const 5)) -- 25

This seems to be in line with what I was looking for. Took me a couple days but I think this is it. Thank you friends for your guidance and help, and especially for the references and resources. Now to figure out the type of propositional formulas...

[Arien Malec]

Ah, yes, my version of assign has recursion issue for Lean.

[Arien Malec]

My naive solution runs into issues, and my less naive solution also runs into issues:

inductive Calc where
  | const (n : Nat) : Calc
  | var (l: String) (n: Nat): Calc
  | plus (s: Calc) (t: Calc):  Calc
  | times (s: Calc) (t: Calc): Calc
deriving Repr

namespace Calc

def eval (c: Calc): Nat :=
  match c with
  | const n => n
  | var _ n => n
  | plus s t => eval s + eval t
  | times s t => eval s * eval t

def isLeaf (c: Calc): Bool :=
  match c with
  | const _ => true
  | var _ _ => true
  | _ => false

def assign (l: String) (n: Nat) (c: Calc) : Calc :=
  match c with
  | var l' _ => if l == l' then var l n else c
  | const _ => c
  | plus s t => plus (assign l n s) (assign l n t)
  | times s t => times (assign l n s) (assign l n t)
termination_by _ _ c => c.isLeaf -- Lean isn't buying this...

#eval eval (times (const 3) (var "a" 6))
#eval (assign "a" 2  (times (const 3) (var "a" 6)))
end Calc

[Arien Malec]

I'm going to guess here is that I haven't proven Calc is a DAG?

[Arien Malec]

I confused myself: this works just fine...

inductive Calc where
  | const (n : Nat) : Calc
  | var (l: String) (n: Nat): Calc
  | plus (s: Calc) (t: Calc):  Calc
  | times (s: Calc) (t: Calc): Calc
deriving Repr

namespace Calc

def eval (c: Calc): Nat :=
  match c with
  | const n => n
  | var _ n => n
  | plus s t => eval s + eval t
  | times s t => eval s * eval t

def assign (l: String) (n: Nat) (c: Calc) : Calc :=
  match c with
  | var l' _ => if l == l' then var l n else c
  | const _ => c
  | plus s t => plus (assign l n s) (assign l n t)
  | times s t => times (assign l n s) (assign l n t)

#eval eval (times (const 3) (var "a" 6)) -- 18
#eval eval (assign "a" 2  (times (const 3) (var "a" 6))) -- 6
end Calc

[Bulhwi Cha]

After @shimsw20 and I read Chapter 1 of Mathematical Logic and Computation by Jeremy Avigad, I came up with another solution. But I think this makes things much more complicated.

Another solution

structure Const : Type where
  index : Nat

notation "𝑐" => Const.mk

structure Var : Type where
  index : Nat

notation "𝑣" => Var.mk

inductive Data : Type where
  | const (n : Nat)
  | var   (n : Nat)
  | plus  (s t : Data)
  | times (s t : Data)

instance : Coe Const Data where
  coe c := Data.const c.index

instance : Coe Var Data where
  coe v := Data.var v.index

structure Model where
  univ  : Type
  const : Const → univ
  plus  : univ → univ → univ
  times : univ → univ → univ

notation "|" 𝔄 "|" => Model.univ 𝔄

namespace Data

def eval (𝔄 : Model) (σ : Var → |𝔄|) (d : Data) : |𝔄| :=
  match d with
  | const (n : Nat) => 𝔄.const (𝑐 n)
  | var   (n : Nat) => σ (𝑣 n)
  | plus  (s : Data) (t : Data) => 𝔄.plus  (eval 𝔄 σ s) (eval 𝔄 σ t)
  | times (s : Data) (t : Data) => 𝔄.times (eval 𝔄 σ s) (eval 𝔄 σ t)

def 𝔄₀ : Model where
  univ  := Nat
  const := fun c : Const ↦ c.index
  plus  := Nat.add
  times := Nat.mul

def σ₀ : Var → Nat := fun v : Var ↦ v.index - 2

#eval eval 𝔄₀ σ₀ (𝑐 3) -- output: 3
#eval eval 𝔄₀ σ₀ (𝑣 6) -- 4
#eval eval 𝔄₀ σ₀ (plus (𝑐 3) (𝑣 6))  -- 7
#eval eval 𝔄₀ σ₀ (times (𝑐 3) (𝑣 6)) -- 12
#eval eval 𝔄₀ σ₀ (times (plus (𝑐 2) (𝑐 3)) (𝑣 6)) -- 20

end Data

Reference

Avigad, Jeremy. “Fundamentals.” In Mathematical Logic and Computation, 1–27. Cambridge: Cambridge University Press, 2022. doi:10.1017/9781108778756.002.