-- contains Unicode characters; download, don't cut-and-paste from browser module nat where open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; trans) open import Data.Nat using (ℕ; suc; zero) open import Data.Product using (∃; ∃-syntax) _+_ : ℕ → ℕ → ℕ zero + m = m suc n + m = suc (n + m) infixl 6 _+_ two-plus-two-is-four : 2 + 2 ≡ 4 two-plus-two-is-four = refl two-plus : ∀ (n : ℕ) → (2 + n) ≡ suc (suc n) two-plus n = refl -- plus-zero : ∀ (n : ℕ) → (n + zero) ≡ n -- option 1: prove eq-elim/subst, then use it -- option 2: use cong -- cong : {A B : Set} → {x y : A} → (f : A → B) → x ≡ y → f x ≡ f y plus-zero₀ : ∀ (n : ℕ) → (n + zero) ≡ n plus-zero₀ zero = refl plus-zero₀ (suc n) = cong suc (plus-zero₀ n) -- option 3: write a helper function plus-zero₁ : ∀ (n : ℕ) → (n + zero) ≡ n plus-zero₁ zero = refl {- does not work, must generalize plus-zero‴ (suc n) = helper (plus-zero‴ n) where helper : {n : ℕ} → (n + zero) ≡ n → suc (n + zero) ≡ suc n helper e = {!e!} -} plus-zero₁ (suc n) = helper (n + zero) (plus-zero₁ n) where helper : {n : ℕ} → (w : ℕ) → w ≡ n → suc w ≡ suc n helper w refl = refl -- option 4: use 'with' notation, shorthand for option 3 (in general) plus-zero₂ : ∀ (n : ℕ) → (n + zero) ≡ n plus-zero₂ zero = refl plus-zero₂ (suc n) with n + zero | plus-zero₂ n ... | .n | refl = refl -- option 5: use 'rewrite', shorthand for option 4 (specifically) plus-zero : ∀ (n : ℕ) → (n + zero) ≡ n plus-zero zero = refl plus-zero (suc n) rewrite plus-zero n = refl -- exercises plus-suc : ∀ (n m : ℕ) → (n + suc m) ≡ suc (n + m) plus-suc = {!!} plus-comm : ∀ (n m : ℕ) → (n + m) ≡ (m + n) plus-comm = {!!} plus-assoc : ∀ (i j k : ℕ) → (i + (j + k)) ≡ ((i + j) + k) plus-assoc = {!!} -- Material from ordering.agda but in standard library open import Data.Nat using (_≤_; z≤n; s≤s; _<_) open import Data.Nat.Properties using (≤-refl; ≤-trans) {- data _≤_ : ℕ → ℕ → Set where z≤n : ∀ {n : ℕ} → zero ≤ n s≤s : ∀ {m n : ℕ} → m ≤ n → suc m ≤ suc n -} ≤-antisym : ∀ {m n} → m ≤ n → n ≤ m → m ≡ n ≤-antisym z≤n z≤n = refl ≤-antisym (s≤s p) (s≤s q) = cong suc (≤-antisym p q) -- could also use rewrite -- Coq's definition of less-than-or-equal-to data _≤₁_ : ℕ → ℕ → Set where ≤₁-refl : ∀ {n : ℕ} → n ≤₁ n ≤₁-suc : ∀ {m n : ℕ} → m ≤₁ n → m ≤₁ suc n -- +-based definition data _≤₊_ : ℕ → ℕ → Set where ∃d : ∀ (d m n : ℕ) → d + m ≡ n → m ≤₊ n -- Exercise: all three are equivalent. -- Some directions are easiest to prove using transitivity of →. -- You may rearrange these. ≤₁→≤ : ∀ (m n : ℕ) → m ≤₁ n → m ≤ n ≤₁→≤ = {!!} ≤→≤₁ : ∀ (m n : ℕ) → m ≤ n → m ≤₁ n ≤→≤₁ = {!!} ≤→≤₊ : ∀ (m n : ℕ) → m ≤ n → m ≤₊ n ≤→≤₊ = {!!} ≤₊→≤ : ∀ (m n : ℕ) → m ≤₊ n → m ≤ n ≤₊→≤ = {!!} ≤₁→≤₊ : ∀ (m n : ℕ) → m ≤₁ n → m ≤₊ n ≤₁→≤₊ = {!!} ≤₊→≤₁ : ∀ (m n : ℕ) → m ≤₊ n → m ≤₁ n ≤₊→≤₁ = {!!} -- divisibility infix 4 _∣_ data _∣_ : ℕ → ℕ → Set where 0|0 : zero ∣ zero zero : ∀ {d} → suc d ∣ zero plus : ∀ {d m} → suc d ∣ m → suc d ∣ suc (d + m) -- suc d + m div-refl : ∀ {a} → a ∣ a div-refl {zero} = 0|0 div-refl {suc a} with plus {a} zero ... | r rewrite plus-zero a = r -- exercises div-plus : ∀ {a b c} → a ∣ b → a ∣ c → a ∣ b + c div-plus = {!!} div-trans : ∀ {a b c} → a ∣ b → b ∣ c → a ∣ c div-trans = {!!} m≤m+n : ∀ m n → m ≤ m + n m≤m+n = {!!} m≤n+m : ∀ m n → m ≤ n + m m≤n+m = {!!} m+n≡k→m≤k : ∀ {m n k} → m + n ≡ k → m ≤ k m+n≡k→m≤k = {!!} m+n≤m→m≡0 : ∀ m n → m + n ≤ m → n ≡ 0 m+n≤m→m≡0 = {!!} div-le : ∀ m n → m ∣ suc n → m ≤ suc n div-le = {!!} div-antisym : ∀ m n → m ∣ n → n ∣ m → m ≡ n div-antisym = {!!} -- "monus" _∸_ : ℕ → ℕ → ℕ zero ∸ n = zero suc m ∸ zero = suc m suc m ∸ suc n = m ∸ n infixl 6 _∸_ -- exercises a∸a≡0 : ∀ a → a ∸ a ≡ zero a∸a≡0 = {!!} a∸0≡a : ∀ a → a ∸ zero ≡ a a∸0≡a = {!!} b+a∸b+c≡a∸c : ∀ a b c → b + a ∸ (b + c) ≡ a ∸ c b+a∸b+c≡a∸c = {!!} a+b∸c+b≡a∸c : ∀ a b c → a + b ∸ (c + b) ≡ a ∸ c a+b∸c+b≡a∸c = {!!} div-mon : ∀ {a b c} → a ∣ b → a ∣ c → a ∣ b ∸ c div-mon = {!!} div-plus-right : ∀ {a b c} → a ∣ (b + c) → a ∣ c → a ∣ b div-plus-right = {!!} div-plus-left : ∀ {a b c} → a ∣ (b + c) → a ∣ b → a ∣ c div-plus-left = {!!} data DivCert : ℕ → ℕ → Set where zspec : DivCert 0 0 spec : ∀ {pd n} w r → w + r ≡ n → (suc pd) ∣ w → r < (suc pd) → DivCert (suc pd) n record DivHInv (pd n wh j k x : ℕ) : Set where constructor invs field fl : k + j ≡ pd eq : wh + (k + x) ≡ n dv : (suc pd) ∣ wh bd : k ≤ pd div-helper : ∀ (pd n wh j k x : ℕ) → DivHInv pd n wh j k x → DivCert (suc pd) n div-helper pd n wh j k zero (invs fl eq dv bd) rewrite plus-zero k = spec wh k eq dv (s≤s bd) div-helper pd n wh zero k (suc x) (invs fl eq dv bd) rewrite plus-suc k x | plus-zero k | plus-assoc wh (suc k) x | plus-comm wh (suc k) | fl = div-helper pd n (suc pd + wh) pd zero x (invs refl eq (plus dv) z≤n) div-helper pd n wh (suc j) k (suc x) (invs fl eq dv bd) rewrite plus-suc k j | plus-suc k x = div-helper pd n wh j (suc k) x (invs fl eq dv (m+n≡k→m≤k fl)) div-alg : ∀ (d n : ℕ) → 0 < d → DivCert d n div-alg zero zero p = zspec div-alg (suc d) n p = div-helper d n 0 d 0 n (invs refl refl zero z≤n) data cdiv (m n k : ℕ) : Set where tok : (∀ d → d ∣ m → d ∣ n → d ∣ k) → cdiv m n k -- exercises cdiv-m : ∀ {m n} → cdiv m n m cdiv-m = {!!} cdiv-n : ∀ {m n} → cdiv m n n cdiv-n = {!!} cdiv-cancel-right : ∀ {m n j k} → cdiv m n (j + k) → cdiv m n k → cdiv m n j cdiv-cancel-right = {!!} cdiv-cancel-left : ∀ {m n j k} → cdiv m n (j + k) → cdiv m n j → cdiv m n k cdiv-cancel-left = {!!} cdiv-plus-left : ∀ {m n k} → cdiv m (m + n) k → cdiv m n k cdiv-plus-left = {!!} cdiv-plus-right : ∀ {m n k} → cdiv (n + m) n k → cdiv m n k cdiv-plus-right = {!!} record GCD (m n : ℕ) : Set where constructor ans field g : ℕ g|m : g ∣ m g|n : g ∣ n greatest : cdiv m n g -- ∀ d → d ∣ m → d ∣ n → d ∣ g