Mercurial > hg > Members > kono > Proof > automaton

changeset 237:709e63cb9d19

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 23:13:07 +0900
parents 9f7e4a4415f7
children 3aad251b8d8b
files automaton-in-agda/src/gcd.agda
diffstat 1 files changed, 14 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Sun Jun 27 22:43:20 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Sun Jun 27 23:13:07 2021 +0900
@@ -299,6 +299,17 @@
    → 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 =
@@ -312,6 +323,9 @@
                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 =