Handling impossible cases in definitions

Stream: new members

[Dan Plyukhin]

I often write definitions where certain cases are impossible because of a hypothesis. What's the idiomatic way to write it? Here's an example:

  -- You can write partial functions by depending on the proof of a proposition.
  def optionify {α β : Type} (f : α → Option β) (h : ∀ a, ∃ b, f a = some b) : α → β :=
    fun a =>
      match f a, h a with
      | some b, _ => b
      | none, foo =>
        have: False := by cases foo; contradiction
        this.elim

The none branch is a little annoying because I have to explicitly construct False and use the eliminator.

[Damiano Testa]

by simp_all seems to solve it for you.

[Dan Plyukhin]

Oh cool! But I have an issue for more complicated cases. I would think I can write something like this:

      | none, foo => by cases foo; contradiction

But I get a sorting error on cases foo:

type mismatch when assigning motive
  fun t => foo = t → β
has type
  (∃ b, none = some b) → Type : Type 1
but is expected to have type
  (∃ b, none = some b) → Prop : Type

Why does cases foo get stuck where simp_all succeeds?

[Aaron Liu]

This seems to be a bug

[Mitchell Lee]

This is not a bug. It is happening because the cases tactic uses docs#Exists.elim, which only applies if the motive (called b in the documentation) is a proposition. See here for more details: #new members > Applying tactic `cases` on a non-variable @ 💬

So, the cases tactic only works inside a proof (i.e. when constructing a term whose type is a proposition). In general, it is not recommended to use tactics for anything except proofs. With this in mind, here is one way you can write your function:

  -- You can write partial functions by depending on the proof of a proposition.
  def optionify {α β : Type} (f : α → Option β) (h : ∀ a, ∃ b, f a = some b) : α → β :=
    fun a =>
      match f a, h a with
      | some b, _ => b
      | none, foo => False.elim (by cases foo; contradiction)

[Aaron Liu]

I see. I remember the error message for that case being a little different so I got confused.

[Mitchell Lee]

Alternatively, there is a tactic exfalso that changes any goal to False. Since this is a proposition, you can then use the cases tactic afterwards.

  -- You can write partial functions by depending on the proof of a proposition.
  def optionify {α β : Type} (f : α → Option β) (h : ∀ a, ∃ b, f a = some b) : α → β :=
    fun a =>
      match f a, h a with
      | some b, _ => b
      | none, foo => by exfalso; cases foo; contradiction

[Dan Plyukhin]

Nice! But if you don't recommend using tactics outside a proof, how would you usually write a function like optionify? i.e. a function where some cases are impossible, but it's not immediately apparent to the type checker that they're impossible

[Mitchell Lee]

I think I most prefer False.elim (by cases foo; contradiction). Here, by cases foo; contradiction is a proof of the proposition False, so this isn't an example of using tactics outside a proof.

[Mitchell Lee]

The way that uses the exfalso tactic is also acceptable and completely equivalent, though. You should use that one if you prefer it.

It's not recommended to use tactics outside a proof because of issues like the one you ran into with the cases tactic, and because it can be hard to reason about definitions that were constructed using tactics. In this case, though, it isn't a problem to use the exfalso tactic as long as you understand what's going on.

[Kyle Miller]

Here's an obscure way to do cases:

def optionify {α β : Type} (f : α → Option β) (h : ∀ a, ∃ b, f a = some b) : α → β :=
    fun a =>
      match f a, h a with
      | some b, _ => b
      | none, foo => False.elim <| nomatch foo

(The match itself could theoretically handle this itself, but it's this large elimination issue that's been mentioned (e.g., not being able to do cases on Exists when the goal is a type) that's preventing it. Using False.elim lets match do its work, and nomatch is syntax for a zero-alternative match.)