text:
%unbound_implicits off

record JamesBondTheme where
  isVinyl : Bool

-- The James Bond Equality states that for every record field `f`,
-- the prefix form `f` must be definitionally equal to `.f`.
jbeq : isVinyl = (.isVinyl)
jbeq = Refl

-- Then its applications are seamlessly interchangeable, too.
jbeqApp : (rec : JamesBondTheme) -> isVinyl rec = rec.isVinyl
jbeqApp _ = Refl


text:
%hint
mycong : (f : a -> b) -> x = y -> f x = f y
mycong f Refl = Refl

plusZ : (n : Nat) -> plus n Z = n

plusS : (n : Nat) -> (m : Nat) -> plus n (S m) = S (plus n m)

ext: idr


text:
module Markdown.String

import Data.Nat
import Text.Lexer
import Text.Quantity

%default total

export
headingSym : Lexer
headingSym
  = some (is '#')

export
imageSym : Lexer
imageSym
  = is '!'

export
newLine : Lexer
newLine = is '\n'

export
italicsSym : Lexer
italicsSym = is '_'

export
boldSym : Lexer
boldSym =
  count (exactly 2) (is '*')

export
link : Lexer
link =
      surround (is '[') (is ']') any
  <+> surround (is '(') (is ')') any

||| Note: we currently don't allow attributes
||| To do so, we might need to move this from the lexer into the parser
export
htmlOpenTag : Lexer
htmlOpenTag =
  surround (is '<') (is '>') alphaNum

export
htmlCloseTag : Lexer
htmlCloseTag =
  surround (exact "</") (is '>') alphaNum

export
pre : Lexer
pre = quote (is '`') (non newline)

export
codeFence : Lexer
codeFence = quote (exact "```") any

