Mercurial > hg > Members > kono > Proof > automaton
changeset 334:1466e18c8180
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 21 Mar 2023 08:23:44 +0900 |
| parents | c19d3af30394 |
| children | ce4e44cee2d3 |
| files | automaton-in-agda/src/bijection.agda automaton-in-agda/src/logic.agda automaton-in-agda/src/temporal-logic.agda |
| diffstat | 3 files changed, 21 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/automaton-in-agda/src/bijection.agda Sun Mar 12 23:17:12 2023 +0900 +++ b/automaton-in-agda/src/bijection.agda Tue Mar 21 08:23:44 2023 +0900 @@ -57,7 +57,7 @@ diagn1 n dn = ¬t=f (diag b n ) ( begin not (diag b n) ≡⟨⟩ - not (not fun← b n n) + not (not (fun← b n n)) ≡⟨ cong (λ k → not (k n) ) (sym (fiso← b _)) ⟩ not (fun← b (fun→ b (diag b)) n) ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩
--- a/automaton-in-agda/src/logic.agda Sun Mar 12 23:17:12 2023 +0900 +++ b/automaton-in-agda/src/logic.agda Tue Mar 21 08:23:44 2023 +0900 @@ -10,6 +10,10 @@ true : Bool false : Bool +data Two : Set where + i0 : Two + i1 : Two + record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where constructor ⟪_,_⟫ field @@ -67,7 +71,7 @@ false \/ false = false _ \/ _ = true -not_ : Bool → Bool +not : Bool → Bool not true = false not false = true @@ -198,3 +202,17 @@ _<b_ : ( x y : ℕ) → Bool x <b y = y >b x + +open import Relation.Binary.PropositionalEquality + +¬i0≡i1 : ¬ ( i0 ≡ i1 ) +¬i0≡i1 () + +¬i0→i1 : {x : Two} → ¬ (x ≡ i0 ) → x ≡ i1 +¬i0→i1 {i0} ne = ⊥-elim ( ne refl ) +¬i0→i1 {i1} ne = refl + +¬i1→i0 : {x : Two} → ¬ (x ≡ i1 ) → x ≡ i0 +¬i1→i0 {i0} ne = refl +¬i1→i0 {i1} ne = ⊥-elim ( ne refl ) +
--- a/automaton-in-agda/src/temporal-logic.agda Sun Mar 12 23:17:12 2023 +0900 +++ b/automaton-in-agda/src/temporal-logic.agda Tue Mar 21 08:23:44 2023 +0900 @@ -16,7 +16,7 @@ open import nat open import Data.Nat.Properties -open import Data.Unit +open import Data.Unit using ( ⊤ ; tt ) -- Linear Time Temporal Logic (clock base, it has ○ (next))