# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1624009884 -32400
# Node ID f1ee71c7c93a6f740049dbb33249755aef899548
# Parent  008309a9da919eae600d149547407e8f92a071fc
another method on fact<

diff -r 008309a9da91 -r f1ee71c7c93a automaton-in-agda/src/prime.agda
--- a/automaton-in-agda/src/prime.agda	Fri Jun 18 17:55:41 2021 +0900
+++ b/automaton-in-agda/src/prime.agda	Fri Jun 18 18:51:24 2021 +0900
@@ -85,44 +85,17 @@
      suc (1 + m * factorial m) ≤⟨ s≤s  (+-monoˡ-≤ _ (factorial≥1 {m})) ⟩
      suc (factorial m + m * factorial m)  ≡⟨ refl ⟩
      suc (factorial (suc m)) ∎  where open ≤-Reasoning
-  fact< : (n : ℕ) → 0 < n → n < suc (suc m) → Dividable n ( factorial (suc m) )
-  fact< n 0<n n<m = record { factor = F.f1 (fact1 m ) n 0<n n<m ; is-factor = last } where
-     record F (m : ℕ) : Set where
-        field
-          f1 : (n : ℕ ) → 0 < n →  n < suc (suc m ) → ℕ
-          is-f1 : (n : ℕ) (0<n : 0 < n ) →  (n<m : n < suc (suc m )) → f1 n 0<n n<m * n ≡ factorial (suc m)
-     init0 : (n : ℕ) → 0 < n → n < 2 → 1 * n ≡ factorial 1
-     init0 (suc zero) (s≤s lt) (s≤s (s≤s z≤n)) = refl
-     init : F 0
-     init = record { f1 = λ n lt lt1 → 1 ; is-f1 = λ n 0<n lt → init0 n 0<n lt } where
-     fact1 : (j : ℕ ) → F j
-     fact1 zero = init
-     fact1 (suc m) = record { f1 = fact2 ; is-f1 = fact3 }  where
-        fact2 : (n : ℕ ) →  0 < n →  n < suc (suc (suc m )) → ℕ
-        fact2 (suc zero) 0<n n<m = factorial (suc (suc m))
-        fact2 (suc (suc n)) (s≤s 0<n) n<m  with <-cmp (suc n) (suc m)
-        ... | tri< a ¬b ¬c = F.f1 (fact1 m) (suc n) (s≤s z≤n) (≤-trans a refl-≤s) -- suc (suc n) ≤ suc m → suc n < suc (suc m)
-        ... | tri≈ ¬a refl ¬c = F.f1 (fact1 m) (suc m) (s≤s z≤n) a<sa * suc m
-        ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (s≤s c) n<m ) -- suc (suc m) ≤ suc n
-        fact3 : (n : ℕ ) (0<n : 0 < n) (n<m : n < suc (suc (suc m))) → fact2 n 0<n n<m * n ≡ factorial (suc (suc m))
-        fact3 n 0<n n<m with  fact2 n 0<n n<m | inspect (fact2 n 0<n ) n<m  
-        fact3 (suc zero) 0<n n<m     | t | record { eq = refl } = m*1=m
-        fact3 (suc (suc n))  0<n n<m | t | record { eq = eq1 }  with <-cmp (suc n) (suc m)
-        ... | tri< a ¬b ¬c = {!!}
-        ... | tri≈ ¬a refl ¬c = begin
-            t * suc (suc m) ≡⟨ cong ( λ k → k * suc (suc m)) (sym eq1) ⟩
-            fact2 (suc (suc n)) 0<n n<m * suc (suc n) ≡⟨ {!!} ⟩
-            suc (suc m) * (F.f1 (fact1 m) (suc m) (s≤s z≤n) a<sa * suc m) ≡⟨ cong ( λ k → suc (suc m) * k ) (F.is-f1 (fact1 m) (suc n) (s≤s z≤n) a<sa) ⟩
-            suc (suc m) * factorial (suc m) ≡⟨ refl ⟩
-            factorial (suc (suc m)) ∎  where open ≡-Reasoning
-        ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (s≤s c) n<m ) -- suc (suc m) ≤ suc n
-     last :  F.f1 (fact1 m) n 0<n n<m * n + 0 ≡ factorial (suc m)
-     last = begin
-         F.f1 (fact1 m ) n 0<n n<m * n + 0 ≡⟨ +-comm _ 0 ⟩
-         F.f1 (fact1 m ) n 0<n n<m * n ≡⟨  F.is-f1 (fact1 m) n 0<n n<m ⟩
-         factorial (suc m) ∎  where open ≡-Reasoning
+  fact< : (m n : ℕ) → 0 < n → n < suc (suc m) → Dividable n ( factorial (suc m) )
+  fact< zero 1 0<n (s≤s (s≤s z≤n)) = record { factor = 1 ; is-factor = refl }
+  fact< (suc m) (suc zero) 0<n n<m = record { factor = factorial (suc (suc m)) ; is-factor = {!!} }
+  fact< (suc m) (suc (suc n)) 0<n n<m with <-cmp (suc (suc n)) (suc (suc m))
+  ... | tri< a ¬b ¬c = record { factor = suc (suc m) * Dividable.factor fact1 ; is-factor = {!!} } where
+      fact1 : Dividable (suc (suc n))  (factorial (suc m ))
+      fact1 = fact< m (suc (suc n)) 0<n a 
+  ... | tri≈ ¬a b ¬c = record { factor = factorial (suc m)  ; is-factor = {!!} }
+  ... | tri> ¬a ¬b c = {!!}
   fact : (n : ℕ) → Prime n → Dividable n ( factorial (suc m) )
-  fact n p = fact< n (<-trans (s≤s z≤n) (Prime.p>0 p)) ( prime<max n p )
+  fact n p = fact< m n (<-trans (s≤s z≤n) (Prime.p>0 p)) ( prime<max n p )
   -- div+1 : { i k : ℕ } → k > 1 →  Dividable k i →  ¬ Dividable k (suc i)
   getPrime : ⊥
   getPrime with PrimeP ( suc (factorial (suc m)) )