# Zulip Chat Archive

## Stream: new members

### Topic: Types and Programming Languages

#### Patrick Thomas (Sep 14 2021 at 00:55):

Did I set this up right? I'm having some trouble proving it.

```
-- Types and Programming Languages Kindle Edition by Benjamin C. Pierce (Author) Format: Kindle Edition
-- Theorem 3.3.4
inductive term : Type
| true
| false
| zero
| succ (t1 : term)
| pred (t1 : term)
| iszero (t1 : term)
| ite (t1 : term) (t2 : term) (t3 : term)
def size : term -> nat
| term.true := 1
| term.false := 1
| term.zero := 1
| (term.succ t1) := (size t1) + 1
| (term.pred t1) := (size t1) + 1
| (term.iszero t1) := (size t1) + 1
| (term.ite t1 t2 t3) := (size t1) + (size t2) + (size t3) + 1
-- principle of complete mathematical induction
axiom PCI :
forall P : nat -> Prop,
(forall m : nat, (forall i : nat, i < m -> P i) -> P m) ->
forall n : nat, P n
-- induction on size
theorem IOS :
forall P : term -> Prop,
(forall s : term, (forall r : term, size r < size s -> P r) -> P s) ->
forall t : term, P t :=
begin
intros P,
let Q := fun (n : nat), forall s : term, (size s = n) -> P s,
have s1 : (forall m : nat, (forall i : nat, i < m -> Q i) -> Q m) -> forall n : nat, Q n, from PCI Q,
sorry
end
```

#### Mario Carneiro (Sep 14 2021 at 01:17):

here's a more leanified version, and a good start on the problem. I removed the definition `Q`

because it obscures more than it helps in this proof.

```
-- principle of complete mathematical induction
theorem PCI (P : ℕ → Prop)
(H : ∀ m : ℕ, (∀ i, i < m → P i) → P m)
(n : ℕ) : P n :=
nat.strong_induction_on n H
-- induction on size
theorem IOS (P : term → Prop)
(H : ∀ s : term, (∀ r : term, size r < size s → P r) → P s)
(t : term) : P t :=
begin
refine PCI (λ (n : nat), ∀ s : term, size s = n → P s) _ _ t rfl,
dsimp only,
intros m ih s e,
sorry
end
```

#### Patrick Thomas (Sep 14 2021 at 01:30):

What is the `refine`

tactic doing?

#### Johan Commelin (Sep 14 2021 at 01:36):

It is like `exact`

, but you can leave some holes using `_`

. If Lean can't figure out what to put in place of those `_`

, it doesn't throw an error, but creates a new goal instead.

#### Patrick Thomas (Sep 14 2021 at 01:39):

So is everything after PCI in that line, the hypotheses to PCI?

#### Johan Commelin (Sep 14 2021 at 01:42):

yup

#### Patrick Thomas (Sep 14 2021 at 01:52):

Where do the `t`

and the `rfl`

line up?

#### Mario Carneiro (Sep 14 2021 at 01:58):

`PCI`

has three arguments, but the result is `P n`

, and since in this case we substituted `λ (n : nat), ∀ s : term, size s = n → P s`

for `P`

, the result after substituting the first three arguments is `∀ s : term, size s = ?n → P s`

and we have space to add two more arguments

#### Mario Carneiro (Sep 14 2021 at 02:00):

here's a more broken down version of the first line:

```
have : ∀ (s : term), size s = size t → P s :=
PCI (λ (n : nat), ∀ s : term, size s = n → P s) _ (size t),
refine this t rfl,
```

#### Patrick Thomas (Sep 14 2021 at 02:02):

I see. Thank you.

#### Patrick Thomas (Sep 14 2021 at 02:19):

Thank you!

```
-- induction on size
theorem IOS (P : term → Prop)
(H : ∀ s : term, (∀ r : term, size r < size s → P r) → P s)
(t : term) : P t :=
begin
refine PCI (λ (n : nat), ∀ s : term, size s = n → P s) _ _ t rfl,
dsimp only,
intros m ih s e,
apply H,
intros r a,
apply (ih (size r)),
rw <- e,
apply a,
refl
end
```

#### Mario Carneiro (Sep 14 2021 at 02:57):

Good job. Now, the cheating way:

