fixes for latest Idris

Author: Alex Gryzlov

README.md

@@ -19,7 +19,7 @@ Others may work, but here are the versions I'm using.
 | Dependency       |                                Version |
 |------------------|----------------------------------------|
 | [(run)ghc][GHC]  |                                  8.0.2 |
-| [Idris][]        |                                    1.0 |
+| [Idris][]        |                                  1.1.1 |
 | [latexmk][]      |                                  4.52c |
 | [Make][]         |                                  4.2.1 |
 | [minted][]       |                                  2.4.1 |

software_foundations.ipkg

@@ -7,6 +7,7 @@ modules    = Basics
            , Tactics
            , Logic
            , IndProp
+           , Imp
 
 brief      = "Software Foundations in Idris"
 version    = 0.0.1.0

src/Imp.lidr

@@ -2,6 +2,8 @@
 
 > module Imp
 
+> import Logic
+
 In this chapter, we begin a new direction that will continue for the rest of the
 course. Up to now most of our attention has been focused on various aspects of
 Idris itself, while from now on we'll mostly be using Idris to formalize other
@@ -1085,9 +1087,9 @@ Here's an attempt at defining an evaluation function for commands, omitting the
 >   let st' = ceval_fun_no_while st c1
 >   in ceval_fun_no_while st' c2
 > ceval_fun_no_while st (CIf b c1 c2) =
->   ceval_fun_no_while st $ if beval st b
->                             then c1
->                             else c2
+>   if beval st b
+>     then ceval_fun_no_while st c1
+>     else ceval_fun_no_while st c2
 > ceval_fun_no_while st (CWhile b c) = st   -- bogus
 
 In a traditional functional programming language like OCaml or Haskell we could
@@ -1232,8 +1234,8 @@ rather than just letting Idris's computation mechanism do it for us.
 >     THEN (Y ::= ANum 3)
 >     ELSE (Z ::= ANum 4)
 >    FI)
->   ) / empty_state
->    |/ (t_update Z 4 $ t_update X 2 empty_state)
+>   ) / Imp.empty_state
+>    |/ (t_update Z 4 $ t_update X 2 Imp.empty_state)
 > ceval_example1 =
 >   E_Seq
 >     (E_Ass Refl)
@@ -1245,8 +1247,8 @@ rather than just letting Idris's computation mechanism do it for us.
 
 > ceval_example2 :
 >    ((X ::= ANum 0);; (Y ::= ANum 1);; (Z ::= ANum 2))
->    / empty_state
->   |/ (t_update Z 2 $ t_update Y 1 $ t_update X 0 empty_state)
+>    / Imp.empty_state
+>   |/ (t_update Z 2 $ t_update Y 1 $ t_update X 0 Imp.empty_state)
 > ceval_example2 = ?ceval_example2_rhs
 
 $\square$
@@ -1262,13 +1264,13 @@ as intended for \idr{X = 2} (this is trickier than you might expect).
 > pup_to_n = ?pup_to_n_rhs
 
 > pup_to_2_ceval :
->   pup_to_n / (t_update X 2 empty_state) |/
+>   Imp.pup_to_n / (t_update X 2 Imp.empty_state) |/
 >    (t_update X 0 $
 >     t_update Y 3 $
 >     t_update X 1 $
 >     t_update Y 2 $
 >     t_update Y 0 $
->     t_update X 2 empty_state)
+>     t_update X 2 Imp.empty_state)
 > pup_to_2_ceval = ?pup_to_2_ceval_rhs
 
 $\square$
@@ -1476,11 +1478,11 @@ will never emit such a malformed program.
 >             List Nat
 > s_execute st stack prog = ?s_execute_rhs
 
-> s_execute1 : s_execute empty_state [] [SPush 5, SPush 3, SPush 1, SMinus]
+> s_execute1 : s_execute Imp.empty_state [] [SPush 5, SPush 3, SPush 1, SMinus]
 >              = [2,5]
 > s_execute1 = ?s_execute1_rhs
 
-> s_execute2 : s_execute (t_update X 3 empty_state) [3,4]
+> s_execute2 : s_execute (t_update X 3 Imp.empty_state) [3,4]
 >                        [SPush 4, SLoad X, SMult, SPlus]
 >              = [15,4]
 > s_execute2 = ?s_execute2_rhs

