module gy3 where import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; cong; sym; trans) open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎) open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_) {- data ℕ : Set where -- \bn zero : ℕ suc : ℕ → ℕ -- \-> {-# BUILTIN NATURAL ℕ #-} _+_ : ℕ → ℕ → ℕ zero + b = b -- pattern matching: C-c C-c suc a + b = suc (a + b) infixl 6 _+_ -} -- _+_ kommutativ felcsoport -- (a : ℕ) → (b : ℕ) → (c : ℕ) → ass : (a b c : ℕ) → (a + b) + c ≡ a + (b + c) ass zero b c = refl ass (suc a) b c = cong suc (ass a b c) idl : (a : ℕ) → zero + a ≡ a idl a = refl idr : (a : ℕ) → a + zero ≡ a idr zero = refl idr (suc a) = cong suc (idr a) -- idr (suc a) = ? lemm : (a b : ℕ) → suc a + b ≡ a + suc b lemm a b = {!!} comm : (a b : ℕ) → a + b ≡ b + a comm zero b = sym (idr b) comm (suc a) b = trans (cong suc (comm a b)) (lemm b a) {- _*_ : Nat → Nat → Nat zero * m = zero suc n * m = m + n * m -} idl* : (a : ℕ) → 1 * a ≡ a idl* a = {!!} idr* : (a : ℕ) → a * 1 ≡ a idr* a = {!!} nulll : (a : ℕ) → 0 * a ≡ 0 nulll a = {!!} nullr : (a : ℕ) → a * 0 ≡ 0 nullr a = {!!} -- this comes next, using equational reasoning distribl : (a b c : ℕ) → a * (b + c) ≡ a * b + a * c distribl zero b c = refl distribl (suc a) b c = trans (cong (b + c +_) (distribl a b c)) {!!} distribr : (a b c : ℕ) → (a + b) * c ≡ a * c + b * c distribr a b c = {!!} ass* : (a b c : ℕ) → a * (b * c) ≡ (a * b) * c ass* zero b c = refl ass* (suc a) b c = trans (cong (b * c +_) (ass* a b c)) {!!} comm* : (a b : ℕ) → a * b ≡ b * a comm* a b = {!!}