Mercurial > hg > Members > kono > Proof > automaton

changeset 250:89120ac828b7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 29 Jun 2021 16:10:06 +0900
parents 0ef9a73cae45
children 9d2cba39b33c
files automaton-in-agda/src/gcd.agda automaton-in-agda/src/prime.agda automaton-in-agda/src/root2.agda
diffstat 3 files changed, 64 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Tue Jun 29 09:35:12 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Tue Jun 29 16:10:06 2021 +0900
@@ -620,8 +620,9 @@
   field
     eqa : ℕ
     eqb : ℕ
-    is-equ< : (eqa * i) > (eqb * j) → ((eqa * i) - (eqb * j) ≡ gcd  )
-    is-equ> : (eqb * j) > (eqa * i) → ((eqb * j) - (eqa * i) ≡ gcd  )
+    is-equ< : eqa * i > eqb * j → (eqa * i) - (eqb * j) ≡ gcd  
+    is-equ> : eqb * j > eqa * i → (eqb * j) - (eqa * i) ≡ gcd  
+    is-equ= : eqa * i ≡ eqb * j → 0 ≡ gcd  
 
 ge3 : {a b c d : ℕ } → b > a → b - a ≡ d - c → d > c
 ge3 {a} {b} {c} {d} b>a eq = minus>0→x<y (subst (λ k → 0 < k ) eq (minus>0 b>a))
@@ -651,17 +652,25 @@
       eb * suc (suc j) + eb * (f * suc i0) ≡⟨ cong (λ k → eb * suc (suc j) + k ) ((sym (*-assoc eb _ _ )) ) ⟩ 
       eb * suc (suc j) + eb * f * suc i0 ∎ where open ≡-Reasoning
 
+ge20 : {i0 j0 : ℕ } →  i0 ≡ 0 → 0 ≡ gcd1 zero i0 zero j0 
+ge20 {i0} {zero} refl = refl
+ge20 {i0} {suc j0} refl = refl
 
 gcd-euclid1 : ( i i0 j j0 : ℕ )  → GCD i i0 j j0  → Euclid i0 j0 (gcd1 i i0 j j0)
 gcd-euclid1 zero i0 zero j0 di with <-cmp i0 j0
-... | tri< a' ¬b ¬c = record { eqa = 1 ; eqb = 0 ; is-equ< = λ _ → +-comm _ 0 ; is-equ> = λ () }
-... | tri≈ ¬a refl ¬c = record { eqa = 1 ; eqb = 0 ; is-equ< = λ _ → +-comm _ 0 ; is-equ> = λ () } 
-... | tri> ¬a ¬b c = record { eqa = 0 ; eqb = 1 ;  is-equ< = λ () ; is-equ> = λ _ → +-comm _ 0 }
+... | tri< a' ¬b ¬c = record { eqa = 1 ; eqb = 0 ; is-equ< = λ _ → +-comm _ 0 ; is-equ> = λ () ; is-equ= = ge21 }  where
+   ge21 : 1 * i0 ≡ 0 * j0 → 0 ≡ i0
+   ge21 eq = trans (sym eq) (+-comm i0 0) 
+... | tri≈ ¬a refl ¬c = record { eqa = 1 ; eqb = 0 ; is-equ< = λ _ → +-comm _ 0 ; is-equ> = λ () ; is-equ= = λ eq →  trans (sym eq) (+-comm i0 0) } 
+... | tri> ¬a ¬b c = record { eqa = 0 ; eqb = 1 ;  is-equ< = λ () ; is-equ> = λ _ → +-comm _ 0 ; is-equ= = ge22 }  where
+   ge22 : 0 * i0 ≡ 1 * j0 → 0 ≡ j0
+   ge22 eq = trans eq (+-comm j0 0) 
 -- i<i0  : zero ≤ i0
 -- j<j0  : 1 ≤ j0
 -- div-i : Dividable i0 ((j0 + zero) - 1)  -- fi * i0 ≡ (j0 + zero) - 1
 -- div-j : Dividable j0 ((i0 + 1) - zero) --  fj * j0 ≡ (i0 + 1) - zero