src/IndProp.lidr

@@ -5,6 +5,8 @@
 > import Basics
 > import Induction
 >
+> %access public export
+>
 > %hide Basics.Numbers.pred
 > %hide Prelude.Stream.(::)
 >

src/Logic.lidr

@@ -4,15 +4,17 @@
 
 > import Basics
 
-> %hide Basics.Numbers.pred 
+> %access public export
+
+> %hide Basics.Numbers.pred
 > %hide Basics.Playground2.plus
 
 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
 \idr{e1 = e2}, with implications (\idr{p -> q}), and with quantified
 propositions (\idr{x -> P(x)}). In this chapter, we will see how Idris can be
-used to carry out other familiar forms of logical reasoning. 
+used to carry out other familiar forms of logical reasoning.
 
 Before diving into details, let's talk a bit about the status of mathematical
 statements in Idris. Recall that Idris is a _typed_ language, which means that
@@ -57,7 +59,7 @@ type signatures.
 But propositions can be used in many other ways. For example, we can give a name
 to a proposition as a value on its own, just as we have given names to
 expressions of other sorts (you'll soon see why we start the name with a capital
-letter). 
+letter).
 
 > Plus_fact : Type
 > Plus_fact = 2+2=4
@@ -82,7 +84,7 @@ arguments of some type and return a proposition. For instance, the following
 function takes a number and returns a proposition asserting that this number is
 equal to three:
 
