Mercurial > hg > Members > anatofuz > agda-slf

changeset 1:fa30a385957d default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Thu, 27 Feb 2020 19:23:07 +0900
parents 99728ee0d697
children
files day.agda
diffstat 1 files changed, 30 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/day.agda	Thu Feb 20 19:52:51 2020 +0900
+++ b/day.agda	Thu Feb 27 19:23:07 2020 +0900
@@ -1,5 +1,7 @@
 module day where
 
+open import Relation.Binary.PropositionalEquality
+
 data day : Set where
   monday : day
   tuesday : day
@@ -43,8 +45,8 @@
 orb true _ = true
 orb false y = y
 
-data _≡_  {a} { A : Set a} ( x : A ) : A → Set a where
-  refl : x ≡ x
+-- data _≡_  {a} { A : Set a} ( x : A ) : A → Set a where
+--  refl : x ≡ x
 
 testOrb1 : (orb true false) ≡ true
 testOrb1 = refl
@@ -97,3 +99,29 @@
 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