Mercurial > hg > Members > kono > Proof > automaton

changeset 238:3aad251b8d8b

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 Mon, 28 Jun 2021 09:30:41 +0900
parents 709e63cb9d19
children d475257ffe30
files automaton-in-agda/src/gcd.agda
diffstat 1 files changed, 35 insertions(+), 24 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Sun Jun 27 23:13:07 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Mon Jun 28 09:30:41 2021 +0900
@@ -299,17 +299,6 @@
    → Dividable k ( gcd i  j ) 
 gcd-div i j k k>1 if jf = gcd-gt i i j j k k>1 (DtoF if) if (DtoF jf) jf (div-div k>1 if jf)
 
--- gcd loop invariant
---
-record GCD ( i i0 j j0 : ℕ ) : Set where
-     i<i0  : i ≤ i0
-     j<j0  : j ≤ j0
-     div-i : Dividable i0 (j0 + i - j )
-     div-j : Dividable j0 (i0 + j - i)
-
-gcd-next : {i i0 j j0 : ℕ} → GCD (suc i) i0 (suc j) j0 → GCD i i0 j j0
-gcd-next = ?
-
 di-next : {i i0 j j0 : ℕ} → Dividable i0  ((j0 + suc i) - suc j ) ∧ Dividable j0 ((i0 + suc j) - suc i) →
            Dividable i0  ((j0 + i) - j ) ∧ Dividable j0 ((i0 + j) - i) 
 di-next {i} {i0} {j} {j0} x =
@@ -323,9 +312,6 @@
                suc (i0 + j) ∎ ) (proj2 x) ) ⟫    
            where open ≡-Reasoning
 
-gcd-next1 : {i0 j j0 : ℕ} → GCD 0 (suc i0) (suc (suc j)) j0 → GCD (suc (suc j)) (suc i0) (suc i0 + suc j) (suc (suc j))
-gcd-next1 = ?
-
 di-next1 : {i0 j j0 : ℕ} →  Dividable (suc i0) ((j0 + 0) - (suc (suc j))) ∧ Dividable j0 (suc (i0 + suc (suc j)))
        →    Dividable (suc i0) ((suc (suc j) + i0) - suc j) ∧ Dividable (suc (suc j)) ((suc i0 + suc j) - i0)
 di-next1 {i0} {j} {j0} x = 
@@ -344,6 +330,31 @@
                ((suc i0 + suc j)   - i0) ∎ ) div= ⟫    
            where open ≡-Reasoning
 
+-- gcd loop invariant
+--
+record GCD ( i i0 j j0 : ℕ ) : Set where
+   field
+     i<i0  : i ≤ i0
+     j<j0  : j ≤ j0
+     div-i : Dividable i0 ((j0 + i) - j)
+     div-j : Dividable j0 ((i0 + j) - i)
+
+GCD-sym : {i i0 j j0 : ℕ} → GCD i i0 j j0 → GCD j j0 i i0
+GCD-sym g = record { i<i0 = GCD.j<j0 g ; j<j0 = GCD.i<i0 g ; div-i = GCD.div-j g ; div-j = GCD.div-i g }
+
+pred-≤ : {i i0 : ℕ } → suc i ≤ suc i0 → i ≤ suc i0
+pred-≤ {i} {i0} (s≤s lt) = ≤-trans lt refl-≤s
+
+gcd-next : {i i0 j j0 : ℕ} → GCD (suc i) i0 (suc j) j0 → GCD i i0 j j0
+gcd-next {i} {0} {j} {0} ()
+gcd-next {i} {suc i0} {j} {suc j0} g = record { i<i0 = pred-≤ (GCD.i<i0 g) ; j<j0 = pred-≤ (GCD.j<j0 g)
+  ; div-i = proj1 (di-next {i} {suc i0} {j} {suc j0} ⟪ GCD.div-i g , GCD.div-j g ⟫ )
+  ; div-j = proj2 (di-next {i} {suc i0} {j} {suc j0} ⟪ GCD.div-i g , GCD.div-j g ⟫ ) }
+
+gcd-next1 : {i0 j j0 : ℕ} → GCD 0 (suc i0) (suc (suc j)) j0 → GCD i0 (suc i0) (suc j) (suc (suc j)) 
+gcd-next1 {i0} {j} {j0} g = record { i<i0 = refl-≤s ; j<j0 = refl-≤s
+  ; div-i = proj1 (di-next1 ⟪ GCD.div-i g , GCD.div-j g ⟫ ) ; div-j = proj2 (di-next1 ⟪ GCD.div-i g , GCD.div-j g ⟫ ) }
+
 -- gcd-dividable1 : ( i i0 j j0 : ℕ )
 --      → Dividable i0  (j0 + i - j ) ∨ Dividable j0 (i0 + j - i)
 --      → Dividable ( gcd1 i i0 j j0  ) i0 ∧ Dividable ( gcd1 i i0 j j0  ) j0
@@ -525,29 +536,29 @@
 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))
 
