Mercurial > hg > Members > kono > Proof > automaton

changeset 285:6e85b8b0d8db

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove ls<n
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 28 Dec 2021 00:28:29 +0900
parents c9f20dec63ad
children f49c6d768e19
files automaton-in-agda/src/fin.agda
diffstat 1 files changed, 27 insertions(+), 31 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/fin.agda	Mon Dec 27 21:45:00 2021 +0900
+++ b/automaton-in-agda/src/fin.agda	Tue Dec 28 00:28:29 2021 +0900
@@ -153,27 +153,16 @@
 ... | tri≈ ¬a b ¬c = list-less ls
 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (fin≤n i) c )
 
-record NList (n m : ℕ) (qs : List (Fin (suc n))) : Set where
+record NList (n : ℕ) (qs : List (Fin (suc n))) : Set where
   field
      ls : List (Fin n)
      lseq : list-less qs ≡ ls
-     ls>n : m + length ls > n
-
 
 fin-dup-in-list>n : {n : ℕ } → (qs : List (Fin n))  → (len> : length qs > n ) → FDup-in-list n qs
 fin-dup-in-list>n {zero} [] ()
 fin-dup-in-list>n {zero} (() ∷ qs) lt
 fin-dup-in-list>n {suc n} qs lt = fdup-phase0 where
      open import Level using ( Level )
-     mapleneq : {n : Level} {a b : Set n} { x : List a } {f : a → b} → length (map f x) ≡ length x
-     mapleneq {_} {_} {_} {[]} {f} = refl
-     mapleneq {_} {_} {_} {x ∷ x₁} {f} = cong suc (mapleneq  {_} {_} {_} {x₁})
-     lt-conv : {l : Level} {a : Set l} {m n : ℕ } ( qs : List a ) → m + suc ( length qs ) > n → suc m + length qs > n
-     lt-conv {_} {_} {m} {n} qs lt = begin
-         suc n ≤⟨ lt ⟩
-         m + suc (length qs) ≡⟨ sym (+-assoc m 1 _)  ⟩
-         (m + 1) + length qs ≡⟨ cong (λ k → k + length qs) (+-comm m _ ) ⟩
-         suc m + length qs ∎  where open ≤-Reasoning
      fdup+1 : (qs : List (Fin (suc n))) (i : Fin n) → fin-dup-in-list i (list-less qs) ≡ true → fin-dup-in-list (fin+1 i) qs ≡ true 
      fdup+1 qs i p = f1-phase1 qs p where
           f1-phase2 : (qs : List (Fin (suc n)) ) → fin-phase2 i (list-less qs) ≡ true → fin-phase2 (fin+1 i) qs ≡ true 
@@ -187,31 +176,38 @@
           ... | tri< a ¬b ¬c = f1-phase1 qs {!!}
           ... | tri≈ ¬a b ¬c = f1-phase2 qs {!!}
           ... | tri> ¬a ¬b c = f1-phase1 qs {!!}
-     fdup-phase2 : (qs : List (Fin (suc n)) ) → {m : ℕ} → m + length qs > n
-         → ( fin-phase2 (fromℕ< a<sa ) qs ≡ true )  ∨ NList n m qs
-     fdup-phase2 [] {m} lt = case2  record { ls = [] ; lseq = refl ; ls>n = lt }
-     fdup-phase2 (x ∷ qs) {m} lt with <-fcmp (fromℕ< a<sa) x
+     fdup-phase2 : (qs : List (Fin (suc n)) ) 
+         → ( fin-phase2 (fromℕ< a<sa ) qs ≡ true )  ∨ NList n qs
+     fdup-phase2 []  = case2  record { ls = [] ; lseq = refl }
+     fdup-phase2 (x ∷ qs)  with <-fcmp (fromℕ< a<sa) x
      ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k) (sym fin<asa) fin<n ))
