Mercurial > hg > Papers > 2020 > ryokka-master
diff paper/src/Reasoning.agda @ 2:c7acb9211784
add code, figure. and paper fix content
author | ryokka |
---|---|
date | Mon, 27 Jan 2020 20:41:36 +0900 |
parents | |
children |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/Reasoning.agda Mon Jan 27 20:41:36 2020 +0900 @@ -0,0 +1,21 @@ +open import Relation.Binary.PropositionalEquality +open import nat +open import nat_add +open ≡-Reasoning + +module nat_add_sym_reasoning where + +addToRight : (n m : Nat) -> S (n + m) ≡ n + (S m) +addToRight O m = refl +addToRight (S n) m = cong S (addToRight n m) + +addSym : (n m : Nat) -> n + m ≡ m + n +addSym O O = refl +addSym O (S m) = cong S (addSym O m) +addSym (S n) O = cong S (addSym n O) +addSym (S n) (S m) = begin + (S n) + (S m) ≡⟨ refl ⟩ + S (n + S m) ≡⟨ cong S (addSym n (S m)) ⟩ + S ((S m) + n) ≡⟨ addToRight (S m) n ⟩ + S (m + S n) ≡⟨ refl ⟩ + (S m) + (S n) ∎