/
basic.lean
63 lines (54 loc) · 1.64 KB
/
basic.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
62
63
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.data.repr init.data.prod init.data.sum.basic
universes u v
inductive ordering
| lt | eq | gt
instance : has_repr ordering :=
⟨(λ s, match s with | ordering.lt := "lt" | ordering.eq := "eq" | ordering.gt := "gt" end)⟩
namespace ordering
def swap : ordering → ordering
| lt := gt
| eq := eq
| gt := lt
@[inline] def or_else : ordering → ordering → ordering
| lt _ := lt
| eq o := o
| gt _ := gt
theorem swap_swap : ∀ (o : ordering), o.swap.swap = o
| lt := rfl
| eq := rfl
| gt := rfl
end ordering
def cmp_using {α : Type u} (lt : α → α → Prop) [decidable_rel lt] (a b : α) : ordering :=
if lt a b then ordering.lt
else if lt b a then ordering.gt
else ordering.eq
def cmp {α : Type u} [has_lt α] [decidable_rel ((<) : α → α → Prop)] (a b : α) : ordering :=
cmp_using (<) a b
instance : decidable_eq ordering :=
λ a b,
match a with
| ordering.lt :=
match b with
| ordering.lt := is_true rfl
| ordering.eq := is_false (λ h, ordering.no_confusion h)
| ordering.gt := is_false (λ h, ordering.no_confusion h)
end
| ordering.eq :=
match b with
| ordering.lt := is_false (λ h, ordering.no_confusion h)
| ordering.eq := is_true rfl
| ordering.gt := is_false (λ h, ordering.no_confusion h)
end
| ordering.gt :=
match b with
| ordering.lt := is_false (λ h, ordering.no_confusion h)
| ordering.eq := is_false (λ h, ordering.no_confusion h)
| ordering.gt := is_true rfl
end
end