# Zulip Chat Archive

## Stream: new members

### Topic: Trying to understand Theorem Proving in Lean 4 exercise 7.3

#### debord (Feb 01 2023 at 17:52):

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 (Feb 01 2023 at 19:49):

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 (Feb 02 2023 at 06:10):

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 (Feb 02 2023 at 17:40):

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

#### Bulhwi Cha (Feb 02 2023 at 18:07):

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 (Feb 02 2023 at 18:14):

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 `var`

s as above. Then you can get fancy with labeled `var`

s. 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 (Feb 02 2023 at 18:15):

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

#### Arien Malec (Feb 02 2023 at 18:15):

The non-monadic version of `assign`

above just updates `var`

if the labels match, and leaves them alone if not...

#### Kevin Buzzard (Feb 02 2023 at 22:11):

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 (Feb 03 2023 at 15:06):

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 (Feb 03 2023 at 19:09):

Ah, yes, my version of `assign`

has recursion issue for Lean.

#### Arien Malec (Feb 03 2023 at 19:31):

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 (Feb 03 2023 at 21:44):

I'm going to guess here is that I haven't proven `Calc`

is a DAG?

#### Arien Malec (Feb 03 2023 at 21:52):

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 (Feb 19 2023 at 15:00):

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

**Reference**

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

Last updated: Dec 20 2023 at 11:08 UTC