Members/kono/Proof/automaton: automaton-in-agda/src/fin.agda comparison

comparison automaton-in-agda/src/fin.agda @ 294:248711134141

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Wed, 29 Dec 2021 19:08:28 +0900
parents	8992ecc40eb1
children	16e47a3c4eda

comparison

equal deleted inserted replaced

-:8992ecc40eb1
+:248711134141
 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 )
+--  make a dup from one level below
 fdup+1 : (qs : List (Fin (suc n))) (i : Fin n) →  fin-dup-in-list  (fromℕ< a<sa ) qs ≡ false
 → fin-dup-in-list i (list-less qs) ≡ true → FDup-in-list (suc n) qs
 fdup+1 qs i ne p = record { dup = fin+1 i ; is-dup = f1-phase1 qs p (case1 ne) } where
+-- we have two loops on the max element and the current level. The disjuction means the phases may differ.
 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 _ )))
 f1-phase2 (x ∷ qs) p (case1 q1) | tri≈ ¬a b ¬c with <-fcmp (fin+1 i) x
 ... | tri< a ¬b ¬c₁ = f1-phase2 qs p (case2 q1)
 ... | tri≈ ¬a₁ b₁ ¬c₁ = refl
 ... | tri> ¬a₁ ¬b c = f1-phase2 qs p (case2 q1)
+-- two fcmp is only different in the size of Fin, but to develop both f1-phase and list-less both fcmps are required
 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₁  = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
 ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
 ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁  = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) fin+1-toℕ (sym (toℕ-fromℕ< _)) a ))
 ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase1 qs p (case2 q1)
 fdup-phase0 : FDup-in-list (suc n) qs
 fdup-phase0 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 } = fdup+1 qs (FDup-in-list.dup fdup) ne (FDup-in-list.is-dup fdup)  where
+-- if no dup in the max element, the list without the element is only one length shorter
 fless : (qs : List (Fin (suc n))) → length qs > suc n  → fin-dup-in-list (fromℕ< a<sa) qs ≡ false → n < length (list-less qs)
 fless qs lt p = fl-phase1 n qs lt p where
 fl-phase2 : (n1 : ℕ) (qs : List (Fin (suc n))) → length qs > n1  → fin-phase2 (fromℕ< a<sa) qs ≡ false → n1 < length (list-less qs)
 fl-phase2 zero (x ∷ qs) (s≤s lt) p 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 = s≤s z≤n
 fl-phase1 (suc n1) (x ∷ qs) (s≤s lt) p 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 = fl-phase2 (suc n1) qs lt p
 ... | tri> ¬a ¬b c = s≤s ( fl-phase1 n1 qs lt p )
+-- if the list without the max element is only one length shorter, we can recurse
 fdup : FDup-in-list n (list-less qs)
 fdup = fin-dup-in-list>n (list-less qs) (fless qs lt ne)

Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/fin.agda @ 294:248711134141