Mercurial > hg > Members > kono > Proof > automaton

changeset 151:9e16cbec717b

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 Fri, 01 Jan 2021 22:10:10 +0900
parents 36d3ecce01b2
children f42008080919
files agda/gcd.agda
diffstat 1 files changed, 42 insertions(+), 27 deletions(-) [+]
line wrap: on
line diff
--- a/agda/gcd.agda	Fri Jan 01 12:36:23 2021 +0900
+++ b/agda/gcd.agda	Fri Jan 01 22:10:10 2021 +0900
@@ -9,6 +9,7 @@
 open import Relation.Binary.PropositionalEquality
 open import Relation.Binary.Definitions
 open import nat
+open import logic
 
 even : (n : ℕ ) → Set
 even zero = ⊤
@@ -32,16 +33,6 @@
 even*n : {n m : ℕ } → even n → even ( n * m )
 even*n {n} {m} en = subst even (*-comm m n) (n*even {m} {n} en)
 
-gcd2 : ( i i0 j j0 : ℕ ) → i ≤ i0 → j ≤ j0 → ℕ
-gcd2 zero i0 zero j0 i<i0 j<j0  = j0
-gcd2 zero i0 (suc zero) j0 i<i0 j<j0 = 1
-gcd2 zero zero (suc (suc j)) j0 i<i0 j<j0 = j0
-gcd2 zero (suc i0) (suc (suc j)) j0 i<i0 j<j0 = gcd2 i0 (suc i0) (suc j) (suc (suc j)) refl-≤s refl-≤s 
-gcd2 (suc zero) i0 zero j0 i<i0 j<j0 = 1
-gcd2 (suc (suc i)) i0 zero zero i<i0 j<j0 = i0
-gcd2 (suc (suc i)) i0 zero (suc j0) i<i0 j<j0 = gcd2 (suc i) (suc (suc i))  j0 (suc j0)   refl-≤s refl-≤s 
-gcd2 (suc i) i0 (suc j) j0 i<i0 j<j0 = gcd2 i i0 j j0 (≤-trans refl-≤s i<i0) (≤-trans refl-≤s j<j0)   
-
 gcd1 : ( i i0 j j0 : ℕ ) → ℕ
 gcd1 zero i0 zero j0 with <-cmp i0 j0
 ... | tri< a ¬b ¬c = j0
@@ -77,22 +68,41 @@
 gcd22 (suc i) i0 zero o0 = refl
 gcd22 (suc i) i0 (suc o) o0 = refl 
 
