## 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: Aug 03 2023 at 10:10 UTC