```
theorem IOS (P : term → Prop)
(H : ∀ s : term, (∀ r : term, size r < size s → P r) → P s)
(t : term) : P t :=
(measure_wf size).induction t H
```

#### Mario Carneiro (Sep 14 2021 at 02:58):

(There are even more cheating ways when you notice that `size`

is the same as `term.sizeof`

, and indeed this particular theorem is applied automatically by lean when you write functions by well founded recursion using the equation compiler.)

#### Mario Carneiro (Sep 14 2021 at 03:04):

here's a golfy proof more similar to yours:

```
theorem IOS (P : term → Prop)
(H : ∀ s : term, (∀ r : term, size r < size s → P r) → P s)
(t : term) : P t :=
begin
refine PCI (λ (n : nat), ∀ s : term, size s = n → P s) _ (size t) t rfl,
rintro m ih s rfl,
refine H _ (λ r h, ih _ h r rfl),
end
```

#### Patrick Thomas (Sep 18 2021 at 15:26):

The book defines structural induction as:

```
If, for each term s,
given P(r) for all immediate subterms r of s we can show P(s),
then P(s) holds for all s.
```

How does one formalize this and show that it follows from weak mathematical induction? Do I define a function `is_immediate_subterm : term -> term -> Prop`

and then:

```
forall P : term -> Prop,
(forall s : term, (forall r : term, (is_immediate_subterm r s) -> P r) -> P s) ->
forall t : term, P t
```

Also, I'm not sure how to go about defining a function `f : term -> nat`

such that `f s = (f r) + 1 iff (is_immediate_subterm r s)`

to use to show that it follows from weak mathematical induction, if that is what I need to do.

#### Chris B (Sep 18 2021 at 15:37):

There might be an even more primitive way of doing this in mathlib, but in core this is done with acc and its recursor, then `measure_wf`

, and `sizeof_measure_wf`

, which are other helper functions/lemmas in that file. `sizeof`

is automatically generated for inductives, I think the general rule is just that `forall a, sizeof(ctor(a)) = sizeof(a) + 1`

.

#### Chris B (Sep 18 2021 at 15:39):

Actually it looks like sizeof is defined manually for some primitives, like list and option.

```
protected def option.sizeof {α : Type u} [has_sizeof α] : option α → nat
| none := 1
| (some a) := 1 + sizeof a
protected def list.sizeof {α : Type u} [has_sizeof α] : list α → nat
| list.nil := 1
| (list.cons a l) := 1 + sizeof a + list.sizeof l
```

#### Mario Carneiro (Sep 18 2021 at 15:49):

That's just because they are needed during bootstrapping. They would normally be created automatically but the sizeof framework isn't yet set up when those inductives are introduced.

#### Mario Carneiro (Sep 18 2021 at 15:52):

Patrick Thomas said:

The book defines structural induction as:

`If, for each term s, given P(r) for all immediate subterms r of s we can show P(s), then P(s) holds for all s.`

How does one formalize this and show that it follows from weak mathematical induction?

In lean, this is the wrong way around. Structural induction is *primitive*; it is true by the axioms associated to each inductive type. Weak induction on nat is a special case of structural induction, as is induction on `acc`

which yields well founded recursion, which proves strong induction using `sizeof`

.

#### Mario Carneiro (Sep 18 2021 at 15:54):

The shape of each structural induction theorem looks a little different since it depends on how the inductive is defined. Try `#print term.rec`

to see what it looks like for `term`

.

#### Patrick Thomas (Sep 18 2021 at 16:04):

Can it still be proven this way around?

#### Mario Carneiro (Sep 18 2021 at 16:13):

The easiest way to prove a theorem using `is_immediate_subterm`

is to define it as an inductive family and then prove it using `term.rec`

#### Patrick Thomas (Sep 18 2021 at 16:16):

I guess I'm trying to do the exercise in the book, to prove that it follows from weak mathematical induction, similar to the earlier proof using size.

#### Mario Carneiro (Sep 18 2021 at 16:17):

It's not possible to do this from weak nat recursion directly, because one term can have two immediate subterm of different heights. For example `ite true (succ zero) zero`

yields the relations:

```
f (ite true (succ zero) zero) = f (succ zero) + 1
f (ite true (succ zero) zero) = f zero + 1
f (succ zero) = f zero + 1
```

