beq_nat -> (==), fix some todos

Author: Alex Gryzlov

src/Basics.lidr

@@ -627,16 +627,19 @@ simply instructions to the Idris parser to accept \idr{x + y} in place of
 \idr{plus x y} and, conversely, to the Idris pretty-printer to display \idr{plus
 x y} as \idr{x + y}.
 
-The \idr{beq_nat} function tests \idr{Nat}ural numbers for \idr{eq}uality,
-yielding a \idr{b}oolean.
+\todo[inline]{Mention interfaces here? Say this is infix}
 
->   ||| Test natural numbers for equality.
->   beq_nat : (n, m : Nat) -> Bool
->   beq_nat  Z     Z    = True
->   beq_nat  Z    (S j) = False
->   beq_nat (S k)  Z    = False
->   beq_nat (S k) (S j) = beq_nat k j
->
+The \idr{(==)} function tests \idr{Nat}ural numbers for equality, yielding a
+\idr{Bool}ean.
+
+```idris
+  ||| Test natural numbers for equality.
+  (==) : (n, m : Nat) -> Bool
+  (==)  Z     Z    = True
+  (==)  Z    (S j) = False
+  (==) (S k)  Z    = False
+  (==) (S k) (S j) = (==) k j
+```
 
 The \idr{lte} function tests whether its first argument is less than or equal to
 its second argument, yielding a boolean.
@@ -839,28 +842,28 @@ can block simplification. For example, if we try to prove the following fact
 using the \idr{Refl} tactic as above, we get stuck.
 
 ```idris
-plus_1_neq_0_firsttry : (n : Nat) -> beq_nat (n + 1) 0 = False
+plus_1_neq_0_firsttry : (n : Nat) -> (n + 1) == 0 = False
 plus_1_neq_0_firsttry n = Refl -- does nothing!
 ```
 
-The reason for this is that the definitions of both \idr{beq_nat} and \idr{+}
+The reason for this is that the definitions of both \idr{(==)} and \idr{+}
 begin by performing a \idr{match} on their first argument. But here, the first
 argument to \idr{+} is the unknown number \idr{n} and the argument to
-\idr{beq_nat} is the compound expression \idr{n + 1}; neither can be simplified.
+\idr{(==)} is the compound expression \idr{n + 1}; neither can be simplified.
 
 To make progress, we need to consider the possible forms of \idr{n} separately.
-If \idr{n} is \idr{Z}, then we can calculate the final result of \idr{beq_nat (n
-+ 1) 0} and check that it is, indeed, \idr{False}. And if \idr{n = S k} for some
+If \idr{n} is \idr{Z}, then we can calculate the final result of \idr{(n + 1) ==
+0} and check that it is, indeed, \idr{False}. And if \idr{n = S k} for some
 \idr{k}, then, although we don't know exactly what number \idr{n + 1} yields, we
 can calculate that, at least, it will begin with one \idr{S}, and this is enough
-to calculate that, again, \idr{beq_nat (n + 1) 0} will yield \idr{False}.
+to calculate that, again, \idr{(n + 1) == 0} will yield \idr{False}.
 
 To tell Idris to consider, separately, the cases where \idr{n = Z} and where
 \idr{n = S k}, simply case split on \idr{n}.
 
 \todo[inline]{Mention case splitting interactively in Emacs, Atom, etc.}
 
->   plus_1_neq_0 : (n : Nat) -> beq_nat (n + 1) 0 = False
+>   plus_1_neq_0 : (n : Nat) -> (n + 1) == 0 = False
 >   plus_1_neq_0  Z    = Refl
 >   plus_1_neq_0 (S k) = Refl
 >
@@ -870,8 +873,8 @@ separately, in order to get Idris to accept the theorem.
 
 In this example, each of the holes is easily filled by a single use of
 \idr{Refl}, which itself performs some simplification -- e.g., the first one
-simplifies \idr{beq_nat (S k + 1) 0} to \idr{False} by first rewriting \idr{(S k
-+ 1)} to \idr{S (k + 1)}, then unfolding \idr{beq_nat}, simplifying its pattern
+simplifies \idr{(S k + 1) == 0} to \idr{False} by first rewriting \idr{(S k +
+1)} to \idr{S (k + 1)}, then unfolding \idr{(==)}, simplifying its pattern
 matching.
 
 There are no hard and fast rules for how proofs should be formatted in Idris.
