From e3f364e1ee07a38d49803d719fa544bc11ed4d7c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 13 Jul 2014 02:48:40 +0100 Subject: [PATCH] feat(library/standard): add well-founded induction theorem Signed-off-by: Leonardo de Moura --- library/standard/wf.lean | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 library/standard/wf.lean diff --git a/library/standard/wf.lean b/library/standard/wf.lean new file mode 100644 index 000000000..02051eaab --- /dev/null +++ b/library/standard/wf.lean @@ -0,0 +1,30 @@ +-- 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 logic classical + +-- Well-founded relation definition +-- We are essentially saying that a relation R is well-founded +-- if every non-empty "set" P, has a R-minimal element +definition wf {A : Type} (R : A → A → Bool) : Bool +:= ∀ P, (∃ w, P w) → ∃ min, P min ∧ ∀ b, R b min → ¬ P b + +-- Well-founded induction theorem +theorem wf_induction {A : Type} {R : A → A → Bool} {P : A → Bool} (Hwf : wf R) (iH : ∀ x, (∀ y, R y x → P y) → P x) + : ∀ x, P x +:= by_contradiction (assume N : ¬ ∀ x, P x, + obtain (w : A) (Hw : ¬ P w), from not_forall_exists N, + -- The main "trick" is to define Q x as ¬ P x. + -- Since R is well-founded, there must be a R-minimal element r s.t. Q r (which is ¬ P r) + let Q [inline] := λ x, ¬ P x in + have Qw : ∃ w, Q w, from exists_intro w Hw, + have Qwf : ∃ min, Q min ∧ ∀ b, R b min → ¬ Q b, from Hwf Q Qw, + obtain (r : A) (Hr : Q r ∧ ∀ b, R b r → ¬ Q b), from Qwf, + -- Using the inductive hypothesis iH and Hr, we show P r, and derive the contradiction. + have s1 : ∀ b, R b r → P b, from + take b : A, assume H : R b r, + -- We are using Hr to derive ¬ ¬ P b + not_not_elim (and_elim_right Hr b H), + have s2 : P r, from iH r s1, + have s3 : ¬ P r, from and_elim_left Hr, + show false, from absurd s2 s3)