which are clearly unsolvable. The easy way to derive this using PCI is to just use strong recursion on terms and use that "immediate subterm" implies sizeof strict inequality.

#### Patrick Thomas (Sep 18 2021 at 16:28):

I'm sorry, what does strong recursion on terms mean?

Do you mean, define the function `is_immediate_subterm: term -> term -> Prop`

, then prove `forall r, s : term, is_immediate_subterm r s -> size r < size s`

. Then proceed as in the earlier proof?

#### Patrick Thomas (Sep 18 2021 at 17:03):

Like this?

```
constant term : Type
constant size : term → ℕ
constant is_immediate_subterm : term → term → Prop
lemma subterm_size (r s : term) : is_immediate_subterm r s -> size r < size s := sorry
-- principle of complete mathematical induction
theorem PCI (P : ℕ → Prop)
(H : ∀ m : ℕ, (∀ i, i < m → P i) → P m)
(n : ℕ) : P n :=
nat.strong_induction_on n H
theorem SI (P : term → Prop)
(H : ∀ s : term, (∀ r : term, is_immediate_subterm r s → P r) → P s)
(t : term) : P t :=
begin
refine PCI (λ (n : nat), ∀ s : term, size s = n → P s) _ _ t rfl,
dsimp only,
intros m ih s e,
apply H,
intros r a,
apply (ih (size r)),
rw <- e,
apply (subterm_size r s a),
refl
end
```

#### Patrick Thomas (Sep 18 2021 at 17:15):

Thank you. I thought it was more complicated and was heading in the wrong direction.

#### Mario Carneiro (Sep 18 2021 at 17:19):

You can actually just apply the previous theorem instead of replaying it

#### Patrick Thomas (Sep 18 2021 at 17:20):

Yeah, that probably would have been simpler :)

#### Patrick Thomas (Sep 25 2021 at 00:37):

3.2.1 Definition [Terms, Inductively]: The set of terms is the smallest set $T$ such that

- {true, false, 0} $\subseteq T$;
- if $t_{1} \in T$, then {succ $t_{1}$, pred $t_{1}$, iszero $t_{1}$} $\subseteq T$;
- if $t_{1} \in T$, $t_{2} \in T$, and $t_{3} \in T$, then if $t_{1}$ then $t_{2}$ else $t_{3}$ $\in T$.

I think the equivalent of Definition 3.2.1 in Lean is

```
inductive term : Type
| true
| false
| zero
| succ (t1 : term)
| pred (t1 : term)
| iszero (t1 : term)
| ite (t1 : term) (t2 : term) (t3 : term)
```

In a similar manner, Is there an equivalent of Definition 3.2.3 in Lean? By equivalent I mean as a translation from set theory to type theory, not the fact that $S$ and $T$ are the same set.

3.2.3 Definition [Terms, Concretely]: For each natural number $i$, define a set $S_{i}$ as follows:

$S_{0} = \empty$

$S_{i+1}$ = {true, false, 0} $\cup$ {succ $t_{1}$, pred $t_{1}$, iszero $t_{1} | t_{1} \in S_{i}$} $\cup$ {if $t_{1}$ then $t_{2}$ else $t_{3}$| $t_{1}, t_{2}, t_{3} \in S_{i}$}.

Finally, let $S = \bigcup S_{i}$.

#### Patrick Thomas (Sep 25 2021 at 00:45):

Maybe the Lean definition I gave goes with definition 3.2.3 and the question is about an equivalent Lean definition for 3.2.1? I'm not certain.

#### Reid Barton (Sep 25 2021 at 01:02):

The Lean translation looks good. Definition 3.2.3 is a standard way in set theory to justify Definition 3.2.1, which is not complete as it stands (because a priori there might not be any set $T$ with this property). You could try to imitate Definition 3.2.3 in Lean, but it would be awkward and it's probably more sensible to just accept that the basic building blocks of type theory are different from in set theory.

#### Patrick Thomas (Sep 25 2021 at 01:08):

I see. Thank you!

#### Patrick Thomas (Sep 25 2021 at 01:12):

Something like this perhaps?

