ProofObjects #31
ProofObjects #31
Conversation
|
Should be ready. So yeah, in its current form it's not so useful. It does contain some good-to-know theory, but if you've made it this far, you most likely already have some intuitive understanding of the things it talks about. We could try putting it earlier in the book, but it depends on |
|
Let's keep collecting the rough translations and we can edit later. Maybe after ten chapters we should focus on editing and then do a "release" (merge to master and regenerate the PDF). |
|
According to the book itself, the first part ("Logical Foundations") ends after |
|
Sounds like a solid plan to me. |
|
Any remarks/edits on this chapter specifically? |
|
I've been busy, but will make sure to review this and the other PRs properly by Monday at the latest. |
|
I've got some comments and edits locally. Will post them tonight. |
|
So, according to https://softwarefoundations.cis.upenn.edu/draft/lf-current/toc.html , "Logical foundations" actually end on |
|
Cool. Let's do a "release" up to Auto then and merge Rel in lot develop after. I got a bit sick last night and likely won't have time tonight, but I can definitely review all the PRs that are ready tomorrow. |
src/ProofObjects.lidr
Outdated
| \idr{Void} is equally simple — indeed, so simple it may look syntactically wrong | ||
| at first glance! | ||
|
|
||
| \todo[inline]{Edit, this actually is wrong, stdlib uses \idr{%runElab} to define |
There was a problem hiding this comment.
We should use just \idr{runElab} until we solve #22.
src/ProofObjects.lidr
Outdated
| evidence) and returns a piece of evidence! Here it is: | ||
|
|
||
| ```coq | ||
| Definition ev_plus4' : ∀n, ev n -> ev (4 + n) := |
There was a problem hiding this comment.
Let's use forall so as not to upset minted.
src/ProofObjects.lidr
Outdated
|
|
||
| > module ProofObjects | ||
|
|
||
| \[ |
There was a problem hiding this comment.
We'll need to add the following to book.tex:
- \usepackage{dirtytalk}
src/ProofObjects.lidr
Outdated
| > module ProofObjects | ||
|
|
||
| \[ | ||
| \say{"\textit{Algorithms are the computational content of proofs.}" - Robert |
There was a problem hiding this comment.
This works for me:
\say{Algorithms are the computational content of proofs.} -- Robert Harper
src/ProofObjects.lidr
Outdated
| \idr{Or}, without resorting to tactics. | ||
|
|
||
|
|
||
| ==== Exercise: 2 stars, optional (or_commut'') |
There was a problem hiding this comment.
or_commut'' should be or_comm
src/ProofObjects.lidr
Outdated
| $\square$ | ||
|
|
||
|
|
||
| === \idr{Unit} and \idr{Void} |
There was a problem hiding this comment.
Here's a dirty hack to work around #24:
-=== \idr{Unit} and \idr{Void}
+\subsection{\idr{Unit} and \idr{Void}}
src/ProofObjects.lidr
Outdated
| | conj HP HQ => conj HQ HP | ||
| end. | ||
|
|
||
| Definition and_comm' P Q : P ∧ Q ↔ Q ∧ P := |
src/ProofObjects.lidr
Outdated
| pattern-matching. For instance: | ||
|
|
||
| ```coq | ||
| Definition and_comm'_aux P Q (H : P ∧ Q) := |
src/ProofObjects.lidr
Outdated
| {n : Nat} -> Ev n -> Ev (S (S n)) | ||
| ``` | ||
|
|
||
| expresses this functionality, in the same way that the polymorphic type \idr{{x |
There was a problem hiding this comment.
\idr{...} needs to be on one line
| only one constructor, so only one subgoal gets generated. Now, though, the form | ||
| of the \idr{EqRefl} constructor does give us some extra information: it tells us | ||
| that the two arguments to \idr{PropEq} must be the same! The `inversion` tactic | ||
| adds this fact to the context. |
There was a problem hiding this comment.
Here's a diff with all my suggestions:
diff --git a/src/ProofObjects.lidr b/src/ProofObjects.lidr
index 7e465b3..2f24cd4 100644
--- a/src/ProofObjects.lidr
+++ b/src/ProofObjects.lidr
@@ -2,10 +2,7 @@
> module ProofObjects
-\[
- \say{"\textit{Algorithms are the computational content of proofs.}" - Robert
-Harper}
-\]
+\say{Algorithms are the computational content of proofs.} -- Robert Harper
We have seen that Idris has mechanisms both for _programming_, using inductive
data types like \idr{Nat} or \idr{List} and functions over these types, and for
@@ -103,9 +100,10 @@ wants to be further applied to evidence that that number is even; its type,
{n : Nat} -> Ev n -> Ev (S (S n))
```
-expresses this functionality, in the same way that the polymorphic type \idr{{x
-: Type} -> List x} expresses the fact that the constructor \idr{Nil} can be
-thought of as a function from types to empty lists with elements of that type.
+expresses this functionality, in the same way that the polymorphic type
+\idr{{x : Type} -> List x} expresses the fact that the constructor \idr{Nil} can
+be thought of as a function from types to empty lists with elements of that
+type.
\todo[inline]{Edit or remove}
@@ -219,7 +217,7 @@ n)} — that is, a function that takes two arguments (one number and a piece of
evidence) and returns a piece of evidence! Here it is:
```coq
-Definition ev_plus4' : ∀n, ev n -> ev (4 + n) :=
+Definition ev_plus4' : forall n, ev n -> ev (4 + n) :=
fun (n : Nat) => fun (H : ev n) =>
ev_SS (S (S n)) (ev_SS n H).
```
@@ -359,12 +357,12 @@ we've been doing. We can also use it to build proofs directly, using
pattern-matching. For instance:
```coq
-Definition and_comm'_aux P Q (H : P ∧ Q) :=
+Definition and_comm'_aux P Q (H : P /\ Q) :=
match H with
| conj HP HQ => conj HQ HP
end.
-Definition and_comm' P Q : P ∧ Q ↔ Q ∧ P :=
+Definition and_comm' P Q : P /\ Q <-> Q /\ P :=
conj (and_comm'_aux P Q) (and_comm'_aux Q P).
```
@@ -396,11 +394,11 @@ Once again, we can also directly write proof objects for theorems involving
\idr{Or}, without resorting to tactics.
-==== Exercise: 2 stars, optional (or_commut'')
+==== Exercise: 2 stars, optional (or_comm)
\ \todo[inline]{Edit}
-Try to write down an explicit proof object for \idr{or_commut} (without using
+Try to write down an explicit proof object for \idr{or_comm} (without using
`Print` to peek at the ones we already defined!).
> or_comm : Or p q -> Or q p
@@ -450,7 +448,7 @@ Complete the definition of the following proof object:
$\square$
-=== \idr{Unit} and \idr{Void}
+\subsection{\idr{Unit} and \idr{Void}}
The inductive definition of the \idr{Unit} proposition is simple:
@@ -465,7 +463,7 @@ a proof of\idr{Unit} is not informative.)
\idr{Void} is equally simple — indeed, so simple it may look syntactically wrong
at first glance!
-\todo[inline]{Edit, this actually is wrong, stdlib uses \idr{%runElab} to define
+\todo[inline]{Edit, this actually is wrong, stdlib uses \idr{runElab} to define
it}
```idris
@@ -570,8 +568,8 @@ In general, the `inversion` tactic...
- adds these equalities to the context (and, for convenience, rewrites them
in the goal), and
- - if the equalities are not satisfiable (e.g., they involve things like `S n
- = Z`), immediately solves the subgoal.
+ - if the equalities are not satisfiable (e.g., they involve things like
+ \idr{S n = Z}), immediately solves the subgoal.
_Example_: If we invert a hypothesis built with \idr{Or}, there are two
constructors, so two subgoals get generated. The conclusion (result type) of the
diff --git a/src/book.tex b/src/book.tex
index a7632b4..6ee6846 100644
--- a/src/book.tex
+++ b/src/book.tex
@@ -42,6 +42,7 @@ header-includes:
- \usepackage{todonotes}
-
- \usepackage{ebproof}
+- \usepackage{dirtytalk}
include-before: \frontmatter
---
|
But |
|
Ha, ok. I misunderstood. 👍 to a "release" after Rel then. |
src/ProofObjects.lidr
Outdated
| @@ -2,10 +2,8 @@ | |||
|
|
|||
| > module ProofObjects | |||
|
|
|||
| \[ | |||
| \say{"\textit{Algorithms are the computational content of proofs.}" - Robert | |||
| \say{"\textit{Algorithms are the computational content of proofs.}" - Robert | |||
There was a problem hiding this comment.
This results in the following in the PDF.
“”Algorithms are the computational content of proofs.” - Robert Harper”
I'm not married to this exact solution, but I don't like the double quotes as it is now.
There was a problem hiding this comment.
\say{\textit{Algorithms are the computational content of proofs.}}
-- Robert Harper... results in:
“Algorithms are the computational content of proofs.” – Robert Harper
|
Actually I'm just gonna merge this and #33 and make the |
It seems so far this chapter will be mostly useless for us, as the distinction between proofs and terms they keep talking about doesn't really exist in Idris. Maybe something interesting will come up later.