Incomplete pattern match

Stream: general

[Patrick Johnson]

There are three most popular ways to deal with partial functions in Lean.

The first way is to require a proof of the membership of the function's domain as a separate argument. The problem is that we need a proof whenever we want to call the function, so we also need proofs in theorem statements. If there are multiple partial functions, the theorem statement becomes hard to state and comprehend.

The second way is to use option type. It introduces unnecessary congitive overhead and forces us to work with option monad even if we want to prove something totally unrelated to the option type.

The third way is to return a junk value. This way turned out to be the most useful and easiest to work with. However, the problem is that it allows us to prove things that are false in real math. For example, nat.pred is implemented such that it returns 0 for 0, so we can prove that the predecessor of 0 is 0, which is false. Also, nat.sub is implemented such that it returns 0 if the result would be negative, so we can prove that 5 - 7 = 0, which doesn't make sense.

In Isabelle/HOL, there is an axiomatically defined constant undefined which returns a "random" value of a given type (all types are inhabited). In Lean, we can implement undefined using nonempty.some, but it still allows us to prove nonsensical things, because nonempty.some always returns the same value for the same type, so it may cancel out if it's used in some other definition.

It would be nice if we could do something like this:

def pred : ℕ → ℕ
| (a+1) := a

def sub : ℕ → ℕ → ℕ
| a 0 := a
| (a+1) (b+1) := sub a b

The equation compiler would basically do the following, except it would make the definitions computable:

import tactic

noncomputable def pred : ℕ → ℕ :=
begin
  refine (_ : ∃ (f : ℕ → ℕ), ∀ (a : ℕ), f a.succ = a).some,
  use λ (a : ℕ), @nat.rec (λ _, ℕ) 0 (λ a _, a) a,
  simp,
end

lemma pred_succ {a : ℕ} : pred a.succ = a :=
pred._proof_1.some_spec _

noncomputable def sub : ℕ → ℕ → ℕ :=
begin
  refine (_ : ∃ (f : ℕ → ℕ → ℕ),
    (∀ (a : ℕ), f a 0 = a) ∧ (∀ (a b : ℕ), f a.succ b.succ = f a b)).some,
  use λ (a b : ℕ), @nat.rec (λ _, ℕ) a (λ _, pred) b,
  split,
  { simp },
  { rintro a b,
    change pred _ = _,
    induction b with b ih,
    { rw [pred_succ] },
    { change pred (pred _) = _,
      rw ih }},
end

lemma sub_zero' {a : ℕ} : sub a 0 = a :=
sub._proof_1.some_spec.1 _

lemma sub_succ' {a b : ℕ} : sub a.succ b.succ = sub a b :=
sub._proof_1.some_spec.2 _ _

So, we can't prove anything about pred 0, just like we can't prove anything about 5 - 7
We can't even prove that 1 - 2 is equal to 2 - 3

I guess it will never be implemented in Lean 3, but are there any plans to have something like this in Lean 4? The key point is to produce computable definitions.

[Damiano Testa]

This is not intended as an answer to your question, but as my way of dealing with the junk values. I have been much happier with nat-subtraction when I started parsing it in my mind as max 0 ("real subtraction"). Thus, what you prove is correct, it is just that the symbol lean.- means something different than maths.-.

[Damiano Testa]

Once I made peace with this, I started even enjoying the fact that if f is a polynomial, then f.derivative.nat_degree ≤ f.nat_degree - 1, with no extra assumptions! Thus, lean.- is goofy, but has ways of surprising you with clean statements.

[Yaël Dillies]

In particular, our goofy nat subtraction has a lot of desirable properties. The main is probably that it is adjoint to addition, namely a - b ≤ c ↔ a ≤ b + c (docs#tsub_le_iff_left). And many other "nonsensical" mathlib definitions are like this.

[Yaël Dillies]

In Isabelle/HOL, there is an axiomatically defined constant undefined which returns a "random" value of a given type (all types are inhabited)

In Lean too, it's called undefined/sorry.

[Patrick Johnson]

Yaël Dillies said:

In Lean too, it's called undefined/sorry.

That's incorrect. In Lean, sorry is a way of cheating - it allows you to prove false (artificially inhabit an empty type). In Isabelle/HOL, undefined is used in real proofs for junk values and you can't derive false from it (implementation bugs aside).

[Yaël Dillies]

So what does undefined : false mean?

[Patrick Johnson]

It means a syntax error. Isabelle is not a dependently-typed language.

[Kyle Miller]

Here's a Lean 4 way to almost do the right thing (it's not quite right because for example rfl : sub 0 1 = sub 0 2).