```
import data.set
open set
-- Terms, Inductively
constant T : set string
def rule_1 (S : set string) := {"true", "false", "zero"} ⊆ S
def rule_2 (S : set string) := forall t1 : string, t1 ∈ S → {"succ" ++ t1, "pred" ++ t1, "iszero" ++ t1} ⊆ S
def rule_3 (S : set string) := forall t1 t2 t3 : string, "ite" ++ t1 ++ t2 ++ t3 ∈ S
constant holds : rule_1 T → rule_2 T → rule_3 T
constant smallest : ∀ S : set string, rule_1 S → rule_2 S → rule_3 S → T ⊆ S
-- Terms, Concretely
def f : ℕ → set string
| nat.zero := ∅
| (nat.succ i) :=
{"true", "false", "zero"}
∪ {("succ" ++ t1) | t1 ∈ f i} ∪ {("pred" ++ t1) | t1 ∈ f i} ∪ {("iszero" ++ t1) | t1 ∈ f i}
∪ {("ite" ++ t1 ++ t2 ++ t3) | t1 t2 t3 ∈ f i}
def S := ⋃ i : ℕ, f i
example : T = S := sorry
```

#### Kyle Miller (Sep 25 2021 at 01:54):

It seems you've forgotten spaces between terms. Also, `holds`

seems odd (maybe you meant conjunctions?), and rather than introducing `smallest`

and `T`

as constants, you can prove that `S`

is smallest as a theorem, replacing the `example`

.

One downside with strings is that to be able to use them as terms you have to go through the effort of parsing them.

#### Patrick Thomas (Sep 25 2021 at 01:57):

What would be a good alternative to strings?

#### Patrick Thomas (Sep 25 2021 at 02:02):

Yes, you are right, I should have defined `holds`

with conjunctions.

#### Kyle Miller (Sep 25 2021 at 02:04):

One option is to add enough parenthesis so parsing is easy (though you still would want to parse). It can also be nice to add some functions to make sure you generate the correct syntax.

```
import data.set
open set
namespace pre_term
def true := "true"
def false := "false"
def zero := "zero"
def succ (s : string) := "(succ " ++ s ++ ")"
def pred (s : string) := "(pred " ++ s ++ ")"
def iszero (s : string) := "(iszero " ++ s ++ ")"
def ite (s t u : string) := "(ite " ++ s ++ " " ++ t ++ " " ++ u ++ ")"
end pre_term
def rule_1 (S : set string) : set string := {pre_term.true, pre_term.false, pre_term.zero}
def rule_2 (S : set string) : set string :=
{(pre_term.succ t1) | t1 ∈ S} ∪ {(pre_term.pred t1) | t1 ∈ S} ∪ {(pre_term.iszero t1) | t1 ∈ S}
def rule_3 (S : set string) : set string := {(pre_term.ite t1 t2 t3) | t1 t2 t3 ∈ S}
def f : ℕ → set string
| nat.zero := ∅
| (nat.succ i) := rule_1 (f i) ∪ rule_2 (f i) ∪ rule_3 (f i)
def S := ⋃ i : ℕ, f i
theorem holds : rule_1 S ⊆ S ∧ rule_2 S ⊆ S ∧ rule_3 S ⊆ S := sorry
theorem smallest : ∀ (T : set string), rule_1 T ⊆ T → rule_2 T ⊆ T → rule_3 T ⊆ T → S ⊆ T := sorry
```

#### Kyle Miller (Sep 25 2021 at 02:06):

And then you could go on to create the subtype of those strings that are in `S`

and make all the constructors:

```
def term : Type := S -- this is the set coerced to a type
namespace term
def true : term := ⟨pre_term.true, begin use (f 1), simp [f, rule_1], use 1, refl, end⟩ -- (not a very pretty proof)
def false : term := sorry
def zero : term := sorry
def succ (t1 : term) : term := sorry
def pred (t1 : term) : term := sorry
def iszero (t1 : term) : term := sorry
def ite (t1 t2 t3 : term) : term := sorry
end term
```

#### Patrick Thomas (Sep 25 2021 at 02:13):

Cool. Thank you!

#### Kyle Miller (Sep 25 2021 at 02:18):

This is another setup that I'd expect to be somewhat easier to parse (and by "parse" I mean writing the recursor). It uses lists of symbols:

