Finished exercise 3.0.1 (mult-comm)

sf/code/ch3.ath

@@ -20,8 +20,6 @@ conclude plus-Z-n := (forall n . 0 + n = n)
  pick-any n:Nat
  (!chain [(0 + n) = n [plus-nat-def]])
 
-
-
 conclude minus-diag := (forall n . n - n = Zero)
  by-induction minus-diag {
  Zero => (!chain [(Zero - Zero) = Zero [minus-nat-def]])
@@ -128,6 +126,65 @@ conclude evenb_S := (forall n . even n <==> ~ even Succ n)
  <==> (~ even Succ Succ k) [even-def]])
  }
 
+conclude plus-rearrange
+ pick-any n1:Nat n2:Nat m1:Nat m2:Nat
+ (!chain [((n1 + n2) + (m1 + m2)) 
+ = ((n2 + n1) + (m1 + m2)) [plus-comm]])
+
+# Exercise 3.0.1, p. 30
+
+define plus-swap := (forall n k m . n + (m + k) = m + (n + k))
+
+conclude plus-swap 
+ pick-any n:Nat k:Nat m:Nat 
+ (!chain [(n + (m + k)) 
+ = ((n + m) + k) [plus-assoc]
+ = ((m + n) + k) [plus-comm]
+ = (m + (n + k)) [plus-assoc]])
+
+define mult-comm := (forall n m . n * m = m * n)
+
+define mult-succ-r := (forall n m . n * Succ m = n + (n * m))
+
+by-induction mult-succ-r {
+ Zero => pick-any m:Nat
+ conclude (Zero * Succ m = Zero + (Zero * m))
+ (!combine-equations
+ (!chain [(Zero * Succ m) = Zero [mult-nat-def]])
+ (!chain [(Zero + (Zero * m)) 
+ = (Zero + Zero) [mult-nat-def]
+ = Zero [plus-nat-def]]))
+| (Succ n') => let {ih := (forall m . n' * Succ m = n' + (n' * m))}
+ conclude (forall m . (Succ n') * (Succ m) = (Succ n') + ((Succ n') * m))
+ pick-any m:Nat 
+ (!combine-equations
+ (!chain [((Succ n') * (Succ m))
+ = ((Succ m) + (n' * (Succ m))) [mult-nat-def]
+ = ((Succ m) + (n' + (n' * m))) [ih]
+ = (Succ (m + (n' + (n' * m)))) [plus-nat-def]
+ = (Succ ((m + n') + (n' * m))) [plus-assoc]])
+ (!chain [((Succ n') + ((Succ n') * m)) 
+ = ((Succ n') + (m + n' * m)) [mult-nat-def] 
+ = (Succ (n' + (m + n' * m))) [plus-nat-def]
+ = (Succ ((n' + m) + n' * m)) [plus-assoc]
+ = (Succ ((m + n') + n' * m)) [plus-comm]]))
+}
+
+by-induction mult-comm {
+ Zero => pick-any m:Nat
+ (!chain [(Zero * m)
+ = Zero [mult-nat-def]
+ = (m * Zero) [mult-0-r]])
+| (Succ k) => let {ih := (forall m . k * m = m * k)}
+ conclude (forall m . (Succ k) * m = m * Succ k)
+ pick-any m:Nat 
+ (!combine-equations 
+ (!chain [((Succ k) * m) 
+ = (m + (k * m)) [mult-nat-def]
+ = (m + (m * k)) [ih]])
+ (!chain [(m * Succ k)
+ = (m + (m * k)) [mult-succ-r]]))
+}
 
+} # Ends Nat extension 
 
-} # Ends module Nat { ... 

sf/latex_sources/ch3.tex

@@ -215,3 +215,54 @@ \section{Proof by Induction}
  (!chain [(even Succ n) <==> (~ even n) [evenb_S]])
 \end{tcAthena}
 \end{solution}
+
+\section{Proofs Within Proofs}
+This section in the SF book appears to be about forcing assertions, which in Athena would be done via the \smkwd{force} keyword. 
+
+In terms of composite proofs: In Coq/Idris, it seems that the main way to develop proofs is via automated rewriting and lemmas. 
+This would be equivalent in style to using ATPs (automated theorem provers) in Athena and simply decomposing a top-level goal 
+into a series of lemmas that could actually be handled by the ATPs. All of the ``proofs'' in such an approach would be 1-line 
+proofs of the following form:
+\begin{tcAthena}
+define goal := ...
+
+conclude lemma-1 := (!prove ...)
+
+conclude lemma-n := (!prove ...) 
+
+conclude goal := (!prove goal [lemma-1 ... lemma-n])
+\end{tcAthena}
+One can of course introduce additional theorem-proving tactics in Idris, though these again seem to be procedural instructions
+for how to get the built-in tactics to behave properly, not declarative proofs. 
+Consider:
+\begin{tcAthena}
+define plus-rearrange := (forall n1 n2 m1 m2 . (n1 + n2) + (m1 + m2) = (n2 + n1) + (m1 + m2))
+\end{tcAthena}
+This is really just a single application of commutativity of addition. 
+Here is the Idris proof (as appears on p. 30):
+\begin{idris}
+plus_rearrange : (n, m, p, q : Nat) ->
+ (n + m) + (p + q) = (m + n) + (p + q)
+plus_rearrange n m p q = rewrite plus_rearrange_lemma n m in Refl
+ where
+ plus_rearrange_lemma : (n, m : Nat) -> n + m = m + n
+ plus_rearrange_lemma = plus_comm
+\end{idris}
+Here is the Athena version: 
+\begin{tcAthena}
+conclude plus-rearrange
+ pick-any n1:Nat n2:Nat m1:Nat m2:Nat
+ (!chain [((n1 + n2) + (m1 + m2)) 
+ = ((n2 + n1) + (m1 + m2)) [plus-comm]])
+\end{tcAthena}
+
+\begin{exercise}[subtitle={\mbox{\rm{\em (SF Exercise 3.0.1, p. 30)}}}]
+Prove: 
+\begin{tcAthena}
+define plus-swap := (forall n k m . n + (m + k) = m + (n + k))
+define mult-comm := (forall n m . n * m = m * n)
+\end{tcAthena}
+\begin{solution}
+\begin{tcAthena}
+\end{tcAthena}
+\end{solution}

sf/latex_sources/main.aux

@@ -20,7 +20,6 @@
 \@writefile{lof}{\addvspace {10\p@ }}
 \@writefile{lot}{\addvspace {10\p@ }}
 \@writefile{toc}{\contentsline {section}{\numberline {3.1}Proof by Induction}{16}\protected@file@percent }
-\XSIM{readaux}
 \newlabel{Eq:IndHyp}{{3.1}{19}}
 \newlabel{Eq:IndHyp@cref}{{[equation][1][3]3.1}{[1][18][]19}}
 \newlabel{Eq:Goal1}{{3.2}{19}}
@@ -29,3 +28,5 @@
 \newlabel{Eq:Aux1@cref}{{[equation][3][3]3.3}{[1][18][]19}}
 \newlabel{Eq:EvenDef}{{3.4}{19}}
 \newlabel{Eq:EvenDef@cref}{{[equation][4][3]3.4}{[1][18][]19}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.2}Proofs Within Proofs}{19}\protected@file@percent }
