diff --git a/Compile.hs b/Compile.hs index 79da7c4..f78af5b 100644 --- a/Compile.hs +++ b/Compile.hs @@ -142,6 +142,8 @@ compileComment (Comment mayName comm) = <$> traverse compileBlock mayName <*> compileBlock comm compileTheoremStatement :: (Monad m, Applicative m) => TheoremStatement FullLocation -> Err m T.Text +compileTheoremStatement (Prove b) = + (\bl -> div "theorem-statement" [tag' "h3" ["Prove"], bl]) <$> compileBlock b compileTheoremStatement (AssumeProve assumps results) = (\as rs -> div "theorem-statement" [ diff --git a/TranslateTex.hs b/TranslateTex.hs index 9cc4b5f..b014762 100644 --- a/TranslateTex.hs +++ b/TranslateTex.hs @@ -93,9 +93,11 @@ simpleSection keyword p = do labelAndStatement :: TexParser Ref (Maybe Label, TheoremStatement Ref) labelAndStatement = (,) <$> optLabel <*> (statement <* texSpace) where - statement = + statement = assumeProve <|> prove + assumeProve = AssumeProve <$> simpleSection "suppose" (many item) <*> simpleSection "then" (many item) + prove = Prove <$> simpleSection "prove" (Block <$> many anyChunk) item = satisfy (== NoArgCmd "item") >> Block <$> many (satisfy (/= NoArgCmd "item")) diff --git a/Types.hs b/Types.hs index 5e0ed7b..36a7d37 100644 --- a/Types.hs +++ b/Types.hs @@ -30,7 +30,11 @@ deriving instance Traversable (DeclarationF a) data Comment loc = Comment (Maybe (Tex.Block loc)) (Tex.Block loc) deriving (Show, Functor, Foldable, Traversable) -data TheoremStatement loc = AssumeProve [Tex.Block loc] [Tex.Block loc] +-- TODO: Clean this up. There needs to be a principled list of things +-- here. Use types +data TheoremStatement loc + = AssumeProve [Tex.Block loc] [Tex.Block loc] + | Prove (Tex.Block loc) deriving (Show, Functor, Foldable, Traversable) type MaybeJustifiedF a loc = (Tex.Block loc, Maybe (ProofF a loc)) diff --git a/examples/primes.tex b/examples/primes.tex index 9c4c05e..7a0d8ef 100644 --- a/examples/primes.tex +++ b/examples/primes.tex @@ -73,7 +73,7 @@ \claim{Q.E.D.} } \claim{$a \leq \sqrt{n}$}{\simple{ - $$a \leq \sqrt{m} \leq \sqrt{n}$$ + $$a = \sqrt{\frac{m}{b}} \leq \sqrt{m} \leq \sqrt{n}$$ which follows from the previous claim and monotonicity of $\sqrt{-}$. }} \claim{ @@ -98,16 +98,11 @@ } \theorem{There are infinitely many prime numbers}{ - \suppose{ - \item There are finitely many primes. - } - \then{ - \item Contradiction. - } + \prove{For any $N \in \bn$, there are at least $N$ primes} \proof{ \suppose{\item $n \in \bn$} - \then{\item $\pi(n) \geq \frac{1}{2} \log n$} + \then{\item $\pi(n) \geq \frac{1}{2} \log_2 n$} \because{ \claim{$2^{\pi(n)} \sqrt{n} \geq n$}{ \claim{$2^{\pi(n)} \sqrt{n} \geq \rs{\mathcal{P}(\Pi(n)) \times \Set{1, \hdots, \floor{\sqrt{n}}}}$}{ @@ -141,11 +136,16 @@ \claim{Q.E.D.}{\simple{Algebra.}} } + \claim{$\pi(2^{2 N}) \geq N$}{ + \simple{ + $$\pi(2^{2 N}) \geq \frac{1}{2} \log_2 2^{2N} = N$$ + } + } + \claim{Q.E.D.}{ \simple{ - Since the function $n \mapsto \frac{1}{2} \log n$ goes - to infinity with $n$, so too does $\pi(n)$. - By \ref{pidef}, this implies there are infinitely many primes. + The total number of primes is at least $\pi(2^{2 N})$, + so by the previous claim, there are at least $N$ primes. } } } diff --git a/src/css/proof.css b/src/css/proof.css index 7ee3102..ce4b268 100644 --- a/src/css/proof.css +++ b/src/css/proof.css @@ -103,19 +103,15 @@ body { font-family: 'Latin-Modern-Roman-Caps'; } -.take { - background-color: #e8dcc5; - padding: 10px; - margin: 10px; - - border-radius: 23px 23px 23px 23px; - -moz-border-radius: 23px 23px 23px 23px; - -webkit-border-radius: 23px 23px 23px 23px; - border: 2px solid #000000; +.list-header { + font-family: 'Latin-Modern-Roman-Caps'; } -.take .list-header { - font-family: 'Latin-Modern-Roman-Caps'; +.suppose { + border-left: 3px solid black; + padding-left: 10px; + margin-bottom: 5px; + margin-top: 5px; } .theorem { @@ -126,10 +122,6 @@ body { display: inline-block; } -.suchthat .list-header { - font-family: 'Latin-Modern-Roman-Caps'; -} - .node-header { cursor: pointer; } diff --git a/src/js/proof.js b/src/js/proof.js index 0823651..a5cc291 100644 --- a/src/js/proof.js +++ b/src/js/proof.js @@ -82,7 +82,6 @@ function annotateWithNumbers(decls, level) { function decorateCaseBlocks(){ $('.cases').each(function() { var block = $(this); - console.log('yo'); block.prepend($('
Cases:
')); // block.children('.case').each(function(i) }); @@ -132,6 +131,16 @@ function decorateSuchThats() { }); } +function decorateSupposes() { + $('.suppose').each(function() { + var suppose = $(this); + var assumptions = suppose.children('.assumptions'); + var results = suppose.children('.results'); + assumptions.before($('
Suppose:
')); + results.before($('
Then:
')); + }) +} + function wrapWithLocation(node) { var wrapper = $('
'); node.replaceWith(wrapper); @@ -169,6 +178,10 @@ function decorateComments() { }); } +function capitalize(s){ + return s.charAt(0).toUpperCase() + s.substring(1); +} + function decorateTheorems() { $('.theorem').each(function() { var theorem = $(this); @@ -182,7 +195,8 @@ function decorateTheorems() { theorem.addClass('top-level'); content.append(statement, proof); - header.append($('

Theorem:

'), name); + var title = capitalize(theorem.attr('data-thmkind')); + header.append($('

' + title + ':

'), name); theorem.append(header, content); var wrapper = $('
'); @@ -198,6 +212,7 @@ function decorateTheorems() { $(function(){ MathJax.Hub.Queue(decorateCaseBlocks); + MathJax.Hub.Queue(decorateSupposes); MathJax.Hub.Queue(decorateTakes); MathJax.Hub.Queue(decorateLets); MathJax.Hub.Queue(decorateSuchThats);