remove negb, use && and ||

Author: Alex Gryzlov

src/Basics.lidr

@@ -249,10 +249,12 @@ standard library.
 
 Functions over booleans can be defined in the same way as above:
 
->   negb : (b : Bool) -> Bool
->   negb True  = False
->   negb False = True
->
+```idris
+  not : (b : Bool) -> Bool
+  not True  = False
+  not False = True
+```
+
 >   andb : (b1 : Bool) -> (b2 : Bool) -> Bool
 >   andb True  b2 = b2
 >   andb False b2 = False
@@ -286,15 +288,17 @@ We can also introduce some familiar syntax for the boolean operations we have
 just defined. The \idr{syntax} command defines a new symbolic notation for an
 existing definition, and \idr{infixl} specifies left-associative fixity.
 
->   infixl 4 /\, \/
->
->   (/\) : Bool -> Bool -> Bool
->   (/\) = andb
->
->   (\/) : Bool -> Bool -> Bool
->   (\/) = orb
->
->   testOrb5 : False \/ False \/ True = True
+```idris
+  infixl 4 &&, ||
+
+  (&&) : Bool -> Bool -> Bool
+  (&&) = andb
+
+  (||) : Bool -> Bool -> Bool
+  (||) = orb
+```
+
+>   testOrb5 : False || False || True = True
 >   testOrb5 = Refl
 >
 
@@ -355,27 +359,27 @@ Every expression in Idris has a type, describing what sort of thing it computes.
 The \idr{:type} (or \idr{:t}) REPL command asks Idris to print the type of an
 expression.
 
-For example, the type of \idr{negb True} is \idr{Bool}.
+For example, the type of \idr{not True} is \idr{Bool}.
 
 ```idris
 λΠ> :type True
 True : Bool
-λΠ> :t negb True
-negb True : Bool
+λΠ> :t not True
+not True : Bool
 ```
 
 \todo[inline]{Confirm the "function types" wording.}
 
-Functions like \idr{negb} itself are also data values, just like \idr{True} and
+Functions like \idr{not} itself are also data values, just like \idr{True} and
 \idr{False}. Their types are called \glspl{function type}, and they are written
 with arrows.
 
 ```idris
-λΠ> :t negb
-negb : Bool -> Bool
+λΠ> :t not
+not : Bool -> Bool
 ```
 
-The type of \idr{negb}, written \idr{Bool -> Bool} and pronounced "\idr{Bool}
+The type of \idr{not}, written \idr{Bool -> Bool} and pronounced "\idr{Bool}
 arrow \idr{Bool}," can be read, "Given an input of type \idr{Bool}, this
 function produces an output of type \idr{Bool}." Similarly, the type of
 \idr{andb}, written \idr{Bool -> Bool -> Bool}, can be read, "Given two inputs,
@@ -499,7 +503,7 @@ simpler definition that is a bit easier to work with:
 >   ||| Determine whether a number is odd.
 >   ||| @n a number
 >   oddb : (n : Nat) -> Bool
->   oddb n = negb (evenb n)
+>   oddb n = not (evenb n)
 >
 >   testOddb1 : oddb 1 = True
 >   testOddb1 = Refl
@@ -886,9 +890,9 @@ For example, we use it next to prove that boolean negation is involutive --
 i.e., that negation is its own inverse.
 
 >   ||| A proof that boolean negation is involutive.
->   negb_involutive : (b : Bool) -> negb (negb b) = b
->   negb_involutive True  = Refl
->   negb_involutive False = Refl
+>   not_involutive : (b : Bool) -> not (not b) = b
+>   not_involutive True  = Refl
+>   not_involutive False = Refl
 >
 
 Note that the case splitting here doesn't introduce any variables because none
@@ -898,7 +902,7 @@ any names.
 It is sometimes useful to case split on more than one parameter, generating yet
 more proof obligations. For example:
 
->   andb_commutative : (b, c : Bool) -> andb b c = andb c b
+>   andb_commutative : (b, c : Bool) -> b && c = c && b
 >   andb_commutative True  True  = Refl
 >   andb_commutative True  False = Refl
 >   andb_commutative False True  = Refl
@@ -908,15 +912,15 @@ more proof obligations. For example:
 In more complex proofs, it is often better to lift subgoals to lemmas:
 
 
->   andb_commutative'_rhs_1 : (c : Bool) -> c = andb c True
+>   andb_commutative'_rhs_1 : (c : Bool) -> c = c && True
 >   andb_commutative'_rhs_1 True  = Refl
 >   andb_commutative'_rhs_1 False = Refl
 >
->   andb_commutative'_rhs_2 : (c : Bool) -> False = andb c False
+>   andb_commutative'_rhs_2 : (c : Bool) -> False = c && False
 >   andb_commutative'_rhs_2 True  = Refl
 >   andb_commutative'_rhs_2 False = Refl
 >
->   andb_commutative' : (b, c : Bool) -> andb b c = andb c b
+>   andb_commutative' : (b, c : Bool) -> b && c = c && b
 >   andb_commutative' True  = andb_commutative'_rhs_1
 >   andb_commutative' False = andb_commutative'_rhs_2
 >
@@ -926,7 +930,7 @@ In more complex proofs, it is often better to lift subgoals to lemmas:
 
 Prove the following claim, lift cases (and subcases) to lemmas when case split.
 
->   andb_true_elim_2 : (b, c : Bool) -> (andb b c = True) -> c = True
+>   andb_true_elim_2 : (b, c : Bool) -> (b && c = True) -> c = True
 >   andb_true_elim_2 b c prf = ?andb_true_elim_2_rhs
 >
 
