Partial functions using `option`

Stream: new members

[Rémi Bottinelli]

Hey! I'm reading #tpil, in which they propose as an exercise to define partial functions using the option type, and to verify that composition behaves as expected.
Here is what I have:

inductive op (α : Sort u)
| so (a : α) : op
| no {} : op

example {α : Sort u} (x : op α) : (x = op.no) ↔ ¬ (∃ a : α, x = op.so a) :=
⟨ λ xisno ⟨a,xissoa⟩,  op.no_confusion (xissoa.symm.trans xisno)
, λ noexists,
    @op.rec
      α
      (λ (x : op α), ¬ (∃ a : α, x = op.so a) → x = op.no )
      ( λ (b : α) noexists, absurd (⟨b,rfl⟩ : ∃ a, op.so b = op.so a) noexists )
      ( λ noexists, rfl)
      x
      noexists
⟩


def comp {α β γ : Sort u} (f : α → op β) (g : β → op γ) : α → op γ :=
λ x : α, op.rec (λ b, g b) (op.no) (f x)

lemma comp_part {α β γ : Sort u} (f : α → op β) (g : β → op γ) :
  ∀ x, (comp f g x) = op.no ↔
       ( f x = op.no ∨
         ( ∃ y : β, f x = op.so y ∧ g y = op.no)) := sorry

but trying to prove comp_part, I get stuck after the basic split/intro boilerplate. I tried defining intermediary lemmas but it doesn't seem to be any use. I also looked at the documentation to see how it's implemented in practice, but it seems this kind of "partial function type" is more of a toy example, and partial functions are implemented differently in practice (using predicates and subtypes). I'd appreciate some hints on how to proceed!

[Kyle Miller]

You can use the raw recursor if you want, but match syntax is pretty nice. For the sorry, it comes down to doing cases on f x. To do this effectively, you need to have an equality that lets you relate f x to the possible cases, and tactic#generalizes' is one solution to this.

import tactic.basic

universe u

inductive op (α : Sort u)
| so (a : α) : op
| no {} : op

example {α : Sort u} (x : op α) : (x = op.no) ↔ ¬ (∃ a : α, x = op.so a) :=
by { cases x; simp }

def comp {α β γ : Sort u} (f : α → op β) (g : β → op γ) : α → op γ :=
λ x, match f x with
     | (op.so b) := g b
     | op.no := op.no
     end

lemma comp_part {α β γ : Sort u} (f : α → op β) (g : β → op γ) (x : α) :
  comp f g x = op.no ↔ f x = op.no ∨ ∃ y : β, f x = op.so y ∧ g y = op.no :=
begin
  generalize' h : f x = y,
  cases y; simp [comp, h],
end

[Kyle Miller]

Here's how you can do that without generalize':

lemma comp_part {α β γ : Sort u} (f : α → op β) (g : β → op γ) (x : α) :
  comp f g x = op.no ↔ f x = op.no ∨ ∃ y : β, f x = op.so y ∧ g y = op.no :=
begin
  have : ∃ y, f x = y := ⟨f x, rfl⟩,
  cases this with y h,
  cases y; simp [comp, h],
end

[Kevin Buzzard]

Here's the API more generally:

import tactic

universe u

inductive op (α : Sort u)
| so (a : α) : op
| no {} : op

example {α : Sort u} : ∀ (x : op α), (x = op.no) ↔ ¬ (∃ a : α, x = op.so a)
| (op.so a) := by simp
| op.no := by simp

def comp {α β γ : Sort u} (f : α → op β) (g : β → op γ) : α → op γ :=
λ x : α, op.rec (λ b, g b) (op.no) (f x)

variables {α β γ : Sort u} (f : α → op β) (g : β → op γ)

lemma comp_no (a : α) (h : f a = op.no) : comp f g a = op.no :=
begin
  unfold comp,
  cases f a,
  { cases h },
  { refl },
end

lemma comp_so (a : α) (b : β) (h : f a = op.so b) : comp f g a = g b :=
begin
  unfold comp,
  cases f a,
  { cases h, refl },
  { cases h },
end

[Kyle Miller]

Regarding partial function types: docs#option is the partial value where you can computably tell whether a value is present, and docs#part is the one where you can't (you need to be able to offer a proof of whatever dom might be), though the value is computable if you're able to prove it's present.

[Kevin Buzzard]

I feel that questions like this are very much on the "type theory" side of Lean and whilst I find them quite interesting as little puzzles, I'm not sure they're too useful for mathematicians (I don't teach anything like this in my course). Getting the basic API out (comp_no and comp_so) from comp is just a case of knowing what the rules of refl are in some sense; the point is that the output of a recursor applied to a constructor is what the corresponding recursor input is, and the proof is refl. I remember spending some time starting at the relevant page of the reference manual when I was getting my head around all of this.

[Kyle Miller]

I'm not sure if there's anything like it in mathlib, but then there's also a fully noncomputable version of partial values:

structure nc_option (α : Type*) :=
(p : α → Prop)
(subsingleton : ∀ x y, p x → p y → x = y)

This is (noncomputably) equivalent to option, and not only can you not tell whether the value is present, but you can't tell what the value even is.

[Kyle Miller]

This composition, by the way, is the Kleisli arrow (known as docs#fish) for option. It seems like there's not really that much about it in mathlib, but at least it's there.

import data.option.basic
import tactic.basic

universe u

example {α : Type u} (x : option α) : (x = none) ↔ ¬ (∃ a : α, x = some a) :=
by { cases x; simp }

def comp {α β γ : Type u} (f : α → option β) (g : β → option γ) : α → option γ :=
f >=> g

lemma comp_some {α β γ : Type u} {f : α → option β} {g : β → option γ} {x : α} {y : β}
  (h : f x = some y) : comp f g x = g y :=
by simp [comp, fish, h]

lemma comp_none {α β γ : Type u} {f : α → option β} {g : β → option γ} {x : α}
  (h : f x = none) : comp f g x = none :=
by simp [comp, fish, h]

lemma comp_part {α β γ : Type u} {f : α → option β} {g : β → option γ} {x : α} :
  comp f g x = none ↔ f x = none ∨ ∃ y : β, f x = some y ∧ g y = none :=
begin
  generalize' h : f x = y,
  cases y,
  { rw [comp_none h],
    simp, },
  { rw [comp_some h],
    simp, },
end

[Yaël Dillies]

You might want to have a look at docs#PartialFun_equiv_Pointed which states that partial functions modelled with pfun and modelled with option are noncomputably the same.

[Rémi Bottinelli]

Woah, thanks all :) I don't know why, but I always trip on this "inspect-on-equality" style of functions.

[Rémi Bottinelli]

I went with:

lemma comp_part {α β γ : Sort u} (f : α → op β) (g : β → op γ) :
  ∀ x, (comp f g x) = op.no ↔  ( f x = op.no ∨ ( ∃ y : β, f x = op.so y ∧ g y = op.no)) :=
begin
  intro x,
  cases h : f x;
  {unfold comp, simp, rw h,},
end

[Rémi Bottinelli]

And to be honest, this for me is a clear example of how much tactic style simplifies writing proofs. Inspector-style/recursion becomes very confusing quite quickly, but via tactics, it's very much a "game" you play with lean.