refactor(library): move basic simp/congr rules to init folder, delete some legacy files
This commit is contained in:
Leonardo de Moura
parent
eb3d73873a
commit
5a98a2538c
20 changed files with 191 additions and 845 deletions
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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])
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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.
|
||||
|
|
@ -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
|
||||
|
|
@ -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)
|
||||
|
||||
|
|
|
|||
|
|
@ -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 :=
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
-/
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in a new issue