@@ -988,7 +992,7 @@ boolean functions.
 
 Now state and prove a theorem \idr{negation_fn_applied_twice} similar to the
 previous one but where the second hypothesis says that the function \idr{f} has
-the property that \idr{f x = negb x}.
+the property that \idr{f x = not x}.
 
 >
 >   -- FILL IN HERE
@@ -1003,7 +1007,7 @@ Prove the following theorem. (You may want to first prove a subsidiary lemma or
 two. Alternatively, remember that you do not have to introduce all hypotheses at
 the same time.)
 
->   andb_eq_orb : (b, c : Bool) -> (andb b c = orb b c) -> b = c
+>   andb_eq_orb : (b, c : Bool) -> (b && c = b || c) -> b = c
 >   andb_eq_orb b c prf = ?andb_eq_orb_rhs
 
 $\square$

src/Induction.lidr

@@ -129,7 +129,7 @@ n} harder when done by induction on \idr{n}, since we may need an induction
 hypothesis about \idr{n - 2}. The following lemma gives a better
 characterization of \idr{evenb (S n)}:
 
-> evenb_S : (n : Nat) -> evenb (S n) = negb (evenb n)
+> evenb_S : (n : Nat) -> evenb (S n) = not (evenb n)
 > evenb_S n = ?evenb_S_rhs
 
 $\square$
@@ -236,7 +236,7 @@ your piece of paper; this is just to encourage you to reflect before you hack!)
 > zero_nbeq_S : (n : Nat) -> beq_nat 0 (S n) = False
 > zero_nbeq_S n = ?zero_nbeq_S_rhs
 
-> andb_false_r : (b : Bool) -> andb b False = False
+> andb_false_r : (b : Bool) -> b && False = False
 > andb_false_r b = ?andb_false_r_rhs
 
 > plus_ble_compat_l : (n, m, p : Nat) ->
@@ -250,10 +250,7 @@ your piece of paper; this is just to encourage you to reflect before you hack!)
 > mult_1_l n = ?mult_1_l_rhs
 
 > all3_spec : (b, c : Bool) ->
->             orb (andb b c)
->                 (orb (negb b)
->                      (negb c))
->             = True
+>             (b && c) || ((not b) || (not c)) = True
 > all3_spec b c = ?all3_spec_rhs
 
 > mult_plus_distr_r : (n, m, p : Nat) -> (n + m) * p = (n * p) + (m * p)

src/Poly.lidr

@@ -546,10 +546,14 @@ body of \idr{doit3times} applies \idr{f} three times to some value \idr{n}.
 -- doit3times : (x -> x) -> x -> x
 ```
 
+\todo[inline]{Explain that the prefixes are needed to avoid the implicit scoping
+rule, seems that this fires up more often when passing functions as parameters
+to other functions}
+
 > test_doit3times : doit3times Numbers.minusTwo 9 = 3
 > test_doit3times = Refl
 
-> test_doit3times' : doit3times Booleans.negb True = False
+> test_doit3times' : doit3times Bool.not True = False
 > test_doit3times' = Refl
 
 
@@ -775,12 +779,16 @@ yields
 
 Some more examples:
 
+\todo[inline]{We go back to \idr{andb} here because \idr{(&&)}'s second
+parameter is lazy, with the left fold the return type is inferred to be lazy
+too, leading to type mismatch.}
+
 ```idris
 λΠ> :t fold andb
 fold andb : List Bool -> Bool -> Bool
 ```
 
-> fold_example1 : fold Nat.mult [1,2,3,4] 1 = 24
+> fold_example1 : fold (*) [1,2,3,4] 1 = 24
 > fold_example1 = Refl
 
 > fold_example2 : fold Booleans.andb [True,True,False,True] True = False
@@ -849,11 +857,9 @@ if we like we can supply just the first. This is called _partial application_.
 > test_plus3 : plus3 4 = 7
 > test_plus3 = Refl
 
-\todo[inline]{This is apparently a bug in Idris,
-https://github.com/idris-lang/Idris-dev/issues/3908}
 
-> -- test_plus3' : doit3times plus3 0 = 9
-> -- test_plus3' = Refl
+> test_plus3' : doit3times Poly.plus3 0 = 9
+> test_plus3' = Refl
 
 > test_plus3'' : doit3times (plus 3) 0 = 9
 > test_plus3'' = Refl

src/Tactics.lidr

@@ -1,4 +1,4 @@
-= Tactics: More Basic Tactics
+= Tactics : More Basic Tactics
 
 This chapter introduces several additional proof strategies and tactics that
 allow us to begin proving more interesting properties of functional programs. We
@@ -1193,7 +1193,7 @@ checks whether every element in a list satisfies a given predicate:
 
       \idr{forallb oddb [1,3,5,7,9] = True}
 
-      \idr{forallb negb [False,False] = True}
+      \idr{forallb not [False,False] = True}
 
       \idr{forallb evenb [0,2,4,5] = False}
 
@@ -1204,14 +1204,14 @@ given predicate:
 
       \idr{existsb (beq_nat 5) [0,2,3,6] = False}
 
-      \idr{existsb (andb True) [True,True,False] = True}
+      \idr{existsb ((&&) True) [True,True,False] = True}
 
       \idr{existsb oddb [1,0,0,0,0,3] = True}
 
       \idr{existsb evenb [] = False}
 
 Next, define a _nonrecursive_ version of \idr{existsb} -- call it \idr{existsb'}
--- using \idr{forallb} and \idr{negb}.
+-- using \idr{forallb} and \idr{not}.
 
 Finally, prove a theorem \idr{existsb_existsb'} stating that \idr{existsb'} and
 \idr{existsb} have the same behavior.