Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro

! This file was ported from Lean 3 source module data.nat.psub
! leanprover-community/mathlib commit 70d50ecfd4900dd6d328da39ab7ebd516abe4025
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Option.Basic
import Mathlib.Data.Nat.Basic

/-!
# Partial predecessor and partial subtraction on the natural numbers

The usual definition of natural number subtraction (`Nat.sub`) returns 0 as a "garbage value" for
`a - b` when `a < b`. Similarly, `Nat.pred 0` is defined to be `0`. The functions in this file
wrap the result in an `Option` type instead:

## Main definitions

- `Nat.ppred`: a partial predecessor operation
- `Nat.psub`: a partial subtraction operation

-/


namespace Nat

/-- Partial predecessor operation. Returns `ppred n = some m`
  if `n = m + 1`, otherwise `none`. -/
def 
ppred: β„• β†’ Option β„•
ppred
:
β„•: Type
β„•
β†’
Option: Type ?u.4 β†’ Type ?u.4
Option
β„•: Type
β„•
| 0 =>
none: {Ξ± : Type ?u.24} β†’ Option Ξ±
none
| n + 1 =>
some: {Ξ± : Type ?u.105} β†’ Ξ± β†’ Option Ξ±
some
n #align nat.ppred
Nat.ppred: β„• β†’ Option β„•
Nat.ppred
@[simp] theorem
ppred_zero: ppred 0 = none
ppred_zero
:
ppred: β„• β†’ Option β„•
ppred
0: ?m.233
0
=
none: {Ξ± : Type ?u.243} β†’ Option Ξ±
none
:=
rfl: βˆ€ {Ξ± : Sort ?u.275} {a : Ξ±}, a = a
rfl
@[simp] theorem
ppred_succ: βˆ€ {n : β„•}, ppred (succ n) = some n
ppred_succ
:
ppred: β„• β†’ Option β„•
ppred
(
succ: β„• β†’ β„•
succ
n: ?m.296
n
) =
some: {Ξ± : Type ?u.300} β†’ Ξ± β†’ Option Ξ±
some
n: ?m.296
n
:=
rfl: βˆ€ {Ξ± : Sort ?u.306} {a : Ξ±}, a = a
rfl
/-- Partial subtraction operation. Returns `psub m n = some k` if `m = n + k`, otherwise `none`. -/ def
psub: β„• β†’ β„• β†’ Option β„•
psub
(m :
β„•: Type
β„•
) :
β„•: Type
β„•
β†’
Option: Type ?u.329 β†’ Type ?u.329
Option
β„•: Type
β„•
| 0 =>
some: {Ξ± : Type ?u.350} β†’ Ξ± β†’ Option Ξ±
some
m | n + 1 =>
psub: β„• β†’ β„• β†’ Option β„•
psub
m n >>=
ppred: β„• β†’ Option β„•
ppred
#align nat.psub
Nat.psub: β„• β†’ β„• β†’ Option β„•
Nat.psub
@[simp] theorem
psub_zero: βˆ€ {m : β„•}, psub m 0 = some m
psub_zero
:
psub: β„• β†’ β„• β†’ Option β„•
psub
m: ?m.717
m
0: ?m.722
0
=
some: {Ξ± : Type ?u.732} β†’ Ξ± β†’ Option Ξ±
some
m: ?m.717
m
:=
rfl: βˆ€ {Ξ± : Sort ?u.738} {a : Ξ±}, a = a
rfl
@[simp] theorem
psub_succ: βˆ€ {m n : β„•}, psub m (succ n) = psub m n >>= ppred
psub_succ
:
psub: β„• β†’ β„• β†’ Option β„•
psub
m: ?m.763
m
(
succ: β„• β†’ β„•
succ
n: ?m.768
n
) =
psub: β„• β†’ β„• β†’ Option β„•
psub
m: ?m.763
m
n: ?m.768
n
>>=
ppred: β„• β†’ Option β„•
ppred
:=
rfl: βˆ€ {Ξ± : Sort ?u.802} {a : Ξ±}, a = a
rfl
theorem
pred_eq_ppred: βˆ€ (n : β„•), pred n = Option.getD (ppred n) 0
pred_eq_ppred
(n :
β„•: Type
β„•
) :
pred: β„• β†’ β„•
pred
n = (
ppred: β„• β†’ Option β„•
ppred
n).
getD: {Ξ± : Type ?u.828} β†’ Option Ξ± β†’ Ξ± β†’ Ξ±
getD
0: ?m.835
0
:=

