michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/data/nat/order): add 'max/min' auxiliary theorems

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-19 20:14:49 -07:00
parent d91627ebec
commit d2f64d7744
1 changed files with 14 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
library/data/nat/order.lean
View file

@ -483,6 +483,20 @@ by rewrite [max_eq_left !zero_le]
theorem zero_max [rewrite] (a : ℕ) : max 0 a = a := theorem zero_max [rewrite] (a : ℕ) : max 0 a = a :=
by rewrite [max_eq_right !zero_le] by rewrite [max_eq_right !zero_le]
theorem min_succ_succ [rewrite] (a b : ℕ) : min (succ a) (succ b) = succ (min a b) :=
by_cases
(suppose a < b, by unfold min; rewrite [if_pos this, if_pos (succ_lt_succ this)])
(suppose ¬ a < b,
assert h : ¬ succ a < succ b, from assume h, absurd (lt_of_succ_lt_succ h) this,
by unfold min; rewrite [if_neg this, if_neg h])
theorem max_succ_succ [rewrite] (a b : ℕ) : max (succ a) (succ b) = succ (max a b) :=
by_cases
(suppose a < b, by unfold max; rewrite [if_pos this, if_pos (succ_lt_succ this)])
(suppose ¬ a < b,
assert h : ¬ succ a < succ b, from assume h, absurd (lt_of_succ_lt_succ h) this,
by unfold max; rewrite [if_neg this, if_neg h])
theorem lt_min {a b c : ℕ} (H₁ : a < b) (H₂ : a < c) : a < min b c := theorem lt_min {a b c : ℕ} (H₁ : a < b) (H₂ : a < c) : a < min b c :=
decidable.by_cases decidable.by_cases
(assume H : b ≤ c, by rewrite (min_eq_left H); apply H₁) (assume H : b ≤ c, by rewrite (min_eq_left H); apply H₁)