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

feat(library/data/nat/decl): add 'measure'

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-22 17:19:03 -08:00
parent d07481f60f
commit 2af5ce364d
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/data/nat/decl.lean
View file

@ -69,6 +69,12 @@ namespace nat
acc.inv (eq.rec_on e ih) hlt)), acc.inv (eq.rec_on e ih) hlt)),
aux hlt rfl))) aux hlt rfl)))
definition measure {A : Type} (f : A → nat) : A → A → Prop :=
inv_image lt f
definition measure.wf {A : Type} (f : A → nat) : well_founded (measure f) :=
inv_image.wf f lt.wf
definition not_lt_zero (a : nat) : ¬ a < zero := definition not_lt_zero (a : nat) : ¬ a < zero :=
have aux : ∀ {b}, a < b → b = zero → false, from have aux : ∀ {b}, a < b → b = zero → false, from
λ b H, lt.cases_on H λ b H, lt.cases_on H