# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1689674086 -32400
# Node ID 6ba2836177b441e18bde604867e10c6cf2a3db46
# Parent  57d007e9c581a3160c61e7daf0f736df2424e36b
fix fin<n

diff -r 57d007e9c581 -r 6ba2836177b4 automaton-in-agda/src/fin.agda
--- a/automaton-in-agda/src/fin.agda	Tue Jul 18 18:03:49 2023 +0900
+++ b/automaton-in-agda/src/fin.agda	Tue Jul 18 18:54:46 2023 +0900
@@ -12,9 +12,9 @@
 
 
 -- toℕ<n
-fin<n : {n : ℕ} {f : Fin n} → toℕ f < n
-fin<n {_} {zero} = s≤s z≤n
-fin<n {suc n} {suc f} = s≤s (fin<n {n} {f})
+fin<n : {n : ℕ} (f : Fin n) → toℕ f < n
+fin<n {_} zero = s≤s z≤n
+fin<n {suc n} (suc f) = s≤s (fin<n {n} f)
 
 -- toℕ≤n
 fin≤n : {n : ℕ} (f : Fin (suc n)) → toℕ f ≤ n
@@ -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
+pred<n {suc n} {suc f} (s≤s z≤n) = fin<n f
 
 fin<asa : {n : ℕ} → toℕ (fromℕ< {n} a<sa) ≡ n
 fin<asa = toℕ-fromℕ< nat.a<sa
@@ -139,7 +139,7 @@
 --    if the length is longer than n, we can find duplicate element as FDup-in-list 
 
 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  where
+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
@@ -230,7 +230,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)
diff -r 57d007e9c581 -r 6ba2836177b4 automaton-in-agda/src/finiteSetUtil.agda
--- a/automaton-in-agda/src/finiteSetUtil.agda	Tue Jul 18 18:03:49 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Tue Jul 18 18:54:46 2023 +0900
@@ -51,7 +51,7 @@
      End : (m : ℕ ) → (p : Q → Bool ) → Set
      End m p = (i : Fin finite) → m ≤ toℕ i → p (Q←F i )  ≡ false 
      first-end :  ( p : Q → Bool ) → End finite p
-     first-end p i i>n = ⊥-elim (nat-≤> i>n (fin<n {finite} {i}) )
+     first-end p i i>n = ⊥-elim (nat-≤> i>n (fin<n {finite} i) )
      next-end : {m : ℕ } → ( p : Q → Bool ) → End (suc m) p
               → (m<n : m < finite ) → p (Q←F (fromℕ< m<n )) ≡ false
               → End m p
@@ -583,10 +583,19 @@
    → (is-B : (a : A ) → Dec (Is B A (InjectiveF.f fi) a)  )
    → FiniteSet B
 inject-fin {A} {B} fa fi is-B with finite fa | inspect finite fa
