Last active
November 2, 2022 01:40
-
-
Save beala/9a53654742f9645fbc961b7015f80abb to your computer and use it in GitHub Desktop.
Some proofs of basic properties of addition and equality in Agda. Update: Now lists and multiplication!
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Nats where | |
open import Agda.Primitive | |
data Equal {a : Level} {X : Set a} : X → X → Set a where | |
equal : {x : X} → Equal x x | |
{-# BUILTIN EQUALITY Equal #-} | |
_==_ : _ | |
_==_ = Equal | |
data ℕ : Set where | |
zero : ℕ | |
suc : ℕ → ℕ | |
{-# BUILTIN NATURAL ℕ #-} | |
{-# BUILTIN REFL equal #-} | |
_+_ : ℕ → ℕ → ℕ | |
zero + y = y | |
suc x + y = suc (x + y) | |
{- Proof of transitivity of equality -} | |
transitive : (a b c : ℕ) → a == b → b == c → a == c | |
transitive zero zero zero p1 p2 = equal | |
transitive zero zero (suc c) equal () | |
transitive zero (suc b) c () p2 | |
transitive (suc a) .(suc a) .(suc a) equal equal = equal | |
symmetry : (a b : ℕ) → a == b → b == a | |
symmetry a .a equal = equal | |
reflex : (a : ℕ) → a == a | |
reflex a = equal | |
{- Proof of commutativity of addition -} | |
x+0 : (a : ℕ) → (a + 0) == a | |
x+0 zero = equal | |
x+0 (suc a) rewrite x+0 a = equal | |
commute' : (a b : ℕ) → (a + suc b) == suc (a + b) | |
commute' zero b = equal | |
commute' (suc a) b rewrite commute' a b = equal | |
commute : (a b : ℕ) → (a + b) == (b + a) | |
commute zero b rewrite x+0 b = equal | |
commute (suc a) b rewrite commute' b a | commute a b = equal | |
{- Applying the commutativity proof: x + 1 == 1 + x -} | |
x+1 : (x : ℕ) → (x + 1) == (1 + x) | |
x+1 x = commute x 1 | |
{- Proof of associativity of addition -} | |
assoc : (a b c : ℕ) → ((a + b) + c) == (a + (b + c)) | |
assoc zero b c = equal | |
assoc (suc a) b c rewrite assoc a b c = equal | |
_*_ : ℕ → ℕ → ℕ | |
zero * _ = zero | |
suc a * b = b + (b * a) | |
a*0 : (a : ℕ) → (a * 0) == 0 | |
a*0 zero = equal | |
a*0 (suc a) rewrite a*0 a = equal | |
{- Proof that 1 is identity element of multiply over nats -} | |
a*1 : (a : ℕ) → (a * 1) == a | |
a*1 zero = equal | |
a*1 (suc a) rewrite a*1 a | a*0 a | x+0 a = equal | |
{- | |
commute* : (a b : ℕ) → (a * b) == (b * a) | |
commute* zero b rewrite a*0 b = equal | |
commute* (suc a) b rewrite commute* a b = {!!} | |
-} | |
infixr 40 _::_ | |
data List (A : Set) : Set where | |
nil : List A | |
_::_ : A → List A → List A | |
id : {ℓ : Level} → {A : Set ℓ} → A → A | |
id a = a | |
map : {A B : Set} → (A → B) → List A → List B | |
map f nil = nil | |
map f (x :: l) = f x :: map f l | |
_++_ : {A : Set} → List A → List A → List A | |
nil ++ r = r | |
x :: l ++ r = x :: (l ++ r) | |
{- Proof of list append associativity -} | |
listAssoc : {A : Set} → (a b c : List A) → (a ++ (b ++ c)) == ((a ++ b) ++ c) | |
listAssoc nil b c = equal | |
listAssoc (x :: a) b c rewrite listAssoc (a) b c = equal | |
{- Proof of the first functor law: map id == id -} | |
mapIdFunctorLaw : {A : Set} → (a : List A) → (map id a) == (id a) | |
mapIdFunctorLaw nil = equal | |
mapIdFunctorLaw (x :: l) rewrite mapIdFunctorLaw l = equal | |
_∘_ : {A B C : Set} → (B -> C) → (A -> B) -> A -> C | |
_∘_ g f a = g (f a) | |
{- Proof of the second functor law: map g ∘ f == map g ∘ map f -} | |
mapComposeLaw : {A B C : Set} → (a : List A) → (f : A → B) → (g : B → C) → map (g ∘ f) a == (map g ∘ map f) a | |
mapComposeLaw nil f g = equal | |
mapComposeLaw (x :: l) f g rewrite mapComposeLaw l f g = equal |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Hi, I noticed that is no long possible to use
{-# BUILTIN REFL equal #-}
.Agda says:
To fix it, is just remove the line xD