Members/kono/Proof/automaton: agda/gcd.agda comparison

comparison agda/gcd.agda @ 154:ba7d4cc92e60

... gcd (i + j) j ≡ gcd i j

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sat, 02 Jan 2021 04:29:20 +0900
parents	d78fc1951c26
children	4b6063ad6de2

comparison

equal deleted inserted replaced

-:d78fc1951c26
+:ba7d4cc92e60
 record Comp ( m n : ℕ ) : Set where
 field
 non-1 : 1 < m
 comp : ℕ
 is-comp : n * comp ≡ m
-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 = case1 (gcd272 t) where
-gcd272 : Comp m (suc (suc i)) → Comp m (suc n0)
-gcd272 = {!!}
-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 = gcd271 n n0 i i0 (trans (sym (gcd22 n n0 i i0)) eq )
-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
-gcd261 : (n n0 m m0 i i0 : ℕ) → 1 < n → 1 < m0  → gcd1 n n0 i i0 ≡ m0 → ¬ ( gcd1 n n0 m m0 ≡ 1 )
-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 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 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 = {!!}
-gcd261 (suc (suc (suc n))) n0 (suc m) m0 (suc i) i0 1<n 1<m gi g1 =
-gcd261 (suc (suc n)) n0 m m0 i i0 (s≤s (s≤s z≤n)) 1<m gi g1
 gcdsym2 : (i j : ℕ) → gcd1 zero i zero j ≡ gcd1 zero j zero i
 gcdsym2 i j with <-cmp i j | <-cmp j i
 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁)
 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (nat-≡< (sym b) a)
 gcd1 (i + suc j1)   (i0 + suc j) (suc j1) j0 ≡⟨ cong (λ k → gcd1 k (i0 + suc j) (suc j1) j0 ) (gcd202 i j1) ⟩
 gcd1 (suc (i + j1)) (i0 + suc j) (suc j1) j0 ≡⟨ gcd22 (i + j1) (i0 + suc j) j1 j0 ⟩
 gcd1 (i + j1) (i0 + suc j) j1 j0 ≡⟨ gcd201 i i0 j j0 j1 ⟩
 gcd1 i (i0 + suc j) zero j0 ∎ where open ≡-Reasoning
 gcd200 : (i i0 j j0 : ℕ) → gcd1 (i + j) (i0 + j) j j0 ≡ gcd1 i i j0 j0
--- gcd200 i i0 zero j0 = subst₂ (λ m k → gcd1 m k zero j0 ≡ gcd1 i i0 zero j0 ) (+-comm zero i) (+-comm zero i0) refl
 gcd200 i i0 zero j0 = {!!}
 gcd200 (suc (suc i)) i0 (suc j) (suc j0) = gcd201 (suc (suc i)) i0 j (suc j0) (suc j)
 gcd200 zero zero (suc zero) j0 = {!!}
 gcd200 zero zero (suc (suc j)) j0 = {!!}
 gcd200 zero (suc i0) (suc j) j0 = {!!}
 gcd200 (suc zero) i0 (suc j) j0 = {!!}
-gcd200 (suc (suc i)) i0 (suc j) zero = ?
+gcd200 (suc (suc i)) i0 (suc j) zero = {!!}
+gcd4 : ( n k : ℕ ) → gcd n k ≡ k → k ≤ n
+gcd4 n k gn = gcd40 n n k k gn where
+gcd40 :  (i i0 j j0 : ℕ) → gcd1 i i0 j j0 ≡ j0 → j0 ≤ i0
+gcd40 zero i0 zero j0  gn = {!!}
+gcd40 zero i0 (suc j) j0 gn = {!!}
+gcd40 (suc i) i0 zero j0 gn = {!!}
+gcd40 (suc i) i0 (suc j) j0 gn = gcd40 i i0 j j0 (subst (λ k → k ≡ j0) (gcd22 i i0 j j0) gn)
+gcd3 : ( n k : ℕ ) → n ≤ k + k → gcd n k ≡ k → n ≡ k
+gcd3 n k n<2k gn = {!!}
+gcd23 : ( n m k : ℕ) → gcd n k ≡ k → gcd m k ≡ k → k ≤ gcd n m
+gcd23 = {!!}
 gcd24 : { n m k : ℕ} → n > 1 → m > 1 → k > 1 → gcd n k ≡ k → gcd m k ≡ k → ¬ ( gcd n m ≡ 1 )
