fix unnecessary copies, some todos

Author: Alex Gryzlov

src/Basics.lidr

@@ -769,7 +769,8 @@ arrow symbol is pronounced "implies."
 As before, we need to be able to reason by assuming the existence of some
 numbers \idr{n} and \idr{m}. We also need to assume the hypothesis \idr{n = m}.
 
-\todo[inline]{Edit.}
+\todo[inline]{Edit, mention the "generate initial pattern match" editor command}
+
 The \idr{intros} tactic will serve to move all three of these from the goal into
 assumptions in the current context.
 

src/IndProp.lidr

@@ -1,13 +1,17 @@
-= IndProp: Inductively Defined Propositions
+= IndProp : Inductively Defined Propositions
 
 > module IndProp
 >
 > import Basics
 > import Induction
+> import Tactics
+> import Logic
 >
 > %hide Basics.Numbers.pred
-> %hide Prelude.Stream.(::)
 >
+> %access public export
+> %default total
+
 
 == Inductively Defined Propositions
 
@@ -106,8 +110,8 @@ When checking argument n to IndType.Wrong_ev:
                 Nat (Expected type)
 ```
 
-\todo[inline]{Edit the explanation, it works fine if you remove the first \idr{n ->}
-in \idr{Wrong_ev_SS}}
+\todo[inline]{Edit the explanation, it works fine if you remove the first \idr{n
+->} in \idr{Wrong_ev_SS}}
 
 ("Parameter" here is Idris jargon for an argument on the left of the colon in an
 Inductive definition; "index" is used to refer to arguments on the right of the
@@ -338,13 +342,6 @@ induction hypothesis talks about n', as opposed to n or some other number.
 The equivalence between the second and third definitions of evenness now
 follows.
 
-\todo[inline]{Copypasted `<->` for now}
-
-> iff : {p,q : Type} -> Type
-> iff {p} {q} = (p -> q, q -> p)
->
-> syntax [p] "<->" [q] = iff {p} {q}
->
 > ev_even_iff : (Ev n) <-> (k ** n = double k)
 > ev_even_iff = (ev_even, fro)
 >   where
@@ -894,16 +891,13 @@ chapter: If \idr{ss : List (List t)} represents a sequence of strings \idr{s1,
 ..., sn}, then \idr{fold (++) ss []} is the result of concatenating them all
 together.
 
-\todo[inline]{Copied these here for now, add hyperlink}
+\todo[inline]{Copied from \idr{Poly}, cannot import it due to tuple sugar
+issues}
 
 > fold : (f : x -> y -> y) -> (l : List x) -> (b : y) -> y
 > fold f [] b = b
 > fold f (h::t) b = f h (fold f t b)
 >
-> In : (x : a) -> (l : List a) -> Type
-> In x [] = Void
-> In x (x' :: xs) = (x' = x) `Either` In x xs
->
 > MStar' : ((s : List t) -> (In s ss) -> (s =~ re)) ->
 >          (fold (++) ss []) =~ Star re
 > MStar' f = ?MStar__rhs
@@ -944,28 +938,6 @@ regular expression:
 
 We can then phrase our theorem as follows:
 
-\todo[inline]{Copied here for now}
-
-> in_app_iff : (In a (l++l')) <-> (In a l `Either` In a l')
-> in_app_iff {l} {l'} = (to l l', fro l l')
->   where
->     to : (l, l' : List x) -> In a (l ++ l') -> (In a l) `Either` (In a l')
->     to [] [] prf = absurd prf
->     to [] _ prf = Right prf
->     to (_ :: _) _ (Left Refl) = Left $ Left Refl
->     to (_ :: xs) l' (Right prf) =
->       case to xs l' prf of
->         Left ixs => Left $ Right ixs
->         Right il' => Right il'
->     fro : (l, l' : List x) -> (In a l) `Either` (In a l') -> In a (l ++ l')
->     fro [] _ (Left prf) = absurd prf
->     fro (_ :: _) _ (Left (Left Refl)) = Left Refl
->     fro (_ :: xs) l' (Left (Right prf)) = Right $ fro xs l' (Left prf)
->     fro _ [] (Right prf) = absurd prf
->     fro [] _ (Right prf) = prf
->     fro (_ :: ys) l' prf@(Right _) = Right $ fro ys l' prf
->
-
 \todo[inline]{Some unfortunate implicit plumbing}
 
 > destruct : In x (s1 ++ s2) -> (In x s1) `Either` (In x s2)
@@ -1243,15 +1215,6 @@ computations to statements in \idr{Type}. But performing this conversion in the
 way we did it there can result in tedious proof scripts. Consider the proof of
 the following theorem:
 
-\todo[inline]{Copy here for now}
-
-> beq_nat_true : {n, m : Nat} -> n == m = True -> n = m
-> beq_nat_true {n=Z} {m=Z} _ = Refl
-> beq_nat_true {n=(S _)} {m=Z} Refl impossible
-> beq_nat_true {n=Z} {m=(S _)} Refl impossible
-> beq_nat_true {n=(S n')} {m=(S m')} eq =
->  rewrite beq_nat_true {n=n'} {m=m'} eq in Refl
->
 > filter_not_empty_In : {n : Nat} -> Not (filter ((==) n) l = []) -> In n l
 > filter_not_empty_In {l=[]} contra = contra Refl
 > filter_not_empty_In {l=(x::_)} {n} contra with (n == x) proof h
@@ -1325,19 +1288,6 @@ perform case analysis on \idr{b} while at the same time generating appropriate
 hypothesis in the two branches (\idr{p} in the first subgoal and \idr{Not p} in
 the second).
 
-\todo[inline]{Copy here for now}
-
-> beq_nat_true_iff : (n1, n2 : Nat) -> (n1 == n2 = True) <-> (n1 = n2)
-> beq_nat_true_iff n1 n2 = (to, fro n1 n2)
->   where
->     to : (n1 == n2 = True) -> (n1 = n2)
->     to = beq_nat_true {n=n1} {m=n2}
->     fro : (n1, n2 : Nat) -> (n1 = n2) -> (n1 == n2 = True)
->     fro n1 n1 Refl = sym $ beq_nat_refl n1
->
-> iff_sym : (p <-> q) -> (q <-> p)
-> iff_sym (pq, qp) = (qp, pq)
->
 > beq_natP : {n, m : Nat} -> Reflect (n = m) (n == m)
 > beq_natP {n} {m} = iff_reflect $ iff_sym $ beq_nat_true_iff n m
 >

src/Lists.lidr

@@ -8,6 +8,7 @@
 > %hide Prelude.Basics.snd
 > %hide Prelude.Nat.pred
 
+> %access public export
 > %default total
 
 
@@ -137,8 +138,12 @@ operator and square brackets as an "outfix" notation for constructing lists.
 > syntax [x] "::" [l] = Cons x l
 > syntax "[ ]" = Nil
 
-\todo[inline]{Figure out \idr{syntax} command for this and edit the section}
+\todo[inline]{Seems it's impossible to make an Idris \idr{syntax} to overload
+the list notation. Edit the section.}
+
+```coq
 Notation "[ x ; .. ; y ]" := ( cons x .. ( cons y nil ) ..).
