# Zulip Chat Archive

## Stream: new members

### Topic: My first original result

#### Jeremy Teitelbaum (Dec 22 2021 at 15:47):

My first original result proved in Lean.

```
example : 0 \in (2 :: 1 :: 0 :: list.nil) :=
begin
right,
right,
left,
refl,
end
```

#### Martin Dvořák (Dec 22 2021 at 15:57):

Welcome!

#### Adam Topaz (Dec 22 2021 at 16:18):

Can you get the proof to a single line?

#### Adam Topaz (Dec 22 2021 at 16:18):

Hint: the computer can compute whether or not a given natural is in a list of naturals ;)

#### Jeremy Teitelbaum (Dec 22 2021 at 16:42):

What I'd really like to understand is how to write this without tactics. Or, more generally, I confess I don't exactly understand what `right`

and `left`

are doing, from the internal point of view. I gather that they `apply`

the first and second constructors of an inductive type. But what is the inductive type under consideration here? I'm trying to read the source code for the `list`

type but I can't match things up.

#### Marcus Rossel (Dec 22 2021 at 16:44):

Jeremy Teitelbaum said:

What I'd really like to understand is how to write this without tactics. Or, more generally, I confess I don't exactly understand what

`right`

and`left`

are doing, from the internal point of view. I gather that they`apply`

the first and second constructors of an inductive type. But what is the inductive type under consideration here? I'm trying to read the source code for the`list`

type but I can't match things up.

You can use the `#print`

command to inspect the term that was constructed by a begin-end block:

```
theorem my_theorem : 0 ∈ (2 :: 1 :: 0 :: list.nil) :=
begin
right,
right,
left,
refl,
end
#print my_theorem
--theorem my_theorem : 0 ∈ [2, 1, 0] := or.inr (or.inr (or.inl (eq.refl 0)))
```

#### Adam Topaz (Dec 22 2021 at 16:44):

`left`

and `right`

are tactics that you can use when you want to prove a disjunction of two props $p \vee q$. If the goal is $p \vee q$, then left will replace the goal with $p$ and right will replace the goal with $q$.

#### Adam Topaz (Dec 22 2021 at 16:45):

The `has_mem`

instance for a list is defined recursively so that $x \in (a :: as)$ if and only if $x = a$ or $x \in as$, and this is why `left`

and/or `right`

work for such a goal.

#### Adam Topaz (Dec 22 2021 at 16:45):

(the base case `x \in list.nil`

is defined to be false.)

#### Patrick Massot (Dec 22 2021 at 16:47):

Jeremy, do you know about tactic#show_term?

#### Jeremy Teitelbaum (Dec 22 2021 at 16:47):

The process by which `0 \in [0,1,2]`

gets converted to `0=0 \or 0\in [1,2]`

seems like utter magic.

#### Marcus Rossel (Dec 22 2021 at 16:48):

Jeremy Teitelbaum said:

The process by which

`0 \in [0,1,2]`

gets converted to`0=0 \or 0\in [1,2]`

seems like utter magic.

That comes from the definition of `list.mem`

:

```
protected def mem : α → list α → Prop
| a [] := false
| a (b :: l) := a = b ∨ mem a l
```

From this definition we can deduce that `0 \in [0,1,2]`

(which is syntactic sugar for `list.mem 0 [0, 1, 2]`

) means the same as `0 = 0 ∨ list.mem 0 [1, 2]`

.

#### Kevin Buzzard (Dec 22 2021 at 16:50):

Jeremy, there is this weird non-mathematical concept called definitional equality.

#### Kevin Buzzard (Dec 22 2021 at 16:50):

For example x+0=x is definitionally true, but 0+x=x is not, you need to prove it by induction.

#### Jeremy Teitelbaum (Dec 22 2021 at 16:50):

Yes, I see that. But I can't find this syntax for definition of a function in the manual. (probably just dumb). I can infer its meaning, but what language mechanism takes a statement like `list.mem 0 [0,1,2]`

, which I gather is a proposition, and rewrites it as the appropriate `\or`

taking into account that `[0,1,2]`

is not null?

#### Kevin Buzzard (Dec 22 2021 at 16:51):

You don't need manuals, you just right click on what you want to see the definition of

#### Kevin Buzzard (Dec 22 2021 at 16:52):

`#check list.mem`

, right click, see what the definitional equalities are

#### Kevin Buzzard (Dec 22 2021 at 16:52):

or `unfold list.mem`

in tactic mode

#### Marcus Rossel (Dec 22 2021 at 16:52):

Jeremy Teitelbaum said:

Yes, I see that. But I can't find this syntax for definition of a function in the manual. (probably just dumb). I can infer its meaning, but what language mechanism takes a statement like

`list.mem 0 [0,1,2]`

, which I gather is a proposition, and rewrites it as the appropriate`\or`

taking into account that`[0,1,2]`

is not null?

For the syntax, cf. https://leanprover.github.io/theorem_proving_in_lean/induction_and_recursion.html#pattern-matching

#### Jeremy Teitelbaum (Dec 22 2021 at 16:54):

Marcus Rossel said:

For the syntax, cf. https://leanprover.github.io/theorem_proving_in_lean/induction_and_recursion.html#pattern-matching

Aha. I am still trying to make sense of the discussion of inductive types in chapter 7. I will press on. Thanks!

#### Kevin Buzzard (Dec 22 2021 at 16:58):

The definition of `list.mem`

says that `a \in []`

is defined to be `false`

and `a \in b :: l`

is defined to be `a = b \or a \in l`

#### Patrick Johnson (Dec 22 2021 at 17:00):

Jeremy Teitelbaum said:

What I'd really like to understand is how to write this without tactics.

```
lemma lem : 0 ∈ [2, 1, 0] := of_as_true trivial
```

#### Kevin Buzzard (Dec 22 2021 at 17:01):

you just keep unwinding the definitions and at each point you observe that there is an algorithm to determine whether the proposition is true or not, so you just keep applying the algorithm.

#### Kevin Buzzard (Dec 22 2021 at 17:01):

equality is decidable for concrete naturals, and if P and Q are decidable then P or Q is decidable (because you just decide them both and see if either are true)

Last updated: Dec 20 2023 at 11:08 UTC