-gcd-euclid1 zero i0 (suc zero) j0 di = record { eqa = 1 ; eqb = Dividable.factor (GCD.div-j di) ; is-equ< = λ lt → ⊥-elim ( ge7 lt) ; is-equ> = λ _ → ge6 } where
+gcd-euclid1 zero i0 (suc zero) j0 di = record { eqa = 1 ; eqb = Dividable.factor (GCD.div-j di) ; is-equ< = λ lt → ⊥-elim ( ge7 lt) ; is-equ> = λ _ → ge6
+      ; is-equ= = λ eq → ⊥-elim (nat-≡< (sym (minus<=0 (subst (λ k → k ≤ 1 * i0) eq refl-≤ ))) (subst (λ k → 0 < k) (sym ge6) a<sa )) } where
    ge6 :  (Dividable.factor (GCD.div-j di) * j0) - (1 * i0) ≡ gcd1 zero i0 1 j0
    ge6  =  begin
         (Dividable.factor (GCD.div-j di) * j0) - (1 * i0)   ≡⟨  cong (λ k → k  - (1 * i0)) (+-comm 0 _)  ⟩
@@ -671,9 +680,11 @@
        1   ∎ where open ≡-Reasoning
    ge7 : ¬ ( 1 * i0 > Dividable.factor (GCD.div-j di) * j0 )
    ge7 lt = ⊥-elim ( nat-≡< (sym ( minus<=0 (<to≤ lt))) (subst (λ k → 0 < k) (sym ge6) (s≤s z≤n)))
-gcd-euclid1 zero zero (suc (suc j)) j0 di = record { eqa = 0 ; eqb = 1 ; is-equ< = λ () ; is-equ> = λ _ → +-comm _ 0 } 
+gcd-euclid1 zero zero (suc (suc j)) j0 di = record { eqa = 0 ; eqb = 1 ; is-equ< = λ () ; is-equ> = λ _ → +-comm _ 0
+    ; is-equ= = λ eq → subst (λ k → 0 ≡ k) (+-comm _ 0) eq } 
 gcd-euclid1 zero (suc i0) (suc (suc j)) j0 di with gcd-euclid1 i0 (suc i0) (suc j) (suc (suc j)) ( gcd-next1 di )
