-
Notifications
You must be signed in to change notification settings - Fork 0
/
SimpleExamples.v
134 lines (97 loc) · 2.61 KB
/
SimpleExamples.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
(* Probabilistic Temporal Logic *)
Require Import Coq.QArith.QArith.
Open Scope Q_scope.
Require Import ProbLogic.
(* Examples *)
Lemma L1: forall f: o, forall a: action, forall w0: W, forall w: W, (f w) /\ ((a w0) = (cons w nil)) -> ((prob f (cons a nil) ) w0 = 1).
Proof.
intros.
unfold prob.
destruct H as [H1 H2].
rewrite H2.
simpl.
destruct (dec f w).
reflexivity.
contradiction.
Qed.
Lemma L2: forall f: o, forall a: action, forall w0: W, forall w: W, (~ (f w)) /\ ((a w0) = (cons w nil)) -> ((prob f (cons a nil) ) w0 = 0).
Proof.
intros.
unfold prob.
destruct H as [H1 H2].
rewrite H2.
simpl.
destruct (dec f w).
contradiction.
reflexivity.
Qed.
Parameter head: i -> o.
Parameter tail: i -> o.
Parameter toss: action.
Axiom ht: [mforall x:i, (head x) m<-> m~ (tail x)].
Axiom two_sucs: forall w, exists w1 w2, (toss w) = (cons w1 (cons w2 nil)).
Axiom tossAx: [mforall x:i, (dia toss (head x))].
Axiom tossAx2: [mforall x:i, (dia toss (tail x))].
Lemma l: forall w w1 w2 x, (toss w) = (cons w1 (cons w2 nil)) -> (head x w1) -> (~ (head x w2)).
Proof.
intros.
intro H1.
assert ((dia toss (tail x)) w).
apply tossAx2.
unfold dia in H2.
destruct H2 as [w3 [R1 H3]].
unfold r in R1.
unfold is_in in R1.
rewrite H in R1.
destruct R1 as [R11 | [R12 | R13] ].
rewrite R11 in H3.
apply ht in H0.
contradiction.
rewrite R12 in H3.
apply ht in H1.
contradiction.
contradiction.
Qed.
Theorem p: [mforall x: i, (probPred (head x) (cons toss nil) (1 # 2))].
Proof. mv.
unfold probPred.
unfold A.
intros.
assert ((dia toss (head x)) w).
apply tossAx.
unfold dia in H.
destruct H as [w1 [R1 H1]].
unfold r in R1.
assert (exists w3 w4, (toss w) = (cons w3 (cons w4 nil))).
apply two_sucs.
destruct H as [w3 [w4 H]].
simpl.
rewrite H.
simpl.
assert (w1 = w3 \/ w1 = w4).
unfold is_in in R1.
rewrite H in R1.
destruct R1 as [R11 | [R12 | R13]].
left; assumption.
right; assumption.
contradiction.
destruct H0 as [H01 | H02].
destruct (dec (head x) w3).
destruct (dec (head x) w4).
apply (l w w3 w4 x H) in h.
contradiction.
reflexivity.
destruct (dec (head x) w4).
reflexivity.
rewrite H01 in H1.
contradiction.
destruct (dec (head x) w3).
destruct (dec (head x) w4).
apply (l w w3 w4 x H) in h.
contradiction.
reflexivity.
destruct (dec (head x) w4).
reflexivity.
rewrite H02 in H1.
contradiction.
Qed.