# HG changeset patch # User Yasutaka Higa # Date 1423625866 -32400 # Node ID e30a02baba55194c8a6160a4f5c70f01cc441e16 # Parent de3397af1f8d5fdf4d2bba69bf3f0f38194ad366 Fix function name diff -r de3397af1f8d -r e30a02baba55 Makefile --- a/Makefile Tue Feb 10 15:30:01 2015 +0900 +++ b/Makefile Wed Feb 11 12:37:46 2015 +0900 @@ -15,7 +15,7 @@ .PHONY : clean all open remake clean: - rm -f *.dvi *.aux *.log *.pdf *.ps *.gz *.bbl *.blg *.toc *~ *.core *.cpt + rm -f *.dvi *.aux *.log *.pdf *.ps *.gz *.bbl *.blg *.toc *~ *.core *.cpt *.lof *.lot *.lol all: $(TARGET).pdf diff -r de3397af1f8d -r e30a02baba55 agda.tex --- a/agda.tex Tue Feb 10 15:30:01 2015 +0900 +++ b/agda.tex Wed Feb 11 12:37:46 2015 +0900 @@ -469,21 +469,21 @@ $ O + (S m) \equiv (S m) + O $ を証明することになる。 この等式は + の定義により $ O + (S m) \equiv S (m + O) $ と変形できる。 - $ S (m + O) $ は $ m + O $ に S を加えたものであるため、 cong を用いて再帰的に \verb/add_sym/ を実行することで証明できる。 + $ S (m + O) $ は $ m + O $ に S を加えたものであるため、 cong を用いて再帰的に \verb/addSym/ を実行することで証明できる。 この2つの証明はこのような意味を持つ。 n が 0 であるとき、 m も 0 なら簡約により等式が成立する。 n が 0 であるとき、 m が 0 でないとき、 m は後続数である。 よって m が (S x) と書かれる時、 x は m の前の値である。 前の値による交換法則を用いてからその結果の後続数も + の定義により等しい。 - ここで、 \verb/add_sym/ に渡される m は1つ値が減っているため、最終的には n = 0, m = 0 である refl にまで簡約され、等式が得られる。 + ここで、 \verb/addSym/ に渡される m は1つ値が減っているため、最終的には n = 0, m = 0 である refl にまで簡約され、等式が得られる。 \item n = S n, m = O $ (S n) + O \equiv O + (S n) $ を証明する。 この等式は + の定義により $ S (n + O) \equiv (S n) $ と変形できる。 さらに変形すれば $ S (n + O) \equiv S (O + n) $ となる。 - よって \verb/add_sym/ により O と n を変換した後に cong で S を加えることで証明ができる。 + よって \verb/addSym/ により O と n を変換した後に cong で S を加えることで証明ができる。 ここで、 $ O + n \equiv n $ は + の定義により自明であるが、$ n + O \equiv n $ をそのまま導出できないことに注意して欲しい。 + の定義は左側の項から S を右側の項への移すだけであるため、右側の項への演算はしない。 diff -r de3397af1f8d -r e30a02baba55 src/nat_add_sym.agda --- a/src/nat_add_sym.agda Tue Feb 10 15:30:01 2015 +0900 +++ b/src/nat_add_sym.agda Wed Feb 11 12:37:46 2015 +0900 @@ -5,10 +5,10 @@ module nat_add_sym where -add_sym : (n m : Nat) -> n + m ≡ m + n -add_sym O O = refl -add_sym O (S m) = cong S (add_sym O m) -add_sym (S n) O = cong S (add_sym n O) -add_sym (S n) (S 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) = {!!} diff -r de3397af1f8d -r e30a02baba55 src/nat_add_sym_reasoning.agda --- a/src/nat_add_sym_reasoning.agda Tue Feb 10 15:30:01 2015 +0900 +++ b/src/nat_add_sym_reasoning.agda Wed Feb 11 12:37:46 2015 +0900 @@ -5,17 +5,18 @@ module nat_add_sym_reasoning where -add_to_right : (n m : Nat) -> S (n + m) ≡ n + (S m) -add_to_right n m = {!!} +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 (add_sym O m) -addSym (S n) O = cong S (add_sym n O) -add_sym (S n) (S m) = begin - S (n + S m) ≡⟨ cong S (add_sym n (S m)) ⟩ +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) ≡⟨ cong S (addSym n (S m)) ⟩ S (S (m + n)) ≡⟨ refl ⟩ - S ((S m) + n) ≡⟨ {!!} ⟩ + S ((S m) + n) ≡⟨ addToRight (S m) n ⟩ S (m + S n) ∎