-
Notifications
You must be signed in to change notification settings - Fork 259
/
Lemmas.lean
61 lines (46 loc) · 1.99 KB
/
Lemmas.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
/-
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Mathlib.Init.Algebra.Classes
import Mathlib.Init.Data.Ordering.Basic
#align_import init.data.ordering.lemmas from "leanprover-community/lean"@"4bd314f7bd5e0c9e813fc201f1279a23f13f9f1d"
/-!
# Some `Ordering` lemmas
-/
universe u
namespace Ordering
@[simp]
theorem ite_eq_lt_distrib (c : Prop) [Decidable c] (a b : Ordering) :
((if c then a else b) = Ordering.lt) = if c then a = Ordering.lt else b = Ordering.lt := by
by_cases c <;> simp [*]
#align ordering.ite_eq_lt_distrib Ordering.ite_eq_lt_distrib
@[simp]
theorem ite_eq_eq_distrib (c : Prop) [Decidable c] (a b : Ordering) :
((if c then a else b) = Ordering.eq) = if c then a = Ordering.eq else b = Ordering.eq := by
by_cases c <;> simp [*]
#align ordering.ite_eq_eq_distrib Ordering.ite_eq_eq_distrib
@[simp]
theorem ite_eq_gt_distrib (c : Prop) [Decidable c] (a b : Ordering) :
((if c then a else b) = Ordering.gt) = if c then a = Ordering.gt else b = Ordering.gt := by
by_cases c <;> simp [*]
#align ordering.ite_eq_gt_distrib Ordering.ite_eq_gt_distrib
end Ordering
section
variable {α : Type u} {lt : α → α → Prop} [DecidableRel lt]
attribute [local simp] cmpUsing
@[simp]
theorem cmpUsing_eq_lt (a b : α) : (cmpUsing lt a b = Ordering.lt) = lt a b := by
simp only [cmpUsing, Ordering.ite_eq_lt_distrib, ite_self, if_false_right, and_true]
#align cmp_using_eq_lt cmpUsing_eq_lt
@[simp]
theorem cmpUsing_eq_gt [IsStrictOrder α lt] (a b : α) : cmpUsing lt a b = Ordering.gt ↔ lt b a := by
simp only [cmpUsing, Ordering.ite_eq_gt_distrib, if_false_right, and_true, if_false_left,
and_iff_right_iff_imp]
exact fun hba hab ↦ (irrefl a) (_root_.trans hab hba)
#align cmp_using_eq_gt cmpUsing_eq_gt
@[simp]
theorem cmpUsing_eq_eq (a b : α) : cmpUsing lt a b = Ordering.eq ↔ ¬lt a b ∧ ¬lt b a := by simp
#align cmp_using_eq_eq cmpUsing_eq_eq
end