constant pred_undefined : Nat

def pred : Nat → Nat
| 0 => pred_undefined
| a+1 => a

constant sub_undefined : Nat

def sub : Nat → Nat → Nat
| 0, b+1 => sub_undefined
| a, 0 => a
| a+1, b+1 => sub a b

#eval pred 0
-- 0
#eval sub 0 1
-- 0

example : pred 0 = sub 0 1 := by
  simp [pred, sub]
  -- ⊢ pred_undefined = sub_undefined
  rfl
  /-
  tactic 'rfl' failed, equality lhs
    pred_undefined
  is not definitionally equal to rhs
    sub_undefined
  ⊢ pred_undefined = sub_undefined
  -/

Note that constant requires the type have an Inhabited instance, and it's not causing the definitions to depend on any additional axioms.

#print axioms sub
-- 'sub' does not depend on any axioms

[Kyle Miller]

After writing that, it occurred to me that you can do the same sort of implementation in Lean 3, but using irreducible definitions instead of constants.

@[irreducible] def pred_undefined : ℕ := 0

def pred : ℕ → ℕ
| 0 := pred_undefined
| (a+1) := a

@[irreducible] def sub_undefined : ℕ := 0

def sub : ℕ → ℕ → ℕ
| 0 (b+1) := sub_undefined
| a 0 := a
| (a+1) (b+1) := sub a b

#eval pred 0
-- 0
#eval sub 0 1
-- 0

example : pred 0 = sub 0 1 :=
begin
  simp [pred, sub],
  -- ⊢ pred_undefined = sub_undefined
  refl,
  /-
  invalid apply tactic, failed to unify
    pred_undefined = sub_undefined
  with
    ?m_2 = ?m_2
  state:
  ⊢ pred_undefined = sub_undefined
  -/
end

[Kyle Miller]

Here's one that goes a little farther by making there be more undefined values.

@[irreducible] def sub_undefined (b : ℕ) : ℕ := 0

def sub : ℕ → ℕ → ℕ
| 0 (b+1) := sub_undefined b
| a 0 := a
| (a+1) (b+1) := sub a b

example : sub 0 1 = sub 0 2 :=
begin
  simp [sub],
  -- ⊢ sub_undefined 0 = sub_undefined 1
  refl,
  /-
  invalid apply tactic, failed to unify
    sub_undefined 0 = sub_undefined 1
  with
    ?m_2 = ?m_2
  -/
end

[Kyle Miller]

Though you can do

example : sub 0 1 = sub 0 1 := rfl

Would that be provable in Isabelle/HOL?

[Eric Wieser]

Your sub_undefined is interesting, because I think you can prove 1 - 2 = 2 - 3 (edit: without cheating like kevin)

[Kevin Buzzard]

@[irreducible] def sub_undefined (b : ℕ) : ℕ := 0

def sub : ℕ → ℕ → ℕ
| 0 (b+1) := sub_undefined b
| a 0 := a
| (a+1) (b+1) := sub a b

example : sub 0 1 = sub 0 2 :=
begin
  simp [sub],
  delta sub_undefined,
  refl, -- muhahaha
end

[Kevin Buzzard]

I think you'll find that if it compiles then it's not cheating, by definition!

[Kyle Miller]

Patrick Johnson said:

In Isabelle/HOL, there is an axiomatically defined constant undefined which returns a "random" value of a given type (all types are inhabited). In Lean, we can implement undefined using nonempty.some, but it still allows us to prove nonsensical things, because nonempty.some always returns the same value for the same type, so it may cancel out if it's used in some other definition.

I'm not familiar with Isabelle/HOL, but when trying to learn more about undefined, it looks like undefined = undefined for a given type. If that's true, that seems to mean it has the same properties as nonempty.some.

