Mercurial > hg > Members > kono > Proof > automaton

changeset 234:65dea8980aee

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 Sun, 27 Jun 2021 12:24:28 +0900
parents 327094b57ee2
children 938d48130144
files automaton-in-agda/src/gcd.agda
diffstat 1 files changed, 55 insertions(+), 34 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Fri Jun 25 20:16:53 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Sun Jun 27 12:24:28 2021 +0900
@@ -470,7 +470,12 @@
   field
     eqa : ℕ
     eqb : ℕ
-    gcd-equ : ((eqa * i) - (eqb * j) ≡ gcd  ) ∨ ((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  )
+
+postulate 
+   gcd-equlid : ( p q r : ℕ )  → 1 < p  → ((i : ℕ ) → i < p → 0 < i   → gcd p i ≡ 1)  →  Dividable p (q * r)  → Dividable p q ∨ Dividable p r
+--   gcd-equlid1 : ( i i0 j j0 : ℕ )  → Dividable i0  ((j0 + i) - j ) ∧ Dividable j0 ((i0 + j) - i) → Equlid i0 j0 (gcd1 i i0 j j0)
 
 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) 
@@ -485,39 +490,55 @@
                suc (i0 + j) ∎ ) (proj2 x) ) ⟫    
            where open ≡-Reasoning
 
