Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1266:a27f28dbed87
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 21 Mar 2023 11:19:15 +0900 |
| parents | 48d37da98331 |
| children | 0d278b809c01 |
| files | src/generic-filter.agda src/nat.agda |
| diffstat | 2 files changed, 717 insertions(+), 79 deletions(-) [+] |
line wrap: on
line diff
--- a/src/generic-filter.agda Mon Mar 20 08:16:10 2023 +0900 +++ b/src/generic-filter.agda Tue Mar 21 11:19:15 2023 +0900 @@ -112,13 +112,6 @@ open PDN ----- --- Generic Filter on Power P for HOD's Countable Ordinal (G ⊆ Power P ≡ G i.e. ℕ → P → Set ) --- --- p 0 ≡ ∅ --- p (suc n) = if ∃ q ∈ M ∧ p n ⊆ q → q (by axiom of choice) ( q = * ( ctl→ n ) ) ---- else p n - P∅ : {P : HOD} → odef (Power P) o∅ P∅ {P} = subst (λ k → odef (Power P) k ) ord-od∅ (lemma o∅ o∅≡od∅) where lemma : (x : Ordinal ) → * x ≡ od∅ → odef (Power P) (& od∅) @@ -131,7 +124,7 @@ gf05 {a} {b} {x} (case2 bx) nax nbx = nbx bx open import Data.Nat.Properties -open import nat +open import nat hiding ( exp ) p-monotonic1 : (L p : HOD ) (C : CountableModel ) → {n : ℕ} → (* (find-p L C n (& p))) ⊆ (* (find-p L C (suc n) (& p))) p-monotonic1 L p C {n} {x} with is-o∅ (& (PGHOD n L C (find-p L C n (& p)))) @@ -181,6 +174,13 @@ genf : ⊆-Ideal {L} {P} LP generic : (D : Dense L ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ ⊆-Ideal.ideal genf ) ≡ od∅ ) +---- +-- Generic Filter on L ⊆ Power P from HOD's Countable Ordinal (G ⊆ Power P ≡ G i.e. ℕ → P → Set ) +-- +-- p 0 ≡ ∅ +-- p (suc n) = if ∃ q ∈ M ∧ p n ⊆ q → q (by axiom of choice) ( q = * ( ctl→ n ) ) +--- else p n + P-GenericFilter : (P L p0 : HOD ) → (LP : L ⊆ Power P) → L ∋ p0 → (C : CountableModel ) → GenericFilter {L} {P} LP ( ctl-M C ) P-GenericFilter P L p0 L⊆PP Lp0 C = record { @@ -192,10 +192,10 @@ record { gr = gr ; pn<gr = λ y qy → pn<gr y (gf00 qy) ; x∈PP = Lq } where gf00 : {y : Ordinal } → odef (* (& q)) y → odef (* (& p)) y gf00 {y} qy = subst (λ k → odef k y ) (sym *iso) (q⊆p (subst (λ k → odef k y) *iso qy )) - Lfp : (i : ℕ ) → odef L (find-p L C i (& p0)) - Lfp zero = Lp0 - Lfp (suc i) with is-o∅ ( & ( PGHOD i L C (find-p L C i (& p0))) ) - ... | yes y = Lfp i + Lan : (i : ℕ ) → odef L (find-p L C i (& p0)) + Lan zero = Lp0 + Lan (suc i) with is-o∅ ( & ( PGHOD i L C (find-p L C i (& p0))) ) + ... | yes y = Lan i ... | no not = proj1 ( ODC.x∋minimal O ( PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq))) exp1 : {p q : HOD} → (ip : PDHOD L p0 C ∋ p) → (ip : PDHOD L p0 C ∋ q) → Exp2 (PDHOD L p0 C) p q exp1 {p} {q} record { gr = pgr ; pn<gr = ppn ; x∈PP = PPp } @@ -204,7 +204,7 @@ Pq = record { gr = qgr ; pn<gr = qpn ; x∈PP = PPq } gf17 : {q : HOD} → (Pq : PDHOD L p0 C ∋ q ) → PDHOD L p0 C ∋ * (find-p L C (gr Pq) (& p0)) gf17 {q} Pq = record { gr = PDN.gr Pq ; pn<gr = λ y qq → subst (λ k → odef (* k) y) &iso qq - ; x∈PP = subst (λ k → odef L k ) (sym &iso) (Lfp (PDN.gr Pq)) } + ; x∈PP = subst (λ k → odef L k ) (sym &iso) (Lan (PDN.gr Pq)) } gf01 : Exp2 (PDHOD L p0 C) p q gf01 with <-cmp pgr qgr ... | tri< a ¬b ¬c = record { exp = * (find-p L C (gr Pq) (& p0)) ; I∋exp = gf17 Pq ; p⊆exp = λ px → gf15 _ px @@ -226,16 +226,6 @@ fdense D MD eq0 = ⊥-elim ( ∅< {Dense.dense D ∩ PDHOD L p0 C} fd01 (≡od∅→=od∅ eq0 )) where open Dense open Expansion - fd09 : (i : ℕ ) → odef L (find-p L C i (& p0)) - fd09 zero = Lp0 - fd09 (suc i) with is-o∅ ( & ( PGHOD i L C (find-p L C i (& p0))) ) - ... | yes _ = fd09 i - ... | no not = fd17 where - fd19 = ODC.minimal O ( PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq)) - fd18 : PGHOD i L C (find-p L C i (& p0)) ∋ fd19 - fd18 = ODC.x∋minimal O (PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq)) - fd17 : odef L ( & (ODC.minimal O ( PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq))) ) - fd17 = proj1 fd18 an : ℕ an = ctl← C (& (dense D)) MD pn : Ordinal @@ -250,7 +240,7 @@ fd07 with is-o∅ ( & ( PGHOD an L C (find-p L C an (& p0))) ) ... | yes y = ⊥-elim ( ¬x<0 ( _==_.eq→ fd10 fd21 ) ) where L∋pn : L ∋ * (find-p L C an (& p0)) - L∋pn = subst (λ k → odef L k) (sym &iso) (fd09 an ) + L∋pn = subst (λ k → odef L k) (sym &iso) (Lan an ) ex = has-exp D L∋pn L∋df : L ∋ ( exp ex ) L∋df = (d⊆P D) (D∋exp ex) @@ -269,14 +259,14 @@ fd27 : odef (dense D) (& fd29) fd27 = subst (λ k → odef k (& fd29)) (sym d=an) (proj1 (proj2 fd28)) fd03 : odef (PDHOD L p0 C) pn+1 - fd03 = record { gr = suc an ; pn<gr = λ y lt → lt ; x∈PP = fd09 (suc an)} + fd03 = record { gr = suc an ; pn<gr = λ y lt → lt ; x∈PP = Lan (suc an)} fd01 : (dense D ∩ PDHOD L p0 C) ∋ (* pn+1) fd01 = ⟪ subst (λ k → odef (dense D) k ) (sym &iso) fd07 , subst (λ k → odef (PDHOD L p0 C) k) (sym &iso) fd03 ⟫ open GenericFilter -- open Filter -record NotCompatible (L p : HOD ) (L∋a : L ∋ p ) : Set (Level.suc (Level.suc n)) where +record Incompatible (L p : HOD ) (L∋a : L ∋ p ) : Set (Level.suc (Level.suc n)) where field q r : HOD Lq : L ∋ q @@ -288,21 +278,20 @@ lemma232 : (P L p0 : HOD ) → (LPP : L ⊆ Power P) → (Lp0 : L ∋ p0 ) → (C : CountableModel ) → ctl-M C ∋ L - → ( {p : HOD} → (Lp : L ∋ p ) → NotCompatible L p Lp ) + → ( {p : HOD} → (Lp : L ∋ p ) → Incompatible L p Lp ) → ¬ ( ctl-M C ∋ ⊆-Ideal.ideal (genf ( P-GenericFilter P L p0 LPP Lp0 C ))) -lemma232 P L p0 LPP Lp0 C ML NC MF = ¬rgf∩D=0 record { eq→ = λ {x} rgf∩D → ⊥-elim( proj2 (proj1 rgf∩D) (proj2 rgf∩D)) - ; eq← = λ lt → ⊥-elim (¬x<0 lt) } where +lemma232 P L p0 LPP Lp0 C ML NC MF = ¬G∩D=0 D∩G=0 where PG = P-GenericFilter P L p0 LPP Lp0 C GF = genf PG - rgf = ⊆-Ideal.ideal (genf PG) + G = ⊆-Ideal.ideal (genf PG) M = ctl-M C D : HOD - D = L ＼ rgf + D = L ＼ G D<M : & D o< & (ctl-M C) D<M = ordtrans≤-< (⊆→o≤ proj1 ) (odef< ML) M∋DM : M ∋ (D ∩ M ) M∋DM = is-model C D D<M - -- G⊆M : rgf ⊆ M + -- G⊆M : G ⊆ M -- G⊆M {x} rx = TC C ML (subst (λ k → odef k x) (sym *iso) (⊆-Ideal.i⊆L GF rx)) -- D⊆M : D ⊆ M -- D⊆M {x} dx = TC C ML (subst (λ k → odef k x) (sym *iso) (proj1 dx)) @@ -319,25 +308,28 @@ exp : {p : HOD} → (Lp : L ∋ p) → Expansion p D exp {p} Lp = exp1 where q : HOD - q = NotCompatible.q (NC Lp) + q = Incompatible.q (NC Lp) r : HOD - r = NotCompatible.r (NC Lp) + r = Incompatible.r (NC Lp) Lq : L ∋ q - Lq = NotCompatible.Lq (NC Lp) + Lq = Incompatible.Lq (NC Lp) Lr : L ∋ r - Lr = NotCompatible.Lr (NC Lp) + Lr = Incompatible.Lr (NC Lp) exp1 : Expansion p D - exp1 with ODC.p∨¬p O (rgf ∋ q) - ... | case2 ngq = record { exp = q ; D∋exp = ⟪ Lq , ngq ⟫ ; p⊆exp = NotCompatible.p⊆q (NC Lp)} - ... | case1 gq with ODC.p∨¬p O (rgf ∋ r) - ... | case2 ngr = record { exp = r ; D∋exp = ⟪ Lr , ngr ⟫ ; p⊆exp = NotCompatible.p⊆r (NC Lp)} - ... | case1 gr = ⊥-elim ( NotCompatible.¬compat (NC Lp) ex2 Le ⟪ q⊆ex2 , r⊆ex2 ⟫ ) where + exp1 with ODC.p∨¬p O (G ∋ q) + ... | case2 ngq = record { exp = q ; D∋exp = ⟪ Lq , ngq ⟫ ; p⊆exp = Incompatible.p⊆q (NC Lp)} + ... | case1 gq with ODC.p∨¬p O (G ∋ r) + ... | case2 ngr = record { exp = r ; D∋exp = ⟪ Lr , ngr ⟫ ; p⊆exp = Incompatible.p⊆r (NC Lp)} + ... | case1 gr = ⊥-elim ( Incompatible.¬compat (NC Lp) ex2 Le ⟪ q⊆ex2 , r⊆ex2 ⟫ ) where ex2 = Exp2.exp (⊆-Ideal.exp GF gq gr) Le = ⊆-Ideal.i⊆L GF (Exp2.I∋exp (⊆-Ideal.exp GF gq gr)) q⊆ex2 = Exp2.p⊆exp (⊆-Ideal.exp GF gq gr) r⊆ex2 = Exp2.q⊆exp (⊆-Ideal.exp GF gq gr) - ¬rgf∩D=0 : ¬ ( (D ∩ rgf ) =h= od∅ ) - ¬rgf∩D=0 eq = generic PG DD M∋D (==→o≡ eq) + ¬G∩D=0 : ¬ ( (D ∩ G ) =h= od∅ ) + ¬G∩D=0 eq = generic PG DD M∋D (==→o≡ eq) + D∩G=0 : (D ∩ G ) =h= od∅ -- because D = L ＼ G + D∩G=0 = record { eq→ = λ {x} G∩D → ⊥-elim( proj2 (proj1 G∩D) (proj2 G∩D)) + ; eq← = λ lt → ⊥-elim (¬x<0 lt) } -- -- P-Generic Filter defines a countable model D ⊂ C from P @@ -372,11 +364,27 @@ z=valy : z ≡ & (val y (val< is-val)) z<x : z o< x -val : (x : HOD) {P L M : HOD } {LP : L ⊆ Power P} - → (G : GenericFilter {L} {P} LP M ) - → HOD +val : (x : HOD) → (G : HOD) → HOD val x G = TransFinite {λ x → HOD } ind (& x) where - ind : (x : Ordinal) → ((y : Ordinal) → y o< x → HOD) → HOD - ind x valy = record { od = record { def = λ z → valS (⊆-Ideal.ideal (genf G)) x z valy } ; odmax = x ; <odmax = v02 } where - v02 : {z : Ordinal} → valS (⊆-Ideal.ideal (genf G)) x z valy → z o< x + ind : (x : Ordinal) → (valy : (y : Ordinal) → y o< x → HOD) → HOD + ind x valy = record { od = record { def = λ z → valS G x z valy } ; odmax = x ; <odmax = v02 } where + v02 : {z : Ordinal} → valS G x z valy → z o< x v02 {z} lt = valS.z<x lt + +TCS : (G : HOD) → Set (Level.suc n) +TCS G = {x y : HOD} → G ∋ x → x ∋ y → G ∋ y + +val∋→∋p : {G : HOD} → (TCS G) → {x y : HOD} → {p : HOD} → G ∋ p → ( val x G ∋ val y G ) → x ∋ < y , p > +val∋→∋p = ? + +p∋→val∋ : {G : HOD} → (TCS G) → {x y : HOD} → {p : HOD} → G ∋ p → x ∋ < y , p > → ( val x G ∋ val y G ) +p∋→val∋ {G} TG {x} {y} {p} Gp = subst (λ k → k ∋ < y , p > → ( val k G ∋ val y G ) ) *iso ( + TransFinite0 {λ x → ( * x ) ∋ < y , p > → ( val (* x) G ∋ val y G )} ? (& x) ) where + pind : (x : Ordinal) → ((z : Ordinal) → z o< x → ( * z ) ∋ < y , p > → val (* z) G ∋ val y G) → + (* x ) ∋ < y , p > → val (* x) G ∋ val y G + pind x prev xyp = ? + -- subst (λ k → odef ( TransFinite (generic-filter.ind (* x) G) (& (* x))) (& (val y G))) ? ( + -- record { y = ? ; p = ? ; G∋p = ? ; is-val = ? ; z=valy = ? ; z<x = ? } ) + + +
--- a/src/nat.agda Mon Mar 20 08:16:10 2023 +0900 +++ b/src/nat.agda Tue Mar 21 11:19:15 2023 +0900 @@ -1,53 +1,683 @@ +{-# OPTIONS --allow-unsolved-metas #-} module nat where -open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) +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 ) - -nat-<> : { x y : Nat } → x < y → y < x → ⊥ +nat-<> : { x y : ℕ } → x < y → y < x → ⊥ nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x -nat-≤> : { x y : Nat } → x ≤ y → y < x → ⊥ +nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥ nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x -nat-<≡ : { x : Nat } → x < x → ⊥ +nat-<≡ : { x : ℕ } → x < x → ⊥ nat-<≡ (s≤s lt) = nat-<≡ lt -nat-≡< : { x y : Nat } → x ≡ y → x < y → ⊥ +nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥ nat-≡< refl lt = nat-<≡ lt -¬a≤a : {la : Nat} → Suc la ≤ la → ⊥ +¬a≤a : {la : ℕ} → suc la ≤ la → ⊥ ¬a≤a (s≤s lt) = ¬a≤a lt -a<sa : {la : Nat} → la < Suc la -a<sa {Zero} = s≤s z≤n -a<sa {Suc la} = s≤s a<sa +a<sa : {la : ℕ} → la < suc la +a<sa {zero} = s≤s z≤n +a<sa {suc la} = s≤s a<sa -<to≤ : {x y : Nat } → 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) +=→¬< : {x : ℕ } → ¬ ( x < x ) +=→¬< {zero} () +=→¬< {suc x} (s≤s lt) = =→¬< lt -=→¬< : {x : Nat } → ¬ ( x < x ) -=→¬< {Zero} () -=→¬< {Suc x} (s≤s lt) = =→¬< lt - ->→¬< : {x y : Nat } → (x < y ) → ¬ ( y < x ) +>→¬< : {x y : ℕ } → (x < y ) → ¬ ( y < x ) >→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x -<-∨ : { x y : Nat } → 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 < 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) + +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 ) + +-- _*_ : ℕ → ℕ → ℕ +-- _*_ 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 | inspect div2 x +... | ⟪ x1 , true ⟫ | record { eq = eq1 } = 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 ⟫ | record { eq = eq1 } = 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 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) + +minus : (a b : ℕ ) → ℕ +minus a zero = a +minus zero (suc b) = zero +minus (suc a) (suc b) = minus a b + +_-_ = minus + +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 {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) + +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-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 : {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 : {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-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-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 ≤ 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) + +<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) + +<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) + +<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) + +refl-≤s : {x : ℕ } → x ≤ suc x +refl-≤s {zero} = z≤n +refl-≤s {suc x} = s≤s (refl-≤s {x}) + +refl-≤ : {x : ℕ } → x ≤ x +refl-≤ {zero} = z≤n +refl-≤ {suc x} = s≤s (refl-≤ {x}) + +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) + +≤→= : {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 ) + +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 + +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) + +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 + + +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+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} 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→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}) + +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ʳ-< (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 -max : (x y : Nat) → Nat -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 ) +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 ) + +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} {.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 + +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 (s≤s lt) = lt + +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< (s≤s a) ¬b ¬c = f-induction0 p x 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→≤ (s≤s lt) = lt +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< (s≤s a) ¬b ¬c = f-induction0 p x 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 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 = (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 + +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 | inspect Dividable.factor d +... | zero | record { eq = eq1 } = ⊥-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 + +decD : {k m : ℕ} → k > 1 → Dec (Dividable k m ) +decD {k} {m} k>1 = n-induction {_} {_} {ℕ} {λ m → Dec (Dividable k m ) } F I m where + F : ℕ → ℕ + F m = m + F0 : ( m : ℕ ) → F (m - k) ≡ 0 → Dec (Dividable k m ) + F0 0 eq = yes record { factor = 0 ; is-factor = refl } + F0 (suc m) eq with <-cmp k (suc m) + ... | tri< a ¬b ¬c = yes record { factor = 1 ; is-factor = + subst (λ g → 1 * k + 0 ≡ g ) (sym (i-j=0→i=j (<to≤ a) eq )) div1*k+0=k } -- (suc m - k) ≡ 0 → k ≡ suc m, k ≤ suc m + ... | tri≈ ¬a refl ¬c = yes record { factor = 1 ; is-factor = div1*k+0=k } + ... | tri> ¬a ¬b c = no ( λ d → ⊥-elim (div<k k>1 (s≤s z≤n ) c d) ) + 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=)) ) + I : Ninduction ℕ _ F + I = record { + pnext = λ p → p - k + ; fzero = λ {m} eq → F0 m eq + ; decline = λ {m} lt → decl lt + ; ind = λ {p} prev → ind p prev + } +