feat(library/data/nat/wf): add nat.lt is well founded theorem

This commit is contained in:
Leonardo de Moura 2014-11-07 10:46:44 -08:00
parent c28227d7a1
commit 64d2cc60c2
2 changed files with 18 additions and 1 deletions

View file

@ -2,4 +2,4 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jeremy Avigad
import .basic .order .sub .div
import .basic .order .sub .div .wf

17
library/data/nat/wf.lean Normal file
View file

@ -0,0 +1,17 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import data.nat.order logic.wf
open nat eq.ops
theorem lt.wf [instance] : well_founded lt :=
well_founded.intro
(take n, nat.induction_on n
(acc.intro zero (λ (y : nat) (H : y < 0),
absurd H !not_lt_zero))
(λ (n : nat) (iH : acc lt n),
acc.intro (succ n) (λ (m : nat) (H : m < succ n),
have H₁ : m < n m = n, from le_imp_lt_or_eq (succ_le_cancel (lt_imp_le_succ H)),
or.elim H₁
(assume Hlt : m < n, acc.inv iH Hlt)
(assume Heq : m = n, Heq⁻¹ ▸ iH))))