Goals accomplished! πŸ™

zero
n✝: β„•


succ
pred (succ n✝) = Option.getD (ppred (succ n✝)) 0

zero
n✝: β„•


succ
pred (succ n✝) = Option.getD (ppred (succ n✝)) 0

Goals accomplished! πŸ™
#align nat.pred_eq_ppred
Nat.pred_eq_ppred: βˆ€ (n : β„•), pred n = Option.getD (ppred n) 0
Nat.pred_eq_ppred
theorem
sub_eq_psub: βˆ€ (m n : β„•), m - n = Option.getD (psub m n) 0
sub_eq_psub
(m :
β„•: Type
β„•
) : βˆ€
n: ?m.938
n
, m -
n: ?m.938
n
= (
psub: β„• β†’ β„• β†’ Option β„•
psub
m
n: ?m.938
n
).
getD: {Ξ± : Type ?u.945} β†’ Option Ξ± β†’ Ξ± β†’ Ξ±
getD
0: ?m.952
0
| 0 =>
rfl: βˆ€ {Ξ± : Sort ?u.1012} {a : Ξ±}, a = a
rfl
| n + 1 => (
pred_eq_ppred: βˆ€ (n : β„•), pred n = Option.getD (ppred n) 0
pred_eq_ppred
(m - n)).
trans: βˆ€ {Ξ± : Sort ?u.1147} {a b c : Ξ±}, a = b β†’ b = c β†’ a = c
trans
<|

Goals accomplished! πŸ™
m, n: β„•


Option.getD (ppred (m - n)) 0 = Option.getD (psub m (n + 1)) 0
m, n: β„•


Option.getD (ppred (m - n)) 0 = Option.getD (psub m (n + 1)) 0
m, n: β„•


Option.getD (ppred (Option.getD (psub m n) 0)) 0 = Option.getD (psub m (n + 1)) 0
m, n: β„•


Option.getD (ppred (m - n)) 0 = Option.getD (psub m (n + 1)) 0
m, n: β„•


Option.getD (ppred (m - n)) 0 = Option.getD (psub m (n + 1)) 0
m, n: β„•


none
m, n, val✝: β„•


some
Option.getD (ppred (Option.getD (some val✝) 0)) 0 = Option.getD (some val✝ >>= ppred) 0
m, n: β„•


none
m, n, val✝: β„•


some
Option.getD (ppred (Option.getD (some val✝) 0)) 0 = Option.getD (some val✝ >>= ppred) 0

Goals accomplished! πŸ™
#align nat.sub_eq_psub
Nat.sub_eq_psub: βˆ€ (m n : β„•), m - n = Option.getD (psub m n) 0
Nat.sub_eq_psub
@[simp] theorem
ppred_eq_some: βˆ€ {m n : β„•}, ppred n = some m ↔ succ m = n
ppred_eq_some
{m :
β„•: Type
β„•
} : βˆ€ {
n: ?m.1756
n
},
ppred: β„• β†’ Option β„•
ppred
n: ?m.1756
n
=
some: {Ξ± : Type ?u.1760} β†’ Ξ± β†’ Option Ξ±
some
m ↔
succ: β„• β†’ β„•
succ
m =
n: ?m.1756
n
| 0 =>

Goals accomplished! πŸ™

mp
ppred 0 = some m β†’ succ m = 0

mpr
succ m = 0 β†’ ppred 0 = some m

mp
ppred 0 = some m β†’ succ m = 0

mpr
succ m = 0 β†’ ppred 0 = some m
m: β„•

h: ppred 0 = some m


mp
succ m = 0
m: β„•

h: ppred 0 = some m


mp
succ m = 0
m: β„•

h: succ m = 0


mpr

Goals accomplished! πŸ™
| n + 1 =>

Goals accomplished! πŸ™
m, n: β„•


ppred (n + 1) = some m ↔ succ m = n + 1
m, n: β„•


mp
ppred (n + 1) = some m β†’ succ m = n + 1
m, n: β„•


mpr
succ m = n + 1 β†’ ppred (n + 1) = some m
m, n: β„•


ppred (n + 1) = some m ↔ succ m = n + 1
m, n: β„•


mp
ppred (n + 1) = some m β†’ succ m = n + 1
m, n: β„•


mpr
succ m = n + 1 β†’ ppred (n + 1) = some m
m, n: β„•


ppred (n + 1) = some m ↔ succ m = n + 1
m, n: β„•

h: succ m = n + 1


mpr
ppred (n + 1) = some m
m, n: β„•


