Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Newer
Older
100644 141 lines (97 sloc) 3.655 kb
409682c @Eelis Use new invariant stability requirement to get rid of one use of tric…
Eelis authored
1
2 (* Doubly-negated types as a monad: *)
3
4 Definition DN (T: Type): Prop := (T -> False) -> False.
5
6 Hint Unfold DN.
7
815fcd2 @Eelis Prove monad laws for DN.
Eelis authored
8 Definition DN_return {T: Type}: T -> DN T :=
9 fun x f => f x.
10
5b675f3 Introducing monadic notation for DN and using it in one of the existi…
Adam.Koprowski authored
11 Notation "'return' x" := (DN_return x) (at level 30).
12
9eaea59 @Eelis Clean up some proofs.
Eelis authored
13 Hint Resolve @DN_return.
14
815fcd2 @Eelis Prove monad laws for DN.
Eelis authored
15 Definition DN_bind {A: Type}: DN A -> forall B, (A -> DN B) -> DN B :=
16 fun X Y Z P => X (fun a => Z a P).
17
5b675f3 Introducing monadic notation for DN and using it in one of the existi…
Adam.Koprowski authored
18 Notation "x <- e ; t" := (DN_bind e _ (fun x => t)) (right associativity, at level 60).
19
815fcd2 @Eelis Prove monad laws for DN.
Eelis authored
20 Definition ext_eq: Prop := forall (A B: Type) (f g: A -> B), (forall x, f x = g x) -> f = g.
409682c @Eelis Use new invariant stability requirement to get rid of one use of tric…
Eelis authored
21
815fcd2 @Eelis Prove monad laws for DN.
Eelis authored
22 Lemma DN_runit: ext_eq -> forall A (x: DN A),
23 DN_bind x _ DN_return = x.
24 Proof.
25 intros.
26 cut (forall y y', y = y' -> x y = x y'). firstorder.
27 congruence.
28 Qed.
29
30 Lemma DN_lunit: ext_eq -> forall A B (a: A) (f: A -> DN B),
31 DN_bind (DN_return a) _ f = f a.
409682c @Eelis Use new invariant stability requirement to get rid of one use of tric…
Eelis authored
32 Proof. firstorder. Qed.
33
815fcd2 @Eelis Prove monad laws for DN.
Eelis authored
34 Lemma DN_assoc A B C (a: DN A) (f: A -> DN B) (g: B -> DN C):
35 DN_bind (DN_bind a _ f) _ g = DN_bind a _ (fun x => DN_bind (f x) _ g).
36 Proof. reflexivity. Qed.
37
409682c @Eelis Use new invariant stability requirement to get rid of one use of tric…
Eelis authored
38 Lemma DN_fmap {A: Type}: DN A -> forall B, (A -> B) -> DN B.
39 Proof. firstorder. Qed.
40
9eaea59 @Eelis Clean up some proofs.
Eelis authored
41 Lemma DN_liftM2 {A B C: Type} (f: A -> B -> C): DN A -> DN B -> DN C.
42 Proof. clear. firstorder. Qed.
43 (* todo: this is a specialization for DN. make a normal monadic version *)
44
9d51b73 @Eelis Make select_region/ContRespect/DiscRespect produce DN'd existentials,…
Eelis authored
45 Lemma DN_exists {T: Type} {P: T -> Prop} {x: T}: DN (P x) -> DN (ex P).
46 Proof. firstorder. Qed.
47
409682c @Eelis Use new invariant stability requirement to get rid of one use of tric…
Eelis authored
48 Inductive Stable P := mkStable: (DN P -> P) -> Stable P.
49 (* Using an Inductive gets us universe polymorphism, which the following
50 simpler alternative does not provide: *)
51
52 (* Definition Stable P := DN P -> P. *)
53
54 Lemma DN_apply {T: Type}: DN T -> forall P, Stable P -> (T -> P) -> P.
55 Proof. firstorder. Qed.
56
c917202 @Eelis Lots and lots of improvements, restructuring, clarification, cleanup.
Eelis authored
57 Lemma DN_free P: Stable P -> DN P -> P.
58 Proof. firstorder. Qed.
59
409682c @Eelis Use new invariant stability requirement to get rid of one use of tric…
Eelis authored
60 Lemma Stable_neg (P: Prop): Stable (~P).
61 Proof. firstorder. Qed.
62
63 Lemma Stable_False: Stable False.
64 Proof. firstorder. Qed.
65
2c388de @Eelis Make unbounded rotator and room heating conc.v's compile (temporarily…
Eelis authored
66 Lemma Stable_True: Stable True.
67 Proof. firstorder. Qed.
68
69 Hint Immediate Stable_False Stable_True.
409682c @Eelis Use new invariant stability requirement to get rid of one use of tric…
Eelis authored
70
9eaea59 @Eelis Clean up some proofs.
Eelis authored
71 Lemma stable_conjunction (A B: Prop): Stable A -> Stable B -> Stable (A /\ B).
72 Proof. firstorder. Qed.
73
74 Hint Resolve stable_conjunction.
75
76 Lemma forall_stable (T: Type) (P: T -> Type): (forall x, Stable (P x)) -> Stable (forall x, P x).
77 Proof. firstorder. Qed.
78
79 Hint Resolve forall_stable.
80
81 Require Import util.
82
83 Lemma decision_stable P: decision P -> Stable P.
84 Proof. firstorder. Qed.
85
86 Require Import CRreal Classic.
87
409682c @Eelis Use new invariant stability requirement to get rid of one use of tric…
Eelis authored
88 Lemma Qle_dec x y: decision (Qle x y).
89 intros.
90 destruct (Qlt_le_dec y x); [right | left]; [apply Qlt_not_le |]; assumption.
91 Defined.
92 (* Todo: Don't I have this elsewhere? *)
93
c917202 @Eelis Lots and lots of improvements, restructuring, clarification, cleanup.
Eelis authored
94 (* Everything is decidable in DN: *)
95
96 Lemma DN_decision (P: Prop): DN (decision P).
97 Proof. firstorder. Qed.
98
99 Lemma DN_decisionT (P: Type): DN (P + (P->False)).
100 Proof. firstorder. Qed.
101
409682c @Eelis Use new invariant stability requirement to get rid of one use of tric…
Eelis authored
102 Lemma CRnonNeg_stable x: Stable (CRnonNeg x).
103 Proof with auto.
104 unfold CRnonNeg.
105 intros.
106 constructor.
107 intros.
108 destruct (Qle_dec (-e) (approximate x e))...
109 elimtype False...
110 Qed.
111
112 Hint Resolve CRnonNeg_stable.
113
114 Lemma CRle_stable (x y: CR): Stable (CRle x y).
115 Proof. unfold CRle. auto. Qed.
116
117 Hint Resolve CRle_stable.
118
6039059 @Eelis Use stability and double negation arguments in c_util to remove uses …
Eelis authored
119 Lemma CReq_stable (x y: CR): Stable (x == y)%CR.
9eaea59 @Eelis Clean up some proofs.
Eelis authored
120 Proof.
121 unfold st_eq. simpl.
122 unfold regFunEq, ball. simpl.
123 unfold Qmetric.Qball, AbsSmall.
124 auto using decision_stable, Qle_dec.
125 Qed.
409682c @Eelis Use new invariant stability requirement to get rid of one use of tric…
Eelis authored
126
127 Open Local Scope CR_scope.
128
129 Lemma DN_or P Q: Not ((Not P) /\ (Not Q)) -> DN (P + Q).
130 Proof. firstorder. Qed.
131
c917202 @Eelis Lots and lots of improvements, restructuring, clarification, cleanup.
Eelis authored
132 Coercion COr_to_sum A B (x: COr A B): A + B :=
133 match x with
134 | Cinleft y => inl y
135 | Cinright y => inr y
136 end.
9eaea59 @Eelis Clean up some proofs.
Eelis authored
137
c917202 @Eelis Lots and lots of improvements, restructuring, clarification, cleanup.
Eelis authored
138 Definition not_forall_exists_not_DN (T: Type) (P: T -> Prop) (Pd: forall x, P x \/ ~ P x):
139 (~ forall x, P x) -> DN (exists x, ~ P x).
140 Proof. firstorder. Qed.
Something went wrong with that request. Please try again.