--- a/automaton-in-agda/src/fin.agda	Thu Aug 10 09:59:47 2023 +0900
+++ b/automaton-in-agda/src/fin.agda	Sun Sep 24 11:32:01 2023 +0900
@@ -1,9 +1,9 @@
-{-# OPTIONS --allow-unsolved-metas #-} 
+{-# OPTIONS --cubical-compatible  --safe #-}
 
 module fin where
 
 open import Data.Fin hiding (_<_ ; _≤_ ; _>_ ; _+_ )
-open import Data.Fin.Properties as DFP hiding (≤-trans ;  <-trans ;  ≤-refl  ) renaming ( <-cmp to <-fcmp )
+open import Data.Fin.Properties hiding (≤-trans ;  <-trans ;  ≤-refl  ) renaming ( <-cmp to <-fcmp )
 open import Data.Nat
 open import Data.Nat.Properties
 open import logic
@@ -23,7 +23,7 @@
 
 pred<n : {n : ℕ} {f : Fin (suc n)} → n > 0  → Data.Nat.pred (toℕ f) < n
 pred<n {suc n} {zero} (s≤s z≤n) = s≤s z≤n
-pred<n {suc n} {suc f} (s≤s z≤n) = fin<n f
+pred<n {suc n} {suc f} (s≤s z≤n) = fin<n _
 
 fin<asa : {n : ℕ} → toℕ (fromℕ< {n} a<sa) ≡ n
 fin<asa = toℕ-fromℕ< nat.a<sa
@@ -33,17 +33,20 @@
 toℕ→from {0} {zero} refl = refl
 toℕ→from {suc n} {suc x} eq = cong (λ k → suc k ) ( toℕ→from {n} {x} (cong (λ k → Data.Nat.pred k ) eq ))
 
-0≤fmax : {n : ℕ } → (# 0) Data.Fin.≤ fromℕ< {n} a<sa
-0≤fmax  = subst (λ k → 0 ≤ k ) (sym (toℕ-fromℕ< a<sa)) z≤n
+-- 0≤fmax : {n : ℕ } → (# 0) Data.Fin.≤ fromℕ< {n} a<sa
+-- 0≤fmax {n} = ?
 
-0<fmax : {n : ℕ } → (# 0) Data.Fin.< fromℕ< {suc n} a<sa
-0<fmax = subst (λ k → 0 < k ) (sym (toℕ-fromℕ< a<sa)) (s≤s z≤n)
+-- 0<fmax : {n : ℕ } → (# 0) Data.Fin.< fromℕ< {suc n} a<sa
+-- 0<fmax {n} = subst (λ k → 0 < k ) (sym (toℕ-fromℕ< {suc n} {suc (suc n)} a<sa)) (s≤s z≤n)
 
 -- toℕ-injective
 i=j : {n : ℕ} (i j : Fin n) → toℕ i ≡ toℕ j → i ≡ j
 i=j {suc n} zero zero refl = refl
 i=j {suc n} (suc i) (suc j) eq = cong ( λ k → suc k ) ( i=j i j (cong ( λ k → Data.Nat.pred k ) eq) )
 
+fin1≡0 : (f : Fin 1) → # 0 ≡ f
+fin1≡0 zero = refl
+
 -- raise 1
 fin+1 :  { n : ℕ } → Fin n → Fin (suc n)
 fin+1  zero = zero 
@@ -51,9 +54,6 @@
 
 open import Data.Nat.Properties as NatP  hiding ( _≟_ )
 
-fin1≡0 : (f : Fin 1) → # 0 ≡ f
-fin1≡0 zero = refl
-
 fin+1≤ : { i n : ℕ } → (a : i < n)  → fin+1 (fromℕ< a) ≡ fromℕ< (<-trans a a<sa)
 fin+1≤ {0} {suc i} (s≤s z≤n) = refl
 fin+1≤ {suc n} {suc (suc i)} (s≤s (s≤s a)) = cong (λ k → suc k ) ( fin+1≤ {n} {suc i} (s≤s a) )
@@ -90,32 +90,39 @@
 lemma12 {zero} {suc m} (s≤s z≤n) zero refl = refl
 lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl =  cong suc ( lemma12 {n} {m} n<m f refl  ) 
 
-open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+-- this requires K
+--
+-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
 -- <-irrelevant
-<-nat=irr : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n  
-<-nat=irr {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
-<-nat=irr {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( <-nat=irr {i} {i} {n} refl  )
+-- <-nat=irr : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n  
+-- <-nat=irr {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
+-- <-nat=irr {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( <-nat=irr {i} {i} {n} refl  )
+
+-- lemma8 : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n  
+-- lemma8 {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
+-- lemma8 {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8 {i} {i} {n} refl  )
 
-lemma8 : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n  
-lemma8 {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
-lemma8 {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8 {i} {i} {n} refl  )
+lemma10 : {n i j  : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n }  → fromℕ< i<n ≡ fromℕ< j<n
+lemma10 {.(suc _)} {zero} {zero} refl {s≤s z≤n} {s≤s z≤n} = refl
+lemma10 {suc n} {suc i} {suc i} refl {s≤s i<n} {s≤s j<n} = cong suc (lemma10 {n} {i} {i} refl {i<n} {j<n})
 
--- fromℕ<-irrelevant 
-lemma10 : {n i j  : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n }  → fromℕ< i<n ≡ fromℕ< j<n
-lemma10 {n} refl  = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8 refl  ))
+fpred-comm : {n : ℕ } → (x : Fin n) → toℕ (Data.Fin.pred x) ≡ toℕ x ∸ 1
+fpred-comm {suc n} zero = refl
+fpred-comm {suc n} (suc x) = begin
+       toℕ (Data.Fin.pred (suc x)) ≡⟨ sym ( toℕ-fromℕ< _ ) ⟩
+       toℕ (fromℕ< (fin<n _) ) ≡⟨ cong toℕ (lemma10 (toℕ-inject₁ _ ) ) ⟩
+       toℕ (fromℕ< (<-trans (fin<n _) a<sa) ) ≡⟨  toℕ-fromℕ< _ ⟩
+       toℕ (suc x) ∸ 1 ∎  where open ≡-Reasoning
 
-lemma31 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c
-lemma31 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl) 
+-- lemma31 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c
+-- lemma31 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl) 
 
 -- toℕ-fromℕ<
 lemma11 : {n m : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡ toℕ x
 lemma11 {n} {m} {x} n<m  = begin
-              toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m))
-           ≡⟨ toℕ-fromℕ< _ ⟩
-              toℕ x
-           ∎  where
-               open ≡-Reasoning
+      toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡⟨ toℕ-fromℕ< _ ⟩
+      toℕ x ∎  where open ≡-Reasoning
 
 x<y→fin-1 : {n : ℕ } → { x y : Fin (suc n)} →  toℕ x < toℕ y  → Fin n
 x<y→fin-1 {n} {x} {y} lt = fromℕ< (≤-trans lt (fin≤n _ ))
@@ -140,12 +147,21 @@
 -- find duplicate element in a List (Fin n)
 --
 --    if the length is longer than n, we can find duplicate element as FDup-in-list 
+--
+--  How about do it in ℕ ?
 
-list2func : (n : ℕ) → (x : List (Fin n)) → n < length x → Fin (length x) → Fin n
-list2func n x n<l y = lf00 (toℕ y) x (fin<n y)  where
-     lf00 : (i : ℕ) → (x : List (Fin n)) → i < length x → Fin n
-     lf00 zero (x ∷ t) lt = x
-     lf00 (suc i) (x ∷ t) (s≤s lt) = lf00 i t lt
+-- fin-count : { n : ℕ }  (q : Fin n) (qs : List (Fin n) ) → ℕ
+-- fin-count q p[ = 0
+-- fin-count q (q0 ∷ qs ) with <-fcmp q q0 
+-- ... | tri-e = suc (fin-count q qs)
+-- ... | false = fin-count q qs
+
+-- fin-not-dup-in-list : { n : ℕ}  (qs : List (Fin n) ) → Set
+-- fin-not-dup-in-list {n} qs = (q : Fin n) → fin-count q ≤ 1
+
+-- this is far easier
+-- fin-not-dup-in-list→len<n : { n : ℕ}  (qs : List (Fin n) ) → ( (q : Fin n) → fin-not-dup-in-list qs q) → length qs ≤ n
+-- fin-not-dup-in-list→len<n = ?
 
 fin-phase2 : { n : ℕ }  (q : Fin n) (qs : List (Fin n) ) → Bool  -- find the dup
 fin-phase2 q [] = false
@@ -175,6 +191,11 @@
 ... | tri≈ ¬a b ¬c = list-less ls
 ... | tri> ¬a ¬b c = x<y→fin-1 c ∷ list-less ls
 
+fin010 : {n m : ℕ } {x : Fin n} (c : suc (toℕ x) ≤ toℕ (fromℕ< {m} a<sa) ) → toℕ (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) ≡ toℕ x
+fin010 {_} {_} {x} c = begin 
+           toℕ (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa))))  ≡⟨ toℕ-fromℕ< _ ⟩
+           toℕ x  ∎   where open ≡-Reasoning
+
 ---
 ---  if List (Fin n) is longer than n, there is at most one duplication
 ---
@@ -233,7 +254,7 @@
           ... | tri< a ¬b ¬c₁ = f1-phase1 qs p (case2 q1)
           ... | tri≈ ¬a₁ b₁ ¬c₁ = ⊥-elim (fdup-10 b b₁) where
                fdup-10 : fromℕ< a<sa ≡ x → fin+1 i ≡ x → ⊥
-               fdup-10 eq eq1 = nat-≡< (cong toℕ (trans eq1 (sym eq))) (subst₂ (λ j k → j < k ) (sym fin+1-toℕ) (sym fin<asa) (fin<n _)) 
+               fdup-10 eq eq1 = nat-≡< (cong toℕ (trans eq1 (sym eq))) (subst₂ (λ j k → j < k ) (sym fin+1-toℕ) (sym fin<asa) (fin<n _) ) 
           ... | tri> ¬a₁ ¬b c = f1-phase1 qs p (case2 q1)
           f1-phase1 (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-phase1 qs p (case1 q1)
@@ -259,9 +280,9 @@
           ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
           ... | 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
+     fdup-phase0 with fin-dup-in-list (fromℕ< a<sa) qs in eq 
+     ... | true  = record { dup = fromℕ< a<sa ; is-dup = eq }
+     ... | false = fdup+1 qs (FDup-in-list.dup fdup) eq (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
@@ -283,6 +304,6 @@
                ... | 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)
+           fdup = fin-dup-in-list>n (list-less qs) (fless qs lt eq)
 
 --