-... | zero | record { eq = eq1 } = ?
+... | zero | record { eq = eq1 } = record {
+       finite = 0
+       ; Q←F = λ ()
+       ; F←Q = λ b → ⊥-elim ( lem00 b)
+       ; finiso→ = λ b → ⊥-elim ( lem00 b)
+       ; finiso← = λ ()
+       } where
+          lem00 : ( b : B) → ⊥
+          lem00 b with subst (λ k → Fin k ) eq1 (F←Q fa (InjectiveF.f fi b))
+          ... | ()
 ... | suc pfa | record { eq = eq1 } = record {
        finite = maxb
-       ; Q←F = λ fb → CountB.b (cb00 _ (fin<n {_} {fb}))
+       ; Q←F = λ fb → CountB.b (cb00 _ (fin<n {_} fb))
        ; F←Q = λ b → fromℕ< (cb<mb b)
        ; finiso→ = iso1
        ; finiso← = iso0
@@ -642,8 +651,15 @@
              ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | _ | _ = ⊥-elim (nat-≡< (sym b) (subst (λ k → _ < k ) (sym b₁) a<sa) )
              ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c | _ | _ = ⊥-elim (nat-≡< (sym b) (<-trans a<sa c))
              ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c | _ | _ = ⊥-elim (nat-≤> a (<-transʳ  c a<sa ) )
-             ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c | record { eq = eq0 } | record { eq = eq1 }  = ?
-             ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ | _ | _ = ?
+             ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c | record { eq = eq0 } | record { eq = eq1 } with is-B (Q←F fa (fromℕ< c))   
+             ... | yes  isb = refl-≤≡ (sym eq0)
+             ... | no  nisb = refl-≤≡ (sym eq0)
+             lem01 (suc i) | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ | record { eq = eq0 } | record { eq = eq1 } 
+                  with is-B (Q←F fa (fromℕ< c)) | is-B (Q←F fa (fromℕ< c₁)) 
+             ... | yes  isb0 | yes  isb1 = ≤-trans (refl-≤≡ (sym eq0)) a≤sa
+             ... | yes  isb0 | no  nisb1 = refl-≤≡ (sym eq0)
+             ... | no  nisb0 | yes  isb1 = ≤-trans (refl-≤≡ (sym eq0)) a≤sa
+             ... | no  nisb0 | no  nisb1 = refl-≤≡ (sym eq0)
 
     lem31 : (b : B) → 0 < count-B (toℕ (F←Q fa (f b)))
     lem31 b = lem32 (toℕ (F←Q fa (f b))) refl where
@@ -654,21 +670,21 @@
             lem33 : f b ≡ Q←F fa ( fromℕ< {0} 0<fa )
             lem33 = begin
               f b ≡⟨ sym (finiso→  fa _) ⟩
-              Q←F fa ( F←Q fa (f b))  ≡⟨ sym (cong (λ k → Q←F fa k)  ( fromℕ<-toℕ _ fin<n)) ⟩
-              Q←F fa ( fromℕ< fin<n )  ≡⟨ cong (λ k → Q←F fa k) (fromℕ<-cong _ _ eq fin<n 0<fa) ⟩
+              Q←F fa ( F←Q fa (f b))  ≡⟨ sym (cong (λ k → Q←F fa k)  ( fromℕ<-toℕ _ (fin<n _))) ⟩
+              Q←F fa ( fromℕ< (fin<n _) )  ≡⟨ cong (λ k → Q←F fa k) (fromℕ<-cong _ _ eq (fin<n _) 0<fa) ⟩
               Q←F fa ( fromℕ< {0} 0<fa ) ∎ where
                 open ≡-Reasoning
         lem32 (suc i) eq with <-cmp (finite fa) (suc i) | inspect count-B (suc i) 
-        ... | tri< a ¬b ¬c | _ = ⊥-elim ( nat-≡< eq (<-trans fin<n a) )
-        ... | tri≈ ¬a eq1 ¬c | _ = ⊥-elim ( nat-≡< eq (subst (λ k → toℕ (F←Q fa (f b)) < k ) eq1 fin<n ))
+        ... | tri< a ¬b ¬c | _ = ⊥-elim ( nat-≡< eq (<-trans (fin<n _) a) )
+        ... | tri≈ ¬a eq1 ¬c | _ = ⊥-elim ( nat-≡< eq (subst (λ k → toℕ (F←Q fa (f b)) < k ) eq1 (fin<n _)))
         ... | tri> ¬a ¬b c | record { eq = eq1 } with is-B (Q←F fa (fromℕ< c))   
         ... | yes isb = s≤s z≤n 
         ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = lem33 } ) where
             lem33 : f b ≡ Q←F fa ( fromℕ< c)
             lem33 = begin
               f b ≡⟨ sym (finiso→  fa _) ⟩
-              Q←F fa ( F←Q fa (f b))  ≡⟨ sym (cong (λ k → Q←F fa k)  ( fromℕ<-toℕ _ fin<n)) ⟩
-              Q←F fa ( fromℕ< fin<n )  ≡⟨ cong (λ k → Q←F fa k) (fromℕ<-cong _ _ eq fin<n c ) ⟩
+              Q←F fa ( F←Q fa (f b))  ≡⟨ sym (cong (λ k → Q←F fa k)  ( fromℕ<-toℕ _ (fin<n _))) ⟩
+              Q←F fa ( fromℕ< (fin<n _) )  ≡⟨ cong (λ k → Q←F fa k) (fromℕ<-cong _ _ eq (fin<n _) c ) ⟩
               Q←F fa ( fromℕ< c ) ∎ where
                 open ≡-Reasoning
  
@@ -679,7 +695,7 @@
         count-B (finite fa)   ∎ ) where
           open ≤-Reasoning
           lem02 : count-B (toℕ (F←Q fa (f b))) ≤ count-B (finite fa)
-          lem02 = count-B-mono (<to≤ (fin<n {_} {(F←Q fa (f b))})) 
+          lem02 = count-B-mono (<to≤ (fin<n {_} (F←Q fa (f b)))) 
 
     cb00 : (n : ℕ) → n < count-B (finite fa) → CountB n
     cb00 n n<cb = lem09 (finite fa) (count-B (finite fa)) (<-transˡ a<sa n<cb) refl where
@@ -713,31 +729,34 @@
                 toℕ (F←Q fa (f (Is.a isb))) ∎ where open ≡-Reasoning
         ... | case2 (s≤s lt) = lem09 i j lt (cong pred eq)
 