ppred (n + 1) = some m ↔ succ m = n + 1
m, n: β„•

h: ppred (n + 1) = some m


mp
succ m = n + 1
m, n: β„•

h: succ m = n + 1


mpr
ppred (n + 1) = some m
m, n: β„•


ppred (n + 1) = some m ↔ succ m = n + 1
m, n: β„•

n_eq✝: m = Nat.add n 0


mpr
ppred (n + 1) = some m
m, n: β„•


ppred (n + 1) = some m ↔ succ m = n + 1
m, n: β„•

val_eq✝: Nat.add n 0 = m


mp
succ m = n + 1
m, n: β„•

n_eq✝: m = Nat.add n 0


mpr
ppred (n + 1) = some m
m, n: β„•


ppred (n + 1) = some m ↔ succ m = n + 1

mp
succ (Nat.add n 0) = n + 1
m, n: β„•


ppred (n + 1) = some m ↔ succ m = n + 1

mp
succ (Nat.add n 0) = n + 1

mpr
ppred (n + 1) = some (Nat.add n 0)
m, n: β„•


ppred (n + 1) = some m ↔ succ m = n + 1

Goals accomplished! πŸ™
#align nat.ppred_eq_some
Nat.ppred_eq_some: βˆ€ {m n : β„•}, ppred n = some m ↔ succ m = n
Nat.ppred_eq_some
-- Porting note: `contradiction` required an `intro` for the goals -- `ppred (n + 1) = none β†’ n + 1 = 0` and `n + 1 = 0 β†’ ppred (n + 1) = none` @[simp] theorem
ppred_eq_none: βˆ€ {n : β„•}, ppred n = none ↔ n = 0
ppred_eq_none
: βˆ€ {n :
β„•: Type
β„•
},
ppred: β„• β†’ Option β„•
ppred
n =
none: {Ξ± : Type ?u.2054} β†’ Option Ξ±
none
↔ n =
0: ?m.2087
0
| 0 =>

Goals accomplished! πŸ™

ppred 0 = none ↔ 0 = 0

Goals accomplished! πŸ™
| n + 1 =>

Goals accomplished! πŸ™

ppred (n + 1) = none ↔ n + 1 = 0

mp
ppred (n + 1) = none β†’ n + 1 = 0

mpr
n + 1 = 0 β†’ ppred (n + 1) = none

ppred (n + 1) = none ↔ n + 1 = 0

mp
ppred (n + 1) = none β†’ n + 1 = 0

mpr
n + 1 = 0 β†’ ppred (n + 1) = none

ppred (n + 1) = none ↔ n + 1 = 0
n: β„•

a✝: n + 1 = 0


mpr
ppred (n + 1) = none

ppred (n + 1) = none ↔ n + 1 = 0
n: β„•

a✝: ppred (n + 1) = none


mp
n + 1 = 0
n: β„•

a✝: n + 1 = 0


mpr
ppred (n + 1) = none

ppred (n + 1) = none ↔ n + 1 = 0

Goals accomplished! πŸ™
#align nat.ppred_eq_none
Nat.ppred_eq_none: βˆ€ {n : β„•}, ppred n = none ↔ n = 0
Nat.ppred_eq_none
theorem
psub_eq_some: βˆ€ {m n k : β„•}, psub m n = some k ↔ k + n = m
psub_eq_some
{m :
β„•: Type
β„•
} : βˆ€ {
n: ?m.2370
n
k: ?m.2373
k
},
psub: β„• β†’ β„• β†’ Option β„•
psub
m
n: ?m.2370
n
=
some: {Ξ± : Type ?u.2377} β†’ Ξ± β†’ Option Ξ±
some
k: ?m.2373
k
↔
k: ?m.2373
k
+
n: ?m.2370
n
= m | 0, k =>

Goals accomplished! πŸ™
m, k: β„•


psub m 0 = some k ↔ k + 0 = m

Goals accomplished! πŸ™
| n + 1, k =>

Goals accomplished! πŸ™
m, n, k: β„•


psub m (n + 1) = some k ↔ k + (n + 1) = m
m, n, k: β„•


(βˆƒ a, psub m (Nat.add n 0) = some a ∧ ppred a = some k) ↔ k + (n + 1) = m
m, n, k: β„•


psub m (n + 1) = some k ↔ k + (n + 1) = m
m, n, k: β„•


(βˆƒ a, a + Nat.add n 0 = m ∧ succ k = a) ↔ k + (n + 1) = m
m, n, k: β„•


