From 5a98a2538c0fc1400a8b38b9de21ab4725ce5691 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 20 Nov 2015 16:38:10 -0800 Subject: [PATCH] refactor(library): move basic simp/congr rules to init folder, delete some legacy files --- library/algebra/category/constructions.lean | 2 +- library/data/data.md | 1 - library/data/default.lean | 2 +- library/data/finset/bigops.lean | 2 +- library/data/int/basic.lean | 2 +- library/data/nat/bquant.lean | 4 +- library/data/quotient/basic.lean | 319 -------------------- library/data/quotient/classical.lean | 58 ---- library/data/quotient/default.lean | 5 - library/data/quotient/quotient.md | 10 - library/data/quotient/util.lean | 100 ------ library/init/function.lean | 3 - library/init/logic.lean | 184 ++++++++++- library/logic/connectives.lean | 147 +-------- library/logic/default.lean | 2 +- library/logic/examples/instances_test.lean | 36 --- library/logic/examples/negative.lean | 4 +- library/logic/identities.lean | 20 +- library/logic/instances.lean | 77 ----- library/logic/quantifiers.lean | 58 ---- 20 files changed, 191 insertions(+), 845 deletions(-) delete mode 100644 library/data/quotient/basic.lean delete mode 100644 library/data/quotient/classical.lean delete mode 100644 library/data/quotient/default.lean delete mode 100644 library/data/quotient/quotient.md delete mode 100644 library/data/quotient/util.lean delete mode 100644 library/logic/examples/instances_test.lean delete mode 100644 library/logic/instances.lean diff --git a/library/algebra/category/constructions.lean b/library/algebra/category/constructions.lean index 173dd3a3ff..cdc51c09b6 100644 --- a/library/algebra/category/constructions.lean +++ b/library/algebra/category/constructions.lean @@ -48,7 +48,7 @@ namespace category definition type_category [reducible] : category Type := mk (λa b, a → b) (λ a b c, function.compose) - (λ a, function.id) + (λ a, _root_.id) (λ a b c d h g f, symm (function.compose.assoc h g f)) (λ a b f, function.compose.left_id f) (λ a b f, function.compose.right_id f) diff --git a/library/data/data.md b/library/data/data.md index b2e5196f88..215517b45a 100644 --- a/library/data/data.md +++ b/library/data/data.md @@ -26,7 +26,6 @@ Constructors: * [uprod](uprod.lean) : unordered pairs * [option](option.lean) * [subtype](subtype.lean) -* [quotient](quotient/quotient.md) * [squash](squash.lean) : propositional truncation * [list](list/list.md) * [finset](finset/finset.md) : finite sets diff --git a/library/data/default.lean b/library/data/default.lean index 07c9cbb775..74699fae3a 100644 --- a/library/data/default.lean +++ b/library/data/default.lean @@ -4,5 +4,5 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Jeremy Avigad -/ import .empty .unit .bool .num .string .nat .int .rat .fintype -import .prod .sum .sigma .option .quotient .list .finset .set .stream +import .prod .sum .sigma .option .list .finset .set .stream import .fin .real .complex diff --git a/library/data/finset/bigops.lean b/library/data/finset/bigops.lean index f9b83e674f..14845f8308 100644 --- a/library/data/finset/bigops.lean +++ b/library/data/finset/bigops.lean @@ -113,7 +113,7 @@ section deceqA (assume H : a ∉ s, !Union_insert_of_not_mem H) lemma image_eq_Union_index_image (s : finset A) (f : A → finset B) : - Union s f = Union (image f s) function.id := + Union s f = Union (image f s) id := finset.induction_on s (by rewrite Union_empty) (take s1 a Pa IH, by rewrite [image_insert, *Union_insert, IH]) diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 1ac2bcf84f..af13ee87e7 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -149,7 +149,7 @@ have H1 : n - m = succ (pred (n - m)), from eq.symm (succ_pred_of_pos (nat.sub_p show sub_nat_nat m n = nat.cases_on (succ (nat.pred (n - m))) (m -[nat] n) _, from H1 ▸ rfl end -definition nat_abs (a : ℤ) : ℕ := int.cases_on a function.id succ +definition nat_abs (a : ℤ) : ℕ := int.cases_on a id succ theorem nat_abs_of_nat (n : ℕ) : nat_abs n = n := rfl diff --git a/library/data/nat/bquant.lean b/library/data/nat/bquant.lean index 470b60b4fb..e16dd5f7cf 100644 --- a/library/data/nat/bquant.lean +++ b/library/data/nat/bquant.lean @@ -104,13 +104,13 @@ section : decidable (∃ x, x ≤ n ∧ P x) := decidable_of_decidable_of_iff (decidable_bex (succ n) P) - (exists_congr (λn, and_iff_and !lt_succ_iff_le !iff.refl)) + (exists_congr (λn, and_congr !lt_succ_iff_le !iff.refl)) definition decidable_ball_le [instance] (n : nat) (P : nat → Prop) [H : decidable_pred P] : decidable (∀ x, x ≤ n → P x) := decidable_of_decidable_of_iff (decidable_ball (succ n) P) - (forall_congr (λn, imp_iff_imp !lt_succ_iff_le !iff.refl)) + (forall_congr (λ n, imp_congr !lt_succ_iff_le !iff.refl)) end namespace nat diff --git a/library/data/quotient/basic.lean b/library/data/quotient/basic.lean deleted file mode 100644 index 8acb3bace3..0000000000 --- a/library/data/quotient/basic.lean +++ /dev/null @@ -1,319 +0,0 @@ -/- -Copyright (c) 2014 Floris van Doorn. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Floris van Doorn - -An explicit treatment of quotients, without using Lean's built-in quotient types. --/ -import logic logic.cast algebra.relation data.prod -import logic.instances -import .util - -open relation prod inhabited nonempty tactic eq.ops -open subtype relation.iff_ops - -namespace quotient - -/- definition and basics -/ - --- TODO: make this a structure -definition is_quotient {A B : Type} (R : A → A → Prop) (abs : A → B) (rep : B → A) : Prop := - (∀b, abs (rep b) = b) ∧ - (∀b, R (rep b) (rep b)) ∧ - (∀r s, R r s ↔ (R r r ∧ R s s ∧ abs r = abs s)) - -theorem intro {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (H1 : ∀b, abs (rep b) = b) (H2 : ∀b, R (rep b) (rep b)) - (H3 : ∀r s, R r s ↔ (R r r ∧ R s s ∧ abs r = abs s)) : is_quotient R abs rep := -and.intro H1 (and.intro H2 H3) - -theorem and_absorb_left {a : Prop} (b : Prop) (Ha : a) : a ∧ b ↔ b := -iff.intro (assume Hab, and.elim_right Hab) (assume Hb, and.intro Ha Hb) - -theorem intro_refl {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (H1 : reflexive R) (H2 : ∀b, abs (rep b) = b) - (H3 : ∀r s, R r s ↔ abs r = abs s) : is_quotient R abs rep := -intro - H2 - (take b, H1 (rep b)) - (take r s, - have H4 : R r s ↔ R s s ∧ abs r = abs s, - from - subst (symm (and_absorb_left _ (H1 s))) (H3 r s), - subst (symm (and_absorb_left _ (H1 r))) H4) - -theorem abs_rep {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (Q : is_quotient R abs rep) (b : B) : abs (rep b) = b := -and.elim_left Q b - -theorem refl_rep {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (Q : is_quotient R abs rep) (b : B) : R (rep b) (rep b) := -and.elim_left (and.elim_right Q) b - -theorem R_iff {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (Q : is_quotient R abs rep) (r s : A) : R r s ↔ (R r r ∧ R s s ∧ abs r = abs s) := -and.elim_right (and.elim_right Q) r s - -theorem refl_left {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (Q : is_quotient R abs rep) {r s : A} (H : R r s) : R r r := -and.elim_left (iff.elim_left (R_iff Q r s) H) - -theorem refl_right {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (Q : is_quotient R abs rep) {r s : A} (H : R r s) : R s s := -and.elim_left (and.elim_right (iff.elim_left (R_iff Q r s) H)) - -theorem eq_abs {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (Q : is_quotient R abs rep) {r s : A} (H : R r s) : abs r = abs s := -and.elim_right (and.elim_right (iff.elim_left (R_iff Q r s) H)) - -theorem R_intro {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (Q : is_quotient R abs rep) {r s : A} (H1 : R r r) (H2 : R s s) (H3 : abs r = abs s) : R r s := -iff.elim_right (R_iff Q r s) (and.intro H1 (and.intro H2 H3)) - -theorem R_intro_refl {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (Q : is_quotient R abs rep) (H1 : reflexive R) {r s : A} (H2 : abs r = abs s) : R r s := -iff.elim_right (R_iff Q r s) (and.intro (H1 r) (and.intro (H1 s) H2)) - -theorem rep_eq {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (Q : is_quotient R abs rep) {a b : B} (H : R (rep a) (rep b)) : a = b := -calc - a = abs (rep a) : eq.symm (abs_rep Q a) - ... = abs (rep b) : {eq_abs Q H} - ... = b : abs_rep Q b - -theorem R_rep_abs {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (Q : is_quotient R abs rep) {a : A} (H : R a a) : R a (rep (abs a)) := -have H3 : abs a = abs (rep (abs a)), from eq.symm (abs_rep Q (abs a)), -R_intro Q H (refl_rep Q (abs a)) H3 - -theorem quotient_imp_symm {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (Q : is_quotient R abs rep) : symmetric R := -take a b : A, -assume H : R a b, -have Ha : R a a, from refl_left Q H, -have Hb : R b b, from refl_right Q H, -have Hab : abs b = abs a, from eq.symm (eq_abs Q H), -R_intro Q Hb Ha Hab - -theorem quotient_imp_trans {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (Q : is_quotient R abs rep) : transitive R := -take a b c : A, -assume Hab : R a b, -assume Hbc : R b c, -have Ha : R a a, from refl_left Q Hab, -have Hc : R c c, from refl_right Q Hbc, -have Hac : abs a = abs c, from eq.trans (eq_abs Q Hab) (eq_abs Q Hbc), -R_intro Q Ha Hc Hac - -/- recursion -/ - --- (maybe some are superfluous) - -definition rec {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (Q : is_quotient R abs rep) {C : B → Type} (f : forall (a : A), C (abs a)) (b : B) : C b := -eq.rec_on (abs_rep Q b) (f (rep b)) - -theorem comp {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (Q : is_quotient R abs rep) {C : B → Type} {f : forall (a : A), C (abs a)} - (H : forall (r s : A) (H' : R r s), eq.rec_on (eq_abs Q H') (f r) = f s) - {a : A} (Ha : R a a) : rec Q f (abs a) = f a := -assert H2 : R a (rep (abs a)), from - R_rep_abs Q Ha, -assert Heq : abs (rep (abs a)) = abs a, from - abs_rep Q (abs a), -calc - rec Q f (abs a) = eq.rec_on Heq (f (rep (abs a))) : rfl - ... = eq.rec_on Heq (eq.rec_on (Heq⁻¹) (f a)) : {(H _ _ H2)⁻¹} - ... = f a : eq.rec_on_compose (eq_abs Q H2) _ _ - -definition rec_constant {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (Q : is_quotient R abs rep) {C : Type} (f : A → C) (b : B) : C := -f (rep b) - -theorem comp_constant {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (Q : is_quotient R abs rep) {C : Type} {f : A → C} - (H : forall (r s : A) (H' : R r s), f r = f s) - {a : A} (Ha : R a a) : rec_constant Q f (abs a) = f a := -have H2 : R a (rep (abs a)), from R_rep_abs Q Ha, -calc - rec_constant Q f (abs a) = f (rep (abs a)) : rfl - ... = f a : {(H _ _ H2)⁻¹} - -definition rec_binary {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (Q : is_quotient R abs rep) {C : Type} (f : A → A → C) (b c : B) : C := -f (rep b) (rep c) - -theorem comp_binary {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (Q : is_quotient R abs rep) {C : Type} {f : A → A → C} - (H : forall (a a' b b' : A) (Ha : R a a') (Hb : R b b'), f a b = f a' b') - {a b : A} (Ha : R a a) (Hb : R b b) : rec_binary Q f (abs a) (abs b) = f a b := -have H2 : R a (rep (abs a)), from R_rep_abs Q Ha, -have H3 : R b (rep (abs b)), from R_rep_abs Q Hb, -calc - rec_binary Q f (abs a) (abs b) = f (rep (abs a)) (rep (abs b)) : rfl - ... = f a b : {(H _ _ _ _ H2 H3)⁻¹} - -theorem comp_binary_refl {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (Q : is_quotient R abs rep) (Hrefl : reflexive R) {C : Type} {f : A → A → C} - (H : forall (a a' b b' : A) (Ha : R a a') (Hb : R b b'), f a b = f a' b') - (a b : A) : rec_binary Q f (abs a) (abs b) = f a b := -comp_binary Q H (Hrefl a) (Hrefl b) - -definition quotient_map {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (Q : is_quotient R abs rep) (f : A → A) (b : B) : B := -abs (f (rep b)) - -theorem comp_quotient_map {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (Q : is_quotient R abs rep) {f : A → A} - (H : forall (a a' : A) (Ha : R a a'), R (f a) (f a')) - {a : A} (Ha : R a a) : quotient_map Q f (abs a) = abs (f a) := -have H2 : R a (rep (abs a)), from R_rep_abs Q Ha, -have H3 : R (f a) (f (rep (abs a))), from H _ _ H2, -have H4 : abs (f a) = abs (f (rep (abs a))), from eq_abs Q H3, -H4⁻¹ - -definition quotient_map_binary {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (Q : is_quotient R abs rep) (f : A → A → A) (b c : B) : B := -abs (f (rep b) (rep c)) - -theorem comp_quotient_map_binary {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} - (Q : is_quotient R abs rep) {f : A → A → A} - (H : forall (a a' b b' : A) (Ha : R a a') (Hb : R b b'), R (f a b) (f a' b')) - {a b : A} (Ha : R a a) (Hb : R b b) : quotient_map_binary Q f (abs a) (abs b) = abs (f a b) := -have Ha2 : R a (rep (abs a)), from R_rep_abs Q Ha, -have Hb2 : R b (rep (abs b)), from R_rep_abs Q Hb, -have H2 : R (f a b) (f (rep (abs a)) (rep (abs b))), from H _ _ _ _ Ha2 Hb2, -(eq_abs Q H2)⁻¹ - -theorem comp_quotient_map_binary_refl {A B : Type} {R : A → A → Prop} (Hrefl : reflexive R) - {abs : A → B} {rep : B → A} (Q : is_quotient R abs rep) {f : A → A → A} - (H : forall (a a' b b' : A) (Ha : R a a') (Hb : R b b'), R (f a b) (f a' b')) - (a b : A) : quotient_map_binary Q f (abs a) (abs b) = abs (f a b) := -comp_quotient_map_binary Q H (Hrefl a) (Hrefl b) - -/- image -/ - -definition image {A B : Type} (f : A → B) := subtype (fun b, ∃a, f a = b) - -theorem image_inhabited {A B : Type} (f : A → B) (H : inhabited A) : inhabited (image f) := -inhabited.mk (tag (f (default A)) (exists.intro (default A) rfl)) - -theorem image_inhabited2 {A B : Type} (f : A → B) (a : A) : inhabited (image f) := -image_inhabited f (inhabited.mk a) - -definition fun_image {A B : Type} (f : A → B) (a : A) : image f := -tag (f a) (exists.intro a rfl) - -theorem fun_image_def {A B : Type} (f : A → B) (a : A) : - fun_image f a = tag (f a) (exists.intro a rfl) := rfl - -theorem elt_of_fun_image {A B : Type} (f : A → B) (a : A) : elt_of (fun_image f a) = f a := -by esimp - -theorem image_elt_of {A B : Type} {f : A → B} (u : image f) : ∃a, f a = elt_of u := -has_property u - -theorem fun_image_surj {A B : Type} {f : A → B} (u : image f) : ∃a, fun_image f a = u := -subtype.destruct u - (take (b : B) (H : ∃a, f a = b), - obtain a (H': f a = b), from H, - (exists.intro a (tag_eq H'))) - -theorem image_tag {A B : Type} {f : A → B} (u : image f) : ∃a H, tag (f a) H = u := -obtain a (H : fun_image f a = u), from fun_image_surj u, -exists.intro a (exists.intro (exists.intro a rfl) H) - -open eq.ops - -theorem fun_image_eq {A B : Type} (f : A → B) (a a' : A) - : (f a = f a') ↔ (fun_image f a = fun_image f a') := -iff.intro - (assume H : f a = f a', tag_eq H) - (assume H : fun_image f a = fun_image f a', - by injection H; assumption) - -theorem idempotent_image_elt_of {A : Type} {f : A → A} (H : ∀a, f (f a) = f a) (u : image f) - : fun_image f (elt_of u) = u := -obtain (a : A) (Ha : fun_image f a = u), from fun_image_surj u, -calc - fun_image f (elt_of u) = fun_image f (elt_of (fun_image f a)) : by rewrite Ha - ... = fun_image f (f a) : {elt_of_fun_image f a} - ... = fun_image f a : {iff.elim_left (fun_image_eq f (f a) a) (H a)} - ... = u : Ha - -theorem idempotent_image_fix {A : Type} {f : A → A} (H : ∀a, f (f a) = f a) (u : image f) - : f (elt_of u) = elt_of u := -obtain (a : A) (Ha : f a = elt_of u), from image_elt_of u, -calc - f (elt_of u) = f (f a) : {Ha⁻¹} - ... = f a : H a - ... = elt_of u : Ha - -/- construct quotient from representative map -/ - -theorem representative_map_idempotent {A : Type} {R : A → A → Prop} {f : A → A} - (H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b ↔ R a a ∧ R b b ∧ f a = f b) (a : A) : - f (f a) = f a := -(and.elim_right (and.elim_right (iff.elim_left (H2 a (f a)) (H1 a))))⁻¹ - -theorem representative_map_idempotent_equiv {A : Type} {R : A → A → Prop} {f : A → A} - (H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b → f a = f b) (a : A) : - f (f a) = f a := -(H2 a (f a) (H1 a))⁻¹ - -theorem representative_map_refl_rep {A : Type} {R : A → A → Prop} {f : A → A} - (H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b ↔ R a a ∧ R b b ∧ f a = f b) (a : A) : - R (f a) (f a) := -representative_map_idempotent H1 H2 a ▸ H1 (f a) - -theorem representative_map_image_fix {A : Type} {R : A → A → Prop} {f : A → A} - (H1 : ∀a, R a (f a)) (H2 : ∀a a', R a a' ↔ R a a ∧ R a' a' ∧ f a = f a') (b : image f) : - f (elt_of b) = elt_of b := -idempotent_image_fix (representative_map_idempotent H1 H2) b - -theorem representative_map_to_quotient {A : Type} {R : A → A → Prop} {f : A → A} - (H1 : ∀a, R a (f a)) (H2 : ∀a a', R a a' ↔ R a a ∧ R a' a' ∧ f a = f a') : - is_quotient R (fun_image f) elt_of := -let abs := fun_image f in -intro - (take u : image f, - obtain (a : A) (Ha : f a = elt_of u), from image_elt_of u, - have H : elt_of (abs (elt_of u)) = elt_of u, from - calc - elt_of (abs (elt_of u)) = f (elt_of u) : elt_of_fun_image _ _ - ... = f (f a) : {Ha⁻¹} - ... = f a : representative_map_idempotent H1 H2 a - ... = elt_of u : Ha, - show abs (elt_of u) = u, from subtype.eq H) - (take u : image f, - show R (elt_of u) (elt_of u), from - obtain (a : A) (Ha : f a = elt_of u), from image_elt_of u, - Ha ▸ (@representative_map_refl_rep A R f H1 H2 a)) - (take a a', - subst (fun_image_eq f a a') (H2 a a')) - -theorem representative_map_equiv_inj {A : Type} {R : A → A → Prop} - (equiv : is_equivalence R) {f : A → A} - (H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b → f a = f b) {a b : A} (H3 : f a = f b) : - R a b := -have symmR : relation.symmetric R, from rel_symm R, -have transR : relation.transitive R, from rel_trans R, -show R a b, from - have H2 : R a (f b), from H3 ▸ (H1 a), - have H3 : R (f b) b, from symmR (H1 b), - transR H2 H3 - -theorem representative_map_to_quotient_equiv {A : Type} {R : A → A → Prop} - (equiv : is_equivalence R) {f : A → A} (H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b → f a = f b) : - @is_quotient A (image f) R (fun_image f) elt_of := -representative_map_to_quotient - H1 - (take a b, - have reflR : reflexive R, from rel_refl R, - have H3 : f a = f b → R a b, from representative_map_equiv_inj equiv H1 H2, - have H4 : R a b ↔ f a = f b, from iff.intro (H2 a b) H3, - have H5 : R a b ↔ R b b ∧ f a = f b, - from subst (symm (and_absorb_left _ (reflR b))) H4, - subst (symm (and_absorb_left _ (reflR a))) H5) - -end quotient diff --git a/library/data/quotient/classical.lean b/library/data/quotient/classical.lean deleted file mode 100644 index 7f17d669c9..0000000000 --- a/library/data/quotient/classical.lean +++ /dev/null @@ -1,58 +0,0 @@ -/- -Copyright (c) 2014 Floris van Doorn. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Floris van Doorn - -A classical treatment of quotients, using Hilbert choice. --/ -import algebra.relation -import .basic - -namespace quotient -open relation nonempty subtype classical - -/- abstract quotient -/ - -noncomputable definition prelim_map {A : Type} (R : A → A → Prop) (a : A) := --- TODO: it is interesting how the elaborator fails here --- epsilon (fun b, R a b) -@epsilon _ (nonempty.intro a) (fun b, R a b) - --- TODO: only needed R reflexive (or weaker: R a a) -theorem prelim_map_rel {A : Type} {R : A → A → Prop} (H : is_equivalence R) (a : A) - : R a (prelim_map R a) := -have reflR : reflexive R, from is_equivalence.refl R, -epsilon_spec (exists.intro a (reflR a)) - --- TODO: only needed: R PER -theorem prelim_map_congr {A : Type} {R : A → A → Prop} (H1 : is_equivalence R) {a b : A} - (H2 : R a b) : prelim_map R a = prelim_map R b := -have symmR : relation.symmetric R, from is_equivalence.symm R, -have transR : relation.transitive R, from is_equivalence.trans R, -have H3 : ∀c, R a c ↔ R b c, from - take c, - iff.intro - (assume H4 : R a c, transR (symmR H2) H4) - (assume H4 : R b c, transR H2 H4), -have H4 : (fun c, R a c) = (fun c, R b c), from - funext (take c, eq.of_iff (H3 c)), -assert H5 : nonempty A, from - nonempty.intro a, -show epsilon (λc, R a c) = epsilon (λc, R b c), from - congr_arg _ H4 - -noncomputable definition quotient {A : Type} (R : A → A → Prop) : Type := image (prelim_map R) - -noncomputable definition quotient_abs {A : Type} (R : A → A → Prop) : A → quotient R := -fun_image (prelim_map R) - -noncomputable definition quotient_elt_of {A : Type} (R : A → A → Prop) : quotient R → A := elt_of - -theorem quotient_is_quotient {A : Type} (R : A → A → Prop) (H : is_equivalence R) - : is_quotient R (quotient_abs R) (quotient_elt_of R) := -representative_map_to_quotient_equiv - H - (prelim_map_rel H) - (@prelim_map_congr _ _ H) - -end quotient diff --git a/library/data/quotient/default.lean b/library/data/quotient/default.lean deleted file mode 100644 index 9c14314742..0000000000 --- a/library/data/quotient/default.lean +++ /dev/null @@ -1,5 +0,0 @@ ---- Copyright (c) 2014 Microsoft Corporation. All rights reserved. ---- Released under Apache 2.0 license as described in the file LICENSE. ---- Author: Jeremy Avigad - -import .basic diff --git a/library/data/quotient/quotient.md b/library/data/quotient/quotient.md deleted file mode 100644 index da837789a9..0000000000 --- a/library/data/quotient/quotient.md +++ /dev/null @@ -1,10 +0,0 @@ -data.quotient -============= - -* [util](util.lean) : auxiliary facts about products -* [basic](basic.lean) : the constructive core of the quotient construction -* [classical](classical.lean) : the classical version, using Hilbert choice - -These files provide an approach to defining quotients, without using -the built-in quotient types. They were initially used to define the -integers, but are no longer used there. \ No newline at end of file diff --git a/library/data/quotient/util.lean b/library/data/quotient/util.lean deleted file mode 100644 index ba25b02221..0000000000 --- a/library/data/quotient/util.lean +++ /dev/null @@ -1,100 +0,0 @@ -/- -Copyright (c) 2014 Floris van Doorn. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Floris van Doorn --/ -import logic ..prod algebra.relation -open prod eq.ops - -namespace quotient - -/- auxiliary facts about products -/ - - variables {A B : Type} - - /- flip -/ - - definition flip (a : A × B) : B × A := pair (pr2 a) (pr1 a) - - theorem flip_def (a : A × B) : flip a = pair (pr2 a) (pr1 a) := rfl - theorem flip_pair (a : A) (b : B) : flip (pair a b) = pair b a := rfl - theorem flip_pr1 (a : A × B) : pr1 (flip a) = pr2 a := rfl - theorem flip_pr2 (a : A × B) : pr2 (flip a) = pr1 a := rfl - theorem flip_flip : Π a : A × B, flip (flip a) = a - | (pair x y) := rfl - - theorem P_flip {P : A → B → Prop} (a : A × B) (H : P (pr1 a) (pr2 a)) - : P (pr2 (flip a)) (pr1 (flip a)) := - (flip_pr1 a)⁻¹ ▸ (flip_pr2 a)⁻¹ ▸ H - - theorem flip_inj {a b : A × B} (H : flip a = flip b) : a = b := - have H2 : flip (flip a) = flip (flip b), from congr_arg flip H, - show a = b, from (flip_flip a) ▸ (flip_flip b) ▸ H2 - - /- coordinatewise unary maps -/ - - definition map_pair (f : A → B) (a : A × A) : B × B := - pair (f (pr1 a)) (f (pr2 a)) - - theorem map_pair_def (f : A → B) (a : A × A) - : map_pair f a = pair (f (pr1 a)) (f (pr2 a)) := - rfl - - theorem map_pair_pair (f : A → B) (a a' : A) - : map_pair f (pair a a') = pair (f a) (f a') := - (pr1.mk a a') ▸ (pr2.mk a a') ▸ rfl - - theorem map_pair_pr1 (f : A → B) (a : A × A) : pr1 (map_pair f a) = f (pr1 a) := - by esimp - - theorem map_pair_pr2 (f : A → B) (a : A × A) : pr2 (map_pair f a) = f (pr2 a) := - by esimp - - /- coordinatewise binary maps -/ - - definition map_pair2 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) : C × C := - pair (f (pr1 a) (pr1 b)) (f (pr2 a) (pr2 b)) - - theorem map_pair2_def {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) : - map_pair2 f a b = pair (f (pr1 a) (pr1 b)) (f (pr2 a) (pr2 b)) := rfl - - theorem map_pair2_pair {A B C : Type} (f : A → B → C) (a a' : A) (b b' : B) : - map_pair2 f (pair a a') (pair b b') = pair (f a b) (f a' b') := by esimp - - theorem map_pair2_pr1 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) : - pr1 (map_pair2 f a b) = f (pr1 a) (pr1 b) := by esimp - - theorem map_pair2_pr2 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) : - pr2 (map_pair2 f a b) = f (pr2 a) (pr2 b) := by esimp - - theorem map_pair2_flip {A B C : Type} (f : A → B → C) : Π (a : A × A) (b : B × B), - flip (map_pair2 f a b) = map_pair2 f (flip a) (flip b) - | (pair a₁ a₂) (pair b₁ b₂) := rfl - --- add_rewrite flip_pr1 flip_pr2 flip_pair --- add_rewrite map_pair_pr1 map_pair_pr2 map_pair_pair --- add_rewrite map_pair2_pr1 map_pair2_pr2 map_pair2_pair - -theorem map_pair2_comm {A B : Type} {f : A → A → B} (Hcomm : ∀a b : A, f a b = f b a) - : Π (v w : A × A), map_pair2 f v w = map_pair2 f w v -| (pair v₁ v₂) (pair w₁ w₂) := - !map_pair2_pair ⬝ by rewrite [Hcomm v₁ w₁, Hcomm v₂ w₂] ⬝ (eq.symm !map_pair2_pair) - -theorem map_pair2_assoc {A : Type} {f : A → A → A} - (Hassoc : ∀a b c : A, f (f a b) c = f a (f b c)) (u v w : A × A) : - map_pair2 f (map_pair2 f u v) w = map_pair2 f u (map_pair2 f v w) := -show pair (f (f (pr1 u) (pr1 v)) (pr1 w)) (f (f (pr2 u) (pr2 v)) (pr2 w)) = - pair (f (pr1 u) (f (pr1 v) (pr1 w))) (f (pr2 u) (f (pr2 v) (pr2 w))), -by rewrite [Hassoc (pr1 u) (pr1 v) (pr1 w), Hassoc (pr2 u) (pr2 v) (pr2 w)] - -theorem map_pair2_id_right {A B : Type} {f : A → B → A} {e : B} (Hid : ∀a : A, f a e = a) - : Π (v : A × A), map_pair2 f v (pair e e) = v -| (pair v₁ v₂) := - !map_pair2_pair ⬝ by rewrite [Hid v₁, Hid v₂] - -theorem map_pair2_id_left {A B : Type} {f : B → A → A} {e : B} (Hid : ∀a : A, f e a = a) - : Π (v : A × A), map_pair2 f (pair e e) v = v -| (pair v₁ v₂) := - !map_pair2_pair ⬝ by rewrite [Hid v₁, Hid v₂] - -end quotient diff --git a/library/init/function.lean b/library/init/function.lean index 18d8315f9b..dff86273b3 100644 --- a/library/init/function.lean +++ b/library/init/function.lean @@ -21,9 +21,6 @@ definition compose_right [reducible] [unfold_full] (f : B → B → B) (g : A definition compose_left [reducible] [unfold_full] (f : B → B → B) (g : A → B) : A → B → B := λ a b, f (g a) b -definition id [reducible] [unfold_full] (a : A) : A := -a - definition on_fun [reducible] [unfold_full] (f : B → B → C) (g : A → B) : A → A → C := λx y, f (g x) (g y) diff --git a/library/init/logic.lean b/library/init/logic.lean index 1ddb4d955d..593a19db4a 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -6,6 +6,9 @@ Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn prelude import init.datatypes init.reserved_notation +definition id [reducible] [unfold_full] {A : Type} (a : A) : A := +a + /- implication -/ definition implies (a b : Prop) := a → b @@ -237,6 +240,9 @@ variables {a b c d : Prop} theorem and.elim (H₁ : a ∧ b) (H₂ : a → b → c) : c := and.rec H₂ H₁ +theorem and.swap : a ∧ b → b ∧ a := +and.rec (λHa Hb, and.intro Hb Ha) + /- or -/ notation a \/ b := or a b @@ -253,6 +259,8 @@ assume not_em : ¬(a ∨ ¬a), assume pos_a : a, absurd (or.inl pos_a) not_em, absurd (or.inr neg_a) not_em +theorem or.swap : a ∨ b → b ∨ a := or.rec or.inr or.inl + /- iff -/ definition iff (a b : Prop) := (a → b) ∧ (b → a) @@ -322,38 +330,146 @@ attribute iff.refl [refl] attribute iff.symm [symm] attribute iff.trans [trans] +theorem imp_congr [congr] (H1 : a ↔ c) (H2 : b ↔ d) : (a → b) ↔ (c → d) := +iff.intro + (λHab Hc, iff.mp H2 (Hab (iff.mpr H1 Hc))) + (λHcd Ha, iff.mpr H2 (Hcd (iff.mp H1 Ha))) + theorem not_not_intro (Ha : a) : ¬¬a := assume Hna : ¬a, Hna Ha -theorem not_true : (¬ true) ↔ false := +theorem not_true [simp] : (¬ true) ↔ false := iff_false_intro (not_not_intro trivial) -theorem not_false_iff : (¬ false) ↔ true := +theorem not_false_iff [simp] : (¬ false) ↔ true := iff_true_intro not_false +theorem not_congr [congr] (H : a ↔ b) : ¬a ↔ ¬b := +iff.intro (λ H₁ H₂, H₁ (iff.mpr H H₂)) (λ H₁ H₂, H₁ (iff.mp H H₂)) + theorem ne_self_iff_false {A : Type} (a : A) : (a ≠ a) ↔ false := iff.intro false_of_ne false.elim -theorem eq_self_iff_true {A : Type} (a : A) : (a = a) ↔ true := +theorem eq_self_iff_true [simp] {A : Type} (a : A) : (a = a) ↔ true := iff_true_intro rfl -theorem heq_self_iff_true {A : Type} (a : A) : (a == a) ↔ true := +theorem heq_self_iff_true [simp] {A : Type} (a : A) : (a == a) ↔ true := iff_true_intro (heq.refl a) -theorem iff_not_self (a : Prop) : (a ↔ ¬a) ↔ false := +theorem iff_not_self [simp] (a : Prop) : (a ↔ ¬a) ↔ false := iff_false_intro (λ H, have H' : ¬a, from (λ Ha, (iff.mp H Ha) Ha), H' (iff.mpr H H')) -theorem true_iff_false : (true ↔ false) ↔ false := +theorem true_iff_false [simp] : (true ↔ false) ↔ false := iff_false_intro (λ H, iff.mp H trivial) -theorem false_iff_true : (false ↔ true) ↔ false := +theorem false_iff_true [simp] : (false ↔ true) ↔ false := iff_false_intro (λ H, iff.mpr H trivial) theorem false_of_true_iff_false : (true ↔ false) → false := assume H, iff.mp H trivial +/- and simp rules -/ +theorem and.imp (H₂ : a → c) (H₃ : b → d) : a ∧ b → c ∧ d := +and.rec (λHa Hb, and.intro (H₂ Ha) (H₃ Hb)) + +theorem and_congr [congr] (H1 : a ↔ c) (H2 : b ↔ d) : (a ∧ b) ↔ (c ∧ d) := +iff.intro (and.imp (iff.mp H1) (iff.mp H2)) (and.imp (iff.mpr H1) (iff.mpr H2)) + +theorem and.comm [simp] : a ∧ b ↔ b ∧ a := +iff.intro and.swap and.swap + +theorem and.assoc [simp] : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) := +iff.intro + (and.rec (λ H' Hc, and.rec (λ Ha Hb, and.intro Ha (and.intro Hb Hc)) H')) + (and.rec (λ Ha, and.rec (λ Hb Hc, and.intro (and.intro Ha Hb) Hc))) + +theorem and.left_comm [simp] : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) := +iff.trans (iff.symm !and.assoc) (iff.trans (and_congr !and.comm !iff.refl) !and.assoc) + +theorem and_iff_left {a b : Prop} (Hb : b) : (a ∧ b) ↔ a := +iff.intro and.left (λHa, and.intro Ha Hb) + +theorem and_iff_right {a b : Prop} (Ha : a) : (a ∧ b) ↔ b := +iff.intro and.right (and.intro Ha) + +theorem and_true [simp] (a : Prop) : a ∧ true ↔ a := +and_iff_left trivial + +theorem true_and [simp] (a : Prop) : true ∧ a ↔ a := +and_iff_right trivial + +theorem and_false [simp] (a : Prop) : a ∧ false ↔ false := +iff_false_intro and.right + +theorem false_and [simp] (a : Prop) : false ∧ a ↔ false := +iff_false_intro and.left + +theorem and_self [simp] (a : Prop) : a ∧ a ↔ a := +iff.intro and.left (assume H, and.intro H H) + +/- or simp rules -/ + +theorem or.imp (H₂ : a → c) (H₃ : b → d) : a ∨ b → c ∨ d := +or.rec (λ H, or.inl (H₂ H)) (λ H, or.inr (H₃ H)) + +theorem or.imp_left (H : a → b) : a ∨ c → b ∨ c := +or.imp H id + +theorem or.imp_right (H : a → b) : c ∨ a → c ∨ b := +or.imp id H + +theorem or_congr [congr] (H1 : a ↔ c) (H2 : b ↔ d) : (a ∨ b) ↔ (c ∨ d) := +iff.intro (or.imp (iff.mp H1) (iff.mp H2)) (or.imp (iff.mpr H1) (iff.mpr H2)) + +theorem or.comm [simp] : a ∨ b ↔ b ∨ a := iff.intro or.swap or.swap + +theorem or.assoc [simp] : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) := +iff.intro + (or.rec (or.imp_right or.inl) (λ H, or.inr (or.inr H))) + (or.rec (λ H, or.inl (or.inl H)) (or.imp_left or.inr)) + +theorem or.left_comm [simp] : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c) := +iff.trans (iff.symm !or.assoc) (iff.trans (or_congr !or.comm !iff.refl) !or.assoc) + +theorem or_true [simp] (a : Prop) : a ∨ true ↔ true := +iff_true_intro (or.inr trivial) + +theorem true_or [simp] (a : Prop) : true ∨ a ↔ true := +iff_true_intro (or.inl trivial) + +theorem or_false [simp] (a : Prop) : a ∨ false ↔ a := +iff.intro (or.rec id false.elim) or.inl + +theorem false_or [simp] (a : Prop) : false ∨ a ↔ a := +iff.trans or.comm !or_false + +theorem or_self [simp] (a : Prop) : a ∨ a ↔ a := +iff.intro (or.rec id id) or.inl + +/- iff simp rules -/ + +theorem iff_true [simp] (a : Prop) : (a ↔ true) ↔ a := +iff.intro (assume H, iff.mpr H trivial) iff_true_intro + +theorem true_iff [simp] (a : Prop) : (true ↔ a) ↔ a := +iff.trans iff.comm !iff_true + +theorem iff_false [simp] (a : Prop) : (a ↔ false) ↔ ¬ a := +iff.intro and.left iff_false_intro + +theorem false_iff [simp] (a : Prop) : (false ↔ a) ↔ ¬ a := +iff.trans iff.comm !iff_false + +theorem iff_self [simp] (a : Prop) : (a ↔ a) ↔ true := +iff_true_intro iff.rfl + +theorem iff_congr [congr] (H1 : a ↔ c) (H2 : b ↔ d) : (a ↔ b) ↔ (c ↔ d) := +and_congr (imp_congr H1 H2) (imp_congr H2 H1) + +/- exists -/ + inductive Exists {A : Type} (P : A → Prop) : Prop := intro : ∀ (a : A), P a → Exists P @@ -366,6 +482,54 @@ theorem exists.elim {A : Type} {p : A → Prop} {B : Prop} (H1 : ∃x, p x) (H2 : ∀ (a : A), p a → B) : B := Exists.rec H2 H1 +/- exists unique -/ + +definition exists_unique {A : Type} (p : A → Prop) := +∃x, p x ∧ ∀y, p y → y = x + +notation `∃!` binders `, ` r:(scoped P, exists_unique P) := r + +theorem exists_unique.intro {A : Type} {p : A → Prop} (w : A) (H1 : p w) (H2 : ∀y, p y → y = w) : + ∃!x, p x := +exists.intro w (and.intro H1 H2) + +theorem exists_unique.elim {A : Type} {p : A → Prop} {b : Prop} + (H2 : ∃!x, p x) (H1 : ∀x, p x → (∀y, p y → y = x) → b) : b := +exists.elim H2 (λ w Hw, H1 w (and.left Hw) (and.right Hw)) + +theorem exists_unique_of_exists_of_unique {A : Type} {p : A → Prop} + (Hex : ∃ x, p x) (Hunique : ∀ y₁ y₂, p y₁ → p y₂ → y₁ = y₂) : ∃! x, p x := +exists.elim Hex (λ x px, exists_unique.intro x px (take y, suppose p y, Hunique y x this px)) + +theorem exists_of_exists_unique {A : Type} {p : A → Prop} (H : ∃! x, p x) : ∃ x, p x := +exists.elim H (λ x Hx, exists.intro x (and.left Hx)) + +theorem unique_of_exists_unique {A : Type} {p : A → Prop} + (H : ∃! x, p x) {y₁ y₂ : A} (py₁ : p y₁) (py₂ : p y₂) : y₁ = y₂ := +exists_unique.elim H + (take x, suppose p x, + assume unique : ∀ y, p y → y = x, + show y₁ = y₂, from eq.trans (unique _ py₁) (eq.symm (unique _ py₂))) + +/- exists, forall, exists unique congruences -/ +section +variables {A : Type} {p₁ p₂ : A → Prop} + +theorem forall_congr [congr] {A : Type} {P Q : A → Prop} (H : ∀a, (P a ↔ Q a)) : (∀a, P a) ↔ ∀a, Q a := +iff.intro (λp a, iff.mp (H a) (p a)) (λq a, iff.mpr (H a) (q a)) + +theorem exists_imp_exists {A : Type} {P Q : A → Prop} (H : ∀a, (P a → Q a)) (p : ∃a, P a) : ∃a, Q a := +exists.elim p (λa Hp, exists.intro a (H a Hp)) + +theorem exists_congr [congr] {A : Type} {P Q : A → Prop} (H : ∀a, (P a ↔ Q a)) : (∃a, P a) ↔ ∃a, Q a := +iff.intro + (exists_imp_exists (λa, iff.mp (H a))) + (exists_imp_exists (λa, iff.mpr (H a))) + +theorem exists_unique_congr [congr] (H : ∀ x, p₁ x ↔ p₂ x) : (∃! x, p₁ x) ↔ (∃! x, p₂ x) := +exists_congr (λx, and_congr (H x) (forall_congr (λy, imp_congr (H y) iff.rfl))) +end + /- decidable -/ inductive decidable [class] (p : Prop) : Type := @@ -621,6 +785,12 @@ theorem if_simp_congr [congr] {A : Type} {b c : Prop} [dec_b : decidable b] {x y ite b x y = (@ite c (decidable_of_decidable_of_iff dec_b h_c) A u v) := @if_ctx_simp_congr A b c dec_b x y u v h_c (λ h, h_t) (λ h, h_e) +definition if_true [simp] {A : Type} (t e : A) : (if true then t else e) = t := +if_pos trivial + +definition if_false [simp] {A : Type} (t e : A) : (if false then t else e) = e := +if_neg not_false + theorem if_congr_prop {b c x y u v : Prop} [dec_b : decidable b] [dec_c : decidable c] (h_c : b ↔ c) (h_t : c → (x ↔ u)) (h_e : ¬c → (y ↔ v)) : ite b x y ↔ ite c u v := diff --git a/library/logic/connectives.lean b/library/logic/connectives.lean index 279dfdc4f0..bc6dc782bf 100644 --- a/library/logic/connectives.lean +++ b/library/logic/connectives.lean @@ -37,11 +37,6 @@ theorem imp_false (a : Prop) : (a → false) ↔ ¬ a := iff.rfl theorem false_imp (a : Prop) : (false → a) ↔ true := iff_true_intro false.elim -theorem imp_iff_imp (H1 : a ↔ c) (H2 : b ↔ d) : (a → b) ↔ (c → d) := -iff.intro - (λHab Hc, iff.mp H2 (Hab (iff.mpr H1 Hc))) - (λHcd Ha, iff.mpr H2 (Hcd (iff.mp H1 Ha))) - /- not -/ theorem not.elim {A : Type} (H1 : ¬a) (H2 : a) : A := absurd H2 H1 @@ -73,12 +68,6 @@ not.mto and.left definition not_and_of_not_right (a : Prop) {b : Prop} : ¬b → ¬(a ∧ b) := not.mto and.right -theorem and.swap : a ∧ b → b ∧ a := -and.rec (λHa Hb, and.intro Hb Ha) - -theorem and.imp (H₂ : a → c) (H₃ : b → d) : a ∧ b → c ∧ d := -and.rec (λHa Hb, and.intro (H₂ Ha) (H₃ Hb)) - theorem and.imp_left (H : a → b) : a ∧ c → b ∧ c := and.imp H imp.id @@ -94,61 +83,16 @@ and.imp_left H H₁ theorem and_of_and_of_imp_right (H₁ : c ∧ a) (H : a → b) : c ∧ b := and.imp_right H H₁ -theorem and.comm [simp] : a ∧ b ↔ b ∧ a := -iff.intro and.swap and.swap - -theorem and.assoc [simp] : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) := -iff.intro - (assume H, - obtain [Ha Hb] Hc, from H, - and.intro Ha (and.intro Hb Hc)) - (assume H, - obtain Ha Hb Hc, from H, - and.intro (and.intro Ha Hb) Hc) - -theorem and_iff_right {a b : Prop} (Ha : a) : (a ∧ b) ↔ b := -iff.intro and.right (and.intro Ha) - -theorem and_iff_left {a b : Prop} (Hb : b) : (a ∧ b) ↔ a := -iff.intro and.left (λHa, and.intro Ha Hb) - -theorem and_true [simp] (a : Prop) : a ∧ true ↔ a := -and_iff_left trivial - -theorem true_and [simp] (a : Prop) : true ∧ a ↔ a := -and_iff_right trivial - -theorem and_false [simp] (a : Prop) : a ∧ false ↔ false := -iff_false_intro and.right - -theorem false_and [simp] (a : Prop) : false ∧ a ↔ false := -iff_false_intro and.left - -theorem and_self [simp] (a : Prop) : a ∧ a ↔ a := -iff.intro and.left (assume H, and.intro H H) - theorem and_imp_iff (a b c : Prop) : (a ∧ b → c) ↔ (a → b → c) := iff.intro (λH a b, H (and.intro a b)) and.rec theorem and_imp_eq (a b c : Prop) : (a ∧ b → c) = (a → b → c) := propext !and_imp_iff -theorem and_iff_and (H1 : a ↔ c) (H2 : b ↔ d) : (a ∧ b) ↔ (c ∧ d) := -iff.intro (and.imp (iff.mp H1) (iff.mp H2)) (and.imp (iff.mpr H1) (iff.mpr H2)) - /- or -/ definition not_or : ¬a → ¬b → ¬(a ∨ b) := or.rec -theorem or.imp (H₂ : a → c) (H₃ : b → d) : a ∨ b → c ∨ d := -or.rec (imp.syl or.inl H₂) (imp.syl or.inr H₃) - -theorem or.imp_left (H : a → b) : a ∨ c → b ∨ c := -or.imp H imp.id - -theorem or.imp_right (H : a → b) : c ∨ a → c ∨ b := -or.imp imp.id H - theorem or_of_or_of_imp_of_imp (H₁ : a ∨ b) (H₂ : a → c) (H₃ : b → d) : c ∨ d := or.imp H₂ H₃ H₁ @@ -161,21 +105,12 @@ or.imp_right H H₁ theorem or.elim3 (H : a ∨ b ∨ c) (Ha : a → d) (Hb : b → d) (Hc : c → d) : d := or.elim H Ha (assume H₂, or.elim H₂ Hb Hc) -theorem or.swap : a ∨ b → b ∨ a := or.rec or.inr or.inl - theorem or_resolve_right (H₁ : a ∨ b) (H₂ : ¬a) : b := or.elim H₁ (not.elim H₂) imp.id theorem or_resolve_left (H₁ : a ∨ b) : ¬b → a := or_resolve_right (or.swap H₁) -theorem or.comm [simp] : a ∨ b ↔ b ∨ a := iff.intro or.swap or.swap - -theorem or.assoc [simp] : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) := -iff.intro - (or.rec (or.imp_right or.inl) (imp.syl or.inr or.inr)) - (or.rec (imp.syl or.inl or.inl) (or.imp_left or.inr)) - theorem or.imp_distrib : ((a ∨ b) → c) ↔ ((a → c) ∧ (b → c)) := iff.intro (λH, and.intro (imp.syl H or.inl) (imp.syl H or.inr)) @@ -187,21 +122,6 @@ iff.intro (or.rec Ha imp.id) or.inr theorem or_iff_left_of_imp {a b : Prop} (Hb : b → a) : (a ∨ b) ↔ a := iff.intro (or.rec imp.id Hb) or.inl -theorem or_true [simp] (a : Prop) : a ∨ true ↔ true := -iff_true_intro (or.inr trivial) - -theorem true_or [simp] (a : Prop) : true ∨ a ↔ true := -iff_true_intro (or.inl trivial) - -theorem or_false [simp] (a : Prop) : a ∨ false ↔ a := -iff.intro (or.rec imp.id false.elim) or.inl - -theorem false_or [simp] (a : Prop) : false ∨ a ↔ a := -iff.trans or.comm !or_false - -theorem or_self (a : Prop) : a ∨ a ↔ a := -iff.intro (or.rec imp.id imp.id) or.inl - theorem or_iff_or (H1 : a ↔ c) (H2 : b ↔ d) : (a ∨ b) ↔ (c ∨ d) := iff.intro (or.imp (iff.mp H1) (iff.mp H2)) (or.imp (iff.mpr H1) (iff.mpr H2)) @@ -221,79 +141,14 @@ iff.intro (and.rec (or.rec (imp.syl imp.intro or.inl) (imp.syl or.imp_right and.intro))) theorem or.right_distrib (a b c : Prop) : (a ∧ b) ∨ c ↔ (a ∨ c) ∧ (b ∨ c) := -iff.trans (iff.trans !or.comm !or.left_distrib) (and_iff_and !or.comm !or.comm) +iff.trans (iff.trans !or.comm !or.left_distrib) (and_congr !or.comm !or.comm) /- iff -/ definition iff.def : (a ↔ b) = ((a → b) ∧ (b → a)) := rfl -theorem iff_true [simp] (a : Prop) : (a ↔ true) ↔ a := -iff.intro (assume H, iff.mpr H trivial) iff_true_intro - -theorem true_iff [simp] (a : Prop) : (true ↔ a) ↔ a := -iff.trans iff.comm !iff_true - -theorem iff_false [simp] (a : Prop) : (a ↔ false) ↔ ¬ a := -iff.intro and.left iff_false_intro - -theorem false_iff [simp] (a : Prop) : (false ↔ a) ↔ ¬ a := -iff.trans iff.comm !iff_false - -theorem iff_self [simp] (a : Prop) : (a ↔ a) ↔ true := -iff_true_intro iff.rfl - theorem forall_imp_forall {A : Type} {P Q : A → Prop} (H : ∀a, (P a → Q a)) (p : ∀a, P a) (a : A) : Q a := (H a) (p a) -theorem forall_iff_forall {A : Type} {P Q : A → Prop} (H : ∀a, (P a ↔ Q a)) : (∀a, P a) ↔ ∀a, Q a := -iff.intro (λp a, iff.mp (H a) (p a)) (λq a, iff.mpr (H a) (q a)) - -theorem exists_imp_exists {A : Type} {P Q : A → Prop} (H : ∀a, (P a → Q a)) (p : ∃a, P a) : ∃a, Q a := -exists.elim p (λa Hp, exists.intro a (H a Hp)) - -theorem exists_iff_exists {A : Type} {P Q : A → Prop} (H : ∀a, (P a ↔ Q a)) : (∃a, P a) ↔ ∃a, Q a := -iff.intro - (exists_imp_exists (λa, iff.mp (H a))) - (exists_imp_exists (λa, iff.mpr (H a))) - theorem imp_iff {P : Prop} (Q : Prop) (p : P) : (P → Q) ↔ Q := iff.intro (λf, f p) imp.intro - -theorem iff_iff_iff (H1 : a ↔ c) (H2 : b ↔ d) : (a ↔ b) ↔ (c ↔ d) := -and_iff_and (imp_iff_imp H1 H2) (imp_iff_imp H2 H1) - -/- if-then-else -/ - -section - open eq.ops - - variables {A : Type} {c₁ c₂ : Prop} - - definition if_true [simp] (t e : A) : (if true then t else e) = t := - if_pos trivial - - definition if_false [simp] (t e : A) : (if false then t else e) = e := - if_neg not_false -end - -/- congruences -/ - -theorem congr_not [congr] {a b : Prop} (H : a ↔ b) : ¬a ↔ ¬b := -not_iff_not H - -section - variables {a₁ b₁ a₂ b₂ : Prop} - variables (H₁ : a₁ ↔ b₁) (H₂ : a₂ ↔ b₂) - - theorem congr_and [congr] : a₁ ∧ a₂ ↔ b₁ ∧ b₂ := - and_iff_and H₁ H₂ - - theorem congr_or [congr] : a₁ ∨ a₂ ↔ b₁ ∨ b₂ := - or_iff_or H₁ H₂ - - theorem congr_imp [congr] : (a₁ → a₂) ↔ (b₁ → b₂) := - imp_iff_imp H₁ H₂ - - theorem congr_iff [congr] : (a₁ ↔ a₂) ↔ (b₁ ↔ b₂) := - iff_iff_iff H₁ H₂ -end diff --git a/library/logic/default.lean b/library/logic/default.lean index fc251202e3..21d615c022 100644 --- a/library/logic/default.lean +++ b/library/logic/default.lean @@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Jeremy Avigad -/ import logic.eq logic.connectives logic.cast -import logic.quantifiers logic.instances logic.identities +import logic.quantifiers logic.identities diff --git a/library/logic/examples/instances_test.lean b/library/logic/examples/instances_test.lean deleted file mode 100644 index 1b8888e4c9..0000000000 --- a/library/logic/examples/instances_test.lean +++ /dev/null @@ -1,36 +0,0 @@ -/- -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Jeremy Avigad - -Illustrates substitution and congruence with iff. --/ - -import ..instances -open relation -open relation.general_subst -open relation.iff_ops -open eq.ops - -example (a b : Prop) (H : a ↔ b) (H1 : a) : b := mp H H1 - -/- -exit -example (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) := -H1 ▸ H2 - -example (a b c d e : Prop) (H1 : a ↔ b) : (a ∨ c → ¬(d → a)) ↔ (b ∨ c → ¬(d → b)) := -is_congruence.congr iff (λa, (a ∨ c → ¬(d → a))) H1 - -example (T : Type) (a b c d : T) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d := -H1 ⬝ H2⁻¹ ⬝ H3 - -example (a b c d : Prop) (H1 : a ↔ b) (H2 : c ↔ b) (H3 : c ↔ d) : a ↔ d := -H1 ⬝ (H2⁻¹ ⬝ H3) - -example (T : Type) (a b c d : T) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d := -H1 ⬝ H2⁻¹ ⬝ H3 - -example (a b c d : Prop) (H1 : a ↔ b) (H2 : c ↔ b) (H3 : c ↔ d) : a ↔ d := -H1 ⬝ H2⁻¹ ⬝ H3 --/ diff --git a/library/logic/examples/negative.lean b/library/logic/examples/negative.lean index 2e8d07afee..e62fdf1343 100644 --- a/library/logic/examples/negative.lean +++ b/library/logic/examples/negative.lean @@ -23,8 +23,8 @@ axiom introD : (D → D) → D axiom recD : Π {C : D → Type}, (Π (f : D → D) (r : Π d, C (f d)), C (introD f)) → (Π (d : D), C d) -- We would also get a computational rule for the eliminator, but we don't need it for deriving the inconsistency. -noncomputable definition id : D → D := λd, d -noncomputable definition v : D := introD id +noncomputable definition id' : D → D := λd, d +noncomputable definition v : D := introD id' theorem inconsistent : false := recD (λ f ih, ih v) v diff --git a/library/logic/identities.lean b/library/logic/identities.lean index 700d47e1fc..81473cd8dc 100644 --- a/library/logic/identities.lean +++ b/library/logic/identities.lean @@ -6,8 +6,8 @@ Authors: Jeremy Avigad, Leonardo de Moura Useful logical identities. Since we are not using propositional extensionality, some of the calculations use the type class support provided by logic.instances. -/ -import logic.connectives logic.instances logic.quantifiers logic.cast -open relation decidable relation.iff_ops +import logic.connectives logic.quantifiers logic.cast +open decidable theorem or.right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b := calc @@ -15,12 +15,6 @@ calc ... ↔ a ∨ (c ∨ b) : {or.comm} ... ↔ (a ∨ c) ∨ b : iff.symm or.assoc -theorem or.left_comm [simp] (a b c : Prop) : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c) := -calc - a ∨ (b ∨ c) ↔ (a ∨ b) ∨ c : iff.symm or.assoc - ... ↔ (b ∨ a) ∨ c : {or.comm} - ... ↔ b ∨ (a ∨ c) : or.assoc - theorem and.right_comm (a b c : Prop) : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b := calc (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) : and.assoc @@ -31,19 +25,13 @@ theorem or_not_self_iff {a : Prop} [D : decidable a] : a ∨ ¬ a ↔ true := iff.intro (assume H, trivial) (assume H, em a) theorem not_or_self_iff {a : Prop} [D : decidable a] : ¬ a ∨ a ↔ true := -!or.comm ▸ !or_not_self_iff +iff.intro (λ H, trivial) (λ H, or.swap (em a)) theorem and_not_self_iff {a : Prop} : a ∧ ¬ a ↔ false := iff.intro (assume H, (and.right H) (and.left H)) (assume H, false.elim H) theorem not_and_self_iff {a : Prop} : ¬ a ∧ a ↔ false := -!and.comm ▸ !and_not_self_iff - -theorem and.left_comm [simp] (a b c : Prop) : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) := -calc - a ∧ (b ∧ c) ↔ (a ∧ b) ∧ c : iff.symm and.assoc - ... ↔ (b ∧ a) ∧ c : {and.comm} - ... ↔ b ∧ (a ∧ c) : and.assoc +iff.intro (λ H, and.elim H (by contradiction)) (λ H, false.elim H) theorem not_not_iff {a : Prop} [D : decidable a] : (¬¬a) ↔ a := iff.intro by_contradiction not_not_intro diff --git a/library/logic/instances.lean b/library/logic/instances.lean deleted file mode 100644 index 2f5cf01ca1..0000000000 --- a/library/logic/instances.lean +++ /dev/null @@ -1,77 +0,0 @@ -/- -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Jeremy Avigad - -Class instances for iff and eq. --/ - -import logic.connectives algebra.relation - -namespace relation - -/- logical equivalence relations -/ - -definition is_equivalence_eq [instance] (T : Type) : relation.is_equivalence (@eq T) := -relation.is_equivalence.mk (@eq.refl T) (@eq.symm T) (@eq.trans T) - -definition is_equivalence_iff [instance] : relation.is_equivalence iff := -relation.is_equivalence.mk @iff.refl @iff.symm @iff.trans - -/- congruences for logic operations -/ - -definition is_congruence_not : is_congruence iff iff not := -is_congruence.mk @congr_not - -definition is_congruence_and : is_congruence2 iff iff iff and := -is_congruence2.mk @congr_and - -definition is_congruence_or : is_congruence2 iff iff iff or := -is_congruence2.mk @congr_or - -definition is_congruence_imp : is_congruence2 iff iff iff imp := -is_congruence2.mk @congr_imp - -definition is_congruence_iff : is_congruence2 iff iff iff iff := -is_congruence2.mk @congr_iff - -definition is_congruence_not_compose [instance] := is_congruence.compose is_congruence_not -definition is_congruence_and_compose [instance] := is_congruence.compose21 is_congruence_and -definition is_congruence_or_compose [instance] := is_congruence.compose21 is_congruence_or -definition is_congruence_implies_compose [instance] := is_congruence.compose21 is_congruence_imp -definition is_congruence_iff_compose [instance] := is_congruence.compose21 is_congruence_iff - -/- a general substitution operation with respect to an arbitrary congruence -/ - -namespace general_subst - theorem subst {T : Type} (R : T → T → Prop) ⦃P : T → Prop⦄ [C : is_congruence R iff P] - {a b : T} (H : R a b) (H1 : P a) : P b := iff.elim_left (is_congruence.app C H) H1 -end general_subst - -/- iff can be coerced to implication -/ - -definition mp_like_iff [instance] : relation.mp_like iff := -relation.mp_like.mk @iff.mp - -/- support for calculations with iff -/ - -namespace iff - theorem subst {P : Prop → Prop} [C : is_congruence iff iff P] {a b : Prop} - (H : a ↔ b) (H1 : P a) : P b := - @general_subst.subst Prop iff P C a b H H1 -end iff - -attribute iff.subst [subst] - -namespace iff_ops - notation H ⁻¹ := iff.symm H - notation H1 ⬝ H2 := iff.trans H1 H2 - notation H1 ▸ H2 := iff.subst H1 H2 - definition refl := iff.refl - definition symm := @iff.symm - definition trans := @iff.trans - definition subst := @iff.subst - definition mp := @iff.mp -end iff_ops - -end relation diff --git a/library/logic/quantifiers.lean b/library/logic/quantifiers.lean index ca55b9cdd9..5fad4f62cf 100644 --- a/library/logic/quantifiers.lean +++ b/library/logic/quantifiers.lean @@ -27,12 +27,6 @@ assume H1 : ∃ x, ¬ p x, theorem not_forall_of_exists_not {A : Type} {P : A → Prop} (H : ∃ a : A, ¬ P a) : ¬ ∀ a : A, P a := assume H', not_exists_not_of_forall H' H -theorem forall_congr {A : Type} {φ ψ : A → Prop} : (∀ x, φ x ↔ ψ x) → ((∀ x, φ x) ↔ (∀ x, ψ x)) := -forall_iff_forall - -theorem exists_congr {A : Type} {φ ψ : A → Prop} : (∀ x, φ x ↔ ψ x) → ((∃ x, φ x) ↔ (∃ x, ψ x)) := -exists_iff_exists - theorem forall_true_iff_true (A : Type) : (∀ x : A, true) ↔ true := iff_true_intro (λH, trivial) @@ -70,41 +64,6 @@ section else inr (Exists.rec (λh, and.rec (λheq, eq.substr heq pa))) end -/- exists_unique -/ - -definition exists_unique {A : Type} (p : A → Prop) := -∃x, p x ∧ ∀y, p y → y = x - -notation `∃!` binders `, ` r:(scoped P, exists_unique P) := r - -theorem exists_unique.intro {A : Type} {p : A → Prop} (w : A) (H1 : p w) (H2 : ∀y, p y → y = w) : - ∃!x, p x := -exists.intro w (and.intro H1 H2) - -theorem exists_unique.elim {A : Type} {p : A → Prop} {b : Prop} - (H2 : ∃!x, p x) (H1 : ∀x, p x → (∀y, p y → y = x) → b) : b := -obtain w Hw, from H2, -H1 w (and.left Hw) (and.right Hw) - -theorem exists_unique_of_exists_of_unique {A : Type} {p : A → Prop} - (Hex : ∃ x, p x) (Hunique : ∀ y₁ y₂, p y₁ → p y₂ → y₁ = y₂) : - ∃! x, p x := -obtain x px, from Hex, -exists_unique.intro x px (take y, suppose p y, show y = x, from !Hunique this px) - -theorem exists_of_exists_unique {A : Type} {p : A → Prop} (H : ∃! x, p x) : - ∃ x, p x := -obtain x Hx, from H, -exists.intro x (and.left Hx) - -theorem unique_of_exists_unique {A : Type} {p : A → Prop} - (H : ∃! x, p x) {y₁ y₂ : A} (py₁ : p y₁) (py₂ : p y₂) : - y₁ = y₂ := -exists_unique.elim H - (take x, suppose p x, - assume unique : ∀ y, p y → y = x, - show y₁ = y₂, from eq.trans (unique _ py₁) (eq.symm (unique _ py₂))) - /- definite description -/ section @@ -120,20 +79,3 @@ section y = the H := unique_of_exists_unique H Hy (the_spec H) end - -/- congruences -/ - -section - variables {A : Type} {p₁ p₂ : A → Prop} (H : ∀ x, p₁ x ↔ p₂ x) - - theorem congr_forall : (∀ x, p₁ x) ↔ (∀ x, p₂ x) := - forall_congr H - - theorem congr_exists : (∃ x, p₁ x) ↔ (∃ x, p₂ x) := - exists_congr H - - include H - theorem congr_exists_unique : (∃! x, p₁ x) ↔ (∃! x, p₂ x) := - congr_exists (λx, congr_and (H x) (congr_forall - (λy, congr_imp (H y) iff.rfl))) -end