-... | e = record { eqa = ea + eb * f ; eqb =  eb
+... | e = record { eqa = ea + eb * f ; eqb =  eb 
+      ;  is-equ= =  λ eq → Euclid.is-equ= e (ge23 eq) 
       ;  is-equ< =  λ lt → subst (λ k → ((ea + eb * f) * suc i0) - (eb * j0) ≡ k ) (Euclid.is-equ< e (ge3 lt (ge1 ))) (ge1 )
       ;  is-equ> =  λ lt → subst (λ k → (eb * j0) - ((ea + eb * f) * suc i0) ≡ k ) (Euclid.is-equ> e (ge3 lt (ge2 ))) (ge2 ) } where
    ea = Euclid.eqa e 
@@ -689,7 +700,16 @@
       (eb * j0) - ((ea + eb * f) * suc i0)  ≡⟨ cong₂ (λ j k → j - k ) (proj2 (ge01  i0 j j0 ea eb di)) (proj1 (ge01  i0 j j0 ea eb di))  ⟩
       ( eb * suc (suc j) + ((eb * f) * (suc i0)) ) - (ea * suc i0 + (eb * f ) * suc i0 )   ≡⟨  minus+xy-zy {eb * suc (suc j)}{(eb * f ) * suc i0} {ea * suc i0}  ⟩
       (eb * suc (suc j)) - (ea * suc i0)   ∎ where open ≡-Reasoning
-gcd-euclid1 (suc zero) i0 zero j0 di = record { eqb = 1 ; eqa = Dividable.factor (GCD.div-i di) ; is-equ> = λ lt → ⊥-elim ( ge7' lt) ; is-equ< = λ _ → ge6' } where
+   ge23 : (ea + eb * f) * suc i0 ≡ eb * j0 → ea * suc i0 ≡ eb * suc (suc j)
+   ge23 eq = begin
+       ea * suc i0     ≡⟨ sym (minus+y-y {_} {(eb * f ) * suc i0} ) ⟩
+       (ea * suc i0 +  ((eb * f ) * suc i0 )) -  ((eb * f ) * suc i0 )  ≡⟨ cong (λ k → k - ((eb * f ) * suc i0 )) (sym ( proj1 (ge01  i0 j j0 ea eb di)))  ⟩
+       ((ea + eb * f) * suc i0)  -  ((eb * f ) * suc i0 )  ≡⟨ cong (λ k → k - ((eb * f ) * suc i0 ))  eq ⟩
+        (eb * j0) -  ((eb * f ) * suc i0 )  ≡⟨  cong (λ k → k - ((eb * f ) * suc i0 )) ( proj2 (ge01  i0 j j0 ea eb di)) ⟩
+       (eb * suc (suc j) +  ((eb * f ) * suc i0 )) -  ((eb * f ) * suc i0 )  ≡⟨ minus+y-y {_} {(eb * f ) * suc i0 }  ⟩
+       eb * suc (suc j)   ∎ where open ≡-Reasoning
+gcd-euclid1 (suc zero) i0 zero j0 di = record { eqb = 1 ; eqa = Dividable.factor (GCD.div-i di) ; is-equ> = λ lt → ⊥-elim ( ge7' lt) ; is-equ< = λ _ → ge6'
+       ; is-equ= = λ eq → ⊥-elim (nat-≡< (sym (minus<=0 (subst (λ k → k ≤ 1 * j0) (sym eq) refl-≤ ))) (subst (λ k → 0 < k) (sym ge6') a<sa )) } where
    ge6' :  (Dividable.factor (GCD.div-i di) * i0) - (1 * j0) ≡ gcd1 (suc zero) i0 zero j0 
    ge6'  =  begin
         (Dividable.factor (GCD.div-i di) * i0) - (1 * j0)   ≡⟨  cong (λ k → k  - (1 * j0)) (+-comm 0 _)  ⟩
@@ -699,9 +719,11 @@
        1   ∎ where open ≡-Reasoning
    ge7' : ¬ ( 1 * j0 > Dividable.factor (GCD.div-i di) * i0 )
    ge7' lt = ⊥-elim ( nat-≡< (sym ( minus<=0 (<to≤ lt))) (subst (λ k → 0 < k) (sym ge6') (s≤s z≤n)))
-gcd-euclid1 (suc (suc i)) i0 zero zero di = record { eqb = 0 ; eqa = 1 ; is-equ> = λ () ; is-equ< = λ _ → +-comm _ 0 }
+gcd-euclid1 (suc (suc i)) i0 zero zero di = record { eqb = 0 ; eqa = 1 ; is-equ> = λ () ; is-equ< = λ _ → +-comm _ 0
+    ; is-equ= =  λ eq → subst (λ k → 0 ≡ k) (+-comm _ 0) (sym eq) }
 gcd-euclid1 (suc (suc i)) i0 zero (suc j0) di with gcd-euclid1 (suc i) (suc (suc i)) j0 (suc j0) (GCD-sym (gcd-next1 (GCD-sym di)))
-... | e =  record { eqa = ea ; eqb =  eb + ea * f 
+... | e =  record { eqa = ea ; eqb =  eb + ea * f
+      ; is-equ= = λ eq → Euclid.is-equ= e (ge24 eq)
       ;  is-equ< =  λ lt → subst (λ k → ((ea * i0) - ((eb + ea * f) * suc j0))  ≡ k ) (Euclid.is-equ< e (ge3 lt ge4)) ge4 
       ;  is-equ> =  λ lt → subst (λ k →  (((eb + ea * f) * suc j0) - (ea * i0)) ≡ k ) (Euclid.is-equ> e (ge3 lt ge5)) ge5 } where
    ea = Euclid.eqa e 
@@ -717,6 +739,14 @@
         (ea * i0) - ((eb + ea * f) * suc j0) ≡⟨ cong₂ (λ j k → j - k ) (proj2 (ge01 j0 i i0 eb ea (GCD-sym di) )) (proj1 (ge01 j0 i i0 eb ea (GCD-sym di) )) ⟩
         (ea * suc (suc i) + (ea * f )* suc j0) - ( eb * suc j0 + (ea * f )* suc j0)  ≡⟨ minus+xy-zy {ea * suc (suc i)} {(ea * f )* suc j0} { eb * suc j0}   ⟩
         (ea * suc (suc i)) - (eb * suc j0) ∎ where open ≡-Reasoning
+   ge24 : ea * i0 ≡ (eb + ea * f) * suc j0 → ea * suc (suc i) ≡ eb * suc j0
+   ge24 eq = begin
+       ea * suc (suc i)   ≡⟨ sym ( minus+y-y {_} {(ea * f ) * suc j0 })  ⟩
+       (ea * suc (suc i) + (ea * f ) * suc j0 ) - ((ea * f ) * suc j0) ≡⟨  cong (λ k → k - ((ea * f ) * suc j0 )) (sym (proj2 (ge01 j0 i i0 eb ea (GCD-sym di) )))  ⟩
+        (ea * i0) - ((ea * f ) * suc j0)  ≡⟨  cong (λ k → k - ((ea * f ) * suc j0 )) eq  ⟩
+       ((eb + ea * f) * suc j0) - ((ea * f ) * suc j0) ≡⟨   cong (λ k → k - ((ea * f ) * suc j0 )) ((proj1 (ge01 j0 i i0 eb ea (GCD-sym di)))) ⟩
+       ( eb * suc j0 + (ea * f ) * suc j0 ) - ((ea * f ) * suc j0) ≡⟨  minus+y-y {_} {(ea * f ) * suc j0 }  ⟩
+       eb * suc j0   ∎ where open ≡-Reasoning
 gcd-euclid1 (suc zero) i0 (suc j) j0 di =
      gcd-euclid1 zero i0 j j0  (gcd-next di)
 gcd-euclid1 (suc (suc i)) i0 (suc j) j0  di = 
@@ -761,7 +791,7 @@
          (b * a) * Euclid.eqb ge11   ≡⟨ *-assoc b a (Euclid.eqb ge11 ) ⟩
          b * (a * Euclid.eqb ge11 ) ∎ where open ≡-Reasoning
     ge19 : ( Euclid.eqa ge11 * p ) ≡ (  Euclid.eqb ge11 * a ) → ((b * Euclid.eqa ge11) - (Dividable.factor div-ab * Euclid.eqb ge11)) * p + 0 ≡ b
-    ge19 = {!!}
+    ge19 eq = ⊥-elim ( nat-≡< (Euclid.is-equ= ge11 eq) (subst (λ k → 0 < k ) (sym ge10) a<sa ) )
     ge14 : ( Euclid.eqa ge11 * p ) > (  Euclid.eqb ge11 * a ) → ((b * Euclid.eqa ge11) - (Dividable.factor div-ab * Euclid.eqb ge11)) * p + 0 ≡ b
     ge14 lt = begin
          (((b * Euclid.eqa ge11) - (Dividable.factor div-ab * Euclid.eqb ge11)) * p) + 0 ≡⟨ +-comm _ 0 ⟩
--- a/automaton-in-agda/src/prime.agda	Tue Jun 29 09:35:12 2021 +0900
+++ b/automaton-in-agda/src/prime.agda	Tue Jun 29 16:10:06 2021 +0900
@@ -93,7 +93,7 @@
          ... | tri≈ ¬a b ¬c = skip-case (np1 (gcd n m) m ngcd c
               (subst (λ k → Factoring m k) (sym b) (findFactor m ≤-refl (λ j n≤j j<n → ⊥-elim (nat-≤>  n≤j j<n) ))))
          ... | tri> ¬a ¬b' c with <-cmp 0 m
-         ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> (gcd-≥ m n a (≤-trans refl-≤s m≤n)) c )
+         ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> (subst (λ k → k ≤ m) (gcdsym {m} {n}) (gcd-≤ a (<-trans a m≤n))) c ) 
          ... | tri≈ ¬a' b' ¬c = ⊥-elim ( np record { isPrime = λ j lt 0<j → mg j (subst (λ k → k < j) b' 0<j) lt ; p>1 = 1<n } ) -- suc m ≤ j
     np1 n zero np 1<n (skipFactor n ())
     np1 n (suc m) np 1<n  (skipFactor n n<m) with <-cmp m n
--- a/automaton-in-agda/src/root2.agda	Tue Jun 29 09:35:12 2021 +0900
+++ b/automaton-in-agda/src/root2.agda	Tue Jun 29 16:10:06 2021 +0900
@@ -29,12 +29,14 @@
 divdable^2 zero zero () 1<n pk dn2
 divdable^2 (suc n) (suc k) 1<k 1<n pk dn2 with decD {suc k} {suc n} 1<k
 ... | yes y = y
-... | no non with gcd-equlid (suc k) (suc n) (suc n) 1<k (Prime.isPrime pk) dn2
+... | no non with gcd-euclid (suc k) (suc n) (suc n) 1<k (<-trans a<sa 1<n) (<-trans a<sa 1<n) (Prime.isPrime pk) dn2 
 ... | case1 dn = dn
 ... | case2 dm = dm
 
 p2 : Prime 2
-  p2 = record { p>1 = a<sa ; isPrime = {!!} }
+p2 = record { p>1 = a<sa ; isPrime = p22 } where
+   p22 : (j : ℕ) → j < 2 → 0 < j → gcd 2 j ≡ 1
+   p22 1 (s≤s (s≤s z≤n)) (s≤s 0<j) = refl
 
 -- gcd-div : ( i j k : ℕ ) → (if : Dividable k i) (jf : Dividable k j )
 --    → Dividable k ( gcd i  j )
@@ -46,8 +48,23 @@
     ... | zero | ()
     ... | suc n | ()
     dm : Dividable 2 m
-    dm = divdable^2 m 2 a<sa m>1 p2 record { factor = n * n ; is-factor = {!!} }
+    dm = divdable^2 m 2 a<sa m>1 p2 record { factor = n * n ; is-factor = begin
+       (n * n) * 2 + 0 ≡⟨  +-comm _ 0 ⟩
+       (n * n) * 2  ≡⟨ *-comm (n * n) 2 ⟩
+       2 * (n * n)  ≡⟨ sym (*-assoc 2 n n)  ⟩
+       (2 * n) * n ≡⟨ 2nm  ⟩
+       m * m ∎ }  where open ≡-Reasoning
+    df = Dividable.factor dm
     dn : Dividable 2 n
-    dn = divdable^2 n 2 a<sa n>1 p2 record { factor = Dividable.factor dm * m ; is-factor = {!!} }
+    dn = divdable^2 n 2 a<sa n>1 p2 record { factor = Dividable.factor dm * m ; is-factor = begin
+        df * m * 2 + 0  ≡⟨ *-cancelʳ-≡ _ _ {1} ( begin 
+          {!!}  ≡⟨  {!!} ⟩
+          ((df * m) * 2 )  ≡⟨  {!!} ⟩
+          ((m * df) * 2 )  ≡⟨  {!!} ⟩
+          (m * (df * 2) )  ≡⟨  {!!} ⟩
+          (m * (df * 2 + 0) )  ≡⟨  {!!} ⟩
+          m * m   ≡⟨  {!!} ⟩
+          n * n * 2 ∎  ) ⟩
+       n * n ∎ }  where open ≡-Reasoning