text:
-- USAGE: $ idris2 -q -p effects -x main shell-effects.idr
-- FAIL: no "Effects" in Idris2

-- SRC: https://stackoverflow.com/questions/39812465/how-can-i-call-a-subprocess-in-idris
-- http://docs.idris-lang.org/en/latest/effects/index.html

import Effects
import Effect.System
import Effect.StdIO

execAndPrint : (cmd : String) -> Eff () [STDIO, SYSTEM]
execAndPrint cmd = do
  exitCode <- system cmd
  putStrLn $ "Exit code: " ++ show exitCode

script : Eff () [STDIO, SYSTEM]
script = do
  execAndPrint "echo HelloWorld!"
  execAndPrint "sh -c \"echo HelloWorld!; exit 1\""

main : IO ()
main = run script

max_stars_repo_name: amerlyq/aeternum-langs

max_issues_repo_name: amerlyq/aeternum-langs

max_forks_repo_name: amerlyq/aeternum-langs


text:
-- 自己写的一个一个链表翻转程序和验证程序

{- 翻转函数 -}
myreverse : List a-> List a
myreverse [] = []
myreverse (x::xs) = myreverse xs ++ [x]

{- 引理1 -}
app_nil_r : (l:List a)->(l++[]=l)
app_nil_r [] = Refl
app_nil_r (x::xs) =
    let ind_xs = app_nil_r xs in
        rewrite ind_xs in Refl

{- 引理2：结合性 -}
app_assoc : (l1: List a) -> (l2 : List a) -> (l3:List a) -> ((l1++l2)++l3=l1++(l2++l3))
app_assoc [] l2 l3 = Refl
app_assoc (x::xs) l2 l3 =
    let ind_xs = app_assoc xs l2 l3 in
        rewrite ind_xs in Refl

{- 引理3：分配律 -}
app_distr : (l1:List a)->(l2:List a)->(myreverse (l1++l2)=myreverse l2++myreverse l1)
app_distr [] l2 =
    rewrite app_nil_r (myreverse l2) in Refl
app_distr (x::xs) l2 =
    rewrite app_distr xs l2 in
        rewrite app_assoc (myreverse l2) (myreverse xs) [x] in Refl

{- 定理：链表翻转的函数的逆元是其自身 -}
myreverseSym : (l:List a)->(l=myreverse (myreverse l))
myreverseSym [] = Refl
myreverseSym (x::xs) =
    let ind_xs = myreverseSym xs in
        rewrite app_distr (myreverse xs) [x] in
            rewrite ind_xs in Refl

ext: idr

max_stars_repo_name: shij-hsu/idr

max_issues_repo_name: shij-hsu/idr

max_forks_repo_name: shij-hsu/idr


text:
module Control.Monad.Identity

import Data.Bits

%default total

public export
record Identity (a : Type) where
  constructor Id
  runIdentity : a

public export
Functor Identity where
    map fn (Id a) = Id (fn a)

public export
Applicative Identity where
    pure x = Id x
    (Id f) <*> (Id g) = Id (f g)

public export
Monad Identity where
    (Id x) >>= k = k x

public export
Show a => Show (Identity a) where
  showPrec d (Id x) = showCon d "Id" $ showArg x

public export
Eq a => Eq (Identity a) where
  (Id x) == (Id y) = x == y

public export
Ord a => Ord (Identity a) where
  compare (Id x) (Id y) = compare x y

-- public export
-- Enum a => Enum (Identity a) where
--   toNat (Id x) = toNat x
--   fromNat n = Id $ fromNat n
--   pred (Id n) = Id $ pred n

public export
Semigroup a => Semigroup (Identity a) where
  (<+>) x y = Id (runIdentity x <+> runIdentity y)

public export
Monoid a => Monoid (Identity a) where
  neutral = Id (neutral)

public export
Num a => Num (Identity a) where
  Id x + Id y = Id (x + y)
  Id x * Id y = Id (x * y)
  fromInteger = Id . fromInteger

public export
Neg a => Neg (Identity a) where
  negate (Id x)    = Id (negate x)
  Id x - Id y = Id (x - y)

public export
Abs a => Abs (Identity a) where
  abs (Id x)    = Id (abs x)

public export
Fractional a => Fractional (Identity a) where
  recip (Id x)     = Id (recip x)
  Id x / Id y = Id (x / y)

public export
Integral a => Integral (Identity a) where
  Id x `div` Id y = Id (x `div` y)
  Id x `mod` Id y = Id (x `mod` y)

public export
Bits a => Bits (Identity a) where
  Index = Index {a}
  Id x .&. Id y = Id (x .&. y)
  Id x .|. Id y = Id (x .|. y)
  Id x `xor` Id y = Id (x `xor` y)
  shiftL (Id v) ix = Id (shiftL v ix)
  shiftR (Id v) ix = Id (shiftR v ix)
  bit = Id . bit
  zeroBits = Id zeroBits
  complement (Id v) = Id (complement v)
  oneBits = Id oneBits
  complementBit (Id v) ix = Id (complementBit v ix)
  clearBit (Id v) ix = Id (clearBit v ix)
  testBit (Id v) ix = testBit v ix
  setBit (Id v) ix = Id (setBit v ix)

public export
FromString a => FromString (Identity a) where
  fromString = Id . fromString


text:
-- Define module to wrap constants starting with lower case to not
-- confuse them with implicitly bound argument.  See
-- https://docs.idris-lang.org/en/latest/faq/faq.html#why-can-t-i-use-a-function-with-no-arguments-in-a-type
module Halfer

import public RealizedFunction

%default total

-- Realized halfer
public export
halfer : Int -> Int
halfer = (flip div 2)

public export
halfer_attrs : RealizedAttributes
halfer_attrs = MkRealizedAttributes (MkCosts 300 30 3) 0.8

public export
rlz_halfer : RealizedFunction (Int -> Int) Halfer.halfer_attrs
rlz_halfer = MkRealizedFunction halfer halfer_attrs

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
module Foo

-- fact'' : ((Nat -> Nat) -> (Nat -> Nat))
-- fact'' f1 = (\x => case x of
--                         Z => Z
--                         (S k) => (S k) * (f1 k))

-- fact' : ((Nat -> Nat) -> (Nat -> Nat)) -> Nat -> Nat
-- fact' f = f (\y => f
-- fact' f (S k) = (S k) * (f k)

-- fact : Nat -> Nat
-- fact x = fact' fact' x

--cant do y combinator, because can't specify type of self within self
-- part-fact : ((Nat -> Nat) -> Nat -> Nat) -> Nat -> Nat
-- part-fact self n =
--   case n of
--     Z => 1
--     (S k) => (* (S k) (self self k))


text:
module Replica.Command.New

import Data.List
import Data.List1
import Data.String
import System.Path

import Replica.Help
import public Replica.Option.Types
import Replica.Other.Decorated

public export
data FileFormat = JSON | Dhall

export
Show FileFormat where
  show JSON = "JSON"
  show Dhall = "Dhall"

public export
record NewCommand' (f : Type -> Type) where
  constructor MkNewCommand
  format : f FileFormat
  includeSample : f Bool
  file : f String

public export
NewCommand : Type
NewCommand = Done NewCommand'

TyMap NewCommand' where
  tyMap func x =
    MkNewCommand
      (func x.format)
      (func x.includeSample)
      (func x.file)

TyTraversable NewCommand' where
  tyTraverse func x = [|
    MkNewCommand
      (func x.format)
      (func x.includeSample)
      (func x.file)
      |]

Show NewCommand where
  show x = unwords
    [ "MkNewCommand"
    , show x.format
    , show x.includeSample
    , show x.file
    ]

formatPart : Part (Builder NewCommand') FileFormat
formatPart = inj $ MkOption
  (singleton $ MkMod (singleton "format") ['f']
    (Right $ MkValue "FORMAT" (parseFormat . toLower))
    "format of the file to create (json|dhall)")
  Dhall
  go
  where
    parseFormat : String -> Maybe FileFormat
    parseFormat "json" = Just JSON
    parseFormat "dhall"= Just Dhall
    parseFormat x = Nothing
    go : FileFormat -> Builder NewCommand' -> Either String (Builder NewCommand')
    go = one format
             (\x => record {format = Right x})
             (\x, y => "More than one format given: \{show y}, \{show x}")

includeSamplePart : Part (Builder NewCommand') Bool
includeSamplePart = inj $ MkOption (toList1
      [ MkMod (singleton "includeSample") ['s'] (Left True)
            "include a sample test"
      , MkMod (singleton "noSample") ['S'] (Left False)
            "no sample test"
      ])
      True
      go
  where
    go : Bool -> Builder NewCommand' -> Either String (Builder NewCommand')
    go = ifSame includeSample
                (\x => record {includeSample = Right x})
                (const $ const "Contradictory values for includeSample")

fileParamPart : Part (Builder NewCommand') String
fileParamPart = inj $ MkParam1 "NEW_TEST_FILE" Just go
  where
    checkFileType : String -> Maybe FileFormat
    checkFileType "json" = Just JSON
    checkFileType "dhall" = Just Dhall
    checkFileType x = Nothing
    setFile : String -> Builder NewCommand' -> Builder NewCommand'
    setFile f = record {file = Right f}
    setFileAndFormat : String -> FileFormat -> Builder NewCommand' -> Builder NewCommand'
    setFileAndFormat f fmt = record {file = Right f, format = Right fmt}
    go : String -> Builder NewCommand' -> Either String (Builder NewCommand')
    go = one file
             (\x, cmd => case cmd.format of
                 Left _ => maybe
                   (setFile x cmd)
                   (\fmt => setFileAndFormat x fmt cmd)
                   (checkFileType =<< (toLower <$> extension x))
                 Right _ => setFile x cmd
             )
             (const $ const $"Can't write more than one test file")

