Mercurial > hg > Members > kono > Proof > automaton

changeset 248:de959bb968ed

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 23:21:25 +0900
parents 61d9fdb22f2d
children 0ef9a73cae45
files automaton-in-agda/src/gcd.agda
diffstat 1 files changed, 13 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Mon Jun 28 23:01:27 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Mon Jun 28 23:21:25 2021 +0900
@@ -752,18 +752,21 @@
     ge11 = gcd-euclid1 p p a a GCDi
     ge18 : (Dividable.factor div-ab * Euclid.eqb ge11) * p ≡  b * (a * Euclid.eqb ge11 )
     ge18 = begin
-         (Dividable.factor div-ab * Euclid.eqb ge11) * p  ≡⟨ {!!}   ⟩
-         (Euclid.eqb ge11 * p)  ≡⟨ {!!}   ⟩
-         (p * Euclid.eqb ge11 )  ≡⟨ {!!}   ⟩
-         (Dividable.factor div-ab * p ) * Euclid.eqb ge11   ≡⟨ {!!}   ⟩
-         (Dividable.factor div-ab * p + 0) * Euclid.eqb ge11   ≡⟨ {!!}   ⟩
-         (a * b) * Euclid.eqb ge11   ≡⟨ {!!}   ⟩
-         (b * a) * Euclid.eqb ge11   ≡⟨ {!!}   ⟩
+         (Dividable.factor div-ab * Euclid.eqb ge11) * p  ≡⟨ *-assoc (Dividable.factor div-ab) (Euclid.eqb ge11) p ⟩
+         Dividable.factor div-ab * (Euclid.eqb ge11 * p)  ≡⟨ cong (λ k →  Dividable.factor div-ab  * k)  (*-comm _ p) ⟩
+          Dividable.factor div-ab * (p * Euclid.eqb ge11 )  ≡⟨ sym (*-assoc  (Dividable.factor div-ab) p (Euclid.eqb ge11) ) ⟩
+         (Dividable.factor div-ab * p ) * Euclid.eqb ge11   ≡⟨ cong (λ k → k * Euclid.eqb ge11 ) (+-comm 0  (Dividable.factor div-ab * p )) ⟩
+         (Dividable.factor div-ab * p + 0) * Euclid.eqb ge11   ≡⟨ cong (λ k → k *  Euclid.eqb ge11) (((Dividable.is-factor div-ab))) ⟩
+         (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
     ge14 lt = begin
-         (b * Euclid.eqa ge11 - Dividable.factor div-ab * Euclid.eqb ge11) * p + 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) + 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 ))  ≡⟨ {!!}   ⟩
@@ -774,7 +777,7 @@
          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 lt = begin
-         (Dividable.factor div-ab * Euclid.eqb ge11 - b * Euclid.eqa ge11  ) * p + 0  ≡⟨ {!!}   ⟩
+         (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) * 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 )   ≡⟨ {!!}   ⟩