-
Notifications
You must be signed in to change notification settings - Fork 259
/
PropInstances.lean
125 lines (96 loc) · 3.82 KB
/
PropInstances.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
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl
-/
import Mathlib.Order.Disjoint
#align_import order.prop_instances from "leanprover-community/mathlib"@"6623e6af705e97002a9054c1c05a980180276fc1"
/-!
# The order on `Prop`
Instances on `Prop` such as `DistribLattice`, `BoundedOrder`, `LinearOrder`.
-/
/-- Propositions form a distributive lattice. -/
instance Prop.instDistribLattice : DistribLattice Prop where
sup := Or
le_sup_left := @Or.inl
le_sup_right := @Or.inr
sup_le := fun _ _ _ => Or.rec
inf := And
inf_le_left := @And.left
inf_le_right := @And.right
le_inf := fun _ _ _ Hab Hac Ha => And.intro (Hab Ha) (Hac Ha)
le_sup_inf := fun _ _ _ => or_and_left.2
#align Prop.distrib_lattice Prop.instDistribLattice
/-- Propositions form a bounded order. -/
instance Prop.instBoundedOrder : BoundedOrder Prop where
top := True
le_top _ _ := True.intro
bot := False
bot_le := @False.elim
#align Prop.bounded_order Prop.instBoundedOrder
theorem Prop.bot_eq_false : (⊥ : Prop) = False :=
rfl
#align Prop.bot_eq_false Prop.bot_eq_false
theorem Prop.top_eq_true : (⊤ : Prop) = True :=
rfl
#align Prop.top_eq_true Prop.top_eq_true
instance Prop.le_isTotal : IsTotal Prop (· ≤ ·) :=
⟨fun p q => by by_cases h : q <;> simp [h]⟩
#align Prop.le_is_total Prop.le_isTotal
noncomputable instance Prop.linearOrder : LinearOrder Prop := by
classical
exact Lattice.toLinearOrder Prop
#align Prop.linear_order Prop.linearOrder
@[simp]
theorem sup_Prop_eq : (· ⊔ ·) = (· ∨ ·) :=
rfl
#align sup_Prop_eq sup_Prop_eq
@[simp]
theorem inf_Prop_eq : (· ⊓ ·) = (· ∧ ·) :=
rfl
#align inf_Prop_eq inf_Prop_eq
namespace Pi
variable {ι : Type*} {α' : ι → Type*} [∀ i, PartialOrder (α' i)]
theorem disjoint_iff [∀ i, OrderBot (α' i)] {f g : ∀ i, α' i} :
Disjoint f g ↔ ∀ i, Disjoint (f i) (g i) := by
classical
constructor
· intro h i x hf hg
refine' (update_le_iff.mp <| h (update_le_iff.mpr ⟨hf, fun _ _ => _⟩)
(update_le_iff.mpr ⟨hg, fun _ _ => _⟩)).1
· exact bot_le
· exact bot_le
· intro h x hf hg i
apply h i (hf i) (hg i)
#align pi.disjoint_iff Pi.disjoint_iff
theorem codisjoint_iff [∀ i, OrderTop (α' i)] {f g : ∀ i, α' i} :
Codisjoint f g ↔ ∀ i, Codisjoint (f i) (g i) :=
@disjoint_iff _ (fun i => (α' i)ᵒᵈ) _ _ _ _
#align pi.codisjoint_iff Pi.codisjoint_iff
theorem isCompl_iff [∀ i, BoundedOrder (α' i)] {f g : ∀ i, α' i} :
IsCompl f g ↔ ∀ i, IsCompl (f i) (g i) := by
simp_rw [_root_.isCompl_iff, disjoint_iff, codisjoint_iff, forall_and]
#align pi.is_compl_iff Pi.isCompl_iff
end Pi
@[simp]
theorem Prop.disjoint_iff {P Q : Prop} : Disjoint P Q ↔ ¬(P ∧ Q) :=
disjoint_iff_inf_le
#align Prop.disjoint_iff Prop.disjoint_iff
@[simp]
theorem Prop.codisjoint_iff {P Q : Prop} : Codisjoint P Q ↔ P ∨ Q :=
codisjoint_iff_le_sup.trans <| forall_const True
#align Prop.codisjoint_iff Prop.codisjoint_iff
@[simp]
theorem Prop.isCompl_iff {P Q : Prop} : IsCompl P Q ↔ ¬(P ↔ Q) := by
rw [_root_.isCompl_iff, Prop.disjoint_iff, Prop.codisjoint_iff, not_iff]
by_cases P <;> by_cases Q <;> simp [*]
#align Prop.is_compl_iff Prop.isCompl_iff
-- Porting note: Lean 3 would unfold these for us, but we need to do it manually now
section decidable_instances
universe u
variable {α : Type u}
instance Prop.decidablePredBot : DecidablePred (⊥ : α → Prop) := fun _ => instDecidableFalse
instance Prop.decidablePredTop : DecidablePred (⊤ : α → Prop) := fun _ => instDecidableTrue
instance Prop.decidableRelBot : DecidableRel (⊥ : α → α → Prop) := fun _ _ => instDecidableFalse
instance Prop.decidableRelTop : DecidableRel (⊤ : α → α → Prop) := fun _ _ => instDecidableTrue
end decidable_instances