rnhmjoj/interlude
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

refactor commutativity proof

Browse Source
This commit is contained in:
rnhmjoj 2016-11-15 00:04:50 +01:00
parent f483b9c6c4
commit cbd12fe5b8
No known key found for this signature in database
GPG Key ID: 362BB82B7E496B7C
1 changed files with 12 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
src/Data/Nat.hs
View File

@ -121,14 +121,22 @@ switch SZ m = Refl
switch (SS n) m = cong SS (switch n m)
-- | Lemma
succ ∷ Sℕ n → Sℕ m → S (n :+ m) :≡ (n :+ S m)
succ SZ m = Refl
succ (SS n) m = cong SS (succ n m)
succ_right ∷ Sℕ n → Sℕ m → S (n :+ m) :≡ (n :+ S m)
succ_right SZ m = Refl
succ_right (SS n) m = cong SS (succ_right n m)
-- | Lemma
succ_left ∷ Sℕ n → Sℕ m → S (n :+ m) :≡ (S n :+ m)
succ_left n m = succ_right n m ∾ switch n m
-- | Relation between successor and addition
succ_plus ∷ Sℕ n → (n :+ S Z) :≡ S n
succ_plus n = switch n SZ ∾ plus_right_id (SS n)
-- | Successor of predecessor
succ_pred ∷ Sℕ (S n) → S (Pred n) :≡ n
succ_pred (SS (SS n)) = Refl
-- | Right identity of addition
plus_right_id ∷ Sℕ n → (n :+ Z) :≡ n
plus_right_id SZ = Refl
@ -143,5 +151,4 @@ plus_assoc (SS a) b c = cong SS (plus_assoc a b c)
plus_commut ∷ Sℕ n → Sℕ m → (n :+ m) :≡ (m :+ n)
plus_commut n SZ = plus_right_id n
plus_commut n (SS m) =
(sym (succ n m) ∾ cong SS (plus_commut n m)) ∾
(succ m n ∾ switch m n)
sym (succ_right n m) ∾ cong SS (plus_commut n m) ∾ succ_left m n