-> is_three : Nat -> Type 
+> is_three : Nat -> Type
 > is_three n = n=3
 
 ```idris
@@ -171,8 +173,8 @@ intermediate steps in proofs, especially in bigger developments. Here's a simple
 example:
 
 > and_example3 : (n, m : Nat) -> n + m = 0 -> n * m = 0
-> and_example3 n m prf = 
->  let (nz, _) = and_exercise n m prf in 
+> and_example3 n m prf =
+>  let (nz, _) = and_exercise n m prf in
 >  rewrite nz in Refl
 
 \todo[inline]{Remove lemma and exercise, use \idr{fst} and \idr{snd} directly?}
@@ -344,7 +346,7 @@ Write an informal proof of \idr{double_neg}:
 
 _Theorem_: \idr{p} implies \idr{Not $ Not p}, for any proposition \idr{p}.
 
-> -- FILL IN HERE 
+> -- FILL IN HERE
 
 $\square$
 
@@ -369,7 +371,7 @@ $\square$
 
 Write an informal proof (in English) of the proposition \idr{Not (p, Not p)}.
 
-> -- FILL IN HERE 
+> -- FILL IN HERE
 
 $\square$
 
@@ -484,16 +486,16 @@ We can now use these facts with \idr{rewrite} and \idr{Refl} to give smooth
 proofs of statements involving equivalences. Here is a ternary version of the
 previous \idr{mult_0} result:
 
->   mult_0_3 : (n * m * p = Z) <-> 
+>   mult_0_3 : (n * m * p = Z) <->
 >              ((n = Z) `Either` ((m = Z) `Either` (p = Z)))
 >   mult_0_3 = (to, fro)
->   where 
+>   where
 >     to : (n * m * p = Z) -> ((n = Z) `Either` ((m = Z) `Either` (p = Z)))
->     to {n} {m} {p} prf = let 
+>     to {n} {m} {p} prf = let
 >       (nm_p_to, _) = mult_0 {n=(n*m)} {m=p}
 >       (n_m_to, _) = mult_0 {n} {m}
 >       (_, or_a_fro) = or_assoc {p=(n=Z)} {q=(m=Z)} {r=(p=Z)}
->       in or_a_fro $ case nm_p_to prf of 
+>       in or_a_fro $ case nm_p_to prf of
 >            Left prf => Left $ n_m_to prf
 >            Right prf => Right prf
 >     fro : ((n = Z) `Either` ((m = Z) `Either` (p = Z))) -> (n * m * p = Z)
@@ -504,7 +506,7 @@ previous \idr{mult_0} result:
 The apply tactic can also be used with \idr{<->}. When given an equivalence as
 its argument, apply tries to guess which side of the equivalence to use.
 
->    apply_iff_example : (n, m : Nat) -> n * m = Z -> ((n = Z) `Either` (m = Z))  
+>    apply_iff_example : (n, m : Nat) -> n * m = Z -> ((n = Z) `Either` (m = Z))
 >    apply_iff_example n m = fst $ mult_0 {n} {m}
 
 
@@ -549,7 +551,7 @@ $\square$
 
 Prove that existential quantification distributes over disjunction.
 
-> dist_exists_or : {p, q : a -> Type} -> (x ** (p x `Either` q x)) <-> 
+> dist_exists_or : {p, q : a -> Type} -> (x ** (p x `Either` q x)) <->
 >                                       ((x ** p x) `Either` (x ** q x))
 > dist_exists_or = ?dist_exists_or_rhs
 
@@ -593,7 +595,7 @@ We can also prove more generic, higher-level lemmas about \idr{In}.
 Note, in the next, how \idr{In} starts out applied to a variable and only gets
 expanded when we do case analysis on this variable:
 
-> In_map : (f : a -> b) -> (l : List a) -> (x : a) -> In x l -> 
+> In_map : (f : a -> b) -> (l : List a) -> (x : a) -> In x l ->
 >          In (f x) (map f l)
 > In_map _ [] _ ixl = absurd ixl
 > In_map f (x' :: xs) x (Left prf) = rewrite prf in Left Refl
@@ -609,7 +611,7 @@ set of strengths and limitations.
 
 ==== Exercise: 2 stars (In_map_iff)
 
-> In_map_iff : (f : a -> b) -> (l : List a) -> (y : b) -> 
+> In_map_iff : (f : a -> b) -> (l : List a) -> (y : b) ->
 >              (In y (map f l)) <-> (x ** (f x = y, In x l))
 > In_map_iff f l y = ?In_map_iff_rhs
 
@@ -758,7 +760,7 @@ A more elegant alternative is to apply \idr{plusCommutative} directly to the
 arguments we want to instantiate it with, in much the same way as we apply a
 polymorphic function to a type argument.
 
-> plus_comm3 n m p = rewrite plusCommutative n (m+p) in 
+> plus_comm3 n m p = rewrite plusCommutative n (m+p) in
 >                    rewrite plusCommutative m p in Refl
 
 You can "use theorems as functions" in this way with almost all tactics that
@@ -768,12 +770,12 @@ example, to supply wildcards as arguments to be inferred, or to declare some
 hypotheses to a theorem as implicit by default. These features are illustrated
 in the proof below.
 
-> lemma_application_ex : (n : Nat) -> (ns : List Nat) -> 
+> lemma_application_ex : (n : Nat) -> (ns : List Nat) ->
 >                        In n (map (\m => m * 0) ns) -> n = 0
 > lemma_application_ex _ [] prf = absurd prf
-> lemma_application_ex _ (y :: _) (Left prf) = 
+> lemma_application_ex _ (y :: _) (Left prf) =
 >   rewrite sym $ multZeroRightZero y in sym prf
-> lemma_application_ex n (_ :: xs) (Right prf) = 
+> lemma_application_ex n (_ :: xs) (Right prf) =
 >   lemma_application_ex n xs prf
 
 We will see many more examples of the idioms from this section in later chapters.
@@ -850,7 +852,7 @@ that this isn't just something we're going to come back and fill in later!
 We can now invoke functional extensionality in proofs:
 
 > function_equality_ex2 : (\x => plus x 1) = (\x => plus 1 x)
-> function_equality_ex2 = functional_extensionality $ \x => plusCommutative x 1 
+> function_equality_ex2 = functional_extensionality $ \x => plusCommutative x 1
 
 Naturally, we must be careful when adding new axioms into Idris's logic, as they
 may render it _inconsistent_ -- that is, they may make it possible to prove
@@ -883,7 +885,7 @@ Print Assumptions function_equality_ex2.
 One problem with the definition of the list-reversing function \idr{rev} that we
 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. 
+has quadratic running time.
 
 > rev : (l : List x) -> List x
 > rev [] = []
@@ -928,8 +930,8 @@ 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 : (n : Nat) -> Nat
+> double  Z    = Z
 > double (S k) = S (S (double k))
 
 > evenb_double : evenb (double k) = True
@@ -952,8 +954,8 @@ $\square$
 > where
 >   to : evenb n = True -> (k ** n = double k)
 >   to {n} prf = let
->     (k ** p) = evenb_double_conv {n} 
->   in 
+>     (k ** p) = evenb_double_conv {n}
+>   in
 
 \todo[inline]{Is there a shorter way?}
 
@@ -973,10 +975,10 @@ These two notions are equivalent.
 >  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 = beq_nat n n
 >  beq_nat_refl Z = Refl
->  beq_nat_refl (S k) = beq_nat_refl k 
+>  beq_nat_refl (S k) = beq_nat_refl k
 
 >  beq_nat_true_iff : (n1, n2 : Nat) -> (beq_nat n1 n2 = True) <-> (n1 = n2)
 >  beq_nat_true_iff n1 n2 = (to, fro n1 n2)
@@ -1068,11 +1070,11 @@ showing the complementary strengths of booleans and general propositions.
 The following lemmas relate the propositional connectives studied in this
 chapter to the corresponding boolean operations.
 
-> andb_true_iff : (b1, b2 : Bool) -> (b1 && b2 = True) <-> 
+> andb_true_iff : (b1, b2 : Bool) -> (b1 && b2 = True) <->
 >                                    (b1 = True, b2 = True)
 > andb_true_iff b1 b2 = ?andb_true_iff_rhs
 
-> orb_true_iff : (b1, b2 : Bool) -> (b1 || b2 = True) <-> 
+> orb_true_iff : (b1, b2 : Bool) -> (b1 || b2 = True) <->
 >                                   ((b1 = True) `Either` (b2 = True))
 > orb_true_iff b1 b2 = ?orb_true_iff_rhs
 
@@ -1102,7 +1104,7 @@ function below. To make sure that your definition is correct, prove the lemma
 > beq_list : (beq : a -> a -> Bool) -> (l1, l2 : List a) -> Bool
 > beq_list beq l1 l2 = ?beq_list_rhs
 
-> beq_list_true_iff : (beq : a -> a -> Bool) -> 
+> beq_list_true_iff : (beq : a -> a -> Bool) ->
 >                     ((a1, a2 : a) -> (beq a1 a2 = True) <-> (a1 = a2)) ->
 >       ((l1, l2 : List a) -> (beq_list beq l1 l2 = True) <-> (l1 = l2))
 > beq_list_true_iff beq f l1 l2 = ?beq_list_true_iff_rhs
@@ -1118,18 +1120,18 @@ Recall the function \idr{forallb}, from the exercise
 > forallb : (test : x -> Bool) -> (l : List x) -> Bool
 > forallb _ [] = True
 > forallb test (x :: xs) = test x && forallb test xs
-  
+
 Prove the theorem below, which relates \idr{forallb} to the \idr{All} property
 of the above exercise.
 
-> forallb_true_iff : (l : List x) -> (forallb test l = True) <-> 
+> forallb_true_iff : (l : List x) -> (forallb test l = True) <->
 >                                    (All (\x => test x = True) l)
 > forallb_true_iff l = ?forallb_true_iff_rhs
 
 Are there any important properties of the function \idr{forallb} which are not
 captured by this specification?
 
-> -- FILL IN HERE 
+> -- FILL IN HERE
 
 $\square$
 
@@ -1158,12 +1160,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
@@ -1174,9 +1170,9 @@ natural numbers \idr{n} and \idr{m}.
 \todo[inline]{Is there a simpler way to write this? Maybe with setoids?}
 
 > restricted_excluded_middle_eq : (n, m : Nat) -> (n = m) `Either` Not (n = m)
-> restricted_excluded_middle_eq n m = 
+> restricted_excluded_middle_eq n m =
 >   restricted_excluded_middle (to n m, fro n m)
-> where 
+> where
 >   to : (n, m : Nat) -> (n=m) -> (n==m)=True
 >   to Z Z prf = Refl
 >   to Z (S _) Refl impossible

src/Makefile

@@ -18,7 +18,9 @@ LIDR_FILES := Preface.lidr \
 	Poly.lidr \
 	Tactics.lidr \
 	Logic.lidr \
-	IndProp.lidr
+	IndProp.lidr \
+	Imp.lidr
+
 # TODO: Add more chapters, in order, here.