394e0d5f0a
Now, `cmp` is just a fixed helper function. In the future, we will be able to use (more efficient) specialized versions during code generation by defining simp rules.
222 lines
8.5 KiB
Text
222 lines
8.5 KiB
Text
/-
|
||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Leonardo de Moura
|
||
-/
|
||
prelude
|
||
import init.logic init.data.ordering.basic
|
||
universes u
|
||
|
||
@[algebra] class is_commutative (α : Type u) (op : α → α → α) : Prop :=
|
||
(comm : ∀ a b, op a b = op b a)
|
||
|
||
@[algebra] class is_associative (α : Type u) (op : α → α → α) : Prop :=
|
||
(assoc : ∀ a b c, op (op a b) c = op a (op b c))
|
||
|
||
@[algebra] class is_left_id (α : Type u) (op : α → α → α) (o : inout α) : Prop :=
|
||
(left_id : ∀ a, op o a = a)
|
||
|
||
@[algebra] class is_right_id (α : Type u) (op : α → α → α) (o : inout α) : Prop :=
|
||
(right_id : ∀ a, op a o = a)
|
||
|
||
@[algebra] class is_left_null (α : Type u) (op : α → α → α) (o : inout α) : Prop :=
|
||
(left_null : ∀ a, op o a = o)
|
||
|
||
@[algebra] class is_right_null (α : Type u) (op : α → α → α) (o : inout α) : Prop :=
|
||
(right_null : ∀ a, op a o = o)
|
||
|
||
@[algebra] class is_left_cancel (α : Type u) (op : α → α → α) : Prop :=
|
||
(left_cancel : ∀ a b c, op a b = op a c → b = c)
|
||
|
||
@[algebra] class is_right_cancel (α : Type u) (op : α → α → α) : Prop :=
|
||
(right_cancel : ∀ a b c, op a b = op c b → a = c)
|
||
|
||
@[algebra] class is_idempotent (α : Type u) (op : α → α → α) : Prop :=
|
||
(idempotent : ∀ a, op a a = a)
|
||
|
||
@[algebra] class is_left_distrib (α : Type u) (op₁ : α → α → α) (op₂ : inout α → α → α) : Prop :=
|
||
(left_distrib : ∀ a b c, op₁ a (op₂ b c) = op₂ (op₁ a b) (op₁ a c))
|
||
|
||
@[algebra] class is_right_distrib (α : Type u) (op₁ : α → α → α) (op₂ : inout α → α → α) : Prop :=
|
||
(right_distrib : ∀ a b c, op₁ (op₂ a b) c = op₂ (op₁ a c) (op₁ b c))
|
||
|
||
@[algebra] class is_left_inv (α : Type u) (op : α → α → α) (inv : inout α → α) (o : inout α) : Prop :=
|
||
(left_inv : ∀ a, op (inv a) a = o)
|
||
|
||
@[algebra] class is_right_inv (α : Type u) (op : α → α → α) (inv : inout α → α) (o : inout α) : Prop :=
|
||
(right_inv : ∀ a, op a (inv a) = o)
|
||
|
||
@[algebra] class is_cond_left_inv (α : Type u) (op : α → α → α) (inv : inout α → α) (o : inout α) (p : inout α → Prop) : Prop :=
|
||
(left_inv : ∀ a, p a → op (inv a) a = o)
|
||
|
||
@[algebra] class is_cond_right_inv (α : Type u) (op : α → α → α) (inv : inout α → α) (o : inout α) (p : inout α → Prop) : Prop :=
|
||
(right_inv : ∀ a, p a → op a (inv a) = o)
|
||
|
||
@[algebra] class is_distinct (α : Type u) (a : α) (b : α) : Prop :=
|
||
(distinct : a ≠ b)
|
||
|
||
/-
|
||
-- The following type class doesn't seem very useful, a regular simp lemma should work for this.
|
||
class is_inv (α : Type u) (β : Type v) (f : α → β) (g : inout β → α) : Prop :=
|
||
(inv : ∀ a, g (f a) = a)
|
||
|
||
-- The following one can also be handled using a regular simp lemma
|
||
class is_idempotent (α : Type u) (f : α → α) : Prop :=
|
||
(idempotent : ∀ a, f (f a) = f a)
|
||
-/
|
||
|
||
@[algebra] class is_irrefl (α : Type u) (r : α → α → Prop) : Prop :=
|
||
(irrefl : ∀ a, ¬ r a a)
|
||
|
||
@[algebra] class is_refl (α : Type u) (r : α → α → Prop) : Prop :=
|
||
(refl : ∀ a, r a a)
|
||
|
||
@[algebra] class is_symm (α : Type u) (r : α → α → Prop) : Prop :=
|
||
(symm : ∀ a b, r a b → r b a)
|
||
|
||
@[algebra] class is_asymm (α : Type u) (r : α → α → Prop) : Prop :=
|
||
(asymm : ∀ a b, r a b → ¬ r b a)
|
||
|
||
@[algebra] class is_antisymm (α : Type u) (r : α → α → Prop) : Prop :=
|
||
(antisymm : ∀ a b, r a b → r b a → a = b)
|
||
|
||
@[algebra] class is_trans (α : Type u) (r : α → α → Prop) : Prop :=
|
||
(trans : ∀ a b c, r a b → r b c → r a c)
|
||
|
||
@[algebra] class is_total (α : Type u) (r : α → α → Prop) : Prop :=
|
||
(total : ∀ a b, r a b ∨ r b a)
|
||
|
||
@[algebra] class is_preorder (α : Type u) (r : α → α → Prop) extends is_refl α r, is_trans α r : Prop.
|
||
|
||
@[algebra] class is_total_preorder (α : Type u) (r : α → α → Prop) extends is_trans α r, is_total α r : Prop.
|
||
|
||
instance is_total_preorder_is_preorder (α : Type u) (r : α → α → Prop) [s : is_total_preorder α r] : is_preorder α r :=
|
||
{trans := s.trans,
|
||
refl := λ a, or.elim (is_total.total r a a) id id}
|
||
|
||
@[algebra] class is_partial_order (α : Type u) (r : α → α → Prop) extends is_preorder α r, is_antisymm α r : Prop.
|
||
|
||
@[algebra] class is_linear_order (α : Type u) (r : α → α → Prop) extends is_partial_order α r, is_total α r : Prop.
|
||
|
||
@[algebra] class is_equiv (α : Type u) (r : α → α → Prop) extends is_preorder α r, is_symm α r : Prop.
|
||
|
||
@[algebra] class is_per (α : Type u) (r : α → α → Prop) extends is_symm α r, is_trans α r : Prop.
|
||
|
||
@[algebra] class is_strict_order (α : Type u) (r : α → α → Prop) extends is_irrefl α r, is_trans α r : Prop.
|
||
|
||
@[algebra] class is_strict_weak_order (α : Type u) (lt : α → α → Prop) extends is_strict_order α lt : Prop :=
|
||
(incomp_trans : ∀ a b c, (¬ lt a b ∧ ¬ lt b a) → (¬ lt b c ∧ ¬ lt c b) → (¬ lt a c ∧ ¬ lt c a))
|
||
|
||
instance eq_is_equiv (α : Type u) : is_equiv α (=) :=
|
||
{symm := @eq.symm _, trans := @eq.trans _, refl := eq.refl}
|
||
|
||
section
|
||
variables {α : Type u} {r : α → α → Prop}
|
||
local infix `≺`:50 := r
|
||
|
||
lemma irrefl [is_irrefl α r] (a : α) : ¬ a ≺ a :=
|
||
is_irrefl.irrefl _ a
|
||
|
||
lemma refl [is_refl α r] (a : α) : a ≺ a :=
|
||
is_refl.refl _ a
|
||
|
||
lemma trans [is_trans α r] {a b c : α} : a ≺ b → b ≺ c → a ≺ c :=
|
||
is_trans.trans _ _ _
|
||
|
||
lemma symm [is_symm α r] {a b : α} : a ≺ b → b ≺ a :=
|
||
is_symm.symm _ _
|
||
|
||
lemma antisymm [is_antisymm α r] {a b : α} : a ≺ b → b ≺ a → a = b :=
|
||
is_antisymm.antisymm _ _
|
||
|
||
lemma asymm [is_asymm α r] {a b : α} : a ≺ b → ¬ b ≺ a :=
|
||
is_asymm.asymm _ _
|
||
|
||
instance is_asymm_of_is_trans_of_is_irrefl [is_trans α r] [is_irrefl α r] : is_asymm α r :=
|
||
⟨λ a b h₁ h₂, absurd (trans h₁ h₂) (irrefl a)⟩
|
||
|
||
section explicit_relation_variants
|
||
variable (r)
|
||
|
||
@[elab_simple]
|
||
lemma irrefl_of [is_irrefl α r] (a : α) : ¬ a ≺ a := irrefl a
|
||
|
||
@[elab_simple]
|
||
lemma refl_of [is_refl α r] (a : α) : a ≺ a := refl a
|
||
|
||
@[elab_simple]
|
||
lemma trans_of [is_trans α r] {a b c : α} : a ≺ b → b ≺ c → a ≺ c := trans
|
||
|
||
@[elab_simple]
|
||
lemma symm_of [is_symm α r] {a b : α} : a ≺ b → b ≺ a := symm
|
||
|
||
@[elab_simple]
|
||
lemma asymm_of [is_asymm α r] {a b : α} : a ≺ b → ¬ b ≺ a := asymm
|
||
|
||
@[elab_simple]
|
||
lemma total_of [is_total α r] (a b : α) : a ≺ b ∨ b ≺ a :=
|
||
is_total.total _ _ _
|
||
|
||
end explicit_relation_variants
|
||
|
||
end
|
||
|
||
namespace strict_weak_order
|
||
section
|
||
parameters {α : Type u} {r : α → α → Prop} [is_strict_weak_order α r]
|
||
local infix `≺`:50 := r
|
||
|
||
def equiv (a b : α) : Prop :=
|
||
¬ a ≺ b ∧ ¬ b ≺ a
|
||
|
||
local infix ` ≈ `:50 := equiv
|
||
|
||
lemma erefl (a : α) : a ≈ a :=
|
||
⟨irrefl a, irrefl a⟩
|
||
|
||
lemma esymm {a b : α} : a ≈ b → b ≈ a :=
|
||
λ ⟨h₁, h₂⟩, ⟨h₂, h₁⟩
|
||
|
||
lemma etrans {a b c : α} : a ≈ b → b ≈ c → a ≈ c :=
|
||
is_strict_weak_order.incomp_trans _ _ _
|
||
|
||
lemma not_lt_of_equiv {a b : α} : a ≈ b → ¬ a ≺ b :=
|
||
λ h, h.1
|
||
|
||
lemma not_lt_of_equiv' {a b : α} : a ≈ b → ¬ b ≺ a :=
|
||
λ h, h.2
|
||
|
||
instance : is_equiv α equiv :=
|
||
{refl := erefl, trans := @etrans, symm := @esymm}
|
||
end
|
||
|
||
/- Notation for the equivalence relation induced by lt -/
|
||
notation a ` ≈[`:50 lt `]` b:50 := @equiv _ lt _ a b
|
||
end strict_weak_order
|
||
|
||
lemma is_strict_weak_order_of_is_total_preorder {α : Type u} {le : α → α → Prop} {lt : α → α → Prop} [decidable_rel le] [s : is_total_preorder α le]
|
||
(h : ∀ a b, lt a b ↔ ¬ le b a) : is_strict_weak_order α lt :=
|
||
{
|
||
trans :=
|
||
λ a b c hab hbc,
|
||
have nba : ¬ le b a, from iff.mp (h _ _) hab,
|
||
have ncb : ¬ le c b, from iff.mp (h _ _) hbc,
|
||
have hab : le a b, from or.resolve_left (total_of le b a) nba,
|
||
have nca : ¬ le c a, from λ hca : le c a,
|
||
have hcb : le c b, from trans_of le hca hab,
|
||
absurd hcb ncb,
|
||
iff.mpr (h _ _) nca,
|
||
|
||
irrefl := λ a hlt, absurd (refl_of le a) (iff.mp (h _ _) hlt),
|
||
|
||
incomp_trans := λ a b c ⟨nab, nba⟩ ⟨nbc, ncb⟩,
|
||
have hba : le b a, from decidable.of_not_not (iff.mp (not_iff_not_of_iff (h _ _)) nab),
|
||
have hab : le a b, from decidable.of_not_not (iff.mp (not_iff_not_of_iff (h _ _)) nba),
|
||
have hcb : le c b, from decidable.of_not_not (iff.mp (not_iff_not_of_iff (h _ _)) nbc),
|
||
have hbc : le b c, from decidable.of_not_not (iff.mp (not_iff_not_of_iff (h _ _)) ncb),
|
||
have hac : le a c, from trans_of le hab hbc,
|
||
have hca : le c a, from trans_of le hcb hba,
|
||
and.intro
|
||
(λ n, absurd hca (iff.mp (h _ _) n))
|
||
(λ n, absurd hac (iff.mp (h _ _) n))
|
||
}
|