3
$\begingroup$

In Lean, how do I prove that a variable, or more generally an expression, ranging over a finite type must be equal to one of the values of the finite type?

In particular, the following should be easy, but I do not know where to begin:

inductive Foo where 
  | alice 
  | bob 
  | charles

open Foo

inductive Bar where 
  | boy
  | girl

open Bar

def f : Foo → Bar 
  | charles => boy
  | alice => girl
  | bob => boy

example (x:Foo) (h: f x = boy): (x=bob ∨ x=charles) :=
  sorry
$\endgroup$

2 Answers 2

4
$\begingroup$

Here's a shorter proof using the equation compiler:

example : ∀ (x : Foo), f x = boy → x = bob ∨ x = charles
| .bob, _ => .inl rfl
| .charles, _ => .inr rfl
$\endgroup$
3
$\begingroup$

Here is a verbose/expressive proof in "term mode":

example (x:Foo) (h: f x = boy): (x=bob ∨ x=charles) :=   
  match x with
    | bob => 
      have h : bob = bob := rfl
      show bob=bob ∨ bob=charles from Or.inl h
    | charles =>
      have h : charles = charles := rfl
      show charles=bob ∨ charles=charles from Or.inr h
    | alice => 
      have h1 : f alice = girl := rfl
      have h2 : girl ≠ boy := Bar.noConfusion
      have h3 : f alice = boy := h
      have h4 : girl = boy := h1 ▸ h3
      show alice=bob ∨ alice=charles from False.elim  (h2 h4)
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.