forked from Eelis/hybrid
-
Notifications
You must be signed in to change notification settings - Fork 0
/
stability.v
142 lines (99 loc) · 3.57 KB
/
stability.v
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
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
(* Doubly-negated types as a monad: *)
Definition DN (T: Type): Prop := (T -> False) -> False.
Hint Unfold DN.
Definition DN_return {T: Type}: T -> DN T :=
fun x f => f x.
Notation "'return' x" := (DN_return x) (at level 30).
Hint Resolve @DN_return.
Definition DN_bind {A: Type}: DN A -> forall B, (A -> DN B) -> DN B :=
fun X Y Z P => X (fun a => Z a P).
Notation "x <- e ; t" := (DN_bind e _ (fun x => t)) (right associativity, at level 60).
Definition ext_eq: Prop := forall (A B: Type) (f g: A -> B), (forall x, f x = g x) -> f = g.
Lemma DN_runit: ext_eq -> forall A (x: DN A),
DN_bind x _ DN_return = x.
Proof.
intros.
cut (forall y y', y = y' -> x y = x y'). firstorder.
congruence.
Qed.
Lemma DN_lunit: ext_eq -> forall A B (a: A) (f: A -> DN B),
DN_bind (DN_return a) _ f = f a.
Proof. firstorder. Qed.
Lemma DN_assoc A B C (a: DN A) (f: A -> DN B) (g: B -> DN C):
DN_bind (DN_bind a _ f) _ g = DN_bind a _ (fun x => DN_bind (f x) _ g).
Proof. reflexivity. Qed.
Lemma DN_fmap {A: Type}: DN A -> forall B, (A -> B) -> DN B.
Proof. firstorder. Qed.
Lemma DN_liftM2 {A B C: Type} (f: A -> B -> C): DN A -> DN B -> DN C.
Proof. firstorder. Qed.
(* todo: this is a specialization for DN. make a normal monadic version *)
Lemma DN_exists {T: Type} {P: T -> Prop} {x: T}: DN (P x) -> DN (ex P).
Proof. firstorder. Qed.
Inductive Stable P := mkStable: (DN P -> P) -> Stable P.
(* Using an Inductive gets us universe polymorphism, which the following
simpler alternative does not provide: *)
(* Definition Stable P := DN P -> P. *)
Lemma DN_apply {T: Type}: DN T -> forall P, Stable P -> (T -> P) -> P.
Proof. firstorder. Qed.
Lemma DN_free P: Stable P -> DN P -> P.
Proof. firstorder. Qed.
Lemma Stable_neg (P: Prop): Stable (~P).
Proof. firstorder. Qed.
Lemma Stable_False: Stable False.
Proof. firstorder. Qed.
Lemma Stable_True: Stable True.
Proof. firstorder. Qed.
Hint Immediate Stable_False Stable_True.
Lemma stable_conjunction (A B: Prop): Stable A -> Stable B -> Stable (A /\ B).
Proof. firstorder. Qed.
Hint Resolve stable_conjunction.
Lemma forall_stable (T: Type) (P: T -> Type): (forall x, Stable (P x)) -> Stable (forall x, P x).
Proof. firstorder. Qed.
Hint Resolve forall_stable.
Require Import util.
Lemma decision_stable P: decision P -> Stable P.
Proof. firstorder. Qed.
Require Import CRreal Classic.
Lemma Qle_dec x y: decision (Qle x y).
intros.
destruct (Qlt_le_dec y x); [right | left]; [apply Qlt_not_le |]; assumption.
Defined.
(* Todo: Don't I have this elsewhere? *)
(* Everything is decidable in DN: *)
Lemma DN_decision (P: Prop): DN (decision P).
Proof. firstorder. Qed.
Lemma DN_decisionT (P: Type): DN (P + (P->False)).
Proof. firstorder. Qed.
Lemma CRnonNeg_stable x: Stable (CRnonNeg x).
Proof with auto.
unfold CRnonNeg.
intros.
constructor.
intros.
destruct (Qle_dec (-e) (approximate x e))...
elimtype False...
Qed.
Hint Resolve CRnonNeg_stable.
Lemma CRle_stable (x y: CR): Stable (CRle x y).
Proof. unfold CRle. auto. Qed.
Hint Resolve CRle_stable.
Lemma CReq_stable (x y: CR): Stable (x == y)%CR.
Proof.
unfold st_eq. simpl.
unfold regFunEq, ball. simpl.
unfold Qmetric.Qball, AbsSmall.
auto using decision_stable, Qle_dec.
Qed.
Open Local Scope CR_scope.
Lemma DN_or P Q: Not ((Not P) /\ (Not Q)) -> DN (P + Q).
Proof. firstorder. Qed.
(*
Coercion COr_to_sum A B (x: COr A B): A + B :=
match x with
| Cinleft y => inl y
| Cinright y => inr y
end.
*)
Definition not_forall_exists_not_DN (T: Type) (P: T -> Prop) (Pd: forall x, P x \/ ~ P x):
(~ forall x, P x) -> DN (exists x, ~ P x).
Proof. firstorder. Qed.