Mercurial > hg > Members > kono > Proof > automaton

changeset 193:875eb1fa9694

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dividable reorganzaiton
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 16 Jun 2021 08:36:40 +0900
parents 8007206a5a19
children ee25ec7a27f6
files automaton-in-agda/src/gcd.agda
diffstat 1 files changed, 31 insertions(+), 26 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Tue Jun 15 22:30:13 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Wed Jun 16 08:36:40 2021 +0900
@@ -20,10 +20,16 @@
 record Dividable (n m : ℕ ) : Set where
    field 
       factor : ℕ
+      f>1 : factor > 1
       is-factor : factor * n + 0 ≡ m 
 
 open Factor
 
+DtoF : {n m : ℕ} → Dividable n m → Factor n m
+DtoF {n} {m} record { factor = f ; f>1 = f>1 ; is-factor = fa } = record { factor = f ; remain = 0 ; is-factor = fa }
+
+FtoD : {n m : ℕ} → (fc : Factor n m) → factor fc > 1 → remain fc ≡ 0 → Dividable n m 
+FtoD {n} {m} record { factor = f ; remain = r ; is-factor = fa } f>1 refl = record { factor = f ; f>1 = f>1  ; is-factor = fa }
 
 decf : { n k : ℕ } → ( x : Factor k (suc n) ) → Factor k n
 decf {n} {k} record { factor = f ; remain = r ; is-factor = fa } = 
@@ -59,24 +65,24 @@
 
 decf-step : {i k i0 : ℕ } → (if : Factor k (suc i)) → (i0f : Factor k i0) → Dividable k (suc i - remain if)  → Dividable k (i - remain (decf {i} {k} if))
 decf-step {i} {k} {i0} if i0f div = 
-  decf-step1 {i} {k} {i0} (factor if) (remain if) (is-factor if) i0f div where
-   decf-step1 : {i k i0 : ℕ } →  (f r : ℕ) → (fa : f * k + r ≡ suc i) →  (i0f : Factor k i0)
+  decf-step1 {i} {k} {i0} (factor if) (remain if) (is-factor if) {!!} i0f div where
+   decf-step1 : {i k i0 : ℕ } →  (f r : ℕ) → (fa : f * k + r ≡ suc i) → f > 1  →  (i0f : Factor k i0)
         → Dividable k (suc i - r)  → Dividable k (i - remain (decf record {factor = f ; remain = r ; is-factor = fa}))
