2014-08-05 00:07:59 +00:00
|
|
|
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
|
|
|
-- Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
-- Author: Jeremy Avigad
|
|
|
|
|
2014-09-16 18:58:54 +00:00
|
|
|
-- algebra.relation
|
2014-08-30 03:54:28 +00:00
|
|
|
-- ==============
|
|
|
|
|
2014-10-05 17:50:13 +00:00
|
|
|
import logic.prop
|
2014-08-05 00:07:59 +00:00
|
|
|
|
2014-08-20 02:32:44 +00:00
|
|
|
|
2014-08-05 00:07:59 +00:00
|
|
|
-- General properties of relations
|
|
|
|
-- -------------------------------
|
|
|
|
|
|
|
|
namespace relation
|
|
|
|
|
2014-09-17 21:39:05 +00:00
|
|
|
definition reflexive {T : Type} (R : T → T → Type) : Type := ∀x, R x x
|
|
|
|
definition symmetric {T : Type} (R : T → T → Type) : Type := ∀⦃x y⦄, R x y → R y x
|
|
|
|
definition transitive {T : Type} (R : T → T → Type) : Type := ∀⦃x y z⦄, R x y → R y z → R x z
|
2014-08-05 00:07:59 +00:00
|
|
|
|
|
|
|
|
2014-10-08 01:02:15 +00:00
|
|
|
inductive is_reflexive [class] {T : Type} (R : T → T → Type) : Prop :=
|
2014-09-04 23:36:06 +00:00
|
|
|
mk : reflexive R → is_reflexive R
|
2014-08-20 02:32:44 +00:00
|
|
|
|
|
|
|
namespace is_reflexive
|
2014-08-05 00:07:59 +00:00
|
|
|
|
2014-10-09 21:43:07 +00:00
|
|
|
definition app ⦃T : Type⦄ {R : T → T → Prop} (C : is_reflexive R) : reflexive R :=
|
2014-09-04 22:03:59 +00:00
|
|
|
is_reflexive.rec (λu, u) C
|
2014-08-05 00:07:59 +00:00
|
|
|
|
2014-10-12 20:06:00 +00:00
|
|
|
definition infer ⦃T : Type⦄ (R : T → T → Prop) [C : is_reflexive R] : reflexive R :=
|
2014-09-04 22:03:59 +00:00
|
|
|
is_reflexive.rec (λu, u) C
|
2014-08-05 00:07:59 +00:00
|
|
|
|
2014-08-12 00:35:25 +00:00
|
|
|
end is_reflexive
|
2014-08-05 00:07:59 +00:00
|
|
|
|
|
|
|
|
2014-10-08 01:02:15 +00:00
|
|
|
inductive is_symmetric [class] {T : Type} (R : T → T → Type) : Prop :=
|
2014-09-04 23:36:06 +00:00
|
|
|
mk : symmetric R → is_symmetric R
|
2014-08-20 02:32:44 +00:00
|
|
|
|
|
|
|
namespace is_symmetric
|
2014-08-05 00:07:59 +00:00
|
|
|
|
2014-10-09 21:43:07 +00:00
|
|
|
definition app ⦃T : Type⦄ {R : T → T → Prop} (C : is_symmetric R) : symmetric R :=
|
2014-09-04 22:03:59 +00:00
|
|
|
is_symmetric.rec (λu, u) C
|
2014-08-05 00:07:59 +00:00
|
|
|
|
2014-10-12 20:06:00 +00:00
|
|
|
definition infer ⦃T : Type⦄ (R : T → T → Prop) [C : is_symmetric R] : symmetric R :=
|
2014-09-04 22:03:59 +00:00
|
|
|
is_symmetric.rec (λu, u) C
|
2014-08-05 00:07:59 +00:00
|
|
|
|
2014-08-12 00:35:25 +00:00
|
|
|
end is_symmetric
|
2014-08-05 00:07:59 +00:00
|
|
|
|
|
|
|
|
2014-10-08 01:02:15 +00:00
|
|
|
inductive is_transitive [class] {T : Type} (R : T → T → Type) : Prop :=
|
2014-09-04 23:36:06 +00:00
|
|
|
mk : transitive R → is_transitive R
|
2014-08-05 00:07:59 +00:00
|
|
|
|
2014-08-20 02:32:44 +00:00
|
|
|
namespace is_transitive
|
|
|
|
|
2014-10-09 21:43:07 +00:00
|
|
|
definition app ⦃T : Type⦄ {R : T → T → Prop} (C : is_transitive R) : transitive R :=
|
2014-09-04 22:03:59 +00:00
|
|
|
is_transitive.rec (λu, u) C
|
2014-08-05 00:07:59 +00:00
|
|
|
|
2014-10-12 20:06:00 +00:00
|
|
|
definition infer ⦃T : Type⦄ (R : T → T → Prop) [C : is_transitive R] : transitive R :=
|
2014-09-04 22:03:59 +00:00
|
|
|
is_transitive.rec (λu, u) C
|
2014-08-05 00:07:59 +00:00
|
|
|
|
2014-08-12 00:35:25 +00:00
|
|
|
end is_transitive
|
2014-08-05 00:07:59 +00:00
|
|
|
|
2014-08-17 21:41:23 +00:00
|
|
|
|
2014-10-08 01:02:15 +00:00
|
|
|
inductive is_equivalence [class] {T : Type} (R : T → T → Type) : Prop :=
|
2014-09-04 23:36:06 +00:00
|
|
|
mk : is_reflexive R → is_symmetric R → is_transitive R → is_equivalence R
|
2014-08-17 21:41:23 +00:00
|
|
|
|
2014-09-19 19:42:22 +00:00
|
|
|
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
|
2014-08-17 21:41:23 +00:00
|
|
|
|
2014-09-19 19:42:22 +00:00
|
|
|
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
|
2014-08-17 21:41:23 +00:00
|
|
|
|
2014-09-19 19:42:22 +00:00
|
|
|
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
|
2014-08-17 21:41:23 +00:00
|
|
|
|
2014-08-20 02:32:44 +00:00
|
|
|
-- partial equivalence relation
|
|
|
|
inductive is_PER {T : Type} (R : T → T → Type) : Prop :=
|
2014-09-04 23:36:06 +00:00
|
|
|
mk : is_symmetric R → is_transitive R → is_PER R
|
2014-08-20 02:32:44 +00:00
|
|
|
|
2014-09-19 19:42:22 +00:00
|
|
|
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
|
2014-08-17 21:41:23 +00:00
|
|
|
|
2014-09-19 19:42:22 +00:00
|
|
|
theorem is_PER.is_transitive [instance]
|
|
|
|
{T : Type} {R : T → T → Type} {C : is_PER R} : is_transitive R :=
|
2014-09-04 22:03:59 +00:00
|
|
|
is_PER.rec (λx y, y) C
|
2014-08-17 21:41:23 +00:00
|
|
|
|
2014-08-05 00:07:59 +00:00
|
|
|
-- Congruence for unary and binary functions
|
|
|
|
-- -----------------------------------------
|
|
|
|
|
2014-10-08 01:02:15 +00:00
|
|
|
inductive congruence [class] {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
|
2014-08-05 00:07:59 +00:00
|
|
|
(f : T1 → T2) : Prop :=
|
2014-09-04 23:36:06 +00:00
|
|
|
mk : (∀x y, R1 x y → R2 (f x) (f y)) → congruence R1 R2 f
|
2014-08-05 00:07:59 +00:00
|
|
|
|
|
|
|
-- for binary functions
|
2014-10-08 01:02:15 +00:00
|
|
|
inductive congruence2 [class] {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
|
2014-08-05 00:07:59 +00:00
|
|
|
{T3 : Type} (R3 : T3 → T3 → Prop) (f : T1 → T2 → T3) : Prop :=
|
2014-09-04 23:36:06 +00:00
|
|
|
mk : (∀(x1 y1 : T1) (x2 y2 : T2), R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2)) →
|
2014-08-30 03:54:28 +00:00
|
|
|
congruence2 R1 R2 R3 f
|
2014-08-05 00:07:59 +00:00
|
|
|
|
2014-08-30 03:54:28 +00:00
|
|
|
namespace congruence
|
2014-08-05 00:07:59 +00:00
|
|
|
|
2014-09-17 21:39:05 +00:00
|
|
|
definition app {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop}
|
2014-08-30 03:54:28 +00:00
|
|
|
{f : T1 → T2} (C : congruence R1 R2 f) ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
|
2014-09-04 23:36:06 +00:00
|
|
|
rec (λu, u) C x y
|
2014-08-05 00:07:59 +00:00
|
|
|
|
2014-08-20 02:32:44 +00:00
|
|
|
theorem infer {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
|
2014-10-12 20:06:00 +00:00
|
|
|
(f : T1 → T2) [C : congruence R1 R2 f] ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
|
2014-09-04 23:36:06 +00:00
|
|
|
rec (λu, u) C x y
|
2014-08-05 00:07:59 +00:00
|
|
|
|
2014-09-17 21:39:05 +00:00
|
|
|
definition app2 {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop}
|
2014-08-20 02:32:44 +00:00
|
|
|
{T3 : Type} {R3 : T3 → T3 → Prop}
|
2014-08-30 03:54:28 +00:00
|
|
|
{f : T1 → T2 → T3} (C : congruence2 R1 R2 R3 f) ⦃x1 y1 : T1⦄ ⦃x2 y2 : T2⦄ :
|
2014-08-20 02:32:44 +00:00
|
|
|
R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2) :=
|
2014-09-04 22:03:59 +00:00
|
|
|
congruence2.rec (λu, u) C x1 y1 x2 y2
|
2014-08-05 00:07:59 +00:00
|
|
|
|
2014-08-20 02:32:44 +00:00
|
|
|
-- ### general tools to build instances
|
2014-08-05 00:07:59 +00:00
|
|
|
|
2014-08-20 02:32:44 +00:00
|
|
|
theorem compose
|
|
|
|
{T2 : Type} {R2 : T2 → T2 → Prop}
|
|
|
|
{T3 : Type} {R3 : T3 → T3 → Prop}
|
2014-08-30 03:54:28 +00:00
|
|
|
{g : T2 → T3} (C2 : congruence R2 R3 g)
|
2014-08-20 02:32:44 +00:00
|
|
|
⦃T1 : Type⦄ {R1 : T1 → T1 → Prop}
|
2014-08-30 03:54:28 +00:00
|
|
|
{f : T1 → T2} (C1 : congruence R1 R2 f) :
|
|
|
|
congruence R1 R3 (λx, g (f x)) :=
|
2014-09-04 23:36:06 +00:00
|
|
|
mk (λx1 x2 H, app C2 (app C1 H))
|
2014-08-20 02:32:44 +00:00
|
|
|
|
|
|
|
theorem compose21
|
|
|
|
{T2 : Type} {R2 : T2 → T2 → Prop}
|
|
|
|
{T3 : Type} {R3 : T3 → T3 → Prop}
|
|
|
|
{T4 : Type} {R4 : T4 → T4 → Prop}
|
2014-08-30 03:54:28 +00:00
|
|
|
{g : T2 → T3 → T4} (C3 : congruence2 R2 R3 R4 g)
|
2014-08-20 02:32:44 +00:00
|
|
|
⦃T1 : Type⦄ {R1 : T1 → T1 → Prop}
|
2014-08-30 03:54:28 +00:00
|
|
|
{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)) :=
|
2014-09-04 23:36:06 +00:00
|
|
|
mk (λx1 x2 H, app2 C3 (app C1 H) (app C2 H))
|
2014-08-20 02:32:44 +00:00
|
|
|
|
|
|
|
theorem const {T2 : Type} (R2 : T2 → T2 → Prop) (H : relation.reflexive R2)
|
|
|
|
⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) :
|
2014-08-30 03:54:28 +00:00
|
|
|
congruence R1 R2 (λu : T1, c) :=
|
2014-09-04 23:36:06 +00:00
|
|
|
mk (λx y H1, H c)
|
2014-08-20 02:32:44 +00:00
|
|
|
|
2014-08-30 03:54:28 +00:00
|
|
|
end congruence
|
2014-08-05 00:07:59 +00:00
|
|
|
|
2014-08-30 03:54:28 +00:00
|
|
|
-- Notice these can't be in the congruence namespace, if we want it visible without
|
|
|
|
-- using congruence.
|
2014-08-05 00:07:59 +00:00
|
|
|
|
2014-08-30 03:54:28 +00:00
|
|
|
theorem congruence_const [instance] {T2 : Type} (R2 : T2 → T2 → Prop)
|
2014-10-12 20:06:00 +00:00
|
|
|
[C : is_reflexive R2] ⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) :
|
2014-08-30 03:54:28 +00:00
|
|
|
congruence R1 R2 (λu : T1, c) :=
|
|
|
|
congruence.const R2 (is_reflexive.app C) R1 c
|
2014-08-05 00:07:59 +00:00
|
|
|
|
2014-08-30 03:54:28 +00:00
|
|
|
theorem congruence_trivial [instance] {T : Type} (R : T → T → Prop) :
|
|
|
|
congruence R R (λu, u) :=
|
2014-09-04 23:36:06 +00:00
|
|
|
congruence.mk (λx y H, H)
|
2014-08-05 00:07:59 +00:00
|
|
|
|
|
|
|
|
|
|
|
-- Relations that can be coerced to functions / implications
|
|
|
|
-- ---------------------------------------------------------
|
|
|
|
|
2014-10-08 01:02:15 +00:00
|
|
|
inductive mp_like [class] {R : Type → Type → Prop} {a b : Type} (H : R a b) : Type :=
|
2014-09-04 23:36:06 +00:00
|
|
|
mk {} : (a → b) → @mp_like R a b H
|
2014-08-05 00:07:59 +00:00
|
|
|
|
|
|
|
namespace mp_like
|
|
|
|
|
2014-09-29 15:18:10 +00:00
|
|
|
definition app.{l} {R : Type → Type → Prop} {a : Type} {b : Type} {H : R a b}
|
2014-09-04 23:36:06 +00:00
|
|
|
(C : mp_like H) : a → b := rec (λx, x) C
|
2014-08-05 00:07:59 +00:00
|
|
|
|
2014-08-20 02:32:44 +00:00
|
|
|
definition infer ⦃R : Type → Type → Prop⦄ {a : Type} {b : Type} (H : R a b)
|
2014-09-04 23:36:06 +00:00
|
|
|
{C : mp_like H} : a → b := rec (λx, x) C
|
2014-08-05 00:07:59 +00:00
|
|
|
|
2014-08-12 00:35:25 +00:00
|
|
|
end mp_like
|
2014-08-05 00:07:59 +00:00
|
|
|
|
|
|
|
|
|
|
|
-- Notation for operations on general symbols
|
|
|
|
-- ------------------------------------------
|
|
|
|
|
2014-08-20 02:32:44 +00:00
|
|
|
-- e.g. if R is an instance of the class, then "refl R" is reflexivity for the class
|
2014-08-20 22:49:44 +00:00
|
|
|
definition rel_refl := is_reflexive.infer
|
|
|
|
definition rel_symm := is_symmetric.infer
|
|
|
|
definition rel_trans := is_transitive.infer
|
|
|
|
definition rel_mp := mp_like.infer
|
2014-08-05 00:07:59 +00:00
|
|
|
|
2014-08-12 00:35:25 +00:00
|
|
|
end relation
|