@@ -939,7 +942,7 @@ $\square$
 
 ==== Exercise: 1 star (zero_nbeq_plus_1)
 
->   zero_nbeq_plus_1 : (n : Nat) -> beq_nat 0 (n + 1) = False
+>   zero_nbeq_plus_1 : (n : Nat) -> 0 == (n + 1) = False
 >   zero_nbeq_plus_1 n = ?zero_nbeq_plus_1_rhs
 >
 

src/IndProp.lidr

@@ -1245,42 +1245,42 @@ the following theorem:
 
 \todo[inline]{Copy here for now}
 
-> beq_nat_true : beq_nat n m = True -> n = m
+> 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 : Not (filter (beq_nat n) l = []) -> In n l
+> 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 (beq_nat n x) proof h
+> filter_not_empty_In {l=(x::_)} {n} contra with (n == x) proof h
 >   filter_not_empty_In contra | True =
 >     Left $ sym $ beq_nat_true $ sym h
 >   filter_not_empty_In contra | False =
 >     Right $ filter_not_empty_In contra
 >
 
 In the second case we explicitly apply the \idr{beq_nat_true} lemma to the
-equation generated by doing a dependent match on \idr{beq_nat n x}, to convert
-the assumption \idr{beq_nat n x = True} into the assumption \idr{n = m}.
+equation generated by doing a dependent match on \idr{n == x}, to convert the
+assumption \idr{n == x = True} into the assumption \idr{n = m}.
 
 We can streamline this by defining an inductive proposition that yields a better
-case-analysis principle for \idr{beq_nat n m}. Instead of generating an equation
-such as \idr{beq_nat n m = True}, which is generally not directly useful, this
-principle gives us right away the assumption we really need: \idr{n = m}.
+case-analysis principle for \idr{n == m}. Instead of generating an equation such
+as \idr{n == m = True}, which is generally not directly useful, this principle
+gives us right away the assumption we really need: \idr{n = m}.
 
 We'll actually define something a bit more general, which can be used with
 arbitrary properties (and not just equalities):
 
+\todo[inline]{Update the text: seems that additional \idr{(b=...)} constructor
+parameter is needed for this to work in Idris.}
+
 ```idris
 data Reflect : Type -> Bool -> Type where
-  ReflectT : (p : Type) -> Reflect p True
-  ReflectF : (p : Type) -> (Not p) -> Reflect p False
-```
-
-\todo[inline]{Seems that additional `(b=True/False)` constructor parameter is
-needed for this to work in Idris. Update the text.`}
+ ReflectT : (p : Type) -> (b=True) -> Reflect p b
+ ReflectF : (p : Type) -> (Not p) -> (b=False) -> Reflect p b
+ ```
 
 Before explaining this, let's rearrange it a little: Since the types of both
 \idr{ReflectT} and \idr{ReflectF} begin with \idr{(p : Type)}, we can make the
@@ -1327,18 +1327,18 @@ the second).
 
 \todo[inline]{Copy here for now}
 
-> beq_nat_true_iff : (n1, n2 : Nat) -> (beq_nat n1 n2 = True) <-> (n1 = n2)
+> beq_nat_true_iff : (n1, n2 : Nat) -> (n1 == n2 = True) <-> (n1 = n2)
 > beq_nat_true_iff n1 n2 = (to, fro n1 n2)
 >   where
->     to : (beq_nat n1 n2 = True) -> (n1 = n2)
+>     to : (n1 == n2 = True) -> (n1 = n2)
 >     to = beq_nat_true {n=n1} {m=n2}
->     fro : (n1, n2 : Nat) -> (n1 = n2) -> (beq_nat n1 n2 = True)
+>     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 : Reflect (n = m) (beq_nat n m)
+> beq_natP : {n, m : Nat} -> Reflect (n = m) (n == m)
 > beq_natP {n} {m} = iff_reflect $ iff_sym $ beq_nat_true_iff n m
 >
 
@@ -1352,7 +1352,7 @@ calls to destruct and apply are combined into a single call to destruct.
 Idris and observe the differences in proof state at the beginning of the first
 case of the destruct.)
 