-     fdup-phase2 (x ∷ qs) {m} lt | tri≈ ¬a b ¬c = case1 refl
-     fdup-phase2 (x ∷ qs) {m} lt | tri> ¬a ¬b c with fdup-phase2 qs {suc m} (lt-conv qs lt)
+     fdup-phase2 (x ∷ qs)  | tri≈ ¬a b ¬c = case1 refl
+     fdup-phase2 (x ∷ qs)  | tri> ¬a ¬b c with fdup-phase2 qs 
      ... | case1 p = case1 p
-     ... | case2 nlist = case2 record { ls = x<y→fin-1 c ∷ NList.ls nlist ; lseq = {!!} ; ls>n = {!!} }
-     fdup-phase1 : (qs : List (Fin (suc n)) ) → {m : ℕ} → m + length qs > n → (fin-phase1  (fromℕ< a<sa) qs ≡ true)  ∨ NList n m qs
-     fdup-phase1 [] {m} lt = case2  record { ls = [] ; lseq = refl ; ls>n = lt }
-     fdup-phase1 (x ∷ qs) {m} lt with  <-fcmp (fromℕ< a<sa) x
-     fdup-phase1 (x ∷ qs) {m} lt | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k) (sym fin<asa) fin<n ))
-     fdup-phase1 (x ∷ qs) {m} lt | tri≈ ¬a b ¬c with fdup-phase2 qs {m} ?
+     ... | case2 nlist = case2 record { ls = x<y→fin-1 c ∷ NList.ls nlist ; lseq = fdup01 } 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 )
+     fdup-phase1 : (qs : List (Fin (suc n)) ) → (fin-phase1  (fromℕ< a<sa) qs ≡ true)  ∨ NList n qs
+     fdup-phase1 [] = case2  record { ls = [] ; lseq = refl }
+     fdup-phase1 (x ∷ qs) with  <-fcmp (fromℕ< a<sa) x
+     fdup-phase1 (x ∷ qs) | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k) (sym fin<asa) fin<n ))
+     fdup-phase1 (x ∷ qs) | tri≈ ¬a b ¬c with fdup-phase2 qs 
      ... | case1 p = case1 p
-     ... | case2 nlist = case2 record { ls = NList.ls nlist ; lseq = {!!} ; ls>n = NList.ls>n nlist }
-     fdup-phase1 (x ∷ qs) {m} lt | tri> ¬a ¬b c with fdup-phase1 qs {m} {!!}
+     ... | case2 nlist = case2 record { ls = NList.ls nlist ; lseq = {!!} } where
+           fdup03 : list-less (x ∷ qs) ≡ NList.ls nlist
+           fdup03 = {!!}
+     fdup-phase1 (x ∷ qs) | tri> ¬a ¬b c with fdup-phase1 qs  
      ... | case1 p = case1 p
-     ... | case2 nlist = case2 record { ls = x<y→fin-1 c ∷ NList.ls nlist ; lseq = {!!} ; ls>n = {!!} }
+     ... | case2 nlist = case2 record { ls = x<y→fin-1 c ∷ NList.ls nlist ; lseq = {!!} }
      fdup-phase0 : FDup-in-list (suc n) qs 
-     fdup-phase0 with fdup-phase1 qs {0} ( <-trans a<sa lt ) 
+     fdup-phase0 with fdup-phase1 qs 
      ... | case1 dup   = record { dup =  fromℕ< a<sa ; is-dup = dup }
      ... | case2 nlist = record { dup = fin+1 (FDup-in-list.dup fdup)
               ; is-dup = fdup+1 qs (FDup-in-list.dup fdup) (FDup-in-list.is-dup fdup) } where
-           flt :  length (list-less qs) > n
-           flt = subst ( λ k → length k > n ) (sym (NList.lseq nlist)) ( NList.ls>n nlist )
            fdup : FDup-in-list n (list-less qs)
-           fdup = fin-dup-in-list>n (list-less qs) flt
+           fdup = fin-dup-in-list>n (list-less qs) {!!}