-- Grab the next non-newline character (even if it's special, like a *),
-- and then consume non-special characters until we find another special marker.
export
text : Lexer
text = (isNot '\n') <+> manyUntil (oneOf "_*\n<>#[]()`") any

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
> module SequentialDecisionProblems.FullTheory

> import SequentialDecisionProblems.CoreTheory

> import Sigma.Sigma
> import Sigma.Operations

> %default total
> %access public export
> %auto_implicits off

> -- %hide Prelude.Nat.LTE

* Preliminaries

In order to prove the correctness of |backwardsInduction| (see
|CoreTheory|), we need a number of additional assumptions, which we
introduce here.  These result in proof obligations for the user of the
framework.  As in |CoreTheory|, they are represented as meta-variables
(or ``holes'').  Once the user has discharged these obligations, type
checking this file will prove the optimality of |backwardsInduction|
(with some caveats related to the current Idris implementation).

* |LTE|

The binary relation introduced in |CoreTheory| for comparing values of
sequences of policies has to be a preorder:

> reflexiveLTE : (a : Val) -> a `LTE` a
> transitiveLTE : (a : Val) -> (b : Val) -> (c : Val) -> a `LTE` b -> b `LTE` c -> a `LTE` c

Additionally, |plus| is required to be monotonic with respect to |LTE|:

> monotonePlusLTE : {a, b, c, d : Val} -> a `LTE` b -> c `LTE` d -> (a `plus` c) `LTE` (b `plus` d)

* |meas|

The function |meas| introduced in |CoreTheory| to describe how a
decision maker measures the possible rewards entailed by (lists,
probability distributions, etc. of) possible next states is required to
fulfill a monotonicity condition:

> measMon  :  {A : Type} ->
>             (f : A -> Val) -> (g : A -> Val) ->
>             ((a : A) -> (f a) `LTE` (g a)) ->
>             (ma : M A) -> meas (fmap f ma) `LTE` meas (fmap g ma)

In a nutshell, |measMon| says that, if |ma| and |mb| are similar
|M|-structures and |ma| is smaller or equal to |mb|, than it cannot be
the case that the measure of |ma| is greater than the measure of |mb|.

This conditions was originally formalized by Ionescu in [2] to give a
consistent meaning to harm measures in vulnerability studies.

* |cvalargmax|

The function |cvalargmax| introduced in |CoreTheory| must deliver
optimal controls.  We need the function |cvalmax|, returning the value
of those optimal controls, in order to fully specify |cvalargmax|:

> cvalmax  :  {t, n : Nat} ->
>             (x : State t) -> (r : Reachable x) -> (v : Viable (S n) x) ->
>             (ps : PolicySeq (S t) n) -> Val

> cvalargmaxSpec  :  {t : Nat} -> {n : Nat} ->
>                    (x  : State t) -> (r  : Reachable x) ->
>                    (v  : Viable (S n) x) ->  (ps : PolicySeq (S t) n) ->
>                    cvalmax x r v ps = cval x r v ps (cvalargmax x r v ps)

> cvalmaxSpec  :  {t : Nat} -> {n : Nat} ->
>                 (x  : State t) -> (r  : Reachable x) ->
>                 (v  : Viable (S n) x) ->  (ps : PolicySeq (S t) n) ->
>                 (y : GoodCtrl t x n) ->
>                 (cval x r v ps y) `LTE` (cvalmax x r v ps)

The reason for using these very specific functions, instead of more
general |argmax|, |max|, |argmaxSpec| and |maxSpec| like for instance

< argmax : {t : Nat} -> {n : Nat} ->
<          (x : State t) -> (Viable (S n) x) ->
<          (f : GoodCtrl t x n -> Val) -> GoodCtrl t x n

< max    : {t : Nat} -> {n : Nat} ->
<          (x : State t) -> (Viable (S n) x) ->
<          (f : GoodCtrl t x n -> Val) -> Val

< argmaxSpec : {t : Nat} -> {n : Nat} ->
<              (x : State t) -> (v : Viable (S n) x) ->
<              (f : GoodCtrl t x n -> Val) ->
<              max x v f = f (argmax x v f)

< maxSpec : {t : Nat} -> {n : Nat} ->
<           (x : State t) -> (v : Viable (S n) x) ->
<           (f : GoodCtrl t x n -> Val) -> (y : GoodCtrl t x n) ->
<           (f y) `LTE` (max x v f)

is that optimisation is, in most case, not computable.  The assumptions
on |cvalmax| and |cvalargmax| are the minimal requirements for the
computability of optimal extensions. Anything more general risks being
non-implementable.

* The proof of correctness of |backwardsInduction|:

** Policy sequences of length zero are optimal

> |||
> nilOptPolicySeq : OptPolicySeq Nil
> nilOptPolicySeq ps' x r v = reflexiveLTE zero

** Bellman's principle of optimality:

> |||
> Bellman  :  {t, m : Nat} ->
>             (ps  :  PolicySeq (S t) m)  ->   OptPolicySeq ps ->
>             (p   :  Policy t (S m))     ->   OptExt ps p ->
>             OptPolicySeq (p :: ps)

> Bellman {t} {m} ps ops p oep = opps where
>   opps : OptPolicySeq (p :: ps)
>   {-
>   opps (p' :: ps') x r v = transitiveLTE (val x r v (p' :: ps'))
>                                          (val x r v (p' :: ps))
>                                          (val x r v (p :: ps))
>                                          s4 s5 where
>   -}
>   opps x r v (p' :: ps') = transitiveLTE (val x r v (p' :: ps'))
>                                          (val x r v (p' :: ps))
>                                          (val x r v (p :: ps))
>                                          s4 s5 where
>     gy' : GoodCtrl t x m
>     gy' = p' x r v
>     y'  : Ctrl t x
>     y'  = ctrl gy'
>     mx' : M (State (S t))
>     mx' = nexts t x y'
>     av' : All (Viable m) mx'
>     av' = allViable gy'
>     f' : PossibleNextState x (ctrl gy') -> Val
>     f' = sval x r v gy' ps'
>     f  : PossibleNextState x (ctrl gy') -> Val
>     f  = sval x r v gy' ps
>     s1 : (x' : State (S t)) -> (r' : Reachable x') -> (v' : Viable m x') ->
>          val x' r' v' ps' `LTE` val x' r' v' ps
>     -- s1 x' r' v' = ops ps' x' r' v'
>     s1 x' r' v' = ops x' r' v' ps'
>     s2 : (z : PossibleNextState x (ctrl gy')) -> (f' z) `LTE` (f z)
>     s2 (MkSigma x' x'emx') =
>       monotonePlusLTE (reflexiveLTE (reward t x y' x')) (s1 x' r' v') where
>         ar' : All Reachable mx'
>         ar' = reachableSpec1 x r y'
>         r'  : Reachable x'
>         r'  = allElemSpec0 x' mx' ar' x'emx'
>         v'  : Viable m x'
>         v'  = allElemSpec0 x' mx' av' x'emx'
>     s3 : meas (fmap f' (tagElem mx')) `LTE` meas (fmap f (tagElem mx'))
>     s3 = measMon f' f s2 (tagElem mx')
>     s4 : val x r v (p' :: ps') `LTE` val x r v (p' :: ps)
>     s4 = s3
>     s5 : val x r v (p' :: ps) `LTE` val x r v (p :: ps)
>     -- s5 = oep p' x r v
>     s5 = oep x r v p'

> |||
> optExtLemma  :  {t, n : Nat} ->
>                 (ps : PolicySeq (S t) n) -> OptExt ps (optExt ps)
> {-
> optExtLemma {t} {n} ps p' x r v = s5 where
>   p     :  Policy t (S n)
>   p     =  optExt ps
>   gy    :  GoodCtrl t x n
>   gy    =  p x r v
>   y     :  Ctrl t x
>   y     =  ctrl gy
>   av    :  All (Viable n) (nexts t x y)
>   av    =  allViable gy
>   gy'   :  GoodCtrl t x n
>   gy'   =  p' x r v
>   y'    :  Ctrl t x
>   y'    =  ctrl gy'
>   av'   :  All (Viable n) (nexts t x y')
>   av'   =  allViable gy'
>   f     :  PossibleNextState x (ctrl gy) -> Val
>   f     =  sval x r v gy ps
>   f'    :  PossibleNextState x (ctrl gy') -> Val
>   f'    =  sval x r v gy' ps
>   s1    :  cval x r v ps gy' `LTE` cvalmax x r v ps
>   s1    =  cvalmaxSpec x r v ps gy'
>   s2    :  cval x r v ps gy' `LTE` cval x r v ps (cvalargmax x r v ps)
>   s2    =  replace {P = \ z => (cval x r v ps gy' `LTE` z)} (cvalargmaxSpec x r v ps) s1
>   -- the rest of the steps are for the (sort of) human reader
>   s3    :  cval x r v ps gy' `LTE` cval x r v ps gy
>   s3    =  s2
>   s4    :  meas (fmap f' (tagElem (nexts t x y'))) `LTE` meas (fmap f (tagElem (nexts t x y)))
>   s4    =  s3
>   s5    :  val x r v (p' :: ps) `LTE` val x r v (p :: ps)
>   s5    =  s4
> -}
> optExtLemma {t} {n} ps x r v p' = s5 where
>   p     :  Policy t (S n)
>   p     =  optExt ps
>   gy    :  GoodCtrl t x n
>   gy    =  p x r v
>   y     :  Ctrl t x
>   y     =  ctrl gy
>   av    :  All (Viable n) (nexts t x y)
>   av    =  allViable gy
>   gy'   :  GoodCtrl t x n
>   gy'   =  p' x r v
>   y'    :  Ctrl t x
>   y'    =  ctrl gy'
>   av'   :  All (Viable n) (nexts t x y')
>   av'   =  allViable gy'
>   f     :  PossibleNextState x (ctrl gy) -> Val
>   f     =  sval x r v gy ps
>   f'    :  PossibleNextState x (ctrl gy') -> Val
>   f'    =  sval x r v gy' ps
>   s1    :  cval x r v ps gy' `LTE` cvalmax x r v ps
>   s1    =  cvalmaxSpec x r v ps gy'
>   s2    :  cval x r v ps gy' `LTE` cval x r v ps (cvalargmax x r v ps)
>   s2    =  replace {P = \ z => (cval x r v ps gy' `LTE` z)} (cvalargmaxSpec x r v ps) s1
>   -- the rest of the steps are for the (sort of) human reader
>   s3    :  cval x r v ps gy' `LTE` cval x r v ps gy
>   s3    =  s2
>   s4    :  meas (fmap f' (tagElem (nexts t x y'))) `LTE` meas (fmap f (tagElem (nexts t x y)))
>   s4    =  s3
>   s5    :  val x r v (p' :: ps) `LTE` val x r v (p :: ps)
>   s5    =  s4

** Correctness of backwards induction

> backwardsInductionLemma : (t : Nat) -> (n : Nat) -> OptPolicySeq (backwardsInduction t n)
> backwardsInductionLemma t  Z     =  nilOptPolicySeq
> backwardsInductionLemma t (S n)  =  Bellman ps ops p oep where
>   ps   :  PolicySeq (S t) n
>   ps   =  backwardsInduction (S t) n
>   ops  :  OptPolicySeq ps
>   ops  =  backwardsInductionLemma (S t) n
>   p    :  Policy t (S n)
>   p    =  optExt ps
>   oep  :  OptExt ps p
>   oep  =  optExtLemma ps

Thus, we can compute provably optimal sequences of policies for
arbitrary SDPs and number of decision steps.

> {-

> ---}

[1] Bellman, Richard; "Dynamic Programming", Princeton University Press,
    1957

[2] Ionescu, Cezar; "Vulnerability Modelling and Monadic Dynamical
    Systems", Freie Universitaet Berlin, 2009

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
import Data.Vect
||| Modeled from https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf page 10

data ANTContext : {n: Nat} -> Type

data Binding : ANTContext -> Type

||| All contexts that are definable using this structure are valid.
|||
||| They can have variables added into them as specified by Binding
data ANTContext : {n: Nat} -> Type where
  Empty : ANTContext {n=0}
  AddBinding : (ctx : ANTContext {n=n})
                -> (b : Binding ctx)
                -> ANTContext {n=S n}

data ANTExp : ANTContext -> Type

||| This simple returns TypeN
||| Since data constructors can't recursively reference each other, this
||| breaks the loop
mkTypeN : (g : ANTContext) -> Nat -> ANTExp g

typeForExp : {g : ANTContext} -> ANTExp g -> ANTExp g

||| Context B encompass context A if any expression that is implied
||| by A can also be implied by B. This means that no matter what vars
||| are added to a context, it still implies *at least* the same
||| expressions as it did before. B is a descendent of A
|||
||| In other words, an *inner* context can reference anything from
||| an *outer* context, and all context applied in the outer also
||| apply to the inner.
|||
||| Ex: let x = (15 : Int) in (let y = 3 : Int) in x + y)
|||                           ^^^^^^^^^^^^^^^^^^^^^^^^^^^ -- outer context (A), x is defined
|||      inner context (B), x and y are defined -- ^^^^^
data ContextEncompasses : (des : ANTContext) -> (anc : ANTContext)
     -> Type where
  Self : {self : ANTContext} -> ContextEncompasses self self
  Child : (b : Binding anc) -> {prf : ContextEncompasses des anc}
         -> ContextEncompasses des (AddBinding anc b)

||| Represents a variable into the context. Note this is not the same thing
||| as creating a Lam/Pi/Let Expression. It is rather the resulting
||| context to be used *within* the body of a lam/pi/let expression that
||| has been created. Ex:
|||
||| Let x = (16 : Int) in (....)
|||                        ^^^^-- binding should be added to context for this part
|||
||| See ANTExp.Lam to create a Lam, etc.
|||
data Binding : (ctx : ANTContext) -> Type where
  |||  G |- S' : Type(i)
  |||  ------------------
  |||  G;\x:S' |- valid
  LamBinding : (S' : ANTExp ctx)
            -> (typeForExp S' = (mkTypeN ctx i)) -> Binding ctx

  |||  G |- S' : Type(i)
  |||  ------------------
  |||  G;forall x:S' |- valid
  PiBinding : (S' : ANTExp ctx)
            -> (typeForExp S' = (mkTypeN ctx i)) -> Binding ctx

  |||  G |- S' : Type(i)    G |- s : S'
  |||  --------------------------------
  |||  G;let x = s : S' |- valid
  LetBinding : (S' : ANTExp ctx)
            -> (typeForExp S' = (mkTypeN ctx i))
            -> (s : ANTExp ctx)
            -> (typeForExp s = S')
            -> Binding ctx

--isEquivalentExp : ANTExp des -> ANTExp anc -> ContextEncompasses des anc -> Type

alphaEq : ANTExp g -> ANTExp g -> Type

||| This is a *valid* expression of the context. An expression can
||| only be created if a context implies it by running one or more of
||| its base rules
|||
||| Basically if a rule ends in:
|||    ....
|||    -------
|||    G |- x
||| then this represents that "G |- x" is true, according to the rules
data ANTExp : ANTContext -> Type where

  ||| This is our own made up rule. It's not in the design doc, but it
  ||| inherently implied:
  |||
  |||  G |- X
  |||  ---------
  |||  G;a |- X
  |||
  ||| It means that if you add a new variable, a to G, everything that
  ||| G implied before is still valid
  ChildContextImpliesSame :
    (parent : ANTContext) -> (b : Binding parent) -> ANTExp parent -> ANTExp (AddBinding parent b)

  |||       G |- valid
  |||  Type ------------
  |||       G |- Type(n) : Type(n+1)
  ||| Part 1: Every context implies Type(n) exists
  ||| Part 2 of this, that TypeN has a Type(n+1) is in typeForExpr
  TypeN : (g : ANTContext) -> (n : Nat) -> ANTExp g

  |||       (\x:S) in G
  |||  Var1 ------------
  |||       G |- x : S
  |||
  |||       (forall x:S) in G
  |||  Var2 ------------
  |||       G |- x : S
  |||
  |||       (let x = s : S) in G
  |||  Var3 ------------
  |||       G |- x : S
  ||| Part 1: A valid var lookup
  ||| Part 2 of this, that x has a type of S, is in typeForExpr
  Var : (g : ANTContext {n} ) -> (n : Fin n) -> ANTExp g

  |||         G;forall x:S' |- T : Type(m)    G |- S' : Type(n)
  ||| Forall  ------------------------------------------------- (Exists(p).m <= p, n <= p)
  |||         G |- (x : S') -> T : Type(p)
  |||
  ||| Note that T is in (G;forall x:S'), but even so, (x : S') -> T is
  ||| in G The idea being if you can create a context from G that has
  ||| the additional "forall x:S'" in it and it implies that T exists,
  ||| then you can say that "(x : S') -> T" aka "forall x:S'.T" is implied
  ||| in G
  -- TODO 2 this only represents that (x : S') -> T is created, it doesn't specify
  --  the type as Type(p).. should we specify type in typeForExp??? seems so
  Pi : { n : Nat }
    -> (g : ANTContext)
    -> (S' : ANTExp g)
    -> (prf : typeForExp S' = (mkTypeN g n))
    -> (T : ANTExp (AddBinding g (PiBinding S' prf)))
    -> ANTExp g

  |||     G;\x:S' |- e : T   G |- (x : S') -> T : Type(n)
  ||| Lam ---------------------------------------------
  |||     G |- \x:S'.e : (x : S') -> T
  |||
  ||| Note, not in rule, but implied (S' : Type(n))... must be because
  ||| that's the only way to create G;\x:S', see Binding
  |||
  ||| Given a context, an arg type within that context, and an expression
  ||| that uses that var, returns a Lam.
  Lam : (g : ANTContext {n=i})
    -> (S' : ANTExp g)
    -> (prf : typeForExp S' = (mkTypeN g i)) -- necessary because LamBinding needs it
    -> (T : ANTExp g)
    -> (e : ANTExp (AddBinding g (LamBinding S' prf)))
    -> alphaEq (typeForExp e) (ChildContextImpliesSame g (LamBinding S' prf) T)
    -> ANTExp g

alphaEq (ChildContextImpliesSame parent b x) (ChildContextImpliesSame parent b y) = alphaEq x y
alphaEq (ChildContextImpliesSame parent b x) y@(TypeN (AddBinding parent b) n) = alphaEq x y
alphaEq (ChildContextImpliesSame parent b x) (Var (AddBinding parent b) n2) = Void --TODO this is wrong, because if child is a var, then it could be referencing the same
alphaEq (ChildContextImpliesSame parent b x) (Pi (AddBinding parent b) S' prf T) = Void
alphaEq (ChildContextImpliesSame parent b x) (Lam (AddBinding parent b) S' prf T e y) = Void
alphaEq x@(TypeN g n) y = x = y
alphaEq x@(Var g n2) y = x = y --TODO 2 this is wrong, because we have to take into account a parent context referencing same var as a child, ChildContextImpliesSame
alphaEq x@(Pi g S' prf T) y = x = y
alphaEq x@(Lam g S' prf T e x) y = x = y

mkTypeN g k = TypeN g k

{-

-- lemmaVarStillExists : (g : ANTContext) -> (e : ANTExp g)
--                     -> (e2 : ANTExp (AddVar g binder

lemmaLamTypeOfTypeIsTypeN : (n : Nat) -> (argType : ANTExp g) -> (i : Nat)
                    -> typeForExp argType = mkTypeN g i

lemmaPiTypeOfTypeIsTypeN : (n : Nat) -> (argType : ANTExp g) -> (i : Nat)
  -> typeForExp argType = mkTypeN g i

typeForExp (TypeN g n) = TypeN g (S n)
--typeForExp (Lam g argType exp) = ?typeForExp_rhs_2
typeForExp (Pi g S' prf T) = TypeN g ?chooseNForPi
  where
    chooseNForPi : {g : ANTContext} -> ANTExp g -> ANTExp g -> Nat
    chooseNForPi x y = ?chooseNForPi_rhs

{-
||| All contexts that are definable using this structure are valid.
|||
||| They can have variables added into them.  Variables come in 3
||| times, Lambda, Forall, and Let
|||
||| TODO 3 - Not sure why we need seperate types, idris impl decl says
||| "We record the binding ||| form in the context, as well as the
||| type, because type checking relies on evaluation. In particular,
||| let bound names may reduce."
--TODO 2.5 do we need "n"?
data ANTContext :  {n : Nat} -> Type where
  |||
  |||  --------
  |||  |- valid
  Empty : ANTContext {n}

  |||  G |- S' : Type(i)
  |||  ------------------
  |||  G;\x:S' |- valid
  |||
  |||  G |- S' : Type(i)
  |||  ------------------
  |||  G;forall x:S' |- valid
  |||
  ||| Adds a variable into the context. Note this is not the same
  ||| thing as creating a Lam Expression. It is rather the resulting
  ||| context to be used *within* the body of a lam expression that
  ||| has been created
  |||
  ||| See ANTExp.Lam to create a Lam, etc.
  AddVar : {i : Nat} -> {n : Nat} -> (ctx : ANTContext {n=n})
    -> (binder : Binder)
    -> (S' : ANTExp ctx)
    -> (typeForExp S' = (mkTypeN ctx i))
    -> ANTContext {n=n} -- HACK {n=S n}

    |||  G |- S : Type(i)
  |||  ------------------
  |||  G;forall x:S |- valid
  AddForallVar : {S : Expr} -> {i : Nat} -> (ctx : ANTContext)
    -> ImpliesExpr ctx (TypedExp S (TypeN i))
    -> ANTContext {S n}

  |||  G |- S : Type(i)   G |- s : S
  |||  --------------------------------
  |||  G;let x => s : S |- valid
  AddForallVar : {s : Expr} -> {S : Expr} -> {i : Nat} -> (ctx : ANTContext)
    -> ImpliesExpr ctx (TypedExp S (TypeN i))
    -> ImpliesExpr ctx (TypedExp s S)
    -> ANTContext {S n}

data ImpliesExpr : ANTContext -> TypedExp -> Type

||| Context
||| @n total number of vars
data ANTContext : {n : Nat} -> Type
data Expr : ANTContext -> Type
data ANTTypedExp : {ctx : ANTContext} -> (exp : Expr ctx) -> (typ : Expr ctx) -> Type where

||| Modeled from https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf page 10
data ANTContext : {n : Nat} -> Type where
  |||
  |||  --------
  |||  |- valid
  Empty : ANTContext {n=0}

  |||  G |- S : Type(i)
  |||  ------------------
  |||  G;\x:S |- valid
  AddVar : (ctx : ANTContext {n}) -> Expr ctx -> ANTContext {n=(S n)}

getExprLemma1 : ANTContext -> Expr ctx -> Expr (AddVar ctx unrelatedVar)

||| TODO 2 getExpr doesn't prove it's getting the right expression
||| it could return anything. We need a view
getExpr : {n : Nat} -> (ctx : ANTContext {n}) -> Fin n -> ANTTypedExp ctx

betaEq : Expr ctx -> Expr ctx -> Type
betaEq = ?x

-- I Int | BI Integer | Fl Double | Ch Char | Str String

||| This represents when a context implies something. It is laid out
||| as the basic rules of the type theory system
||| Modeled from https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf page 11
data Expr : ANTContext -> Type where
  |||  G |- valid
  |||  ------------
  |||  G |- Int : Type(0)
  ||| Part 1: the type "Int" can be implied from any context
  IntT : {ctx : ANTContext} -> Expr ctx

  |||  G |- valid
  |||  ------------
  |||  G |- Type(n) : Type(n+1)
  ||| Part 1: Every context implies Type(n) exists
  ||| Part 2 of this, that TypeN has a Type(n+1) is in data ANTType
  TypeN : (n : Nat) -> (g : ANTContext) -> Expr g

  |||  G |- valid
  |||  ------------
  |||  G |- i : Int
  IntC : {g : ANTContext} -> (i : Int) -> Expr g

  |||     G |- f : (x : S) -> T   G |- s : S
  ||| App ----------------------------------
  |||     G |- f s : T[s/x]
  App : (ctx : ANTContext {n})
    -> Ex
    -> (sInd : Fin n)
    -> betaEq (getExpr ctx fInd) (getExpr ctx sInd)
    -> Expr ctx
  |||     G;\x:S |- e : T   G |- (x : S) -> T : Type(n)
  ||| Lam ---------------------------------------------
  |||     G |- \x:S.e : (x : S) -> T
  ||| Given a context, an arg type within that context, and an expression
  ||| that uses that var, returns a Lam (variable name not specified
  ||| since we are using DeBrujin indexes)
  Lam : (ctx : ANTContext) -> (argType : Expr ctx)
    -> Expr (AddVar ctx argType) -> Expr ctx

||| This is an expression with an associated type.
|||
||| Note that the type is just a plain expression, even though, every
||| expression must have a type. This is because we can't have a typed
||| expression refer to itself in it's declaration, or it becomes an
||| infinite loop.
data ANTTypedExp : {ctx : ANTContext} -> (exp : Expr ctx) -> (typ : Expr ctx) -> Type where
  |||  G |- valid
  |||  ------------
  |||  G |- Type(n) : Type(n+1)
  ||| Part 2 TypeN has a Type(n+1) is in data ANTType
  TypeSNofN : (n : Nat) -> (g : ANTContext) -> ANTTypedExp (TypeN n g) (TypeN (S n) g)

  |||  G |- valid
  |||  ------------
  |||  G |- Int : Type(0)
  ||| Part 2 The type of Int is Type(0)
  Type0OfIntT : (g : ANTContext) -> ANTTypedExp IntT (TypeN 0 g)

  |||  G |- valid
  |||  ------------
  |||  G |- Int : Type(0)
  ||| Part 2 The type of IntC is IntT
  IntTOfInt : (i : Int) -> (g : ANTContext) -> ANTTypedExp (IntC i) IntT

getExprLemma1 x y = ?getExprLemma1_rhs

getExpr {n = Z} Empty FZ impossible
getExpr {n = Z} Empty (FS _) impossible
getExpr {n = (S k)} (AddVar ctx val) FZ = getExprLemma1 ctx val
getExpr {n = (S k)} (AddVar ctx val) (FS x) = getExprLemma1 ctx (getExpr ctx x)
-}

{-

||| Constants, c ::= Type i  (type universes)
|||                | i (integer literal)
|||                | str (string literal)
data ANTConst : Type where
  CType : Nat -> ANTConst
  CInt : Int -> ANTConst
  CStr : String -> ANTConst

||| Binders, b ::= \x : t (abstraction)
|||              | let x => t : t (let binding)
|||              | forall x : t (function space)
data ANTBinder : Type where
  BAbs : {n : Nat} -> ANTBinder
  BLet : {n : Nat} -> ANTBinder
  BForall : {n : Nat} -> ANTBinder

||| Terms, t ::= c (constant)
|||            | x (variable)
|||            | b. t (binding)
|||            | t t (application)
|||            | T (type constructor)
|||            | D (data constructor)
data ANTTerm : Type where
  TConst : ANTConst -> ANTTerm
  ||| each var has a name that must be unique
  TVar : String -> ANTTerm
  TBinding : ANTBinder -> ANTTerm
  TApp : ANTTerm -> ANTTerm -> ANTTerm
  TTypeCons : ANTTerm -- TODO 2 how to represent this?
  TDataCons : ANTTerm -- TODO 2 how to represent this?

data ContextualExpr : ANTTerm -> Type where
  TConst :

data ANTContext :  {n : Nat} -> Type where
  |||
  |||  --------
  |||  |- valid
  Empty : ANTContext {n}

  |||  G |- S : Type(i)
  |||  ------------------
  |||  G;\x:S |- valid
  AddLambdaVar : (n : Nat) -> (i : Nat) -> (varName : String)
    -> (ctx : ANTContext {n})
    -> (S : ContextualExpr ctx (TypeN i))
    -> ANTContext {n=S n}

-}
-}


text:
module Generics.Newtype.Fractional

import Generics.Newtype.Num

import Generics.Derive
%language ElabReflection

--------------------------------------------------------------------------------
--          Fractional
--------------------------------------------------------------------------------

public export %hint
FractionalToNumNP : NP (Fractional . f) ks -> NP (Num . f) ks
FractionalToNumNP = mapNP (\_ => materialize Num)

public export %hint
FractionalToNumPOP : POP (Fractional . f) kss -> POP (Num . f) kss
FractionalToNumPOP = mapPOP (\_ => materialize Num)

-- Derivation of Fractional for n-ary products or newtypes
-- e.g. `(a,b,c)` or `data Foo a = MkFoo a`  or  `data Foo = Foo Int`

-- n-ary products, e.g. (a,b,c)   (data Foo x y = MkFoo x y)
public export
NP (Fractional . f) ks => Fractional (NP f ks) where
  (/) = hcliftA2 (Fractional . f) (/)
  recip = hcliftA (Fractional . f) recip

-- This type of deriving is for newtypes so we restrict oursellves to single constructor types.
public export
(all : NP (Fractional . f) [k']) => Fractional (NS f [k']) where
  (/) {all = _::_} (Z x) (Z y) = Z $ x / y
  recip {all = _::_} (Z x) = Z (recip x)

public export
POP (Fractional . f) kss => Fractional (POP f kss) where
  (/) = hcliftA2 (Fractional . f) (/)
  recip = hcliftA (Fractional . f) recip

public export
POP (Fractional . f) [ks] => Fractional (SOP_ k f [ks]) where
  MkSOP x / MkSOP y = MkSOP $ x / y
  recip (MkSOP n) = MkSOP $ recip n

export
genericDivFractional : Generic t [code] => POP Fractional [code] => t -> t -> t
genericDivFractional x y = to $ (/) (from x) (from y)

export
genericRecip : Generic t [code] => POP Fractional [code] => t -> t
genericRecip = to . recip . from

export
||| Derives a `Fractional` implementation for the given data type
||| and visibility.
FractionalVis : Visibility -> DeriveUtil -> InterfaceImpl
FractionalVis vis g = MkInterfaceImpl "Fractional" vis []
                       `(MkFractional genericDivFractional genericRecip)
                       (implementationType `(Fractional) g)

export
||| Alias for `EncodeVis Public`.
Fractional : DeriveUtil -> InterfaceImpl
Fractional = FractionalVis Public


text:
> module SimpleProb.MonadicOperations

> import Data.List
> import Data.List.Quantifiers
> import Syntax.PreorderReasoning

> import SimpleProb.SimpleProb
> import SimpleProb.BasicOperations
> import SimpleProb.BasicProperties
> import NonNegRational.NonNegRational
> import NonNegRational.BasicOperations
> import NonNegRational.BasicProperties
> import Nat.Positive
> import Fraction.Normal
> import Num.Refinements
> import Fun.Operations
> import List.Operations
> import List.Properties
> import Sigma.Sigma

> %default total
> %access public export
> %auto_implicits off

* |SimpleProb| is a functor:

> |||
> fmap : {A, B : Type} -> (A -> B) -> SimpleProb A -> SimpleProb B
> fmap f (MkSimpleProb aps s1p) = MkSimpleProb aps' s1p' where
>   aps' : List (B, NonNegRational)
>   aps' = map (cross f id) aps
>   s1p' : sumMapSnd aps' = 1
>   s1p' = trans s1 (trans s2 s3) where
>     s1 : sumMapSnd aps' = sum (map snd aps')
>     s1 = Refl
>     s2 : sum (map snd aps') = sum (map snd aps)
>     s2 = cong (mapSndMapCrossAnyIdLemma f aps)
>     s3 : sum (map snd aps) = 1
>     s3 = s1p
>
> {-
>   s1p' = ( sumMapSnd aps' )
>        ={ Refl }=
>          ( sum (map snd aps') )
>        ={ cong (mapSndMapCrossAnyIdLemma f aps) }=
>          ( sum (map snd aps) )
>        ={ Refl }=
>          ( sumMapSnd aps )
>        ={ s1p }=
>          ( 1 )
>        QED
> -}

* |SimpleProb| is a monad:

> |||
> ret : {A : Type} -> A -> SimpleProb A
> ret {A} a = MkSimpleProb [(a, 1)] (sumMapSndSingletonLemma a 1)

> |||
> bind : {A, B : Type} -> SimpleProb A -> (A -> SimpleProb B) -> SimpleProb B
> bind {A} {B} (MkSimpleProb aps s1p) f = MkSimpleProb bps' s1p' where
>   f' : A -> List (B, NonNegRational)
>   f' a = toList (f a)
>   s1ps' : (a : A) -> sumMapSnd (f' a) = 1
>   s1ps' a = toListLemma (f a)
>   bps' : List (B, NonNegRational)
>   bps' = mvMult aps f'
>   s1p' : sumMapSnd bps' = 1
>   s1p' = ( sumMapSnd bps' )
>        ={ Refl }=
>          ( sumMapSnd (mvMult aps f') )
>        ={ mvMultLemma aps f' s1ps' }=
>          ( sumMapSnd aps )
>        ={ s1p }=
>          ( 1 )
>        QED

* |SimpleProb| is a container monad:

> |||
> Elem : {A : Type} -> A -> SimpleProb A -> Type
> Elem a sp = Elem a (support sp)

> |||
> NonEmpty : {A : Type} -> SimpleProb A -> Type
> NonEmpty sp = List.Operations.NonEmpty (support sp)

> |||
> All : {A : Type} -> (P : A -> Type) -> SimpleProb A -> Type
> All P sp = All P (support sp)

> ||| Tagging
> tagElem  :  {A : Type} -> (sp : SimpleProb A) -> SimpleProb (Sigma A (\ a => a `Elem` sp))
> tagElem sp = MkSimpleProb aps' s1p' where
>     ssp  : List A
>     ssp  = support sp
>     psp  : List NonNegRational
>     psp  = probs sp
>     as'  : List (Sigma A (\ a => a `Elem` sp))
>     as'  = List.Operations.tagElem ssp
>     aps' : List (Sigma A (\ a => a `Elem` sp), NonNegRational)
>     aps' = zip as' psp
>     s1p' : sumMapSnd aps' = 1
>     s1p' = trans s1 (trans s7 s8) where
>       s1 : sumMapSnd aps' = sum (snd (unzip aps'))
>       s1 = sumMapSndUnzipLemma aps'
>       s2 : length as' = length ssp
>       s2 = tagElemPreservesLength ssp
>       s3 : length ssp = length psp
>       s3 = lengthSupportProbsLemma sp
>       s4 : length as' = length psp
>       s4 = trans s2 s3
>       s5 : unzip (zip as' psp) = (as', psp)
>       s5 = unzipZipLemma as' psp s4
>       s6 : snd (unzip aps') = psp
>       s6 = cong {f = snd} s5
>       s7 : sum (snd (unzip aps')) = sum psp
>       s7 = cong {f = sum} s6
>       s8 : sum psp = 1
>       s8 = sumProbsLemma sp

> {-

> ---}


text:
module Utils.Misc

import Data.Bits
import Data.DPair
import Data.Fin
import Data.List
import Data.Nat
import Data.Nat.Division
import Data.Stream
import Data.Vect
import Data.List1
import Data.Fin.Extra
import Syntax.WithProof

||| primarily used for `hack_*` functions for hacking open ADTs into sums ^/v products
public export
Eithers : List Type -> Type
Eithers [] = Void
Eithers (x :: []) = x
Eithers (x :: xs) = Either x (Eithers xs)

public export
kill_linear : Void -> (1 _ : a) -> s
kill_linear x = void x

public export
pair_to_list : (a, a) -> List a
pair_to_list (x1, x2) = [x1, x2]

public export
vect_to_pair : Vect 2 a -> (a, a)
vect_to_pair [x1, x2] = (x1, x2)

public export
pair_to_vect : (a, a) -> Vect 2 a
pair_to_vect (x1, x2) = [x1, x2]

public export
from_vect : Vect 1 a -> a
from_vect [x] = x

public export
to_vect : a -> Vect 1 a
to_vect x = [x]

||| strict version of `(&&)`
public export
s_and : Bool -> Bool -> Bool
s_and True False = False
s_and True True = True
s_and False False = False
s_and False True = False

public export
mmod : Integer -> (m : Nat) -> {auto 0 ok : NonZero m} -> Nat
mmod n m =
  let m' = natToInteger m
  in integerToNat ((m' + n `mod` m') `mod` m')

public export
mod': Integer -> Integer -> Integer
mod' _ 0 = 0
mod' n m = (m + n `mod` m) `mod` m

public export
s_eq : (Bits b, Eq b) => Vect n b -> Vect n b -> Bool
s_eq a b = (zeroBits ==) $ foldr (.|.) zeroBits $ zipWith xor a b

public export
s_eq' : (Bits b, Eq b) => List b -> List b -> Bool
s_eq' a b = (length a == length b) `s_and` ((zeroBits ==) $ foldr (.|.) zeroBits $ zipWith xor a b)

public export
vect_zip_with : {n : Nat} -> {m : Nat} -> (a -> b -> c) -> Vect n a -> Vect m b -> Vect (minimum n m) c
vect_zip_with {n=0} {m} f [] _ = []
vect_zip_with {n} {m=0} f _ [] = rewrite minimumZeroZeroLeft n in []
vect_zip_with f (x::xs) (y::ys) = f x y :: vect_zip_with f xs ys

public export
group : (n : Nat) -> (m : Nat) -> Vect (n * m) a -> Vect n (Vect m a)
group Z     _ _  = []
group (S n) m xs = let (l, r) = splitAt m xs in l :: group n m r

public export
chunk : Nat -> List a -> List (List a)
chunk _ [] = []
chunk n xs = (take n xs) :: (chunk n (drop n xs))

-- https://gist.github.com/buzden/afc798fd2b01388f1626ae58c6ab8548
public export
group' : (n : Nat) -> (m : Nat) -> Vect (n * m) a -> Vect m (Vect n a)
group' n m xs = group m n $ rewrite multCommutative m n in xs

-- https://gist.github.com/buzden/afc798fd2b01388f1626ae58c6ab8548
-- to prove that, say given `xs : Vect (n + m) a`, can be splitted at index `n` into `l` and `r` (the (0 _ : splitAt n xs = (l, r)) part), and then be concatenated back into xs
export
split_at_concat_rev : (n : Nat) -> (xs : Vect (n + m) a) -> {0 l : Vect n a} -> {0 r : Vect m a} -> (0 _ : splitAt n xs = (l, r)) -> l ++ r = xs
split_at_concat_rev Z _ Refl = Refl
split_at_concat_rev (S n) (x :: xs) {l} prf with (splitAt n xs) proof sprf
  split_at_concat_rev (S n) (x :: xs) {l = x :: l} Refl | (l, _) = cong (x ::) $ split_at_concat_rev n xs sprf

-- https://gist.github.com/buzden/afc798fd2b01388f1626ae58c6ab8548
public export
concat_group_id : (n : Nat) -> (m : Nat) -> (v : Vect (n * m) a) -> concat (group n m v) = v
concat_group_id Z     _ [] = Refl
concat_group_id (S n) m xs with (splitAt m xs) proof prf
  _ | (l, r) = rewrite concat_group_id n m r in split_at_concat_rev m xs prf

pow_mod' : Integer -> Integer -> Integer -> Integer -> Integer
pow_mod' n x y m =
  if y == 0
     then n
     else let n' = (n * x) `mod` m
              y' = shiftR y 1
              x' = (x * x) `mod` m
          in pow_mod' (if testBit y 0 then n' else n) x' y' m

public export
pow_mod : Integer -> Integer -> Integer -> Integer
pow_mod x y m = pow_mod' 1 (x `mod'` m) (y `mod'` m) m

mul_mod' : Integer -> Integer -> Integer -> Integer -> Integer
mul_mod' n x y m =
  if y == 0
     then n
     else let n' = (n + x) `mod` m
              y' = shiftR y 1
              x' = (x * 2) `mod` m
          in mul_mod' (if testBit y 0 then n' else n) x' y' m

public export
mul_mod : Integer -> Integer -> Integer -> Integer
mul_mod x y m = mul_mod' 0 (x `mod'` m) (y `mod'` m) m

public export
quot_rem : Integer -> Integer -> (Integer, Integer)
quot_rem val d =
  let dividend = if d < 0 then -(val `div` abs d) else val `div` d
      remainder = abs (val - dividend * d)
  in (dividend, remainder)

public export
gcd' : Integer -> Integer -> Integer
gcd' a 0 = a
gcd' a b = gcd' b (a `mod` b)

public export
are_coprimes : Integer -> Integer -> Bool
are_coprimes x y = (gcd' x y) == 1

-- Extended Euclidean Algorithm
-- Only valid when gcd(a, b) = 1
public export
extended_gcd : Integer -> Integer -> (Integer, Integer)
extended_gcd a 0 = (1, 0)
extended_gcd a b =
  let (q, r) = quot_rem a b
      (s, t) = extended_gcd b r
  in (t, s - q * t)

-- Only valid when gcd(a, b) = 1
public export
inv_mul_mod : Integer -> Integer -> Integer
inv_mul_mod a m =
  let (x, y) = extended_gcd a m
  in mod' x m

public export
forM : Applicative f => (n : Nat) -> (f b) -> f (Vect n b)
forM n f = for (the (Vect n (Fin n)) range) (const f)

utf8_bytelen : Bits8 -> Maybe (Bits8, Nat)
utf8_bytelen x =
  if (x .&. 0b01111111) == x then Just (x, 0) -- ascii
    else if (shiftR x 5) == 0b110   then Just (x .&. 0b0011111, 1)
    else if (shiftR x 4) == 0b1110  then Just (x .&. 0b0001111, 2)
    else if (shiftR x 3) == 0b11110 then Just (x .&. 0b0000111, 3)
    else Nothing

utf8_unmask : Bits8 -> Maybe Bits8
utf8_unmask x = const (x .&. 0b00111111) <$> guard (shiftR x 6 == 0b10)

utf8_pushbits : Integer -> List Bits8 -> Integer
utf8_pushbits acc [] = acc
utf8_pushbits acc (x::xs) = utf8_pushbits ((shiftL acc 6) .|. (cast x)) xs

public export
utf8_decode : List Bits8 -> Maybe String
utf8_decode = go []
  where
    go : List Char -> List Bits8 -> Maybe String
    go acc [] = Just $ pack $ reverse acc
    go acc (x :: xs) = do
      (x, l) <- utf8_bytelen x
      let (y,ys) = splitAt l xs
      guard (length y == l)
      y <- traverse utf8_unmask y
      let c = utf8_pushbits (cast x) y
      go ((cast c) :: acc) ys

public export
stream_concat : Foldable t => Stream (t a) -> Stream a
stream_concat = go . map toList
  where
    go : Stream (List a) -> Stream a
    go ([] :: ys) = stream_concat ys
    go ((x :: xs) :: ys) = x :: stream_concat (xs :: ys)

public export
ok_minus : (n : Nat) -> (m : Nat) -> LTE m n -> Nat
ok_minus n Z LTEZero = n
ok_minus (S n) (S m) (LTESucc wit) = ok_minus n m wit

namespace List
  public export
  enumerate : Nat -> List a -> List (Nat, a)
  enumerate n [] = []
  enumerate n (x :: xs) = (n, x) :: enumerate (S n) xs

namespace Vect
  public export
  replace_vect : (0 _ : n = m) -> Vect n a -> Vect m a
  replace_vect prf input = rewrite sym prf in input

  public export
  cycle : Vect (S n) a -> Stream a
  cycle xs = go xs
    where
    go : Vect i a -> Stream a
    go [] = go xs
    go (z :: zs) = z :: go zs

  public export
  unsnoc : Vect (S n) a -> (Vect n a, a)
  unsnoc (x :: []) = ([], x)
  unsnoc (x :: (y :: ys)) = let (zs, z) = unsnoc (y :: ys) in (x :: zs, z)

namespace Stream
  public export
  prepend : List a -> Stream a -> Stream a
  prepend [] ys = ys
  prepend (x :: xs) ys = x :: prepend xs ys

  public export
  duplicate : Stream a -> Stream (Stream a)
  duplicate (x :: xs) = (x :: xs) :: duplicate xs

  public export
  split : (n : Nat) -> Stream a -> (Vect n a, Stream a)
  split Z xs = ([], xs)
  split (S n) (v :: xs) = let (vs, xs') = split n xs in (v :: vs, xs')

  public export
  chunk : (n : Nat) -> Stream a -> Stream (Vect n a)
  chunk n xs = let (y, ys) = split n xs in y :: chunk n ys

public export
lte_plus_left : (a : _) -> LTE (a + b) c -> LTE b c
lte_plus_left Z x = x
lte_plus_left (S k) x = lte_plus_left k (lteSuccLeft x)

public export
maybe_to_either : Maybe a -> Lazy b -> Either b a
maybe_to_either Nothing b = Left $ force b
maybe_to_either (Just a) _ = Right a

public export
init' : List a -> List a
init' [] = []
init' (x :: xs) = init (x :: xs)

public export
uncons1 : List1 a -> (List a, a)
uncons1 lst = (init lst, last lst)

public export
splitAt : (n : Nat) -> Stream a -> (Vect n a, Stream a)
splitAt n s = (take n s, drop n s)

public export
zeros : {n : Nat} -> Vect n Bits8
zeros = map (const 0) Fin.range

public export
splitLastAt1 : (n : Nat) -> List a -> Maybe (List1 a, Vect n a)
splitLastAt1 n v = do
  let m = minus (length v) n
  let (a, b) = splitAt m v
  a' <- fromList a
  b' <- exactLength n $ fromList b
  pure (a', b')

public export
modFinNZ : Nat -> (b : Nat) -> NonZero b -> Fin b
modFinNZ a b prf = let x = boundModNatNZ a b prf in natToFinLTE (modNatNZ a b prf) x

public export
collapse_ordering : List Ordering -> Ordering
collapse_ordering (LT :: xs) = LT
collapse_ordering (GT :: xs) = GT
collapse_ordering (EQ :: xs) = collapse_ordering xs
collapse_ordering [] = EQ

public export
pad_zero : Nat -> List Bits8 -> List Bits8
pad_zero Z a = a
pad_zero (S n) a =
  let l = length a
      l = minus ((S n) * (divCeilNZ l (S n) SIsNonZero)) l
  in a <+> replicate l 0

public export
splitAtExact : (n : Nat) -> List a -> Maybe (Vect n a, List a)
splitAtExact n list =
  let (a, b) = splitAt n list
  in (, b) <$> exactLength n (fromList a)


text:
data Vect : Nat -> Type -> Type where
    Nil  : Vect Z a
    (::) : a -> Vect k a -> Vect (S k) a

%name Vect xs, ys, zs

zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c


text:
main : IO ()
-- main = putStrLn "Hello World"
main = getLine >>= putStrLn

max_stars_repo_name: ioanluca/real-world-idris

max_issues_repo_name: ioanluca/real-world-idris

max_forks_repo_name: ioanluca/real-world-idris


text:
module PowerSource

data PowerSource = Petrol | Pedal

data Vehicle : PowerSource -> Type where
     Bicycle : Vehicle Pedal
     Unicycle : Vehicle Pedal
     Car : (fuel : Nat) -> Vehicle Petrol
     Motorbike : (fuel : Nat) -> Vehicle Petrol
     Bus : (fuel : Nat) -> Vehicle Petrol

wheels : Vehicle power -> Nat
wheels Bicycle = 2
wheels Unicycle = 1
wheels (Car fuel) = 4
wheels (Bus fuel) = 4
wheels (Motorbike fuel) = 2

refuel : Vehicle Petrol -> Vehicle Petrol
refuel (Car fuel) = Car 100
refuel (Bus fuel) = Bus 200
refuel (Motorbike fuel) = Motorbike 20
-- If we add impossible to the above case, Idris will report that it is a valid case
refuel Bicycle impossible

max_stars_repo_name: balajisivaraman/idris-book

max_issues_repo_name: balajisivaraman/idris-book

max_forks_repo_name: balajisivaraman/idris-book


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

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
||| Logic for manipulating combat odds
module Bautzen.Odds

import Prelude.Bound
import Prelude.Enum

import Data.Fin
import Data.Nat.DivMod

||| The raw odds in a combat, basically a glorified pair.
public export
record RawOdds where
  constructor MkRawOdds

  ||| Raw attack factor
  attackFactor : Nat

  ||| Raw defense factor
  ||| TODO make it a positive so that we prevent stupid odds from
  ||| happening
  defenseFactor : Nat

public export
Semigroup RawOdds where
  (<+>) (MkRawOdds atk def) (MkRawOdds atk' def') = MkRawOdds (atk + atk') (def + def')

||| The actual odds representing a column in the combat table
public export
data Odds : Type where
  OneVsTwo : Odds
  OneVsOne : Odds
  TwoVsOne : Odds
  ThreeVsOne : Odds
  FourVsOne : Odds
  FiveVsOne : Odds
  SixVsOne : Odds
  SevenVsOne : Odds

public export
Eq Odds where
  OneVsTwo == OneVsTwo = True
  OneVsOne == OneVsOne = True
  TwoVsOne == TwoVsOne = True
  ThreeVsOne == ThreeVsOne = True
  FourVsOne == FourVsOne = True
  FiveVsOne == FiveVsOne = True
  SixVsOne == SixVsOne = True
  SevenVsOne == SevenVsOne = True
  _ == _ = False

public export
Enum Odds where
  pred OneVsTwo = OneVsTwo
  pred OneVsOne = OneVsTwo
  pred TwoVsOne = OneVsOne
  pred ThreeVsOne = TwoVsOne
  pred FourVsOne = ThreeVsOne
  pred FiveVsOne = FourVsOne
  pred SixVsOne = FiveVsOne
  pred SevenVsOne = SixVsOne

  succ OneVsTwo = OneVsOne
  succ OneVsOne = TwoVsOne
  succ TwoVsOne = ThreeVsOne
  succ ThreeVsOne = FourVsOne
  succ FourVsOne = FiveVsOne
  succ FiveVsOne = SixVsOne
  succ SixVsOne = SevenVsOne
  succ SevenVsOne = SevenVsOne

  toNat OneVsTwo = 0
  toNat OneVsOne = 1
  toNat TwoVsOne = 2
  toNat ThreeVsOne = 3
  toNat FourVsOne = 4
  toNat FiveVsOne = 5
  toNat SixVsOne = 6
  toNat SevenVsOne = 7

  fromNat Z = OneVsTwo
  fromNat (S k) = succ (fromNat k)

public export
Ord Odds where
  compare x y = compare (toNat x) (toNat y)

public export
MinBound Odds where
  minBound = OneVsTwo

public export
MaxBound Odds where
  maxBound = SevenVsOne

public export
toFin : Odds -> Fin 8
toFin OneVsTwo = 0
toFin OneVsOne = 1
toFin TwoVsOne = 2
toFin ThreeVsOne = 3
toFin FourVsOne = 4
toFin FiveVsOne = 5
toFin SixVsOne = 6
toFin SevenVsOne = 7

||| Transform a concrete attack/defense ratio into `Odds`
|||
||| The quotient is rounded to the lowest integer to produce `Odds`. By convention
||| if the `defenseFactor` is 0 the ratio is the greatest possible. This situation
||| should not happen
|||
||| @odds raw odds to transform into a column
public export
odds : (odds: RawOdds) -> Odds
odds (MkRawOdds attackFactor Z) = maxBound -- by convention, should not happen
odds (MkRawOdds attackFactor (S def)) with (attackFactor `divMod` def)
  odds (MkRawOdds (r + (q * (S def))) (S def)) | (MkDivMod q r _) = fromNat q

infixl 6 >>>
infixl 6 <<<

||| Shift odds by a given number of steps "up".
|||
||| @odds original odds
||| @steps number of steps to shift odds
public export
(>>>) : (odds : Odds) -> (steps : Nat) -> Odds
c >>> Z = c
c >>> (S k) = foldl (const . succ) c [0.. k]

||| Shift odds by a given number of steps "down".
|||
||| @odds original odds
||| @steps number of steps to shift odds
public export
(<<<) : (odds : Odds) -> (steps : Nat) -> Odds
c <<< Z = c
c <<< (S k) = foldl (const . pred) c [0.. k]

namespace OddsTest

  odds_are_rounded_down : odds (MkRawOdds 3 2) = OneVsOne
  odds_are_rounded_down = Refl

  odds_are_capped : odds (MkRawOdds 20 2) = SevenVsOne
  odds_are_capped = Refl

  odds_are_floored : odds (MkRawOdds 2 20) = OneVsTwo
  odds_are_floored = Refl

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
import Data.Either
import Data.List
import Data.Maybe
import Data.String
import Data.Binary
import Data.Binary.Digit

import System.File

significant: List Nat -> String -> List Nat
significant l s = (\(i,c) => if c == '1' then i + 1 else i)
                  <$> zip l (unpack s)

gamma : Nat -> List Nat -> Nat
gamma s l = toNat $ reverse $ (\i => if i + i > s then I else O) <$> l
epsilon : Nat -> List Nat -> Nat
epsilon s l = toNat $ reverse $ (\i => if i + i > s then O else I) <$> l

run : String -> IO ()
run s = do let lines = lines $ trim $ s
           let s = foldl significant (replicate 12 0) $ lines
           let gamma = gamma (length lines) s
           let epsilon = epsilon (length lines) s
           putStrLn $ show $ gamma * epsilon

main : IO ()
main = do Right s <- readFile "input.txt"
            | Left err => putStrLn $ show err
          run s


text:
identityInt : Int -> Int
identityInt x = x

identityString : String -> String
identityString x = x

identityBool : Bool -> Bool
identityBool x = x

identity : ty -> ty
identity x = x

doubleNat : Nat -> Nat
doubleNat x = x + x

doubleInteger : Integer -> Integer
doubleInteger x = x + x

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


text:
module PLFI.Part1.Naturals

-- https://plfa.gihub.io/Naturals

data Vect : Nat -> (t : Type) -> Type where
  Nil  : Vect 0 t
  (::) : (x : t) -> Vect n t -> Vect (1 + n) t

replicate : Nat -> t -> List t

replicateV : (n : Nat) -> t -> Vect n t
replicateV 0 x = []
replicateV (S k) x = x :: replicateV k x

%hide (+)
%hide (*)

-- %default total

-- data N0 = Zero | Suc N0

{-
----------- Zero
  Zero : N

   m : N
----------- Suc
 Suc m : N
-}

public export
data N : Type where

  -- Base case
  Zero :
    --------
       N

  -- Inductive case
  Suc :
    (m : N) ->
    ----------
         N

export
Num N where
  (*) = ?m1
  (+) = ?a1
  fromInteger n with (compare n 0)
     fromInteger n | LT = Zero
     fromInteger n | EQ = Zero
     fromInteger n | GT = Suc (assert_total (fromInteger (n-1)))

ex1 : N
ex1 = Suc (Suc (Suc (Suc (Suc (Suc (Suc Zero))))))

test : N
test = (-7)

total
public export
(+) : N -> N -> N
Zero    + m = m
(Suc n) + m = Suc (n + m)

export
addEquation1 : {n : N} -> (Zero + n) = n -- Refl : Equal x x
addEquation1 = Refl

export
addEquation2 : (Suc m) + n = Suc (m + n)
addEquation2 = Refl

total
public export
(*) : N -> N -> N
Zero    * n = Zero
(Suc m) * n = n + (m * n)

-- N -> Zero * ? = Zero
multEquation0 : {n : N} -> Zero * n = Zero
-- test :: Maybe (Maybe Int)
-- test : Maybe $ Maybe Int
-- test : (n : Nat) -> let m = n + n in Vect m Int

export
multEquation1 : Zero * n = Zero
multEquation1 = Refl

export
multEquation2 : (Suc m) * n = n + (m * n)
multEquation2 = Refl

infixr 8 ^

-- Exercise: recommended

total
export
(^) : N -> N -> N
m ^ Zero    = Suc Zero
m ^ (Suc n) = m * (m ^ n)

-- m ^ 0        =  1
-- m ^ (1 + n)  =  m * (m ^ n)

export
expEquation1 : m ^ Zero = Suc Zero
expEquation1 = Refl

export
expEquation2 : m ^ (Suc n) = m * (m ^ n)
expEquation2 = Refl

-- monus

infixl 6 -*

total
export
(-*) : N -> N -> N
m       -* Zero     = m
Zero    -* (Suc n)  = Zero
(Suc m) -* (Suc n)  = m -* n

-- Exercise: strech

public export
data Bin : Type where
  E : Bin
  O : Bin -> Bin
  I : Bin -> Bin

-- 1101 is encoded as
-- IOIIE this needs to be read reversed:
-- EIIOI

export
inc : Bin -> Bin

export
to : N -> Bin

export
from : Bin -> N

max_stars_repo_name: andorp/PLFI

max_issues_repo_name: andorp/PLFI

max_forks_repo_name: andorp/PLFI


text:
module Functor

-- Functor typeclasee from memory
interface MyFunctor (s : Type -> Type) where
          fmap : s (a -> b) -> s a -> s b


text:
infix 3 #

data T : Type where
  (#) : T -> T -> T
  leaf : T


text:
%default total

data InfIO : Type where
     Do : IO a -> (a -> Inf InfIO) -> InfIO
     Seq : IO () -> Inf InfIO -> InfIO

(>>=) : IO a -> (a -> Inf InfIO) -> InfIO
(>>=) = Do

(>>) : IO () -> Inf InfIO -> InfIO
(>>) = Seq

loopPrint : String -> InfIO
loopPrint msg = do putStrLn msg
                   loopPrint msg

data Fuel = Dry | More (Lazy Fuel)

tank : Nat -> Fuel
tank Z = Dry
tank (S k) = More (tank k)

partial
runPartial : InfIO -> IO ()
runPartial (Do action f) = do res <- action
                              runPartial (f res)

run : Fuel -> InfIO -> IO ()
run (More fuel) (Do c f) = do res <- c
                              run fuel (f res)
run (More fuel) (Seq io k) = do io; run fuel k
run Dry p = putStrLn "Out of fuel"

partial
forever : Fuel
forever = More forever

partial
main : IO ()
main = run (tank 10) (loopPrint "vroom")


text:
module C

import B

public export
bar : {default defaultRec rec : Rec} -> Char
bar {rec} = field rec


text:
module SnocList

-- data SnocList ty = Empty | Snoc (SnocList ty) ty

data SnocList : List a -> Type where
     Empty : SnocList []
     Snoc : (rec : SnocList xs) -> SnocList (xs ++ [x])

snocListHelp : (snoc : SnocList input) -> (rest : List a) -> SnocList (input ++ rest)
snocListHelp {input} snoc [] = rewrite appendNilRightNeutral input in snoc
snocListHelp {input} snoc (x :: xs) = rewrite appendAssociative input [x] xs in
                                              snocListHelp (Snoc snoc {x}) xs

snocList : (xs : List a) -> SnocList xs
snocList xs = snocListHelp Empty xs

-- myReverseHelper : (input : List a) -> SnocList input -> List a
-- myReverseHelper [] Empty = []
-- myReverseHelper (xs ++ [x]) (Snoc rec) = x :: myReverseHelper xs rec

-- myReverse : List a -> List a
-- myReverse xs = myReverseHelper xs $ snocList xs

-- Alternate attempt to write a variation of myReverse that is also total before I was introduced to fun | sugaring.
-- myReverse : List a -> List a
-- myReverse xs = myRev xs $ snocList xs
--   where
--   myRev : (xs : List a) -> SnocList xs -> List a
--   myRev xs slxs with (slxs)
--     myRev [] slxs | Empty = []
--     myRev (ys ++ [x]) slxs | (Snoc rec) = x :: myRev ys rec

myReverse : List a -> List a
myReverse xs with (snocList xs)
  myReverse [] | Empty = []
  myReverse (ys ++ [x]) | (Snoc rec) = x :: myReverse ys | rec

isSuffix : Eq a => List a -> List a -> Bool
isSuffix xs ys with (snocList xs)
  isSuffix [] ys | Empty = True
  isSuffix (zs ++ [z]) ys | (Snoc zsrec) with (snocList ys)
    isSuffix (zs ++ [z]) [] | (Snoc zsrec) | Empty = False
    isSuffix (zs ++ [z]) (ys ++ [y]) | (Snoc zsrec) | (Snoc ysrec) = case z == y of
                                                                          False => False
                                                                          True => isSuffix zs ys | zsrec | ysrec


text:
module Part1.Sec2_2_2_the

||| reimplemented "the" function from Prelude
the' : (ty : Type) -> ty -> ty
the' ty x = x

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
-- ----------------------------------------------------------- [ DataTypes.idr ]
-- Module      : Chapter.DataTypes
-- Description : Definitions from Chapter 4 of Edwin Brady's book,
--               "Type-Driven Development with Idris."
-- --------------------------------------------------------------------- [ EOH ]
module Chapter.DataTypes

%access export

-- ------------------------------------------------------- [ 4.1.2 Union Types ]

public export
data Shape = Triangle Double Double
           | Rectangle Double Double
           | Circle Double

%name Shape shape, shape1, shape2

namespace Shape

  ||| Calculate the area of a shape.
  area : Shape -> Double
  area (Triangle base  height)  = 0.5 * base * height
  area (Rectangle width height) = width * height
  area (Circle radius)          = pi * radius * radius

-- --------------------------------------------------- [ 4.1.3 Recursive Types ]

public export
data Picture = ||| A primitive shape.
               Primitive Shape
             | ||| A combination of two other pictures.
               Combine Picture Picture
             | ||| A picture rotated through an angle.
             Rotate Double Picture
             | ||| A picture translated to a different location.
             Translate Double Double Picture

%name Picture pic, pic1, pic2

namespace Picture

  area : Picture -> Double
  area (Primitive shape)   = area shape
  area (Combine pic pic1)  = area pic + area pic1
  area (Rotate _ pic)      = area pic
  area (Translate _ _ pic) = area pic

-- ------------------------------------------------ [ 4.1.4 Generic Data Types ]

||| A binary search tree.
public export
data Tree elem = ||| A tree with no data.
                 Empty
               | ||| A node with a left subtree, a value, and a right subtree.
                 Node (Tree elem) elem (Tree elem)

%name Tree tree, tree1

||| Insert a value into a binary search tree.
||| @ x a value to insert
||| @ tree a binary search tree to insert into
insert : Ord elem => (x : elem) -> (tree : Tree elem) -> Tree elem
insert x Empty = Node Empty x Empty
insert x orig@(Node left val right)
       = case compare x val of
              LT => Node (insert x left) val right
              EQ => orig
              GT => Node left val (insert x right)

-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
module Time

import Coda.Range

%access public export
%default total

{-
  ISO 8601 Time Package

  Time Representation includes:

    Hour : Minute : Second (+/-) Offset

  Where (+/-) Offset is represented as a TimeZone

  And Hour : Minute : Second is represented as an Instant

  And the combination of both is represented as a LocalTime

-}

{-
  Type Definitions
-}

data Second : Type where
  MkSec : (s : Nat) -> { auto prf : (Dec (0 <= s = s < 60) ) } -> Second

%name Second s,s1,s2,s3

data Minute : Type where
  MkMin : (m : Nat) -> { auto prf : (Dec (0 <= m = m < 60) ) } -> Minute

%name Minute m,m1,m2,m3

data Hour : Type where
  MkHour : (h : Nat) -> { auto prf : (Dec (0 <= h = h < 24) ) } -> Hour

%name Hour h,m1,m2,m3

data Instant : Type where
  MkInstant : (h : Hour) -> (m : Minute) -> (s : Second) -> Instant

%name Instant i,i1,i2,i3

data Sign : Type where
  (+) : Sign
  (-) : Sign

%name Sign s,s1,s2,s3

data Offset : Type where
  MkOffset : (sign : Sign) -> (i : Instant) -> Offset

%name Offset off,off1,off2,off3

data TimeZone : Offset -> Type where
  MkTimeZone : (name : String) -> (offset : Offset) -> TimeZone offset

%name TimeZone tz,tz1,tz2,tz3

data LocalTime : TimeZone offset -> Type where
  MkLocalTime : (tz : TimeZone offset) -> (i : Instant) -> LocalTime tz

%name LocalTime lt,lt1,lt2,lt3

{-
  Standard Interface Implementations
-}

Eq Second where
  (==) (MkSec s) (MkSec s') = s == s'

Ord Second where
  compare (MkSec s) (MkSec s') = compare s s'

Show Second where
  show (MkSec s) = if s < 10 then "0"++show s else show s

Eq Minute where
  (==) (MkMin s) (MkMin s') = s == s'

Ord Minute where
  compare (MkMin s) (MkMin s') = compare s s'

Show Minute where
  show (MkMin m) = if m < 10 then "0"++show m else show m

Eq Hour where
  (==) (MkHour s) (MkHour s') = s == s'

Ord Hour where
  compare (MkHour s) (MkHour s') = compare s s'

Show Hour where
  show (MkHour h) = if h < 10 then "0"++show h else show h

Eq Instant where
  (==) (MkInstant h m s) (MkInstant h' m' s') = h == h' && m == m' && s == s'

Ord Instant where
  compare (MkInstant h m s) (MkInstant h' m' s') =
    case compare h h' of
         EQ => case compare m m' of
                    EQ => compare s s'
                    r => r
         r => r

Show Instant where
  show (MkInstant h m s) = "" ++ show h ++ ":" ++ show m ++ ":" ++ show s

Eq Sign where
  (==) (+) (+) = True
  (==) (-) (-) = True
  (==) _ _ = False

Ord Sign where
  compare (+) (-) = GT
  compare (-) (+) = LT
  compare (+) (+) = EQ
  compare (-) (-) = EQ

Show Sign where
  show (+) = "+"
  show (-) = "-"

Eq Offset where
  (==) (MkOffset sign i) (MkOffset sign' i') = sign == sign' && i == i'

Ord Offset where
  compare (MkOffset sign i) (MkOffset sign' i') =
    case compare sign sign' of
         EQ => compare i i'
         r => r

Show Offset where
  show (MkOffset sign i@(MkInstant h m _)) =
    if isZero i
       then "Z"
       else show sign ++ show h ++ ":" ++ show m
    where isZero : Instant -> Bool
          isZero (MkInstant (MkHour Z) (MkMin Z) (MkSec Z)) = True
          isZero _ = False

Eq (TimeZone offset) where
  (==) (MkTimeZone name _) (MkTimeZone name' _) = name == name'

Ord (TimeZone offset) where
  compare (MkTimeZone name _) (MkTimeZone name' _) = compare name name'

Show (TimeZone offset) where
  show (MkTimeZone name offset) = show name ++ show offset

Eq (LocalTime tz) where
  (==) (MkLocalTime _ i) (MkLocalTime _ i') = i == i'

Ord (LocalTime tz) where
  compare (MkLocalTime _ i) (MkLocalTime _ i') = compare i i'

Show (LocalTime (MkTimeZone name offset)) where
  show (MkLocalTime (MkTimeZone name offset) i) = show i ++ show offset

{-
  Utility Functions
-}

minuteToSeconds : Minute -> Integer
minuteToSeconds (MkMin m) = (toIntegerNat m) * 60

hourToSeconds : Hour -> Integer
hourToSeconds (MkHour h) = (toIntegerNat h) * 60 * 60

instantToSeconds : Instant -> Integer
instantToSeconds (MkInstant h m (MkSec s)) = (hourToSeconds h) +
                                             (minuteToSeconds m) +
                                             (toIntegerNat s)

Distance Instant Integer where
  distance (MkRange x y) = (instantToSeconds y) - (instantToSeconds x)

instantZero : Instant
instantZero = (MkInstant (MkHour 0) (MkMin 0) (MkSec 0))

UTC : TimeZone (MkOffset (+) Time.instantZero)
UTC = MkTimeZone "UTC" (MkOffset (+) instantZero)

max_stars_repo_name: ostera/idris-coda

max_issues_repo_name: ostera/idris-coda

max_forks_repo_name: ostera/idris-coda


text:
||| Simple GADTs for F#
module TypeTheory

%default total
%access public export

||| A term in the language
||| universe 0 - values
||| universe 1 - types
||| universe 2 - kinds
||| universe 2 - sorts
data Term : (universe : Nat) -> Type where
  ||| A named term or variable
  Var : String -> Term u
  ||| An explicit type annotation
  Ann : Term u -> Term (S u) -> Term u
  ||| Function application
  Appl : Term u -> Term u -> Term u
  ||| Type constructor operator. Its terms cannot be values.
  Arrow : Term (S u) -> Term (S u) -> Term (S u)
  ||| The name of Type in any universe starting with 2 (since the lowest Type
  ||| has as its type Kind).
  Tau : Term (S (S n))

||| A primitive type or type constructor in universe one, opaque to the
||| source language because taken for granted as existing in the target
||| language. Syntax:
|||   primitive string : Type
|||   primitive Maybe : Type -> Type
|||   primitive Either : Type -> Type -> Type
||| The term in universe two is the type of the primitive: all primitives
||| have a type of Type or of some type constructor, which are kinds, so it
||| is in universe two.
primType : String -> Term 2 -> Term 1
primType name type = Ann (Var name) type

||| With full dependent types, equality is a problem that needs gamma, and
||| requires evaluation. We do not yet need this.
equal : Term u -> Term u -> Bool
equal (Var a) (Var c) = a == c
equal (Ann a b) (Ann c d) = equal a c && equal b d
equal (Appl a b) (Appl c d) = equal a c && equal b d
equal (Arrow a b) (Arrow c d) = equal a c && equal b d
equal Tau Tau = True
equal _ _ = False

equal' : Term u -> Term v -> Bool
equal' {u} {v} x y =
  case decEq u v of
    Yes prf => equal x (rewrite prf in y)
    No _ => False

||| Typing environment, where its universe is one larger than the universe of
||| the biggest terms for which it contains typing information: or said another
||| way, perhaps more lucidly, the universe off the typing environment is equal
||| to the universe of the types of the biggest terms it contains.
data Gamma : (universe : Nat) -> Type where
  ||| To ensure that the typing information is always cumulative from its
  ||| biggest universe all the way down to values, we must ground the empty
  ||| universe as size zero. This also makes sense with the definition of its
  ||| universe being one larger than the universe of its biggest terms: there is
  ||| no universe below Z and therefore if Z is one larger than the biggest
  ||| terms in Nil there are no terms in Nil.
  Nil : Gamma Z
    -- List (u : Nat ** List (Term u, Term (S u)))
  (::) : List (Term u, Term (S u)) -> Gamma u -> Gamma (S u)

typeInEnv : Gamma v -> Term u -> Maybe (Term (S u))
-- The empty type environment contains no judgements, by definition.
typeInEnv {v=Z} {u=_} [] _ = Nothing
-- u is at least as big as v if not bigger in this case. That means the typing
-- environment is insufficiently large to contain information on this term.
typeInEnv {v=S Z} {u = (S _)} (_ :: _) _ = Nothing
typeInEnv {v=S j} {u = k} (x :: xs) t =
  case decEq k j of
    Yes prf => lookupBy equal t (rewrite prf in x)
    No _ => typeInEnv xs t

checkTypeInEnv : Gamma v -> Term u -> Term (S u) -> Bool
checkTypeInEnv gamma x t =
  let maybeT = typeInEnv gamma x
  in case maybeT of
    Just t' => equal t t'
    Nothing => False

mutual
  check : Gamma v -> Term u -> Term (S u) -> Bool
  check gamma x@(Var _) t = checkTypeInEnv gamma x t
  check _ (Ann _ t) t' = equal t t'
  check gamma (Appl f a) t =
    case synthesize gamma f of
      Just (Arrow at bt) => check gamma a at && equal t bt
      -- The first term in an application must be a function, i.e. must have an
      -- arrow type, else it is bogus and we can't synthesize a type for that
      _ => False
  check _ (Arrow _ _) Tau = True
  check _ (Arrow _ _) _ = False
  check _ Tau Tau = True
  check _ Tau _ = False

  synthesize : Gamma v -> Term u -> Maybe (Term (S u))
  synthesize gamma x@(Var _) = typeInEnv gamma x
  synthesize _ (Ann _ t) = Just t
  synthesize gamma (Appl f a) =
    case synthesize gamma f of
      Just (Arrow at bt) => if check gamma a at then Just bt else Nothing
      -- The first term in an application must be a function, i.e. must have an
      -- arrow type, else it is bogus and we can't synthesize a type for that
      _ => Nothing
  synthesize _ (Arrow _ _) = Just Tau
  synthesize _ Tau = Just Tau

max_stars_repo_name: Kazark/fspp

max_issues_repo_name: Kazark/fspp

max_forks_repo_name: Kazark/fspp


text:
import Data.Vect

-- using implicit arguments in pattern matching
length : Vect n elem -> Nat
length {n} xs = n

-- give explicit values for implicit arguments by
-- using the notation {n = value}
create_empties : Vect n (Vect 0 a)
create_empties {n = Z} = []
create_empties {n = (S k)} = [] :: create_empties


text:
module Twist.Cycle

import Control.Algebra
import Data.Fin
import Data.Vect

%default total
%access export

data Cycle : (n : Nat) -> Type where
  By : Fin (S k) -> Cycle (S k)

Uninhabited (Cycle Z) where
  uninhabited (By SZ) impossible

Eq (Cycle n) where
  (By x) == (By y) = x == y

DecEq (Cycle n) where
  decEq (By x) (By y) with (decEq x y)
    | Yes p = Yes $ cong p
    | No p  = let result = No p in ?helpCycle

showCycle_debug : {n : Nat} -> Cycle n -> String
showCycle_debug {n=Z} _ impossible
showCycle_debug {n=n@(S k)} (By x) = show (finToNat x) ++ "/" ++ show n

showCycle_4 : Cycle 4 -> String
showCycle_4 (By x) = index x ["0", "", "2", "'"]

showCycle : {n : Nat} -> Cycle n -> String
showCycle {n=Z} _                 impossible
showCycle {n=(S (S (S (S Z))))} c = showCycle_4 c
showCycle {n=_}                 c = showCycle_debug c

Show (Cycle n) where
  show = showCycle

||| Convert from (Cycle n) to (Cycle (S n)), without incrementing its value.
||| The resulting cycle will have the same degree as the original.
promote : Cycle (S n) -> Cycle (S (S n))
promote {n} (By x) = By (weaken x)

-- fullPromote : {n, m : Nat} -> {auto p : LTE n m} -> Cycle (S n) -> Cycle (S m)
-- fullPromote {n} {m=(S k)} {p} c = promote (fullPromote {n} {m=k} c)

||| Convert from (Cycle n) to (Cycle (S n)) by incrementing the value.
promote' : Cycle (S n) -> Cycle (S (S n))
promote' {n} (By x) = By (FS x)

||| Convert fom (Cycle (S n)) to (Cycle n), without decrementing its value.
||| The resulting cycle will have the same degree as the original (mod n).
demote : {n : Nat} -> Cycle (S (S n)) -> Cycle (S n)
demote {n} (By x) = By (either (const FZ) id (strengthen x))

||| Convert from (Cycle (S n)) to (Cycle n) by decrementing the underlying value.
demote' : {n : Nat} -> Cycle (S (S n)) -> Cycle (S n)
demote' {n} (By FZ)     = By last
demote' {n} (By (FS x)) = By x

next : Cycle (S n) -> Cycle (S n)
next {n=Z}     _ = By FZ
next {n=(S _)} c = demote (promote' c)

nextN : Nat -> Cycle (S n) -> Cycle (S n)
nextN Z c = c
nextN (S j) c = nextN j (next c)

prev : Cycle (S n) -> Cycle (S n)
prev {n=Z}     _ = By FZ
prev {n=(S _)} c = promote (demote' c)

invertCycle : {n : Nat} -> Cycle (S n) -> Cycle (S n)
invertCycle {n=_}     (By FZ)       = (By FZ)
invertCycle {n=(S k)} (By (FS FZ))  = By last
invertCycle {n=(S k)} (By (FS x))   = promote (invertCycle (By x))

||| Construct a (Cycle n) with degree 0.
cycleZ : (n : Nat) -> {auto n_GTE_1 : GTE n (S Z)} -> Cycle n
cycleZ (S k) {n_GTE_1} = By FZ

||| Construct a (Cycle n) with degree 1.
cycle : (n : Nat) -> {auto n_GTE_2 : GTE n (S (S Z))} -> Cycle n
cycle n@(S _) {n_GTE_2} = next (cycleZ n)

||| Construct a (Cycle n) with degree' 1.
cycle' : (n : Nat) -> {auto n_GTE_2 : GTE n (S (S Z))} -> Cycle n
cycle' n@(S _) {n_GTE_2} = invertCycle (cycle n)

||| Construct a (Cycle n) with degree x.
cycleN : (n : Nat) -> {auto n_GT_0 : GT n Z} -> (x : Nat) -> {auto x_LT_n : LT x n} -> Cycle n
cycleN (S k) {n_GT_0} x {x_LT_n} = nextN x (cycleZ (S k))

cyclePlus : {n : Nat} -> Cycle (S n) -> Cycle (S n) -> Cycle (S n)
cyclePlus {n=_}     (By FZ)     y = y
cyclePlus {n=(S j)} (By (FS p)) y = promote' (cyclePlus (By p) (demote y))

Semigroup (Cycle (S n)) where
  (<+>) = cyclePlus

Monoid (Cycle (S n)) where
  neutral = By FZ

Group (Cycle (S n)) where
  inverse = invertCycle

degree : Cycle (S n) -> Nat
degree (By x) = toNat x

degree' : Cycle (S n) -> Nat
degree' c = degree (inverse c)

max_stars_repo_name: msmorgan/idris-twist

max_issues_repo_name: msmorgan/idris-twist

max_forks_repo_name: msmorgan/idris-twist


text:
-- --------------------------------------------------------------- [ Utils.idr ]
--
-- Utilities
--
-- --------------------------------------------------------------------- [ EOH ]
module RFC.Utils

import System

%access public

||| Representation of String literals that are to be sent.
Literal : String -> Type
Literal str = (str' : String ** str' = str)

-- ----------------------------------------------------------------- [ DayTime ]
||| Simple Record for DayTime
record DayTime : Type where
  MkDaytime : (y : Int)
            -> (m : Int)
            -> (d : Int)
            -> (hh : Int)
            -> (mm : Int)
            -> (ss : Int)
            -> DayTime

instance Show DayTime where
    show date = unwords [show (y  date), "-",
                         show (m  date), "-",
                         show (d  date), " ",
                         show (hh date), ":",
                         show (mm date), ":",
                         show (ss date) ]

-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-protocol-examples

max_issues_repo_name: jfdm/idris-protocol-examples

max_forks_repo_name: jfdm/idris-protocol-examples


text:
module Decidable.Decidable.Extra

import Data.Rel
import Data.Fun
import Data.Vect
import Data.HVect
import Data.Fun.Extra
import Decidable.Decidable

public export
NotNot : {n : Nat} -> {ts : Vect n Type} -> (r : Rel ts) -> Rel ts
NotNot r = map @{Nary} (Not . Not) r

[DecidablePartialApplication] {x : t} -> (tts : Decidable (t :: ts) r) => Decidable ts (r x) where
  decide = decide @{tts} x

public export
doubleNegationElimination : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable ts r =>
  (witness : HVect ts) ->
  uncurry (NotNot {ts} r) witness ->
  uncurry              r  witness
doubleNegationElimination {ts = []     } @{dec} [] prfnn =
  case decide @{dec} of
    Yes prf   => prf
    No  prfn => absurd $ prfnn prfn
doubleNegationElimination {ts = t :: ts} @{dec} (w :: witness) prfnn =
  doubleNegationElimination {ts} {r = r w} @{ DecidablePartialApplication @{dec} } witness prfnn

doubleNegationForall : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable ts r =>
  All ts (NotNot {ts} r) -> All ts r
doubleNegationForall @{dec} forall_prf =
  let prfnn : (witness : HVect ts) -> uncurry (NotNot {ts} r) witness
      prfnn = uncurryAll forall_prf
      prf   : (witness : HVect ts) -> uncurry              r  witness
      prf witness = doubleNegationElimination @{dec} witness (prfnn witness)
  in curryAll prf

public export
doubleNegationExists : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable ts r =>
  Ex ts (NotNot {ts} r) ->
  Ex ts r
doubleNegationExists {ts} {r} @{dec} nnxs =
  let witness : HVect ts
      witness = extractWitness nnxs
      witnessingnn : uncurry (NotNot {ts} r) witness
      witnessingnn = extractWitnessCorrect nnxs
      witnessing   : uncurry              r  witness
      witnessing   = doubleNegationElimination @{dec} witness witnessingnn
  in introduceWitness witness witnessing


text:
module Equis.Matrix.Arithmetic

import Matrix
import Data.Matrix.Numeric

%access private

||| Hadamard multiplication (element-wise product) of two matrices.
|||
||| @x the first matrix
||| @y the second matrix
export
hadamard : Num a => (x, y : Matrix n m a) -> Matrix n m a
hadamard x y = mapMatrix (\(i, j) => i * j) (zipMatrix x y)

||| Calculates a Gramian matrix.
|||
||| @x the matrix
export
gram : Num a => (x : Matrix n m a) -> Matrix m m a
gram x = (transpose x) <> x

||| Calculates the determinant of a square matrix (including order 1 and 0 matrices).
|||
||| @x the matrix
export
determinant : Neg a => (x : Matrix n n a) -> a
determinant {n = Z} _ = 1
determinant {n = (S Z)} x = scalar x
determinant {n = (S (S _))} x = det x

||| Calculates the matrix of minors for the given square matrix.
|||
||| @x the matrix
export
minors : Neg a => (x : Matrix n n a) -> Matrix n n a
minors {n = Z} _ = []
minors {n = (S _)} x = mapMatrix determinant (minors' x) where
  ||| Generates a matrix of m - 1 × n - 1 submatrices within the given matrix.
  |||
  ||| @x the matrix
  minors' : (x : Matrix (S n) (S m) a) -> Matrix (S n) (S m) (Matrix n m a)
  minors' {n} {m} x = mapMatrix (\(i, j) => subMatrix i j x) (coords (S n) (S m))

||| Calculates the matrix of cofactors for the given square matrix.
|||
||| @x the matrix
export
cofactors : Neg a => (x : Matrix n n a) -> Matrix n n a
cofactors {n} x = hadamard (signs n n False) (minors x) where
  ||| Generates an alternating vector of +1 and -1 of length `n`
  |||
  ||| @n the length of the vector to ganerate
  ||| @b if set to false, the first element will be 1, otherwise it will be -1
  signs' : (n : Nat) -> (b : Bool) -> Vect n a
  signs' Z _ = []
  signs' (S k) False = 1 :: (signs' k True)
  signs' (S k) True = -1 :: (signs' k False)
  ||| Generates an alternating matrix of +1 and -1 of order m × n.
  |||
  ||| @n the first matrix dimension
  ||| @m the second matrix dimension
  ||| @b if set to false, the first element will be 1, otherwise it will be -1
  signs : (n : Nat) -> (m : Nat) -> (b : Bool) -> Matrix n m a
  signs Z m _ = []
  signs (S k) m False = (signs' m False) :: (signs k m True)
  signs (S k) m True = (signs' m True) :: (signs k m False)

||| Calculates the adjugate of the given square matrix.
|||
||| @x the matrix
export
adjugate : Neg a => (x : Matrix n n a) -> Matrix n n a
adjugate x = transpose (cofactors x)

||| Calculates the inverse of the given square matrix (must be of at least order 1).
|||
||| @x the matrix
export
inverse : Neg a => Fractional a => (x : Matrix n n a) -> Matrix n n a
inverse x = (1 / (determinant x)) <#> (adjugate x)

||| Calculates an inverse Gramian matrix.
|||
||| @x the matrix
export
inverseGram : Neg a => Fractional a => (x : Matrix (S n) (S m) a) -> Matrix (S m) (S m) a
inverseGram x = inverse (gram x)

max_stars_repo_name: lambdacasserole/equis

max_issues_repo_name: lambdacasserole/equis

max_forks_repo_name: lambdacasserole/equis


text:
module Prelude

{-
The Prelude is minimal (since it is effectively part of the language
specification, this seems to be desirable - we should, nevertheless, aim to
provide a good selection of base libraries). A rule of thumb is that it should
contain the basic functions required by almost any non-trivial program.

As such, it should contain:

- Anything the elaborator can desugar to (e.g. pairs, unit, =, laziness)
- Basic types Bool, Nat, List, Dec, Maybe, Either
- The most important utility functions: id, the, composition, etc
- Interfaces for arithmetic and implementations for the primitives and
  basic types
- Char and String manipulation
- Show, Eq, Ord, and implementations for all types in the prelude
- Interfaces and functions for basic proof (cong, Uninhabited, etc) --
- Semigroup, Monoid
- Functor, Applicative, Monad and related functions
- Foldable, Traversable
- Enum for range syntax
- Console IO and interfaces for supporting IO

Everything else should be in the base libraries, and imported as required.
In particular, proofs of Nat/List properties that almost never get used in
practice would probably be better in base libraries.

Everything should be total, unless there's a good justification for it not
to be (division by zero, as a concrete example).

(These guidelines will probably get revised a few times.)
-}

import public Builtin
import public PrimIO
import public Prelude.Basics as Prelude
import public Prelude.EqOrd as Prelude
import public Prelude.Interfaces as Prelude
import public Prelude.IO as Prelude
import public Prelude.Num as Prelude
import public Prelude.Ops as Prelude
import public Prelude.Show as Prelude
import public Prelude.Types as Prelude
import public Prelude.Uninhabited as Prelude


text:
module Test

import Data.List
import System

import DecompressionTest
import ClientTest
import Control.Monad.Error.Either

%default partial

run_test : String -> EitherT String IO () -> IO Bool
run_test name test = do
  Right () <- runEitherT test
  | Left err => putStrLn "\{name}: failed \{err}" $> False
  putStrLn "\{name}: success" $> True

run : List (IO Bool) -> IO ()
run tests = do
  results <- sequence tests
  let [] = filter not results
  | xs => putStrLn "\{show (length xs)} tests failed" *> exitFailure
  putStrLn "all tests passed"

export
main : IO ()
main = run
  [ run_test "decompress random.bin.gz" test_gzip_uncompressed
  , run_test "decompress hello.gz" test_gzip_fixed_huffman
  , run_test "decompress jabberwock.txt.gz" test_gzip_text
  , run_test "decompress jabberwocky.jpg.gz" test_gzip_jpg
  , run_test "decompress concatenated.gz" test_gzip_concated
  , run_test "http close w/out read" test_close_without_read
  , run_test "http cookie jar" test_cookie
  , run_test "http httpbin deflate" test_json_deflate
  , run_test "http httpbin gzip" test_json_gzip
  , run_test "http httpbin post" test_post
  , run_test "http openbsd redirect" test_redirect
  ]


text:
module ExplicitNamespaces

namespace X
  export
  test : Int -> Int
  test x = x * 2

namespace Y
  export
  test : String -> String
  test s = "Hello, " ++ s

max_stars_repo_name: timmyjose-study/idris-from-the-docs

max_issues_repo_name: timmyjose-study/idris-from-the-docs

max_forks_repo_name: timmyjose-study/idris-from-the-docs


text:
module Data.SortedSet

import Data.Maybe
import Data.SortedMap

export
data SortedSet k = SetWrapper (Data.SortedMap.SortedMap k ())

export
empty : Ord k => SortedSet k
empty = SetWrapper Data.SortedMap.empty

export
insert : k -> SortedSet k -> SortedSet k
insert k (SetWrapper m) = SetWrapper (Data.SortedMap.insert k () m)

export
delete : k -> SortedSet k -> SortedSet k
delete k (SetWrapper m) = SetWrapper (Data.SortedMap.delete k m)

export
contains : k -> SortedSet k -> Bool
contains k (SetWrapper m) = isJust (Data.SortedMap.lookup k m)

export
fromList : Ord k => List k -> SortedSet k
fromList l = SetWrapper (Data.SortedMap.fromList (map (\i => (i, ())) l))

export
toList : SortedSet k -> List k
toList (SetWrapper m) = map (\(i, _) => i) (Data.SortedMap.toList m)

export
Foldable SortedSet where
  foldr f e xs = foldr f e (Data.SortedSet.toList xs)

||| Set union. Inserts all elements of x into y
export
union : (x, y : SortedSet k) -> SortedSet k
union x y = foldr insert x y

||| Set difference. Delete all elments in y from x
export
difference : (x, y : SortedSet k) -> SortedSet k
difference x y = foldr delete x y

||| Set symmetric difference. Uses the union of the differences.
export
symDifference : (x, y : SortedSet k) -> SortedSet k
symDifference x y = union (difference x y) (difference y x)

||| Set intersection. Implemented as the difference of the union and the symetric difference.
export
intersection : (x, y : SortedSet k) -> SortedSet k
intersection x y = difference x (difference x y)

export
Ord k => Semigroup (SortedSet k) where
  (<+>) = union

export
Ord k => Monoid (SortedSet k) where
  neutral = empty

export
keySet : SortedMap k v -> SortedSet k
keySet = SetWrapper . map (const ())


text:
module Test.Asserts

%default total
%access public export

assertEq : Eq a => (given : a) -> (expected : a) -> IO ()
assertEq g e = if g == e
    then putStrLn "Test Passed"
    else putStrLn "Test Failed"

max_stars_repo_name: rpeszek/idris-chain

max_issues_repo_name: rpeszek/idris-chain

max_forks_repo_name: rpeszek/idris-chain


text:
= ProofObjects : The Curry-Howard Correspondence

> module ProofObjects
>

\say{\textit{Algorithms are the computational content of proofs.}}
-- Robert Harper

> import Logic
> import IndProp
>

We have seen that Idris has mechanisms both for _programming_, using inductive
data types like \idr{Nat} or \idr{List} and functions over these types, and for
_proving_ properties of these programs, using inductive propositions (like
\idr{Ev}), implication, universal quantification, and the like. So far, we have
mostly treated these mechanisms as if they were quite separate, and for many
purposes this is a good way to think. But we have also seen hints that Idris's
programming and proving facilities are closely related. For example, the keyword
\idr{data} is used to declare both data types and propositions, and \idr{->} is
used both to describe the type of functions on data and logical implication.
This is not just a syntactic accident! In fact, programs and proofs in Idris are
almost the same thing. In this chapter we will study how this works.

We have already seen the fundamental idea: provability in Idris is represented
by concrete _evidence_. When we construct the proof of a basic proposition, we
are actually building a tree of evidence, which can be thought of as a data
structure.

If the proposition is an implication like \idr{A -> B}, then its proof will be
an evidence _transformer_: a recipe for converting evidence for \idr{A} into
evidence for \idr{B}. So at a fundamental level, proofs are simply programs that
manipulate evidence.

Question: If evidence is data, what are propositions themselves?

Answer: They are types!

Look again at the formal definition of the \idr{Ev} property.

```idris
data Ev : Nat -> Type where
  Ev_0 : Ev Z
  Ev_SS : {n : Nat} -> Ev n -> Ev (S (S n))
```

Suppose we introduce an alternative pronunciation of "\idr{:}". Instead of "has
type," we can say "is a proof of." For example, the second line in the
definition of \idr{Ev} declares that \idr{Ev_0 : Ev 0}. Instead of "\idr{Ev_0}
has type \idr{Ev 0}," we can say that "\idr{Ev_0} is a proof of \idr{Ev 0}."

This pun between types and propositions — between \idr{:} as "has type" and
\idr{:} as "is a proof of" or "is evidence for" — is called the Curry-Howard
correspondence. It proposes a deep connection between the world of logic and the
world of computation:

                 propositions  ~  types
                 proofs        ~  data values

\todo[inline]{Add http://dl.acm.org/citation.cfm?id=2699407 as a link}

See [Wadler 2015] for a brief history and an up-to-date exposition.

Many useful insights follow from this connection. To begin with, it gives us a
natural interpretation of the type of the \idr{Ev_SS} constructor:

```idris
λΠ> :t Ev_SS
Ev_SS : Ev n -> Ev (S (S n))
```

This can be read "\idr{Ev_SS} is a constructor that takes two arguments — a
number \idr{n} and evidence for the proposition \idr{Ev n} — and yields evidence
for the proposition \idr{Ev (S (S n))}."

Now let's look again at a previous proof involving \idr{Ev}.

> ev_4 : Ev 4
> ev_4 = Ev_SS {n=2} $ Ev_SS {n=0} Ev_0

As with ordinary data values and functions, we can use the \idr{:printdef}
command to see the proof object that results from this proof script.

```idris
λΠ> :printdef ev_4
ev_4 : Ev 4
ev_4 = Ev_SS (Ev_SS Ev_0)
```

As a matter of fact, we can also write down this proof object directly, without
the need for a separate proof script:

```idris
λΠ> Ev_SS $ Ev_SS Ev_0
Ev_SS (Ev_SS Ev_0) : Ev 4
```

The expression \idr{Ev_SS {n=2} $ Ev_SS {n=0} Ev_0} can be thought of as
instantiating the parameterized constructor \idr{Ev_SS} with the specific
arguments \idr{2} and \idr{0} plus the corresponding proof objects for its
premises \idr{Ev 2} and \idr{Ev 0}. Alternatively, we can think of \idr{Ev_SS}
as a primitive "evidence constructor" that, when applied to a particular number,
wants to be further applied to evidence that that number is even; its type,

```idris
      {n : Nat} -> Ev n -> Ev (S (S n))
```

expresses this functionality, in the same way that the polymorphic type
\idr{{x : Type} -> List x} expresses the fact that the constructor \idr{Nil} can
be thought of as a function from types to empty lists with elements of that
type.

\todo[inline]{Edit or remove}

We saw in the `Logic` chapter that we can use function application syntax to
instantiate universally quantified variables in lemmas, as well as to supply
evidence for assumptions that these lemmas impose. For instance:

```coq
Theorem ev_4': ev 4.
Proof.
  apply (ev_SS 2 (ev_SS 0 ev_0)).
Qed.
```

We can now see that this feature is a trivial consequence of the status the
Idris grants to proofs and propositions: Lemmas and hypotheses can be combined
in expressions (i.e., proof objects) according to the same basic rules used for
programs in the language.

== Proof Scripts

\ \todo[inline]{Rewrite, keep explanation about holes? Seems a bit late for
that}

The _proof objects_ we've been discussing lie at the core of how Idris operates.
When Idris is following a proof script, what is happening internally is that it
is gradually constructing a proof object — a term whose type is the proposition
being proved. The expression on the right hand side of \idr{=} tell it how to
build up a term of the required type. To see this process in action, let's use
the `Show Proof` command to display the current state of the proof tree at
various points in the following tactic proof.

```coq
Theorem ev_4'' : ev 4.
Proof.
  Show Proof.
  apply ev_SS.
  Show Proof.
  apply ev_SS.
  Show Proof.
  apply ev_0.
  Show Proof.
Qed.
```

At any given moment, Idris has constructed a term with a "hole" (indicated by
`?Goal` here, and so on), and it knows what type of evidence is needed to fill
this hole.

Each hole corresponds to a subgoal, and the proof is finished when there are no
more subgoals. At this point, the evidence we've built stored in the global
context under the name given in the type definition.

Tactic proofs are useful and convenient, but they are not essential: in
principle, we can always construct the required evidence by hand, as shown
above. Then we can use `Definition` (rather than `Theorem`) to give a global
name directly to a piece of evidence.

```coq
Definition ev_4''' : ev 4 :=
  ev_SS 2 (ev_SS 0 ev_0).
```

All these different ways of building the proof lead to exactly the same evidence
being saved in the global environment.

```coq
Print ev_4.
(* ===> ev_4    =   ev_SS 2 (ev_SS 0 ev_0) : ev 4 *)
Print ev_4'.
(* ===> ev_4'   =   ev_SS 2 (ev_SS 0 ev_0) : ev 4 *)
Print ev_4''.
(* ===> ev_4''  =   ev_SS 2 (ev_SS 0 ev_0) : ev 4 *)
Print ev_4'''.
(* ===> ev_4''' =   ev_SS 2 (ev_SS 0 ev_0) : ev 4 *)
```

==== Exercise: 1 star (eight_is_even)

\ \todo[inline]{Remove?}

Give a tactic proof and a proof object showing that \idr{Ev 8}.

> ev_8 : Ev 8
> ev_8 = ?ev_8_rhs

$\square$

==== Quantifiers, Implications, Functions

\ \todo[inline]{Edit the section}

In Idris's computational universe (where data structures and programs live),
there are two sorts of values with arrows in their types: _constructors_
introduced by \idr{data} definitions, and _functions_.

Similarly, in Idris's logical universe (where we carry out proofs), there are
two ways of giving evidence for an implication: constructors introduced by
\idr{data}-defined propositions, and... functions!

For example, consider this statement:

> ev_plus4 : Ev n -> Ev (4 + n)
> ev_plus4 x = Ev_SS $ Ev_SS x

What is the proof object corresponding to `ev_plus4`?

We're looking for an expression whose type is
\idr{{n: Nat} -> Ev n -> Ev (4 + n)} — that is, a function that takes two
arguments (one number and a piece of evidence) and returns a piece of evidence!
Here it is:

```coq
Definition ev_plus4' : forall n, ev n -> ev (4 + n) :=
  fun (n : Nat) => fun (H : ev n) =>
    ev_SS (S (S n)) (ev_SS n H).
```

Recall that \idr{\n => blah} means "the function that, given \idr{n}, yields
\idr{blah}," and that Idris treats \idr{4 + n} and \idr{S (S (S (S n)))} as
synonyms. Another equivalent way to write this definition is:

```coq
Definition ev_plus4'' (n : Nat) (H : ev n) : ev (4 + n) :=
  ev_SS (S (S n)) (ev_SS n H).

Check ev_plus4''.
(* ===> ev_plus4'' : forall n : Nat, ev n -> ev (4 + n) *)
```

When we view the proposition being proved by \idr{ev_plus4} as a function type,
one aspect of it may seem a little unusual. The second argument's type,
\idr{Ev n}, mentions the _value_ of the first argument, \idr{n}. While such
_dependent types_ are not found in conventional programming languages, they can
be useful in programming too, as the recent flurry of activity in the functional
programming community demonstrates.

\todo[inline]{Reword?}

Notice that both implication (\idr{->}) and quantification
(\idr{(x : t) -> f x}) correspond to functions on evidence. In fact, they are
really the same thing: \idr{->} is just a shorthand for a degenerate use of
quantification where there is no dependency, i.e., no need to give a name to the
type on the left-hand side of the arrow.

For example, consider this proposition:

> ev_plus2 : Type
> ev_plus2 = (n : Nat) -> (e : Ev n) -> Ev (n + 2)

A proof term inhabiting this proposition would be a function with two arguments:
a number \idr{n} and some evidence \idr{e} that \idr{n} is even. But the name
\idr{e} for this evidence is not used in the rest of the statement of
\idr{ev_plus2}, so it's a bit silly to bother making up a name for it. We could
write it like this instead:

> ev_plus2' : Type
> ev_plus2' = (n : Nat) -> Ev n -> Ev (n + 2)

In general, "\idr{p -> q}" is just syntactic sugar for "\idr{(_ : p) -> q}".

== Programming with Tactics

\ \todo[inline]{Edit and move to an appendix about ElabReflection/Pruviloj?}

If we can build proofs by giving explicit terms rather than executing tactic
scripts, you may be wondering whether we can build _programs_ using _tactics_
rather than explicit terms. Naturally, the answer is yes!

```coq
Definition add1 : Nat -> Nat.
intro n.
Show Proof.
apply S.
Show Proof.
apply n. Defined.

Print add1.
(* ==>
    add1 = fun n : Nat => S n
         : Nat -> Nat
*)

Compute add1 2.
(* ==> 3 : Nat *)
```

Notice that we terminate the `Definition` with a `.` rather than with `:=`
followed by a term. This tells Idris to enter _proof scripting mode_ to build an
object of type \idr{Nat -> Nat}. Also, we terminate the proof with `Defined`
rather than `Qed`; this makes the definition _transparent_ so that it can be
used in computation like a normally-defined function. (`Qed`-defined objects are
opaque during computation.)

This feature is mainly useful for writing functions with dependent types, which
we won't explore much further in this book. But it does illustrate the
uniformity and orthogonality of the basic ideas in Idris.

== Logical Connectives as Inductive Types

Inductive definitions are powerful enough to express most of the connectives and
quantifiers we have seen so far. Indeed, only universal quantification (and thus
implication) is built into Idris; all the others are defined inductively. We'll
see these definitions in this section.

=== Conjunction

\ \todo[inline]{Edit}

To prove that \idr{(p,q)} holds, we must present evidence for both \idr{p} and
\idr{q}. Thus, it makes sense to define a proof object for \idr{(p,q)} as
consisting of a pair of two proofs: one for \idr{p} and another one for \idr{q}.
This leads to the following definition.

> data And : (p, q : Type) -> Type where
>   Conj : p -> q -> And p q

Notice the similarity with the definition of the \idr{Prod} type, given in
chapter `Poly`; the only difference is that \idr{Prod} takes Type arguments,
whereas and takes Prop arguments.

```idris
data Prod : (x, y : Type) -> Type where
  PPair : x -> y -> Prod x y
```

This should clarify why pattern matching can be used on a conjunctive
hypothesis. Case analysis allows us to consider all possible ways in which
\idr{(p,q)} was proved — here just one (the \idr{Conj} constructor). Similarly,
the `split` tactic actually works for any inductively defined proposition with
only one constructor. In particular, it works for \idr{And}:

> and_comm : (And p q) <-> (And q p)
> and_comm = (\(Conj x y) => Conj y x,
>             \(Conj y x) => Conj x y)

This shows why the inductive definition of `and` can be manipulated by tactics
as we've been doing. We can also use it to build proofs directly, using
pattern-matching. For instance:

> and_comm'_aux : And p q -> And q p
> and_comm'_aux (Conj x y) = Conj y x

> and_comm' : (And p q) <-> (And q p)
> and_comm' {p} {q} = (and_comm'_aux {p} {q}, and_comm'_aux {p=q} {q=p})

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

Construct a proof object demonstrating the following proposition.

> conj_fact : And p q -> And q r -> And p r
> conj_fact pq qr = ?conj_fact_rhs

$\square$

=== Disjunction

The inductive definition of disjunction uses two constructors, one for each side
of the disjunct:

> data Or : (p, q : Type) -> Type where
>   IntroL : p -> Or p q
>   IntroR : q -> Or p q

This declaration explains the behavior of pattern matching on a disjunctive
hypothesis, since the generated subgoals match the shape of the \idr{IntroL} and
\idr{IntroR} constructors.

Once again, we can also directly write proof objects for theorems involving
\idr{Or}, without resorting to tactics.

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

\ \todo[inline]{Edit}

Try to write down an explicit proof object for \idr{or_comm} (without using
`Print` to peek at the ones we already defined!).

> or_comm : Or p q -> Or q p
> or_comm pq = ?or_comm_rhs

$\square$

=== Existential Quantification

To give evidence for an existential quantifier, we package a witness \idr{x}
together with a proof that \idr{x} satisfies the property \idr{p}:

> data Ex : (p : a -> Type) -> Type where
>   ExIntro : (x : a) -> p x -> Ex p

This may benefit from a little unpacking. The core definition is for a type
former \idr{Ex} that can be used to build propositions of the form \idr{Ex p},
where \idr{p} itself is a function from witness values in the type \idr{a} to
propositions. The \idr{ExIntro} constructor then offers a way of constructing
evidence for \idr{Ex p}, given a witness \idr{x} and a proof of \idr{p x}.

The more familiar form \idr{(x ** p x)} desugars to an expression involving
\idr{Ex}:

\todo[inline]{Edit}

```coq
Check ex (fun n => ev n).
(* ===> exists n : Nat, ev n
        : Prop *)
```

Here's how to define an explicit proof object involving \idr{Ex}:

> some_nat_is_even : Ex (\n => Ev n)
> some_nat_is_even = ExIntro 4 (Ev_SS $ Ev_SS Ev_0)

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

Complete the definition of the following proof object:

> ex_ev_Sn : Ex (\n => Ev (S n))
> ex_ev_Sn = ?ex_ev_Sn_rhs

$\square$

\subsection{\idr{Unit} and \idr{Void}}

The inductive definition of the \idr{Unit} proposition is simple:

```idris
data Unit : Type where
  () : Unit
```

It has one constructor (so every proof of \idr{Unit} is the same, so being given
a proof of\idr{Unit} is not informative.)

\idr{Void} is equally simple — indeed, so simple it may look syntactically wrong
at first glance!

\todo[inline]{Edit, this actually is wrong, stdlib uses \idr{runElab} to define
it}

```idris
data Void : Type where
```

That is, \idr{Void} is an inductive type with _no_ constructors — i.e., no way
to build evidence for it.

== Equality

\ \todo[inline]{Edit, it actually is built in}

Even Idris's equality relation is not built in. It has the following inductive
definition. (Actually, the definition in the standard library is a small variant
of this, which gives an induction principle that is slightly easier to use.)

> data PropEq : {t : Type} -> t -> t -> Type where
>   EqRefl : PropEq x x

> syntax [x] "='" [y] = PropEq x y

The way to think about this definition is that, given a set \idr{t}, it defines
a _family_ of propositions "\idr{x} is equal to \idr{y}," indexed by pairs of
values (\idr{x} and \idr{y}) from \idr{t}. There is just one way of constructing
evidence for each member of this family: applying the constructor \idr{EqRefl}
to a type \idr{t} and a value \idr{x : t} yields evidence that \idr{x} is equal
to \idr{x}.

\todo[inline]{Edit}

We can use \idr{EqRefl} to construct evidence that, for example, \idr{2 = 2}.
Can we also use it to construct evidence that \idr{1 + 1 = 2}? Yes, we can.
Indeed, it is the very same piece of evidence! The reason is that Idris treats
as "the same" any two terms that are _convertible_ according to a simple set of
computation rules. These rules, which are similar to those used by `Compute`,
include evaluation of function application, inlining of definitions, and
simplification of `match`es.

> four : (2 + 2) =' (1 + 3)
> four = EqRefl

The \idr{Refl} that we have used to prove equalities up to now is essentially
just an application of an equality constructor.

\todo[inline]{Edit}

In tactic-based proofs of equality, the conversion rules are normally hidden in
uses of `simpl` (either explicit or implicit in other tactics such as
`reflexivity`). But you can see them directly at work in the following explicit
proof objects:

```coq
Definition four' : 2 + 2 = 1 + 3 :=
  eq_refl 4.
```

> singleton : ([]++[x]) =' (x::[])
> singleton = EqRefl

> quiz6 : Ex (\x => (x + 3) =' 4)
> quiz6 = ExIntro 1 EqRefl

==== Exercise: 2 stars (equality__leibniz_equality)

The inductive definition of equality corresponds to _Leibniz equality_: what we
mean when we say "\idr{x} and \idr{y} are equal" is that every property \idr{p}
that is true of \idr{x} is also true of \idr{y}.

> equality__leibniz_equality : (x =' y) -> ((p : t -> Type) -> p x -> p y)
> equality__leibniz_equality eq p px = ?equality__leibniz_equality_rhs

$\square$

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

Show that, in fact, the inductive definition of equality is _equivalent_ to
Leibniz equality:

> leibniz_equality__equality : ((p : t -> Type) -> p x -> p y) -> (x =' y)
> leibniz_equality__equality pxy = ?leibniz_equality__equality_rhs

$\square$

=== Inversion, Again

\ \todo[inline]{Edit/remove}

We've seen `inversion` used with both equality hypotheses and hypotheses about
inductively defined propositions. Now that we've seen that these are actually
the same thing, we're in a position to take a closer look at how `inversion`
behaves.

In general, the `inversion` tactic...

  - takes a hypothesis `H` whose type `P` is inductively defined, and

  - for each constructor `C` in `P`'s definition,

    - generates a new subgoal in which we assume `H` was built with `C`,

    - adds the arguments (premises) of `C` to the context of the subgoal as
      extra hypotheses,

    - matches the conclusion (result type) of `C` against the current goal and
      calculates a set of equalities that must hold in order for `C` to be
      applicable,

    - adds these equalities to the context (and, for convenience, rewrites them
      in the goal), and

    - if the equalities are not satisfiable (e.g., they involve things like
      \idr{S n = Z}), immediately solves the subgoal.

_Example_: If we invert a hypothesis built with \idr{Or}, there are two
constructors, so two subgoals get generated. The conclusion (result type) of the
constructor (\idr{Or p q}) doesn't place any restrictions on the form of \idr{p}
or \idr{q}, so we don't get any extra equalities in the context of the subgoal.

_Example_: If we invert a hypothesis built with \idr{And}, there is only one
constructor, so only one subgoal gets generated. Again, the conclusion (result
type) of the constructor (\idr{And p q}) doesn't place any restrictions on the
form of \idr{p} or \idr{q}, so we don't get any extra equalities in the context
of the subgoal. The constructor does have two arguments, though, and these can
be seen in the context in the subgoal.

_Example_: If we invert a hypothesis built with \idr{PropEq}, there is again
only one constructor, so only one subgoal gets generated. Now, though, the form
of the \idr{EqRefl} constructor does give us some extra information: it tells us
that the two arguments to \idr{PropEq} must be the same! The `inversion` tactic
adds this fact to the context.

max_stars_repo_name: diseraluca/software-foundations

max_issues_repo_name: diseraluca/software-foundations

max_forks_repo_name: diseraluca/software-foundations