-gcd-equlid1 : ( i i0 j j0 : ℕ )  → Dividable i0  ((j0 + i) - j ) ∧ Dividable j0 ((i0 + j) - i) → Equlid i0 j0 (gcd1 i i0 j j0)
+gcd-equlid1 : ( i i0 j j0 : ℕ )  → GCD i i0 j j0  → Equlid i0 j0 (gcd1 i i0 j j0)
 gcd-equlid1 zero i0 zero j0 di with <-cmp i0 j0
 ... | tri< a' ¬b ¬c = record { eqa = 1 ; eqb = 0 ; is-equ< = {!!} ; is-equ> = {!!}  }
 ... | tri≈ ¬a refl ¬c = record { eqa = 1 ; eqb = 0 ; is-equ< = {!!} ; is-equ> = {!!} } 
 ... | tri> ¬a ¬b c = record { eqa = 0 ; eqb = 1 ;  is-equ< = {!!} ; is-equ> = {!!} }
 gcd-equlid1 zero i0 (suc zero) j0 di = record { eqa = 1 ; eqb = 1 ; is-equ< = {!!} ; is-equ> = {!!} } 
 gcd-equlid1 zero zero (suc (suc j)) j0 di = record { eqa = 0 ; eqb = 1 ; is-equ< = {!!} ; is-equ> = {!!} } 
-gcd-equlid1 zero (suc i0) (suc (suc j)) j0 di with gcd-equlid1 i0 (suc i0) (suc j) (suc (suc j)) ( di-next1 di )
+gcd-equlid1 zero (suc i0) (suc (suc j)) j0 di with gcd-equlid1 i0 (suc i0) (suc j) (suc (suc j)) ( gcd-next1 di )
 ... | e = record { eqa = ea + eb * f ; eqb =  eb ;  is-equ< = ge0 ; is-equ> = {!!} } where
    ea = Equlid.eqa e 
    eb = Equlid.eqb e
-   f = Dividable.factor (proj1 di)
+   f = Dividable.factor (GCD.div-i di)
    ge4 :  suc (j0 + 0) > suc (suc j)
-   ge4 = {!!}
+   ge4 = subst (λ k → k > suc (suc j)) (+-comm 0 _ ) ( s≤s (GCD.j<j0  di))
    ge0 : (ea + eb * f) * suc i0 > eb * j0 → (((ea + eb * f) * suc i0) - (eb * j0)) ≡ gcd1 i0 (suc i0) (suc j) (suc (suc j))
    ge0 lt = subst (λ k → ((ea + eb * f) * suc i0) - (eb * j0) ≡ k ) (Equlid.is-equ< e ge2 ) ge1 where
     ge1 : ((ea + eb * f) * suc i0) - (eb * j0)  ≡ (ea * suc i0) - (eb * suc (suc j))       
     ge1  = begin
       ((ea + eb * f ) * suc i0) - (eb * j0)  ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - (eb * k)) (+-comm 0 _) ⟩ 
-      ((ea + eb * f ) * suc i0) - (eb * (j0 + 0) )  ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - (eb * k)) (sym (minus+n {j0 + 0} {suc (suc j)} {!!} )) ⟩ 
+      ((ea + eb * f ) * suc i0) - (eb * (j0 + 0) )  ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - (eb * k)) (sym (minus+n {j0 + 0} {suc (suc j)} ge4 )) ⟩ 
       ((ea + eb * f ) * suc i0) - (eb * (((j0 + 0) -  suc (suc j)) + suc (suc j)  )) ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - (eb * k)) (+-comm _ (suc (suc j)) ) ⟩
       ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + ((j0 + 0) -  suc (suc j))))
-              ≡⟨ cong (λ k → ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + k) )) (sym (Dividable.is-factor (proj1 di)))  ⟩ 
+              ≡⟨ cong (λ k → ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + k) )) (sym (Dividable.is-factor (GCD.div-i di)))  ⟩ 
       ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + (f * suc i0 + 0) )) ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + k))) (+-comm _ 0) ⟩ 
       ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + (f * suc i0 ) )) ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - k) (*-distribˡ-+  eb (suc (suc j)) (f * suc i0)) ⟩ 
       ((ea + eb * f ) * suc i0) - (eb * suc (suc j) + eb * (f * suc i0)) ≡⟨ cong (λ k → k - (eb * suc (suc j) + eb * (f * suc i0))) (*-distribʳ-+ (suc i0)  ea  _) ⟩ 
@@ -557,14 +568,14 @@
       (ea * suc i0) - (eb * suc (suc j)) ∎ where open ≡-Reasoning
     ge2 : ea * suc i0 > eb * suc (suc j)
     ge2 = ge3 lt ge1 
-gcd-equlid1 (suc zero) i0 zero j0 di = subst (λ k → {!!}) {!!} ( gcd-equlid1 zero j0 (suc zero) i0 (∧-exch di))
+gcd-equlid1 (suc zero) i0 zero j0 di = {!!} 
 gcd-equlid1 (suc (suc i)) i0 zero zero di = {!!}
-gcd-equlid1 (suc (suc i)) i0 zero (suc j0) di with gcd-equlid1 (suc i) (suc (suc i)) j0 (suc j0) (∧-exch (di-next1 (∧-exch di)))
+gcd-equlid1 (suc (suc i)) i0 zero (suc j0) di with gcd-equlid1 (suc i) (suc (suc i)) j0 (suc j0) (GCD-sym (gcd-next1 (GCD-sym di)))
 ... | e = {!!}
 gcd-equlid1 (suc zero) i0 (suc j) j0 di =
-     gcd-equlid1 zero i0 j j0  (di-next di)
+     gcd-equlid1 zero i0 j j0  (gcd-next di)
 gcd-equlid1 (suc (suc i)) i0 (suc j) j0  di = 
-     gcd-equlid1 (suc i) i0 j j0 (di-next di)
+     gcd-equlid1 (suc i) i0 j j0 (gcd-next di)
 
 
 div→gcd : {n k : ℕ } → k > 1 → Dividable k n → gcd n k ≡ k