Mercurial > hg > Gears > GearsAgda
changeset 949:057d3309ed9d
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 04 Aug 2024 13:05:12 +0900 |
| parents | e5288029f850 |
| children | 5c75fc6dfe59 |
| files | DPP.agda ModelChecking.agda RBTree.agda logic.agda nat.agda |
| diffstat | 5 files changed, 1427 insertions(+), 177 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/DPP.agda Sun Aug 04 13:05:12 2024 +0900 @@ -0,0 +1,206 @@ +{-# OPTIONS --cubical-compatible #-} +-- {-# OPTIONS --cubical-compatible --safe #-} +module DPP where + +open import Level renaming (zero to Z ; suc to succ) + +open import Data.Nat hiding (compare) +open import Data.Nat.Properties as NatProp +open import Data.Maybe +-- open import Data.Maybe.Properties +open import Data.Empty +open import Data.List +-- open import Data.Tree.Binary +-- open import Data.Product +open import Function as F hiding (const) +open import Relation.Binary +open import Relation.Binary.PropositionalEquality +open import Relation.Nullary +open import logic +open import Data.Unit hiding ( _≟_ ) -- ; _≤?_ ; _≤_) +open import Relation.Binary.Definitions + +open import ModelChecking + + +-- +-- single process implemenation +-- + + +record Phil : Set where + field + ptr : ℕ + left right : AtomicNat + +init-Phil : Phil +init-Phil = record { ptr = 0 ; left = init-AtomicNat ; right = init-AtomicNat } + +pickup_rfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t +pickup_lfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t +eating : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t +putdown_rfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t +putdown_lfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t +thinking : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t + +pickup_rfork p next = f_set (Phil.right p) (Phil.ptr p) ( λ f → pickup_lfork record p { right = f } next ) +pickup_lfork p next = f_set (Phil.left p) (Phil.ptr p) ( λ f → eating record p { left = f } next ) +eating p next = putdown_rfork p next +putdown_rfork p next = f_set (Phil.right p) 0 ( λ f → putdown_lfork record p { right = f } next ) +putdown_lfork p next = f_set (Phil.left p) 0 ( λ f → thinking record p { left = f } next ) +thinking p next = next p + +run : Phil +run = pickup_rfork record { ptr = 1 ; left = record { ptr = 2 ; value = 0 } ; right = record { ptr = 3 ; value = 0 } } $ λ p → p + +-- +-- Coda Gear +-- + +data Code : Set where + C_nop : Code + C_cas_int : Code + C_putdown_rfork : Code + C_putdown_lfork : Code + C_thinking : Code + C_pickup_rfork : Code + C_pickup_lfork : Code + C_eating : Code + +-- +-- all possible arguments in -APIs +-- + +record Phil-API : Set where + field + next : Code + impl : Phil + +-- +-- Data Gear +-- +-- waiting / pointer / available +-- +data Data : Set where + -- D_AtomicNat : AtomicNat → ℕ → Data + D_AtomicNat : AtomicNat → Data + D_Phil : Phil → Data + D_Error : Error → Data + +-- data API : Set where +-- A_AtomicNat : AtomicNat-API → API +-- A_Phil : Phil-API → API + +-- open import hoareBinaryTree + +data bt {n : Level} (A : Set n) : Set n where + leaf : bt A + node : (key : ℕ) → (value : A) → + (left : bt A ) → (right : bt A ) → bt A + +updateTree : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (empty : bt A → t ) → (next : A → bt A → t ) → t +updateTree = ? + +insertTree : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (next : bt A → t ) → t +insertTree = ? + + +-- +-- second level stub +-- + +-- putdown_rfork : Phil → (? → t) → t +-- putdown_rfork p next = goto p->lfork->cas( 0 , putdown_lfork, putdown_lfork ) , next + +Phil_putdown_rfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t +Phil_putdown_rfork_sub c next = next C_cas_int record c { + c_AtomicNat-API = record { impl = Phil.right phil ; value = 0 ; fail = C_putdown_lfork ; next = C_putdown_lfork } } where + phil : Phil + phil = Phil-API.impl ( Context.c_Phil-API c ) + +Phil_putdown_lfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t +Phil_putdown_lfork_sub c next = next C_cas_int record c { + c_AtomicNat-API = record { impl = Phil.left phil ; value = 0 ; fail = C_thinking ; next = C_thinking } } where + phil : Phil + phil = Phil-API.impl ( Context.c_Phil-API c ) + +Phil_thiking : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t +Phil_thiking c next = next C_pickup_rfork c + +Phil_pickup_lfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t +Phil_pickup_lfork_sub c next = next C_cas_int record c { + c_AtomicNat-API = record { impl = Phil.left phil ; value = Phil.ptr phil ; fail = C_pickup_lfork ; next = C_pickup_rfork } } where + phil : Phil + phil = Phil-API.impl ( Context.c_Phil-API c ) + +Phil_pickup_rfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t +Phil_pickup_rfork_sub c next = next C_cas_int record c { + c_AtomicNat-API = record { impl = Phil.left phil ; value = Phil.ptr phil ; fail = C_pickup_rfork ; next = C_eating } } where + phil : Phil + phil = Phil-API.impl ( Context.c_Phil-API c ) + +Phil_eating_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t +Phil_eating_sub c next = next C_putdown_rfork c + +code_table : {n : Level} {t : Set n} → Code → Context → ( Code → Context → t) → t +code_table C_nop = λ c next → next C_nop c +code_table C_cas_int = AtomicInt_cas_stub +code_table C_putdown_rfork = Phil_putdown_rfork_sub +code_table C_putdown_lfork = Phil_putdown_lfork_sub +code_table C_thinking = Phil_thiking +code_table C_pickup_rfork = Phil_pickup_lfork_sub +code_table C_pickup_lfork = Phil_pickup_rfork_sub +code_table C_eating = Phil_eating_sub + + +init-Phil-0 : (ps : List Context) → (left right : AtomicNat ) → List Context +init-Phil-0 ps left right = new-data (c1 ps) ( λ ptr → D_Phil (p ptr) ) $ λ c ptr → record c { c_Phil-API = record { next = C_thinking ; impl = p ptr }} ∷ ps where + p : ℕ → Phil + p ptr = record init-Phil { ptr = ptr ; left = left ; right = right } + c1 : List Context → Context + c1 [] = init-context + c1 (c2 ∷ ct) = c2 + +init-AtomicNat1 : {n : Level} {t : Set n} → Context → ( Context → AtomicNat → t ) → t +init-AtomicNat1 c1 next = new-data c1 ( λ ptr → D_AtomicNat (a ptr) ) $ λ c2 ptr → next c2 (a ptr) where + a : ℕ → AtomicNat + a ptr = record { ptr = ptr ; value = 0 } + +init-Phil-1 : (c1 : Context) → Context +init-Phil-1 c1 = record c1 { memory = mem2 $ mem1 $ mem ; mbase = n + 3 } where + n : ℕ + n = Context.mbase c1 + left = record { ptr = suc n ; value = 0} + right = record { ptr = suc (suc n) ; value = 0} + mem : bt Data + mem = insertTree ( Context.memory c1) (suc n) (D_AtomicNat left) + $ λ t → t + mem1 : bt Data → bt Data + mem1 t = insertTree t (suc (suc n)) (D_AtomicNat right ) + $ λ t → t + mem2 : bt Data → bt Data + mem2 t = insertTree t (n + 3) (D_Phil record { ptr = n + 3 ; left = left ; right = right }) + $ λ t → t + +test-i0 : bt Data +test-i0 = Context.memory (init-Phil-1 init-context) + +make-phil : ℕ → Context +make-phil zero = init-context +make-phil (suc n) = init-Phil-1 ( make-phil n ) + +test-i5 : bt Data +test-i5 = Context.memory (make-phil 5) + +-- loop exexution + +-- concurrnt execution + +-- state db ( binary tree of processes ) + +-- depth first execution + +-- verify temporal logic poroerries + + +
--- a/ModelChecking.agda Sat Jul 20 17:01:50 2024 +0900 +++ b/ModelChecking.agda Sun Aug 04 13:05:12 2024 +0900 @@ -1,3 +1,5 @@ +-- {-# OPTIONS --cubical-compatible --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} module ModelChecking where open import Level renaming (zero to Z ; suc to succ) @@ -33,44 +35,12 @@ f_set : {n : Level } {t : Set n} → AtomicNat → (value : ℕ) → ( AtomicNat → t ) → t f_set a v next = next record a { value = v } -record Phil : Set where - field - ptr : ℕ - left right : AtomicNat - -init-Phil : Phil -init-Phil = record { ptr = 0 ; left = init-AtomicNat ; right = init-AtomicNat } - -pickup_rfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t -pickup_lfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t -eating : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t -putdown_rfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t -putdown_lfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t -thinking : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t - -pickup_rfork p next = f_set (Phil.right p) (Phil.ptr p) ( λ f → pickup_lfork record p { right = f } next ) -pickup_lfork p next = f_set (Phil.left p) (Phil.ptr p) ( λ f → eating record p { left = f } next ) -eating p next = putdown_rfork p next -putdown_rfork p next = f_set (Phil.right p) 0 ( λ f → putdown_lfork record p { right = f } next ) -putdown_lfork p next = f_set (Phil.left p) 0 ( λ f → thinking record p { left = f } next ) -thinking p next = next p - -run : Phil -run = pickup_rfork record { ptr = 1 ; left = record { ptr = 2 ; value = 0 } ; right = record { ptr = 3 ; value = 0 } } $ λ p → p - -- -- Coda Gear -- data Code : Set where - C_nop : Code - C_cas_int : Code - C_putdown_rfork : Code - C_putdown_lfork : Code - C_thinking : Code - C_pickup_rfork : Code - C_pickup_lfork : Code - C_eating : Code + CC_nop : Code -- -- all possible arguments in -APIs @@ -82,11 +52,6 @@ value : ℕ impl : AtomicNat -record Phil-API : Set where - field - next : Code - impl : Phil - data Error : Set where E_panic : Error E_cas_fail : Error @@ -96,17 +61,15 @@ -- -- waiting / pointer / available -- + data Data : Set where -- D_AtomicNat : AtomicNat → ℕ → Data - D_AtomicNat : AtomicNat → Data - D_Phil : Phil → Data - D_Error : Error → Data + CD_AtomicNat : AtomicNat → Data -- data API : Set where -- A_AtomicNat : AtomicNat-API → API -- A_Phil : Phil-API → API -open import hoareBinaryTree record Context : Set where field @@ -116,11 +79,11 @@ -- -API list (frame in Gears Agda ) --- a Data of API -- api : List API -- c_Phil-API : Maybe Phil-API - c_Phil-API : Phil-API - c_AtomicNat-API : AtomicNat-API + -- c_Phil-API : ? + -- c_AtomicNat-API : AtomicNat-API mbase : ℕ - memory : bt Data + -- memory : ? error : Data fail_next : Code @@ -128,80 +91,29 @@ -- second level stub -- AtomicInt_cas_stub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t -AtomicInt_cas_stub {_} {t} c next = updateTree (Context.memory c) (AtomicNat.ptr ai) ( D_AtomicNat (record ai { value = AtomicNat-API.value api } )) - ( λ bt → next ( Context.fail c ) c ) -- segmentation fault ( null pointer ) - $ λ prev bt → f_cas prev bt where - api : AtomicNat-API - api = Context.c_AtomicNat-API c - ai : AtomicNat - ai = AtomicNat-API.impl api - f_cas : Data → bt Data → t - f_cas (D_AtomicNat prev) bt with <-cmp ( AtomicNat.value ai ) ( AtomicNat.value prev ) - ... | tri≈ ¬a b ¬c = next (AtomicNat-API.next api) ( record c { memory = bt ; c_AtomicNat-API = record api { impl = prev } } ) -- update memory - ... | tri< a₁ ¬b ¬c = next (AtomicNat-API.fail api) c --- cleaer API - ... | tri> ¬a ¬b _ = next (AtomicNat-API.fail api) c - f_cas a bt = next ( Context.fail c ) c -- type error / panic - --- putdown_rfork : Phil → (? → t) → t --- putdown_rfork p next = goto p->lfork->cas( 0 , putdown_lfork, putdown_lfork ) , next - -Phil_putdown_rfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t -Phil_putdown_rfork_sub c next = next C_cas_int record c { - c_AtomicNat-API = record { impl = Phil.right phil ; value = 0 ; fail = C_putdown_lfork ; next = C_putdown_lfork } } where - phil : Phil - phil = Phil-API.impl ( Context.c_Phil-API c ) +AtomicInt_cas_stub {_} {t} c next = ? -Phil_putdown_lfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t -Phil_putdown_lfork_sub c next = next C_cas_int record c { - c_AtomicNat-API = record { impl = Phil.left phil ; value = 0 ; fail = C_thinking ; next = C_thinking } } where - phil : Phil - phil = Phil-API.impl ( Context.c_Phil-API c ) - -Phil_thiking : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t -Phil_thiking c next = next C_pickup_rfork c - -Phil_pickup_lfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t -Phil_pickup_lfork_sub c next = next C_cas_int record c { - c_AtomicNat-API = record { impl = Phil.left phil ; value = Phil.ptr phil ; fail = C_pickup_lfork ; next = C_pickup_rfork } } where - phil : Phil - phil = Phil-API.impl ( Context.c_Phil-API c ) - -Phil_pickup_rfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t -Phil_pickup_rfork_sub c next = next C_cas_int record c { - c_AtomicNat-API = record { impl = Phil.left phil ; value = Phil.ptr phil ; fail = C_pickup_rfork ; next = C_eating } } where - phil : Phil - phil = Phil-API.impl ( Context.c_Phil-API c ) - -Phil_eating_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t -Phil_eating_sub c next = next C_putdown_rfork c code_table : {n : Level} {t : Set n} → Code → Context → ( Code → Context → t) → t -code_table C_nop = λ c next → next C_nop c -code_table C_cas_int = AtomicInt_cas_stub -code_table C_putdown_rfork = Phil_putdown_rfork_sub -code_table C_putdown_lfork = Phil_putdown_lfork_sub -code_table C_thinking = Phil_thiking -code_table C_pickup_rfork = Phil_pickup_lfork_sub -code_table C_pickup_lfork = Phil_pickup_rfork_sub -code_table C_eating = Phil_eating_sub +code_table = ? step : {n : Level} {t : Set n} → List Context → (List Context → t) → t step {n} {t} [] next0 = next0 [] step {n} {t} (p ∷ ps) next0 = code_table (Context.next p) p ( λ code np → next0 (update-context ps np ++ ( record np { next = code } ∷ [] ))) where update-context : List Context → Context → List Context update-context [] _ = [] - update-context (c1 ∷ t) np = record c1 { memory = Context.memory np ; mbase = Context.mbase np } ∷ t + update-context (c1 ∷ t) np = ? -- record c1 { memory = Context.memory np ; mbase = Context.mbase np } ∷ t init-context : Context init-context = record { - next = C_nop - ; fail = C_nop - ; c_Phil-API = record { next = C_nop ; impl = init-Phil } - ; c_AtomicNat-API = record { next = C_nop ; fail = C_nop ; value = 0 ; impl = init-AtomicNat } + next = CC_nop + ; fail = CC_nop + -- ; c_Phil-API = ? + -- ; c_AtomicNat-API = record { next = CC_nop ; fail = CC_nop ; value = 0 ; impl = init-AtomicNat } ; mbase = 0 - ; memory = leaf - ; error = D_Error E_panic - ; fail_next = C_nop + -- ; memory = ? + ; error = ? + ; fail_next = CC_nop } alloc-data : {n : Level} {t : Set n} → ( c : Context ) → ( Context → ℕ → t ) → t @@ -209,51 +121,61 @@ mnext = suc ( Context.mbase c ) new-data : {n : Level} {t : Set n} → ( c : Context ) → (ℕ → Data ) → ( Context → ℕ → t ) → t -new-data c x next = alloc-data c $ λ c1 n → insertTree (Context.memory c1) n (x n) ( λ bt → next record c1 { memory = bt } n ) +new-data c x next = alloc-data c $ λ c1 n → ? -- insertTree (Context.memory c1) n (x n) ( λ bt → next record c1 { memory = bt } n ) init-AtomicNat0 : {n : Level} {t : Set n} → Context → ( Context → ℕ → t ) → t -init-AtomicNat0 c1 next = new-data c1 ( λ ptr → D_AtomicNat (a ptr) ) $ λ c2 ptr → next c2 ptr where - a : ℕ → AtomicNat - a ptr = record { ptr = ptr ; value = 0 } +init-AtomicNat0 c1 next = ? + +add< : { i : ℕ } (j : ℕ ) → i < suc i + j +add< {i} j = begin + suc i ≤⟨ m≤m+n (suc i) j ⟩ + suc i + j ∎ where open ≤-Reasoning + +nat-<> : { x y : ℕ } → x < y → y < x → ⊥ +nat-<> {x} {y} x<y y<x with <-cmp x y +... | tri< a ¬b ¬c = ⊥-elim ( ¬c y<x ) +... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c y<x ) +... | tri> ¬a ¬b c = ⊥-elim ( ¬a x<y ) -init-Phil-0 : (ps : List Context) → (left right : AtomicNat ) → List Context -init-Phil-0 ps left right = new-data (c1 ps) ( λ ptr → D_Phil (p ptr) ) $ λ c ptr → record c { c_Phil-API = record { next = C_thinking ; impl = p ptr }} ∷ ps where - p : ℕ → Phil - p ptr = record init-Phil { ptr = ptr ; left = left ; right = right } - c1 : List Context → Context - c1 [] = init-context - c1 (c2 ∷ ct) = c2 +nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥ +nat-≤> {x} {y} x≤y y<x with <-cmp x y +... | tri< a ¬b ¬c = ⊥-elim ( ¬c y<x ) +... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c y<x ) +... | tri> ¬a ¬b c = ? -init-AtomicNat1 : {n : Level} {t : Set n} → Context → ( Context → AtomicNat → t ) → t -init-AtomicNat1 c1 next = new-data c1 ( λ ptr → D_AtomicNat (a ptr) ) $ λ c2 ptr → next c2 (a ptr) where - a : ℕ → AtomicNat - a ptr = record { ptr = ptr ; value = 0 } + +nat-<≡ : { x : ℕ } → x < x → ⊥ +nat-<≡ {x} x<x with <-cmp x x +... | tri< a ¬b ¬c = ⊥-elim ( ¬c x<x ) +... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c x<x ) +... | tri> ¬a ¬b c = ⊥-elim ( ¬a x<x ) -init-Phil-1 : (c1 : Context) → Context -init-Phil-1 c1 = record c1 { memory = mem2 $ mem1 $ mem ; mbase = n + 3 } where - n : ℕ - n = Context.mbase c1 - left = record { ptr = suc n ; value = 0} - right = record { ptr = suc (suc n) ; value = 0} - mem : bt Data - mem = insertTree ( Context.memory c1) (suc n) (D_AtomicNat left) - $ λ t → t - mem1 : bt Data → bt Data - mem1 t = insertTree t (suc (suc n)) (D_AtomicNat right ) - $ λ t → t - mem2 : bt Data → bt Data - mem2 t = insertTree t (n + 3) (D_Phil record { ptr = n + 3 ; left = left ; right = right }) - $ λ t → t - -test-i0 : bt Data -test-i0 = Context.memory (init-Phil-1 init-context) +nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥ +nat-≡< refl lt = nat-<≡ lt + +lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥ +lemma3 refl () +lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥ +lemma5 {i} {j} i<1 j<i with <-cmp j i +... | tri< a ¬b ¬c = ⊥-elim ( ¬c ? ) +... | tri≈ ¬a b ¬c = ⊥-elim (¬a j<i ) +... | tri> ¬a ¬b c = ⊥-elim ( ¬a j<i ) -make-phil : ℕ → Context -make-phil zero = init-context -make-phil (suc n) = init-Phil-1 ( make-phil n ) +¬x<x : {x : ℕ} → ¬ (x < x) +¬x<x x<x = ? -test-i5 : bt Data -test-i5 = Context.memory (make-phil 5) +TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ) + → (r : Index) → (p : Invraiant r) + → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t +TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r) +... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) +... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (m≤n⇒m≤1+n lt1) p1 lt1 ) where + TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t + TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) + TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j) + ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt + ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 ) + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) -- loop exexution
--- a/RBTree.agda Sat Jul 20 17:01:50 2024 +0900 +++ b/RBTree.agda Sun Aug 04 13:05:12 2024 +0900 @@ -1,5 +1,6 @@ -{-# OPTIONS --allow-unsolved-metas #-} --- {-# OPTIONS --cubical-compatible --allow-unsolved-metas #-} +{-# OPTIONS cubical-compatible --allow-unsolved-metas #-} +-- {-# OPTIONS --cubical-compatible --safe #-} +-- {-# OPTIONS --cubical-compatible #-} module RBTree where open import Level hiding (suc ; zero ; _⊔_ )
--- a/logic.agda Sat Jul 20 17:01:50 2024 +0900 +++ b/logic.agda Sun Aug 04 13:05:12 2024 +0900 @@ -1,14 +1,11 @@ -{-# OPTIONS --safe --cubical-compatible #-} +{-# OPTIONS --cubical-compatible --safe #-} + module logic where -open import Level - +open import Level open import Relation.Nullary -open import Relation.Binary hiding (_⇔_) -open import Relation.Binary.PropositionalEquality - +open import Relation.Binary hiding (_⇔_ ) open import Data.Empty -open import Data.Nat hiding (_⊔_) data Bool : Set where @@ -49,45 +46,139 @@ dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b ) dont-orb {A} {B} (case1 a) ¬B = a - infixr 130 _∧_ infixr 140 _∨_ infixr 150 _⇔_ -_/\_ : Bool → Bool → Bool +_/\_ : Bool → Bool → Bool true /\ true = true _ /\ _ = false -_<B?_ : ℕ → ℕ → Bool -ℕ.zero <B? x = true -ℕ.suc x <B? ℕ.zero = false -ℕ.suc x <B? ℕ.suc xx = x <B? xx - --- _<BT_ : ℕ → ℕ → Set --- ℕ.zero <BT ℕ.zero = ⊤ --- ℕ.zero <BT ℕ.suc b = ⊤ --- ℕ.suc a <BT ℕ.zero = ⊥ --- ℕ.suc a <BT ℕ.suc b = a <BT b - - -_≟B_ : Decidable {A = Bool} _≡_ -true ≟B true = yes refl -false ≟B false = yes refl -true ≟B false = no λ() -false ≟B true = no λ() - -_\/_ : Bool → Bool → Bool +_\/_ : Bool → Bool → Bool false \/ false = false _ \/ _ = true -not_ : Bool → Bool +not : Bool → Bool not true = false -not false = true +not false = true -_<=>_ : Bool → Bool → Bool +_<=>_ : Bool → Bool → Bool true <=> true = true false <=> false = true _ <=> _ = false infixr 130 _\/_ infixr 140 _/\_ + +open import Relation.Binary.PropositionalEquality + +record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where + field + fun← : S → R + fun→ : R → S + fiso← : (x : R) → fun← ( fun→ x ) ≡ x + fiso→ : (x : S ) → fun→ ( fun← x ) ≡ x + +injection : {n m : Level} (R : Set n) (S : Set m) (f : R → S ) → Set (n Level.⊔ m) +injection R S f = (x y : R) → f x ≡ f y → x ≡ y + + +-- Cubical Agda has trouble with std-lib's Dec +-- we sometimes use simpler version of Dec + +data Dec0 {n : Level} (A : Set n) : Set n where + yes0 : A → Dec0 A + no0 : (A → ⊥) → Dec0 A + +open _∧_ +∧-injective : {n m : Level} {A : Set n} {B : Set m} → {a b : A ∧ B} → proj1 a ≡ proj1 b → proj2 a ≡ proj2 b → a ≡ b +∧-injective refl refl = refl + +not-not-bool : { b : Bool } → not (not b) ≡ b +not-not-bool {true} = refl +not-not-bool {false} = refl + +¬t=f : (t : Bool ) → ¬ ( not t ≡ t) +¬t=f true () +¬t=f false () + +≡-Bool-func : {A B : Bool } → ( A ≡ true → B ≡ true ) → ( B ≡ true → A ≡ true ) → A ≡ B +≡-Bool-func {true} {true} a→b b→a = refl +≡-Bool-func {false} {true} a→b b→a with b→a refl +... | () +≡-Bool-func {true} {false} a→b b→a with a→b refl +... | () +≡-Bool-func {false} {false} a→b b→a = refl + +bool-≡-? : (a b : Bool) → Dec0 ( a ≡ b ) +bool-≡-? true true = yes0 refl +bool-≡-? true false = no0 (λ ()) +bool-≡-? false true = no0 (λ ()) +bool-≡-? false false = yes0 refl + +¬-bool-t : {a : Bool} → ¬ ( a ≡ true ) → a ≡ false +¬-bool-t {true} ne = ⊥-elim ( ne refl ) +¬-bool-t {false} ne = refl + +¬-bool-f : {a : Bool} → ¬ ( a ≡ false ) → a ≡ true +¬-bool-f {true} ne = refl +¬-bool-f {false} ne = ⊥-elim ( ne refl ) + +¬-bool : {a : Bool} → a ≡ false → a ≡ true → ⊥ +¬-bool refl () + +lemma-∧-0 : {a b : Bool} → a /\ b ≡ true → a ≡ false → ⊥ +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} {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} eq = refl +bool-∧→tt-0 {false} {_} () + +bool-∧→tt-1 : {a b : Bool} → ( a /\ b ) ≡ true → b ≡ true +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} 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} 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} 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} eq = refl + +bool-and-1 : {a b : Bool} → a ≡ false → (a /\ b ) ≡ false +bool-and-1 {false} {b} eq = refl +bool-and-2 : {a b : Bool} → b ≡ false → (a /\ b ) ≡ false +bool-and-2 {true} {false} eq = refl +bool-and-2 {false} {false} eq = refl +bool-and-2 {true} {true} () +bool-and-2 {false} {true} () + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/nat.agda Sun Aug 04 13:05:12 2024 +0900 @@ -0,0 +1,1030 @@ +{-# OPTIONS --cubical-compatible --safe #-} + +module nat where + +open import Data.Nat +open import Data.Nat.Properties +open import Data.Empty +open import Relation.Nullary +open import Relation.Binary.PropositionalEquality +open import Relation.Binary.Core +open import Relation.Binary.Definitions +open import logic +open import Level hiding ( zero ; suc ) + +=→¬< : {x : ℕ } → ¬ ( x < x ) +=→¬< {x} x<x with <-cmp x x +... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) +... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a x<x ) +... | tri> ¬a ¬b c = ⊥-elim ( ¬b refl ) + +>→¬< : {x y : ℕ } → (x < y ) → ¬ ( y < x ) +>→¬< {x} {y} x<y y<x with <-cmp x y +... | tri< a ¬b ¬c = ⊥-elim ( ¬c y<x ) +... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c y<x ) +... | tri> ¬a ¬b c = ⊥-elim ( ¬a x<y ) + +nat-<> : { x y : ℕ } → x < y → y < x → ⊥ +nat-<> {x} {y} x<y y<x with <-cmp x y +... | tri< a ¬b ¬c = ⊥-elim ( ¬c y<x ) +... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c y<x ) +... | tri> ¬a ¬b c = ⊥-elim ( ¬a x<y ) + +a<sa : {la : ℕ} → la < suc la +a<sa {zero} = s≤s z≤n +a<sa {suc la} = s≤s a<sa + +refl-≤s : {x : ℕ } → x ≤ suc x +refl-≤s {zero} = z≤n +refl-≤s {suc x} = s≤s (refl-≤s {x}) + +a≤sa : {x : ℕ } → x ≤ suc x +a≤sa = refl-≤s + +nat-<≡ : { x : ℕ } → x < x → ⊥ +nat-<≡ {x} x<x with <-cmp x x +... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) +... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a x<x ) +... | tri> ¬a ¬b c = ⊥-elim ( ¬a x<x ) + +nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥ +nat-≡< refl lt = nat-<≡ lt + +nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥ +nat-≤> {x} {y} x≤y y<x with <-cmp x y +... | tri< a ¬b ¬c = ⊥-elim ( ¬c y<x ) +... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c y<x ) +... | tri> ¬a ¬b c = ⊥-elim (nat-<≡ (≤-trans c x≤y)) + +≤-∨ : { x y : ℕ } → x ≤ y → ( (x ≡ y ) ∨ (x < y) ) +≤-∨ {x} {y} x≤y with <-cmp x y +... | tri< a ¬b ¬c = case2 a +... | tri≈ ¬a b ¬c = case1 b +... | tri> ¬a ¬b c = ⊥-elim ( nat-<≡ (≤-trans c x≤y)) + +<-∨ : { x y : ℕ } → x < suc y → ( (x ≡ y ) ∨ (x < y) ) +<-∨ {x} {y} x<sy with <-cmp x y +... | tri< a ¬b ¬c = case2 a +... | tri≈ ¬a b ¬c = case1 b +... | tri> ¬a ¬b c = ⊥-elim ( nat-<≡ (≤-trans x<sy c )) + +¬a≤a : {la : ℕ} → suc la ≤ la → ⊥ +¬a≤a {x} sx≤x = ⊥-elim ( nat-≤> sx≤x a<sa ) + +max : (x y : ℕ) → ℕ +max zero zero = zero +max zero (suc x) = (suc x) +max (suc x) zero = (suc x) +max (suc x) (suc y) = suc ( max x y ) + +x≤max : (x y : ℕ) → x ≤ max x y +x≤max zero zero = ≤-refl +x≤max zero (suc x) = z≤n +x≤max (suc x) zero = ≤-refl +x≤max (suc x) (suc y) = s≤s( x≤max x y ) + +y≤max : (x y : ℕ) → y ≤ max x y +y≤max zero zero = ≤-refl +y≤max zero (suc x) = ≤-refl +y≤max (suc x) zero = z≤n +y≤max (suc x) (suc y) = s≤s( y≤max x y ) + +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) lt with <-cmp x y +... | tri< a ¬b ¬c = cong suc (x≤y→max=y x y (≤-trans a≤sa a)) +... | tri≈ ¬a refl ¬c = cong suc (x≤y→max=y x y ≤-refl ) +... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c lt ) + +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) lt with <-cmp y x +... | tri< a ¬b ¬c = cong suc (y≤x→max=x x y (≤-trans a≤sa a)) +... | tri≈ ¬a refl ¬c = cong suc (y≤x→max=x x y ≤-refl ) +... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c lt ) + + +-- _*_ : ℕ → ℕ → ℕ +-- _*_ zero _ = zero +-- _*_ (suc n) m = m + ( n * m ) + +-- x ^ y +exp : ℕ → ℕ → ℕ +exp _ zero = 1 +exp n (suc m) = n * ( exp n m ) + +div2 : ℕ → (ℕ ∧ Bool ) +div2 zero = ⟪ 0 , false ⟫ +div2 (suc zero) = ⟪ 0 , true ⟫ +div2 (suc (suc n)) = ⟪ suc (proj1 (div2 n)) , proj2 (div2 n) ⟫ where + open _∧_ + +div2-rev : (ℕ ∧ Bool ) → ℕ +div2-rev ⟪ x , true ⟫ = suc (x + x) +div2-rev ⟪ x , false ⟫ = x + x + +div2-eq : (x : ℕ ) → div2-rev ( div2 x ) ≡ x +div2-eq zero = refl +div2-eq (suc zero) = refl +div2-eq (suc (suc x)) with div2 x in eq1 +... | ⟪ x1 , true ⟫ = begin -- eq1 : div2 x ≡ ⟪ x1 , true ⟫ + div2-rev ⟪ suc x1 , true ⟫ ≡⟨⟩ + suc (suc (x1 + suc x1)) ≡⟨ cong (λ k → suc (suc k )) (+-comm x1 _ ) ⟩ + suc (suc (suc (x1 + x1))) ≡⟨⟩ + suc (suc (div2-rev ⟪ x1 , true ⟫)) ≡⟨ cong (λ k → suc (suc (div2-rev k ))) (sym eq1) ⟩ + suc (suc (div2-rev (div2 x))) ≡⟨ cong (λ k → suc (suc k)) (div2-eq x) ⟩ + suc (suc x) ∎ where open ≡-Reasoning +... | ⟪ x1 , false ⟫ = begin + div2-rev ⟪ suc x1 , false ⟫ ≡⟨⟩ + suc (x1 + suc x1) ≡⟨ cong (λ k → (suc k )) (+-comm x1 _ ) ⟩ + suc (suc (x1 + x1)) ≡⟨⟩ + suc (suc (div2-rev ⟪ x1 , false ⟫)) ≡⟨ cong (λ k → suc (suc (div2-rev k ))) (sym eq1) ⟩ + suc (suc (div2-rev (div2 x))) ≡⟨ cong (λ k → suc (suc k)) (div2-eq x) ⟩ + suc (suc x) ∎ where open ≡-Reasoning + +sucprd : {i : ℕ } → 0 < i → suc (pred i) ≡ i +sucprd {suc i} 0<i = refl + +0<s : {x : ℕ } → zero < suc x +0<s {_} = s≤s z≤n + +px<py : {x y : ℕ } → pred x < pred y → x < y +px<py {zero} {suc y} lt = 0<s +px<py {suc x} {suc y} lt with <-cmp x y +... | tri< a ¬b ¬c = s≤s a +... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< b lt ) +... | tri> ¬a ¬b c = ⊥-elim ( nat-<> c lt ) + +minus : (a b : ℕ ) → ℕ +minus a zero = a +minus zero (suc b) = zero +minus (suc a) (suc b) = minus a b + +_-_ = minus + +sn-m=sn-m : {m n : ℕ } → m ≤ n → suc n - m ≡ suc ( n - m ) +sn-m=sn-m {0} {n} m≤n = refl +sn-m=sn-m {suc m} {suc n} le with <-cmp m n +... | tri< a ¬b ¬c = sm00 where + sm00 : suc n - m ≡ suc ( n - m ) + sm00 = sn-m=sn-m {m} {n} (≤-trans a≤sa a ) +... | tri≈ ¬a refl ¬c = sn-m=sn-m {m} {n} ≤-refl +... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c le ) + +si-sn=i-n : {i n : ℕ } → n < i → suc (i - suc n) ≡ (i - n) +si-sn=i-n {i} {n} n<i = begin + suc (i - suc n) ≡⟨ sym (sn-m=sn-m n<i ) ⟩ + suc i - suc n ≡⟨⟩ + i - n + ∎ where + open ≡-Reasoning + +n-m<n : (n m : ℕ ) → n - m ≤ n +n-m<n zero zero = z≤n +n-m<n (suc n) zero = s≤s (n-m<n n zero) +n-m<n zero (suc m) = z≤n +n-m<n (suc n) (suc m) = ≤-trans (n-m<n n m ) refl-≤s + +m-0=m : {m : ℕ } → m - zero ≡ m +m-0=m {zero} = refl +m-0=m {suc m} = cong suc (m-0=m {m}) + +m-m=0 : {m : ℕ } → m - m ≡ zero +m-m=0 {zero} = refl +m-m=0 {suc m} = m-m=0 {m} + +refl-≤ : {x : ℕ } → x ≤ x +refl-≤ {zero} = z≤n +refl-≤ {suc x} = s≤s (refl-≤ {x}) + +refl-≤≡ : {x y : ℕ } → x ≡ y → x ≤ y +refl-≤≡ refl = refl-≤ + +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} x≤y = refl-≤ +px≤py {suc x} {zero} () +px≤py {zero} {suc y} le = z≤n +px≤py {suc x} {suc y} x≤y with <-cmp x y +... | tri< a ¬b ¬c = ≤-trans a≤sa a +... | tri≈ ¬a b ¬c = refl-≤≡ b +... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c x≤y ) + +n-n-m=m : {m n : ℕ } → m ≤ n → m ≡ (n - (n - m)) +n-n-m=m {0} {zero} le = refl +n-n-m=m {0} {suc n} lt = begin + 0 ≡⟨ sym (m-m=0 {suc n}) ⟩ + suc n - suc n + ∎ where open ≡-Reasoning +n-n-m=m {suc m} {suc n} le = begin + suc m ≡⟨ cong suc ( n-n-m=m (px≤py le)) ⟩ + suc (n - (n - m)) ≡⟨ sym (sn-m=sn-m (n-m<n n m)) ⟩ + suc n - (n - m) ∎ where open ≡-Reasoning + +m+= : {i j m : ℕ } → m + i ≡ m + j → i ≡ j +m+= {i} {j} {zero} refl = refl +m+= {i} {j} {suc m} eq = m+= {i} {j} {m} ( cong (λ k → pred k ) eq ) + ++m= : {i j m : ℕ } → i + m ≡ j + m → i ≡ j ++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 sn<m = <-trans a<sa sn<m + +sa=b→a<b : { n m : ℕ } → suc n ≡ m → n < m +sa=b→a<b {n} {m} sn=m = subst (λ k → n < k ) sn=m a<sa + +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} lt = ⊥-elim ( nat-≤> lt (≤-trans a<sa (s≤s (s≤s z≤n)) )) +minus+n {suc x} {suc y} y<sx with <-cmp y (suc x) +... | tri< a ¬b ¬c = 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} a ⟩ + x ∎ ) ⟩ + suc x ∎ where open ≡-Reasoning +... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< b (px≤py y<sx )) +... | tri> ¬a ¬b c = ⊥-elim ( nat-<> c (px≤py y<sx )) + ++<-cong : {x y z : ℕ } → x < y → z + x < z + y ++<-cong {x} {y} {zero} x<y = x<y ++<-cong {x} {y} {suc z} x<y = s≤s (+<-cong {x} {y} {z} x<y) + +<-minus-0 : {x y z : ℕ } → z + x < z + y → x < y +<-minus-0 {x} {y} {z} x<y with <-cmp x y +... | tri< a ¬b ¬c = a +... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< (cong (λ k → z + k ) b) x<y ) +... | tri> ¬a ¬b c = ⊥-elim ( nat-<> x<y (+<-cong {y} {x} {z} c)) + +<-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 ) + +x≤x+y : {z y : ℕ } → z ≤ z + y +x≤x+y {zero} {y} = z≤n +x≤x+y {suc z} {y} = s≤s (x≤x+y {z} {y}) + +x≤y+x : {z y : ℕ } → z ≤ y + z +x≤y+x {z} {y} = subst (λ k → z ≤ k ) (+-comm _ y ) x≤x+y + +x≤x+sy : {x y : ℕ} → x < x + suc y +x≤x+sy {x} {y} = begin + suc x ≤⟨ x≤x+y ⟩ + suc x + y ≡⟨ cong (λ k → k + y) (+-comm 1 x ) ⟩ + (x + 1) + y ≡⟨ (+-assoc x 1 _) ⟩ + x + suc y ∎ where open ≤-Reasoning + + +<-plus-0 : {x y z : ℕ } → x < y → z + x < z + y +<-plus-0 = +<-cong + +<-plus : {x y z : ℕ } → x < y → x + z < y + z +<-plus {x} {y} {z} x<y = subst₂ (λ j k → j < k ) (+-comm z x ) (+-comm z y ) ( <-plus-0 x<y ) + +≤-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 ) + +≤-plus : {x y z : ℕ } → x ≤ y → x + z ≤ y + z +≤-plus {x} {y} {z} x≤y = subst₂ (λ j k → j ≤ k ) (+-comm z x ) (+-comm z y ) ( ≤-plus-0 x≤y ) + +x+y<z→x<z : {x y z : ℕ } → x + y < z → x < z +x+y<z→x<z {x} {zero} {z} xy<z = subst (λ k → k < z ) (+-comm x zero ) xy<z +x+y<z→x<z {x} {suc y} {z} xy<z = <-minus {x} {z} {suc y} (<-trans xy<z x≤x+sy ) + +*≤ : {x y z : ℕ } → x ≤ y → x * z ≤ y * z +*≤ lt = *-mono-≤ lt ≤-refl + +<to≤ : {x y : ℕ } → x < y → x ≤ y +<to≤ {x} {y} x<y with <-cmp x (suc y) +... | tri< a ¬b ¬c = px≤py a +... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< b (≤-trans x<y a≤sa )) +... | tri> ¬a ¬b c = ⊥-elim ( nat-<> c (≤-trans x<y a≤sa )) + +<sto≤ : {x y : ℕ } → x < suc y → x ≤ y +<sto≤ {x} {y} x<sy with <-cmp x y +... | tri< a ¬b ¬c = <to≤ a +... | tri≈ ¬a refl ¬c = ≤-refl +... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c x<sy ) + +*< : {x y z : ℕ } → x < y → x * suc z < y * suc z +*< {x} {zero} {z} () +*< {x} {suc y} {z} x<y = s≤s ( begin + x * suc z ≤⟨ lem01 ⟩ + y * suc z ≤⟨ x≤x+y ⟩ + y * suc z + z ≡⟨ +-comm _ z ⟩ + z + y * suc z ∎ ) where + open ≤-Reasoning + lem01 : x * suc z ≤ y * suc z + lem01 = *-mono-≤ {x} {y} {suc z} (<sto≤ x<y) ≤-refl + +<to<s : {x y : ℕ } → x < y → x < suc y +<to<s x<y = <-trans x<y a<sa + +<tos<s : {x y : ℕ } → x < y → suc x < suc y +<tos<s x<y = s≤s x<y + +<∨≤ : ( x y : ℕ ) → (x < y ) ∨ (y ≤ x) +<∨≤ x y with <-cmp x y +... | tri< a ¬b ¬c = case1 a +... | tri≈ ¬a refl ¬c = case2 ≤-refl +... | tri> ¬a ¬b c = case2 (<to≤ c) + +x<y→≤ : {x y : ℕ } → x < y → x ≤ suc y +x<y→≤ {x} {y} x<y with <-cmp x (suc y) +... | tri< a ¬b ¬c = <to≤ a +... | tri≈ ¬a b ¬c = refl-≤≡ b +... | tri> ¬a ¬b c = ⊥-elim ( ¬a ( ≤-trans x<y a≤sa )) + +≤→= : {i j : ℕ} → i ≤ j → j ≤ i → i ≡ j +≤→= {i} {j} i≤j j≤i with <-cmp i j +... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> j≤i a ) +... | tri≈ ¬a b ¬c = b +... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> i≤j c ) + +sx≤py→x≤y : {x y : ℕ } → suc x ≤ suc y → x ≤ y +sx≤py→x≤y = px≤py + +sx<py→x<y : {x y : ℕ } → suc x < suc y → x < y +sx<py→x<y {x} {y} sx<sy with <-cmp x y +... | tri< a ¬b ¬c = a +... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< (cong suc b) sx<sy ) +... | tri> ¬a ¬b c = ⊥-elim ( nat-<> (s≤s c) sx<sy ) + +sx≤y→x≤y : {x y : ℕ } → suc x ≤ y → x ≤ y +sx≤y→x≤y sx≤y = ≤-trans a≤sa sx≤y + +x<sy→x≤y : {x y : ℕ } → x < suc y → x ≤ y +x<sy→x≤y = <sto≤ + +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 sx≤y = sx≤y + +open import Data.Product + +i-j=0→i=j : {i j : ℕ } → j ≤ i → i - j ≡ 0 → i ≡ j +i-j=0→i=j {i} {j} le j=0 = begin + i ≡⟨ sym (m-0=m) ⟩ + i - 0 ≡⟨ cong (λ k → i - k ) (sym j=0) ⟩ + i - (i - j ) ≡⟨ sym (n-n-m=m le) ⟩ + j ∎ where open ≡-Reasoning + +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} eq = 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} y≤x = minus+1 {x} {y} (sx≤py→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 +minus+yz {suc x} {y} {z} z≤y = begin + suc x + minus y z ≡⟨ cong suc ( minus+yz z≤y ) ⟩ + suc (minus (x + y) z) ≡⟨ minus+1 {x + y} {z} (≤-trans z≤y (subst (λ g → y ≤ g) (+-comm y x) x≤x+y) ) ⟩ + minus (suc x + y) z ∎ where open ≡-Reasoning + +minus<=0 : {x y : ℕ } → x ≤ y → minus x y ≡ 0 +minus<=0 {0} {zero} le = refl +minus<=0 {0} {suc y} le = refl +minus<=0 {suc x} {suc y} le = minus<=0 {x} {y} (sx≤py→x≤y le) + +minus>0 : {x y : ℕ } → x < y → 0 < minus y x +minus>0 {zero} {suc _} lt = lt +minus>0 {suc x} {suc y} lt = minus>0 {x} {y} (sx<py→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 +... | tri< a ¬b ¬c = a +... | tri≈ ¬a refl ¬c = ⊥-elim ( nat-≡< (sym (minus<=0 {x} ≤-refl)) lt ) +... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym (minus<=0 {y} (≤-trans refl-≤s c ))) lt ) + +minus+y-y : {x y : ℕ } → (x + y) - y ≡ x +minus+y-y {zero} {y} = minus<=0 {zero + y} {y} ≤-refl +minus+y-y {suc x} {y} = begin + (suc x + y) - y ≡⟨ sym (minus+1 {_} {y} x≤y+x) ⟩ + suc ((x + y) - y) ≡⟨ cong suc (minus+y-y {x} {y}) ⟩ + suc x ∎ where open ≡-Reasoning + +minus+yx-yz : {x y z : ℕ } → (y + x) - (y + z) ≡ x - z +minus+yx-yz {x} {zero} {z} = refl +minus+yx-yz {x} {suc y} {z} = minus+yx-yz {x} {y} {z} + +minus+xy-zy : {x y z : ℕ } → (x + y) - (z + y) ≡ x - z +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} lt = +cancel<l x z {y} (sx<py→x<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 ) + +minus<z : {x y z : ℕ } → x < y → z ≤ x → x - z < y - z +minus<z {x} {y} {z} x<y z≤x = +cancel<r _ _ ( begin + suc ( (x - z) + z ) ≡⟨ cong suc (minus+n (s≤s z≤x) ) ⟩ + suc x ≤⟨ x<y ⟩ + y ≡⟨ sym ( minus+n (<-trans (s≤s z≤x) (s≤s x<y) )) ⟩ + (y - z ) + z ∎ ) where open ≤-Reasoning + + +y-x<y : {x y : ℕ } → 0 < x → 0 < y → y - x < y +y-x<y {x} {y} 0<x 0<y with <-cmp x (suc y) +... | tri< a ¬b ¬c = +cancel<r (y - x) _ ( begin + suc ((y - x) + x) ≡⟨ cong suc (minus+n {y} {x} a ) ⟩ + suc y ≡⟨ +-comm 1 _ ⟩ + y + suc 0 ≤⟨ +-mono-≤ ≤-refl 0<x ⟩ + y + x ∎ ) where open ≤-Reasoning +... | tri≈ ¬a refl ¬c = subst ( λ k → k < y ) (sym (minus<=0 {y} {x} refl-≤s )) 0<y +... | tri> ¬a ¬b c = subst ( λ k → k < y ) (sym (minus<=0 {y} {x} (≤-trans (≤-trans refl-≤s refl-≤s) c))) 0<y -- suc (suc y) ≤ x → y ≤ x + +open import Relation.Binary.Definitions + +distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z) +distr-minus-* {x} {zero} {z} = refl +distr-minus-* {x} {suc y} {z} with <-cmp x y +distr-minus-* {x} {suc y} {z} | tri< a ¬b ¬c = begin + minus x (suc y) * z + ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} (x<y→≤ a)) ⟩ + 0 * z + ≡⟨ sym (minus<=0 {x * z} {z + y * z} le ) ⟩ + minus (x * z) (z + y * z) + ∎ where + open ≡-Reasoning + le : x * z ≤ z + y * z + le = ≤-trans lemma (subst (λ k → y * z ≤ k ) (+-comm _ z ) (x≤x+y {y * z} {z} ) ) where + lemma : x * z ≤ y * z + lemma = *≤ {x} {y} {z} (<to≤ a) +distr-minus-* {x} {suc y} {z} | tri≈ ¬a refl ¬c = begin + minus x (suc y) * z + ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} refl-≤s ) ⟩ + 0 * z + ≡⟨ sym (minus<=0 {x * z} {z + y * z} (lt {x} {z} )) ⟩ + minus (x * z) (z + y * z) + ∎ where + open ≡-Reasoning + lt : {x z : ℕ } → x * z ≤ z + x * z + lt {zero} {zero} = z≤n + lt {suc x} {zero} = lt {x} {zero} + lt {x} {suc z} = ≤-trans lemma refl-≤s where + lemma : x * suc z ≤ z + x * suc z + lemma = subst (λ k → x * suc z ≤ k ) (+-comm _ z) (x≤x+y {x * suc z} {z}) +distr-minus-* {x} {suc y} {z} | tri> ¬a ¬b c = +m= {_} {_} {suc y * z} ( begin + minus x (suc y) * z + suc y * z + ≡⟨ sym (proj₂ *-distrib-+ z (minus x (suc y) ) _) ⟩ + ( minus x (suc y) + suc y ) * z + ≡⟨ cong (λ k → k * z) (minus+n {x} {suc y} (s≤s c)) ⟩ + x * z + ≡⟨ sym (minus+n {x * z} {suc y * z} (s≤s (lt c))) ⟩ + minus (x * z) (suc y * z) + suc y * z + ∎ ) where + open ≡-Reasoning + lt : {x y z : ℕ } → suc y ≤ x → z + y * z ≤ x * z + lt {x} {y} {z} le = *≤ le + +distr-minus-*' : {z x y : ℕ } → z * (minus x y) ≡ minus (z * x) (z * y) +distr-minus-*' {z} {x} {y} = begin + z * (minus x y) ≡⟨ *-comm _ (x - y) ⟩ + (minus x y) * z ≡⟨ distr-minus-* {x} {y} {z} ⟩ + minus (x * z) (y * z) ≡⟨ cong₂ (λ j k → j - k ) (*-comm x z ) (*-comm y z) ⟩ + minus (z * x) (z * y) ∎ where open ≡-Reasoning + +minus- : {x y z : ℕ } → suc x > z + y → minus (minus x y) z ≡ minus x (y + z) +minus- {x} {y} {z} gt = +m= {_} {_} {z} ( begin + minus (minus x y) z + z + ≡⟨ minus+n {_} {z} lemma ⟩ + minus x y + ≡⟨ +m= {_} {_} {y} ( begin + minus x y + y + ≡⟨ minus+n {_} {y} lemma1 ⟩ + x + ≡⟨ sym ( minus+n {_} {z + y} gt ) ⟩ + minus x (z + y) + (z + y) + ≡⟨ sym ( +-assoc (minus x (z + y)) _ _ ) ⟩ + minus x (z + y) + z + y + ∎ ) ⟩ + minus x (z + y) + z + ≡⟨ cong (λ k → minus x k + z ) (+-comm _ y ) ⟩ + minus x (y + z) + z + ∎ ) where + open ≡-Reasoning + lemma1 : suc x > y + lemma1 = x+y<z→x<z (subst (λ k → k < suc x ) (+-comm z _ ) gt ) + lemma : suc (minus x y) > z + lemma = <-minus {_} {_} {y} ( subst ( λ x → z + y < suc x ) (sym (minus+n {x} {y} lemma1 )) gt ) + +sn≤1→n=0 : {n : ℕ } → suc n ≤ 1 → n ≡ 0 +sn≤1→n=0 {n} sn≤1 with <-cmp n 0 +... | tri≈ ¬a b ¬c = b +... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c sn≤1 ) + +minus-* : {M k n : ℕ } → n < k → minus k (suc n) * M ≡ minus (minus k n * M ) M +minus-* {zero} {k} {n} lt = begin + minus k (suc n) * zero + ≡⟨ *-comm (minus k (suc n)) zero ⟩ + zero * minus k (suc n) + ≡⟨⟩ + 0 * minus k n + ≡⟨ *-comm 0 (minus k n) ⟩ + minus (minus k n * 0 ) 0 + ∎ where + open ≡-Reasoning +minus-* {suc m} {k} {n} lt with <-cmp k 1 +minus-* {suc m} {k} {n} lt | tri< a ¬b ¬c = ⊥-elim ( nat-≤> (sx≤py→x≤y a) (≤-trans (s≤s z≤n) lt) ) +minus-* {suc m} {k} {n} lt | tri≈ ¬a refl ¬c = subst (λ k → minus 0 k * suc m ≡ minus (minus 1 k * suc m) (suc m)) (sym n=0) lem where + n=0 : n ≡ 0 + n=0 = sn≤1→n=0 lt + lem : minus 0 0 * suc m ≡ minus (minus 1 0 * suc m) (suc m) + lem = begin + minus 0 0 * suc m ≡⟨⟩ + 0 ≡⟨ sym ( minus<=0 {suc m} {suc m} ≤-refl ) ⟩ + minus (suc m) (suc m) ≡⟨ cong (λ k → minus k (suc m)) (+-comm 0 (suc m) ) ⟩ + minus (suc m + 0) (suc m) ≡⟨⟩ + minus (minus 1 0 * suc m) (suc m) ∎ where open ≡-Reasoning +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 {n} {k} {m} lt = ≤-plus-0 {_} {_} {1} (*≤ lt ) + open ≡-Reasoning + +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 +x=y+z→x-z=y {suc x} {suc y} {zero} eq = begin -- suc x ≡ suc (y + zero) → (suc x - zero) ≡ suc y + suc x - zero ≡⟨ refl ⟩ + suc x ≡⟨ eq ⟩ + suc y + zero ≡⟨ +-comm _ zero ⟩ + suc y ∎ where open ≡-Reasoning +x=y+z→x-z=y {suc x} {suc y} {suc z} eq = x=y+z→x-z=y {x} {suc y} {z} ( begin + x ≡⟨ cong pred eq ⟩ + pred (suc y + suc z) ≡⟨ +-comm _ (suc z) ⟩ + suc z + y ≡⟨ cong suc ( +-comm _ y ) ⟩ + suc y + z ∎ ) where open ≡-Reasoning + +m*1=m : {m : ℕ } → m * 1 ≡ m +m*1=m {zero} = refl +m*1=m {suc m} = cong suc m*1=m + ++-cancel-1 : (x y z : ℕ ) → x + y ≡ x + z → y ≡ z ++-cancel-1 zero y z eq = eq ++-cancel-1 (suc x) y z eq = +-cancel-1 x y z (cong pred eq ) + ++-cancel-0 : (x y z : ℕ ) → y + x ≡ z + x → y ≡ z ++-cancel-0 x y z eq = +-cancel-1 x y z (trans (+-comm x y) (trans eq (sym (+-comm x z)) )) + +*-cancel-left : {x y z : ℕ } → x > 0 → x * y ≡ x * z → y ≡ z +*-cancel-left {suc x} {zero} {zero} lt eq = refl +*-cancel-left {suc x} {zero} {suc z} lt eq = ⊥-elim ( nat-≡< eq (s≤s (begin + x * zero ≡⟨ *-comm x _ ⟩ + zero ≤⟨ z≤n ⟩ + z + x * suc z ∎ ))) where open ≤-Reasoning +*-cancel-left {suc x} {suc y} {zero} lt eq = ⊥-elim ( nat-≡< (sym eq) (s≤s (begin + x * zero ≡⟨ *-comm x _ ⟩ + zero ≤⟨ z≤n ⟩ + _ ∎ ))) where open ≤-Reasoning +*-cancel-left {suc x} {suc y} {suc z} lt eq with cong pred eq +... | eq1 = cong suc (*-cancel-left {suc x} {y} {z} lt (+-cancel-0 x _ _ (begin + y + x * y + x ≡⟨ +-assoc y _ _ ⟩ + y + (x * y + x) ≡⟨ cong (λ k → y + (k + x)) (*-comm x _) ⟩ + y + (y * x + x) ≡⟨ cong (_+_ y) (+-comm _ x) ⟩ + y + (x + y * x ) ≡⟨ refl ⟩ + y + suc y * x ≡⟨ cong (_+_ y) (*-comm (suc y) _) ⟩ + y + x * suc y ≡⟨ eq1 ⟩ + z + x * suc z ≡⟨ refl ⟩ + _ ≡⟨ sym ( cong (_+_ z) (*-comm (suc z) _) ) ⟩ + _ ≡⟨ sym ( cong (_+_ z) (+-comm _ x)) ⟩ + z + (z * x + x) ≡⟨ sym ( cong (λ k → z + (k + x)) (*-comm x _) ) ⟩ + z + (x * z + x) ≡⟨ sym ( +-assoc z _ _) ⟩ + z + x * z + x ∎ ))) where open ≡-Reasoning + +record Finduction {n m : Level} (P : Set n ) (Q : P → Set m ) (f : P → ℕ) : Set (n Level.⊔ m) where + field + fzero : {p : P} → f p ≡ zero → Q p + pnext : (p : P ) → P + decline : {p : P} → 0 < f p → f (pnext p) < f p + ind : {p : P} → Q (pnext p) → Q p + +y<sx→y≤x : {x y : ℕ} → y < suc x → y ≤ x +y<sx→y≤x = x<sy→x≤y + +fi0 : (x : ℕ) → x ≤ zero → x ≡ zero +fi0 .0 z≤n = refl + +f-induction : {n m : Level} {P : Set n } → {Q : P → Set m } + → (f : P → ℕ) + → Finduction P Q f + → (p : P ) → Q p +f-induction {n} {m} {P} {Q} f I p with <-cmp 0 (f p) +... | tri> ¬a ¬b () +... | tri≈ ¬a b ¬c = Finduction.fzero I (sym b) +... | tri< lt _ _ = f-induction0 p (f p) (<to≤ (Finduction.decline I lt)) where + 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< a ¬b ¬c = f-induction0 p x (px≤py a) + ... | 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} + (subst (λ k → 0 < k ) (sym b) (s≤s z≤n ) )) + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> le c ) + + +record Ninduction {n m : Level} (P : Set n ) (Q : P → Set m ) (f : P → ℕ) : Set (n Level.⊔ m) where + field + pnext : (p : P ) → P + fzero : {p : P} → f (pnext p) ≡ zero → Q p + decline : {p : P} → 0 < f p → f (pnext p) < f p + ind : {p : P} → Q (pnext p) → Q p + +s≤s→≤ : { i j : ℕ} → suc i ≤ suc j → i ≤ j +s≤s→≤ = sx≤py→x≤y + +n-induction : {n m : Level} {P : Set n } → {Q : P → Set m } + → (f : P → ℕ) + → Ninduction P Q f + → (p : P ) → Q p +n-induction {n} {m} {P} {Q} f I p = f-induction0 p (f (Ninduction.pnext I p)) ≤-refl where + 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< a ¬b ¬c = f-induction0 p x (px≤py a) + ... | 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 ) + nle : suc (f (Ninduction.pnext I (Ninduction.pnext I p))) ≤ suc x + nle = subst (λ k → suc (f (Ninduction.pnext I (Ninduction.pnext I p))) ≤ k) b (Ninduction.decline I {Ninduction.pnext I p} f>0 ) + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> le c ) + + +record Factor (n m : ℕ ) : Set where + field + factor : ℕ + remain : ℕ + is-factor : factor * n + remain ≡ m + +record Factor< (n m : ℕ ) : Set where + field + factor : ℕ + remain : ℕ + is-factor : factor * n + remain ≡ m + remain<n : remain < n + +record Dividable (n m : ℕ ) : Set where + field + factor : ℕ + is-factor : factor * n + 0 ≡ m + +open Factor + +DtoF : {n m : ℕ} → Dividable n m → Factor n m +DtoF {n} {m} record { factor = f ; is-factor = fa } = record { factor = f ; remain = 0 ; is-factor = fa } + +FtoD : {n m : ℕ} → (fc : Factor n m) → remain fc ≡ 0 → Dividable n m +FtoD {n} {m} record { factor = f ; remain = r ; is-factor = fa } refl = record { factor = f ; is-factor = fa } + +--divdable^2 : ( n k : ℕ ) → Dividable k ( n * n ) → Dividable k n +--divdable^2 n k dn2 = {!!} + +decf : { n k : ℕ } → ( x : Factor k (suc n) ) → Factor k n +decf {n} {k} record { factor = f ; remain = r ; is-factor = fa } = + decf1 {n} {k} f r fa where + decf1 : { n k : ℕ } → (f r : ℕ) → (f * k + r ≡ suc n) → Factor k n + decf1 {n} {k} f (suc r) fa = -- this case must be the first + record { factor = f ; remain = r ; is-factor = ( begin -- fa : f * k + suc r ≡ suc n + f * k + r ≡⟨ cong pred ( begin + suc ( f * k + r ) ≡⟨ +-comm _ r ⟩ + r + suc (f * k) ≡⟨ sym (+-assoc r 1 _) ⟩ + (r + 1) + f * k ≡⟨ cong (λ t → t + f * k ) (+-comm r 1) ⟩ + (suc r ) + f * k ≡⟨ +-comm (suc r) _ ⟩ + f * k + suc r ≡⟨ fa ⟩ + suc n ∎ ) ⟩ + n ∎ ) } where open ≡-Reasoning + decf1 {n} {zero} (suc f) zero fa = ⊥-elim ( nat-≡< fa ( + begin suc (suc f * zero + zero) ≡⟨ cong suc (+-comm _ zero) ⟩ + suc (f * 0) ≡⟨ cong suc (*-comm f zero) ⟩ + suc zero ≤⟨ s≤s z≤n ⟩ + suc n ∎ )) where open ≤-Reasoning + decf1 {n} {suc k} (suc f) zero fa = + record { factor = f ; remain = k ; is-factor = ( begin -- fa : suc (k + f * suc k + zero) ≡ suc n + f * suc k + k ≡⟨ +-comm _ k ⟩ + k + f * suc k ≡⟨ +-comm zero _ ⟩ + (k + f * suc k) + zero ≡⟨ cong pred fa ⟩ + n ∎ ) } where open ≡-Reasoning + +div0 : {k : ℕ} → Dividable k 0 +div0 {k} = record { factor = 0; is-factor = refl } + +div= : {k : ℕ} → Dividable k k +div= {k} = record { factor = 1; is-factor = ( begin + k + 0 * k + 0 ≡⟨ trans ( +-comm _ 0) ( +-comm _ 0) ⟩ + k ∎ ) } where open ≡-Reasoning + +div1 : { k : ℕ } → k > 1 → ¬ Dividable k 1 +div1 {k} k>1 record { factor = f1 ; is-factor = fa } = ⊥-elim ( nat-≡< (sym fa) ( begin + 2 ≤⟨ k>1 ⟩ + k ≡⟨ +-comm 0 _ ⟩ + k + 0 ≡⟨ refl ⟩ + 1 * k ≤⟨ *-mono-≤ {1} {f1} (lem1 _ fa) ≤-refl ⟩ + f1 * k ≡⟨ +-comm 0 _ ⟩ + f1 * k + 0 ∎ )) where + open ≤-Reasoning + lem1 : (f1 : ℕ) → f1 * k + 0 ≡ 1 → 1 ≤ f1 + lem1 zero () + lem1 (suc f1) eq = s≤s z≤n + +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 + fki = Dividable.factor di + fkj = Dividable.factor dj + div+div1 : Dividable k (i + j) + div+div1 = record { factor = fki + fkj ; is-factor = ( begin + (fki + fkj) * k + 0 ≡⟨ +-comm _ 0 ⟩ + (fki + fkj) * k ≡⟨ *-distribʳ-+ k fki _ ⟩ + fki * k + fkj * k ≡⟨ cong₂ ( λ i j → i + j ) (+-comm 0 (fki * k)) (+-comm 0 (fkj * k)) ⟩ + (fki * k + 0) + (fkj * k + 0) ≡⟨ cong₂ ( λ i j → i + j ) (Dividable.is-factor di) (Dividable.is-factor dj) ⟩ + i + j ∎ ) } where + open ≡-Reasoning + +div-div : { i j k : ℕ } → k > 1 → Dividable k i → Dividable k j → Dividable k (i - j) ∧ Dividable k (j - i) +div-div {i} {j} {k} k>1 di dj = ⟪ div-div1 di dj , div-div1 dj di ⟫ where + div-div1 : {i j : ℕ } → Dividable k i → Dividable k j → Dividable k (i - j) + div-div1 {i} {j} di dj = record { factor = fki - fkj ; is-factor = ( begin + (fki - fkj) * k + 0 ≡⟨ +-comm _ 0 ⟩ + (fki - fkj) * k ≡⟨ distr-minus-* {fki} {fkj} ⟩ + (fki * k) - (fkj * k) ≡⟨ cong₂ ( λ i j → i - j ) (+-comm 0 (fki * k)) (+-comm 0 (fkj * k)) ⟩ + (fki * k + 0) - (fkj * k + 0) ≡⟨ cong₂ ( λ i j → i - j ) (Dividable.is-factor di) (Dividable.is-factor dj) ⟩ + i - j ∎ ) } where + open ≡-Reasoning + fki = Dividable.factor di + fkj = Dividable.factor dj + +open _∧_ + +div+1 : { i k : ℕ } → k > 1 → Dividable k i → ¬ Dividable k (suc i) +div+1 {i} {k} k>1 d d1 = div1 k>1 div+11 where + div+11 : Dividable k 1 + div+11 = subst (λ g → Dividable k g) (minus+y-y {1} {i} ) ( proj2 (div-div k>1 d d1 ) ) + +div<k : { m k : ℕ } → k > 1 → m > 0 → m < k → ¬ Dividable k m +div<k {m} {k} k>1 m>0 m<k d = ⊥-elim ( nat-≤> (div<k1 (Dividable.factor d) (Dividable.is-factor d)) m<k ) where + div<k1 : (f : ℕ ) → f * k + 0 ≡ m → k ≤ m + div<k1 zero eq = ⊥-elim (nat-≡< eq m>0 ) + div<k1 (suc f) eq = begin + k ≤⟨ x≤x+y ⟩ + k + (f * k + 0) ≡⟨ sym (+-assoc k _ _) ⟩ + k + f * k + 0 ≡⟨ eq ⟩ + m ∎ where open ≤-Reasoning + +0<factor : { m k : ℕ } → k > 0 → m > 0 → (d : Dividable k m ) → Dividable.factor d > 0 +0<factor {m} {k} k>0 m>0 d with Dividable.factor d in eq1 +... | zero = ⊥-elim ( nat-≡< ff1 m>0 ) where + ff1 : 0 ≡ m + ff1 = begin + 0 ≡⟨⟩ + 0 * k + 0 ≡⟨ cong (λ j → j * k + 0) (sym eq1) ⟩ + Dividable.factor d * k + 0 ≡⟨ Dividable.is-factor d ⟩ + m ∎ where open ≡-Reasoning +... | suc t = s≤s z≤n + +div→k≤m : { m k : ℕ } → k > 1 → m > 0 → Dividable k m → m ≥ k +div→k≤m {m} {k} k>1 m>0 d with <-cmp m k +... | tri< a ¬b ¬c = ⊥-elim ( div<k k>1 m>0 a d ) +... | tri≈ ¬a refl ¬c = ≤-refl +... | tri> ¬a ¬b c = <to≤ c + +div1*k+0=k : {k : ℕ } → 1 * k + 0 ≡ k +div1*k+0=k {k} = begin + 1 * k + 0 ≡⟨ cong (λ g → g + 0) (+-comm _ 0) ⟩ + k + 0 ≡⟨ +-comm _ 0 ⟩ + k ∎ where open ≡-Reasoning + + +factor< : {k m : ℕ} → k > 1 → Factor< k m +factor< {k} {m} k>1 = n-induction {_} {_} {ℕ} {λ m → Factor< k m} F I m where + F : ℕ → ℕ + F m = m + F0 : ( m : ℕ ) → F (m - k) ≡ 0 → Factor< k m + F0 0 eq = record { factor = 0 ; remain = 0 ; is-factor = refl ; remain<n = <-trans a<sa k>1 } + F0 (suc m) eq with <-cmp k (suc m) + ... | tri< a ¬b ¬c = record { factor = 1 ; remain = 0 ; is-factor = lem00 ; remain<n = <-trans a<sa k>1 } where + lem00 : k + zero + 0 ≡ suc m + lem00 = begin -- minus (suc m) k ≡ 0 + k + zero + 0 ≡⟨ +-comm (k + 0) _ ⟩ + k + 0 ≡⟨ +-comm k _ ⟩ + k ≡⟨ sym ( i-j=0→i=j (≤-trans a≤sa a) eq ) ⟩ + suc m ∎ where open ≡-Reasoning + ... | tri≈ ¬a b ¬c = record { factor = 1 ; remain = 0 ; is-factor = trans (trans (+-comm (k + 0) _) (+-comm k 0)) b ; remain<n = <-trans a<sa k>1 } + ... | tri> ¬a ¬b c = record { factor = 0 ; remain = suc m ; is-factor = refl ; remain<n = c } + ind : {m : ℕ} → Factor< k (m - k) → Factor< k m + ind {m} record { factor = f ; remain = r ; is-factor = isf ; remain<n = r<n } with <-cmp k (suc m) + ... | tri≈ ¬a b ¬c = record { factor = 0 ; remain = m ; is-factor = refl ; remain<n = subst (λ j → m < j) (sym b) a<sa } + ... | tri> ¬a ¬b c = record { factor = 0 ; remain = m ; is-factor = refl ; remain<n = <-trans a<sa c } + ... | tri< a ¬b ¬c = record { factor = suc f ; remain = r ; is-factor = lem00 ; remain<n = r<n } where + k<sm : k < suc m + k<sm = a + lem00 : k + f * k + r ≡ m + lem00 = begin + k + f * k + r ≡⟨ +-assoc k _ _ ⟩ + k + (f * k + r) ≡⟨ +-comm k _ ⟩ + (f * k + r) + k ≡⟨ cong (λ i → i + k ) isf ⟩ + (m - k) + k ≡⟨ minus+n k<sm ⟩ + m ∎ where open ≡-Reasoning + decl : {m : ℕ } → 0 < m → m - k < m + decl {m} 0<m = y-x<y (<-trans a<sa k>1 ) 0<m + I : Ninduction ℕ _ F + I = record { + pnext = λ p → p - k + ; fzero = λ {m} eq → F0 m eq + ; decline = λ {m} lt → decl lt + ; ind = λ {p} prev → ind prev + } + +Factor<→¬k≤m : {k m : ℕ} → k ≤ m → (x : Factor< k m ) → Factor<.factor x > 0 +Factor<→¬k≤m {k} {m} k≤m x with Factor<.factor x in eqx +... | zero = ⊥-elim ( nat-≤> k≤m (begin + suc m ≡⟨ cong suc (sym (Factor<.is-factor x)) ⟩ + suc (Factor<.factor x * k + Factor<.remain x) ≡⟨ cong (λ j → suc (j * k + _)) eqx ⟩ + suc (0 * k + Factor<.remain x) ≡⟨ refl ⟩ + suc (Factor<.remain x) ≤⟨ Factor<.remain<n x ⟩ + k ∎ ) ) where open ≤-Reasoning +... | suc fa = s≤s z≤n + +Factor<-inject : {k m : ℕ} → k > 1 → (x y : Factor< k m) → (Factor<.factor x ≡ Factor<.factor y ) ∧ (Factor<.remain x ≡ Factor<.remain y ) +Factor<-inject {k} {m} k>1 x y = n-induction {_} {_} {ℕ} + {λ m → (x y : Factor< k m) → (Factor<.factor x ≡ Factor<.factor y ) ∧ (Factor<.remain x ≡ Factor<.remain y ) } F I m x y where + F : ℕ → ℕ + F m = m + f00 : (m : ℕ ) → ( k ≡ suc m ) → (x y : Factor< k (suc m)) → (Factor<.factor x ≡ Factor<.factor y ) ∧ (Factor<.remain x ≡ Factor<.remain y ) + f00 m lem00 x y = ⟪ trans (lem02 x) (sym (lem02 y)) , trans (lem01 x) (sym (lem01 y)) ⟫ where + lem02 : (f : Factor< k (suc m)) → Factor<.factor f ≡ 1 + lem02 f with <-cmp (Factor<.factor f) 1 + ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (Factor<.is-factor f) (begin + suc (Factor<.factor f * k + Factor<.remain f) ≤⟨ s≤s (≤-plus {_} {_} {Factor<.remain f} (*≤ (px≤py a)) ) ⟩ + suc (0 * k + Factor<.remain f) ≡⟨⟩ + suc (0 + Factor<.remain f) ≡⟨⟩ + suc (Factor<.remain f) ≤⟨ Factor<.remain<n f ⟩ + k ≡⟨ lem00 ⟩ + suc m ∎ )) where open ≤-Reasoning + ... | tri≈ ¬a b ¬c = b + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym (Factor<.is-factor f)) (begin -- 1 < Factor<. factor f, fa * k + r > k ≡ suc m + suc (suc m) ≡⟨ cong suc (sym lem00) ⟩ + suc k ≡⟨ sym (+-comm k 1) ⟩ + k + 1 <⟨ <-plus-0 k>1 ⟩ + k + k ≡⟨ cong (λ j → k + j) (+-comm 0 _ ) ⟩ + k + (k + 0) ≡⟨⟩ + k + (k + 0 * k) ≡⟨ refl ⟩ + 2 * k ≤⟨ *≤ c ⟩ + Factor<.factor f * k ≤⟨ x≤x+y ⟩ + Factor<.factor f * k + Factor<.remain f ∎ ) ) where open ≤-Reasoning + lem03 : k ≡ 1 * k + lem03 = +-comm 0 k + lem01 : (f : Factor< k (suc m)) → Factor<.remain f ≡ 0 + lem01 f = +-cancel-1 _ _ _ ( begin + Factor<.factor f * k + Factor<.remain f ≡⟨ Factor<.is-factor f ⟩ + suc m ≡⟨ sym lem00 ⟩ + k ≡⟨ +-comm 0 k ⟩ + k + 0 ≡⟨ cong (λ j → j + 0) lem03 ⟩ + 1 * k + 0 ≡⟨ cong (λ j → j * k + 0) (sym (lem02 f)) ⟩ + Factor<.factor f * k + 0 ∎ ) where open ≡-Reasoning + F0 : ( m : ℕ ) → F (m - k) ≡ 0 → (x y : Factor< k m) → (Factor<.factor x ≡ Factor<.factor y ) ∧ (Factor<.remain x ≡ Factor<.remain y ) + F0 0 eq x y = ⟪ trans (lem00 x) (sym (lem00 y)) , trans (lem01 x) (sym (lem01 y)) ⟫ where + lem01 : (f : Factor< k 0) → Factor<.remain f ≡ 0 + lem01 f with Factor<.remain f in eq1 + ... | zero = refl + ... | suc n = ⊥-elim ( nat-≡< (sym (Factor<.is-factor f)) (begin + suc 0 ≤⟨ s≤s z≤n ⟩ + suc n ≡⟨ sym eq1 ⟩ + Factor<.remain f ≡⟨ refl ⟩ + 0 + Factor<.remain f ≤⟨ x≤y+x ⟩ + Factor<.factor f * k + Factor<.remain f ∎ ) ) where open ≤-Reasoning + lem00 : (f : Factor< k 0) → Factor<.factor f ≡ 0 + lem00 f with m*n=0⇒m=0∨n=0 {Factor<.factor f} {k} (trans (+-comm 0 (Factor<.factor f * k) ) (subst (λ j → _ + j ≡ 0) (lem01 f) (Factor<.is-factor f))) + ... | case1 fa=0 = fa=0 + ... | case2 k=0 = ⊥-elim (nat-≡< (sym k=0) (<-trans a<sa k>1) ) + F0 (suc m) eq x y with <-cmp k (suc m) + ... | tri< a ¬b ¬c = ⊥-elim ( ¬b lem00 ) where + lem00 : k ≡ suc m + lem00 = begin + k ≡⟨ sym ( i-j=0→i=j (≤-trans a≤sa a) eq ) ⟩ + suc m ∎ where open ≡-Reasoning + ... | tri≈ ¬a b ¬c = f00 m b x y + ... | tri> ¬a ¬b c = ⟪ trans ( lem00 x ) (sym (lem00 y)) , trans (lem01 x) (sym (lem01 y)) ⟫ where + lem00 : (f : Factor< k (suc m)) → Factor<.factor f ≡ 0 + lem00 f with Factor<.factor f in eq1 + ... | zero = refl + ... | suc fa = ⊥-elim ( nat-≡< (sym (Factor<.is-factor f)) (begin + suc (suc m) ≤⟨ c ⟩ + k ≤⟨ x≤x+y ⟩ + k + Factor<.remain f ≡⟨ cong (λ j → j + _) (+-comm 0 k) ⟩ + suc 0 * k + Factor<.remain f ≤⟨ ≤-plus {_} {_} {Factor<.remain f} (*≤ {suc 0} {suc fa} {k} (s≤s z≤n)) ⟩ + suc fa * k + Factor<.remain f ≡⟨ cong (λ j → j * k + Factor<.remain f) (sym eq1) ⟩ + Factor<.factor f * k + Factor<.remain f ∎ ) ) where open ≤-Reasoning + lem01 : (f : Factor< k (suc m)) → Factor<.remain f ≡ (suc m) + lem01 f = begin + Factor<.remain f ≡⟨ refl ⟩ + 0 * k + Factor<.remain f ≡⟨ cong (λ j → j * k + Factor<.remain f) (sym (lem00 f)) ⟩ + Factor<.factor f * k + Factor<.remain f ≡⟨ Factor<.is-factor f ⟩ + suc m ∎ where open ≡-Reasoning + ind : {m : ℕ} + → ( (x y : Factor< k (m - k)) → (Factor<.factor x ≡ Factor<.factor y ) ∧ (Factor<.remain x ≡ Factor<.remain y ) ) + → (x y : Factor< k m) → (Factor<.factor x ≡ Factor<.factor y ) ∧ (Factor<.remain x ≡ Factor<.remain y ) + ind {m} prev x y with <∨≤ m k + ... | case1 m<k = ⟪ trans (lem00 x) (sym (lem00 y)) , trans (lem01 x) (sym (lem01 y)) ⟫ where + lem00 : (x : Factor< k m ) → Factor<.factor x ≡ 0 + lem00 x with Factor<.factor x in eqx + ... | zero = refl + ... | suc fa = ⊥-elim ( nat-≤> (begin + k ≤⟨ x≤x+y ⟩ + k + (fa * k + Factor<.remain x) ≡⟨ sym (+-assoc k _ _) ⟩ + ( k + fa * k ) + Factor<.remain x ≡⟨ refl ⟩ + suc fa * k + Factor<.remain x ≡⟨ cong (λ j → j * k + Factor<.remain x) (sym eqx) ⟩ + Factor<.factor x * k + Factor<.remain x ≡⟨ Factor<.is-factor x ⟩ + m ∎ ) + m<k ) where open ≤-Reasoning + lem01 : (f : Factor< k m) → Factor<.remain f ≡ m + lem01 f = begin + Factor<.remain f ≡⟨ refl ⟩ + 0 * k + Factor<.remain f ≡⟨ cong (λ j → j * k + Factor<.remain f) (sym (lem00 f)) ⟩ + Factor<.factor f * k + Factor<.remain f ≡⟨ Factor<.is-factor f ⟩ + m ∎ where open ≡-Reasoning + ... | case2 k≤m = px=py x y k≤m where + lem07 : (x : Factor< k m ) → {fa : ℕ } → suc fa ≡ Factor<.factor x → fa * k + Factor<.remain x ≡ m - k + lem07 x {fa} eq1 = begin + fa * k + Factor<.remain x ≡⟨ sym (minus+y-y {_} {k} ) ⟩ + (fa * k + Factor<.remain x + k ) - k ≡⟨ cong (λ j → j - k) ( begin + fa * k + Factor<.remain x + k ≡⟨ +-assoc (fa * k) _ _ ⟩ + fa * k + (Factor<.remain x + k) ≡⟨ cong (λ j → fa * k + j) (+-comm _ k) ⟩ + fa * k + (k + Factor<.remain x ) ≡⟨ sym (+-assoc (fa * k) k _ ) ⟩ + (fa * k + k) + Factor<.remain x ≡⟨ cong (λ j → j + Factor<.remain x ) (+-comm (fa * k) k) ⟩ + suc fa * k + Factor<.remain x ≡⟨ cong (λ j → j * k + _) (eq1) ⟩ + Factor<.factor x * k + Factor<.remain x ∎ ) ⟩ + (Factor<.factor x * k + Factor<.remain x) - k ≡⟨ cong (λ j → j - k ) (Factor<.is-factor x) ⟩ + m - k ∎ where open ≡-Reasoning + px=py : (x y : Factor< k m) → k ≤ m → (Factor<.factor x ≡ Factor<.factor y ) ∧ (Factor<.remain x ≡ Factor<.remain y ) + px=py x y k≤m with Factor<.factor x in eqx | Factor<.factor y in eqy + ... | zero | _ = ⊥-elim ( nat-≡< (sym eqx) (Factor<→¬k≤m k≤m x) ) + ... | _ | zero = ⊥-elim ( nat-≡< (sym eqy) (Factor<→¬k≤m k≤m y) ) + ... | suc fx | suc fy with prev + record { factor = fx ; remain = Factor<.remain x ; is-factor = lem07 x (sym eqx) ; remain<n = Factor<.remain<n x } + record { factor = fy ; remain = Factor<.remain y ; is-factor = lem07 y (sym eqy) ; remain<n = Factor<.remain<n y } + ... | ⟪ eqf , eqr ⟫ = ⟪ cong suc eqf , eqr ⟫ + decl : {m : ℕ } → 0 < m → m - k < m + decl {m} 0<m = y-x<y (<-trans a<sa k>1 ) 0<m + I : Ninduction ℕ _ F + I = record { + pnext = λ p → p - k + ; fzero = λ {m} eq → F0 m eq + ; decline = λ {m} lt → decl lt + ; ind = λ {p} prev → ind prev + } + +F<toD : {n m : ℕ} → (fc : Factor< n m) → Factor<.remain fc ≡ 0 → Dividable n m +F<toD {n} {m} record { factor = f ; remain = r ; is-factor = fa ; remain<n = _ } refl + = record { factor = f ; is-factor = fa } + +DtoF< : {n m : ℕ} → Dividable n m → 0 < n → Factor< n m +DtoF< {n} {m} record { factor = f ; is-factor = fa } 0<n = record { factor = f ; is-factor = fa ; remain = 0 ; remain<n = 0<n } + +F<to¬D : {n m nx : ℕ} → (fc : Factor< n m) → 1 < n → Factor<.remain fc ≡ suc nx → ¬ Dividable n m +F<to¬D {n} {m} fc 1<n eq div = ⊥-elim ( nat-≡< (sym (proj2 ( Factor<-inject {n} {m} 1<n fc (DtoF< div (<-trans a<sa 1<n) )))) 0<r ) where + 0<r : 0 < Factor<.remain fc + 0<r = subst ( λ k → 0 < k ) (sym eq) (s≤s z≤n) + +-- +-- we can use factor< and check Factor.remain ≡ 0 +-- Factor.remain ≡ 0 → Dividable k m +-- ¬ Factor.remain ≡ 0 → ¬ Dividable k m +-- +decD : {k m : ℕ} → k > 1 → Dec0 (Dividable k m ) +decD {k} {m} k>1 = dec0 (factor< {k} {m} k>1) where + dec0 : Factor< k m → Dec0 (Dividable k m) + dec0 fc with Factor<.remain fc in eq1 + ... | zero = yes0 record { factor = Factor<.factor fc ; is-factor = trans (cong (λ j → Factor<.factor fc * k + j) (sym eq1)) (Factor<.is-factor fc) } + ... | suc t = no0 ( λ dv → F<to¬D fc k>1 eq1 dv ) + + +