refactor(library/algebra/relation, library/logic/instances): revise equivalence relations and congruences to use structure command
This commit is contained in:
Jeremy Avigad
Leonardo de Moura
parent
7571f50870
commit
bb8d436e75
7 changed files with 141 additions and 245 deletions
|
|
@ -132,7 +132,7 @@ namespace morphism
|
|||
theorem symm ⦃a b : ob⦄ (H : a ≅ b) : b ≅ a := mk (inverse (iso H))
|
||||
theorem trans ⦃a b c : ob⦄ (H1 : a ≅ b) (H2 : b ≅ c) : a ≅ c := mk (iso H2 ∘ iso H1)
|
||||
theorem is_equivalence_eq [instance] (T : Type) : is_equivalence isomorphic :=
|
||||
is_equivalence.mk (is_reflexive.mk refl) (is_symmetric.mk symm) (is_transitive.mk trans)
|
||||
is_equivalence.mk refl symm trans
|
||||
end isomorphic
|
||||
|
||||
inductive is_mono [class] (f : a ⟶ b) : Prop :=
|
||||
|
|
|
|||
|
|
@ -12,178 +12,113 @@ import logic.prop
|
|||
|
||||
namespace relation
|
||||
|
||||
section
|
||||
variables {T : Type} (R : T → T → Type)
|
||||
/- properties of binary relations -/
|
||||
|
||||
definition reflexive : Type := ∀x, R x x
|
||||
definition symmetric : Type := ∀⦃x y⦄, R x y → R y x
|
||||
definition transitive : Type := ∀⦃x y z⦄, R x y → R y z → R x z
|
||||
end
|
||||
section
|
||||
variables {T : Type} (R : T → T → Type)
|
||||
|
||||
inductive is_reflexive [class] {T : Type} (R : T → T → Type) : Prop :=
|
||||
mk : reflexive R → is_reflexive R
|
||||
|
||||
namespace is_reflexive
|
||||
|
||||
definition app ⦃T : Type⦄ {R : T → T → Prop} (C : is_reflexive R) : reflexive R :=
|
||||
is_reflexive.rec (λu, u) C
|
||||
|
||||
definition infer ⦃T : Type⦄ (R : T → T → Prop) [C : is_reflexive R] : reflexive R :=
|
||||
is_reflexive.rec (λu, u) C
|
||||
|
||||
end is_reflexive
|
||||
definition reflexive : Type := ∀x, R x x
|
||||
definition symmetric : Type := ∀⦃x y⦄, R x y → R y x
|
||||
definition transitive : Type := ∀⦃x y z⦄, R x y → R y z → R x z
|
||||
end
|
||||
|
||||
|
||||
inductive is_symmetric [class] {T : Type} (R : T → T → Type) : Prop :=
|
||||
mk : symmetric R → is_symmetric R
|
||||
/- classes for equivalence relations -/
|
||||
|
||||
namespace is_symmetric
|
||||
structure is_reflexive [class] {T : Type} (R : T → T → Type) := (refl : reflexive R)
|
||||
structure is_symmetric [class] {T : Type} (R : T → T → Type) := (symm : symmetric R)
|
||||
structure is_transitive [class] {T : Type} (R : T → T → Type) := (trans : transitive R)
|
||||
|
||||
definition app ⦃T : Type⦄ {R : T → T → Prop} (C : is_symmetric R) : symmetric R :=
|
||||
is_symmetric.rec (λu, u) C
|
||||
|
||||
definition infer ⦃T : Type⦄ (R : T → T → Prop) [C : is_symmetric R] : symmetric R :=
|
||||
is_symmetric.rec (λu, u) C
|
||||
|
||||
end is_symmetric
|
||||
|
||||
|
||||
inductive is_transitive [class] {T : Type} (R : T → T → Type) : Prop :=
|
||||
mk : transitive R → is_transitive R
|
||||
|
||||
namespace is_transitive
|
||||
|
||||
definition app ⦃T : Type⦄ {R : T → T → Prop} (C : is_transitive R) : transitive R :=
|
||||
is_transitive.rec (λu, u) C
|
||||
|
||||
definition infer ⦃T : Type⦄ (R : T → T → Prop) [C : is_transitive R] : transitive R :=
|
||||
is_transitive.rec (λu, u) C
|
||||
|
||||
end is_transitive
|
||||
|
||||
|
||||
inductive is_equivalence [class] {T : Type} (R : T → T → Type) : Prop :=
|
||||
mk : is_reflexive R → is_symmetric R → is_transitive R → is_equivalence R
|
||||
|
||||
theorem is_equivalence.is_reflexive [instance]
|
||||
{T : Type} (R : T → T → Type) {C : is_equivalence R} : is_reflexive R :=
|
||||
is_equivalence.rec (λx y z, x) C
|
||||
|
||||
theorem is_equivalence.is_symmetric [instance]
|
||||
{T : Type} {R : T → T → Type} {C : is_equivalence R} : is_symmetric R :=
|
||||
is_equivalence.rec (λx y z, y) C
|
||||
|
||||
theorem is_equivalence.is_transitive [instance]
|
||||
{T : Type} {R : T → T → Type} {C : is_equivalence R} : is_transitive R :=
|
||||
is_equivalence.rec (λx y z, z) C
|
||||
structure is_equivalence [class] {T : Type} (R : T → T → Type)
|
||||
extends is_reflexive R, is_symmetric R, is_transitive R
|
||||
|
||||
-- partial equivalence relation
|
||||
inductive is_PER {T : Type} (R : T → T → Type) : Prop :=
|
||||
mk : is_symmetric R → is_transitive R → is_PER R
|
||||
structure is_PER {T : Type} (R : T → T → Type) extends is_symmetric R, is_transitive R
|
||||
|
||||
theorem is_PER.is_symmetric [instance]
|
||||
{T : Type} {R : T → T → Type} {C : is_PER R} : is_symmetric R :=
|
||||
is_PER.rec (λx y, x) C
|
||||
-- Generic notation. For example, is_refl R is the reflexivity of R, if that can be
|
||||
-- inferred by type class inference
|
||||
section
|
||||
variables {T : Type} (R : T → T → Type)
|
||||
definition rel_refl [C : is_reflexive R] := is_reflexive.refl R
|
||||
definition rel_symm [C : is_symmetric R] := is_symmetric.symm R
|
||||
definition rel_trans [C : is_transitive R] := is_transitive.trans R
|
||||
end
|
||||
|
||||
theorem is_PER.is_transitive [instance]
|
||||
{T : Type} {R : T → T → Type} {C : is_PER R} : is_transitive R :=
|
||||
is_PER.rec (λx y, y) C
|
||||
|
||||
-- Congruence for unary and binary functions
|
||||
-- -----------------------------------------
|
||||
/- classes for unary and binary congruences with respect to arbitrary relations -/
|
||||
|
||||
inductive congruence [class] {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
|
||||
(f : T1 → T2) : Prop :=
|
||||
mk : (∀x y, R1 x y → R2 (f x) (f y)) → congruence R1 R2 f
|
||||
structure is_congruence [class]
|
||||
{T1 : Type} (R1 : T1 → T1 → Prop)
|
||||
{T2 : Type} (R2 : T2 → T2 → Prop)
|
||||
(f : T1 → T2) :=
|
||||
(congr : ∀{x y}, R1 x y → R2 (f x) (f y))
|
||||
|
||||
-- for binary functions
|
||||
inductive congruence2 [class] {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
|
||||
{T3 : Type} (R3 : T3 → T3 → Prop) (f : T1 → T2 → T3) : Prop :=
|
||||
mk : (∀(x1 y1 : T1) (x2 y2 : T2), R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2)) →
|
||||
congruence2 R1 R2 R3 f
|
||||
structure is_congruence2 [class]
|
||||
{T1 : Type} (R1 : T1 → T1 → Prop)
|
||||
{T2 : Type} (R2 : T2 → T2 → Prop)
|
||||
{T3 : Type} (R3 : T3 → T3 → Prop)
|
||||
(f : T1 → T2 → T3) :=
|
||||
(congr2 : ∀{x1 y1 : T1} {x2 y2 : T2}, R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2))
|
||||
|
||||
namespace congruence
|
||||
namespace is_congruence
|
||||
|
||||
-- makes the type class explicit
|
||||
definition app {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop}
|
||||
{f : T1 → T2} (C : congruence R1 R2 f) ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
|
||||
rec (λu, u) C x y
|
||||
|
||||
theorem infer {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
|
||||
(f : T1 → T2) [C : congruence R1 R2 f] ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
|
||||
rec (λu, u) C x y
|
||||
{f : T1 → T2} (C : is_congruence R1 R2 f) ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
|
||||
is_congruence.rec (λu, u) C x y
|
||||
|
||||
definition app2 {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop}
|
||||
{T3 : Type} {R3 : T3 → T3 → Prop}
|
||||
{f : T1 → T2 → T3} (C : congruence2 R1 R2 R3 f) ⦃x1 y1 : T1⦄ ⦃x2 y2 : T2⦄ :
|
||||
{f : T1 → T2 → T3} (C : is_congruence2 R1 R2 R3 f) ⦃x1 y1 : T1⦄ ⦃x2 y2 : T2⦄ :
|
||||
R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2) :=
|
||||
congruence2.rec (λu, u) C x1 y1 x2 y2
|
||||
is_congruence2.rec (λu, u) C x1 y1 x2 y2
|
||||
|
||||
-- ### general tools to build instances
|
||||
/- tools to build instances -/
|
||||
|
||||
theorem compose
|
||||
{T2 : Type} {R2 : T2 → T2 → Prop}
|
||||
{T3 : Type} {R3 : T3 → T3 → Prop}
|
||||
{g : T2 → T3} (C2 : congruence R2 R3 g)
|
||||
{g : T2 → T3} (C2 : is_congruence R2 R3 g)
|
||||
⦃T1 : Type⦄ {R1 : T1 → T1 → Prop}
|
||||
{f : T1 → T2} (C1 : congruence R1 R2 f) :
|
||||
congruence R1 R3 (λx, g (f x)) :=
|
||||
mk (λx1 x2 H, app C2 (app C1 H))
|
||||
{f : T1 → T2} (C1 : is_congruence R1 R2 f) :
|
||||
is_congruence R1 R3 (λx, g (f x)) :=
|
||||
is_congruence.mk (λx1 x2 H, app C2 (app C1 H))
|
||||
|
||||
theorem compose21
|
||||
{T2 : Type} {R2 : T2 → T2 → Prop}
|
||||
{T3 : Type} {R3 : T3 → T3 → Prop}
|
||||
{T4 : Type} {R4 : T4 → T4 → Prop}
|
||||
{g : T2 → T3 → T4} (C3 : congruence2 R2 R3 R4 g)
|
||||
{g : T2 → T3 → T4} (C3 : is_congruence2 R2 R3 R4 g)
|
||||
⦃T1 : Type⦄ {R1 : T1 → T1 → Prop}
|
||||
{f1 : T1 → T2} (C1 : congruence R1 R2 f1)
|
||||
{f2 : T1 → T3} (C2 : congruence R1 R3 f2) :
|
||||
congruence R1 R4 (λx, g (f1 x) (f2 x)) :=
|
||||
mk (λx1 x2 H, app2 C3 (app C1 H) (app C2 H))
|
||||
{f1 : T1 → T2} (C1 : is_congruence R1 R2 f1)
|
||||
{f2 : T1 → T3} (C2 : is_congruence R1 R3 f2) :
|
||||
is_congruence R1 R4 (λx, g (f1 x) (f2 x)) :=
|
||||
is_congruence.mk (λx1 x2 H, app2 C3 (app C1 H) (app C2 H))
|
||||
|
||||
theorem const {T2 : Type} (R2 : T2 → T2 → Prop) (H : relation.reflexive R2)
|
||||
⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) :
|
||||
congruence R1 R2 (λu : T1, c) :=
|
||||
mk (λx y H1, H c)
|
||||
is_congruence R1 R2 (λu : T1, c) :=
|
||||
is_congruence.mk (λx y H1, H c)
|
||||
|
||||
end congruence
|
||||
|
||||
-- Notice these can't be in the congruence namespace, if we want it visible without
|
||||
-- using congruence.
|
||||
end is_congruence
|
||||
|
||||
theorem congruence_const [instance] {T2 : Type} (R2 : T2 → T2 → Prop)
|
||||
[C : is_reflexive R2] ⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) :
|
||||
congruence R1 R2 (λu : T1, c) :=
|
||||
congruence.const R2 (is_reflexive.app C) R1 c
|
||||
is_congruence R1 R2 (λu : T1, c) :=
|
||||
is_congruence.const R2 (is_reflexive.refl R2) R1 c
|
||||
|
||||
theorem congruence_trivial [instance] {T : Type} (R : T → T → Prop) :
|
||||
congruence R R (λu, u) :=
|
||||
congruence.mk (λx y H, H)
|
||||
is_congruence R R (λu, u) :=
|
||||
is_congruence.mk (λx y H, H)
|
||||
|
||||
|
||||
-- Relations that can be coerced to functions / implications
|
||||
-- ---------------------------------------------------------
|
||||
/- relations that can be coerced to functions / implications-/
|
||||
|
||||
inductive mp_like [class] {R : Type → Type → Prop} {a b : Type} (H : R a b) : Type :=
|
||||
mk {} : (a → b) → mp_like H
|
||||
structure mp_like [class] (R : Type → Type → Type) :=
|
||||
(app : Π{a b : Type}, R a b → (a → b))
|
||||
|
||||
namespace mp_like
|
||||
definition rel_mp (R : Type → Type → Type) [C : mp_like R] {a b : Type} (H : R a b) :=
|
||||
mp_like.app H
|
||||
|
||||
definition app.{l} {R : Type → Type → Prop} {a : Type} {b : Type} {H : R a b}
|
||||
(C : mp_like H) : a → b := rec (λx, x) C
|
||||
|
||||
definition infer ⦃R : Type → Type → Prop⦄ {a : Type} {b : Type} (H : R a b)
|
||||
{C : mp_like H} : a → b := rec (λx, x) C
|
||||
|
||||
end mp_like
|
||||
|
||||
|
||||
-- Notation for operations on general symbols
|
||||
-- ------------------------------------------
|
||||
|
||||
-- e.g. if R is an instance of the class, then "refl R" is reflexivity for the class
|
||||
definition rel_refl := is_reflexive.infer
|
||||
definition rel_symm := is_symmetric.infer
|
||||
definition rel_trans := is_transitive.infer
|
||||
definition rel_mp := mp_like.infer
|
||||
|
||||
end relation
|
||||
|
|
|
|||
|
|
@ -47,10 +47,7 @@ have H3 : pr1 a + pr2 c + pr2 b = pr2 a + pr1 c + pr2 b, from
|
|||
show pr1 a + pr2 c = pr2 a + pr1 c, from add.cancel_right H3
|
||||
|
||||
theorem rel_equiv : is_equivalence rel :=
|
||||
is_equivalence.mk
|
||||
(is_reflexive.mk @rel_refl)
|
||||
(is_symmetric.mk @rel_symm)
|
||||
(is_transitive.mk @rel_trans)
|
||||
is_equivalence.mk @rel_refl @rel_symm @rel_trans
|
||||
|
||||
theorem rel_flip {a b : ℕ × ℕ} (H : rel a b) : rel (flip a) (flip b) :=
|
||||
calc
|
||||
|
|
|
|||
|
|
@ -21,14 +21,14 @@ definition prelim_map {A : Type} (R : A → A → Prop) (a : A) :=
|
|||
-- 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_reflexive.infer R,
|
||||
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_symmetric.infer R,
|
||||
have transR : relation.transitive R, from is_transitive.infer R,
|
||||
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
|
||||
|
|
|
|||
|
|
@ -1,9 +1,10 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura
|
||||
/-
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
-- logic.axioms.classical
|
||||
-- ======================
|
||||
Module: logic.axims.classical
|
||||
Author: Leonardo de Moura
|
||||
-/
|
||||
|
||||
import logic.quantifiers logic.cast algebra.relation
|
||||
|
||||
|
|
@ -49,8 +50,8 @@ propext
|
|||
(assume H, eq_to_iff H)
|
||||
|
||||
open relation
|
||||
theorem iff_congruence [instance] (P : Prop → Prop) : congruence iff iff P :=
|
||||
congruence.mk
|
||||
theorem iff_congruence [instance] (P : Prop → Prop) : is_congruence iff iff P :=
|
||||
is_congruence.mk
|
||||
(take (a b : Prop),
|
||||
assume H : a ↔ b,
|
||||
show P a ↔ P b, from eq_to_iff (iff_to_eq H ▸ eq.refl (P a)))
|
||||
|
|
|
|||
|
|
@ -1,47 +1,38 @@
|
|||
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
--- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
--- Author: Jeremy Avigad
|
||||
/-
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: logic.examples.instances_test
|
||||
Author: Jeremy Avigad
|
||||
|
||||
Illustrates substitution and congruence with iff.
|
||||
-/
|
||||
|
||||
import ..instances
|
||||
|
||||
open relation
|
||||
open relation.general_operations
|
||||
open relation.general_subst
|
||||
open relation.iff_ops
|
||||
open eq.ops
|
||||
|
||||
section
|
||||
example (a b : Prop) (H : a ↔ b) (H1 : a) : b := mp H H1
|
||||
|
||||
theorem test1 (a b : Prop) (H : a ↔ b) (H1 : a) : b := mp H H1
|
||||
|
||||
end
|
||||
|
||||
|
||||
section
|
||||
|
||||
theorem test2 (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
|
||||
example (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
|
||||
subst iff H1 H2
|
||||
|
||||
theorem test3 (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
|
||||
example (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
|
||||
H1 ▸ H2
|
||||
|
||||
end
|
||||
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
|
||||
|
||||
|
||||
theorem test4 (a b c d e : Prop) (H1 : a ↔ b) : (a ∨ c → ¬(d → a)) ↔ (b ∨ c → ¬(d → b)) :=
|
||||
congruence.infer iff iff (λa, (a ∨ c → ¬(d → a))) H1
|
||||
|
||||
|
||||
section
|
||||
|
||||
theorem test5 (T : Type) (a b c d : T) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
|
||||
example (T : Type) (a b c d : T) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
|
||||
H1 ⬝ H2⁻¹ ⬝ H3
|
||||
|
||||
theorem test6 (a b c d : Prop) (H1 : a ↔ b) (H2 : c ↔ b) (H3 : c ↔ d) : a ↔ d :=
|
||||
example (a b c d : Prop) (H1 : a ↔ b) (H2 : c ↔ b) (H3 : c ↔ d) : a ↔ d :=
|
||||
H1 ⬝ (H2⁻¹ ⬝ H3)
|
||||
|
||||
theorem test7 (T : Type) (a b c d : T) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
|
||||
example (T : Type) (a b c d : T) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
|
||||
H1 ⬝ H2⁻¹ ⬝ H3
|
||||
|
||||
theorem test8 (a b c d : Prop) (H1 : a ↔ b) (H2 : c ↔ b) (H3 : c ↔ d) : a ↔ d :=
|
||||
example (a b c d : Prop) (H1 : a ↔ b) (H2 : c ↔ b) (H3 : c ↔ d) : a ↔ d :=
|
||||
H1 ⬝ H2⁻¹ ⬝ H3
|
||||
end
|
||||
|
|
|
|||
|
|
@ -1,126 +1,97 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Jeremy Avigad
|
||||
/-
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
-- logic.instances
|
||||
-- ====================
|
||||
Module: logic.instances
|
||||
Author: Jeremy Avigad
|
||||
|
||||
Class instances for iff and eq.
|
||||
-/
|
||||
|
||||
import logic.connectives algebra.relation
|
||||
|
||||
namespace relation
|
||||
|
||||
open relation
|
||||
/- logical equivalence relations -/
|
||||
|
||||
-- Congruences for logic
|
||||
-- ---------------------
|
||||
theorem is_equivalence_eq [instance] (T : Type) : relation.is_equivalence (@eq T) :=
|
||||
relation.is_equivalence.mk (@eq.refl T) (@eq.symm T) (@eq.trans T)
|
||||
|
||||
theorem congruence_not : congruence iff iff not :=
|
||||
congruence.mk
|
||||
theorem is_equivalence_iff [instance] : relation.is_equivalence iff :=
|
||||
relation.is_equivalence.mk @iff.refl @iff.symm @iff.trans
|
||||
|
||||
|
||||
/- congruences for logic operations -/
|
||||
|
||||
theorem is_congruence_not : is_congruence iff iff not :=
|
||||
is_congruence.mk
|
||||
(take a b,
|
||||
assume H : a ↔ b, iff.intro
|
||||
(assume H1 : ¬a, assume H2 : b, H1 (iff.elim_right H H2))
|
||||
(assume H1 : ¬b, assume H2 : a, H1 (iff.elim_left H H2)))
|
||||
|
||||
theorem congruence_and : congruence2 iff iff iff and :=
|
||||
congruence2.mk
|
||||
theorem is_congruence_and : is_congruence2 iff iff iff and :=
|
||||
is_congruence2.mk
|
||||
(take a1 b1 a2 b2,
|
||||
assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2,
|
||||
iff.intro
|
||||
(assume H3 : a1 ∧ a2, and.imp_and H3 (iff.elim_left H1) (iff.elim_left H2))
|
||||
(assume H3 : b1 ∧ b2, and.imp_and H3 (iff.elim_right H1) (iff.elim_right H2)))
|
||||
|
||||
theorem congruence_or : congruence2 iff iff iff or :=
|
||||
congruence2.mk
|
||||
theorem is_congruence_or : is_congruence2 iff iff iff or :=
|
||||
is_congruence2.mk
|
||||
(take a1 b1 a2 b2,
|
||||
assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2,
|
||||
iff.intro
|
||||
(assume H3 : a1 ∨ a2, or.imp_or H3 (iff.elim_left H1) (iff.elim_left H2))
|
||||
(assume H3 : b1 ∨ b2, or.imp_or H3 (iff.elim_right H1) (iff.elim_right H2)))
|
||||
|
||||
theorem congruence_imp : congruence2 iff iff iff imp :=
|
||||
congruence2.mk
|
||||
theorem is_congruence_imp : is_congruence2 iff iff iff imp :=
|
||||
is_congruence2.mk
|
||||
(take a1 b1 a2 b2,
|
||||
assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2,
|
||||
iff.intro
|
||||
(assume H3 : a1 → a2, assume Hb1 : b1, iff.elim_left H2 (H3 ((iff.elim_right H1) Hb1)))
|
||||
(assume H3 : b1 → b2, assume Ha1 : a1, iff.elim_right H2 (H3 ((iff.elim_left H1) Ha1))))
|
||||
|
||||
theorem congruence_iff : congruence2 iff iff iff iff :=
|
||||
congruence2.mk
|
||||
theorem is_congruence_iff : is_congruence2 iff iff iff iff :=
|
||||
is_congruence2.mk
|
||||
(take a1 b1 a2 b2,
|
||||
assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2,
|
||||
iff.intro
|
||||
(assume H3 : a1 ↔ a2, iff.trans (iff.symm H1) (iff.trans H3 H2))
|
||||
(assume H3 : b1 ↔ b2, iff.trans H1 (iff.trans H3 (iff.symm H2))))
|
||||
|
||||
-- theorem congruence_const_iff [instance] := congruence.const iff iff.refl
|
||||
definition congruence_not_compose [instance] := congruence.compose congruence_not
|
||||
definition congruence_and_compose [instance] := congruence.compose21 congruence_and
|
||||
definition congruence_or_compose [instance] := congruence.compose21 congruence_or
|
||||
definition congruence_implies_compose [instance] := congruence.compose21 congruence_imp
|
||||
definition congruence_iff_compose [instance] := congruence.compose21 congruence_iff
|
||||
|
||||
-- Generalized substitution
|
||||
-- ------------------------
|
||||
|
||||
-- TODO: note that the target has to be "iff". Otherwise, there is not enough
|
||||
-- information to infer an mp-like relation.
|
||||
|
||||
namespace general_operations
|
||||
|
||||
theorem subst {T : Type} (R : T → T → Prop) ⦃P : T → Prop⦄ [C : congruence R iff P]
|
||||
{a b : T} (H : R a b) (H1 : P a) : P b := iff.elim_left (congruence.app C H) H1
|
||||
|
||||
end general_operations
|
||||
|
||||
-- = is an equivalence relation
|
||||
-- ----------------------------
|
||||
|
||||
theorem is_reflexive_eq [instance] (T : Type) : relation.is_reflexive (@eq T) :=
|
||||
relation.is_reflexive.mk (@eq.refl T)
|
||||
|
||||
theorem is_symmetric_eq [instance] (T : Type) : relation.is_symmetric (@eq T) :=
|
||||
relation.is_symmetric.mk (@eq.symm T)
|
||||
|
||||
theorem is_transitive_eq [instance] (T : Type) : relation.is_transitive (@eq T) :=
|
||||
relation.is_transitive.mk (@eq.trans T)
|
||||
|
||||
-- TODO: this is only temporary, needed to inform Lean that is_equivalence is a class
|
||||
theorem is_equivalence_eq [instance] (T : Type) : relation.is_equivalence (@eq T) :=
|
||||
relation.is_equivalence.mk _ _ _
|
||||
-- theorem is_congruence_const_iff [instance] := is_congruence.const iff iff.refl
|
||||
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
|
||||
|
||||
|
||||
-- iff is an equivalence relation
|
||||
-- ------------------------------
|
||||
/- a general substitution operation with respect to an arbitrary congruence -/
|
||||
|
||||
theorem is_reflexive_iff [instance] : relation.is_reflexive iff :=
|
||||
relation.is_reflexive.mk (@iff.refl)
|
||||
|
||||
theorem is_symmetric_iff [instance] : relation.is_symmetric iff :=
|
||||
relation.is_symmetric.mk (@iff.symm)
|
||||
|
||||
theorem is_transitive_iff [instance] : relation.is_transitive iff :=
|
||||
relation.is_transitive.mk (@iff.trans)
|
||||
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
|
||||
|
||||
|
||||
-- Mp-like for iff
|
||||
-- ---------------
|
||||
/- iff can be coerced to implication -/
|
||||
|
||||
theorem mp_like_iff [instance] (a b : Prop) (H : a ↔ b) : @relation.mp_like iff a b H :=
|
||||
relation.mp_like.mk (iff.elim_left H)
|
||||
definition mp_like_iff [instance] : relation.mp_like iff :=
|
||||
relation.mp_like.mk (λa b (H : a ↔ b), iff.elim_left H)
|
||||
|
||||
|
||||
-- Substition for iff
|
||||
-- ------------------
|
||||
/- support for calculations with iff -/
|
||||
|
||||
namespace iff
|
||||
theorem subst {P : Prop → Prop} [C : congruence iff iff P] {a b : Prop} (H : a ↔ b) (H1 : P a) :
|
||||
P b :=
|
||||
@general_operations.subst Prop iff P C a b H H1
|
||||
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
|
||||
|
||||
-- Support for calculations with iff
|
||||
-- ----------------
|
||||
|
||||
calc_subst iff.subst
|
||||
|
||||
namespace iff_ops
|
||||
|
|
@ -133,4 +104,5 @@ namespace iff_ops
|
|||
definition subst := @iff.subst
|
||||
definition mp := @iff.mp
|
||||
end iff_ops
|
||||
|
||||
end relation
|
||||
|
|
|
|||
Loading…
Reference in a new issue