[Kyle Miller]

@Kevin Buzzard I forgot that irreducible only applies to the elaborator! Oh well. I think the Lean 4 version is safe from anything that (certainly you can't use delta on a constant).

[Reid Barton]

In Isabelle can you prove 0 - 1 = 0 - 2?

[Reid Barton]

Oh, I guess you said you can't

[Reid Barton]

I think the semantics of this kind of thing get tricky. Let's say sub uses undefined in the "garbage" case. Then I copy and paste the definition of sub to sub2. Does sub 0 1 = sub2 0 1?

[Kyle Miller]

Reid Barton said:

In Isabelle can you prove 0 - 1 = 0 - 2?

It looks like it depends on how you define the function.

If you do

fun sub :: "nat ⇒ nat => nat"
where
  "sub a b = (case b of 0 ⇒ a | Suc b' => case sub a b' of Suc k ⇒ k)"

then the undefined jams up the case (and I, who installed Isabelle only about an hour ago, couldn't tell whether case undefined of ... could simplify to undefined or not).

lemma foo4 : "sub 0 1 = sub 0 2"
  by (simp_all add: sub_def)
  (* fails. goal: undefined = (case undefined of Suc k ⇒ k) *)

If instead we define subtraction like

fun sub2 :: "nat ⇒ nat => nat"
where
  "sub2 a 0 = a"
| "sub2 a (Suc b) = (case a of Suc a' ⇒ sub2 a' b)"

then you can prove 0 - 1 = 0 - 2 since it simplifies to undefined = undefined, which does end up being true in Isabelle.

lemma foo24 : "sub2 0 1 = sub2 0 (Suc 1)"
  by (simp_all add: sub_def)

lemma foo1: "(undefined::nat) = undefined"
  by simp_all

With both definitions you can't prove 0 - 1 = 0.

lemma foo23: "sub2 0 1 = 0"
  by (simp_all add: sub_def)
  (* fails. goal: undefined = 0 *)

Isabelle code

theory Scratch
  imports Main
begin

lemma foo1: "(undefined::nat) = undefined"
  by simp_all

fun sub :: "nat ⇒ nat => nat"
where
  "sub a b = (case b of 0 ⇒ a | Suc b' => case sub a b' of Suc k ⇒ k)"

lemma foo2: "sub 0 0 = 0"
  by (simp_all add: sub_def)

lemma foo3: "sub 0 1 = 0"
  by (simp_all add: sub_def)
  (* fails: undefined = 0 *)

lemma foo4 : "sub 0 1 = sub 0 2"
  by (simp_all add: sub_def)
  (* fails:  undefined = (case undefined of Suc k ⇒ k) *)

fun sub2 :: "nat ⇒ nat => nat"
where
  "sub2 a 0 = a"
| "sub2 a (Suc b) = (case a of Suc a' ⇒ sub2 a' b)"

lemma foo22: "sub2 0 0 = 0"
  by (simp_all add: sub_def)

lemma foo23: "sub2 0 1 = 0"
  by (simp_all add: sub_def)
  (* fails: undefined = 0 *)

lemma foo24 : "sub2 0 1 = sub2 0 (Suc 1)"
  by (simp_all add: sub_def)

end

[Reid Barton]

So if the answer to "can you prove 0 - 1 = 0 - 2" is "it depends on the exact definition of -" then I'm not convinced that is an improvement on the answer "yes"

[Kyle Miller]

Whatever the answer, it seems like having a special

@[irreducible] def undefined {α : Type*} [inhabited α] : α := arbitrary α

could still be useful as a way to mark which values are explicitly junk, while doing so in a way that, if it's something you're concerned about, gives you some amount of protection from proving nonsense (so long as you avoid piercing through the irreducible like Kevin did, though that's irrelevant in Lean 4, and also with the caveat that you still need to think about whether a function will evaluate to undefined).

Lean 3 example with undefined

namespace foo
-- in a namespace since there is already a top-level `meta def undefined`

@[irreducible] def undefined {α : Type*} [inhabited α] : α := arbitrary α

def sub : ℕ → ℕ → ℕ
| 0 (b+1) := undefined
| a 0 := a
| (a+1) (b+1) := sub a b

example : sub 0 1 = sub 0 2 := rfl

example : sub 0 1 = 0 :=
begin
  unfold sub,
  -- ⊢ undefined = 0
  refl,
  -- failed to unify
end

end foo

[Patrick Johnson]

When I said

In Isabelle/HOL, there is an axiomatically defined constant undefined which returns a "random" value of a given type (all types are inhabited). In Lean, we can implement undefined using nonempty.some, but it still allows us to prove nonsensical things, because nonempty.some always returns the same value for the same type, so it may cancel out if it's used in some other definition.

my point was not that Isabelle has something that lean doesn't, but that different theorem provers deal with junk cases in different ways. And yes, undefined is just like nonempty.some in Lean (it's a fixed value of the given type, but we don't know the exact value, except for singleton types). The point is that in Isabelle, undefined is preferred over some exact default value in junk cases. But it's still not the best way to deal with it, since it may cancel out with undefineds from other functions.

In Lean, I think this definition would be much better:

import data.string.basic

@[irreducible]
def junk {α β : Sort*} [inhabited β] (a : α) : β := default

def pred : ℕ → ℕ
| 0 := junk "pred"
| (a+1) := a

def sub : ℕ → ℕ → ℕ
| a 0 := a
| 0 (b+1) := junk ("sub", b)
| (a+1) (b+1) := sub a b

What I would like to see in Lean 4 is that we can make opaque rather than irreducible definitions (opaque is the kernel's version of irreducible, rather than elaborator's) and to have some macro junk which passes everything from the current definition's context to the junk function in a tuple, so that we don't have to deal with it explicitly.

[Kyle Miller]

That's like sub_undefined in this message but generalized. For what it's worth, it does have some potentially unexpected behavior:

example : sub 0 1 = sub 1 2 := rfl

[Kyle Miller]

Patrick Johnson said:

What I would like to see in Lean 4 is that we can make opaque rather than irreducible definitions (opaque is the kernel's version of irreducible, rather than elaborator's) and to have some macro junk which passes everything from the current definition's context to the junk function in a tuple, so that we don't have to deal with it explicitly.

Expect for the macro part, constant does the first part, right?

[Kyle Miller]

constant junk {α β : Type} [Inhabited β] (a : α) : β := default

def pred : Nat → Nat
| 0 => junk "pred"
| a+1 => a

def sub : Nat → Nat → Nat
| a, 0 => a
| 0, b+1 => junk ("sub", b)
| a+1, b+1 => sub a b

[Brandon Brown]

Naive question, why does it not make sense that pred 0 is 0 and that 5 - 7 = 0 when the numbers are Nat? Seems very reasonable to me...

[Kyle Miller]

It both makes sense and doesn't make sense. It makes sense in that it's monus, but it doesn't make sense in that it doesn't agree with the minus when you embed Nat into Int.

[Kyle Miller]

I think whether it makes sense or not just depends on what you're trying to model.

[Kevin Buzzard]

Mathematically it's bad, for sociological reasons. Computer scientists have seen phenomena like this before (eg perhaps 5/2=2 in a system with integers and division) but to a mathematician (who has probably never heard of types) statements like "0-1=0" and "5/2=2" are indisputably wrong which is problematic. When a mathematician talks about a-b with a,b naturals they would never mean monus, because they've never heard of monus and monus is basically mathematically useless even though it has a role in CS

[Brandon Brown]

But if you haven't invented the integers or rationals yet, then why is 5 - 7 = 0 wrong? It wouldn't make sense to think of embeddings if those supersets haven't been defined yet right?

[Kevin Buzzard]

We invented those things hundreds of years ago and we're not trying to market the software to mathematicians who haven't discovered them yet because they're all dead.

[Kevin Buzzard]

The concept of the integers having "not been defined yet" is alien to us (as is the concept of being artificially restricted to answers in a certain type because we think about numerals in a more fluid way)

[Alex J. Best]

If mathematicians want to write monus they normally end up writing something like min 0 (a - b) I've basically never seen this ceiling subtraction as it's own function

[Ruben Van de Velde]

Wouldn't they write "max"?