Mercurial > hg > Members > anatofuz > agda-slf
view day.agda @ 1:fa30a385957d default tip
...
author | anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 27 Feb 2020 19:23:07 +0900 |
parents | 99728ee0d697 |
children |
line wrap: on
line source
module day where open import Relation.Binary.PropositionalEquality data day : Set where monday : day tuesday : day wednesday : day thursday : day friday : day saturday : day sunday : day -- ↑はただのデータ nextWeekday : day → day nextWeekday monday = tuesday nextWeekday tuesday = wednesday nextWeekday wednesday = thursday nextWeekday thursday = friday nextWeekday friday = monday nextWeekday saturday = monday nextWeekday sunday = monday hoge : day → day hoge x = nextWeekday x data bool : Set where true : bool false : bool negb : bool → bool negb true = false negb false = true andb : bool → bool → bool -- andb true true = true -- andb true false = false -- andb false true = false -- andb false false = false andb true b = b andb false _ = false orb : (x y : bool) → bool orb true _ = true orb false y = y -- data _≡_ {a} { A : Set a} ( x : A ) : A → Set a where -- refl : x ≡ x testOrb1 : (orb true false) ≡ true testOrb1 = refl data nat : Set where O : nat Succ : nat → nat pred : nat → nat pred O = O pred (Succ x) = x minustwo : nat → nat minustwo x = pred (pred x) evenb : nat → bool evenb O = true evenb (Succ O) = false evenb (Succ (Succ x)) = evenb x open import Data.Nat.Base factorial : ℕ → ℕ factorial zero = 1 factorial (suc x) = x * (factorial (x)) beqNat : ℕ → ℕ → bool beqNat zero zero = true beqNat zero (suc y) = false beqNat (suc x) zero = false beqNat (suc x) (suc y) = beqNat x y -- beqNat x y with x | y -- beqNat x y | zero | zero = true -- beqNat x y | zero | suc a = false -- beqNat x y | suc z | zero = false -- beqNat x y | suc z | suc a = beqNat z a open import Data.Nat.Properties open import Data.Empty n+0 : ( n : ℕ ) → ( n + 0 ) ≡ n n+0 zero = refl n+0 (suc x) rewrite ( +-comm (suc x) 0 ) = refl andbTrueElim2 : ( b c : bool ) → (andb b c ) ≡ true → c ≡ true -- andbTrueElim2 true c d with d -- andbTrueElim2 true .true d | refl = refl andbTrueElim2 _ true d = refl andbTrueElim2 false false () andbTrueElim2 true false () mult0r : ( n : ℕ ) → ( n * zero) ≡ zero mult0r zero = refl -- mult0r (suc n) = mult0r n mult0r (suc n) rewrite ( *-comm (suc n) 0 ) = refl double : (n : ℕ ) → ℕ double zero = zero double (suc x) = suc ( suc ( double x)) sucEqPlus1 : ( n : ℕ ) → (n + 1) ≡(suc n) sucEqPlus1 x rewrite (+-comm x 1 ) = refl plusNSm : (n m : ℕ ) → (suc ( n + m)) ≡ (n + suc (m)) plusNSm zero zero = refl plusNSm zero (suc y) = refl plusNSm (suc x) zero rewrite sucEqPlus1 x | n+0 x = refl plusNSm (suc x) (suc y) = cong (suc) (plusNSm x (suc y)) doublePlus : (n : ℕ ) → (double n) ≡ (n + n) doublePlus zero = refl doublePlus (suc n) rewrite (doublePlus n) | plusNSm n n = refl plusSwap : ( n m p : ℕ ) → ( n + (m + p)) ≡ ( m + (n + p)) plusSwap zero y z = refl plusSwap (suc x) y z rewrite sym (plusNSm (y) (x + z)) | plusSwap x y z = refl