Mercurial > hg > Papers > 2020 > ryokka-master

annotate paper/src/Reasoning.agda.replaced @ 2:c7acb9211784

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add code, figure. and paper fix content
author ryokka
date Mon, 27 Jan 2020 20:41:36 +0900
parents
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
2
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
1 open import Relation.Binary.PropositionalEquality
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
2 open import nat
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
3 open import nat_add
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
4 open @$\equiv$@-Reasoning
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
5
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
6 module nat_add_sym_reasoning where
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
7
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
8 addToRight : (n m : Nat) @$\rightarrow$@ S (n + m) @$\equiv$@ n + (S m)
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
9 addToRight O m = refl
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
10 addToRight (S n) m = cong S (addToRight n m)
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
11
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
12 addSym : (n m : Nat) @$\rightarrow$@ n + m @$\equiv$@ m + n
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
13 addSym O O = refl
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
14 addSym O (S m) = cong S (addSym O m)
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
15 addSym (S n) O = cong S (addSym n O)
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
16 addSym (S n) (S m) = begin
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
17 (S n) + (S m) @$\equiv$@@$\langle$@ refl @$\rangle$@
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
18 S (n + S m) @$\equiv$@@$\langle$@ cong S (addSym n (S m)) @$\rangle$@
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
19 S ((S m) + n) @$\equiv$@@$\langle$@ addToRight (S m) n @$\rangle$@
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
20 S (m + S n) @$\equiv$@@$\langle$@ refl @$\rangle$@
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
21 (S m) + (S n) @$\blacksquare$@