Case analysis on match in assumptions

Stream: new members

[Thalia Archibald]

I'm writing a verified Brainfuck compiler as an exercise in learning Lean. As a small lemma, I want to prove that Token.ofChar and Token.toChar are inverses of each other; however, the fallthrough case of Token.ofChar is tripping me up. It should just be a simple proof by contradiction with some t = none, but matching in the proof does not come with a proof that c is not equal to the values of the other cases.

In a Coq-style tactic-oriented approach, I'd destruct on decideable equality of the Char for each of the cases, which would introduce hypotheses for the equalities. The match would then need to somehow be desugared into disjunctions and implications and I could pull it apart according to the equalities.

I think it's likely I'm approaching this wrong. Any suggestions?

inductive Token
  | right
  | left
  | inc
  | dec
  | output
  | input
  | head
  | tail
deriving Repr

def Token.ofChar : Char → Option Token
  | '>' => Token.right
  | '<' => Token.left
  | '+' => Token.inc
  | '-' => Token.dec
  | '.' => Token.output
  | ',' => Token.input
  | '[' => Token.head
  | ']' => Token.tail
  | _ => none

def Token.toChar : Token → Char
  | Token.right => '>'
  | Token.left => '<'
  | Token.inc => '+'
  | Token.dec => '-'
  | Token.output => '.'
  | Token.input => ','
  | Token.head => '['
  | Token.tail => ']'

theorem Token.toChar_ofChar t :
  Token.ofChar (t.toChar) = some t :=
by cases t <;> rfl

theorem Token.ofChar_toChar c t :
  some t = Token.ofChar c → c = t.toChar :=
by
  simp [Token.ofChar, Token.toChar]
  match c with
  | '>' | '<' | '+' | '-' | '.' | ',' | '[' | ']' =>
    simp; intro H; subst H; rfl
  | c' => admit

As an aside, if I replace theorem with lemma, it reports unexpected identifier; expected command for the lemma keyword. I thought they would be interchangeable. Is this a bug? I'm using Lean v4.7.0-rc2.

[Kyle Miller]

lemma is a mathlib-only command — you just need to be sure to import pretty much any module of mathlib to get it.

[Kyle Miller]

To get a hypothesis for c, you can use match h : c with syntax, but that doesn't give you the fact that it's not any of the preceding cases unfortunately.

[Thalia Archibald]

Strange that lemma isn't in the stdlib

[Thalia Archibald]

match h : c with

Is it Lean convention to lowercase hypotheses?

[Kyle Miller]

Here:

theorem Token.ofChar_toChar c t :
  some t = Token.ofChar c → c = t.toChar :=
by
  simp [Token.ofChar, Token.toChar]
  split <;> intro h <;> cases h <;> rfl

[Thalia Archibald]

split looks like it does a lot of heavy lifting. Very nice!