-    iso0 : (x : Fin maxb) → fromℕ< (cb<mb (CountB.b (cb00 (toℕ x) fin<n))) ≡ x 
+    iso0 : (x : Fin maxb) → fromℕ< (cb<mb (CountB.b (cb00 (toℕ x) (fin<n _)))) ≡ x 
     iso0 x = begin
-         fromℕ< (cb<mb (CountB.b (cb00 (toℕ x) fin<n))) ≡⟨ fromℕ<-cong _ _ ( begin 
-            pred (count-B (toℕ (F←Q fa (f (CountB.b (cb00 (toℕ x) fin<n))))))  ≡⟨ sym (cong (λ k → pred (count-B k)) (CountB.b=cn CB)) ⟩
+         fromℕ< (cb<mb (CountB.b (cb00 (toℕ x) (fin<n _)))) ≡⟨ fromℕ<-cong _ _ ( begin 
+            pred (count-B (toℕ (F←Q fa (f (CountB.b (cb00 (toℕ x) (fin<n _)))))))  ≡⟨ sym (cong (λ k → pred (count-B k)) (CountB.b=cn CB)) ⟩
             pred (count-B (CountB.cb CB))   ≡⟨ cong pred (CountB.cb=n CB) ⟩
             pred (suc (toℕ x))  ≡⟨ refl ⟩
-            toℕ x ∎ ) (cb<mb (CountB.b CB)) fin<n ⟩ 
-         fromℕ< (fin<n {_} {x}) ≡⟨ fromℕ<-toℕ _ (fin<n {_} {x}) ⟩ 
+            toℕ x ∎ ) (cb<mb (CountB.b CB)) (fin<n _) ⟩ 
+         fromℕ< (fin<n {_} x) ≡⟨ fromℕ<-toℕ _ (fin<n {_} x) ⟩ 
          x ∎ where
              open ≡-Reasoning
-             CB = cb00 (toℕ x) fin<n
+             CB = cb00 (toℕ x) (fin<n _)
 
-    iso1 : (b : B) → CountB.b (cb00 (toℕ (fromℕ< (cb<mb b))) fin<n) ≡ b
-    iso1 b with count-B (toℕ (fromℕ< (cb<mb b))) | inspect count-B (toℕ (fromℕ< (cb<mb b))) 
-    ... | zero | record { eq = eq1 } = ?
-    ... | suc n | record { eq = eq1 } =  begin
+    iso1 : (b : B) → CountB.b (cb00 (toℕ (fromℕ< (cb<mb b))) (fin<n _)) ≡ b
+    iso1 b = begin
          CountB.b CB ≡⟨ InjectiveF.inject fi (F←Q-inject fa (toℕ-injective (begin
             toℕ (F←Q fa (f (CountB.b CB))) ≡⟨ sym (CountB.b=cn CB) ⟩
-            CountB.cb CB ≡⟨ CountB.cb-inject CB _ fin<n isb lem30 ⟩
+            CountB.cb CB ≡⟨ CountB.cb-inject CB _ (fin<n _) isb lem30 ⟩
             toℕ (F←Q fa (f b)) ∎ ) ))  ⟩
          b ∎ where
              open ≡-Reasoning
-             CB = cb00 (toℕ (fromℕ< (cb<mb b))) fin<n
-             isb : Is B A f (Q←F fa (fromℕ< fin<n))
-             isb = ?
+             CB = cb00 (toℕ (fromℕ< (cb<mb b))) (fin<n _)
+             isb : Is B A f (Q←F fa (fromℕ< (fin<n {_} (F←Q fa (f b)) )))
+             isb = record { a = b ; fa=c = lem33 } where
+                 lem33 : f b ≡ Q←F fa (fromℕ< (fin<n (F←Q fa (f b)))) 
+                 lem33 = begin
+                     f b ≡⟨ sym (finiso→ fa _) ⟩
+                     Q←F fa (F←Q fa (f b))  ≡⟨ cong (Q←F fa) (sym (fromℕ<-toℕ _ (fin<n (F←Q fa (f b))))) ⟩
+                     Q←F fa (fromℕ< (fin<n (F←Q fa (f b))))  ∎ 
              lem30 : count-B (CountB.cb CB) ≡ count-B (toℕ (F←Q fa (InjectiveF.f fi b)))
              lem30 = begin
                  count-B (CountB.cb CB) ≡⟨ CountB.cb=n CB ⟩
@@ -746,6 +765,4 @@
                  count-B (toℕ (F←Q fa (f b))) ∎ 
 
 
-
-
 -- end