psub m (n + 1) = some k ↔ k + (n + 1) = m

Goals accomplished! πŸ™
#align nat.psub_eq_some
Nat.psub_eq_some: βˆ€ {m n k : β„•}, psub m n = some k ↔ k + n = m
Nat.psub_eq_some
theorem
psub_eq_none: βˆ€ {m n : β„•}, psub m n = none ↔ m < n
psub_eq_none
{m n :
β„•: Type
β„•
} :
psub: β„• β†’ β„• β†’ Option β„•
psub
m n =
none: {Ξ± : Type ?u.4777} β†’ Option Ξ±
none
↔ m < n :=

Goals accomplished! πŸ™
m, n: β„•


psub m n = none ↔ m < n
m, n: β„•

s: psub m n = none


none
none = none ↔ m < n
m, n, val✝: β„•

s: psub m n = some val✝


some
some val✝ = none ↔ m < n
m, n: β„•


psub m n = none ↔ m < n
m, n: β„•

s: psub m n = none


none
none = none ↔ m < n
m, n, val✝: β„•

s: psub m n = some val✝


some
some val✝ = none ↔ m < n
m, n: β„•


psub m n = none ↔ m < n
m, n: β„•

s: psub m n = none


none
m < n
m, n: β„•


psub m n = none ↔ m < n
m, n: β„•

s: psub m n = none


none
m < n
m, n: β„•

s: psub m n = none


none
m < n
m, n, val✝: β„•

s: psub m n = some val✝


some
m, n: β„•

s: psub m n = none


none
m < n
m, n: β„•

s: psub m n = none


none
m < n
m, n: β„•

s: psub m n = none

h: m β‰₯ n


none
m, n: β„•

s: psub m n = none


none
m < n
m, n: β„•

s: psub m n = none

h: m β‰₯ n

k: β„•

e: n + k = m


none.intro
m, n: β„•

s: psub m n = none


none
m < n

Goals accomplished! πŸ™
m, n: β„•


psub m n = none ↔ m < n
m, n, val✝: β„•

s: psub m n = some val✝


some
m, n, val✝: β„•

s: psub m n = some val✝


some
m, n, val✝: β„•

s: psub m n = some val✝


some
m, n, val✝: β„•

s: psub m n = some val✝


some
m, n, val✝: β„•

s: psub m n = some val✝


some
m, n, val✝: β„•

s: psub m n = some val✝


some
n ≀ val✝ + n
m, n, val✝: β„•

s: psub m n = some val✝


some
n ≀ val✝ + n
m, n, val✝: β„•

s: psub m n = some val✝


some

Goals accomplished! πŸ™
#align nat.psub_eq_none
Nat.psub_eq_none: βˆ€ {m n : β„•}, psub m n = none ↔ m < n
Nat.psub_eq_none
theorem
ppred_eq_pred: βˆ€ {n : β„•}, 0 < n β†’ ppred n = some (pred n)
ppred_eq_pred
{n} (
h: 0 < n
h
:
0: ?m.5526
0
<
n: ?m.5521
n
) :
ppred: β„• β†’ Option β„•
ppred
n: ?m.5521
n
=
some: {Ξ± : Type ?u.5585} β†’ Ξ± β†’ Option Ξ±
some
(
pred: β„• β†’ β„•
pred
n: ?m.5521
n
) :=
ppred_eq_some: βˆ€ {m n : β„•}, ppred n = some m ↔ succ m = n
ppred_eq_some
.
2: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
2
<|
succ_pred_eq_of_pos: βˆ€ {n : β„•}, 0 < n β†’ succ (pred n) = n
succ_pred_eq_of_pos
h: 0 < n
h
#align nat.ppred_eq_pred
Nat.ppred_eq_pred: βˆ€ {n : β„•}, 0 < n β†’ ppred n = some (pred n)
Nat.ppred_eq_pred
theorem
psub_eq_sub: βˆ€ {m n : β„•}, n ≀ m β†’ psub m n = some (m - n)
psub_eq_sub
{
m: ?m.5620
m
n} (
h: n ≀ m
h
:
n: ?m.5623
n
≀
m: ?m.5620
m
) :
psub: β„• β†’ β„• β†’ Option β„•
psub
m: ?m.5620
m
n: ?m.5623
n
=
some: {Ξ± : Type ?u.5668} β†’ Ξ± β†’ Option Ξ±
some
(
m: ?m.5620
m
-
n: ?m.5623
n
) :=
psub_eq_some: βˆ€ {m n k : β„•}, psub m n = some k ↔ k + n = m
psub_eq_some
.
2: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
2
<|
Nat.sub_add_cancel: βˆ€ {n m : β„•}, m ≀ n β†’ n - m + m = n
Nat.sub_add_cancel
h: n ≀ m
h
#align nat.psub_eq_sub
Nat.psub_eq_sub: βˆ€ {m n : β„•}, n ≀ m β†’ psub m n = some (m - n)
Nat.psub_eq_sub
-- Porting note: we only have the simp lemma `Option.bind_some` which uses `Option.bind` not `>>=` theorem
psub_add: βˆ€ (m n k : β„•), psub m (n + k) = do let __do_lift ← psub m n psub __do_lift k
psub_add
(
m: ?m.5751
m
n
k: ?m.5757
k
) :
psub: β„• β†’ β„• β†’ Option β„•
psub
m: ?m.5751
m
(
n: ?m.5754
n
+
k: ?m.5757
k
) = (do
psub: β„• β†’ β„• β†’ Option β„•
psub
(← psub m n): ?m.5865
(←
psub: β„• β†’ β„• β†’ Option β„•
psub
(← psub m n): ?m.5865
m: ?m.5751
m
(← psub m n): ?m.5865
n: ?m.5754
n
(← psub m n): ?m.5865
)
k: ?m.5757
k
) :=