-postulate 
-   gcd-equlid : ( p q r : ℕ )  → 1 < p  → ((i : ℕ ) → i < p → 0 < i   → gcd p i ≡ 1)  →  Dividable p (q * r)  → Dividable p q ∨ Dividable p r
-   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 zero i0 zero j0 di with <-cmp i0 j0
--- ... | tri< a' ¬b ¬c = record { eqa = 1 ; eqb = 0 ; gcd-equ = case1 {!!} }
--- ... | tri≈ ¬a refl ¬c = record { eqa = 1 ; eqb = 0 ; gcd-equ = case1 {!!} }
--- ... | tri> ¬a ¬b c = record { eqa = 0 ; eqb = 1 ; gcd-equ = case2 {!!} }
--- gcd-equlid1 zero i0 (suc zero) j0 di = record { eqa = 1 ; eqb = 1 ; gcd-equ = case1 {!!} }
--- gcd-equlid1 zero zero (suc (suc j)) j0 di = record { eqa = 0 ; eqb = 1 ; gcd-equ = case2 {!!} }
--- gcd-equlid1 zero (suc i0) (suc (suc j)) j0 di with gcd-equlid1 i0 (suc i0) (suc j) (suc (suc j))  {!!} 
--- ... | e with Equlid.gcd-equ e
--- ... | case1 x = record { eqa = ea + eb * f ; eqb =  eb ; gcd-equ = case1 (trans  ge1 x ) } where
---    --   Dividable (suc i0) ((j0 + 0) - (suc (suc j))) ∨ Dividable j0 (suc (i0 + suc (suc j)))
---    --        (j0 + 0) - (suc (suc j)) ≡ f * (suc i0)
---    ea = Equlid.eqa e 
---    eb = Equlid.eqb e
---    f = Dividable.factor (proj1 di)
---    ge1 : ((ea + eb * f) * suc i0) - (eb * j0)  ≡ (ea * suc i0) - (eb * suc (suc j))       
---    ge1  = begin
---       ((ea + eb * f ) * suc i0) - (eb * j0)  ≡⟨ {!!} ⟩ 
---       ((ea + eb * f ) * suc i0) - eb * (f * (suc i0) + suc (suc j) )  ≡⟨ {!!} ⟩ 
---       ((ea + eb * f ) * suc i0 - (eb * f) * (suc i0)) + eb * suc (suc j)   ≡⟨ {!!} ⟩ 
---       ((ea * suc i0 + (eb * f ) * suc i0 ) - (eb * f) * (suc i0)) + eb * suc (suc j)   ≡⟨ {!!} ⟩ 
---       (ea * suc i0) - (eb * suc (suc j)) ∎ where open ≡-Reasoning
--- ... | case2 x = {!!}
--- 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) {!!} 
--- ... | e = {!!}
--- gcd-equlid1 (suc zero) i0 (suc j) j0 di =
---      gcd-equlid1 zero i0 j j0  (di-next di)
--- gcd-equlid1 (suc (suc i)) i0 (suc j) j0  di = 
---      gcd-equlid1 (suc i) i0 j j0 (di-next di)
+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 = 
+      ⟪ record { factor = 1 ; is-factor = begin
+           1 * suc i0 + 0 ≡⟨ cong suc ( trans (+-comm _ 0)  (+-comm _ 0) ) ⟩
+           suc i0  ≡⟨ sym (minus+y-y {suc i0} {j})  ⟩
+           (suc i0 + j) - j ≡⟨ cong (λ k → k - j ) (+-comm (suc i0) _ ) ⟩
+           (suc j + suc i0 ) - suc j ≡⟨ cong (λ k → k - suc j) (sym (+-assoc (suc j) 1 i0 ))  ⟩
+           ((suc j + 1) + i0) - suc j ≡⟨ cong (λ k → (k + i0) - suc j) (+-comm _ 1) ⟩
+           (suc (suc j) + i0) - suc j ∎ }  , 
+        subst (λ k → Dividable (suc (suc j)) k) ( begin
+               suc (suc j) ≡⟨ sym ( minus+y-y {suc (suc j)}{i0} ) ⟩ 
+               (suc (suc j) + i0 ) - i0  ≡⟨ cong (λ k → (k + i0) - i0) (cong suc (+-comm 1 _ )) ⟩ 
+               ((suc j + 1) + i0 ) - i0  ≡⟨ cong (λ k → k - i0) (+-assoc (suc j) 1  _ ) ⟩ 
+               (suc j + suc i0 ) - i0  ≡⟨ cong (λ k → k - i0) (+-comm (suc j) _) ⟩ 
+               ((suc i0 + suc j)   - i0) ∎ ) div= ⟫    
+           where open ≡-Reasoning
+
+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 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 )
+... | e = record { eqa = ea + eb * f ; eqb =  eb ;  is-equ< = {!!} ; is-equ> = {!!} } where
+   --   Dividable (suc i0) ((j0 + 0) - (suc (suc j))) ∨ Dividable j0 (suc (i0 + suc (suc j)))
+   --        (j0 + 0) - (suc (suc j)) ≡ f * (suc i0)
+   ea = Equlid.eqa e 
+   eb = Equlid.eqb e
+   f = Dividable.factor (proj1 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 = ?
+   ge1 : ((ea + eb * f) * suc i0) - (eb * j0)  ≡ (ea * suc i0) - (eb * suc (suc j))       
+   ge1  = begin
+      ((ea + eb * f ) * suc i0) - (eb * j0)  ≡⟨ {!!} ⟩ 
+      ((ea + eb * f ) * suc i0) - eb * (f * (suc i0) + suc (suc j) )  ≡⟨ {!!} ⟩ 
+      ((ea + eb * f ) * suc i0 - (eb * f) * (suc i0)) + eb * suc (suc j)   ≡⟨ {!!} ⟩ 
+      ((ea * suc i0 + (eb * f ) * suc i0 ) - (eb * f) * (suc i0)) + eb * suc (suc j)   ≡⟨ {!!} ⟩ 
+      (ea * suc i0) - (eb * suc (suc j)) ∎ where open ≡-Reasoning
+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)))
+... | e = {!!}
+gcd-equlid1 (suc zero) i0 (suc j) j0 di =
+     gcd-equlid1 zero i0 j j0  (di-next di)
+gcd-equlid1 (suc (suc i)) i0 (suc j) j0  di = 
+     gcd-equlid1 (suc i) i0 j j0 (di-next di)
 
 
 div→gcd : {n k : ℕ } → k > 1 → Dividable k n → gcd n k ≡ k