-   decf-step1 {i} {k} {i0}  f (suc r) fa i0f div = 
-      record { factor = f ;  is-factor = ( --  f * k + suc r ≡ suc i → f * k + suc r ≡ suc i
+   decf-step1 {i} {k} {i0}  f (suc r) fa f>1 i0f div = 
+      record { factor = f ;  f>1 = {!!} ; is-factor = ( --  f * k + suc r ≡ suc i → f * k + suc r ≡ suc i
         begin f * k + 0 ≡⟨ +-comm _ 0 ⟩
         f * k ≡⟨ sym ( x=y+z→x-z=y {suc i} {_} {suc r} (sym fa) ) ⟩
         suc i - suc r ≡⟨ refl ⟩
         i - r ≡⟨ refl ⟩
          (i - remain (decf (record { factor = f ; remain = suc r ; is-factor = fa }))) ∎ ) }  where
             open ≡-Reasoning
-   decf-step1 {i} {zero} {i0} (suc f) zero fa i0f div = ⊥-elim (nat-≡< fa (
+   decf-step1 {i} {zero} {i0} (suc f) zero fa f>1 i0f div = ⊥-elim (nat-≡< fa (
         begin suc (suc f * zero + zero) ≡⟨ cong suc (+-comm _ zero)  ⟩
         suc (f * 0) ≡⟨ cong suc (*-comm f zero)  ⟩
         suc zero ≤⟨ s≤s z≤n ⟩
         suc i ∎ )) where open ≤-Reasoning  -- suc (0 + i) ≡ i0
-   decf-step1 {i} {suc k} {i0} (suc f)  zero fa i0f div = 
-      record { factor = f ;  is-factor = ( --  suc (k + f * suc k + zero) ≡ suc i →  f * suc k + 0 ≡ i - k 
+   decf-step1 {i} {suc k} {i0} (suc f)  zero fa f>1 i0f div = 
+      record { factor = f ;  f>1 = {!!} ; is-factor = ( --  suc (k + f * suc k + zero) ≡ suc i →  f * suc k + 0 ≡ i - k 
         begin f * suc k + 0 ≡⟨ sym ( x=y+z→x-z=y {i} {_} {k} (begin
           i ≡⟨ sym (cong pred fa) ⟩
           pred (suc f * suc k + zero) ≡⟨ refl ⟩
@@ -120,31 +126,30 @@
 nfk : (k : ℕ ) → k > 1 → ¬ (Dividable k 1)
 nfk k k>1 fk1 = ⊥-elim ( nat-≡< (sym (Dividable.is-factor fk1))  {!!} )
 
-gcd-gt : ( i i0 j j0 k : ℕ ) → k > 1 → (if : Factor k i) (i0f : Factor k i0 ) (jf : Factor k j ) (j0f : Factor k j0)
-   → remain i0f ≡ 0 → remain j0f ≡  0
+gcd-gt : ( i i0 j j0 k : ℕ ) → k > 1 → (if : Factor k i) (i0f : Dividable k i0 ) (jf : Factor k j ) (j0f : Dividable k j0)
    → Dividable k (i - remain if) → Dividable k (j - remain jf) 
    → Dividable k ( gcd1 i i0 j j0 ) 
-gcd-gt zero i0 zero j0 k k>1 if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 with <-cmp i0 j0
-... | tri< a ¬b ¬c = record { factor = factor i0f ; is-factor = ifk0 i0 k i0f i0=0 } 
-... | tri≈ ¬a refl ¬c = record { factor = factor i0f ;  is-factor = ifk0 i0 k i0f i0=0 } 
-... | tri> ¬a ¬b c = record { factor = factor j0f ;  is-factor = ifk0 j0 k j0f j0=0 } 
-gcd-gt zero i0 (suc zero) j0 k k>1 if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} -- can't happen
-gcd-gt zero zero (suc (suc j)) j0 k k>1 if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = record { factor = factor j0f ; is-factor = ifk0 j0 k j0f j0=0 } 
-gcd-gt zero (suc i0) (suc (suc j)) j0 k k>1 if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 =  
-    gcd-gt i0 (suc i0) (suc j) (suc (suc j))  k k>1 (decf i0f) i0f (decf jf) jf i0=0 {!!} ? (decf-step jf j0f jr=j0 )
-gcd-gt (suc zero) i0 zero j0 k k>1 if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} -- can't happen
-gcd-gt (suc (suc i)) i0 zero zero k k>1 if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = record { factor = factor i0f ; is-factor = ifk0 i0 k i0f i0=0 } 
-gcd-gt (suc (suc i)) i0 zero (suc j0) k k>1 if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 =
-     gcd-gt (suc i) (suc (suc i)) j0 (suc j0) k k>1 (decf if) if (decf j0f) j0f {!!}  j0=0 (decf-step if i0f ir=i0 ) {!!}
-gcd-gt (suc zero) i0 (suc j) j0 k k>1 if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 =  
-     gcd-gt zero i0 j j0 k k>1 (decf if) i0f (decf jf) j0f i0=0 j0=0 (decf-step if i0f ir=i0 ) (decf-step jf j0f jr=j0 )
-gcd-gt (suc (suc i)) i0 (suc j) j0 k k>1 if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = 
-     gcd-gt (suc i) i0 j j0 k k>1 (decf if) i0f (decf jf) j0f i0=0 j0=0 (decf-step if i0f ir=i0 ) (decf-step jf j0f jr=j0 )
+gcd-gt zero i0 zero j0 k k>1 if i0f jf j0f ir=i0 jr=j0 with <-cmp i0 j0
+... | tri< a ¬b ¬c = record { factor = Dividable.factor i0f ; f>1 = {!!} ; is-factor = ifk0 i0 k {!!} {!!} } 
+... | tri≈ ¬a refl ¬c = record { factor = Dividable.factor i0f ; f>1 = {!!} ;  is-factor = ifk0 i0 k {!!} {!!} } 
+... | tri> ¬a ¬b c = record { factor = Dividable.factor j0f ; f>1 = {!!} ;  is-factor = ifk0 j0 k {!!} {!!} } 
+gcd-gt zero i0 (suc zero) j0 k k>1 if i0f jf j0f ir=i0 jr=j0 = {!!} -- can't happen
+gcd-gt zero zero (suc (suc j)) j0 k k>1 if i0f jf j0f ir=i0 jr=j0 = record { factor = Dividable.factor j0f ; f>1 = {!!} ; is-factor = ifk0 j0 k {!!} {!!} } 
+gcd-gt zero (suc i0) (suc (suc j)) j0 k k>1 if i0f jf j0f ir=i0 jr=j0 =  
+    gcd-gt i0 (suc i0) (suc j) (suc (suc j))  k k>1 (decf {!!}) i0f (decf {!!}) {!!} {!!} (decf-step jf {!!} jr=j0 )
+gcd-gt (suc zero) i0 zero j0 k k>1 if i0f jf j0f ir=i0 jr=j0 = {!!} -- can't happen
+gcd-gt (suc (suc i)) i0 zero zero k k>1 if i0f jf j0f ir=i0 jr=j0 = record { factor = Dividable.factor i0f ; f>1 = {!!} ; is-factor = ifk0 i0 k {!!} {!!} } 
+gcd-gt (suc (suc i)) i0 zero (suc j0) k k>1 if i0f jf j0f ir=i0 jr=j0 =
+     gcd-gt (suc i) (suc (suc i)) j0 (suc j0) k k>1 (decf if) {!!} (decf {!!}) j0f (decf-step if {!!} ir=i0 ) {!!}
+gcd-gt (suc zero) i0 (suc j) j0 k k>1 if i0f jf j0f ir=i0 jr=j0 =  
+     gcd-gt zero i0 j j0 k k>1 (decf if) i0f (decf jf) j0f (decf-step if {!!} ir=i0 ) (decf-step jf {!!} jr=j0 )
+gcd-gt (suc (suc i)) i0 (suc j) j0 k k>1 if i0f jf j0f ir=i0 jr=j0 = 
+     gcd-gt (suc i) i0 j j0 k k>1 (decf if) i0f (decf jf) j0f (decf-step if {!!} ir=i0 ) (decf-step jf {!!} jr=j0 )
 
 gcd-div : ( i j k : ℕ ) → k > 1 → (if : Factor k i) (jf : Factor k j ) 
    → remain if ≡ 0 → remain jf ≡  0
    → Dividable k ( gcd i  j ) 
-gcd-div i j k k>1 if jf i0=0 j0=0 = gcd-gt i i j j k k>1 if if jf jf i0=0 j0=0 {!!} {!!} where
+gcd-div i j k k>1 if jf i0=0 j0=0 = gcd-gt i i j j k k>1 if {!!} jf {!!} {!!} {!!} where
     gf4 : {m n : ℕ} → n ≡ 0  →  n + m ≡ m
     gf4 {m} {n} eq = begin
         n + m ≡⟨ cong (λ k → k + m) eq  ⟩