+```
 
 It is not necessary to understand the details of these declarations, but in case
 you are interested, here is roughly what's going on. The right associativity
@@ -158,19 +163,21 @@ The at level 60 part tells Coq how to parenthesize expressions that involve both
 :: and some other infix operator. For example, since we defined + as infix
 notation for the plus function at level 50,
 
+```coq
 Notation "x + y" := ( plus x y )
 ( at level 50, left associativity ).
+```
 
-the + operator will bind tighter than :: , so 1 + 2 :: [3] will be parsed, as
-we'd expect, as (1 + 2) :: [3] rather than 1 + (2 :: [3]) .
+the `+` operator will bind tighter than `::` , so `1 + 2 :: [3]` will be parsed,
+as we'd expect, as `(1 + 2) :: [3]` rather than `1 + (2 :: [3])`.
 
-(Expressions like "1 + 2 :: [3]" can be a little confusing when you read them
-in a .v file. The inner brackets, around 3, indicate a list, but the outer
+(Expressions like "`1 + 2 :: [3]`" can be a little confusing when you read them
+in a `.v` file. The inner brackets, around `3`, indicate a list, but the outer
 brackets, which are invisible in the HTML rendering, are there to instruct the
 "coqdoc" tool that the bracketed part should be displayed as Coq code rather
 than running text.)
 
-The second and third Notation declarations above introduce the standard
+The second and third `Notation` declarations above introduce the standard
 square-bracket notation for lists; the right-hand side of the third one
 illustrates Coq's syntax for declaring n-ary notations and translating them to
 nested sequences of binary constructors.
@@ -337,6 +344,7 @@ multisets a little bit differently, which is why we don't use that name for this
 operation.)
 
 \todo[inline]{How to forbid recursion here? Edit}
+
 For \idr{sum} we're giving you a header that does not give explicit names to the
 arguments. Moreover, it uses the keyword Definition instead of Fixpoint, so
 even if you had names for the arguments, you wouldn't be able to process them
@@ -506,6 +514,7 @@ lists \idr{l}. Here's a concrete example:
 >     rewrite inductiveHypothesis in Refl
 
 \todo[inline]{Edit}
+
 Notice that, as when doing induction on natural numbers, the as ... clause
 provided to the induction tactic gives a name to the induction hypothesis
 corresponding to the smaller list l1' in the cons case. Once again, this Coq
@@ -689,22 +698,24 @@ default for our present purposes.
 \ \todo[inline]{Edit, mention \idr{:s} and \idr{:apropos}?}
 
 We've seen that proofs can make use of other theorems we've already proved,
-e.g., using rewrite . But in order to refer to a theorem, we need to know its
-name! Indeed, it is often hard even to remember what theorems have been proven,
-much less what they are called.
+e.g., using \idr{rewrite}. But in order to refer to a theorem, we need to know
+its name! Indeed, it is often hard even to remember what theorems have been
+proven, much less what they are called.
 
-Coq's Search command is quite helpful with this. Typing Search foo will cause
-Coq to display a list of all theorems involving foo . For example, try
+Coq's `Search` command is quite helpful with this. Typing `Search foo` will
+cause Coq to display a list of all theorems involving `foo`. For example, try
 uncommenting the following line to see a list of theorems that we have proved
-about rev :
+about `rev`:
 
+```coq
 (* Search rev. *)