```
import data.set
open set
inductive symb
| true | false | zero | succ | pred | iszero | ite
namespace pre_term
def true := [symb.true]
def false := [symb.false]
def zero := [symb.zero]
def succ (s : list symb) := [symb.succ] ++ s
def pred (s : list symb) := [symb.pred] ++ s
def iszero (s : list symb) := [symb.iszero] ++ s
def ite (s t u : list symb) := [symb.ite] ++ s ++ t ++ u
end pre_term
def rule_1 : set (list symb) := {pre_term.true, pre_term.false, pre_term.zero}
def rule_2 (S : set (list symb)) : set (list symb) :=
{(pre_term.succ t1) | t1 ∈ S} ∪ {(pre_term.pred t1) | t1 ∈ S} ∪ {(pre_term.iszero t1) | t1 ∈ S}
def rule_3 (S : set (list symb)) : set (list symb) := {(pre_term.ite t1 t2 t3) | t1 t2 t3 ∈ S}
def f : ℕ → set (list symb)
| nat.zero := ∅
| (nat.succ i) := rule_1 ∪ rule_2 (f i) ∪ rule_3 (f i)
def S := ⋃ i : ℕ, f i
theorem holds : rule_1 ⊆ S ∧ rule_2 S ⊆ S ∧ rule_3 S ⊆ S := sorry
theorem smallest : ∀ (T : set (list symb)), rule_1 ⊆ T → rule_2 T ⊆ T → rule_3 T ⊆ T → S ⊆ T := sorry
def term : Type := S
namespace term
def true : term := ⟨pre_term.true, begin use (f 1), simp [f, rule_1], use 1, refl, end⟩
def false : term := sorry
def zero : term := sorry
def succ (t1 : term) : term := sorry
def pred (t1 : term) : term := sorry
def iszero (t1 : term) : term := sorry
def ite (t1 t2 t3 : term) : term := sorry
end term
```

#### Patrick Thomas (Sep 25 2021 at 02:23):

Nice!

#### Patrick Thomas (Sep 26 2021 at 16:30):

Going back to the discussion on induction; in set theory, the principle of mathematical induction follows from the well ordering principle, and is equivalent to complete mathematical induction. In addition, we have just shown that structural induction follows from complete mathematical induction. Do all forms of induction in set theory then follow from the well ordering principle? What about induction on inductively defined propositions? Can I formalize and show this in Lean?

#### Patrick Thomas (Sep 26 2021 at 16:32):

I'm not sure how to formalize the well ordering principle in Lean, or what a generic formalization of induction on inductively defined propositions would look like, in a vein similar to:

```
forall P : nat -> Prop,
(forall m : nat, (forall i : nat, i < m -> P i) -> P m) ->
forall n : nat, P n
```

#### Patrick Thomas (Sep 26 2021 at 16:49):

That is, I think we have that all of these are equivalent:

```
-- Principle of Mathematical Induction
def PMI :=
∀ P : ℕ → Prop,
P 0 ∧ (∀ m : ℕ, P m → P (m + 1)) →
∀ n : ℕ, P n
-- Principle of Induction from a Starting Point
def SP :=
∀ P : ℕ → Prop,
∀ m : ℕ,
P m ∧ (∀ i : ℕ, i ≥ m → (P i → P (i + 1))) →
∀ n : ℕ, n ≥ m → P n
-- Principle of Complete Induction
def PCI :=
∀ P : ℕ → Prop,
(∀ m : ℕ, (∀ i : ℕ, i < m → P i) → P m) →
∀ n : ℕ, P n
-- Structural induction
constant term : Type
constant size : term -> ℕ
constant is_immediate_subterm : term -> term -> Prop
lemma subterm_size : ∀ r s : term, is_immediate_subterm r s → size r < size s := sorry
def SI :=
∀ P : term → Prop,
(∀ s : term, (∀ r : term, is_immediate_subterm r s → P r) → P s) ->
∀ t : term, P t
```

How do we formalize the well ordering principle to show that they all follow from it, and also give a similar formal definition of induction over an inductively defined proposition and show that it follows as well.

#### Eric Wieser (Sep 26 2021 at 17:04):

Proving that `PMI`

follows from well-ordering is as interesting as showing `true`

follows from it, because PMI is true by definition of `nat.rec`

