Mercurial > hg > Members > kono > Proof > automaton

changeset 112:6cf7dd270e9f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
finite
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 18 Nov 2019 12:08:09 +0900
parents ed0a2dad62f4
children 58b009043733
files agda/finiteSet.agda
diffstat 1 files changed, 20 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/agda/finiteSet.agda	Mon Nov 18 11:00:31 2019 +0900
+++ b/agda/finiteSet.agda	Mon Nov 18 12:08:09 2019 +0900
@@ -162,6 +162,8 @@
 import Data.Nat.DivMod
 import Data.Nat.Properties
 
+open _∧_
+
 fin→' : {A : Set} → { a : ℕ } → FiniteSet A {a} → FiniteSet (A → Bool ) {exp 2 a}
 fin→' {A} {a} fin = record {
         Q←F = Q←F  
@@ -175,15 +177,28 @@
         shift n with (n Data.Nat.DivMod.mod 2) ≟ (# 0)
         shift n | yes p = record { proj1 = n Data.Nat.DivMod.div 2 ; proj2 = true }
         shift n | no ¬p = record { proj1 = n Data.Nat.DivMod.div 2 ; proj2 = false }
-        Q←F-shift : (n : ℕ) → A → Bool
-        Q←F-shift zero = {!!}
-        Q←F-shift (suc n) = {!!}
+        Q←F-shift : (n : ℕ) → ℕ → ℕ → Bool
+        Q←F-shift zero an flag with zero Data.Nat.Properties.≟ an | shift flag
+        ... | yes _ | F = proj2 F
+        ... | no _ | _ = true
+        Q←F-shift (suc n) an flag with zero Data.Nat.Properties.≟ an | shift flag
+        ... | yes _ | F = proj2 F
+        ... | no _ | F = Q←F-shift n an (proj1 F)
         Q : Set 
         Q = A → Bool
         Q←F : Fin n → Q
-        Q←F f = λ qa → {!!}
+        Q←F f = λ qa → Q←F-shift a (toℕ (FiniteSet.F←Q fin qa)) (toℕ f)
+        unshift : (n : ℕ) → Bool → ℕ
+        unshift n true = n * 2 Data.Nat.+ 1
+        unshift n false = n * 2
+        F←Q-unshift : Q → (i : ℕ ) → Fin (exp 2 i) 
+        F←Q-unshift fq zero with fq (FiniteSet.Q←F fin {!!})
+        ... | false = # 0
+        ... | true = fromℕ≤ {!!}
+        F←Q-unshift fq (suc n) with unshift (toℕ (F←Q-unshift fq n )) (fq (FiniteSet.Q←F fin {!!})) 
+        ... | ttt = fromℕ≤ {!!}
         F←Q : Q → Fin n
-        F←Q fq = {!!}
+        F←Q fq = F←Q-unshift fq a
         finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
         finiso→ = {!!}
         finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f