Mercurial > hg > Members > kono > Proof > automaton

changeset 113:58b009043733

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 18 Nov 2019 19:51:08 +0900
parents 6cf7dd270e9f
children a7364dfcc51e
files agda/finiteSet.agda
diffstat 1 files changed, 28 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/agda/finiteSet.agda	Mon Nov 18 12:08:09 2019 +0900
+++ b/agda/finiteSet.agda	Mon Nov 18 19:51:08 2019 +0900
@@ -140,31 +140,36 @@
         n = a Data.Nat.+ b
         Q : Set 
         Q = A ∨ B
+        f-a : ∀{i} → (f : Fin i ) → (a : ℕ ) → toℕ f > a  → toℕ f < a Data.Nat.+ b  → Fin b
+        f-a {i} f zero lt lt2 = fromℕ≤ lt2 
+        f-a {suc i} (suc f) (suc a) (s≤s lt) (s≤s lt2) = f-a f a lt lt2
+        f-a zero (suc x) () _
         Q←F : Fin n → Q
         Q←F f with Data.Nat.Properties.<-cmp (toℕ f) a
         Q←F f | tri< lt ¬b ¬c = case1 (FiniteSet.Q←F fa (fromℕ≤ lt )) 
-        Q←F f | tri≈ ¬a eq ¬c = case2 (FiniteSet.Q←F fb (fromℕ≤ 0<b )) where
-            0<b : 0 < b
-            0<b = {!!}
-        Q←F f | tri> ¬a ¬b c = case2 (FiniteSet.Q←F fb (fromℕ≤ f-a<b )) where
-            f-a : ℕ
-            f-a = {!!}
-            f-a<b : f-a < b
-            f-a<b = {!!} 
+        Q←F f | tri≈ ¬a eq ¬c = case2 (FiniteSet.Q←F fb (fromℕ≤ (0<b a (a<a+b eq ) ))) where
+            a<a+b : toℕ f ≡ a → a < a Data.Nat.+ b 
+            a<a+b eq = subst (λ k → k < a Data.Nat.+ b) eq ( toℕ<n f )
+            0<b : (a : ℕ ) → a < a Data.Nat.+ b  → 0 < b
+            0<b zero a<a+b = a<a+b
+            0<b (suc a) (s≤s a<a+b) = 0<b a a<a+b
+        Q←F f | tri> ¬a ¬b c = case2 (FiniteSet.Q←F fb (f-a f a c (toℕ<n f) ))
         F←Q : Q → Fin n
         F←Q (case1 qa) = inject+ b (FiniteSet.F←Q fa qa)
         F←Q (case2 qb) = raise a (FiniteSet.F←Q fb qb)
         finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
         finiso→ = {!!}
+        -- (case1 qa) = {!!}
+        -- finiso→ (case2 qb) = {!!}
         finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
-        finiso← = {!!}
+        finiso← f = {!!} -- with Data.Nat.Properties.<-cmp (toℕ f) a
 
 import Data.Nat.DivMod
 import Data.Nat.Properties
 
 open _∧_
 
-fin→' : {A : Set} → { a : ℕ } → FiniteSet A {a} → FiniteSet (A → Bool ) {exp 2 a}
+fin→' : {A : Set} → { a : ℕ } → FiniteSet A {suc a} → FiniteSet (A → Bool ) {exp 2 (suc a)}
 fin→' {A} {a} fin = record {
         Q←F = Q←F  
       ; F←Q =  F←Q  
@@ -172,7 +177,7 @@
       ; finiso← = finiso← 
    } where
         n : ℕ
-        n = exp 2 a
+        n = exp 2 (suc a)
         shift : (n : ℕ) →  ℕ ∧ Bool
         shift n with (n Data.Nat.DivMod.mod 2) ≟ (# 0)
         shift n | yes p = record { proj1 = n Data.Nat.DivMod.div 2 ; proj2 = true }
@@ -188,17 +193,20 @@
         Q = A → Bool
         Q←F : Fin n → Q
         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 {!!})
+        unshift : {i : ℕ } (n : Fin i) → Bool → Fin (i Data.Nat.+ i)
+        unshift {i} n true = fromℕ≤ 2n<2i where
+            2n<2i : (toℕ n) Data.Nat.+ (toℕ n) <  i Data.Nat.+ i
+            2n<2i = {!!}
+        unshift {i} n false = fromℕ≤ 2n<2i+1 where
+            2n<2i+1 : (toℕ n) Data.Nat.+ (toℕ n) Data.Nat.+ 1 <  i Data.Nat.+ i
+            2n<2i+1 = {!!}
+        F←Q-unshift : Q → (i : ℕ ) → i < suc a → Fin (exp 2 (suc i)) 
+        F←Q-unshift fq zero lt with fq (FiniteSet.Q←F fin (fromℕ≤ a<sa))
         ... | 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ℕ≤ {!!}
+        ... | true = # 1
+        F←Q-unshift fq (suc n) lt = cast {!!} (unshift (F←Q-unshift fq n {!!} ) (fq (FiniteSet.Q←F fin (fromℕ≤ lt )))) 
         F←Q : Q → Fin n
-        F←Q fq = F←Q-unshift fq a
+        F←Q fq = F←Q-unshift fq a a<sa
         finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
         finiso→ = {!!}
         finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f