Goals accomplished! πŸ™
m, n, k: β„•


psub m (n + k) = do let __do_lift ← psub m n psub __do_lift k
m, n: β„•


zero
psub m (n + zero) = do let __do_lift ← psub m n psub __do_lift zero
m, n, n✝: β„•

n_ih✝: psub m (n + n✝) = do let __do_lift ← psub m n psub __do_lift n✝


succ
psub m (n + succ n✝) = do let __do_lift ← psub m n psub __do_lift (succ n✝)
m, n, k: β„•


psub m (n + k) = do let __do_lift ← psub m n psub __do_lift k
m, n, n✝: β„•

n_ih✝: psub m (n + n✝) = do let __do_lift ← psub m n psub __do_lift n✝


succ
psub m (n + succ n✝) = do let __do_lift ← psub m n psub __do_lift (succ n✝)
m, n, k: β„•


psub m (n + k) = do let __do_lift ← psub m n psub __do_lift k

Goals accomplished! πŸ™
#align nat.psub_add
Nat.psub_add: βˆ€ (m n k : β„•), psub m (n + k) = do let __do_lift ← psub m n psub __do_lift k
Nat.psub_add
/-- Same as `psub`, but with a more efficient implementation. -/ @[inline] def
psub': β„• β†’ β„• β†’ Option β„•
psub'
(m n :
β„•: Type
β„•
) :
Option: Type ?u.6877 β†’ Type ?u.6877
Option
β„•: Type
β„•
:= if n ≀ m then
some: {Ξ± : Type ?u.6902} β†’ Ξ± β†’ Option Ξ±
some
(m - n) else
none: {Ξ± : Type ?u.6945} β†’ Option Ξ±
none
#align nat.psub'
Nat.psub': β„• β†’ β„• β†’ Option β„•
Nat.psub'
theorem
psub'_eq_psub: βˆ€ (m n : β„•), psub' m n = psub m n
psub'_eq_psub
(
m: ?m.7004
m
n: ?m.7007
n
) :
psub': β„• β†’ β„• β†’ Option β„•
psub'
m: ?m.7004
m
n: ?m.7007
n
=
psub: β„• β†’ β„• β†’ Option β„•
psub
m: ?m.7004
m
n: ?m.7007
n
:=

Goals accomplished! πŸ™
m, n: β„•


psub' m n = psub m n
m, n: β„•


psub' m n = psub m n
m, n: β„•


(if n ≀ m then some (m - n) else none) = psub m n
m, n: β„•


(if n ≀ m then some (m - n) else none) = psub m n
m, n: β„•


psub' m n = psub m n
m, n: β„•

h: n ≀ m


inl
some (m - n) = psub m n
m, n: β„•

h: Β¬n ≀ m


inr
none = psub m n
m, n: β„•


psub' m n = psub m n
m, n: β„•

h: Β¬n ≀ m


inr
none = psub m n
m, n: β„•


psub' m n = psub m n

Goals accomplished! πŸ™
#align nat.psub'_eq_psub
Nat.psub'_eq_psub: βˆ€ (m n : β„•), psub' m n = psub m n
Nat.psub'_eq_psub
end Nat