Mercurial > hg > Members > kono > Proof > automaton

changeset 288:e4b910112fdf

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 Tue, 28 Dec 2021 12:38:16 +0900
parents ce16779e72a5
children c9802aa2a8c9
files automaton-in-agda/src/fin.agda
diffstat 1 files changed, 32 insertions(+), 24 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/fin.agda	Tue Dec 28 03:17:29 2021 +0900
+++ b/automaton-in-agda/src/fin.agda	Tue Dec 28 12:38:16 2021 +0900
@@ -148,10 +148,10 @@
 
 list-less : {n : ℕ } → List (Fin (suc n)) → List (Fin n)
 list-less [] = []
-list-less {n} (i ∷ ls) with NatP.<-cmp (toℕ i) n
-... | tri< a ¬b ¬c = fromℕ< a ∷ list-less ls
+list-less {n} (i ∷ ls) with <-fcmp (fromℕ< a<sa) i
+... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ i < suc k ) (sym fin<asa) (fin≤n _ )))
 ... | tri≈ ¬a b ¬c = list-less ls
-... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (fin≤n i) c )
+... | tri> ¬a ¬b c = x<y→fin-1 c ∷ list-less ls
 
 record NList (n : ℕ) (qs : List (Fin (suc n))) : Set where
   field
@@ -167,21 +167,29 @@
      fdup+1 : (qs : List (Fin (suc n))) (i : Fin n) → fin-dup-in-list i (list-less qs) ≡ true → FDup-in-list (suc n) qs
      fdup+1 qs i p with fin-dup-in-list (fromℕ< a<sa ) qs | inspect (fin-dup-in-list (fromℕ< a<sa )) qs 
      ... | true  | record {eq = eq } = record { dup = fromℕ< a<sa ; is-dup = eq }
-     ... | false | record {eq = ne } = f1-phase1 qs p where
-          f1-phase2 : (qs : List (Fin (suc n)) ) → fin-phase2 i (list-less qs) ≡ true → {!!}
-          f1-phase2 (x ∷ qs) p with <-fcmp (fin+1 i) x
-          f1-phase2 (x ∷ qs) p | tri< a ¬b ¬c with NatP.<-cmp (toℕ x) n
-          ... | tri< a₁ ¬b₁ ¬c₁ = f1-phase2 qs {!!}
-          ... | tri≈ ¬a b ¬c₁ = f1-phase2 qs {!!}
-          ... | tri> ¬a ¬b₁ c = {!!} -- ⊥-elim ( nat-<> fin<n c )
-          f1-phase2 (x ∷ qs) p | tri≈ ¬a b ¬c = refl
-          f1-phase2 (x ∷ qs) p | tri> ¬a ¬b c = f1-phase2 qs {!!}
-          f1-phase1 : (qs : List (Fin (suc n)) ) → fin-phase1 i (list-less qs) ≡ true → {!!}
-          f1-phase1 [] ()
-          f1-phase1 (x ∷ qs) p with <-fcmp (fin+1 i) x
-          ... | tri< a ¬b ¬c = f1-phase1 qs {!!}
-          ... | tri≈ ¬a b ¬c = f1-phase2 qs {!!}
-          ... | tri> ¬a ¬b c = f1-phase1 qs {!!}
+     ... | false | record {eq = ne } = record { dup = fin+1 i ; is-dup = f1-phase1 qs p (case1 ne) } where
+          f1-phase2 : (qs : List (Fin (suc n)) ) → fin-phase2 i (list-less qs) ≡ true
+              → (fin-phase1 (fromℕ< a<sa) qs ≡ false ) ∨ (fin-phase2 (fromℕ< a<sa) qs ≡ false)
+              → fin-phase2 (fin+1 i) qs ≡ true
+          f1-phase2 (x ∷ qs) p (case1 q1) with  <-fcmp (fromℕ< a<sa) x
+          ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
+          ... | tri≈ ¬a b ¬c = {!!}
+          f1-phase2 (x ∷ qs) p (case1 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x
+          ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase2 qs p (case1 q1)
+          ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁ = {!!}
+          ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = {!!}
+          ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁ = {!!}
+          ... | tri≈ ¬a₁ b ¬c | tri≈ ¬a₂ b₁ ¬c₁ = refl
+          ... | tri≈ ¬a₁ b ¬c | tri> ¬a₂ ¬b₁ c₁ = {!!}
+          ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = {!!}
+          ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = {!!}
+          ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase2 qs p (case1 q1)
+          f1-phase2 (x ∷ qs) p (case2 q2) = {!!}
+          f1-phase1 : (qs : List (Fin (suc n)) ) → fin-phase1 i (list-less qs) ≡ true
+              → (fin-phase1 (fromℕ< a<sa) qs ≡ false ) ∨ (fin-phase2 (fromℕ< a<sa) qs ≡ false)
+              → fin-phase1 (fin+1 i) qs ≡ true
+          f1-phase1 (x ∷ qs) p (case1 q1) = {!!}
+          f1-phase1 (x ∷ qs) p (case2 q2) = {!!}
      fdup-phase2 : (qs : List (Fin (suc n)) ) 
          → ( fin-phase2 (fromℕ< a<sa ) qs ≡ true )  ∨ NList n qs
      fdup-phase2 []  = case2  record { ls = [] ; lseq = refl ; ls< = case1 refl }
@@ -192,12 +200,12 @@
      ... | case1 p = case1 p
      ... | case2 nlist = case2 record { ls = x<y→fin-1 c ∷ NList.ls nlist ; lseq = fdup01 ; ls< = case1 {!!} } where
            fdup01 : list-less (x ∷ qs) ≡ x<y→fin-1 c ∷ NList.ls nlist
-           fdup01 with NatP.<-cmp (toℕ x) n
-           ... | tri< a ¬b ¬c = begin
-                fromℕ< a ∷ list-less qs ≡⟨ cong₂ (λ j k → j ∷ k ) (lemma10 refl) (NList.lseq nlist) ⟩
-                fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa))) ∷ NList.ls nlist ∎  where open ≡-Reasoning
-           ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< b (subst (λ k → toℕ x < k ) fin<asa c ))
-           ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (fin≤n x) c )
+           fdup01 with <-fcmp (fromℕ< a<sa) x 
+           ... | tri< a ¬b ¬c = {!!} -- begin
+                -- fromℕ< a ∷ list-less qs ≡⟨ cong₂ (λ j k → j ∷ k ) (lemma10 refl) (NList.lseq nlist) ⟩
+                -- fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa))) ∷ NList.ls nlist ∎  where open ≡-Reasoning
+           ... | tri≈ ¬a b ¬c = {!!} -- ⊥-elim ( nat-≡< b (subst (λ k → toℕ x < k ) fin<asa c ))
+           ... | tri> ¬a ¬b c = {!!} -- ⊥-elim ( nat-≤> (fin≤n x) c )
      fdup-phase1 : (qs : List (Fin (suc n)) ) → (fin-phase1  (fromℕ< a<sa) qs ≡ true)  ∨ NList n qs
      fdup-phase1 [] = case2  record { ls = [] ; lseq = refl ; ls< = case1 refl  }
      fdup-phase1 (x ∷ qs) with  <-fcmp (fromℕ< a<sa) x