Mercurial > hg > Members > atton > agda-proofs

annotate LTL/LTL.agda @ 77:a2e6f61d5f2b default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add modus-ponens
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 09 Feb 2017 06:32:03 +0000
parents a59bebe0265a
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
12
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 -- Principles of Model Checking
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Level
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Relation.Binary.PropositionalEquality
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open ≡-Reasoning
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 module LTL where
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 -- Syntax Definition (p227)
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 data AP : Set where
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 data LTL : Set where
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 true : LTL
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 ap : AP -> LTL
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 _and_ : LTL -> LTL -> LTL
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 not : LTL -> LTL
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 next : LTL -> LTL
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 _until_ : LTL -> LTL -> LTL
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 _or_ : LTL -> LTL -> LTL
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 a or b = not ((not a) and (not b))
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 _implies_ : LTL -> LTL -> LTL
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 a implies b = (not a) or b
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 _equiv_ : LTL -> LTL -> LTL
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 a equiv b = (a implies b) and (b implies a)
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 _xor_ : LTL -> LTL -> LTL
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 a xor b = (a and (not b)) or (b and (not a))
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 eventually : LTL -> LTL
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 eventually a = true until a
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 always : LTL -> LTL
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 always a = not (eventually (not a))
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 -- Equivalences (p244)
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 next-duality-law : (a : LTL) -> not (next a) ≡ next (not a)
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 next-duality-law true = begin
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 not (next true)
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 ≡⟨ {!!} ⟩
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 next (not true)
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 ∎
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 next-duality-law (ap x) = begin
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 not (next (ap x))
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 ≡⟨ {!!} ⟩
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 next (not (ap x))
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 ∎
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 next-duality-law (a and b) = begin
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 not (next (a and b))
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 ≡⟨ {!!} ⟩
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 next (not (a and b))
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 ∎
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 next-duality-law (not a) = {!!}
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 next-duality-law (next a) = {!!}
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 next-duality-law (a until b) = {!!}
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 eventually-duality-law : (a : LTL) -> not (eventually a) ≡ always (not a)
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 eventually-duality-law true = {!!}
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 eventually-duality-law (ap x) = {!!}
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 eventually-duality-law (a and b) = {!!}
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 eventually-duality-law (not a) = {!!}
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 eventually-duality-law (next a) = {!!}
a59bebe0265a Trying LTL
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 eventually-duality-law (a until b) = {!!}