Mercurial > hg > Members > kono > Proof > automaton

changeset 235:938d48130144

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 18:49:54 +0900
parents 65dea8980aee
children 9f7e4a4415f7
files automaton-in-agda/src/gcd.agda automaton-in-agda/src/nat.agda
diffstat 2 files changed, 54 insertions(+), 42 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Sun Jun 27 12:24:28 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Sun Jun 27 18:49:54 2021 +0900
@@ -299,6 +299,37 @@
    → 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)
 
+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 =
+      ⟪ ( subst (λ k → Dividable i0 (k - suc j)) ( begin
+               j0 + suc i ≡⟨ sym (+-assoc j0 1 i ) ⟩ 
+               (j0 + 1) + i ≡⟨ cong (λ k → k + i) (+-comm j0 _ ) ⟩ 
+               suc (j0 + i) ∎ ) (proj1 x) ) ,
+       ( subst (λ k → Dividable j0 (k - suc i)) ( begin
+               i0 + suc j ≡⟨ sym (+-assoc i0 1 j ) ⟩ 
+               (i0 + 1) + j ≡⟨ cong (λ k → k + j) (+-comm i0 _ ) ⟩ 
+               suc (i0 + j) ∎ ) (proj2 x) ) ⟫    
+           where open ≡-Reasoning
+
+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-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
@@ -470,43 +501,15 @@
   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  )
 
 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) 
-di-next {i} {i0} {j} {j0} x =
-      ⟪ ( subst (λ k → Dividable i0 (k - suc j)) ( begin
-               j0 + suc i ≡⟨ sym (+-assoc j0 1 i ) ⟩ 
-               (j0 + 1) + i ≡⟨ cong (λ k → k + i) (+-comm j0 _ ) ⟩ 
-               suc (j0 + i) ∎ ) (proj1 x) ) ,
-       ( subst (λ k → Dividable j0 (k - suc i)) ( begin
-               i0 + suc j ≡⟨ sym (+-assoc i0 1 j ) ⟩ 
-               (i0 + 1) + j ≡⟨ cong (λ k → k + j) (+-comm i0 _ ) ⟩ 
-               suc (i0 + j) ∎ ) (proj2 x) ) ⟫    
-           where open ≡-Reasoning
-
-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
+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 zero i0 zero j0 di with <-cmp i0 j0
@@ -516,22 +519,25 @@
 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)
+... | 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)
-   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)  ≡⟨ {!!} ⟩ 
+   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)  ≡⟨ {!!}   ⟩ 
+      ((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)))  ⟩ 
+      ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + (f * suc i0 + 0) )) ≡⟨ {!!} ⟩ 
       ((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 + 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 = {!!}
+    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 (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 = {!!}
--- a/automaton-in-agda/src/nat.agda	Sun Jun 27 12:24:28 2021 +0900
+++ b/automaton-in-agda/src/nat.agda	Sun Jun 27 18:49:54 2021 +0900
@@ -227,6 +227,12 @@
 minus>0 {zero} {suc _} (s≤s z≤n) = s≤s z≤n
 minus>0 {suc x} {suc y} (s≤s lt) = minus>0 {x} {y} lt
 
+minus>0→x<y : {x y : ℕ } → 0 < minus y x  → x < y
+minus>0→x<y {x} {y} lt with <-cmp x y
+... | tri< a ¬b ¬c = a
+... | tri≈ ¬a refl ¬c = ⊥-elim ( nat-≡< (sym (minus<=0 {x} ≤-refl)) lt )
+... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym (minus<=0 {y} (≤-trans refl-≤s c ))) lt )
+
 minus+y-y : {x y : ℕ } → (x + y) - y  ≡ x
 minus+y-y {zero} {y} = minus<=0 {zero + y} {y} ≤-refl 
 minus+y-y {suc x} {y} = begin