From df84c4c2ca2ca2e3aa089bc7dbf1f35b46df81bb Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Thu, 31 Jul 2014 14:05:33 -0700 Subject: [PATCH] refactor(library/standard): clean up logic, reorder arguments to elim rules --- library/standard/congr.lean | 77 ++++++++++++++++----------------- library/standard/decidable.lean | 4 +- library/standard/logic.lean | 70 +++++++++++++++++++++++++----- 3 files changed, 97 insertions(+), 54 deletions(-) diff --git a/library/standard/congr.lean b/library/standard/congr.lean index 24b70f712..6ffdb9995 100644 --- a/library/standard/congr.lean +++ b/library/standard/congr.lean @@ -18,31 +18,30 @@ abbreviation reflexive {T : Type} (R : T → T → Type) : Prop := ∀x, R x x -- Congruence classes for unary and binary functions -- ------------------------------------------------- --- TODO: call this 'class', so outside it is congruence.class -inductive struc {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop) +inductive class {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop) (f : T1 → T2) : Prop := -| mk : (∀x y : T1, R1 x y → R2 (f x) (f y)) → struc R1 R2 f +| mk : (∀x y : T1, R1 x y → R2 (f x) (f y)) → class R1 R2 f abbreviation app {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop} - {f : T1 → T2} (C : struc R1 R2 f) ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) := -struc_rec id C x y + {f : T1 → T2} (C : class R1 R2 f) ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) := +class_rec id C x y -- to trigger class inference theorem infer {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop) - (f : T1 → T2) {C : struc R1 R2 f} ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) := -struc_rec id C x y + (f : T1 → T2) {C : class R1 R2 f} ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) := +class_rec id C x y -- for binary functions -inductive struc2 {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop) +inductive class2 {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop) {T3 : Type} (R3 : T3 → T3 → Prop) (f : T1 → T2 → T3) : Prop := | mk2 : (∀(x1 y1 : T1) (x2 y2 : T2), R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2)) → - struc2 R1 R2 R3 f + class2 R1 R2 R3 f abbreviation app2 {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop} {T3 : Type} {R3 : T3 → T3 → Prop} - {f : T1 → T2 → T3} (C : struc2 R1 R2 R3 f) ⦃x1 y1 : T1⦄ ⦃x2 y2 : T2⦄ + {f : T1 → T2 → T3} (C : class2 R1 R2 R3 f) ⦃x1 y1 : T1⦄ ⦃x2 y2 : T2⦄ : R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2) := -struc2_rec id C x1 y1 x2 y2 +class2_rec id C x1 y1 x2 y2 -- General tools to build instances @@ -51,52 +50,40 @@ struc2_rec id C x1 y1 x2 y2 theorem compose {T2 : Type} {R2 : T2 → T2 → Prop} {T3 : Type} {R3 : T3 → T3 → Prop} - {g : T2 → T3} (C2 : congr.struc R2 R3 g) + {g : T2 → T3} (C2 : congr.class R2 R3 g) {{T1 : Type}} {R1 : T1 → T1 → Prop} - {f : T1 → T2} (C1 : congr.struc R1 R2 f) : - congr.struc R1 R3 (λx, g (f x)) := mk (take x1 x2 H, app C2 (app C1 H)) + {f : T1 → T2} (C1 : congr.class R1 R2 f) : + congr.class R1 R3 (λx, g (f x)) := mk (take x1 x2 H, app C2 (app C1 H)) theorem compose21 {T2 : Type} {R2 : T2 → T2 → Prop} {T3 : Type} {R3 : T3 → T3 → Prop} {T4 : Type} {R4 : T4 → T4 → Prop} - {g : T2 → T3 → T4} (C3 : congr.struc2 R2 R3 R4 g) + {g : T2 → T3 → T4} (C3 : congr.class2 R2 R3 R4 g) ⦃T1 : Type⦄ {R1 : T1 → T1 → Prop} - {f1 : T1 → T2} (C1 : congr.struc R1 R2 f1) - {f2 : T1 → T3} (C2 : congr.struc R1 R3 f2) : - congr.struc R1 R4 (λx, g (f1 x) (f2 x)) := mk (take x1 x2 H, app2 C3 (app C1 H) (app C2 H)) + {f1 : T1 → T2} (C1 : congr.class R1 R2 f1) + {f2 : T1 → T3} (C2 : congr.class R1 R3 f2) : + congr.class R1 R4 (λx, g (f1 x) (f2 x)) := mk (take x1 x2 H, app2 C3 (app C1 H) (app C2 H)) -theorem trivial [instance] {T : Type} (R : T → T → Prop) : struc R R id := +theorem trivial [instance] {T : Type} (R : T → T → Prop) : class R R id := mk (take x y H, H) theorem const {T2 : Type} (R2 : T2 → T2 → Prop) (H : reflexive R2) : - ∀(T1 : Type) (R1 : T1 → T1 → Prop) (c : T2), struc R1 R2 (function.const T1 c) := + ∀(T1 : Type) (R1 : T1 → T1 → Prop) (c : T2), class R1 R2 (function.const T1 c) := take T1 R1 c, mk (take x y H1, H c) + -- instances for logic -- ------------------- --- TODO: swap order for and_elim? - -abbreviation imp (a b : Prop) : Prop := a → b - -theorem and_imp_and {a b c d : Prop} (H1 : a ∧ b) (H2 : a → c) (H3 : b → d) : c ∧ d := -and_elim (assume Ha : a, assume Hb : b, and_intro (H2 Ha) (H3 Hb)) H1 - -theorem imp_and_left {a b c : Prop} (H1 : a ∧ c) (H : a → b) : b ∧ c := -and_elim (assume Ha : a, assume Hc : c, and_intro (H Ha) Hc) H1 - -theorem imp_and_right {a b c : Prop} (H1 : c ∧ a) (H : a → b) : c ∧ b := -and_elim (assume Hc : c, assume Ha : a, and_intro Hc (H Ha)) H1 - -theorem congr_not : congr.struc iff iff not := +theorem congr_not : congr.class iff iff not := congr.mk (take a b, assume H : a ↔ b, iff_intro (assume H1 : ¬a, assume H2 : b, H1 (iff_elim_right H H2)) (assume H1 : ¬b, assume H2 : a, H1 (iff_elim_left H H2))) -theorem congr_and : congr.struc2 iff iff iff and := +theorem congr_and : congr.class2 iff iff iff and := congr.mk2 (take a1 b1 a2 b2, assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2, @@ -104,7 +91,7 @@ congr.mk2 (assume H3 : a1 ∧ a2, and_imp_and H3 (iff_elim_left H1) (iff_elim_left H2)) (assume H3 : b1 ∧ b2, and_imp_and H3 (iff_elim_right H1) (iff_elim_right H2))) -theorem congr_or : congr.struc2 iff iff iff or := +theorem congr_or : congr.class2 iff iff iff or := congr.mk2 (take a1 b1 a2 b2, assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2, @@ -112,7 +99,7 @@ congr.mk2 (assume H3 : a1 ∨ a2, or_imp_or H3 (iff_elim_left H1) (iff_elim_left H2)) (assume H3 : b1 ∨ b2, or_imp_or H3 (iff_elim_right H1) (iff_elim_right H2))) -theorem congr_imp : congr.struc2 iff iff iff imp := +theorem congr_imp : congr.class2 iff iff iff imp := congr.mk2 (take a1 b1 a2 b2, assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2, @@ -120,7 +107,7 @@ congr.mk2 (assume H3 : a1 → a2, assume Hb1 : b1, iff_elim_left H2 (H3 ((iff_elim_right H1) Hb1))) (assume H3 : b1 → b2, assume Ha1 : a1, iff_elim_right H2 (H3 ((iff_elim_left H1) Ha1)))) -theorem congr_iff : congr.struc2 iff iff iff iff := +theorem congr_iff : congr.class2 iff iff iff iff := congr.mk2 (take a1 b1 a2 b2, assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2, @@ -135,11 +122,21 @@ theorem congr_or_compose [instance] := congr.compose21 congr_or theorem congr_implies_compose [instance] := congr.compose21 congr_imp theorem congr_iff_compose [instance] := congr.compose21 congr_iff -theorem subst_iff {T : Type} {R : T → T → Prop} {P : T → Prop} {C : struc R iff P} - {a b : T} (H : R a b) (H1 : P a) : P b := iff_mp_left (app C H) H1 +theorem subst_iff {T : Type} {R : T → T → Prop} {P : T → Prop} {C : class R iff P} + {a b : T} (H : R a b) (H1 : P a) : P b := iff_elim_left (app C H) H1 theorem test1 (a b c d e : Prop) (H1 : a ↔ b) : (a ∨ c → ¬(d → a)) ↔ (b ∨ c → ¬(d → b)) := congr.infer iff iff _ H1 theorem test2 (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) := subst_iff H1 H2 + +-- TODO: move these to new file + +theorem or_right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b := +calc + (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) : or_assoc _ _ _ + ... ↔ a ∨ (c ∨ b) : congr.infer iff iff _ (or_comm b c) + ... ↔ (a ∨ c) ∨ b : iff_symm (or_assoc _ _ _) + +-- TODO: add or_left_comm, and_right_comm, and_left_comm diff --git a/library/standard/decidable.lean b/library/standard/decidable.lean index d5d89880c..68f244cbb 100644 --- a/library/standard/decidable.lean +++ b/library/standard/decidable.lean @@ -58,9 +58,9 @@ theorem decidable_iff [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable rec_on Ha (assume Ha, rec_on Hb (assume Hb : b, inl (iff_intro (assume H, Hb) (assume H, Ha))) - (assume Hnb : ¬b, inr (assume H : a ↔ b, absurd (iff_mp_left H Ha) Hnb))) + (assume Hnb : ¬b, inr (assume H : a ↔ b, absurd (iff_elim_left H Ha) Hnb))) (assume Hna, rec_on Hb - (assume Hb : b, inr (assume H : a ↔ b, absurd (iff_mp_right H Hb) Hna)) + (assume Hb : b, inr (assume H : a ↔ b, absurd (iff_elim_right H Hb) Hna)) (assume Hnb : ¬b, inl (iff_intro (assume Ha, absurd_elim b Ha Hna) (assume Hb, absurd_elim a Hb Hnb)))) theorem decidable_implies [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a → b) := diff --git a/library/standard/logic.lean b/library/standard/logic.lean index e7395847e..660a8bd0c 100644 --- a/library/standard/logic.lean +++ b/library/standard/logic.lean @@ -1,8 +1,15 @@ -- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. -- Authors: Leonardo de Moura, Jeremy Avigad + definition Prop [inline] := Type.{0} +abbreviation imp (a b : Prop) : Prop := a → b + + +-- true and false +-- -------------- + inductive false : Prop theorem false_elim (c : Prop) (H : false) : c := @@ -17,6 +24,10 @@ prefix `¬`:40 := not notation `assume` binders `,` r:(scoped f, f) := r notation `take` binders `,` r:(scoped f, f) := r + +-- not +-- --- + theorem not_intro {a : Prop} (H : a → false) : ¬a := H theorem not_elim {a : Prop} (H1 : ¬a) (H2 : a) : false := H1 H2 @@ -47,14 +58,18 @@ assume Hna : ¬a, absurd (assume Ha : a, absurd_elim b Ha Hna) H theorem not_implies_right {a b : Prop} (H : ¬(a → b)) : ¬b := assume Hb : b, absurd (assume Ha : a, Hb) H + +-- and +-- --- + inductive and (a b : Prop) : Prop := | and_intro : a → b → and a b infixr `/\`:35 := and infixr `∧`:35 := and -theorem and_elim {a b c : Prop} (H1 : a → b → c) (H2 : a ∧ b) : c := -and_rec H1 H2 +theorem and_elim {a b c : Prop} (H1 : a ∧ b) (H2 : a → b → c) : c := +and_rec H2 H1 theorem and_elim_left {a b : Prop} (H : a ∧ b) : a := and_rec (λa b, a) H @@ -71,6 +86,19 @@ assume H : a ∧ b, absurd (and_elim_left H) Hna theorem and_not_right (a : Prop) {b : Prop} (Hnb : ¬b) : ¬(a ∧ b) := assume H : a ∧ b, absurd (and_elim_right H) Hnb +theorem and_imp_and {a b c d : Prop} (H1 : a ∧ b) (H2 : a → c) (H3 : b → d) : c ∧ d := +and_elim H1 (assume Ha : a, assume Hb : b, and_intro (H2 Ha) (H3 Hb)) + +theorem imp_and_left {a b c : Prop} (H1 : a ∧ c) (H : a → b) : b ∧ c := +and_elim H1 (assume Ha : a, assume Hc : c, and_intro (H Ha) Hc) + +theorem imp_and_right {a b c : Prop} (H1 : c ∧ a) (H : a → b) : c ∧ b := +and_elim H1 (assume Hc : c, assume Ha : a, and_intro Hc (H Ha)) + + +-- or +-- -- + inductive or (a b : Prop) : Prop := | or_intro_left : a → or a b | or_intro_right : b → or a b @@ -113,6 +141,10 @@ or_elim H1 (assume H2 : c, or_inl H2) (assume H2 : a, or_inr (H H2)) + +-- eq +-- -- + inductive eq {A : Type} (a : A) : A → Prop := | refl : eq a a @@ -181,6 +213,10 @@ assume Ha, H2 ◂ (H1 Ha) theorem eq_imp_trans {a b c : Prop} (H1 : a = b) (H2 : b → c) : a → c := assume Ha, H2 (H1 ◂ Ha) + +-- ne +-- -- + definition ne [inline] {A : Type} (a b : A) := ¬(a = b) infix `≠`:50 := ne @@ -202,6 +238,10 @@ theorem ne_eq_trans {A : Type} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c calc_trans eq_ne_trans calc_trans ne_eq_trans + +-- iff +-- --- + definition iff (a b : Prop) := (a → b) ∧ (b → a) infix `<->`:25 := iff infix `↔`:25 := iff @@ -216,12 +256,6 @@ iff_elim (assume H1 H2, H1) H theorem iff_elim_right {a b : Prop} (H : a ↔ b) : b → a := iff_elim (assume H1 H2, H2) H -theorem iff_mp_left {a b : Prop} (H1 : a ↔ b) (H2 : a) : b := -(iff_elim_left H1) H2 - -theorem iff_mp_right {a b : Prop} (H1 : a ↔ b) (H2 : b) : a := -(iff_elim_right H1) H2 - theorem iff_flip_sign {a b : Prop} (H1 : a ↔ b) : ¬a ↔ ¬b := iff_intro (assume Hna, mt (iff_elim_right H1) Hna) @@ -232,19 +266,23 @@ iff_intro (assume H, H) (assume H, H) theorem iff_trans {a b c : Prop} (H1 : a ↔ b) (H2 : b ↔ c) : a ↔ c := iff_intro - (assume Ha, iff_mp_left H2 (iff_mp_left H1 Ha)) - (assume Hc, iff_mp_right H1 (iff_mp_right H2 Hc)) + (assume Ha, iff_elim_left H2 (iff_elim_left H1 Ha)) + (assume Hc, iff_elim_right H1 (iff_elim_right H2 Hc)) theorem iff_symm {a b : Prop} (H : a ↔ b) : b ↔ a := iff_intro - (assume Hb, iff_mp_right H Hb) - (assume Ha, iff_mp_left H Ha) + (assume Hb, iff_elim_right H Hb) + (assume Ha, iff_elim_left H Ha) calc_trans iff_trans theorem eq_to_iff {a b : Prop} (H : a = b) : a ↔ b := iff_intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb) + +-- comm and assoc for and / or +-- --------------------------- + theorem and_comm (a b : Prop) : a ∧ b ↔ b ∧ a := iff_intro (λH, and_swap H) (λH, and_swap H) @@ -273,6 +311,10 @@ iff_intro (assume Hb, or_inl (or_inr Hb)) (assume Hc, or_inr Hc))) + +-- exists +-- ------ + inductive Exists {A : Type} (P : A → Prop) : Prop := | exists_intro : ∀ (a : A), P a → Exists P @@ -305,6 +347,10 @@ theorem exists_unique_elim {A : Type} {p : A → Prop} {b : Prop} obtain w Hw, from H2, H1 w (and_elim_left Hw) (and_elim_right Hw) + +-- inhabited +-- --------- + inductive inhabited (A : Type) : Prop := | inhabited_intro : A → inhabited A