--- gcd27 : ( i i0 : ℕ ) → gcd1 i i0 0 1 ≤ 1
--- gcd27 zero zero = ≤-refl
--- gcd27 zero (suc i0) = {!!}
--- gcd27 (suc i) zero = {!!}
--- gcd27 (suc i) (suc i0) = {!!}
+gcdmm : (n m : ℕ) → gcd1 n m n m ≡ m
+gcdmm zero m with <-cmp m m
+... | tri< a ¬b ¬c = refl
+... | tri≈ ¬a refl ¬c = refl
+... | tri> ¬a ¬b c = refl
+gcdmm (suc n) m  = subst (λ k → k ≡ m) (sym (gcd22 n m n m )) (gcdmm n m )
+
+record Comp ( m n : ℕ ) : Set where
+   field
+       non-1 : 1 < m
+       comp : ℕ
+       is-comp : n * comp ≡ m
+
+gcd28 : (n m  : ℕ) → Comp n m → Comp (n bb
+gcd28 = ?
 
-gcd-kk : ( i : ℕ ) → gcd1 i i i i ≡ i
-gcd-kk zero = refl
-gcd-kk (suc i) = gcd-kk1 i i i i refl refl where
-   gcd-kk1 : (i i0 j j0 : ℕ) → i ≡ j → i0 ≡ j0 →  gcd1 (suc i) (suc i0) (suc j) (suc j0) ≡ suc i0
-   gcd-kk1 zero i0 zero j0 i=j i0=j0 with <-cmp (suc i0) (suc j0)
-   ... | tri< a ¬b ¬c = ⊥-elim (¬b (cong suc i0=j0))
-   ... | tri≈ ¬a refl ¬c = refl
-   ... | tri> ¬a ¬b c = ⊥-elim (¬b (cong suc i0=j0))
-   gcd-kk1 (suc i) i0 (suc j) j0 refl i0=j0 = 
-        gcd-kk1 i i0 j j0 refl i0=j0 
+gcd27 : (n m i : ℕ) → 1 < m  → gcd n i ≡ m → Comp m n ∨ Comp m i
+gcd27 n m i 1<m gn = gcd271 n n i i gn where
+    gcd271 : (n n0 i i0 : ℕ ) → gcd1 n n0 i i0 ≡ m → Comp m n0 ∨ Comp m i0
+    gcd271 zero n0 zero i0 eq with <-cmp n0 i0
+    ... | tri< a ¬b ¬c = case2 (record { non-1 = 1<m ; comp = 1 ; is-comp = subst (λ k → k ≡ m) {!!} eq })
+    ... | tri≈ ¬a refl ¬c = case1 (record { non-1 = 1<m ; comp = 1 ; is-comp = subst (λ k → k ≡ m) {!!} eq })
+    ... | tri> ¬a ¬b c = case1 (record { non-1 = 1<m ; comp = 1 ; is-comp = subst (λ k → k ≡ m) {!!} eq })
+    gcd271 zero n0 (suc zero) i0 eq = ⊥-elim ( nat-≡< eq 1<m )
+    gcd271 zero zero (suc (suc i)) i0 eq = case2 (record { non-1 = 1<m ; comp = 1 ; is-comp = subst (λ k → k ≡ m) {!!} eq })
+    gcd271 zero (suc n0) (suc (suc i)) i0 eq with gcd271 n0 (suc n0) (suc i) (suc (suc i)) eq
+    ... | case1 t = case1 t
+    -- t : Comp m (suc (suc i)),    (suc n0) + (suc (suc i)) ≡ i0
+    ... | case2 t = case2 (record { non-1 = 1<m ; comp = suc (suc i) ; is-comp = subst (λ k → k ≡ m) {!!} eq })
+    gcd271 (suc zero) n0 zero i0 eq = ⊥-elim ( nat-≡< eq 1<m )
+    gcd271 (suc (suc n)) n0 zero zero eq = case2 (record { non-1 = 1<m ; comp = n0 ; is-comp = subst (λ k → k ≡ m) {!!} eq })
+    gcd271 (suc (suc n)) n0 zero (suc i0) eq = {!!}
+    gcd271 (suc n) n0 (suc i) i0 eq with gcd271 n n0 i i0 (trans (sym (gcd22 n n0 i i0)) eq )
+    ... | case1 x = case1 x
+    ... | case2 x = case2 x
 
 gcd26 : (n m i : ℕ) → 1 < n → 1 < m  → gcd n i ≡ m → ¬ ( gcd n m ≡ 1 )
 gcd26 n m i 1<n 1<m gi g1 = gcd261 n n m m i i 1<n 1<m gi g1 where
@@ -100,14 +110,19 @@
     gcd261 zero n0 m m0 i i0 () 1<m gi g1
     -- gi       : gcd1 (suc n) n0 zero i0 ≡ m0
     -- g1       : gcd1 (suc n) n0 m m0 ≡ 1
-    gcd261 (suc n) n0 m m0 zero i0 1<n 1<m gi g1 = {!!}
+    gcd261 (suc zero) n0 m m0 zero i0 1<n 1<m gi g1 = ⊥-elim (  nat-≡< gi 1<m )
+    gcd261 (suc (suc n)) n0 zero m0 zero zero 1<n 1<m gi g1 = {!!}
+    gcd261 (suc (suc n)) n0 zero m0 zero (suc i0) 1<n 1<m gi g1 = {!!}
+    gcd261 (suc (suc n)) n0 (suc zero) m0 zero i0 1<n 1<m gi g1 = {!!}
+    gcd261 (suc (suc n)) n0 (suc (suc m)) m0 zero zero 1<n 1<m gi g1 = {!!}
+    gcd261 (suc (suc n)) n0 (suc (suc m)) m0 zero (suc i0) 1<n 1<m gi g1 = {!!}
     -- gi       : gcd1 (suc n) n0 (suc i) i0 ≡ m0
     -- g1       : gcd1 (suc n) n0 zero m0 ≡ 1
     gcd261 (suc n) n0 zero m0 (suc i) i0 1<n 1<m gi g1 = {!!}
     gcd261 (suc zero) n0 (suc m) m0 (suc i) i0 1<n 1<m gi g1 = ⊥-elim ( nat-<≡ 1<n  )
     gcd261 (suc (suc zero)) n0 (suc m) m0 (suc zero) i0 1<n 1<m gi g1 = ⊥-elim (  nat-≡< gi 1<m )
     -- gi       : gcd1 0 n0 i i0 ≡ m0
-    gcd261 (suc (suc zero)) n0 (suc zero) m0 (suc (suc i)) i0 1<n 1<m gi g1 = {!!}
+    gcd261 (suc (suc zero)) n0 (suc zero) m0 (suc (suc i)) i0 1<n 1<m gi refl = {!!}
     -- gi       : gcd1 0 n0 i i0 ≡ m0
     -- g1       : gcd1 0 n0 m m0 ≡ 1
     gcd261 (suc (suc zero)) n0 (suc (suc m)) m0 (suc (suc i)) i0 1<n 1<m gi g1 = {!!}