Mercurial > hg > Members > kono > Proof > automaton

changeset 117:f00c990a24da

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 Wed, 20 Nov 2019 00:01:38 +0900
parents a8b55fbca18d
children 37c919cec9ac
files agda/finiteSet.agda
diffstat 1 files changed, 35 insertions(+), 40 deletions(-) [+]
line wrap: on
line diff
--- a/agda/finiteSet.agda	Tue Nov 19 10:50:35 2019 +0900
+++ b/agda/finiteSet.agda	Wed Nov 20 00:01:38 2019 +0900
@@ -162,6 +162,9 @@
                    suc f
                 ∎  where
                 open ≡-Reasoning
+        lemma6 : {a b : ℕ } → {f : Fin a} → toℕ (inject+ b f) ≡ toℕ f
+        lemma6 {suc a} {b} {zero} = refl
+        lemma6 {suc a} {b} {suc f} = cong (λ k → suc k ) (lemma6 {a} {b} {f})
         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 )) 
@@ -171,8 +174,27 @@
         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→ (case1 qa) = lemma7 where
+            lemma5 : toℕ (inject+ b (FiniteSet.F←Q fa qa)) < a 
+            lemma5 = subst (λ k → k < a ) (sym lemma6) (toℕ<n (FiniteSet.F←Q fa qa))
+            lemma8 : ((toℕ (inject+ b (FiniteSet.F←Q fa qa))) < a) ≡ ( toℕ (FiniteSet.F←Q fa qa) < a )
+            lemma8 = {!!}
+            lemma7 : Q←F (F←Q (case1 qa)) ≡ case1 qa
+            lemma7 with Data.Nat.Properties.<-cmp (toℕ (inject+ b (FiniteSet.F←Q fa qa))) a
+            lemma7 | tri< lt ¬b ¬c = begin
+                   case1 (FiniteSet.Q←F fa (fromℕ≤ lt ))
+                ≡⟨ {!!} ⟩
+                   case1 (FiniteSet.Q←F fa (fromℕ≤ (toℕ<n (FiniteSet.F←Q fa qa)) ))
+                ≡⟨ cong (λ k → case1 (FiniteSet.Q←F fa k )) lemma4 ⟩
+                   case1 (FiniteSet.Q←F fa (FiniteSet.F←Q fa qa) )
+                ≡⟨ cong (λ k → case1 k ) (FiniteSet.finiso→ fa _ ) ⟩
+                   case1 qa
+                ∎  where open ≡-Reasoning
+            lemma7 | tri≈ ¬a b ¬c = ⊥-elim ( ¬a lemma5 )
+            lemma7 | tri> ¬a ¬b c = ⊥-elim ( ¬a lemma5 )
+        finiso→ (case2 qb) = {!!} where
+            lemma9 :  Q←F (F←Q (case2 qb)) ≡ case2 qb
+            lemma9 = {!!} 
         finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
         finiso← f with Data.Nat.Properties.<-cmp (toℕ f) a
         finiso← f | tri< lt ¬b ¬c = lemma11 where
@@ -298,45 +320,18 @@
                   f
               ∎  where open ≡-Reasoning
 
-record FiniteSubSet ( Q : Set ) ( n m : ℕ ) : Set  where
-     field
-        n<m : n < suc m
-        finite : FiniteSet Q {m}
-        Q←F : Fin n → Q
-        F←Q : Q → Fin n
-        finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
-        finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
-
-finiteSubSetN :  { Q : Set } → {n  : ℕ } → FiniteSet Q {n} → FiniteSubSet Q n n 
-finiteSubSetN = {!!}
-
-finiteSubSet-1 :  { Q : Set } → {n m : ℕ } → FiniteSubSet Q (suc n) m → FiniteSubSet Q n m 
-finiteSubSet-1 = {!!}
-
-Func2List' : { Q : Set } → {n m : ℕ } → FiniteSubSet Q  n m → ( Q → Bool ) → Vec Bool n
-Func2List' {Q} {zero} fin Q→B = []
-Func2List' {Q} {suc n} {m} fin Q→B = Q→B (FiniteSubSet.Q←F fin (fromℕ≤ (a<sa {n})))  ∷ Func2List' {Q} {n} {m} (finiteSubSet-1 fin ) Q→B
+Func2List : { Q : Set } → {n m : ℕ } → n < suc m → FiniteSet Q {m} → ( Q → Bool ) → Vec Bool n
+Func2List {Q} {zero} _ fin Q→B = []
+Func2List {Q} {suc n} {m} (s≤s n<m) fin Q→B = Q→B (FiniteSet.Q←F fin (fromℕ≤ n<m)) ∷ Func2List {Q} {n} {m} (Data.Nat.Properties.<-trans n<m a<sa ) fin Q→B
 
-List2Func' : { Q : Set } → {n m : ℕ } → FiniteSubSet Q n m → Vec Bool n →  Q → Bool 
-List2Func' {Q} {zero}  fin [] q = false
-List2Func' {Q} {suc n} {m} fin (h ∷ t) q with  FiniteSubSet.F←Q fin q ≟ fromℕ≤ (a<sa {n})
+List2Func : { Q : Set } → {n m : ℕ } → n < suc m → FiniteSet Q {m} → Vec Bool n →  Q → Bool 
+List2Func {Q} {zero} _ fin [] q = false
+List2Func {Q} {suc n} {m} (s≤s n<m) fin (h ∷ t) q with  FiniteSet.F←Q fin q ≟ fromℕ≤ n<m
 ... | yes _ = h
-... | no _ = List2Func' {Q} {n} {m} (finiteSubSet-1 fin) t q
+... | no _ = List2Func {Q} {n} {m} (Data.Nat.Properties.<-trans n<m a<sa ) fin t q
 
-Func2List : { Q : Set } → {n : ℕ } → FiniteSet Q {n}  → ( Q → Bool ) → Vec Bool n
-Func2List {Q} {n} fin Q→B = to-list Q→B where
-     list1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → Vec Bool m
-     list1  zero  _ _ = []
-     list1 ( suc m ) m<n p with bool-≡-? (p (FiniteSet.Q←F fin (fromℕ≤ {m} {n} m<n))) true
-     ... | yes _ = true ∷ list1 m (lt2 m<n) p
-     ... | no  _ = false ∷ list1 m (lt2 m<n) p
-     to-list : ( Q → Bool ) → Vec Bool n
-     to-list p = list1 n (lt0 n) p 
+F2L-iso : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q {n}) → (x : Vec Bool n ) → Func2List a<sa fin (List2Func a<sa fin x ) ≡ x
+F2L-iso = {!!}
 
-get : { Σ : Set  } {n : ℕ} →  (x : Vec Σ n ) → { i : ℕ } → i < n  → Σ
-get [] ()
-get (h ∷ t) {0} (s≤s lt) = h
-get (h ∷ t) {suc i} (s≤s lt) = get t lt
-
-List2Func : { Q : Set } → {n : ℕ } → FiniteSet Q {n}  → Vec Bool n →  Q → Bool 
-List2Func {Q} {n} fin x q = get (reverse x) (toℕ<n (FiniteSet.F←Q fin q ) )
+L2F-iso : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q {n}) → (f : Q → Bool ) → (q : Q ) → (List2Func a<sa fin (Func2List a<sa fin f )) q ≡ f q
+L2F-iso = {!!}