forked from Eelis/hybrid
-
Notifications
You must be signed in to change notification settings - Fork 0
/
interval_spec.v
98 lines (81 loc) · 2.99 KB
/
interval_spec.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
Require geometry abstract.
Require Import bnat util c_util stability.
Require Import Morphisms.
Set Implicit Arguments.
Open Scope CR_scope.
Section contents.
Variables
(chs: concrete.System)
(component: morpher (@cs_eq (concrete.Point chs) ==> @cs_eq CRasCSetoid)%signature).
Inductive IntervalSpec: Q -> nat -> Type :=
| highest b: IntervalSpec b 0
| bound: forall (nb ob: Q) (p: (nb <= ob)%Q) (l: nat),
IntervalSpec ob l -> IntervalSpec nb (S l).
Definition spec_bounds b n: IntervalSpec b n -> bnat (S n) -> geometry.OpenQRange.
apply (IntervalSpec_rect
(fun cr n _ => bnat (S n) -> geometry.OpenQRange) (fun q _ => geometry.qabove q)).
intros nb ob.
intros.
destruct (bnat_cases H0).
destruct s.
subst.
apply (H x).
subst.
exists (Some nb, Some ob).
assumption.
Defined.
Definition bounds b n: IntervalSpec b n -> bnat (S (S n)) -> geometry.OpenQRange.
intros s i.
destruct (bnat_cases i) as [[p A] | B].
exact (spec_bounds s p).
exact (geometry.qbelow b).
Defined.
Definition spec_interval b n (s: IntervalSpec b n) (p: concrete.Point chs):
DN (sig (fun i => geometry.in_orange (spec_bounds s i) (component p)) + (component p < 'b)).
Proof with simpl; auto.
revert s p.
induction s; intro p'.
simpl spec_bounds.
generalize (component p').
intro c.
apply (DN_fmap (@CRle_lt_dec ('b) c)). intros [A|B]...
left. exists (bO 0). unfold geometry.in_orange...
apply (DN_bind (@CRle_lt_dec ('nb) (component p'))). intros [A|B].
apply (DN_fmap (IHs p')). intro.
left.
destruct H.
destruct s0.
exists (bS x)...
exists (bO (S l)).
unfold geometry.in_orange...
apply DN_return...
Qed.
Definition select_interval b n (s: IntervalSpec b n) l p: concrete.invariant (l, p) ->
DN (sig (fun i => geometry.in_orange (bounds s i) (component p))).
Proof with simpl; auto.
intros.
apply (DN_fmap (spec_interval s p)). intros [[i H0] | H0].
exists (bS i)...
exists (bO (S n)).
split...
Qed.
Definition select_interval' b n (s: IntervalSpec b n)
(inv_lower: forall l p, concrete.invariant (l, p) -> 'b <= component p)
l p: concrete.invariant (l, p) ->
DN (sig (fun i => geometry.in_orange (spec_bounds s i) (component p))).
Proof with eauto.
intros.
apply (DN_fmap (spec_interval s p)). intros [[i H0] | H0]...
elimtype False.
apply CRlt_le_asym with (component p) ('b)...
Qed.
Variables (b: Q) (n: nat) (s: IntervalSpec b n).
Definition Region := bnat (S (S n)).
Require interval_abstraction.
Definition ap: abstract.Space chs :=
interval_abstraction.space chs component (NoDup_bnats _) (bounds s) (select_interval s).
Definition ap' (UH: forall l p, concrete.invariant (l, p) -> ' b <= component p):
abstract.Space chs :=
interval_abstraction.space chs component (NoDup_bnats _) (spec_bounds s) (select_interval' s UH).
End contents.
Implicit Arguments bound [ob l].