-gcd24 {n} {m} {k} 1<n 1<m 1<k gn gm gnm = gcd21 n n m m k k 1<n 1<m 1<k gn gm gnm where
+gcd24 {n} {m} {k} 1<n 1<m 1<k gn gm gnm = ⊥-elim ( nat-≡< (sym gnm) (≤-trans 1<k (gcd23 n m k gn gm  )))
-gcd23 : {i0 j0 : ℕ } → 1 < i0  → 1 < j0 → 1 < gcd1 zero i0 zero j0
-gcd23 {i0} {j0} 1<i 1<j with <-cmp i0 j0
-... | tri< a ¬b ¬c = 1<j
-... | tri≈ ¬a refl ¬c = 1<i
-... | tri> ¬a ¬b c = 1<i
-1<ss : {j : ℕ} → 1 < suc (suc j)
-1<ss = s≤s (s≤s z≤n)
-gcd21 : ( i i0 j j0 o o0 : ℕ ) → 1 < i0 → 1 < j0 → 1 < o0 →  gcd1 i i0 o o0 ≡ k → gcd1 j j0 o o0 ≡ k → gcd1 i i0 j j0 ≡ 1 → ⊥
-gcd21 zero i0 zero j0 o o0 1<i 1<j 1<o refl gm gnm = nat-≡< (sym gnm) (gcd23 1<i 1<j)
-gcd21 zero i0 (suc j) j0 zero o0 1<i 1<j 1<o refl gm gnm = gcd25 i0 o0 j j0 1<o 1<i 1<k gm (subst (λ k → k ≡ 1) (gcdsym1 zero _ (suc j) _) gnm)  where
--- gcd1 (suc j) (suc (suc j)) (suc o0) (suc (suc o0)) ≡ suc (suc i0) , gcd1 (suc j) (suc (suc j)) (suc i0) (suc (suc i0)) ≡ 1
-gcd25 : (i0 o0 j j0 : ℕ) → 1 < o0 → 1 < i0
-→ 1 < gcd1 zero i0 zero o0
-→ ( gm : gcd1 (suc j) j0 zero o0 ≡ gcd1 zero i0 zero o0 ) → (gnm : gcd1 (suc j) j0 zero i0 ≡ 1) → ⊥
-gcd25 i0 o0 zero j0 1<o 1<i 1<k gm refl with <-cmp i0 o0
-... | tri< a ¬b ¬c    = ⊥-elim ( nat-≡< gm 1<o )
-... | tri≈ ¬a refl ¬c = ⊥-elim ( nat-≡< gm 1<o )
-... | tri> ¬a ¬b c    = ⊥-elim ( nat-≡< gm 1<i )
--- gm       : gcd1 (suc j) (suc (suc j)) (suc o0) (suc (suc o0)) ≡ (gcd1 zero (suc i0) zero (suc (suc o0))
---            gcd1 j       (suc (suc j))       o0 (suc (suc o0))
--- gnm      : gcd1 (suc j) (suc (suc j)) i0 (suc i0) ≡ 1
-gcd25 i0       (suc zero)     (suc j) j0 1<o 1<i 1<k gm gnm = {!!} -- ⊥-elim ( nat-≤> (subst (λ k → k ≤ 1 ) gm (gcd27 (suc j) (suc (suc j)))) 1<k )
-gcd25 (suc zero) (suc (suc o0)) (suc j) j0 1<o 1<i 1<k gm gnm = {!!}
---     (suc (suc i0)) > (suc (suc o0)) → gm = gnm → (suc (suc i0)) ≡ 1
---     (suc (suc i0)) < (suc (suc o0)) → ? gcd1 (suc j) (suc (suc j)) (suc o0) (suc (suc o0)) ≡  (suc (suc o0))
---                                         gcd1 (suc j) (suc (suc j)) (suc i0) (suc (suc i0)) ≡  1
-gcd25 (suc (suc i0)) (suc (suc o0)) (suc j) j0 1<o 1<i 1<k gm gnm with <-cmp  (suc (suc i0))   (suc (suc o0))
-... | tri< a ¬b ¬c = {!!}
-... | tri≈ ¬a b ¬c = {!!}
-... | tri> ¬a ¬b c = gcd26 {!!} {!!} {!!} {!!} {!!} {!!} {!!}
-gcd21 zero i0 (suc j) j0 (suc zero) o0 1<i 1<j 1<o refl gm gnm = nat-<≡ 1<k
-gcd21 zero (suc i0) (suc j) j0 (suc (suc o)) o0 1<i 1<j 1<o gn gm gnm =
-gcd21 i0 {!!} (suc j) j0 (suc o) (suc (suc o)) 1<i 1<j {!!} gn {!!} {!!}
-gcd21 (suc i) i0 zero j0 o o0 1<i 1<j 1<o gn gm gnm = {!!}
-gcd21 (suc i) i0 (suc j) j0 zero o0 1<i 1<j 1<o gn gm gnm = {!!}
-gcd21 (suc i) i0 (suc j) j0 (suc o) o0 1<i 1<j 1<o gn gm gnm =
-gcd21 i i0 j j0 o o0 1<i 1<j 1<o (subst (λ m → m ≡ k) (gcd22 i i0 _ _ ) gn)
-(subst (λ m → m ≡ k) (gcd22 j j0 _ _ ) gm) (subst (λ k → k ≡ 1) (gcd22 i i0 _ _ ) gnm)
 record Even (i : ℕ) : Set where
 field
 j : ℕ
 is-twice : i ≡ 2 * j

Mercurial > hg > Members > kono > Proof > automaton

comparison agda/gcd.agda @ 154:ba7d4cc92e60