# Zulip Chat Archive

## Stream: general

### Topic: Reverse cases_on

#### Fingy Soupy (Apr 16 2022 at 16:47):

Hello, I have a short property I'd like to prove:

```
inductive tv
| vtrue
| vundef
| vfalse
def tv_nat (a : tv) : ℕ := tv.cases_on a 3 2 1
def tv_unnat {a b : tv} (h : (tv_nat a) = (tv_nat b)) : a = b :=
sorry
```

I know there are few tools for dealing with inductive types but I can't seem to find them. Could anyone point me in the right direction?

#### Kyle Miller (Apr 16 2022 at 16:53):

Here's a quick tactic proof:

```
inductive tv
| vtrue
| vundef
| vfalse
def tv_nat (a : tv) : ℕ := tv.cases_on a 3 2 1
theorem tv_unnat {a b : tv} (h : (tv_nat a) = (tv_nat b)) : a = b :=
by { cases a; cases b; simp [tv_nat] at h; contradiction }
```

(For Prop-valued things, it's better to use `theorem`

or `lemma`

, which is why I changed it from `def`

.)

#### Fingy Soupy (Apr 16 2022 at 17:10):

Thanks, I think it's going to take me a while to unpack all that but I appreciate it :)

Is there a functional different between def and theorem?

#### Kyle Miller (Apr 16 2022 at 17:21):

Yeah, there's a functional difference. It's sort of like the difference between `let`

and `have`

: theorems are opaque, since you're just caring that there is a proof, not what the proof is. Unlike definitions, theorems don't generate equation lemmas, and since the proof can't be inspected, Lean is able to typecheck proofs of theorems in parallel. Definitions need to be processed completely sequentially.

#### Kyle Miller (Apr 16 2022 at 17:23):

Example of opaqueness:

```
def a : ℕ := 37
noncomputable theorem b : ℕ := 37
example : a = 37 := rfl
example : b = 37 := rfl -- error
```

(Don't worry about the `noncomputable`

. That's telling Lean "yes, I know that theorems don't generate executable code, I know what I'm doing here." It's not the cause of the difference in behavior.)

#### Fingy Soupy (Apr 16 2022 at 18:06):

Ah, that is very informative. Thank you very much!

#### Fingy Soupy (Apr 16 2022 at 22:45):

What does the ';' after a tactic do?

I see that it is causing the other tactics to be applied to all of the goals rather than just the current goal but I can't find a reference to it in the documentation

#### Kyle Miller (Apr 16 2022 at 22:52):

https://leanprover.github.io/theorem_proving_in_lean/tactics.html#tactic-combinators

Last updated: Dec 20 2023 at 11:08 UTC