+\XSIM{readaux}

sf/latex_sources/main.log

@@ -1,4 +1,4 @@
-This is pdfTeX, Version 3.14159265-2.6-1.40.20 (TeX Live 2019/Debian) (preloaded format=pdflatex 2024.4.23) 9 JUN 2024 12:38
+This is pdfTeX, Version 3.14159265-2.6-1.40.20 (TeX Live 2019/Debian) (preloaded format=pdflatex 2024.4.23) 9 JUN 2024 13:00
 entering extended mode
  restricted \write18 enabled.
  %&-line parsing enabled.
@@ -1964,16 +1964,16 @@ Chapter 3.
 \openout10 = `main-exercise-13-solution-body.tex'.
 
 
-(./main-exercise-13-solution-body.tex))
+(./main-exercise-13-solution-body.tex) [19])
 \tf@thm=\write11
 \openout11 = `main.thm'.
 
- [19] (./main.aux (./main.xsim)) ) 
+ [20] (./main.aux (./main.xsim)) ) 
 Here is how much of TeX's memory you used:
- 55169 strings out of 481239
- 1328553 string characters out of 5920377
+ 55184 strings out of 481239
+ 1328777 string characters out of 5920377
  2413936 words of memory out of 5000000
- 69344 multiletter control sequences out of 15000+600000
+ 69359 multiletter control sequences out of 15000+600000
  597998 words of font info for 123 fonts, out of 8000000 for 9000
  1141 hyphenation exceptions out of 8191
  81i,9n,138p,1608b,1742s stack positions out of 5000i,500n,10000p,200000b,80000s
@@ -1989,10 +1989,10 @@ xmf-dist/fonts/type1/public/amsfonts/cm/cmr9.pfb></usr/share/texlive/texmf-dist
 urier/ucrr8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmb8a.pf
 b></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmr8a.pfb></usr/share/t
 exlive/texmf-dist/fonts/type1/urw/times/utmri8a.pfb>
-Output written on main.pdf (20 pages, 172592 bytes).
+Output written on main.pdf (21 pages, 174604 bytes).
 PDF statistics:
- 157 PDF objects out of 1000 (max. 8388607)
- 98 compressed objects within 1 object stream
+ 160 PDF objects out of 1000 (max. 8388607)
+ 100 compressed objects within 1 object stream
  0 named destinations out of 1000 (max. 500000)
  157 words of extra memory for PDF output out of 10000 (max. 10000000)