Reverse cases_on

Stream: general

[Fingy Soupy]

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]

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]

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]

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]

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]

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

[Fingy Soupy]

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]

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