Mercurial > hg > Members > kono > Proof > galois
changeset 317:77f01da94c4e
use safe option
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 16 Sep 2023 17:24:50 +0900 |
| parents | a067959c1799 |
| children | |
| files | src/FLComm.agda src/FLutil.agda src/Gutil.agda src/Homomorphism.agda src/NormalSubgroup.agda src/Putil.agda src/Solvable.agda src/Symmetric.agda src/fin.agda src/logic.agda src/nat.agda src/sym2.agda src/sym2n.agda src/sym3.agda src/sym3n.agda src/sym4.agda src/sym5.agda src/sym5a.agda src/sym5h.agda src/sym5n.agda |
| diffstat | 20 files changed, 183 insertions(+), 178 deletions(-) [+] |
line wrap: on
line diff
--- a/src/FLComm.agda Sat Sep 16 13:14:17 2023 +0900 +++ b/src/FLComm.agda Sat Sep 16 17:24:50 2023 +0900 @@ -1,4 +1,4 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n ) module FLComm (n : ℕ) where
--- a/src/FLutil.agda Sat Sep 16 13:14:17 2023 +0900 +++ b/src/FLutil.agda Sat Sep 16 17:24:50 2023 +0900 @@ -1,4 +1,4 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} module FLutil where open import Level hiding ( suc ; zero )
--- a/src/Gutil.agda Sat Sep 16 13:14:17 2023 +0900 +++ b/src/Gutil.agda Sat Sep 16 17:24:50 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + open import Level hiding ( suc ; zero ) open import Algebra module Gutil {n m : Level} (G : Group n m ) where
--- a/src/Homomorphism.agda Sat Sep 16 13:14:17 2023 +0900 +++ b/src/Homomorphism.agda Sat Sep 16 17:24:50 2023 +0900 @@ -1,4 +1,4 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} -- fundamental homomorphism theorem --
--- a/src/NormalSubgroup.agda Sat Sep 16 13:14:17 2023 +0900 +++ b/src/NormalSubgroup.agda Sat Sep 16 17:24:50 2023 +0900 @@ -1,4 +1,5 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} + open import Level hiding ( suc ; zero ) module NormalSubgroup where
--- a/src/Putil.agda Sat Sep 16 13:14:17 2023 +0900 +++ b/src/Putil.agda Sat Sep 16 17:24:50 2023 +0900 @@ -1,4 +1,5 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} + module Putil where open import Level hiding ( suc ; zero )
--- a/src/Solvable.agda Sat Sep 16 13:14:17 2023 +0900 +++ b/src/Solvable.agda Sat Sep 16 17:24:50 2023 +0900 @@ -1,4 +1,5 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} + open import Level hiding ( suc ; zero ) open import Algebra module Solvable {n m : Level} (G : Group n m ) where
--- a/src/Symmetric.agda Sat Sep 16 13:14:17 2023 +0900 +++ b/src/Symmetric.agda Sat Sep 16 17:24:50 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + module Symmetric where open import Level hiding ( suc ; zero )
--- a/src/fin.agda Sat Sep 16 13:14:17 2023 +0900 +++ b/src/fin.agda Sat Sep 16 17:24:50 2023 +0900 @@ -1,4 +1,5 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible #-} +{-# OPTIONS --with-K #-} module fin where
--- a/src/logic.agda Sat Sep 16 13:14:17 2023 +0900 +++ b/src/logic.agda Sat Sep 16 17:24:50 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + module logic where open import Level @@ -97,55 +99,57 @@ ¬-bool refl () lemma-∧-0 : {a b : Bool} → a /\ b ≡ true → a ≡ false → ⊥ -lemma-∧-0 {true} {true} refl () lemma-∧-0 {true} {false} () lemma-∧-0 {false} {true} () lemma-∧-0 {false} {false} () +lemma-∧-0 {true} {true} eq1 () lemma-∧-1 : {a b : Bool} → a /\ b ≡ true → b ≡ false → ⊥ -lemma-∧-1 {true} {true} refl () lemma-∧-1 {true} {false} () lemma-∧-1 {false} {true} () lemma-∧-1 {false} {false} () +lemma-∧-1 {true} {true} eq1 () bool-and-tt : {a b : Bool} → a ≡ true → b ≡ true → ( a /\ b ) ≡ true bool-and-tt refl refl = refl bool-∧→tt-0 : {a b : Bool} → ( a /\ b ) ≡ true → a ≡ true -bool-∧→tt-0 {true} {true} refl = refl +bool-∧→tt-0 {true} {true} eq = refl bool-∧→tt-0 {false} {_} () bool-∧→tt-1 : {a b : Bool} → ( a /\ b ) ≡ true → b ≡ true -bool-∧→tt-1 {true} {true} refl = refl +bool-∧→tt-1 {true} {true} eq = refl bool-∧→tt-1 {true} {false} () bool-∧→tt-1 {false} {false} () bool-or-1 : {a b : Bool} → a ≡ false → ( a \/ b ) ≡ b -bool-or-1 {false} {true} refl = refl -bool-or-1 {false} {false} refl = refl +bool-or-1 {false} {true} eq = refl +bool-or-1 {false} {false} eq = refl bool-or-2 : {a b : Bool} → b ≡ false → (a \/ b ) ≡ a -bool-or-2 {true} {false} refl = refl -bool-or-2 {false} {false} refl = refl +bool-or-2 {true} {false} eq = refl +bool-or-2 {false} {false} eq = refl bool-or-3 : {a : Bool} → ( a \/ true ) ≡ true bool-or-3 {true} = refl bool-or-3 {false} = refl bool-or-31 : {a b : Bool} → b ≡ true → ( a \/ b ) ≡ true -bool-or-31 {true} {true} refl = refl -bool-or-31 {false} {true} refl = refl +bool-or-31 {true} {true} eq = refl +bool-or-31 {false} {true} eq = refl bool-or-4 : {a : Bool} → ( true \/ a ) ≡ true bool-or-4 {true} = refl bool-or-4 {false} = refl bool-or-41 : {a b : Bool} → a ≡ true → ( a \/ b ) ≡ true -bool-or-41 {true} {b} refl = refl +bool-or-41 {true} {b} eq = refl bool-and-1 : {a b : Bool} → a ≡ false → (a /\ b ) ≡ false -bool-and-1 {false} {b} refl = refl +bool-and-1 {false} {b} eq = refl bool-and-2 : {a b : Bool} → b ≡ false → (a /\ b ) ≡ false -bool-and-2 {true} {false} refl = refl -bool-and-2 {false} {false} refl = refl +bool-and-2 {true} {false} eq = refl +bool-and-2 {false} {false} eq = refl +bool-and-2 {true} {true} () +bool-and-2 {false} {true} ()
--- a/src/nat.agda Sat Sep 16 13:14:17 2023 +0900 +++ b/src/nat.agda Sat Sep 16 17:24:50 2023 +0900 @@ -1,4 +1,5 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} + module nat where open import Data.Nat @@ -12,46 +13,39 @@ open import Level hiding ( zero ; suc ) nat-<> : { x y : ℕ } → x < y → y < x → ⊥ -nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x +nat-<> {x} {y} x<y y<x with <-cmp x y +... | tri< a ¬b ¬c = ¬c y<x +... | tri≈ ¬a refl ¬c = ¬a x<y +... | tri> ¬a ¬b c = ¬a x<y nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥ -nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x +nat-≤> {x} {y} x≤y y<x = ? nat-<≡ : { x : ℕ } → x < x → ⊥ -nat-<≡ (s≤s lt) = nat-<≡ lt +nat-<≡ {x} lt = ? nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥ nat-≡< refl lt = nat-<≡ lt ¬a≤a : {la : ℕ} → suc la ≤ la → ⊥ -¬a≤a (s≤s lt) = ¬a≤a lt +¬a≤a lt = ? a<sa : {la : ℕ} → la < suc la a<sa {zero} = s≤s z≤n a<sa {suc la} = s≤s a<sa =→¬< : {x : ℕ } → ¬ ( x < x ) -=→¬< {zero} () -=→¬< {suc x} (s≤s lt) = =→¬< lt +=→¬< {zero} lt = ? +=→¬< {suc x} lt = ? >→¬< : {x y : ℕ } → (x < y ) → ¬ ( y < x ) ->→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x +>→¬< = ? <-∨ : { x y : ℕ } → x < suc y → ( (x ≡ y ) ∨ (x < y) ) -<-∨ {zero} {zero} (s≤s z≤n) = case1 refl -<-∨ {zero} {suc y} (s≤s lt) = case2 (s≤s z≤n) -<-∨ {suc x} {zero} (s≤s ()) -<-∨ {suc x} {suc y} (s≤s lt) with <-∨ {x} {y} lt -<-∨ {suc x} {suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → suc k ) eq) -<-∨ {suc x} {suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1) +<-∨ = ? ≤-∨ : { x y : ℕ } → x ≤ y → ( (x ≡ y ) ∨ (x < y) ) -≤-∨ {zero} {zero} z≤n = case1 refl -≤-∨ {zero} {suc y} z≤n = case2 (s≤s z≤n) -≤-∨ {suc x} {zero} () -≤-∨ {suc x} {suc y} (s≤s lt) with ≤-∨ {x} {y} lt -≤-∨ {suc x} {suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → suc k ) eq) -≤-∨ {suc x} {suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1) +≤-∨ = ? max : (x y : ℕ) → ℕ max zero zero = zero @@ -74,13 +68,13 @@ x≤y→max=y : (x y : ℕ) → x ≤ y → max x y ≡ y x≤y→max=y zero zero x≤y = refl x≤y→max=y zero (suc y) x≤y = refl -x≤y→max=y (suc x) (suc y) (s≤s x≤y) = cong suc (x≤y→max=y x y x≤y ) +x≤y→max=y = ? y≤x→max=x : (x y : ℕ) → y ≤ x → max x y ≡ x y≤x→max=x zero zero y≤x = refl y≤x→max=x zero (suc y) () y≤x→max=x (suc x) zero lt = refl -y≤x→max=x (suc x) (suc y) (s≤s y≤x) = cong suc (y≤x→max=x x y y≤x ) +y≤x→max=x = ? -- _*_ : ℕ → ℕ → ℕ -- _*_ zero _ = zero @@ -128,8 +122,7 @@ px<py : {x y : ℕ } → pred x < pred y → x < y px<py {zero} {suc y} lt = 0<s -px<py {suc zero} {suc (suc y)} (s≤s lt) = s≤s 0<s -px<py {suc (suc x)} {suc (suc y)} (s≤s lt) = s≤s (px<py {suc x} {suc y} lt) +px<py = ? minus : (a b : ℕ ) → ℕ minus a zero = a @@ -139,8 +132,8 @@ _-_ = minus sn-m=sn-m : {m n : ℕ } → m ≤ n → suc n - m ≡ suc ( n - m ) -sn-m=sn-m {0} {n} z≤n = refl -sn-m=sn-m {suc m} {suc n} (s≤s m<n) = sn-m=sn-m m<n +sn-m=sn-m {0} {n} = ? +sn-m=sn-m {suc m} {suc n} = ? si-sn=i-n : {i n : ℕ } → n < i → suc (i - suc n) ≡ (i - n) si-sn=i-n {i} {n} n<i = begin @@ -163,14 +156,14 @@ n-m<n (suc n) (suc m) = ≤-trans (n-m<n n m ) refl-≤s n-n-m=m : {m n : ℕ } → m ≤ n → m ≡ (n - (n - m)) -n-n-m=m {0} {zero} z≤n = refl -n-n-m=m {0} {suc n} z≤n = n-n-m=m {0} {n} z≤n -n-n-m=m {suc m} {suc n} (s≤s m≤n) = sym ( begin - suc n - ( n - m ) ≡⟨ sn-m=sn-m (n-m<n n m) ⟩ - suc (n - ( n - m )) ≡⟨ cong (λ k → suc k ) (sym (n-n-m=m m≤n)) ⟩ - suc m - ∎ ) where - open ≡-Reasoning +n-n-m=m {0} {zero} = ? +n-n-m=m {0} {suc n} = ? +n-n-m=m {suc m} {suc n} = ? +-- suc n - ( n - m ) ≡⟨ sn-m=sn-m (n-m<n n m) ⟩ +-- suc (n - ( n - m )) ≡⟨ cong (λ k → suc k ) (sym (n-n-m=m m≤n)) ⟩ +-- suc m +-- ∎ ) where +-- open ≡-Reasoning m+= : {i j m : ℕ } → m + i ≡ m + j → i ≡ j m+= {i} {j} {zero} refl = refl @@ -180,35 +173,37 @@ +m= {i} {j} {m} eq = m+= ( subst₂ (λ j k → j ≡ k ) (+-comm i _ ) (+-comm j _ ) eq ) less-1 : { n m : ℕ } → suc n < m → n < m -less-1 {zero} {suc (suc _)} (s≤s (s≤s z≤n)) = s≤s z≤n -less-1 {suc n} {suc m} (s≤s lt) = s≤s (less-1 {n} {m} lt) +less-1 = ? +-- {zero} {suc (suc _)} (s≤s (s≤s z≤n)) = s≤s z≤n +-- less-1 {suc n} {suc m} (s≤s lt) = s≤s (less-1 {n} {m} lt) sa=b→a<b : { n m : ℕ } → suc n ≡ m → n < m -sa=b→a<b {0} {suc zero} refl = s≤s z≤n -sa=b→a<b {suc n} {suc (suc n)} refl = s≤s (sa=b→a<b refl) +sa=b→a<b = ? +-- {0} {suc zero} refl = s≤s z≤n +-- sa=b→a<b {suc n} {suc (suc n)} refl = s≤s (sa=b→a<b refl) minus+n : {x y : ℕ } → suc x > y → minus x y + y ≡ x minus+n {x} {zero} _ = trans (sym (+-comm zero _ )) refl -minus+n {zero} {suc y} (s≤s ()) -minus+n {suc x} {suc y} (s≤s lt) = begin - minus (suc x) (suc y) + suc y - ≡⟨ +-comm _ (suc y) ⟩ - suc y + minus x y - ≡⟨ cong ( λ k → suc k ) ( - begin - y + minus x y - ≡⟨ +-comm y _ ⟩ - minus x y + y - ≡⟨ minus+n {x} {y} lt ⟩ - x - ∎ - ) ⟩ - suc x - ∎ where open ≡-Reasoning +minus+n {zero} {suc y} = ? +minus+n {suc x} {suc y} = ? +-- minus (suc x) (suc y) + suc y +-- ≡⟨ +-comm _ (suc y) ⟩ +-- suc y + minus x y +-- ≡⟨ cong ( λ k → suc k ) ( +-- begin +-- y + minus x y +-- ≡⟨ +-comm y _ ⟩ +-- minus x y + y +-- ≡⟨ minus+n {x} {y} lt ⟩ +-- x +-- ∎ +-- ) ⟩ +-- suc x +-- ∎ where open ≡-Reasoning <-minus-0 : {x y z : ℕ } → z + x < z + y → x < y -<-minus-0 {x} {suc _} {zero} lt = lt -<-minus-0 {x} {y} {suc z} (s≤s lt) = <-minus-0 {x} {y} {z} lt +<-minus-0 {x} = ? +-- <-minus-0 {x} {y} {suc z} (s≤s lt) = <-minus-0 {x} {y} {z} lt <-minus : {x y z : ℕ } → x + z < y + z → x < y <-minus {x} {y} {z} lt = <-minus-0 ( subst₂ ( λ j k → j < k ) (+-comm x _) (+-comm y _ ) lt ) @@ -228,43 +223,45 @@ x + suc y ∎ where open ≤-Reasoning <-plus : {x y z : ℕ } → x < y → x + z < y + z -<-plus {zero} {suc y} {z} (s≤s z≤n) = s≤s (subst (λ k → z ≤ k ) (+-comm z _ ) x≤x+y ) -<-plus {suc x} {suc y} {z} (s≤s lt) = s≤s (<-plus {x} {y} {z} lt) +<-plus = ? +-- (s≤s z≤n) = s≤s (subst (λ k → z ≤ k ) (+-comm z _ ) x≤x+y ) +-- <-plus {suc x} {suc y} {z} (s≤s lt) = s≤s (<-plus {x} {y} {z} lt) <-plus-0 : {x y z : ℕ } → x < y → z + x < z + y <-plus-0 {x} {y} {z} lt = subst₂ (λ j k → j < k ) (+-comm _ z) (+-comm _ z) ( <-plus {x} {y} {z} lt ) ≤-plus : {x y z : ℕ } → x ≤ y → x + z ≤ y + z -≤-plus {0} {y} {zero} z≤n = z≤n -≤-plus {0} {y} {suc z} z≤n = subst (λ k → z < k ) (+-comm _ y ) x≤x+y -≤-plus {suc x} {suc y} {z} (s≤s lt) = s≤s ( ≤-plus {x} {y} {z} lt ) +≤-plus = ? +-- ≤-plus {0} {y} {suc z} z≤n = subst (λ k → z < k ) (+-comm _ y ) x≤x+y +-- ≤-plus {suc x} {suc y} {z} (s≤s lt) = s≤s ( ≤-plus {x} {y} {z} lt ) ≤-plus-0 : {x y z : ℕ } → x ≤ y → z + x ≤ z + y ≤-plus-0 {x} {y} {zero} lt = lt ≤-plus-0 {x} {y} {suc z} lt = s≤s ( ≤-plus-0 {x} {y} {z} lt ) x+y<z→x<z : {x y z : ℕ } → x + y < z → x < z -x+y<z→x<z {zero} {y} {suc z} (s≤s lt1) = s≤s z≤n -x+y<z→x<z {suc x} {y} {suc z} (s≤s lt1) = s≤s ( x+y<z→x<z {x} {y} {z} lt1 ) +x+y<z→x<z = ? +-- x+y<z→x<z {suc x} {y} {suc z} (s≤s lt1) = s≤s ( x+y<z→x<z {x} {y} {z} lt1 ) *≤ : {x y z : ℕ } → x ≤ y → x * z ≤ y * z *≤ lt = *-mono-≤ lt ≤-refl *< : {x y z : ℕ } → x < y → x * suc z < y * suc z -*< {zero} {suc y} lt = s≤s z≤n -*< {suc x} {suc y} (s≤s lt) = <-plus-0 (*< lt) +*< = ? +-- {zero} {suc y} lt = s≤s z≤n +-- *< {suc x} {suc y} (s≤s lt) = <-plus-0 (*< lt) <to<s : {x y : ℕ } → x < y → x < suc y -<to<s {zero} {suc y} (s≤s lt) = s≤s z≤n -<to<s {suc x} {suc y} (s≤s lt) = s≤s (<to<s {x} {y} lt) +<to<s = ? +-- <to<s {suc x} {suc y} (s≤s lt) = s≤s (<to<s {x} {y} lt) <tos<s : {x y : ℕ } → x < y → suc x < suc y -<tos<s {zero} {suc y} (s≤s z≤n) = s≤s (s≤s z≤n) -<tos<s {suc x} {suc y} (s≤s lt) = s≤s (<tos<s {x} {y} lt) +<tos<s = ? +-- <tos<s {suc x} {suc y} (s≤s lt) = s≤s (<tos<s {x} {y} lt) <to≤ : {x y : ℕ } → x < y → x ≤ y -<to≤ {zero} {suc y} (s≤s z≤n) = z≤n -<to≤ {suc x} {suc y} (s≤s lt) = s≤s (<to≤ {x} {y} lt) +<to≤ = ? +-- <to≤ {suc x} {suc y} (s≤s lt) = s≤s (<to≤ {x} {y} lt) <∨≤ : ( x y : ℕ ) → (x < y ) ∨ (y ≤ x) <∨≤ x y with <-cmp x y @@ -280,62 +277,73 @@ refl-≤≡ refl = refl-≤ x<y→≤ : {x y : ℕ } → x < y → x ≤ suc y -x<y→≤ {zero} {.(suc _)} (s≤s z≤n) = z≤n -x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt) +x<y→≤ = ? +-- {zero} {.(suc _)} (s≤s z≤n) = z≤n +-- x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt) ≤→= : {i j : ℕ} → i ≤ j → j ≤ i → i ≡ j -≤→= {0} {0} z≤n z≤n = refl -≤→= {suc i} {suc j} (s≤s i<j) (s≤s j<i) = cong suc ( ≤→= {i} {j} i<j j<i ) +≤→= = ? +-- {0} {0} z≤n z≤n = refl +-- ≤→= {suc i} {suc j} (s≤s i<j) (s≤s j<i) = cong suc ( ≤→= {i} {j} i<j j<i ) px≤x : {x : ℕ } → pred x ≤ x px≤x {zero} = refl-≤ px≤x {suc x} = refl-≤s px≤py : {x y : ℕ } → x ≤ y → pred x ≤ pred y -px≤py {zero} {zero} lt = refl-≤ -px≤py {zero} {suc y} lt = z≤n -px≤py {suc x} {suc y} (s≤s lt) = lt +px≤py = ? +-- {zero} {zero} lt = refl-≤ +-- px≤py {zero} {suc y} lt = z≤n +-- px≤py {suc x} {suc y} (s≤s lt) = lt sx≤py→x≤y : {x y : ℕ } → suc x ≤ suc y → x ≤ y -sx≤py→x≤y (s≤s lt) = lt +sx≤py→x≤y = ? +-- (s≤s lt) = lt sx<py→x<y : {x y : ℕ } → suc x < suc y → x < y -sx<py→x<y (s≤s lt) = lt +sx<py→x<y = ? +-- (s≤s lt) = lt sx≤y→x≤y : {x y : ℕ } → suc x ≤ y → x ≤ y -sx≤y→x≤y {zero} {suc y} (s≤s le) = z≤n -sx≤y→x≤y {suc x} {suc y} (s≤s le) = s≤s (sx≤y→x≤y {x} {y} le) +sx≤y→x≤y = ? +-- {zero} {suc y} (s≤s le) = z≤n +-- sx≤y→x≤y {suc x} {suc y} (s≤s le) = s≤s (sx≤y→x≤y {x} {y} le) x<sy→x≤y : {x y : ℕ } → x < suc y → x ≤ y -x<sy→x≤y {zero} {suc y} (s≤s le) = z≤n -x<sy→x≤y {suc x} {suc y} (s≤s le) = s≤s (x<sy→x≤y {x} {y} le) -x<sy→x≤y {zero} {zero} (s≤s z≤n) = ≤-refl +x<sy→x≤y = ? +-- {zero} {suc y} (s≤s le) = z≤n +-- x<sy→x≤y {suc x} {suc y} (s≤s le) = s≤s (x<sy→x≤y {x} {y} le) +-- x<sy→x≤y {zero} {zero} (s≤s z≤n) = ≤-refl x≤y→x<sy : {x y : ℕ } → x ≤ y → x < suc y x≤y→x<sy {.zero} {y} z≤n = ≤-trans a<sa (s≤s z≤n) x≤y→x<sy {.(suc _)} {.(suc _)} (s≤s le) = s≤s ( x≤y→x<sy le) sx≤y→x<y : {x y : ℕ } → suc x ≤ y → x < y -sx≤y→x<y {zero} {suc y} (s≤s le) = s≤s z≤n -sx≤y→x<y {suc x} {suc y} (s≤s le) = s≤s ( sx≤y→x<y {x} {y} le ) +sx≤y→x<y = ? +-- {zero} {suc y} (s≤s le) = s≤s z≤n +-- sx≤y→x<y {suc x} {suc y} (s≤s le) = s≤s ( sx≤y→x<y {x} {y} le ) open import Data.Product i-j=0→i=j : {i j : ℕ } → j ≤ i → i - j ≡ 0 → i ≡ j -i-j=0→i=j {zero} {zero} _ refl = refl -i-j=0→i=j {zero} {suc j} () refl -i-j=0→i=j {suc i} {zero} z≤n () -i-j=0→i=j {suc i} {suc j} (s≤s lt) eq = cong suc (i-j=0→i=j {i} {j} lt eq) +i-j=0→i=j = ? +-- {zero} {zero} _ refl = refl +-- i-j=0→i=j {zero} {suc j} () refl +-- i-j=0→i=j {suc i} {zero} z≤n () +-- i-j=0→i=j {suc i} {suc j} (s≤s lt) eq = cong suc (i-j=0→i=j {i} {j} lt eq) m*n=0⇒m=0∨n=0 : {i j : ℕ} → i * j ≡ 0 → (i ≡ 0) ∨ ( j ≡ 0 ) -m*n=0⇒m=0∨n=0 {zero} {j} refl = case1 refl -m*n=0⇒m=0∨n=0 {suc i} {zero} eq = case2 refl +m*n=0⇒m=0∨n=0 = ? +-- {zero} {j} refl = case1 refl +-- m*n=0⇒m=0∨n=0 {suc i} {zero} eq = case2 refl minus+1 : {x y : ℕ } → y ≤ x → suc (minus x y) ≡ minus (suc x) y -minus+1 {zero} {zero} y≤x = refl -minus+1 {suc x} {zero} y≤x = refl -minus+1 {suc x} {suc y} (s≤s y≤x) = minus+1 {x} {y} y≤x +minus+1 = ? +-- {zero} {zero} y≤x = refl +-- minus+1 {suc x} {zero} y≤x = refl +-- minus+1 {suc x} {suc y} (s≤s y≤x) = minus+1 {x} {y} y≤x minus+yz : {x y z : ℕ } → z ≤ y → x + minus y z ≡ minus (x + y) z minus+yz {zero} {y} {z} _ = refl @@ -345,13 +353,15 @@ minus (suc x + y) z ∎ where open ≡-Reasoning minus<=0 : {x y : ℕ } → x ≤ y → minus x y ≡ 0 -minus<=0 {0} {zero} z≤n = refl -minus<=0 {0} {suc y} z≤n = refl -minus<=0 {suc x} {suc y} (s≤s le) = minus<=0 {x} {y} le +minus<=0 = ? +-- {0} {zero} z≤n = refl +-- minus<=0 {0} {suc y} z≤n = refl +-- minus<=0 {suc x} {suc y} (s≤s le) = minus<=0 {x} {y} le minus>0 : {x y : ℕ } → x < y → 0 < minus y x -minus>0 {zero} {suc _} (s≤s z≤n) = s≤s z≤n -minus>0 {suc x} {suc y} (s≤s lt) = minus>0 {x} {y} lt +minus>0 = ? +-- {zero} {suc _} (s≤s z≤n) = s≤s z≤n +-- minus>0 {suc x} {suc y} (s≤s lt) = minus>0 {x} {y} lt minus>0→x<y : {x y : ℕ } → 0 < minus y x → x < y minus>0→x<y {x} {y} lt with <-cmp x y @@ -374,8 +384,9 @@ minus+xy-zy {x} {y} {z} = subst₂ (λ j k → j - k ≡ x - z ) (+-comm y x) (+-comm y z) (minus+yx-yz {x} {y} {z}) +cancel<l : (x z : ℕ ) {y : ℕ} → y + x < y + z → x < z -+cancel<l x z {zero} lt = lt -+cancel<l x z {suc y} (s≤s lt) = +cancel<l x z {y} lt ++cancel<l x z = ? +-- {zero} lt = lt +-- +cancel<l x z {suc y} (s≤s lt) = +cancel<l x z {y} lt +cancel<r : (x z : ℕ ) {y : ℕ} → x + y < z + y → x < z +cancel<r x z {y} lt = +cancel<l x z (subst₂ (λ j k → j < k ) (+-comm x _) (+-comm z _) lt ) @@ -476,36 +487,7 @@ minus (minus k n * 0 ) 0 ∎ where open ≡-Reasoning -minus-* {suc m} {k} {n} lt with <-cmp k 1 -minus-* {suc m} {.0} {zero} lt | tri< (s≤s z≤n) ¬b ¬c = refl -minus-* {suc m} {.0} {suc n} lt | tri< (s≤s z≤n) ¬b ¬c = refl -minus-* {suc zero} {.1} {zero} lt | tri≈ ¬a refl ¬c = refl -minus-* {suc (suc m)} {.1} {zero} lt | tri≈ ¬a refl ¬c = minus-* {suc m} {1} {zero} lt -minus-* {suc m} {.1} {suc n} (s≤s ()) | tri≈ ¬a refl ¬c -minus-* {suc m} {k} {n} lt | tri> ¬a ¬b c = begin - minus k (suc n) * M - ≡⟨ distr-minus-* {k} {suc n} {M} ⟩ - minus (k * M ) ((suc n) * M) - ≡⟨⟩ - minus (k * M ) (M + n * M ) - ≡⟨ cong (λ x → minus (k * M) x) (+-comm M _ ) ⟩ - minus (k * M ) ((n * M) + M ) - ≡⟨ sym ( minus- {k * M} {n * M} (lemma lt) ) ⟩ - minus (minus (k * M ) (n * M)) M - ≡⟨ cong (λ x → minus x M ) ( sym ( distr-minus-* {k} {n} )) ⟩ - minus (minus k n * M ) M - ∎ where - M = suc m - lemma : {n k m : ℕ } → n < k → suc (k * suc m) > suc m + n * suc m - lemma {zero} {suc k} {m} (s≤s lt) = s≤s (s≤s (subst (λ x → x ≤ m + k * suc m) (+-comm 0 _ ) x≤x+y )) - lemma {suc n} {suc k} {m} lt = begin - suc (suc m + suc n * suc m) - ≡⟨⟩ - suc ( suc (suc n) * suc m) - ≤⟨ ≤-plus-0 {_} {_} {1} (*≤ lt ) ⟩ - suc (suc k * suc m) - ∎ where open ≤-Reasoning - open ≡-Reasoning +minus-* = ? x=y+z→x-z=y : {x y z : ℕ } → x ≡ y + z → x - z ≡ y x=y+z→x-z=y {x} {zero} {.x} refl = minus<=0 {x} {x} refl-≤ -- x ≡ suc (y + z) → (x ≡ y + z → x - z ≡ y) → (x - z) ≡ suc y @@ -564,7 +546,7 @@ ind : {p : P} → Q (pnext p) → Q p y<sx→y≤x : {x y : ℕ} → y < suc x → y ≤ x -y<sx→y≤x (s≤s lt) = lt +y<sx→y≤x = ? fi0 : (x : ℕ) → x ≤ zero → x ≡ zero fi0 .0 z≤n = refl @@ -580,7 +562,7 @@ f-induction0 : (p : P) → (x : ℕ) → (f (Finduction.pnext I p)) ≤ x → Q p f-induction0 p zero le = Finduction.ind I (Finduction.fzero I (fi0 _ le)) f-induction0 p (suc x) le with <-cmp (f (Finduction.pnext I p)) (suc x) - ... | tri< (s≤s a) ¬b ¬c = f-induction0 p x a + ... | tri< a ¬b ¬c = ? ... | tri≈ ¬a b ¬c = Finduction.ind I (f-induction0 (Finduction.pnext I p) x (y<sx→y≤x f1)) where f1 : f (Finduction.pnext I (Finduction.pnext I p)) < suc x f1 = subst (λ k → f (Finduction.pnext I (Finduction.pnext I p)) < k ) b ( Finduction.decline I {Finduction.pnext I p} @@ -596,7 +578,7 @@ ind : {p : P} → Q (pnext p) → Q p s≤s→≤ : { i j : ℕ} → suc i ≤ suc j → i ≤ j -s≤s→≤ (s≤s lt) = lt +s≤s→≤ = ? n-induction : {n m : Level} {P : Set n } → {Q : P → Set m } → (f : P → ℕ) @@ -606,7 +588,7 @@ f-induction0 : (p : P) → (x : ℕ) → (f (Ninduction.pnext I p)) ≤ x → Q p f-induction0 p zero lt = Ninduction.fzero I {p} (fi0 _ lt) f-induction0 p (suc x) le with <-cmp (f (Ninduction.pnext I p)) (suc x) - ... | tri< (s≤s a) ¬b ¬c = f-induction0 p x a + ... | tri< a ¬b ¬c = ? ... | tri≈ ¬a b ¬c = Ninduction.ind I (f-induction0 (Ninduction.pnext I p) x (s≤s→≤ nle) ) where f>0 : 0 < f (Ninduction.pnext I p) f>0 = subst (λ k → 0 < k ) (sym b) ( s≤s z≤n ) @@ -672,13 +654,7 @@ k ∎ ) } where open ≡-Reasoning div1 : { k : ℕ } → k > 1 → ¬ Dividable k 1 -div1 {k} k>1 record { factor = (suc f) ; is-factor = fa } = ⊥-elim ( nat-≡< (sym fa) ( begin - 2 ≤⟨ k>1 ⟩ - k ≡⟨ +-comm 0 _ ⟩ - k + 0 ≡⟨ refl ⟩ - 1 * k ≤⟨ *-mono-≤ {1} {suc f} (s≤s z≤n ) ≤-refl ⟩ - suc f * k ≡⟨ +-comm 0 _ ⟩ - suc f * k + 0 ∎ )) where open ≤-Reasoning +div1 {k} k>1 = ? div+div : { i j k : ℕ } → Dividable k i → Dividable k j → Dividable k (i + j) ∧ Dividable k (j + i) div+div {i} {j} {k} di dj = ⟪ div+div1 , subst (λ g → Dividable k g) (+-comm i j) div+div1 ⟫ where @@ -760,19 +736,20 @@ decl : {m : ℕ } → 0 < m → m - k < m decl {m} 0<m = y-x<y (<-trans a<sa k>1 ) 0<m ind : (p : ℕ ) → Dec (Dividable k (p - k) ) → Dec (Dividable k p ) - ind p (yes y) with <-cmp p k - ... | tri≈ ¬a refl ¬c = yes (subst (λ g → Dividable k g) (minus+n ≤-refl ) (proj1 ( div+div y div= ))) - ... | tri> ¬a ¬b k<p = yes (subst (λ g → Dividable k g) (minus+n (<-trans k<p a<sa)) (proj1 ( div+div y div= ))) - ... | tri< a ¬b ¬c with <-cmp p 0 - ... | tri≈ ¬a refl ¬c₁ = yes div0 - ... | tri> ¬a ¬b₁ c = no (λ d → not-div p (Dividable.factor d) a c (Dividable.is-factor d) ) where - not-div : (p f : ℕ) → p < k → 0 < p → f * k + 0 ≡ p → ⊥ - not-div (suc p) (suc f) p<k 0<p eq = nat-≡< (sym eq) ( begin -- ≤-trans p<k {!!}) -- suc p ≤ k - suc (suc p) ≤⟨ p<k ⟩ - k ≤⟨ x≤x+y ⟩ - k + (f * k + 0) ≡⟨ sym (+-assoc k _ _) ⟩ - suc f * k + 0 ∎ ) where open ≤-Reasoning - ind p (no n) = no (λ d → n (proj1 (div-div k>1 d div=)) ) + ind p (does₁ because proof₁) = ? + -- ind p (yes y) with <-cmp p k + -- ... | tri≈ ¬a refl ¬c = yes (subst (λ g → Dividable k g) (minus+n ≤-refl ) (proj1 ( div+div y div= ))) + -- ... | tri> ¬a ¬b k<p = yes (subst (λ g → Dividable k g) (minus+n (<-trans k<p a<sa)) (proj1 ( div+div y div= ))) + -- ... | tri< a ¬b ¬c with <-cmp p 0 + -- ... | tri≈ ¬a refl ¬c₁ = yes div0 + -- ... | tri> ¬a ¬b₁ c = no (λ d → not-div p (Dividable.factor d) a c (Dividable.is-factor d) ) where + -- not-div : (p f : ℕ) → p < k → 0 < p → f * k + 0 ≡ p → ⊥ + -- not-div (suc p) (suc f) p<k 0<p eq = nat-≡< (sym eq) ( begin -- ≤-trans p<k {!!}) -- suc p ≤ k + -- suc (suc p) ≤⟨ p<k ⟩ + -- k ≤⟨ x≤x+y ⟩ + -- k + (f * k + 0) ≡⟨ sym (+-assoc k _ _) ⟩ + -- suc f * k + 0 ∎ ) where open ≤-Reasoning + -- ind p (no n) = no (λ d → n (proj1 (div-div k>1 d div=)) ) I : Ninduction ℕ _ F I = record { pnext = λ p → p - k
--- a/src/sym2.agda Sat Sep 16 13:14:17 2023 +0900 +++ b/src/sym2.agda Sat Sep 16 17:24:50 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + open import Level hiding ( suc ; zero ) open import Algebra module sym2 where
--- a/src/sym2n.agda Sat Sep 16 13:14:17 2023 +0900 +++ b/src/sym2n.agda Sat Sep 16 17:24:50 2023 +0900 @@ -1,3 +1,4 @@ +{-# OPTIONS --cubical-compatible --safe #-} open import Level hiding ( suc ; zero ) open import Algebra module sym2n where
--- a/src/sym3.agda Sat Sep 16 13:14:17 2023 +0900 +++ b/src/sym3.agda Sat Sep 16 17:24:50 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + open import Level hiding ( suc ; zero ) open import Algebra module sym3 where
--- a/src/sym3n.agda Sat Sep 16 13:14:17 2023 +0900 +++ b/src/sym3n.agda Sat Sep 16 17:24:50 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + open import Level hiding ( suc ; zero ) open import Algebra module sym3n where
--- a/src/sym4.agda Sat Sep 16 13:14:17 2023 +0900 +++ b/src/sym4.agda Sat Sep 16 17:24:50 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + open import Level hiding ( suc ; zero ) open import Algebra module sym4 where
--- a/src/sym5.agda Sat Sep 16 13:14:17 2023 +0900 +++ b/src/sym5.agda Sat Sep 16 17:24:50 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + open import Level hiding ( suc ; zero ) open import Algebra module sym5 where
--- a/src/sym5a.agda Sat Sep 16 13:14:17 2023 +0900 +++ b/src/sym5a.agda Sat Sep 16 17:24:50 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + -- -- checking does not terminate, sorry --