From 0641f3f71441c72e23c28898539b7dad9a149a7a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 23 Sep 2016 17:36:32 -0700 Subject: [PATCH] chore(library/init): cleanup proofs using new elaborator --- library/init/default.lean | 3 +- library/init/logic.lean | 7 -- library/init/wf.lean | 214 +++++++++++++++----------------------- library/init/wf_k.lean | 17 --- tests/lean/run/gcd.lean | 11 +- 5 files changed, 86 insertions(+), 166 deletions(-) delete mode 100644 library/init/wf_k.lean diff --git a/library/init/default.lean b/library/init/default.lean index 1813b34d46..34ce6de7f6 100644 --- a/library/init/default.lean +++ b/library/init/default.lean @@ -12,5 +12,4 @@ import init.monad init.option init.state init.fin init.list init.char init.strin import init.monad_combinators init.set import init.timeit init.trace init.unsigned init.ordering init.list_classes init.coe import init.wf init.nat_div init.meta init.instances -import init.wf_k init.sigma_lex -import init.simplifier init.id_locked +import init.sigma_lex init.simplifier init.id_locked diff --git a/library/init/logic.lean b/library/init/logic.lean index baf74c1d4a..b5abf4a336 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -992,10 +992,3 @@ match h₁, h₂ with | (is_true h_c), h₂ := h_c | (is_false h_c), h₂ := false.elim h₂ end - --- namespace used to collect congruence rules for "contextual simplification" -namespace contextual - attribute if_ctx_simp_congr [congr] - attribute if_ctx_simp_congr_prop [congr] - attribute dif_ctx_simp_congr [congr] -end contextual diff --git a/library/init/wf.lean b/library/init/wf.lean index d4845d530a..5604e1fb87 100644 --- a/library/init/wf.lean +++ b/library/init/wf.lean @@ -8,69 +8,64 @@ import init.relation init.nat init.prod universe variables u v -inductive acc {A : Type u} (R : A → A → Prop) : A → Prop -| intro : ∀ x, (∀ y, R y x → acc y) → acc x +inductive acc {A : Type u} (r : A → A → Prop) : A → Prop +| intro : ∀ x, (∀ y, r y x → acc y) → acc x namespace acc - variables {A : Type u} {R : A → A → Prop} + variables {A : Type u} {r : A → A → Prop} - definition inv {x y : A} (H₁ : acc R x) (H₂ : R y x) : acc R y := - acc.rec_on H₁ (λ x₁ ac₁ iH H₂, ac₁ y H₂) H₂ + definition inv {x y : A} (h₁ : acc r x) (h₂ : r y x) : acc r y := + acc.rec_on h₁ (λ x₁ ac₁ ih h₂, ac₁ y h₂) h₂ -- dependent elimination for acc attribute [recursor] protected definition drec - {C : Π (a : A), acc R a → Type v} - (h₁ : Π (x : A) (acx : Π (y : A), R y x → acc R y), - (Π (y : A) (ryx : R y x), C y (acx y ryx)) → C x (acc.intro x acx)) - {a : A} (h₂ : acc R a) : C a h₂ := - @acc.rec _ _ (λ (a : A), Π (x : @acc A R a), C a x) - (λ x acx ih h₂, h₁ x acx (λ y ryx, ih y ryx (acx y ryx))) - _ - h₂ - h₂ + {C : Π (a : A), acc r a → Type v} + (h₁ : Π (x : A) (acx : Π (y : A), r y x → acc r y), (Π (y : A) (ryx : r y x), C y (acx y ryx)) → C x (acc.intro x acx)) + {a : A} (h₂ : acc r a) : C a h₂ := + acc.rec (λ x acx ih h₂, h₁ x acx (λ y ryx, ih y ryx (acx y ryx))) h₂ h₂ end acc -inductive well_founded {A : Type u} (R : A → A → Prop) : Prop -| intro : (∀ a, acc R a) → well_founded +inductive well_founded {A : Type u} (r : A → A → Prop) : Prop +| intro : (∀ a, acc r a) → well_founded namespace well_founded - definition apply {A : Type u} {R : A → A → Prop} (wf : well_founded R) : ∀ a, acc R a := + definition apply {A : Type u} {r : A → A → Prop} (wf : well_founded r) : ∀ a, acc r a := take a, well_founded.rec_on wf (λ p, p) a section - parameters {A : Type u} {R : A → A → Prop} - local infix `≺`:50 := R + parameters {A : Type u} {r : A → A → Prop} + local infix `≺`:50 := r - hypothesis Hwf : well_founded R + hypothesis hwf : well_founded r - theorem recursion {C : A → Type v} (a : A) (H : Π x, (Π y, y ≺ x → C y) → C x) : C a := - acc.rec_on (apply Hwf a) (λ x₁ ac₁ iH, H x₁ iH) + theorem recursion {C : A → Type v} (a : A) (h : Π x, (Π y, y ≺ x → C y) → C x) : C a := + acc.rec_on (apply hwf a) (λ x₁ ac₁ ih, h x₁ ih) - theorem induction {C : A → Prop} (a : A) (H : ∀ x, (∀ y, y ≺ x → C y) → C x) : C a := - recursion a H + theorem induction {C : A → Prop} (a : A) (h : ∀ x, (∀ y, y ≺ x → C y) → C x) : C a := + recursion a h variable {C : A → Type v} variable F : Π x, (Π y, y ≺ x → C y) → C x - definition fix_F (x : A) (a : acc R x) : C x := - acc.rec_on a (λ x₁ ac₁ iH, F x₁ iH) + definition fix_F (x : A) (a : acc r x) : C x := + acc.rec_on a (λ x₁ ac₁ ih, F x₁ ih) - theorem fix_F_eq (x : A) (r : acc R x) : + theorem fix_F_eq (x : A) (r : acc r x) : fix_F F x r = F x (λ (y : A) (p : y ≺ x), fix_F F y (acc.inv r p)) := acc.drec (λ x r ih, rfl) r end - variables {A : Type u} {C : A → Type v} {R : A → A → Prop} + variables {A : Type u} {C : A → Type v} {r : A → A → Prop} -- Well-founded fixpoint - definition fix (Hwf : well_founded R) (F : Π x, (Π y, R y x → C y) → C x) (x : A) : C x := - fix_F F x (apply Hwf x) + definition fix (hwf : well_founded r) (F : Π x, (Π y, r y x → C y) → C x) (x : A) : C x := + fix_F F x (apply hwf x) -- Well-founded fixpoint satisfies fixpoint equation - theorem fix_eq (Hwf : well_founded R) (F : Π x, (Π y, R y x → C y) → C x) (x : A) : - fix Hwf F x = F x (λ y h, fix Hwf F y) := - fix_F_eq F x (apply Hwf x) + theorem fix_eq (hwf : well_founded r) (F : Π x, (Π y, r y x → C y) → C x) (x : A) : + fix hwf F x = F x (λ y h, fix hwf F y) := + fix_F_eq F x (apply hwf x) end well_founded open well_founded @@ -83,95 +78,64 @@ well_founded.intro (λ (a : A), -- Subrelation of a well-founded relation is well-founded namespace subrelation section - parameters {A : Type u} {R Q : A → A → Prop} - parameters (H₁ : subrelation Q R) - parameters (H₂ : well_founded R) + parameters {A : Type u} {r Q : A → A → Prop} + parameters (h₁ : subrelation Q r) + parameters (h₂ : well_founded r) - definition accessible {a : A} (ac : acc R a) : acc Q a := + definition accessible {a : A} (ac : acc r a) : acc Q a := acc.rec_on ac (λ x ax ih, - acc.intro x (λ (y : A) (lt : Q y x), ih y (H₁ lt))) + acc.intro x (λ (y : A) (lt : Q y x), ih y (h₁ lt))) definition wf : well_founded Q := - well_founded.intro (λ a, accessible (apply H₂ a)) + ⟨λ a, accessible (apply h₂ a)⟩ end end subrelation -- The inverse image of a well-founded relation is well-founded namespace inv_image section - parameters {A : Type u} {B : Type v} {R : B → B → Prop} + parameters {A : Type u} {B : Type v} {r : B → B → Prop} parameters (f : A → B) - parameters (H : well_founded R) + parameters (h : well_founded r) - private definition acc_aux : ∀ {b : B}, @acc B R b → (∀ (x : A), @eq B (f x) b → @acc A (@inv_image A B R f) x) := - @acc.rec B R (λ (b : B), ∀ (x : A), f x = b → acc (inv_image R f) x) - (λ (x : B) - (acx : ∀ (y : B), R y x → acc R y) - (ih : ∀ (y : B), R y x → (λ (b : B), ∀ (x : A), f x = b → acc (inv_image R f) x) y) - (z : A) (e : f z = x), - acc.intro z - (λ (y : A) (lt : inv_image R f y z), - @eq.rec B (f z) - (λ (x : B), - (∀ (y : B), R y x → acc R y) → - (∀ (y : B), R y x → (λ (b : B), ∀ (x : A), f x = b → acc (inv_image R f) x) y) → acc (inv_image R f) y) - (λ (acx : ∀ (y : B), R y (f z) → @acc B R y) - (ih : ∀ (y : B), R y (f z) → (λ (b : B), ∀ (x : A), f x = b → acc (inv_image R f) x) y), - ih (f y) lt y (@rfl B (f y))) - x - e - acx - ih)) + private definition acc_aux {b : B} (ac : acc r b) : ∀ (x : A), f x = b → acc (inv_image r f) x := + acc.rec_on ac (λ x acx ih z e, + acc.intro z (λ y lt, eq.rec_on e (λ acx ih, ih (f y) lt y rfl) acx ih)) - definition accessible {a : A} (ac : acc R (f a)) : acc (inv_image R f) a := + definition accessible {a : A} (ac : acc r (f a)) : acc (inv_image r f) a := acc_aux ac a rfl - definition wf : well_founded (inv_image R f) := - well_founded.intro (λ a, accessible (apply H (f a))) + definition wf : well_founded (inv_image r f) := + ⟨λ a, accessible (apply h (f a))⟩ end end inv_image -- The transitive closure of a well-founded relation is well-founded namespace tc section - parameters {A : Type u} {R : A → A → Prop} - local notation `R⁺` := tc R + parameters {A : Type u} {r : A → A → Prop} + local notation `r⁺` := tc r - definition accessible : ∀ {z : A}, acc R z → acc (tc R) z := - @acc.rec A R (acc (tc R)) - (λ (x : A) (acx : ∀ (y : A), R y x → acc R y) (ih : ∀ (y : A), R y x → acc (tc R) y), - @acc.intro A (tc R) x - (λ (y : A) (rel : tc R y x), - @tc.rec A R - (λ (y x : A), - (∀ (y : A), R y x → acc R y) → - (∀ (y : A), R y x → acc (tc R) y) → acc (tc R) y) - (λ (a b : A) (rab : R a b) (acx : ∀ (y : A), R y b → acc R y) - (ih : ∀ (y : A), R y b → acc (tc R) y), - ih a rab) - (λ (a b c : A) (rab : tc R a b) (rbc : tc R b c) - (ih₁ : (∀ (y : A), R y b → acc R y) → (∀ (y : A), R y b → acc (tc R) y) → acc (tc R) a) - (ih₂ : (∀ (y : A), R y c → acc R y) → (∀ (y : A), R y c → acc (tc R) y) → acc (tc R) b) - (acx : ∀ (y : A), R y c → acc R y) (ih : ∀ (y : A), R y c → acc (tc R) y), - @acc.inv A (@tc A R) b a (ih₂ acx ih) rab) - y - x - rel - acx - ih)) + definition accessible {z : A} (ac : acc r z) : acc (tc r) z := + acc.rec_on ac (λ x acx ih, + acc.intro x (λ y rel, + tc.rec_on rel + (λ a b rab acx ih, ih a rab) + (λ a b c rab rbc ih₁ ih₂ acx ih, acc.inv (ih₂ acx ih) rab) + acx ih)) - definition wf (H : well_founded R) : well_founded R⁺ := - well_founded.intro (λ a, accessible (apply H a)) + definition wf (h : well_founded r) : well_founded r⁺ := + ⟨λ a, accessible (apply h a)⟩ end end tc -- less-than is well-founded definition nat.lt_wf : well_founded nat.lt := -well_founded.intro (nat.rec - (acc.intro 0 (λ n H, absurd H (nat.not_lt_zero n))) - (λ n IH, acc.intro (nat.succ n) (λ m H, - or.elim (nat.eq_or_lt_of_le (nat.le_of_succ_le_succ H)) - (λ e, eq.substr e IH) (acc.inv IH)))) +⟨nat.rec + (acc.intro 0 (λ n h, absurd h (nat.not_lt_zero n))) + (λ n ih, acc.intro (nat.succ n) (λ m h, + or.elim (nat.eq_or_lt_of_le (nat.le_of_succ_le_succ h)) + (λ e, eq.substr e ih) (acc.inv ih)))⟩ definition measure {A : Type u} : (A → ℕ) → A → A → Prop := inv_image lt @@ -184,56 +148,46 @@ namespace prod section variables {A : Type u} {B : Type v} - variable (Ra : A → A → Prop) - variable (Rb : B → B → Prop) + variable (ra : A → A → Prop) + variable (rb : B → B → Prop) - -- Lexicographical order based on Ra and Rb + -- Lexicographical order based on ra and rb inductive lex : A × B → A × B → Prop - | left : ∀ {a₁ b₁} a₂ b₂, Ra a₁ a₂ → lex (a₁, b₁) (a₂, b₂) - | right : ∀ a {b₁ b₂}, Rb b₁ b₂ → lex (a, b₁) (a, b₂) + | left : ∀ {a₁ b₁} a₂ b₂, ra a₁ a₂ → lex (a₁, b₁) (a₂, b₂) + | right : ∀ a {b₁ b₂}, rb b₁ b₂ → lex (a, b₁) (a, b₂) - -- Relational product based on Ra and Rb + -- relational product based on ra and rb inductive rprod : A × B → A × B → Prop - | intro : ∀ {a₁ b₁ a₂ b₂}, Ra a₁ a₂ → Rb b₁ b₂ → rprod (a₁, b₁) (a₂, b₂) + | intro : ∀ {a₁ b₁ a₂ b₂}, ra a₁ a₂ → rb b₁ b₂ → rprod (a₁, b₁) (a₂, b₂) end section parameters {A : Type u} {B : Type v} - parameters {Ra : A → A → Prop} {Rb : B → B → Prop} - local infix `≺`:50 := lex Ra Rb + parameters {ra : A → A → Prop} {rb : B → B → Prop} + local infix `≺`:50 := lex ra rb - definition lex_accessible {a} (aca : acc Ra a) (acb : ∀ b, acc Rb b): ∀ b, acc (lex Ra Rb) (a, b) := - acc.rec_on aca - (λ xa aca (iHa : ∀ y, Ra y xa → ∀ b, acc (lex Ra Rb) (y, b)), - λ b, acc.rec_on (acb b) - (λ xb acb - (iHb : ∀ y, Rb y xb → acc (lex Ra Rb) (xa, y)), - acc.intro (xa, xb) (λ p (lt : p ≺ (xa, xb)), - have aux : xa = xa → xb = xb → acc (lex Ra Rb) p, from - @prod.lex.rec_on A B Ra Rb (λ p₁ p₂, fst p₂ = xa → snd p₂ = xb → acc (lex Ra Rb) p₁) - p (xa, xb) lt - (λ a₁ b₁ a₂ b₂ (H : Ra a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ = xb), - show acc (lex Ra Rb) (a₁, b₁), from - have Ra₁ : Ra a₁ xa, from eq.rec_on eq₂ H, - iHa a₁ Ra₁ b₁) - (λ a b₁ b₂ (H : Rb b₁ b₂) (eq₂ : a = xa) (eq₃ : b₂ = xb), - show acc (lex Ra Rb) (a, b₁), from - have Rb₁ : Rb b₁ xb, from eq.rec_on eq₃ H, - have eq₂' : xa = a, from eq.rec_on eq₂ rfl, - eq.rec_on eq₂' (iHb b₁ Rb₁)), - aux rfl rfl))) + definition lex_accessible {a} (aca : acc ra a) (acb : ∀ b, acc rb b): ∀ b, acc (lex ra rb) (a, b) := + acc.rec_on aca (λ xa aca iha b, + acc.rec_on (acb b) (λ xb acb ihb, + acc.intro (xa, xb) (λ p lt, + have aux : xa = xa → xb = xb → acc (lex ra rb) p, from + @prod.lex.rec_on A B ra rb (λ p₁ p₂, fst p₂ = xa → snd p₂ = xb → acc (lex ra rb) p₁) + p (xa, xb) lt + (λ a₁ b₁ a₂ b₂ h (eq₂ : a₂ = xa) (eq₃ : b₂ = xb), iha a₁ (eq.rec_on eq₂ h) b₁) + (λ a b₁ b₂ h (eq₂ : a = xa) (eq₃ : b₂ = xb), eq.rec_on eq₂~>symm (ihb b₁ (eq.rec_on eq₃ h))), + aux rfl rfl))) -- The lexicographical order of well founded relations is well-founded - definition lex_wf (Ha : well_founded Ra) (Hb : well_founded Rb) : well_founded (lex Ra Rb) := - well_founded.intro (λ p, destruct p (λ a b, lex_accessible (apply Ha a) (well_founded.apply Hb) b)) + definition lex_wf (ha : well_founded ra) (hb : well_founded rb) : well_founded (lex ra rb) := + ⟨λ p, destruct p (λ a b, lex_accessible (apply ha a) (well_founded.apply hb) b)⟩ - -- Relational product is a subrelation of the lex - definition rprod_sub_lex : ∀ a b, rprod Ra Rb a b → lex Ra Rb a b := - λ a b H, prod.rprod.rec_on H (λ a₁ b₁ a₂ b₂ H₁ H₂, lex.left Rb a₂ b₂ H₁) + -- relational product is a subrelation of the lex + definition rprod_sub_lex : ∀ a b, rprod ra rb a b → lex ra rb a b := + λ a b h, prod.rprod.rec_on h (λ a₁ b₁ a₂ b₂ h₁ h₂, lex.left rb a₂ b₂ h₁) -- The relational product of well founded relations is well-founded - definition rprod_wf (Ha : well_founded Ra) (Hb : well_founded Rb) : well_founded (rprod Ra Rb) := - subrelation.wf (rprod_sub_lex) (lex_wf Ha Hb) + definition rprod_wf (ha : well_founded ra) (hb : well_founded rb) : well_founded (rprod ra rb) := + subrelation.wf (rprod_sub_lex) (lex_wf ha hb) end diff --git a/library/init/wf_k.lean b/library/init/wf_k.lean deleted file mode 100644 index 482e41fba2..0000000000 --- a/library/init/wf_k.lean +++ /dev/null @@ -1,17 +0,0 @@ --- Copyright (c) 2014 Microsoft Corporation. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Leonardo de Moura -prelude -import init.wf -universe variables u -namespace well_founded - -- This is an auxiliary definition that useful for generating a new "proof" for (well_founded R) - -- that allows us to use well_founded.fix and execute the definitions up to k nested recursive - -- calls without "computing" with the proofs in Hwf. - definition intro_k {A : Type u} {R : A → A → Prop} (Hwf : well_founded R) (k : nat) : well_founded R := - well_founded.intro - (nat.rec_on k - (λ n : A, well_founded.apply Hwf n) - (λ (k' : nat) (f : Π a, acc R a), (λ n : A, acc.intro n (λ y H, f y)))) - -end well_founded diff --git a/tests/lean/run/gcd.lean b/tests/lean/run/gcd.lean index 7def2397c8..27465da953 100644 --- a/tests/lean/run/gcd.lean +++ b/tests/lean/run/gcd.lean @@ -5,7 +5,7 @@ namespace playground -- Setup definition pair_nat.lt := lex nat.lt nat.lt definition pair_nat.lt.wf : well_founded pair_nat.lt := -intro_k (prod.lex_wf lt_wf lt_wf) 20 -- the '20' is for being able to execute the examples... it means 20 recursive call without proof computation +prod.lex_wf lt_wf lt_wf infixl `≺`:50 := pair_nat.lt -- Lemma for justifying recursive call @@ -38,13 +38,4 @@ well_founded.fix_eq pair_nat.lt.wf gcd.F (x+1, 0) theorem gcd_def_sx_sy (x y : nat) : gcd (x+1) (y+1) = if y ≤ x then gcd (x-y) (y+1) else gcd (x+1) (y-x) := well_founded.fix_eq pair_nat.lt.wf gcd.F (x+1, y+1) -example : gcd 4 6 = 2 := -rfl - -example : gcd 15 6 = 3 := -rfl - -example : gcd 0 2 = 2 := -rfl - end playground