#### Eric Wieser (Sep 26 2021 at 17:07):

If you want to prove the recursor of nat (`PMI`

) follows from something more fundamental, then you can't use the built-in definition of `nat`

or any similar inductive definition of nat because such a definition introduces `PMI`

as an "axiom".

#### Patrick Thomas (Sep 26 2021 at 17:10):

I guess I'm not sure how to define `nat`

in Lean in set theoretical terms, and figured I just wouldn't use that fact.

#### Patrick Thomas (Sep 26 2021 at 17:11):

But I would be interested in seeing it in Lean in set theoretical terms.

#### Patrick Thomas (Sep 26 2021 at 17:17):

Or just how to add in induction on inductively defined propositions with it as it is.

#### Patrick Thomas (Sep 26 2021 at 17:32):

Something like?

```
namespace hidden
constant nat : Type
constant le : nat → nat → Prop
constant lt : nat → nat → Prop
def WOP : Prop := ∀ s : set nat, ∃ t : nat, t ∈ s → ∃ u : nat, u ∈ s ∧ ∀ v : nat, v ∈ s → le u v
def PCI : Prop :=
∀ P : nat → Prop,
(∀ m : nat, (∀ i : nat, lt i m → P i) → P m) →
∀ n : nat, P n
example : WOP → PCI := sorry
end hidden
```

#### Eric Wieser (Sep 26 2021 at 18:42):

That looks unprovable because you have nothing saying how `lt`

and `le`

interact.

#### Patrick Thomas (Sep 26 2021 at 19:13):

I was just throwing it together leaving them to be defined.

#### Patrick Thomas (Sep 26 2021 at 19:15):

The question I am most interested in, is how to similarly formalize and show (if it holds true) that induction on inductively defined propositions is related to mathematical induction.

#### Patrick Thomas (Sep 26 2021 at 19:29):

For example, what is the form of the induction principle on `step`

and can it be related to the principle of mathematical induction:

```
inductive term : Type
| true
| false
| zero
| succ (t1 : term)
| pred (t1 : term)
| iszero (t1 : term)
| ite (t1 : term) (t2 : term) (t3 : term)
-- step x y means that (x, y) is in the evaluation relation
inductive step : term → term → Prop
| e_if_true (t2 t3 : term) :
step (term.ite term.true t2 t3) t2
| e_if_false (t2 t3 : term) :
step (term.ite term.false t2 t3) t3
| e_if (t1 t1' t2 t3 : term) :
step t1 t1' → step (term.ite t1 t2 t3) (term.ite t1' t2 t3)
```

#### Eric Wieser (Sep 26 2021 at 20:21):

You can ask lean for the "form of induction principle on `step`

" with `#check @step.rec`

#### Patrick Thomas (Sep 26 2021 at 20:24):

Can that induction principle be shown to follow from one of the others?

#### Eric Wieser (Sep 26 2021 at 20:26):

If it can be shown, you can't write the proof in lean itself while keeping that definition of `step`

.

#### Eric Wieser (Sep 26 2021 at 20:28):

You'd need to formalize the rules of inductive types in lean itself, and describe `step`

in *that* language in order to use Lean to show what you're asking.

#### Patrick Thomas (Sep 26 2021 at 20:33):

I am guessing that there is an axiom in Lean that all of the various forms of induction in Lean follow from?

#### Eric Wieser (Sep 26 2021 at 21:13):

Every time you use the keyword `inductive`

or `structure`

or `class`

you are essentially introducing a new recursor "axiom" (but not `axiom`

) into lean

#### Patrick Thomas (Sep 26 2021 at 21:16):

What ensures that they are permissible?

#### Eric Wieser (Sep 26 2021 at 21:22):

The rules that dictate what is and is not a valid (non-`meta`

)`inductive`

type ensure they are permissible. Lean itself does not provide a proof that they are permissible, that's the foundation you as the user are putting your trust upon.

#### Eric Wieser (Sep 26 2021 at 21:25):

I would expect the paper on lean itself to provide ample references to how exactly that foundation is justified mathematically; but I think those were already linked in your other thread?

#### Patrick Thomas (Sep 26 2021 at 21:32):

I see.

#### One An (May 24 2023 at 12:49):

