-- Functions.Equality_Proofs exercises -- By Xiaoning Bian module Functions.Equality_Proofs where open import Data.Nat using (ℕ; zero; suc; _≤_; z≤n; s≤s) open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _≤_; z≤n; s≤s) open import Data.List using (List; []; _∷_; _++_) open import Data.Unit using (⊤; tt) open import Data.Product using (_×_; _,_) open import Function using (_$_) data _≡_ {A : Set} (x : A) : A → Set where refl : x ≡ x infix 4 _≡_ refl' : ∀ {A} (a : A) → a ≡ a refl' a = refl sym : ∀ {A} {a b : A} → a ≡ b → b ≡ a sym refl = refl -- after pattern matching on 'refl', 'a' and 'b' coincides -- Exercise trans : ∀ {A} {a b c : A} → a ≡ b → b ≡ c → a ≡ c trans refl refl = refl -- Prove that every function is compatible with the equivalence relation (congruency): cong : ∀ {A B} {m n : A} → (f : A → B) → m ≡ n → f m ≡ f n cong f refl = refl -- Finish the ingredients of the proof that (ℕ, _+_) is a commutative monoid! +-left-identity : ∀ a → 0 + a ≡ a +-left-identity a = refl +-assoc : ∀ a b c → a + (b + c) ≡ (a + b) + c -- hint: use cong +-assoc zero b c = refl +-assoc (suc a) b c = cong suc (+-assoc a b c) -- For commutativity you need a helper function first: m+1+n≡1+m+n : ∀ m n → m + suc n ≡ suc (m + n) m+1+n≡1+m+n zero n = refl m+1+n≡1+m+n (suc m) n = cong suc (m+1+n≡1+m+n m n) +-right-identity : ∀ n → n + 0 ≡ n +-right-identity zero = refl +-right-identity (suc n) = cong suc (+-right-identity n) -- Let fromList : List ⊤ → ℕ fromList [] = zero fromList (x ∷ xs) = suc (fromList xs) toList : ℕ → List ⊤ toList zero = [] toList (suc n) = tt ∷ toList n -- Let's prove that fromList and toList are inverses of each other and that they preserve the operations _++_ and _+_! from-to : ∀ a → fromList (toList a) ≡ a from-to zero = refl from-to (suc a) = cong suc ( from-to a) to-from : ∀ a → toList (fromList a) ≡ a to-from [] = refl to-from (x ∷ a) = cong (\ (xs : List ⊤) → (x ∷ xs)) (to-from a) fromPreserves++ : ∀ (a b : List ⊤) → fromList (a ++ b) ≡ fromList a + fromList b fromPreserves++ [] b = refl fromPreserves++ (x ∷ a) b = cong suc (fromPreserves++ a b ) toPreserves+ : ∀ (a b : ℕ) → toList (a + b) ≡ toList a ++ toList b toPreserves+ zero b = refl toPreserves+ (suc a) b = cong (\ (xs : List ⊤) → tt ∷ xs) (toPreserves+ a b ) _≡⟨_⟩_ : ∀ {A : Set} (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z x ≡⟨ refl ⟩ refl = refl infixr 2 _≡⟨_⟩_ _∎ : ∀ {A : Set} (x : A) → x ≡ x x ∎ = refl infix 2 _∎ +-comm' : (n m : ℕ) → n + m ≡ m + n +-comm' zero n = sym (+-right-identity n) +-comm' (suc m) n = suc m + n ≡⟨ refl ⟩ suc (m + n) ≡⟨ cong suc (+-comm' m n) ⟩ suc (n + m) ≡⟨ sym (m+1+n≡1+m+n n m) ⟩ n + suc m ∎ distribʳ-*-+ : ∀ a b c → (a + b) * c ≡ a * c + b * c distribʳ-*-+ zero b c = refl distribʳ-*-+ (suc a) b c = c + (a + b) * c ≡⟨ cong (λ x → c + x) (distribʳ-*-+ a b c) ⟩ c + (a * c + b * c) ≡⟨ +-assoc c (a * c) (b * c) ⟩ c + a * c + b * c ∎ -- Define the following functions: *-assoc : ∀ a b c → a * (b * c) ≡ (a * b) * c *-assoc zero b c = refl *-assoc (suc a) b c = (suc a) * (b * c ) ≡⟨ refl ⟩ (b * c) + a * (b * c) ≡⟨ cong (λ x → ( b * c) + x ) (*-assoc a b c) ⟩ (b * c) + (a * b) * c ≡⟨ sym (distribʳ-*-+ b (a * b) c) ⟩ (b + a * b ) * c ∎ *-left-identity : ∀ a → 1 * a ≡ a *-left-identity zero = refl *-left-identity (suc a) = cong suc (*-left-identity a) *-right-identity : ∀ a → a * 1 ≡ a *-right-identity zero = refl *-right-identity (suc a) = cong suc (*-right-identity a) -- Commutativity: -- helper functions: n*0≡0 : ∀ n → n * 0 ≡ 0 n*0≡0 zero = refl n*0≡0 (suc n) = cong (λ x → 0 + x) (n*0≡0 n) *-suc : ∀ n m → n + n * m ≡ n * suc m *-suc zero m = refl *-suc (suc n) m = (suc n) + (suc n) * m ≡⟨ cong (λ x → (suc n) + x) (refl) ⟩ (suc n) + (m + n * m) ≡⟨ refl ⟩ suc ( n + (m + n * m)) ≡⟨ cong suc (+-assoc n m (n * m)) ⟩ suc ( n + m + n * m) ≡⟨ cong suc (cong (λ x → x + n * m ) (+-comm' n m)) ⟩ suc ( m + n + n * m) ≡⟨ cong suc (sym (+-assoc m n (n * m))) ⟩ suc ( m + (n + n * m)) ≡⟨ cong suc (cong (λ x → m + x ) ( *-suc n m ) ) ⟩ suc ( m + n * suc m) ≡⟨ refl ⟩ suc m + n * suc m ≡⟨ refl ⟩ suc n * suc m ∎ *-comm : ∀ m n → m * n ≡ n * m *-comm zero n = sym (n*0≡0 n) *-comm (suc m) n = (suc m) * n ≡⟨ refl ⟩ n + m * n ≡⟨ cong (λ x → n + x ) (*-comm m n) ⟩ n + n * m ≡⟨ *-suc n m ⟩ n * suc m ∎