export
optParseNew : OptParse (Builder NewCommand') NewCommand
optParseNew =
  [| MkNewCommand
     (liftAp formatPart)
     (liftAp includeSamplePart)
     (liftAp fileParamPart)
  |]

export
defaultNew : Default NewCommand'
defaultNew =
  MkNewCommand
    (defaultPart formatPart)
    (defaultPart includeSamplePart)
    (defaultPart fileParamPart)

export
parseNew : List1 String -> ParseResult NewCommand
parseNew ("new":::xs) = do
  case parse (initBuilder defaultNew) optParseNew xs of
         InvalidMix reason => InvalidMix reason
         InvalidOption ys  => InvalidMix $ "Unknown option: " ++ ys.head
         Done builder      => maybe (InvalidMix "No test file given") Done $ build builder
parseNew xs = InvalidOption xs

export
helpNew : Help
helpNew = commandHelp {b = Builder NewCommand'}
  "new" "Create test files"
  optParseNew
  (Just "NEW_TEST_FILE")

max_stars_repo_name: claymager/REPLica

max_issues_repo_name: claymager/REPLica

max_forks_repo_name: claymager/REPLica


text:
= Logic : Logic in Idris

> 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
\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.

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
every sensible expression in its world has an associated type. Logical claims
are no exception: any statement we might try to prove in Idris has a type,
namely \idr{Type}, the type of _propositions_. We can see this with the \idr{:t}
command:

```idris
λΠ> :t 3 = 3
3 = 3 : Type
```

```idris
λΠ> :t (n, m : Nat) -> n + m = m + n
(n : Nat) -> (m : Nat) -> n + m = m + n : Type
```

Note that _all_ syntactically well-formed propositions have type \idr{Type} in
Idris, regardless of whether they are true or not.

Simply being a proposition is one thing; being provable is something else!

```idris
λΠ> :t (n : Nat) -> n = 2
(n : Nat) -> n = 2 : Type
```

```idris
λΠ> :t 3 = 4
3 = 4 : Type
```

Indeed, propositions don't just have types: they are _first-class objects_ that
can be manipulated in the same ways as the other entities in Idris's world. So
far, we've seen one primary place that propositions can appear: in functions'
type signatures.

> plus_2_2_is_4 : 2 + 2 = 4
> plus_2_2_is_4 = Refl

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).

> Plus_fact : Type
> Plus_fact = 2+2=4

```idris
λΠ> :t Plus_fact
Plus_fact : Type
```

We can later use this name in any situation where a proposition is expected --
for example, in a function declaration.

> plus_fact_is_true : Plus_fact
> plus_fact_is_true = Refl

(Here's the reason - recall that names starting with lowercase letters are
considered implicits in Idris, so \idr{plus_fact} would be considered a free
variable!)

We can also write _parameterized_ propositions -- that is, functions that take
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 n = n=3

```idris
λΠ> :t is_three
is_three : Nat -> Type
```

In Idris, functions that return propositions are said to define _properties_ of
their arguments.

For instance, here's a (polymorphic) property defining the familiar notion of an
_injective function_.

> Injective : (f : a -> b) -> Type
> Injective {a} {b} f = (x, y : a) -> f x = f y -> x = y

> succ_inj : Injective S
> succ_inj x x Refl = Refl

The equality operator \idr{=} is also a function that returns a \idr{Type}.

The expression \idr{n = m} is syntactic sugar for \idr{(=) n m}, defined
internally in Idris. Because \idr{=} can be used with elements of any type, it
is also polymorphic:

```idris
λΠ> :t (=)
(=) : A -> B -> Type
```

== Logical Connectives

=== Conjunction

The _conjunction_ (or _logical and_) of propositions \idr{a} and \idr{b} in
Idris is the same as the pair of \idr{a} and \idr{b}, written \idr{(a, b)},
representing the claim that both \idr{a} and \idr{b} are true.

> and_example : (3 + 4 = 7, 2 * 2 = 4)

To prove a conjunction, we can use value-level pair syntax:

> and_example = (Refl, Refl)

For any propositions \idr{a} and \idr{b}, if we assume that \idr{a} is true and
we assume that \idr{b} is true, we can trivially conclude that \idr{(a,b)} is
also true.

> and_intro : a -> b -> (a, b)
> and_intro = MkPair

==== Exercise: 2 stars (and_exercise)

> and_exercise : (n, m : Nat) -> n + m = 0 -> (n = 0, m = 0)
> and_exercise n m prf = ?and_exercise_rhs

$\square$

So much for proving conjunctive statements. To go in the other direction --
i.e., to _use_ a conjunctive hypothesis to help prove something else -- we
employ pattern matching.

If the proof context contains a hypothesis \idr{h} of the form \idr{(a,b)}, case
splitting will replace it with a pair pattern \idr{(a,b)}.

> and_example2 : (n, m : Nat) -> (n = 0, m = 0) -> n + m = 0
> and_example2 Z Z (Refl,Refl) = Refl
> and_example2 (S _) _ (Refl,_) impossible
> and_example2 _ (S _) (_,Refl) impossible

You may wonder why we bothered packing the two hypotheses \idr{n = 0} and \idr{m
= 0} into a single conjunction, since we could have also stated the theorem with
two separate premises:

> and_example2' : (n, m : Nat) -> n = 0 -> m = 0 -> n + m = 0
> and_example2' Z Z Refl Refl = Refl
> and_example2' (S _) _ Refl _ impossible
> and_example2' _ (S _) _ Refl impossible

For this theorem, both formulations are fine. But it's important to understand
how to work with conjunctive hypotheses because conjunctions often arise from
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
>  rewrite nz in Refl

\todo[inline]{Remove lemma and exercise, use \idr{fst} and \idr{snd} directly?}

Another common situation with conjunctions is that we know \idr{(a,b)} but in
some context we need just \idr{a} (or just \idr{b}). The following lemmas are
useful in such cases:

> proj1 : (p, q) -> p
> proj1 = fst

==== Exercise: 1 star, optional (proj2)

> proj2 : (p, q) -> q
> proj2 x = ?proj2_rhs

$\square$

Finally, we sometimes need to rearrange the order of conjunctions and/or the
grouping of multi-way conjunctions. The following commutativity and
associativity theorems are handy in such cases.

> and_commut : (p, q) -> (q, p)
> and_commut (p, q) = (q, p)

==== Exercise: 2 stars (and_assoc)

\todo[inline]{Remove or demote to 1 star?}

> and_assoc : (p, (q, r)) -> ((p, q), r)
> and_assoc x = ?and_assoc_rhs

$\square$

=== Disjunction

\todo[inline]{Hide \idr{Basics.Booleans} analogues and make syntax synonyms
\idr{(/\)} and \idr{(\/)} for \idr{(,)} and \idr{Either}?}

Another important connective is the _disjunction_, or _logical or_ of two
propositions: \idr{a `Either` b} is true when either \idr{a} or \idr{b} is. The
first case has be tagged with \idr{Left}, and the second with \idr{Right}.

To use a disjunctive hypothesis in a proof, we proceed by case analysis, which,
as for \idr{Nat} or other data types, can be done with pattern matching. Here is
an example:

> or_example : (n, m : Nat) -> ((n = 0) `Either` (m = 0)) -> n * m = 0
> or_example Z _ (Left Refl) = Refl
> or_example (S _) _ (Left Refl) impossible
> or_example n Z (Right Refl) = multZeroRightZero n
> or_example _ (S _) (Right Refl) impossible

Conversely, to show that a disjunction holds, we need to show that one of its
sides does. This can be done via aforementioned \idr{Left} and \idr{Right}
constructors. Here is a trivial use...

> or_intro : a -> a `Either` b
> or_intro = Left

... and a slightly more interesting example requiring both \idr{Left} and
\idr{Right}:

> zero_or_succ : (n : Nat) -> ((n = 0) `Either` (n = S (pred n)))
> zero_or_succ Z = Left Refl
> zero_or_succ (S _) = Right Refl

==== Exercise: 1 star (mult_eq_0)

> mult_eq_0 : n * m = 0 -> ((n = 0) `Either` (m = 0))
> mult_eq_0 prf = ?mult_eq_0_rhs

$\square$

==== Exercise: 1 star (or_commut)

> or_commut : (p `Either` q) -> (q `Either` p)
> or_commut x = ?or_commut_rhs

$\square$

=== Falsehood and Negation

So far, we have mostly been concerned with proving that certain things are
_true_ -- addition is commutative, appending lists is associative, etc. Of
course, we may also be interested in _negative_ results, showing that certain
propositions are _not_ true. In Idris, such negative statements are expressed
with the negation typelevel function \idr{Not}.

\todo[inline]{Add hyperlink}

To see how negation works, recall the discussion of the _principle of explosion_
from the previous chapter; it asserts that, if we assume a contradiction, then
any other proposition can be derived. Following this intuition, we could define
\idr{Not p} as \idr{q -> (p -> q)}. Idris actually makes a slightly different
choice, defining \idr{Not p} as \idr{p -> Void}, where \idr{Void} is a
_particular_ contradictory proposition defined in the standard library as a
data type with no constructors.

```idris
data Void : Type where

Not : Type -> Type
Not a = a -> Void
```

\todo[inline]{Discuss difference between \idr{void} and \idr{absurd}}

Since \idr{Void} is a contradictory proposition, the principle of explosion also
applies to it. If we get \idr{Void} into the proof context, we can call
\idr{void} or \idr{absurd} on it to complete any goal:

> ex_falso_quodlibet : Void -> p
> ex_falso_quodlibet = void

The Latin _ex falso quodlibet_ means, literally, "from falsehood follows
whatever you like"; this is another common name for the principle of explosion.

==== Exercise: 2 stars, optional (not_implies_our_not)

Show that Idris's definition of negation implies the intuitive one mentioned
above:

> not_implies_our_not : Not p -> (q -> (p -> q))
> not_implies_our_not notp q p = ?not_implies_our_not_rhs

$\square$

This is how we use \idr{Not} to state that \idr{0} and \idr{1} are different
elements of \idr{Nat}:

\todo[inline]{Explain \idr{Refl}-lambda syntax and \idr{Uninhabited}, keep in
mind https://github.com/idris-lang/Idris-dev/issues/3943}

> zero_not_one : Not (Z = S _)
> zero_not_one = \Refl impossible

We could also rely on the \idr{Uninhabited} instance in stdlib and write this as

```idris
zero_not_one = uninhabited
```

It takes a little practice to get used to working with negation in Idris. Even
though you can see perfectly well why a statement involving negation is true, it
can be a little tricky at first to get things into the right configuration so
that Idris can understand it! Here are proofs of a few familiar facts to get you
warmed up.

> not_False : Not Void
> not_False = absurd

> contradiction_implies_anything : (p, Not p) -> q
> contradiction_implies_anything (p, notp) = absurd $ notp p

> double_neg : p -> Not $ Not p
> double_neg p notp = notp p

==== Exercise: 2 stars, advanced, recommended (double_neg_inf)

Write an informal proof of \idr{double_neg}:

_Theorem_: \idr{p} implies \idr{Not $ Not p}, for any proposition \idr{p}.

> -- FILL IN HERE

$\square$

==== Exercise: 2 stars, recommended (contrapositive)

> contrapositive : (p -> q) -> (Not q -> Not p)
> contrapositive pq = ?contrapositive_rhs

$\square$

==== Exercise: 1 star (not_both_true_and_false)

> not_both_true_and_false : Not (p, Not p)
> not_both_true_and_false = ?not_both_true_and_false_rhs

$\square$

==== Exercise: 1 star, advanced (informal_not_PNP)

Write an informal proof (in English) of the proposition \idr{Not (p, Not p)}.

> -- FILL IN HERE

$\square$

Similarly, since inequality involves a negation, it requires a little practice
to be able to work with it fluently. Here is one useful trick. If you are trying
to prove a goal that is nonsensical (e.g., the goal state is \idr{False =
True}), apply \idr{absurd} to change the goal to \idr{Void}. This makes it
easier to use assumptions of the form \idr{Not p} that may be available in the
context -- in particular, assumptions of the form \idr{Not (x=y)}.

> not_true_is_false : (b : Bool) -> Not (b = True) -> b = False
> not_true_is_false False h = Refl
> not_true_is_false True h = absurd $ h Refl

=== Truth

Besides \idr{Void}, Idris's standard library also defines \idr{Unit}, a proposition that is
trivially true. To prove it, we use the predefined constant \idr{()}:

> True_is_true : Unit
> True_is_true = ()

Unlike \idr{Void}, which is used extensively, \idr{Unit} is used quite rarely in
proofs, since it is trivial (and therefore uninteresting) to prove as a goal,
and it carries no useful information as a hypothesis. But it can be quite useful
when defining complex proofs using conditionals or as a parameter to
higher-order proofs. We will see examples of such uses of \idr{Unit} later on.

=== Logical Equivalence

The handy "if and only if" connective, which asserts that two propositions have
the same truth value, is just the conjunction of two implications.

> namespace MyIff

>   iff : {p,q : Type} -> Type
>   iff {p} {q} = (p -> q, q -> p)

Idris's stdlib has a more general form of this, \idr{Iso}, in
\idr{Control.Isomorphism}.

>   syntax [p] "<->" [q] = iff {p} {q}

>   iff_sym : (p <-> q) -> (q <-> p)
>   iff_sym (pq, qp) = (qp, pq)

>   not_true_iff_false : (Not (b = True)) <-> (b = False)
>   not_true_iff_false {b} = (not_true_is_false b, not_true_and_false b)
>   where
>     not_true_and_false : (b : Bool) -> (b = False) -> Not (b = True)
>     not_true_and_false False _ Refl impossible
>     not_true_and_false True Refl _ impossible

==== Exercise: 1 star, optional (iff_properties)

Using the above proof that \idr{<->} is symmetric (\idr{iff_sym}) as a guide,
prove that it is also reflexive and transitive.

>   iff_refl : p <-> p
>   iff_refl = ?iff_refl_rhs

>   iff_trans : (p <-> q) -> (q <-> r) -> (p <-> r)
>   iff_trans piq qir = ?iff_trans_rhs

$\square$

==== Exercise: 3 stars (or_distributes_over_and)

>   or_distributes_over_and : (p `Either` (q,r)) <-> (p `Either` q, p `Either` r)
>   or_distributes_over_and = ?or_distributes_over_and_rhs

$\square$

\todo[inline]{Edit the rest of the section. What to do with Setoids? We could
probably just use profunctors here}

Some of Idris's tactics treat iff statements specially, avoiding the need for
some low-level proof-state manipulation. In particular, rewrite and reflexivity
can be used with iff statements, not just equalities. To enable this behavior,
we need to import a special Idris library that allows rewriting with other
formulas besides equality (setoids).

Here is a simple example demonstrating how these tactics work with iff. First,
let's prove a couple of basic iff equivalences...

>   mult_0 : (n * m = Z) <-> ((n = Z) `Either` (m = Z))
>   mult_0 {n} {m} = (to n m, or_example n m)
>   where
>     to : (n, m : Nat) -> (n * m = Z) -> (n = 0) `Either` (m = 0)
>     to Z _ Refl = Left Refl
>     to (S _) Z _ = Right Refl
>     to (S _) (S _) Refl impossible

>   or_assoc : (p `Either` (q `Either` r)) <-> ((p `Either` q) `Either` r)
>   or_assoc = (to, fro)
>   where
>     to : Either p (Either q r) -> Either (Either p q) r
>     to (Left p) = Left $ Left p
>     to (Right (Left q)) = Left $ Right q
>     to (Right (Right r)) = Right r
>     fro : Either (Either p q) r -> Either p (Either q r)
>     fro (Left (Left p)) = Left p
>     fro (Left (Right q)) = Right $ Left q
>     fro (Right r) = Right $ Right r

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) <->
>              ((n = Z) `Either` ((m = Z) `Either` (p = Z)))
>   mult_0_3 = (to, fro)
>   where
>     to : (n * m * p = Z) -> ((n = Z) `Either` ((m = Z) `Either` (p = Z)))
>     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
>            Left prf => Left $ n_m_to prf
>            Right prf => Right prf
>     fro : ((n = Z) `Either` ((m = Z) `Either` (p = Z))) -> (n * m * p = Z)
>     fro (Left Refl) = Refl
>     fro {n} (Right (Left Refl)) = rewrite multZeroRightZero n in Refl
>     fro {n} {m} (Right (Right Refl)) = rewrite multZeroRightZero (n*m) in Refl

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 = fst $ mult_0 {n} {m}

=== Existential Quantification

Another important logical connective is existential quantification. To say that
there is some \idr{x} of type \idr{t} such that some property \idr{p} holds of
\idr{x}, we write \idr{(x : t ** p)}. The type annotation \idr{: t} can be
omitted if Idris is able to infer from the context what the type of \idr{x}
should be.

To prove a statement of the form \idr{(x ** p)}, we must show that \idr{p} holds
for some specific choice of value for \idr{x}, known as the _witness_ of the
existential. This is done in two steps: First, we explicitly tell Idris which
witness \idr{t} we have in mind by writing it on the left side of \idr{**}. Then
we prove that \idr{p} holds after all occurrences of \idr{x} are replaced by
\idr{t}.

> four_is_even : (n : Nat ** 4 = n + n)
> four_is_even = (2 ** Refl)

Conversely, if we have an existential hypothesis \idr{(x ** p)} in the context,
we can pattern match on it to obtain a witness \idr{x} and a hypothesis stating
that \idr{p} holds of \idr{x}.

> exists_example_2 : (m : Nat ** n = 4 + m) -> (o : Nat ** n = 2 + o)
> exists_example_2 (m ** pf) = (2 + m ** pf)

==== Exercise: 1 star (dist_not_exists)

Prove that "\idr{p} holds for all \idr{x}" implies "there is no \idr{x} for
which \idr{p} does not hold."

> dist_not_exists : {p : a -> Type} -> ((x : a) -> p x) -> Not (x ** Not $ p x)
> dist_not_exists f = ?dist_not_exists_rhs

$\square$

==== Exercise: 2 stars (dist_exists_or)

Prove that existential quantification distributes over disjunction.

> 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

$\square$

== Programming with Propositions

The logical connectives that we have seen provide a rich vocabulary for defining
complex propositions from simpler ones. To illustrate, let's look at how to
express the claim that an element \idr{x} occurs in a list \idr{l}. Notice that
this property has a simple recursive structure:

  - If \idr{l} is the empty list, then \idr{x} cannot occur on it, so the
    property "\idr{x} appears in \idr{l}" is simply false.

  - Otherwise, \idr{l} has the form \idr{x' :: xs}. In this case, \idr{x} occurs
    in \idr{l} if either it is equal to \idr{x'} or it occurs in \idr{xs}.

We can translate this directly into a straightforward recursive function from
taking an element and a list and returning a proposition:

> In : (x : a) -> (l : List a) -> Type
> In x [] = Void
> In x (x' :: xs) = (x' = x) `Either` In x xs

When \idr{In} is applied to a concrete list, it expands into a concrete sequence
of nested disjunctions.

> In_example_1 : In 4 [1, 2, 3, 4, 5]
> In_example_1 = Right $ Right $ Right $ Left Refl

> In_example_2 : In n [2, 4] -> (n' : Nat ** n = 2 * n')
> In_example_2 (Left Refl) = (1 ** Refl)
> In_example_2 (Right $ Left Refl) = (2 ** Refl)
> In_example_2 (Right $ Right prf) = absurd prf

(Notice the use of \idr{absurd} to discharge the last case.)

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 (f x) (map f l)
> In_map _ [] _ ixl = absurd ixl
> In_map f (x' :: xs) x (Left prf) = rewrite prf in Left Refl
> In_map f (x' :: xs) x (Right r) = Right $ In_map f xs x r

This way of defining propositions recursively, though convenient in some cases,
also has some drawbacks. In particular, it is subject to Idris's usual
restrictions regarding the definition of recursive functions, e.g., the
requirement that they be "obviously terminating." In the next chapter, we will
see how to define propositions _inductively_, a different technique with its own
set of strengths and limitations.

==== Exercise: 2 stars (In_map_iff)

> 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

$\square$

==== Exercise: 2 stars (in_app_iff)

> in_app_iff : (In a (l++l')) <-> (In a l `Either` In a l')
> in_app_iff = ?in_app_iff_rhs

$\square$

==== Exercise: 3 stars (All)

Recall that functions returning propositions can be seen as _properties_ of
their arguments. For instance, if \idr{p} has type \idr{Nat -> Type}, then
\idr{p n} states that property \idr{p} holds of \idr{n}.

Drawing inspiration from \idr{In}, write a recursive function \idr{All} stating
that some property \idr{p} holds of all elements of a list \idr{l}. To make sure
your definition is correct, prove the \idr{All_In} lemma below. (Of course, your
definition should _not_ just restate the left-hand side of \idr{All_In}.)

> All : (p : t -> Type) -> (l : List t) -> Type
> All p l = ?All_rhs

> All_In : ((x:t) -> In x l -> p x) <-> (All p l)
> All_In = ?All_In_rhs

$\square$

==== Exercise: 3 stars (combine_odd_even)

Complete the definition of the \idr{combine_odd_even} function below. It takes
as arguments two properties of numbers, \idr{podd} and \idr{peven}, and it
should return a property \idr{p} such that \idr{p n} is equivalent to \idr{podd
n} when \idr{n} is odd and equivalent to \idr{peven n} otherwise.

> combine_odd_even : (podd, peven : Nat -> Type) -> (Nat -> Type)
> combine_odd_even podd peven = ?combine_odd_even_rhs

To test your definition, prove the following facts:

> combine_odd_even_intro : (n : Nat) ->
>                          (oddb n = True -> podd n) ->
>                          (oddb n = False -> peven n) ->
>                          combine_odd_even podd peven n
> combine_odd_even_intro n oddp evenp = ?combine_odd_even_intro_rhs

> combine_odd_even_elim_odd : (n : Nat) ->
>                             combine_odd_even podd peven n ->
>                             oddb n = True ->
>                             podd n
> combine_odd_even_elim_odd n x prf = ?combine_odd_even_elim_odd_rhs

> combine_odd_even_elim_even : (n : Nat) ->
>                              combine_odd_even podd peven n ->
>                              oddb n = False ->
>                              peven n
> combine_odd_even_elim_even n x prf = ?combine_odd_even_elim_even_rhs

$\square$

== Applying Theorems to Arguments

One feature of Idris that distinguishes it from many other proof assistants is
that it treats _proofs_ as first-class objects.

\todo[inline]{`nameref` the chapters when they're done}

There is a great deal to be said about this, but it is not necessary to
understand it in detail in order to use Idris. This section gives just a taste,
while a deeper exploration can be found in the optional chapters
`ProofObjects` and `IndPrinciples`.

We have seen that we can use the \idr{:t} command to ask Idris to print the type
of an expression. We can also use \idr{:t} to ask what theorem a particular
identifier refers to.

```idris
λΠ> :t plusCommutative
plusCommutative : (left : Nat) -> (right : Nat) -> left + right = right + left
```

Idris prints the _statement_ of the \idr{plusCommutative} theorem in the same
way that it prints the _type_ of any term that we ask it to check. Why?

The reason is that the identifier \idr{plusCommutative} actually refers to a
_proof object_ -- a data structure that represents a logical derivation
establishing of the truth of the statement \idr{(n, m : Nat) -> n + m = m + n}.
The type of this object _is_ the statement of the theorem that it is a proof of.

Intuitively, this makes sense because the statement of a theorem tells us what
we can use that theorem for, just as the type of a computational object tells us
what we can do with that object -- e.g., if we have a term of type \idr{Nat ->
Nat -> Nat}, we can give it two \idr{Nat}s as arguments and get a \idr{Nat}
back. Similarly, if we have an object of type \idr{n = m -> n + n = m + m} and
we provide it an "argument" of type \idr{n = m}, we can derive \idr{n + n = m +
m}.

Operationally, this analogy goes even further: by applying a theorem, as if it
were a function, to hypotheses with matching types, we can specialize its result
without having to resort to intermediate assertions. For example, suppose we
wanted to prove the following result:

> plus_comm3 : (n, m, p : Nat) -> n + (m + p) = (p + m) + n

\todo[inline]{Edit, we have already done this in previous chapters (add a
hyperlink?)}

It appears at first sight that we ought to be able to prove this by rewriting
with \idr{plusCommutative} twice to make the two sides match. The problem,
however, is that the second \idr{rewrite} will undo the effect of the first.

```coq
Proof.
  intros n m p.
  rewrite plus_comm.
  rewrite plus_comm.
  (* We are back where we started... *)
Abort.
```

One simple way of fixing this problem, using only tools that we already know, is
to use assert to derive a specialized version of plus_comm that can be used to
rewrite exactly where we want.

```coq
Lemma plus_comm3_take2 :
  ∀n m p, n + (m + p) = (p + m) + n.
Proof.
  intros n m p.
  rewrite plus_comm.
  assert (H : m + p = p + m).
  { rewrite plus_comm. reflexivity. }
  rewrite H.
  reflexivity.
Qed.
```

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
>                    rewrite plusCommutative m p in Refl

You can "use theorems as functions" in this way with almost all tactics that
take a theorem name as an argument. Note also that theorem application uses the
same inference mechanisms as function application; thus, it is possible, for
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) ->
>                        In n (map (\m => m * 0) ns) -> n = 0
> lemma_application_ex _ [] prf = absurd 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 prf

We will see many more examples of the idioms from this section in later chapters.

== Idris vs. Set Theory

\todo[inline]{Edit, Idris's core is likely some variant of MLTT}

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
Theory (ZFC), a mathematical object can potentially be a member of many
different sets; a term in Idris's logic, on the other hand, is a member of at
most one type. This difference often leads to slightly different ways of
capturing informal mathematical concepts, but these are, by and large, quite
Natural and easy to work with. For example, instead of saying that a natural
number \idr{n} belongs to the set of even numbers, we would say in Idris that
\idr{ev n} holds, where \idr{ev : Nat -> Type} is a property describing even
numbers.

However, there are some cases where translating standard mathematical reasoning
into Idris can be either cumbersome or sometimes even impossible, unless we
enrich the core logic with additional axioms. We conclude this chapter with a
brief discussion of some of the most significant differences between the two
worlds.

=== Functional Extensionality

The equality assertions that we have seen so far mostly have concerned elements
of inductive types (\idr{Nat}, \idr{Bool}, etc.). But since Idris's equality
operator is polymorphic, these are not the only possibilities -- in particular,
we can write propositions claiming that two _functions_ are equal to each other:

> function_equality_ex1 : plus 3 = plus (pred 4)
> function_equality_ex1 = Refl

In common mathematical practice, two functions `f` and `g` are considered equal
if they produce the same outputs:

\[
     \left(\forall x, f(x) = g(x)\right) \to f = g
\]

This is known as the principle of _functional extensionality_.

Informally speaking, an "extensional property" is one that pertains to an
object's observable behavior. Thus, functional extensionality simply means that
a function's identity is completely determined by what we can observe from it --
i.e., in Idris terms, the results we obtain after applying it.

Functional extensionality is not part of Idris's basic axioms. This means that
some "reasonable" propositions are not provable.

```idris
function_equality_ex2 : (\x => plus x 1) = (\x => plus 1 x)
function_equality_ex2 = ?stuck
```

\todo[inline]{Explain \idr{believe_me} vs \idr{really_believe_me}?}

However, we can add functional extensionality to Idris's core logic using the
\idr{really_believe_me} command.

> functional_extensionality : ((x : a) -> f x = g x) -> f = g
> functional_extensionality = really_believe_me

Using \idr{really_believe_me} has the same effect as stating a theorem and
skipping its proof using a hole, but it alerts the reader (and type checker)
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

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
every proposition, including \idr{Void}!

Unfortunately, there is no simple way of telling whether an axiom is safe to
add: hard work is generally required to establish the consistency of any
particular combination of axioms.

However, it is known that adding functional extensionality, in particular, _is_
consistent.

\todo[inline]{Is there such a command in Idris?}

To check whether a particular proof relies on any additional axioms, use the
`Print Assumptions` command.

```coq
Print Assumptions function_equality_ex2.
(* ===>
     Axioms:
     functional_extensionality :
         forall (X Y : Type) (f g : X -> Y),
                (forall x : X, f x = g x) -> f = g *)
```

==== Exercise: 4 stars (tr_rev)

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.

We can improve this with the following definition:

> rev_append : (l1, l2 : List x) -> List x
> rev_append [] l2 = l2
> rev_append (x :: xs) l2 = rev_append xs (x :: l2)

> tr_rev : (l : List x) -> List x
> tr_rev l = rev_append l []

(This is very similar to how \idr{reverse} is defined in \idr{Prelude.List}.)

This version is said to be _tail-recursive_, because the recursive call to the
function is the last operation that needs to be performed (i.e., we don't have
to execute \idr{++} after the recursive call); a decent compiler will generate
very efficient code in this case. Prove that the two definitions are indeed
equivalent.

> tr_rev_correct : (x : List a) -> tr_rev x = rev x
> tr_rev_correct = ?tr_rev_correct_rhs

$\square$

=== Propositions and Booleans

We've seen two different ways of encoding logical facts in Idris: with
_booleans_ (of type \idr{Bool}), and with _propositions_ (of type \idr{Type}).

For instance, to claim that a number \idr{n} is even, we can say either

  - (1) that \idr{evenb n} returns \idr{True}, or

  - (2) that there exists some \idr{k} such that \idr{n = double k}. Indeed,
    these two notions of evenness are equivalent, as can easily be shown with a
    couple of auxiliary lemmas.

We often say that the boolean \idr{evenb n} _reflects_ the proposition \idr{(k
** n = double k)}.

> evenb_double : evenb (double k) = True
> evenb_double {k = Z} = Refl
> evenb_double {k = (S k')} = evenb_double {k=k'}

==== Exercise: 3 stars (evenb_double_conv)

> evenb_double_conv : (k ** n = if evenb n then double k else S (double k))

*Hint*: Use the \idr{evenb_S} lemma from \idr{Induction}.

> evenb_double_conv = ?evenb_double_conv_rhs

$\square$

> even_bool_prop : (evenb n = True) <-> (k ** n = double k)
> 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 (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.

>  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

However, while the boolean and propositional formulations of a claim are
equivalent from a purely logical perspective, they need not be equivalent
_operationally_. Equality provides an extreme example: knowing that \idr{n == m
= True} is generally of little direct help in the middle of a proof involving
\idr{n} and \idr{m}; however, if we convert the statement to the equivalent form
\idr{n = m}, we can rewrite with it.

The case of even numbers is also interesting. Recall that, when proving the
backwards direction of \idr{even_bool_prop} (i.e., \idr{evenb_double}, going
from the propositional to the boolean claim), we used a simple induction on
\idr{k}. On the other hand, the converse (the \idr{evenb_double_conv} exercise)
required a clever generalization, since we can't directly prove \idr{(k ** n =
double k) -> evenb n = True}.

For these examples, the propositional claims are more useful than their boolean
counterparts, but this is not always the case. For instance, we cannot test
whether a general proposition is true or not in a function definition; as a
consequence, the following code fragment is rejected:

```idris
is_even_prime : Nat -> Bool
is_even_prime n = if n = 2 then True else False
```

Idris complains that \idr{n = 2} has type \idr{Type}, while it expects an
element of \idr{Bool} (or some other inductive type with two elements). The
reason for this error message has to do with the _computational_ nature of
Idris's core language, which is designed so that every function that it can
express is computable and total. One reason for this is to allow the extraction
of executable programs from Idris developments. As a consequence, \idr{Type} in
Idris does _not_ have a universal case analysis operation telling whether any
given proposition is true or false, since such an operation would allow us to
write non-computable functions.

Although general non-computable properties cannot be phrased as boolean
computations, it is worth noting that even many _computable_ properties are
easier to express using \idr{Type} than \idr{Bool}, since recursive function
definitions are subject to significant restrictions in Idris. For instance, the
next chapter shows how to define the property that a regular expression matches
a given string using \idr{Type}. Doing the same with \idr{Bool} would amount to
writing a regular expression matcher, which would be more complicated, harder to
understand, and harder to reason about.

Conversely, an important side benefit of stating facts using booleans is
enabling some proof automation through computation with Idris terms, a technique
known as _proof by reflection_. Consider the following statement:

> even_1000 : (k ** 1000 = double k)

The most direct proof of this fact is to give the value of \idr{k} explicitly.

> even_1000 = (500 ** Refl)

On the other hand, the proof of the corresponding boolean statement is even
simpler:

> even_1000' : evenb 1000 = True
> even_1000' = Refl

What is interesting is that, since the two notions are equivalent, we can use
the boolean formulation to prove the other one without mentioning the value 500
explicitly:

> even_1000'' : (k ** 1000 = double k)
> even_1000'' = (fst $ even_bool_prop {n=1000}) Refl

\todo[inline]{Add http://www.ams.org/journals/notices/200811/tx081101382p.pdf as
a link}

Although we haven't gained much in terms of proof size in this case, larger
proofs can often be made considerably simpler by the use of reflection. As an
extreme example, the Coq proof of the famous _4-color theorem_ uses reflection
to reduce the analysis of hundreds of different cases to a boolean computation.
We won't cover reflection in great detail, but it serves as a good example
showing the complementary strengths of booleans and general propositions.

==== Exercise: 2 stars (logical_connectives)

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) <->
>                                    (b1 = True, b2 = True)
> andb_true_iff b1 b2 = ?andb_true_iff_rhs

> orb_true_iff : (b1, b2 : Bool) -> (b1 || b2 = True) <->
>                                   ((b1 = True) `Either` (b2 = True))
> orb_true_iff b1 b2 = ?orb_true_iff_rhs

$\square$

==== Exercise: 1 star (beq_nat_false_iff)

The following theorem is an alternate "negative" formulation of
\idr{beq_nat_true_iff} that is more convenient in certain situations (we'll see
examples in later chapters).

> beq_nat_false_iff : (x, y : Nat) -> (x == y = False) <-> (Not (x = y))
> beq_nat_false_iff x y = ?beq_nat_false_iff_rhs

$\square$

==== Exercise: 3 stars (beq_list)

Given a boolean operator \idr{beq} for testing equality of elements of some type
\idr{a}, we can define a function \idr{beq_list beq} for testing equality of
lists with elements in \idr{a}. Complete the definition of the \idr{beq_list}
function below. To make sure that your definition is correct, prove the lemma
\idr{beq_list_true_iff}.

> 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) ->
>                     ((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

$\square$

==== Exercise: 2 stars, recommended (All_forallb)

Recall the function \idr{forallb}, from the exercise
\idr{forall_exists_challenge} in chapter `Tactics`:

> 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) <->
>                                    (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

$\square$

=== Classical vs. Constructive Logic

We have seen that it is not possible to test whether or not a proposition
\idr{p} holds while defining a Idris function. You may be surprised to learn
that a similar restriction applies to _proofs_! In other words, the following
intuitive reasoning principle is not derivable in Idris:

```idris
excluded_middle : p `Either` (Not p)
```

To understand operationally why this is the case, recall that, to prove a
statement of the form \idr{p `Either` q}, we use the \idr{Left} and \idr{Right}
pattern matches, which effectively require knowing which side of the disjunction
holds. But the universally quantified \idr{p} in \idr{excluded_middle} is an
arbitrary proposition, which we know nothing about. We don't have enough
information to choose which of \idr{Left} or \idr{Right} to apply, just as Idris
doesn't have enough information to mechanically decide whether \idr{p} holds or
not inside a function.

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}.

> 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

In particular, the excluded middle is valid for equations \idr{n = m}, between
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 (to n m, fro n m)
> where
>   to : (n, m : Nat) -> (n=m) -> (n==m)=True
>   to Z Z prf = Refl
>   to Z (S _) Refl impossible
>   to (S _) Z Refl impossible
>   to (S k) (S j) prf = to k j (succInjective k j prf)
>   fro : (n, m : Nat) -> (n==m)=True -> (n=m)
>   fro Z Z Refl = Refl
>   fro Z (S _) Refl impossible
>   fro (S _) Z Refl impossible
>   fro (S k) (S j) prf = rewrite fro k j prf in Refl

(Idris has a built-in version of this, called \idr{decEq}.)

It may seem strange that the general excluded middle is not available by default
in Idris; after all, any given claim must be either true or false. Nonetheless,
there is an advantage in not assuming the excluded middle: statements in Idris
can make stronger claims than the analogous statements in standard mathematics.
Notably, if there is a Idris proof of \idr{(x ** p x)}, it is possible to
explicitly exhibit a value of \idr{x} for which we can prove \idr{p x} -- in
other words, every proof of existence is necessarily _constructive_.

Logics like Idris's, which do not assume the excluded middle, are referred to as
_constructive logics_.

More conventional logical systems such as ZFC, in which the excluded middle does
hold for arbitrary propositions, are referred to as _classical_.

The following example illustrates why assuming the excluded middle may lead to
non-constructive proofs:

\todo[inline]{Use proper TeX?}

_Claim_: There exist irrational numbers `a` and `b` such that `a ^ b` is
rational.

_Proof_: It is not difficult to show that `sqrt 2` is irrational. If `sqrt 2 ^
sqrt 2` is rational, it suffices to take `a = b = sqrt 2` and we are done.
Otherwise, `sqrt 2 ^ sqrt 2` is irrational. In this case, we can take `a = sqrt
2 ^ sqrt 2` and `b = sqrt 2`, since `a ^ b = sqrt 2 ^ (sqrt 2 * sqrt 2)` = sqrt
2 ^ 2 = 2`. $\square$

Do you see what happened here? We used the excluded middle to consider
separately the cases where `sqrt 2 ^ sqrt 2` is rational and where it is not,
without knowing which one actually holds! Because of that, we wind up knowing
that such `a` and `b` exist but we cannot determine what their actual values are
(at least, using this line of argument).

As useful as constructive logic is, it does have its limitations: There are many
statements that can easily be proven in classical logic but that have much more
complicated constructive proofs, and there are some that are known to have no
constructive proof at all! Fortunately, like functional extensionality, the
excluded middle is known to be compatible with Idris's logic, allowing us to add
it safely as an axiom. However, we will not need to do so in this book: the
results that we cover can be developed entirely within constructive logic at
negligible extra cost.

It takes some practice to understand which proof techniques must be avoided in
constructive reasoning, but arguments by contradiction, in particular, are
infamous for leading to non-constructive proofs. Here's a typical example:
suppose that we want to show that there exists \idr{x} with some property
\idr{p}, i.e., such that \idr{p x}. We start by assuming that our conclusion is
false; that is, \idr{Not (x : a ** p x)}. From this premise, it is not hard to
derive \idr{(x : a) -> Not $ p x}. If we manage to show that this intermediate
fact results in a contradiction, we arrive at an existence proof without ever
exhibiting a value of \idr{x} for which \idr{p x} holds!

The technical flaw here, from a constructive standpoint, is that we claimed to
prove \idr{(x ** p x)} using a proof of \idr{Not $ Not (x ** p x)}. Allowing
ourselves to remove double negations from arbitrary statements is equivalent to
assuming the excluded middle, as shown in one of the exercises below. Thus, this
line of reasoning cannot be encoded in Idris without assuming additional axioms.

==== Exercise: 3 stars (excluded_middle_irrefutable)

The consistency of Idris with the general excluded middle axiom requires
complicated reasoning that cannot be carried out within Idris itself. However,
the following theorem implies that it is always safe to assume a decidability
axiom (i.e., an instance of excluded middle) for any _particular_ type \idr{p}.
Why? Because we cannot prove the negation of such an axiom; if we could, we
would have both \idr{Not (p `Either` Not p)} and \idr{Not $ Not (p `Either` Not
p)}, a contradiction.

> excluded_middle_irrefutable : Not $ Not (p `Either` Not p)
> excluded_middle_irrefutable = ?excluded_middle_irrefutable_rhs

$\square$

==== Exercise: 3 stars, advanced (not_exists_dist)

It is a theorem of classical logic that the following two assertions are
equivalent:

```idris
    Not (x : a ** Not p x)
    (x : a) -> p x
```

\todo[inline]{Add a hyperlink}

The \idr{dist_not_exists} theorem above proves one side of this equivalence.
Interestingly, the other direction cannot be proved in constructive logic. Your
job is to show that it is implied by the excluded middle.

> not_exists_dist : {p : a -> Type} -> Not (x ** Not $ p x) -> ((x : a) -> p x)
> not_exists_dist prf x = ?not_exists_dist_rhs
>   where
>   excluded_middle : (a : Type) -> a `Either` (Not a)
>   excluded_middle p = really_believe_me p

$\square$

==== Exercise: 5 stars, optional (classical_axioms)

For those who like a challenge, here is an exercise taken from the Coq'Art book
by Bertot and Casteran (p. 123). Each of the following four statements, together
with \idr{excluded_middle}, can be considered as characterizing classical logic.
We can't prove any of them in Idris, but we can consistently add any one of them
as an axiom if we wish to work in classical logic.

Prove that all five propositions (these four plus \idr{excluded_middle}) are
equivalent.

> peirce : ((p -> q) -> p) -> p

> double_negation_elimination : Not $ Not p -> p

> de_morgan_not_and_not : Not (Not p, Not q) -> p `Either` q

> implies_to_or : (p -> q) -> ((Not p) `Either` q)

> -- FILL IN HERE

$\square$

ext: lidr

max_stars_repo_name: diseraluca/software-foundations

max_issues_repo_name: diseraluca/software-foundations

max_forks_repo_name: diseraluca/software-foundations


text:
module Data.Time.Calendar.Private

import Data.Time.Clock.Internal.Fixed

export
data PadOption
    = Pad Int
          String
    | NoPad

export
showPadded: PadOption -> String -> String
showPadded (Pad i c) s =
  let
    ix = toNat $ i - cast (length s)
    padding = unlines $ replicate ix c
    y = padding ++ s
  in
    y
showPadded NoPad y = y

export
interface (Num t, Ord t, Show t) => ShowPadded t where
  showPaddedNum: PadOption -> t -> String

export
ShowPadded Integer where
  showPaddedNum NoPad i = show i
  showPaddedNum pad i = case (i < 0) of
                             True => "-" ++ (showPaddedNum pad (negate i))
                             False => showPadded pad $ show i
export
ShowPadded Int where
  showPaddedNum NoPad i = show i
  showPaddedNum pad i =
    case (i < 0) of
         True => "-" ++ (showPaddedNum pad (negate i))
         False => showPadded pad $ show i
export
show2: (ShowPadded t) => t -> String
show2 = showPaddedNum $ Pad 2 "0"

export
show3: (ShowPadded t) => t -> String
show3 = showPaddedNum $ Pad 3 "0"

export
show4: (ShowPadded t) => t -> String
show4 = showPaddedNum $ Pad 4 "0"

-- mod100 :: (Integral i) => i -> i
-- mod100 x = mod x 100

-- div100 :: (Integral i) => i -> i
-- div100 x = div x 100

export
clip : (Ord t) => t -> t -> t -> t
clip a b x = case x < a of
                  True => a
                  _ => case x > b of
                       True => b
                       _ => x

export
clipValid : (Ord t) => t -> t -> t -> Maybe t
clipValid a b x = case x < a of
                  True => Nothing
                  _ => case x > b of
                       True => Nothing
                       _ => Just x

-- Forceful conversion from Integer to Int
export
integerToInt: Integer -> Int
integerToInt x = cast (the String (cast x))

-- quotBy :: (Real a, Integral b) => a -> a -> b
-- quotBy d n = truncate ((toRational n) / (toRational d))

-- remBy :: Real a => a -> a -> a
-- remBy d n = n - (fromInteger f) * d
--   where
--     f = quotBy d n

-- quotRemBy :: (Real a, Integral b) => a -> a -> (b, a)
-- quotRemBy d n = let
--     f = quotBy d n
--     in (f, n - (fromIntegral f) * d)

max_stars_repo_name: gdevanla/idris-time

max_issues_repo_name: gdevanla/idris-time

max_forks_repo_name: gdevanla/idris-time


text:
> module Nat.GCDProperties

> import Nat.GCD
> import Nat.GCDOperations
> import Nat.Divisor
> import Nat.DivisorOperations
> import Nat.DivisorProperties
> import Nat.LTProperties
> import Nat.OperationsProperties
> import Basic.Operations
> import Sigma.Sigma
> import Pairs.Operations

> %default total
> %auto_implicits on
> %access export
> -- %access public export

> |||
> gcdUnique : (d1 : Nat) -> (d2 : Nat) -> GCD d1 m n -> GCD d2 m n -> d1 = d2
> gcdUnique d1 d2 (MkGCD d1Dm d1Dn d1G) (MkGCD d2Dm d2Dn d2G) = s3 where
>   s1 : d1 `Divisor` d2
>   s1 = d2G d1 d1Dm d1Dn
>   s2 : d2 `Divisor` d1
>   s2 = d1G d2 d2Dm d2Dn
>   s3 : d1 = d2
>   s3 = divisorAntisymmetric d1 d2 s1 s2
> %freeze gcdUnique

> |||
> gcdCommutative : GCD d m n -> GCD d n m
> gcdCommutative (MkGCD dDm dDn dG) = (MkGCD dDn dDm (\ d' => \ n => \ m => dG d' m n))
> %freeze gcdCommutative

> ||| If |m| is positive, the greatest common divisor of |m| and |n| is positive
> gcdPreservesPositivity1 : Z `LT` m -> (dv : Sigma Nat (\ d => GCD d m n)) -> Z `LT` (getWitness dv)
> gcdPreservesPositivity1 {m} zLTm (MkSigma d prf) = multLTZeroLeftLTZero d q zLTdq where
>   dDm : d `Divisor` m
>   dDm = gcdDivisorFst prf
>   q : Nat
>   q = quotient m d dDm
>   zLTdq : Z `LT` (d * q)
>   zLTdq = replace {x = m}
>                   {y = d * q}
>                   {P = \ ZUZU => Z `LT` ZUZU}
>                   (sym (quotientLemma m d dDm)) zLTm
> %freeze gcdPreservesPositivity1

> ||| If |n| is positive, the greatest common divisor of |m| and |n| is positive
> gcdPreservesPositivity2 : Z `LT` n -> (dv : Sigma Nat (\ d => GCD d m n)) -> Z `LT` (getWitness dv)
> gcdPreservesPositivity2 {n} zLTn (MkSigma d prf) = multLTZeroLeftLTZero d q zLTdq where
>   dDn : d `Divisor` n
>   dDn = gcdDivisorSnd prf
>   q : Nat
>   q = quotient n d dDn
>   zLTdq : Z `LT` (d * q)
>   zLTdq = replace {x = n}
>                   {y = d * q}
>                   {P = \ ZUZU => Z `LT` ZUZU}
>                   (sym (quotientLemma n d dDn)) zLTn
> %freeze gcdPreservesPositivity2

> |||
> gcdLemma : (v : GCD (S d) m n) ->
>            d' `Divisor` (quotient m (S d) (gcdDivisorFst v)) ->
>            d' `Divisor` (quotient n (S d) (gcdDivisorSnd v)) ->
>            d' `Divisor` S Z
> gcdLemma {d} {d'} {m} {n} v d'DmoSd d'DnoSd = divisorOneLemma d d' Sdd'DSd where
>   SdDm    : (S d) `Divisor` m
>   SdDm    = gcdDivisorFst v
>   SdDn    : (S d) `Divisor` n
>   SdDn    = gcdDivisorSnd v
>   SdG     : (d' : Nat) -> d' `Divisor` m -> d' `Divisor` n -> d' `Divisor` (S d)
>   SdG     = gcdDivisorGreatest v
>   Sdd'Dm  : (S d) * d' `Divisor` m
>   Sdd'Dm  = divisorTowerLemma (S d) d' m SdDm d'DmoSd
>   Sdd'Dn  : (S d) * d' `Divisor` n
>   Sdd'Dn  = divisorTowerLemma (S d) d' n SdDn d'DnoSd
>   Sdd'DSd : (S d) * d' `Divisor` (S d)
>   Sdd'DSd = SdG ((S d) * d') Sdd'Dm Sdd'Dn
> %freeze gcdLemma

> |||
> gcdLemma' : (v : GCD d m n) -> Not (d = Z) ->
>             d' `Divisor` (quotient m d (gcdDivisorFst v)) ->
>             d' `Divisor` (quotient n d (gcdDivisorSnd v)) ->
>             d' `Divisor` S Z
> gcdLemma' {d} {d'} {m} {n} v dNotZ d'DmoSd d'DnoSd = divisorOneLemma' d d' dNotZ Sdd'DSd where
>   SdDm    : d `Divisor` m
>   SdDm    = gcdDivisorFst v
>   SdDn    : d `Divisor` n
>   SdDn    = gcdDivisorSnd v
>   SdG     : (d' : Nat) -> d' `Divisor` m -> d' `Divisor` n -> d' `Divisor` d
>   SdG     = gcdDivisorGreatest v
>   Sdd'Dm  : d * d' `Divisor` m
>   Sdd'Dm  = divisorTowerLemma d d' m SdDm d'DmoSd
>   Sdd'Dn  : d * d' `Divisor` n
>   Sdd'Dn  = divisorTowerLemma d d' n SdDn d'DnoSd
>   Sdd'DSd : d * d' `Divisor` d
>   Sdd'DSd = SdG (d * d') Sdd'Dm Sdd'Dn
> %freeze gcdLemma'

> |||
> gcdLemma'' : (d : Nat) -> (m : Nat) -> (n : Nat) ->
>              (dDm : d `Divisor` m) -> (dDn : d `Divisor` n) ->
>              (v : GCD d m n) -> Z `LT` d ->
>              (d' : Nat) ->
>              d' `Divisor` (quotient m d dDm) ->
>              d' `Divisor` (quotient n d dDn) ->
>              d' `Divisor` S Z
> gcdLemma'' d m n dDm dDn v zLTd d' d'Dqmd d'Dqnd = divisorOneLemma'' d d' zLTd dd'Dd where
>   dG     : (d' : Nat) -> d' `Divisor` m -> d' `Divisor` n -> d' `Divisor` d
>   dG     = gcdDivisorGreatest v
>   dd'Dm  : d * d' `Divisor` m
>   dd'Dm  = divisorTowerLemma d d' m dDm d'Dqmd
>   dd'Dn  : d * d' `Divisor` n
>   dd'Dn  = divisorTowerLemma d d' n dDn d'Dqnd
>   dd'Dd  : d * d' `Divisor` d
>   dd'Dd  = dG (d * d') dd'Dm dd'Dn
> %freeze gcdLemma''

> ||| d GCD ((S a) * m) ((S a) * n) => d/(S a) GCD m n
> |||
> ||| The implementation is based on a proof by Tim Richter. We have to show
> |||
> |||   1) d/(S a) is a divisor of m
> |||   2) d/(S a) is a divisor of n
> |||   3) if d' is a divisor of m and n, then d' is a divisor of d/(S a)
> |||
> ||| We know from |quotientDivisorLemma| that
> |||
> |||   a|b, b|c, a|c => (b/a)|(c/a)
> |||
> ||| Thus, we can prove 1) and 2) by applying the lemma to
> |||
> |||   (S a)|d, d|((S a) * m), (S a)|((S a) * m)
> |||
> |||   and
> |||
> |||   (S a)|d, d|((S a) * n), (S a)|((S a) * n)
> |||
> ||| and using |quotientCancellationLemma| to reduce ((S a) * m)/(S a) and
> ||| ((S a) * n)/(S a) to m and n, respectively. Since d is the GCD of
> ||| (S a) * m and (S a) * n and (S a) is trivially a divisor of both, we
> ||| readily have (S a)|d. d|((S a) * m) and d|((S a) * m) also diretly follow
> ||| from d being the GCD of (S a) * m and (S a) * n.
> |||
> ||| In order to prove 3), we again apply |quotientDivisorLemma|, this time to
> |||
> |||   (S a)|((S a) * d'), ((S a) * d')|d, (S a)|d
> |||
> ||| We derive ((S a) * d')|d from the hypothesis d'|m, d'|n by pre-multiplying
> ||| by (S a) (and using |divisorMultLemma1|). This yields
> |||
> |||   ((S a) * d')|((S a) * m), ((S a) * d')|((S a) * n)
> |||
> ||| The result directly follows from d being the GCD of (S a) * m and (S a) * n.
> |||
> gcdDivisorLemma : (d : Nat) -> (m : Nat) -> (n : Nat) -> (a : Nat) ->
>                   GCD d ((S a) * m) ((S a) * n) ->
>                   Sigma ((S a) `Divisor` d) (\ saDd => GCD (quotient d (S a) saDd) m n)

> gcdDivisorLemma d m n a v = MkSigma saDd (MkGCD qDm qDn qG) where
>   dDsam   :  d `Divisor` ((S a) * m)
>   dDsam   =  gcdDivisorFst v
>   saDsam  :  S a `Divisor` ((S a) * m)
>   saDsam  =  Element m Refl
>   dDsan   :  d `Divisor` ((S a) * n)
>   dDsan   =  gcdDivisorSnd v
>   saDsan  :  S a `Divisor` ((S a) * n)
>   saDsan  =  Element n Refl
>   saDd    :  (S a) `Divisor` d
>   saDd    =  gcdDivisorGreatest {d = d} v (S a) saDsam saDsan

>   q       :  Nat
>   q       =  quotient d (S a) saDd
>   preqDm  :  q `Divisor` (quotient ((S a) * m) (S a) saDsam)
>   preqDm  =  quotientDivisorLemma a d ((S a) * m) saDd dDsam saDsam
>   qDm     :  q `Divisor` m
>   qDm     =  replace {x = quotient ((S a) * m) (S a) saDsam}
>                      {y = m}
>                      {P = \ ZUZU => q `Divisor` ZUZU}
>                      (quotientCancellationLemma m a saDsam) preqDm

>   preqDn  :  q `Divisor` (quotient ((S a) * n) (S a) saDsan)
>   preqDn  =  quotientDivisorLemma a d ((S a) * n) saDd dDsan saDsan
>   qDn     :  q `Divisor` n
>   qDn     =  replace {x = quotient ((S a) * n) (S a) saDsan}
>                      {y = n}
>                      {P = \ ZUZU => q `Divisor` ZUZU}
>                      (quotientCancellationLemma n a saDsan) preqDn

>   preqG   :  (d' : Nat) -> d' `Divisor` m -> d' `Divisor` n ->
>              (quotient ((S a) * d') (S a) (Element d' Refl)) `Divisor` q
>   preqG d' d'Dm d'Dn  =  quotientDivisorLemma a ((S a) * d') d (Element d' Refl) sad'Dd saDd
>     where sad'Dsam  :  ((S a) * d') `Divisor` ((S a) * m)
>           sad'Dsam  =  divisorMultLemma1 (S a) (S a) (anyDivisorAny (S a)) m d' d'Dm
>           sad'Dsan  :  ((S a) * d') `Divisor` ((S a) * n)
>           sad'Dsan  =  divisorMultLemma1 (S a) (S a) (anyDivisorAny (S a)) n d' d'Dn
>           sad'Dd    :  ((S a) * d') `Divisor` d
>           sad'Dd    =  gcdDivisorGreatest {d = d} v ((S a) * d') sad'Dsam sad'Dsan
>
>   qG      :  (d' : Nat) -> d' `Divisor` m -> d' `Divisor` n -> d' `Divisor` q
>   qG    d' d'Dm d'Dn     =  replace {x = quotient ((S a) * d') (S a) (Element d' Refl)}
>                                     {y = d'}
>                                     {P = \ ZUZU => ZUZU `Divisor` q}
>                                     (quotientCancellationLemma d' a (Element d' Refl)) (preqG d' d'Dm d'Dn)
> %freeze gcdDivisorLemma

> |||
> gcdScaleInvariant : (d : Nat) -> (m : Nat) -> (n : Nat) -> (d' : Nat) -> (a : Nat) ->
>                     GCD d m n -> GCD d' (a * m) (a * n) -> d' = a * d
> gcdScaleInvariant d m n d'  Z    v  v' = s6 where
>   s0   :  Z `Divisor` (Z * m)
>   s0   =  Element m Refl
>   s1   :  Z `Divisor` (Z * n)
>   s1   =  Element n Refl
>   s2   :  Z `Divisor` d'
>   s2   =  gcdDivisorGreatest {d = d'} v' Z s0 s1
>   s3   :  Nat
>   s3   =  getWitness s2
>   s4   :  Z * s3 = d'
>   s4   =  getProof s2
>   s5   :  d' = Z
>   s5   =  replace {x = Z * s3} {y = Z} {P = \ ZUZU => d' = ZUZU} (multZeroLeftZero s3) (sym s4)
>   s6   :  d' = Z * d
>   s6   =  replace {x = Z} {y = Z * d} {P = \ ZUZU => d' = ZUZU} (sym (multZeroLeftZero d)) s5
> gcdScaleInvariant d m n d' (S a) v  v' = s4 where
>   s0   :  (S a) `Divisor` d'
>   s0   =  getWitness (gcdDivisorLemma d' m n a v')
>   s1   :  GCD (quotient d' (S a) s0) m n
>   s1   =  getProof (gcdDivisorLemma d' m n a v')
>   s2   :  quotient d' (S a) s0 = d
>   s2   =  gcdUnique (quotient d' (S a) s0) d s1 v
>   s3   :  (S a) * (quotient d' (S a) s0) = (S a) * d
>   s3   =  multPreservesEq (S a) (S a) (quotient d' (S a) s0) d Refl s2
>   s4   :  d' = (S a) * d
>   s4   =  replace {x = (S a) * (quotient d' (S a) s0)}
>                   {y = d'}
>                   {P = \ ZUZU => ZUZU = (S a) * d}
>                   (quotientLemma d' (S a) s0) s3
> %freeze gcdScaleInvariant

> |||
> gcdScaleInvariantCoro1 : (m : Nat) -> (n : Nat) -> (d : Nat) -> (d1 : Nat) -> (d2 : Nat) ->
>                          (dDm : d `Divisor` m) -> (dDn : d `Divisor` n) ->
>                          GCD d1 (quotient m d dDm) (quotient n d dDn) -> GCD d2 m n -> d2 = d * d1
> gcdScaleInvariantCoro1 m n d d1 d2 dDm dDn v1 v2 =
>   gcdScaleInvariant d1 (quotient m d dDm) (quotient n d dDn) d2 d v1 v2' where
>     v2'  :  GCD d2 (d * (quotient m d dDm)) (d * (quotient n d dDn))
>     v2'  =  replace2 {a = Nat} {a1 = m} {a2 = d * (quotient m d dDm)}
>                      {b = Nat} {b1 = n} {b2 = d * (quotient n d dDn)}
>                      {P = \ ZAZA => \ ZUZU => GCD d2 ZAZA ZUZU}
>                      (sym (quotientLemma m d dDm)) (sym (quotientLemma n d dDn)) v2
> %freeze gcdScaleInvariantCoro1

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
over_length : (len : Nat) -> (strs : List String) -> Nat
over_length len strs = length (filter (\str => (length str) > len) strs)

max_stars_repo_name: jeremy-miller/type-driven-development

max_issues_repo_name: jeremy-miller/type-driven-development

max_forks_repo_name: jeremy-miller/type-driven-development


text:
module Data.These

%default total

public export
data These a b = This a | That b | Both a b

public export
fromEither : Either a b -> These a b
fromEither = either This That

public export
fromThis : These a b -> Maybe a
fromThis (This a) = Just a
fromThis (That _) = Nothing
fromThis (Both a _) = Just a

public export
fromThat : These a b -> Maybe b
fromThat (This _) = Nothing
fromThat (That b) = Just b
fromThat (Both _ b) = Just b

public export
these : (a -> c) -> (b -> c) -> (a -> b -> c) -> These a b -> c
these l r lr (This a)   = l a
these l r lr (That b)   = r b
these l r lr (Both a b) = lr a b

public export
bimap : (f : a -> b) -> (g : c -> d) -> These a c -> These b d
bimap f g (This a)   = This (f a)
bimap f g (That b)   = That (g b)
bimap f g (Both a b) = Both (f a) (g b)

public export
(Show a, Show b) => Show (These a b) where
  showPrec d (This x)   = showCon d "This" $ showArg x
  showPrec d (That x)   = showCon d "That" $ showArg x
  showPrec d (Both x y) = showCon d "Both" $ showArg x ++ showArg y

public export
Functor (These a) where
  map = bimap id

public export
mapFst : (f : a -> b) -> These a c -> These b c
mapFst f = bimap f id

public export
bifold : Monoid m => These m m -> m
bifold (This a)   = a
bifold (That b)   = b
bifold (Both a b) = a <+> b

public export
bitraverse : Applicative f => (a -> f c) -> (b -> f d) -> These a b -> f (These c d)
bitraverse f g (This a)   = [| This (f a) |]
bitraverse f g (That b)   = [| That (g b) |]
bitraverse f g (Both a b) = [| Both (f a) (g b) |]


text:
module Dbcritic.Check.PrimaryKey

import Control.IOExcept
import Dbcritic.Check
import Dbcritic.Libpq

mkIssue : String -> Issue
mkIssue table =
    let
        identifier  = [ table ]
        description = "The table ‘" ++ table ++ "’ is missing a primary key constraint."
        problems    = [ "Rows cannot be individually addressed when updating or deleting them."
                      , "Rows cannot be individually addressed by potential foreign keys."
                      , "Some tools expect tables to have primary keys to function properly." ]
        solutions   = [ "Create a primary key constraint on ‘" ++ table ++ "’." ]
    in
        MkIssue identifier description problems solutions IsNonEmpty IsNonEmpty IsNonEmpty

export
checkPrimaryKey : Check
checkPrimaryKey = MkCheck name help inspect
    where
    name = "primary_key"
    help = "Check that each table has a primary key constraint."

    inspectRow : List (Maybe String) -> IOExcept String Issue
    inspectRow [Just table] = pure (mkIssue table)
    inspectRow _ = ioe_fail "checkPrimaryKey: Bad result"

    inspect : PgConnection -> IOExcept String (List Issue)
    inspect conn = do
        res <- pgExecute conn """
            SELECT relname
            FROM   pg_class
            WHERE  relkind = 'r' AND
                   NOT EXISTS
                       ( SELECT
                         FROM   pg_constraint
                         WHERE  conrelid = pg_class.oid AND
                                contype  = 'p' ) AND
                   relnamespace <> regnamespace 'information_schema' AND
                   relnamespace <> regnamespace 'pg_catalog'
            ORDER BY relname ASC
        """
        traverse inspectRow (pgGrid res)

max_stars_repo_name: channable/dbcritic

max_issues_repo_name: channable/dbcritic

max_forks_repo_name: channable/dbcritic


text:
twoPlusTwoNotFive : 2 + 2 = 5 -> Void
twoPlusTwoNotFive Refl impossible

valueNotSucc : (x : Nat) -> x = S x -> Void
valueNotSucc _ Refl impossible


text:
||| The content of this module is based on the paper
||| Applications of Applicative Proof Search
||| by Liam O'Connor

module Search.HDecidable

import Data.List.Lazy
import Data.List.Lazy.Quantifiers
import Data.List.Quantifiers
import Data.So

import Search.Negation

%default total

------------------------------------------------------------------------
-- Type, basic functions, and interface

||| Half a decider: when the search succeeds we bother building the proof
public export
record HDec (a : Type) where
  constructor MkHDec
  isTrue   : Bool
  evidence : So isTrue -> a

||| Happy path: we have found a proof!
public export
yes : a -> HDec a
yes = MkHDec True . const

||| Giving up
public export
no : HDec a
no = MkHDec False absurd

public export
fromDec : Dec a -> HDec a
fromDec (Yes p) = yes p
fromDec (No _) = no

public export
fromMaybe : Maybe a -> HDec a
fromMaybe = maybe no yes

public export
toMaybe : HDec a -> Maybe a
toMaybe (MkHDec True p) = Just (p Oh)
toMaybe (MkHDec False _) = Nothing

||| A type constructor satisfying AnHdec is morally an HDec i.e. we can
||| turn values of this type constructor into half deciders
||| It may be more powerful (like Dec) or more basic (like Maybe).

public export
interface AnHDec (0 t : Type -> Type) where
  toHDec : t a -> HDec a

public export AnHDec Dec where toHDec = fromDec
public export AnHDec HDec where toHDec = id
public export AnHDec Maybe where toHDec = fromMaybe

------------------------------------------------------------------------
-- Implementations

public export
Functor HDec where
  map f (MkHDec b prf) = MkHDec b (f . prf)

public export
Applicative HDec where
  pure = yes
  MkHDec False prff <*> _ = MkHDec False absurd
  _ <*> MkHDec False _ = MkHDec False absurd
  MkHDec True prff <*> MkHDec True prfx
    = yes (prff Oh (prfx Oh))

||| Lazy in the second argument
public export
Alternative HDec where
  empty = no
  p@(MkHDec True _) <|> _ = p
  _ <|> q = q

public export
Monad HDec where
  MkHDec True x >>= f = f (x Oh)
  _ >>= _ = no

public export
Show f => Show (HDec f) where
  show (MkHDec True p) = "True: " ++ show (p Oh)
  show _ = "False"

------------------------------------------------------------------------
-- Combinators

||| Half deciders are closed under product
public export
(&&) : (AnHDec l, AnHDec r) => l a -> r b -> HDec (a, b)
p && q = [| (toHDec p, toHDec q) |]

||| Half deciders are closed under sum
public export
(||) : (AnHDec l, AnHDec r) => l a -> r b -> HDec (Either a b)
p || q = [| Left (toHDec p) |] <|> [| Right (toHDec q) |]

||| Half deciders are closed negation. Here we use the `Negates` interface
||| so that we end up looking for *positive* evidence of something which is
||| much easier to find than negative one.
public export
not : (AnHDec l, Negates na a) => l na -> HDec (Not a)
not p = [| toNegation (toHDec p) |]

infixr 3 ==>

||| Half deciders are closed under implication
public export
(==>) : (AnHDec l, AnHDec r, Negates na a) => l na -> r b -> HDec (a -> b)
p ==> q = [| contra (not p) |] <|> [| const (toHDec q) |] where
  contra : Not a -> a -> b
  contra na a = void (na a)

namespace List

  ||| Half deciders are closed under the list quantifier any
  public export
  any : AnHDec l => (xs : List a) -> ((x : a) -> l (p x)) -> HDec (Any p xs)
  any [] p = no
  any (x :: xs) p = [| Here (toHDec (p x)) |] <|> [| There (any xs p) |]

  ||| Half deciders are closed under the list quantifier all
  public export
  all : AnHDec l => (xs : List a) -> ((x : a) -> l (p x)) -> HDec (All p xs)
  all [] p = yes []
  all (x :: xs) p = [| toHDec (p x) :: all xs p |]

namespace LazyList

  ||| Half deciders are closed under the lazy list quantifier any
  public export
  any : AnHDec l => (xs : LazyList a) -> ((x : a) -> l (p x)) -> HDec (Any p xs)
  any [] p = no
  any (x :: xs) p = [| Here (toHDec (p x)) |] <|> [| There (any xs p) |]


text:
||| A simple parser combinator library for String. Inspired by attoparsec zepto.
module Data.String.Parser
import public Control.Monad.Identity
import Control.Monad.Trans

import Data.String
import Data.Fin
import Data.List
import Data.List1
import Data.Vect

%default total

||| The input state, pos is position in the string and maxPos is the length of the input string.
public export
record State where
    constructor S
    input : String
    pos : Int
    maxPos : Int

Show State where
    show s = "(" ++ show s.input ++ ", " ++ show s.pos ++ ", " ++ show s.maxPos ++ ")"

||| Result of applying a parser
public export
data Result a = Fail Int String | OK a State

Functor Result where
  map f (Fail i err) = Fail i err
  map f (OK r s)     = OK (f r) s

public export
record ParseT (m : Type -> Type) (a : Type) where
    constructor P
    runParser : State -> m (Result a)

public export
Parser : Type -> Type
Parser = ParseT Identity

public export
Functor m => Functor (ParseT m) where
    map f p = P $ \s => map (map f) (p.runParser s)

public export
Monad m => Applicative (ParseT m) where
    pure x = P $ \s => pure $ OK x s
    f <*> x = P $ \s => case !(f.runParser s) of
                            OK f' s' => map (map f') (x.runParser s')
                            Fail i err => pure $ Fail i err

public export
Monad m => Alternative (ParseT m) where
    empty = P $ \s => pure $ Fail s.pos "no alternative left"
    a <|> b = P $ \s => case !(a.runParser s) of
                            OK r s' => pure $ OK r s'
                            Fail _ _ => b.runParser s

public export
Monad m => Monad (ParseT m) where
    m >>= k = P $ \s => case !(m.runParser s) of
                             OK a s' => (k a).runParser s'
                             Fail i err => pure $ Fail i err

public export
MonadTrans ParseT where
    lift x = P $ \s => map (flip OK s) x

||| Run a parser in a monad
||| Returns a tuple of the result and final position on success.
||| Returns an error message on failure.
export
parseT : Functor m => ParseT m a -> String -> m (Either String (a, Int))
parseT p str = map (\case
                       OK r s => Right (r, s.pos)
                       Fail i err => Left $ fastAppend ["Parse failed at position ", show i, ": ", err])
                   (p.runParser (S str 0 (strLength str)))

||| Run a parser in a pure function
||| Returns a tuple of the result and final position on success.
||| Returns an error message on failure.
export
parse : Parser a -> String -> Either String (a, Int)
parse p str = runIdentity $ parseT p str

||| Combinator that replaces the error message on failure.
||| This allows combinators to output relevant errors
export
(<?>) : Functor m => ParseT m a -> String -> ParseT m a
(<?>) p msg = P $ \s => map (\case
                                OK r s' => OK r s'
                                Fail i _ => Fail i msg)
                            (p.runParser s)

infixl 0 <?>

||| Discards the result of a parser
export
skip : Functor m => ParseT m a -> ParseT m ()
skip = ignore

||| Maps the result of the parser `p` or returns `def` if it fails.
export
optionMap : Functor m => b -> (a -> b) -> ParseT m a -> ParseT m b
optionMap def f p = P $ \s => map (\case
                                     OK r s'  => OK (f r) s'
                                     Fail _ _ => OK def s)
                                  (p.runParser s)

||| Runs the result of the parser `p` or returns `def` if it fails.
export
option : Functor m => a -> ParseT m a -> ParseT m a
option def = optionMap def id

||| Returns a Bool indicating whether `p` succeeded
export
succeeds : Functor m => ParseT m a -> ParseT m Bool
succeeds = optionMap False (const True)

||| Returns a Maybe that contains the result of `p` if it succeeds or `Nothing` if it fails.
export
optional : Functor m => ParseT m a -> ParseT m (Maybe a)
optional = optionMap Nothing Just

||| Succeeds if and only if the argument parser fails.
|||
||| In Parsec, this combinator is called `notFollowedBy`.
export
requireFailure : Functor m => ParseT m a -> ParseT m ()
requireFailure (P runParser) = P $ \s => reverseResult s <$> runParser s
where
  reverseResult : State -> Result a -> Result ()
  reverseResult s (Fail _ _) = OK () s
  reverseResult s (OK _ _)   = Fail (pos s) "Purposefully changed OK to Fail"

||| Fail with some error message
export
fail : Applicative m => String -> ParseT m a
fail x = P $ \s => pure $ Fail s.pos x

||| Succeeds if the next char satisfies the predicate `f`
export
satisfy : Applicative m => (Char -> Bool) -> ParseT m Char
satisfy f = P $ \s => pure $ if s.pos < s.maxPos
                                  then let ch = assert_total $ strIndex s.input s.pos in
                                       if f ch
                                           then OK ch (S s.input (s.pos + 1) s.maxPos)
                                           else Fail s.pos "satisfy"
                                  else Fail s.pos "satisfy"

||| Succeeds if the string `str` follows.
export
string : Applicative m => String -> ParseT m String
string str = P $ \s => pure $ let len = strLength str in
                              if s.pos+len <= s.maxPos
                                  then let head = strSubstr s.pos len s.input in
                                       if head == str
                                         then OK str (S s.input (s.pos + len) s.maxPos)
                                         else Fail s.pos ("string " ++ show str)
                                  else Fail s.pos ("string " ++ show str)

||| Succeeds if the end of the string is reached.
export
eos : Applicative m => ParseT m ()
eos = P $ \s => pure $ if s.pos == s.maxPos
                           then OK () s
                           else Fail s.pos "expected the end of the string"

||| Succeeds if the next char is `c`
export
char : Applicative m => Char -> ParseT m Char
char c = satisfy (== c) <?> "char " ++ show c

||| Parses a space character
export
space : Applicative m => ParseT m Char
space = satisfy isSpace <?> "space"

||| Parses a letter or digit (a character between \'0\' and \'9\').
||| Returns the parsed character.
export
alphaNum : Applicative m => ParseT m Char
alphaNum = satisfy isAlphaNum <?> "letter or digit"

||| Parses a letter (an upper case or lower case character). Returns the
||| parsed character.
export
letter : Applicative m => ParseT m Char
letter = satisfy isAlpha <?> "letter"

mutual
    ||| Succeeds if `p` succeeds, will continue to match `p` until it fails
    ||| and accumulate the results in a list
    export
    covering
    some : Monad m => ParseT m a -> ParseT m (List a)
    some p = [| p :: many p |]

    ||| Always succeeds, will accumulate the results of `p` in a list until it fails.
    export
    covering
    many : Monad m => ParseT m a -> ParseT m (List a)
    many p = some p <|> pure []

||| Parse left-nested lists of the form `((init op arg) op arg) op arg`
export
covering
hchainl : Monad m => ParseT m init -> ParseT m (init -> arg -> init) -> ParseT m arg -> ParseT m init
hchainl pini pop parg = pini >>= go
  where
  covering
  go : init -> ParseT m init
  go x = (do op <- pop
             arg <- parg
             go $ op x arg) <|> pure x

||| Parse right-nested lists of the form `arg op (arg op (arg op end))`
export
covering
hchainr : Monad m => ParseT m arg -> ParseT m (arg -> end -> end) -> ParseT m end -> ParseT m end
hchainr parg pop pend = go id <*> pend
  where
  covering
  go : (end -> end) -> ParseT m (end -> end)
  go f = (do arg <- parg
             op <- pop
             go $ f . op arg) <|> pure f

||| Always succeeds, applies the predicate `f` on chars until it fails and creates a string
||| from the results.
export
covering
takeWhile : Monad m => (Char -> Bool) -> ParseT m String
takeWhile f = pack <$> many (satisfy f)

||| Similar to `takeWhile` but fails if the resulting string is empty.
export
covering
takeWhile1 : Monad m => (Char -> Bool) -> ParseT m String
takeWhile1 f = pack <$> some (satisfy f)

||| Parses zero or more space characters
export
covering
spaces : Monad m => ParseT m ()
spaces = skip (many space)

||| Parses one or more space characters
export
covering
spaces1 : Monad m => ParseT m ()
spaces1 = skip (some space) <?> "whitespaces"

||| Discards brackets around a matching parser
export
parens : Monad m => ParseT m a -> ParseT m a
parens p = char '(' *> p <* char ')'

||| Discards whitespace after a matching parser
export
covering
lexeme : Monad m => ParseT m a -> ParseT m a
lexeme p = p <* spaces

||| Matches a specific string, then skips following whitespace
export
covering
token : Monad m => String -> ParseT m ()
token s = lexeme (skip $ string s) <?> "token " ++ show s

||| Matches a single digit
export
digit : Monad m => ParseT m (Fin 10)
digit = do x <- satisfy isDigit
           case lookup x digits of
                Nothing => fail "not a digit"
                Just y => pure y
  where
    digits : List (Char, Fin 10)
    digits = [ ('0', 0)
             , ('1', 1)
             , ('2', 2)
             , ('3', 3)
             , ('4', 4)
             , ('5', 5)
             , ('6', 6)
             , ('7', 7)
             , ('8', 8)
             , ('9', 9)
             ]

fromDigits : Num a => (Fin 10 -> a) -> List (Fin 10) -> a
fromDigits f xs = foldl addDigit 0 xs
where
  addDigit : a -> Fin 10 -> a
  addDigit num d = 10*num + f d

intFromDigits : List (Fin 10) -> Integer
intFromDigits = fromDigits finToInteger

natFromDigits : List (Fin 10) -> Nat
natFromDigits = fromDigits finToNat

||| Matches a natural number
export
covering
natural : Monad m => ParseT m Nat
natural = natFromDigits <$> some digit

||| Matches an integer, eg. "12", "-4"
export
covering
integer : Monad m => ParseT m Integer
integer = do minus <- succeeds (char '-')
             x <- some digit
             pure $ if minus then (intFromDigits x)*(-1) else intFromDigits x

||| Parse repeated instances of at least one `p`, separated by `s`,
||| returning a list of successes.
|||
||| @ p the parser for items
||| @ s the parser for separators
export
covering
sepBy1 : Monad m => (p : ParseT m a)
                 -> (s : ParseT m b)
                 -> ParseT m (List1 a)
sepBy1 p s = [| p ::: many (s *> p) |]

||| Parse zero or more `p`s, separated by `s`s, returning a list of
||| successes.
|||
||| @ p the parser for items
||| @ s the parser for separators
export
covering
sepBy : Monad m => (p : ParseT m a)
                -> (s : ParseT m b)
                -> ParseT m (List a)
sepBy p s = optionMap [] forget (p `sepBy1` s)

||| Parses /one/ or more occurrences of `p` separated by `comma`.
export
covering
commaSep1 : Monad m => ParseT m a -> ParseT m (List1 a)
commaSep1 p = p `sepBy1` (char ',')

||| Parses /zero/ or more occurrences of `p` separated by `comma`.
export
covering
commaSep : Monad m => ParseT m a -> ParseT m (List a)
commaSep p = p `sepBy` (char ',')

||| Run the specified parser precisely `n` times, returning a vector
||| of successes.
export
ntimes : Monad m => (n : Nat) -> ParseT m a -> ParseT m (Vect n a)
ntimes    Z  p = pure Vect.Nil
ntimes (S n) p = [| p :: (ntimes n p) |]


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 6

-- check that all functions are total
%default total

data Format = Number Format
            | Doubble Format
            | Str Format
            | Chhar Format
            | Lit String Format
            | End
%name Format fmt, fmt1, fmt2, fmt3

PrintfType : Format -> Type
PrintfType (Number fmt) = (i : Int) -> PrintfType fmt
PrintfType (Doubble fmt) = (d : Double) -> PrintfType fmt
PrintfType (Str fmt) = (str : String) -> PrintfType fmt
PrintfType (Chhar fmt) = (car : Char) -> PrintfType fmt
PrintfType (Lit str fmt) = PrintfType fmt
PrintfType End = String

printFmt : (fmt : Format) -> (acc : String) -> PrintfType fmt
printFmt (Number fmt) acc = \i => printFmt fmt (acc ++ show i)
printFmt (Doubble fmt) acc = \d => printFmt fmt (acc ++ show d)
printFmt (Str fmt) acc = \str => printFmt fmt (acc ++ str)
printFmt (Chhar fmt) acc = \char => printFmt fmt (acc ++ show char)
printFmt (Lit str fmt) acc = printFmt fmt (acc ++ str)
printFmt End acc = acc

toFormat : (xs : List Char) -> Format
toFormat [] = End
toFormat ('%' :: 'd' :: chars) = Number (toFormat chars)
toFormat ('%' :: 'f' :: chars) = Doubble (toFormat chars)
toFormat ('%' :: 's' :: chars) = Str (toFormat chars)
toFormat ('%' :: 'c' :: chars) = Chhar (toFormat chars)
toFormat ('%' :: chars) = Lit "%" (toFormat chars)
toFormat (c :: chars) = case toFormat chars of
                          Lit str chars' => Lit (strCons c str) chars'
                          fmt => Lit (strCons c "") fmt

printf : (fmt : String) -> PrintfType (toFormat (unpack fmt))
printf fmt = printFmt _ ""
-- > :t printf "%s = %d"
-- printf "%s = %d" : String -> Int -> String
-- > :t printf "%c %f"
-- printf "%c %f" : Char -> Double -> String
-- > printf "%c %f" 'X' 24
-- "'X' 24.0" : String

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module JS.VarArg

%default total

-- TODO: How to handle vararg functions
export
data VarArg : Type -> Type where [external]


text:
module Verpackung.Main

import Verpackung.Derive.Derive
import Verpackung.Command
import Idrall.API.V2
import Language.JSON
import Language.Reflection
import System.File.ReadWrite
import System.File.Handle

%default covering
%hide Idrall.IOEither.IOEither -- TODO could be dodgy
%language ElabReflection

record Package where
  constructor MkPackage
  id : String
  repo : String
  ipkgFile : String
  depends : List String
%runElab (deriveFromDhall Record `{ Package })

Show Package where
  show (MkPackage id repo ipkgFile depends) =
    "MkPackage \{show id} \{show repo} \{show ipkgFile} \{show depends}"

record PackageSet where
  constructor MkPackageSet
  packages : List Package
%runElab (deriveFromDhall Record `{ PackageSet })

Show PackageSet where
  show (MkPackageSet packages)  =
    "MkPackage \{show packages}"

record PackageSetEntry where
  constructor MkPackageSetEntry
  id : String
  repo : String
  sha : Maybe String
-- %runElab (deriveFromDhall Record `{ PackageSetEntry })
%runElab deriveJSON defaultOpts `{PackageSetEntry}

Show PackageSetEntry where
  show (MkPackageSetEntry id repo sha) =
    "MkPackage \{show id} \{show repo} \{show sha}"

data BuildStatus
  = Passing PackageSetEntry
  | Failing PackageSetEntry

Show BuildStatus where
  show (Passing x) = "Passing \{show x}"
  show (Failing x) = "Failing \{show x}"

doBuild : Package -> IOEither VerpackungError BuildStatus
doBuild pkg@(MkPackage id repo ipkgFile depends) =
  let workdir = "./tmp/\{id}" in
  do
  cleanup <- exec $ MkCommand "rm" (words "-rf \{workdir}") initOpts
  cloneRes <- exec $ MkCommand "git" (words "clone \{repo} \{workdir}") initOpts
  sha <- exec $ MkCommand "git" (words "-C \{workdir} rev-parse HEAD") initOpts
  copyDepends depends
  liftIO $ buildRes workdir (trim $ stdout sha)
  where
    buildRes : String -> String -> IO BuildStatus
    buildRes workdir sha =
      case exec $ MkCommand "idris2" (words "--build \{ipkgFile}") $ MkCommandOptions $ Just workdir of
           (MkIOEither w) => do
             Right w' <- w | Left err => pure $ Failing $ MkPackageSetEntry id repo $ Just sha
             pure $ Passing $ MkPackageSetEntry id repo $ Just sha
    copyDepends : List String -> IOEither VerpackungError ()
    copyDepends [] = pure ()
    copyDepends (dep :: xs) =
      let depDir = "./tmp/\{id}/depends"
          fakeVersion = "0.10.0" -- TODO hack, need to parse this from ipkg file
      in
      do
        _ <- exec $ MkCommand "mkdir" (words "-p \{depDir}") initOpts
        _ <- exec $ MkCommand "cp" (words "-r ./tmp/\{dep}/build/ttc/ \{depDir}/\{dep}-\{fakeVersion}") initOpts
        copyDepends xs

go : List (Package, IOEither VerpackungError BuildStatus) -> IO (List BuildStatus)
go [] = pure []
go ((pkg, f) :: xs) = do
  Right res <- liftIOEither f
  | Left e => let this = Failing $ MkPackageSetEntry (id pkg) (repo pkg) Nothing in
    pure (this :: !(go xs))
  pure (res :: !(go xs))

record IdrisVersion where
  constructor MkIdrisVersion
  version : String
%runElab deriveJSON defaultOpts `{IdrisVersion}

writePackageSetToFS : String -> String -> (List PackageSetEntry, List PackageSetEntry) -> IO ()
writePackageSetToFS date version (passing, failing) =
  let packageSetDir = "./package-set/\{date}" in
  do
  _ <- liftIOEither $ exec $ MkCommand "mkdir" (words "-p \{packageSetDir}") initOpts
  putStrLn $ show version
  _ <- writeFile "\{packageSetDir}/idris-version.json" (show $ toJSON $ MkIdrisVersion version)
  putStrLn "Passing: \{show $ length passing}"
  putStrLn $ show passing
  _ <- writeFile "\{packageSetDir}/passing.json" (show $ toJSON $ passing)
  putStrLn "Failing: \{show $ length failing}"
  putStrLn $ show failing
  _ <- writeFile "\{packageSetDir}/failing.json" (show $ toJSON $ failing)
  putStrLn "Passing: \{show $ length passing}, Failing: \{show $ length failing}"
  pure ()

main : IO ()
main = do
  Right packageSet <- readPackagesDhall | Left e => putStrLn $ !(fancyError e)
  putStrLn $ show packageSet
  let xs = packages packageSet
  let pkgs = (map (\x=> (x, doBuild x)) xs)
  let final = go pkgs
  let split = splitStatus !final
  let date = !date
  let version = !idrisVersion
  case (date, version) of
       (Right date', Right version') =>
          writePackageSetToFS (trim date') version' split
       (Left x, _) => putStrLn "failed to parse date"
       (_, Left y) => putStrLn "failed to parse idris version"
  where
    readPackagesDhall : IO (Either Error PackageSet)
    readPackagesDhall = liftIOEither $ deriveFromDhallString {ty=PackageSet} "./package-set/packages.dhall"
    splitStatus : List BuildStatus -> (List PackageSetEntry, List PackageSetEntry)
    splitStatus [] = ([], [])
    splitStatus (x :: xs) =
      let rest = splitStatus xs in
      case x of
           (Passing y) => (y :: fst rest, snd rest)
           (Failing y) => (fst rest, y :: snd rest)
    idrisVersion : IO (Either VerpackungError String)
    idrisVersion = getStdout $ MkCommand "idris2" ["--version"] initOpts
    date : IO (Either VerpackungError String)
    date = getStdout $ MkCommand "date" ["+%Y%m%d"] initOpts

max_stars_repo_name: alexhumphreys/verpackung

max_issues_repo_name: alexhumphreys/verpackung

max_forks_repo_name: alexhumphreys/verpackung


text:
double : Num ty => ty -> ty
double x = x + x

add : Num ty => ty -> ty -> ty
add x y = x + y

identity : ty -> ty
identity x = x

twice: (a -> a) -> a -> a
twice f x = f (f x)

quadruple : Num a => a -> a
quadruple = twice double

longer : String -> String -> Nat
longer word1 word2
  = let len1 = length word1
        len2 = length word2 in
        if len1 > len2 then len1 else len2

palindrome : Nat -> String -> Bool
palindrome delim str
  = let len = length str
        forwards = toLower str
        backwards = reverse (toLower str) in
    if len > delim then forwards == backwards else False

counts : String -> (Nat, Nat)
counts str = (length (words str), length str)

top_ten : Ord a => List a -> List a
top_ten lst = take 10 (reverse (sort lst))

over_length : Nat -> List String -> Nat
over_length delim strs = length (
  filter (\x : String => length x > delim) strs)