Mercurial > hg > Members > kono > Proof > automaton

changeset 249:0ef9a73cae45

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 09:35:12 +0900
parents de959bb968ed
children 89120ac828b7
files automaton-in-agda/src/gcd.agda automaton-in-agda/src/nat.agda
diffstat 2 files changed, 27 insertions(+), 21 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Mon Jun 28 23:21:25 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Tue Jun 29 09:35:12 2021 +0900
@@ -760,30 +760,29 @@
          (a * b) * Euclid.eqb ge11   ≡⟨ cong (λ k → k *  Euclid.eqb ge11) (*-comm a b) ⟩
          (b * a) * Euclid.eqb ge11   ≡⟨ *-assoc b a (Euclid.eqb ge11 ) ⟩
          b * (a * Euclid.eqb ge11 ) ∎ where open ≡-Reasoning
-    ge14 : ( Euclid.eqa ge11 * p ) ≤ (  Euclid.eqb ge11 * a ) → (b * Euclid.eqa ge11 - Dividable.factor div-ab * Euclid.eqb ge11) * p + 0 ≡ b
+    ge19 : ( Euclid.eqa ge11 * p ) ≡ (  Euclid.eqb ge11 * a ) → ((b * Euclid.eqa ge11) - (Dividable.factor div-ab * Euclid.eqb ge11)) * p + 0 ≡ b
+    ge19 = {!!}
+    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 ⟩
-         (b * Euclid.eqa ge11 - Dividable.factor div-ab * Euclid.eqb ge11) * p ≡⟨ {!!}  ⟩
-         ((b * Euclid.eqa ge11) - (Dividable.factor div-ab * Euclid.eqb ge11)) * p
-                  ≡⟨ distr-minus-* {b * Euclid.eqa ge11 } {Dividable.factor div-ab * Euclid.eqb ge11} {p} ⟩
-         {!!} ≡⟨ {!!}  ⟩
-         (b * Euclid.eqa ge11) * p - ((Dividable.factor div-ab * Euclid.eqb ge11) * p)  ≡⟨ cong (λ k → (b * Euclid.eqa ge11) * p  - k  ) ge18 ⟩
-         (b * Euclid.eqa ge11) * p - (b * (a * Euclid.eqb ge11 ))  ≡⟨ {!!}   ⟩
-         b * (Euclid.eqa ge11 * p) - (b * (a * Euclid.eqb ge11 ))  ≡⟨ {!!}   ⟩
-         b * ( Euclid.eqa ge11 * p - a * Euclid.eqb ge11 )  ≡⟨ {!!}   ⟩
-         b * ( Euclid.eqa ge11 * p -  Euclid.eqb ge11 * a )  ≡⟨ cong (b *_) {!!} ⟩
+         (((b * Euclid.eqa ge11) - (Dividable.factor div-ab * Euclid.eqb ge11)) * p) + 0 ≡⟨ +-comm _ 0 ⟩
+         ((b * Euclid.eqa ge11) - ((Dividable.factor div-ab * Euclid.eqb ge11)) * p) ≡⟨ distr-minus-* {_} {Dividable.factor div-ab * Euclid.eqb ge11} {p} ⟩
+         ((b * Euclid.eqa ge11) * p) - (((Dividable.factor div-ab * Euclid.eqb ge11) * p))  ≡⟨ cong (λ k → ((b * Euclid.eqa ge11) * p)  - k  ) ge18 ⟩
+         ((b * Euclid.eqa ge11) * p) - (b * (a * Euclid.eqb ge11 ))  ≡⟨ cong (λ k → k - (b * (a * Euclid.eqb ge11)) ) (*-assoc b _ p) ⟩
+         (b * (Euclid.eqa ge11 * p)) - (b * (a * Euclid.eqb ge11 ))  ≡⟨ sym ( distr-minus-*' {b} {Euclid.eqa ge11 * p} {a * Euclid.eqb ge11} )  ⟩
+         b * (( Euclid.eqa ge11 * p) - (a * Euclid.eqb ge11) )  ≡⟨ cong (λ k → b * ( ( Euclid.eqa ge11 * p) - k)) (*-comm a (Euclid.eqb ge11)) ⟩
+         (b * ( (Euclid.eqa ge11 * p)) -  (Euclid.eqb ge11 * a) )  ≡⟨ cong (b *_) (Euclid.is-equ< ge11 lt )⟩
          b * gcd p a  ≡⟨ cong (b *_) ge10 ⟩
          b * 1  ≡⟨ m*1=m ⟩
          b ∎ where open ≡-Reasoning
-    ge15 : ( Euclid.eqa ge11 * p ) > (  Euclid.eqb ge11 * a ) →  (Dividable.factor div-ab * Euclid.eqb ge11 - b * Euclid.eqa ge11  ) * p + 0 ≡ b
+    ge15 : ( Euclid.eqa ge11 * p ) < (  Euclid.eqb ge11 * a ) →  ((Dividable.factor div-ab * Euclid.eqb ge11) - (b * Euclid.eqa ge11 ) ) * p + 0 ≡ b
     ge15 lt = begin
-         (Dividable.factor div-ab * Euclid.eqb ge11 - b * Euclid.eqa ge11  ) * p + 0  ≡⟨  +-comm _ 0 ⟩
-         (Dividable.factor div-ab * Euclid.eqb ge11 - b * Euclid.eqa ge11  ) * p   ≡⟨ {!!}   ⟩
+         ((Dividable.factor div-ab * Euclid.eqb ge11) - (b * Euclid.eqa ge11)  ) * p + 0  ≡⟨  +-comm _ 0 ⟩
+         ((Dividable.factor div-ab * Euclid.eqb ge11) - (b * Euclid.eqa ge11)  ) * p   ≡⟨ distr-minus-* {_} {b * Euclid.eqa ge11} {p} ⟩
          ((Dividable.factor div-ab * Euclid.eqb ge11) * p) - ((b * Euclid.eqa ge11) * p)    ≡⟨ cong (λ k → k - ((b * Euclid.eqa ge11) * p)   ) ge18 ⟩
-         (b * (a * Euclid.eqb ge11 )) - ((b * Euclid.eqa ge11) * p )   ≡⟨ {!!}   ⟩
-         (b * (a * Euclid.eqb ge11 )) - (b * (Euclid.eqa ge11 * p) )   ≡⟨ {!!}   ⟩
-         b * ( a * Euclid.eqb ge11 - (Euclid.eqa ge11 * p) )  ≡⟨ {!!}   ⟩
-         b * ( Euclid.eqb ge11 * a - Euclid.eqa ge11 * p  )  ≡⟨ cong (b *_) {!!} ⟩
+         (b * (a * Euclid.eqb ge11 )) - ((b * Euclid.eqa ge11) * p )   ≡⟨   cong (λ k → (b * (a * Euclid.eqb ge11)) - k ) (*-assoc b _ p) ⟩
+         (b * (a * Euclid.eqb ge11 )) - (b * (Euclid.eqa ge11 * p) )   ≡⟨  sym ( distr-minus-*' {b} {a * Euclid.eqb ge11} {Euclid.eqa ge11 * p}  ) ⟩
+         b * ( (a * Euclid.eqb ge11) - (Euclid.eqa ge11 * p) )  ≡⟨  cong (λ k → b * ( k - ( Euclid.eqa ge11 * p) )) (*-comm a (Euclid.eqb ge11))  ⟩
+         b * ( (Euclid.eqb ge11 * a) - (Euclid.eqa ge11 * p)  )  ≡⟨ cong (b *_) (Euclid.is-equ> ge11 lt) ⟩
          b * gcd p a  ≡⟨ cong (b *_) ge10 ⟩
          b * 1  ≡⟨ m*1=m ⟩
          b ∎ where open ≡-Reasoning
@@ -791,9 +790,9 @@
     ge17 x x refl = refl-≤
     ge16 : Dividable p b
     ge16 with <-cmp ( Euclid.eqa ge11 * p ) (  Euclid.eqb ge11 * a )
-    ... | tri< a ¬b ¬c = record { factor = b * Euclid.eqa ge11 -  Dividable.factor div-ab * Euclid.eqb ge11 ; is-factor = ge14 (<to≤ a) }  
-    ... | tri≈ ¬a eq ¬c = record { factor = b * Euclid.eqa ge11 -  Dividable.factor div-ab * Euclid.eqb ge11 ; is-factor = ge14 (ge17 _ _ eq)  }  
-    ... | tri> ¬a ¬b c = record { factor = Dividable.factor div-ab * Euclid.eqb ge11  - b * Euclid.eqa ge11 ; is-factor = ge15 c }  
+    ... | tri< a ¬b ¬c = record { factor = (Dividable.factor div-ab * Euclid.eqb ge11)  - (b * Euclid.eqa ge11) ; is-factor = ge15 a }
+    ... | tri≈ ¬a eq ¬c = record { factor = (b * Euclid.eqa ge11) - ( Dividable.factor div-ab * Euclid.eqb ge11) ; is-factor = ge19 eq }
+    ... | tri> ¬a ¬b c = record { factor = (b * Euclid.eqa ge11) -  (Dividable.factor div-ab * Euclid.eqb ge11) ; is-factor = ge14 c }  
 
 
 
--- a/automaton-in-agda/src/nat.agda	Mon Jun 28 23:21:25 2021 +0900
+++ b/automaton-in-agda/src/nat.agda	Tue Jun 29 09:35:12 2021 +0900
@@ -301,6 +301,13 @@
             lt : {x y z : ℕ } → suc y ≤ x → z + y * z ≤ x * z
             lt {x} {y} {z} le = *≤ le 
 
+distr-minus-*' : {z x y : ℕ } → z * (minus x y)  ≡ minus (z * x) (z * y) 
+distr-minus-*' {z} {x} {y} = begin
+        z * (minus x y) ≡⟨ *-comm _ (x - y) ⟩
+        (minus x y) * z ≡⟨ distr-minus-* {x} {y} {z} ⟩
+        minus (x * z) (y * z) ≡⟨ cong₂ (λ j k → j - k ) (*-comm x z ) (*-comm y z) ⟩
+        minus (z * x) (z * y) ∎  where open ≡-Reasoning
+
 minus- : {x y z : ℕ } → suc x > z + y → minus (minus x y) z ≡ minus x (y + z)
 minus- {x} {y} {z} gt = +m= {_} {_} {z} ( begin
            minus (minus x y) z + z