-> filter_not_empty_In' : Not (filter (beq_nat n) l = []) -> In n l
+> 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' {n} {l=(x::xs)} contra with (beq_natP {n} {m=x})
 >   filter_not_empty_In' _ | (ReflectT eq _) = Left $ sym eq
@@ -1364,8 +1364,8 @@ case of the destruct.)
 >       contra' = replace notbeq contra
 >                         {P = \a =>
 >                                Not ((if a
->                                         then x :: filter (beq_nat n) xs
->                                         else filter (beq_nat n) xs) = [])}
+>                                         then x :: filter ((==) n) xs
+>                                         else filter ((==) n) xs) = [])}
 >     in
 >       Right $ filter_not_empty_In' contra'
 >
@@ -1377,7 +1377,7 @@ Use \idr{beq_natP} as above to prove the following:
 
 > count : (n : Nat) -> (l : List Nat) -> Nat
 > count _ [] = 0
-> count n (x :: xs) = (if beq_nat n x then 1 else 0) + count n xs
+> count n (x :: xs) = (if n == x then 1 else 0) + count n xs
 >
 > beq_natP_practice : count n l = 0 -> Not (In n l)
 > beq_natP_practice prf = ?beq_natP_practice_rhs

src/Induction.lidr

@@ -233,7 +233,7 @@ your piece of paper; this is just to encourage you to reflect before you hack!)
 > lte_refl : (n : Nat) -> True = lte n n
 > lte_refl n = ?lte_refl_rhs
 
-> zero_nbeq_S : (n : Nat) -> beq_nat 0 (S n) = False
+> zero_nbeq_S : (n : Nat) -> 0 == (S n) = False
 > zero_nbeq_S n = ?zero_nbeq_S_rhs
 
 > andb_false_r : (b : Bool) -> b && False = False
@@ -243,7 +243,7 @@ your piece of paper; this is just to encourage you to reflect before you hack!)
 >                     lte n m = True -> lte (p + n) (p + m) = True
 > plus_ble_compat_l n m p prf = ?plus_ble_compat_l_rhs
 
-> S_nbeq_0 : (n : Nat) -> beq_nat (S n) 0 = False
+> S_nbeq_0 : (n : Nat) -> (S n) == 0 = False
 > S_nbeq_0 n = ?S_nbeq_0_rhs
 
 > mult_1_l : (n : Nat) -> 1 * n = n
@@ -272,7 +272,7 @@ standard library, so we follow suit. Rewriting works equally well in either
 direction, so we will have no problem using the theorem no matter which way we
 state it.)
 
-> beq_nat_refl : (n : Nat) -> True = beq_nat n n
+> beq_nat_refl : (n : Nat) -> True = n == n
 > beq_nat_refl n = ?beq_nat_refl_rhs
 
 $\square$

src/Lists.lidr

@@ -820,7 +820,7 @@ some number to return when the list is too short...
 
 > nth_bad : (l : NatList) -> (n : Nat) -> Nat
 > nth_bad Nil n = 42 -- arbitrary!
-> nth_bad (a :: l') n = case beq_nat n 0 of
+> nth_bad (a :: l') n = case n == 0 of
 >                         True => a
 >                         False => nth_bad l' (pred n)
 
@@ -840,7 +840,7 @@ to indicate that it may result in an error.
 
 > nth_error : (l : NatList) -> (n : Nat) -> NatOption
 > nth_error Nil n = None
-> nth_error (a :: l') n = case beq_nat n 0 of
+> nth_error (a :: l') n = case n == 0 of
 >                           True => Some a
 >                           False => nth_error l' (pred n)
 
@@ -858,7 +858,7 @@ programming language: conditional expressions...
 
 > nth_error' : (l : NatList) -> (n : Nat) -> NatOption
 > nth_error' Nil n = None
-> nth_error' (a :: l') n = if beq_nat n 0
+> nth_error' (a :: l') n = if n == 0
 >                            then Some a
 >                            else nth_error' l' (pred n)
 
@@ -927,7 +927,7 @@ and gives us the flexibility to change representations later if we wish.
 We'll also need an equality test for \idr{Id}s:
 
 > beq_id : (x1, x2 : Id) -> Bool
-> beq_id (MkId n1) (MkId n2) = beq_nat n1 n2
+> beq_id (MkId n1) (MkId n2) = n1 == n2
 
 
 ==== Exercise: 1 star (beq_id_refl)