+```
 
-Keep Search in mind as you do the following exercises and throughout the rest of
-the book; it can save you a lot of time!
+Keep `Search` in mind as you do the following exercises and throughout the rest
+of the book; it can save you a lot of time!
 
-If you are using ProofGeneral, you can run Search with C-c C-a C-a. Pasting its
-response into your buffer can be accomplished with C-c C-;.
+If you are using ProofGeneral, you can run `Search` with `C-c C-a C-a`. Pasting
+its response into your buffer can be accomplished with `C-c C-;`.
 
 
 === List Exercises, Part 1
@@ -862,7 +873,8 @@ programming language: conditional expressions...
 >                            then Some a
 >                            else nth_error' l' (pred n)
 
-\todo[inline]{Edit this paragraph}
+\todo[inline]{Edit or remove this paragraph, doesn't seem to hold in Idris}
+
 Coq's conditionals are exactly like those found in any other language, with one
 small generalization. Since the boolean type is not built in, Coq actually
 supports conditional expressions over any inductively defined type with exactly

src/Logic.lidr

@@ -3,10 +3,15 @@
 > module Logic
 
 > import Basics
+> import Induction
+> import Tactics
 
 > %hide Basics.Numbers.pred
 > %hide Basics.Playground2.plus
 
+> %access public export
+> %default total
+
 In previous chapters, we have seen many examples of factual claims
 (_propositions_) and ways of presenting evidence of their truth (_proofs_). In
 particular, we have worked extensively with equality propositions of the form
@@ -783,7 +788,7 @@ We will see many more examples of the idioms from this section in later chapters
 
 \todo[inline]{Edit, Idris's core is likely some variant of MLTT}
 
-Idris's logical core, the Calculus of Inductive Constructions, differs in some
+Coq's logical core, the Calculus of Inductive Constructions, differs in some
 important ways from other formal systems that are used by mathematicians for
 writing down precise and rigorous proofs. For example, in the most popular
 foundation for mainstream paper-and-pencil mathematics, Zermelo-Fraenkel Set
@@ -885,10 +890,6 @@ have is that it performs a call to \idr{++} on each step; running \idr{++} takes
 time asymptotically linear in the size of the list, which means that \idr{rev}
 has quadratic running time.
 
-> rev : (l : List x) -> List x
-> rev [] = []
-> rev (h::t) = (rev t) ++ [h]
-
 We can improve this with the following definition:
 
 > rev_append : (l1, l2 : List x) -> List x
@@ -928,10 +929,6 @@ For instance, to claim that a number \idr{n} is even, we can say either
 We often say that the boolean \idr{evenb n} _reflects_ the proposition \idr{(k
 ** n = double k)}.
 
-> double : (n : Nat) -> Nat
-> double  Z    = Z
-> double (S k) = S (S (double k))
-
 > evenb_double : evenb (double k) = True
 > evenb_double {k = Z} = Refl
 > evenb_double {k = (S k')} = evenb_double {k=k'}
@@ -951,33 +948,16 @@ $\square$
 > even_bool_prop = (to, fro)
 > where
 >   to : evenb n = True -> (k ** n = double k)
->   to {n} prf = let
->     (k ** p) = evenb_double_conv {n}
->   in
-
-\todo[inline]{Is there a shorter way?}
-
->     (k ** replace prf p {P = \x => n = if x then double k else S (double k)})
+>   to {n} prf =
+>     let (k ** p) = evenb_double_conv {n}
+>     in (k ** rewrite p in rewrite prf in Refl)
 >   fro : (k ** n = double k) -> evenb n = True
 >   fro {n} (k**prf) = rewrite prf in evenb_double {k}
 
 Similarly, to state that two numbers \idr{n} and \idr{m} are equal, we can say
 either (1) that \idr{n == m} returns \idr{True} or (2) that \idr{n = m}. These
 two notions are equivalent.
 
-\todo[inline]{Copy these 2 here for now}
-
->  beq_nat_true : {n, m : Nat} -> n == m = True -> n = m
->  beq_nat_true {n=Z} {m=Z} _ = Refl
->  beq_nat_true {n=(S _)} {m=Z} Refl impossible
->  beq_nat_true {n=Z} {m=(S _)} Refl impossible
->  beq_nat_true {n=(S n')} {m=(S m')} eq =
->   rewrite beq_nat_true {n=n'} {m=m'} eq in Refl
-
->  beq_nat_refl : (n : Nat) -> True = n == n
->  beq_nat_refl Z = Refl
->  beq_nat_refl (S k) = beq_nat_refl k
-
 >  beq_nat_true_iff : (n1, n2 : Nat) -> (n1 == n2 = True) <-> (n1 = n2)
 >  beq_nat_true_iff n1 n2 = (to, fro n1 n2)
 >  where
@@ -1158,12 +1138,6 @@ However, if we happen to know that \idr{p} is reflected in some boolean term
 \idr{b}, then knowing whether it holds or not is trivial: we just have to check
 the value of \idr{b}.
 
-\todo[inline]{Remove when a release with
-https://github.com/idris-lang/Idris-dev/pull/3925 happens}
-
-> Uninhabited (False = True) where
->   uninhabited Refl impossible
-
 > restricted_excluded_middle : (p <-> b = True) -> p `Either` Not p
 > restricted_excluded_middle {b = True} (_, bp) = Left $ bp Refl
 > restricted_excluded_middle {b = False} (pb, _) = Right $ uninhabited . pb