Hello, I'm trying to enter tactic mode, but when I type begin, it shows "unknown identifier 'begin'. Why does it say that begin is an unknown identifier. It does seem like it recognize "end" because it says "invalid 'end', insufficient scopes." Thank you for the help\

#### Kyle Miller (May 24 2023 at 12:56):

Are you using Lean 3 or Lean 4? If Lean 4, then the new syntax is just `by`

, not `begin ... end`

.

If Lean 3, do you have an example you can paste here that shows the error? (You can put the code between triple #backticks to get it to format nicely)

#### One An (May 24 2023 at 13:50):

```
begin
apply and.intro,
exact hp,
apply and.intro,
exact hq,
exact hp
end
```

#### One An (May 24 2023 at 13:51):

how do i use the "by" syntax? is there a tutorial? I will try using lean 4 instead

#### Kyle Miller (May 24 2023 at 13:53):

Is that your complete example? You seem to not have included enough of your file -- where's the code for the theorem you're proving?

#### One An (May 24 2023 at 14:20):

oh sorry, i dont know why it didn't copy for some reason

#### One An (May 24 2023 at 14:20):

```
theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p :=
begin
apply and.intro,
exact hp,
apply and.intro,
exact hq,
exact hp
end
```

#### One An (May 24 2023 at 14:24):

or theres this another example

#### One An (May 24 2023 at 14:24):

```
variables (P Q R : Prop)
lemma identity : P /to P :=
begin
intro hp
exact hp
end
```

#### One An (May 24 2023 at 14:30):

I changed to lean 4 and managed to make it work by using "by" instead!

#### Kyle Miller (May 24 2023 at 14:30):

In Lean 3 this works:

```
variables (P Q R : Prop)
lemma identity : P → P :=
begin
intro hp,
exact hp
end
```

#### Kyle Miller (May 24 2023 at 14:31):

In Lean 4 you get the error you're describing:

```
variable (P Q R : Prop)
lemma identity : P → P :=
begin -- unknown identifier 'begin'
intro hp,
exact hp
end
```

#### Kyle Miller (May 24 2023 at 14:31):

You must have been using Lean 4 to get this error

#### Kyle Miller (May 24 2023 at 14:31):

Here's the valid Lean 4 code:

```
variable (P Q R : Prop)
theorem identity : P → P := by
intro hp
exact hp
```

#### One An (May 24 2023 at 14:33):

image.png

that still doesnt work for lean 4 some reason. Am I doing something wrong?

#### Kyle Miller (May 24 2023 at 14:33):

I just changed it to work without any imports. Now it's `theorem`

#### Kyle Miller (May 24 2023 at 14:34):

If you have Mathlib set up, you can do `import Mathlib`

to get `lemma`

, which is just a `theorem`

as far as Lean is concerned

#### One An (May 24 2023 at 14:35):

How do i import it? Do I do it through bash? Also, do you recommend sticking with lean 4 or going back and downloading lean 3?

#### One An (May 24 2023 at 14:35):

Thank you for helping

#### One An (May 24 2023 at 14:37):

Also, how do i make the goal appear on the left? I've seen some people do it and I'm not sure how

#### Damiano Testa (May 24 2023 at 14:49):

If your project has `Mathlib`

as a dependecy, then you can write at the beginning of the file any number of lines like `import [file]`

and you are "importing" the contents of the files. For instance, `import Mathlib.Data.Nat.Basic`

should work.

To get the goal appear on the left, I think that this is just a matter of dragging the windows around with VSCode (from the picture, it seems that you might be using VSCode, otherwise, I do not know). In any case, this seems more like a setup of your editor, than of Lean.

#### One An (May 24 2023 at 14:52):

Oh i see, thank you so much! For the goal thing, I meant like just making it appear at all because it doesn't seem to appear at all for me when I'm in tactic mode

#### Damiano Testa (May 24 2023 at 14:54):

What do you see if you place your cursor on the `intro hp`

line?

#### One An (May 24 2023 at 14:57):

Nothing shows up

#### Damiano Testa (May 24 2023 at 14:57):

This is what I see

Note that the goal view is *extremely* sensitive to the position of the cursor: it show information about the specific place where you are. This may be nothing at all, for instance if you are between `theorem`

s.

Last updated: Dec 20 2023 at 11:08 UTC