text:
module PLFI.Part1.Induction

-- http://plfa.github.io/Induction/

import PLFI.Part1.Naturals
import public Syntax.PreorderReasoning

%hide Prelude.(+)
%hide Prelude.(*)

{-

Proof by induction

 ------
 P Zero

   P m
---------
P (Suc m)

-}

{-
Our first proof: associativity

(m + n) + p = m + (n + p)

-------------------------------
(Zero + n) + p = Zero + (n + p)

   (m + n) + p = m + (n + p)
---------------------------------
(Suc m + n) + p = suc m + (n + p)
-}

-- export
-- addAssoc : (m, n, p : N) -> (m + n) + p = m + (n + p)
-- addAssoc Zero    n p = Refl
-- addAssoc (Suc m) n p = cong Suc $ addAssoc m n p

export
addAssoc : (m, n, p : N) -> (m + n) + p = m + (n + p)
addAssoc Zero n p = Calc $
  |~ (Zero + n) + p
  ~~ n + p             ... (Refl)
  ~~ Zero + (n + p)    ... (Refl)
addAssoc (Suc m) n p = Calc $
  |~ ((Suc m) + n) + p
  ~~ Suc (m + n) + p    ... (Refl)
  ~~ Suc ((m + n) + p)  ... (Refl)
  ~~ Suc (m + (n + p))  ... (cong Suc (addAssoc m n p))
  ~~ Suc m + (n + p)    ... (Refl)

{-
addAssoc : (m, n, p : N) -> (m + n) + p = m + (n + p)
addAssoc Zero n p = Calc $
  |~ ((Zero + n) + p)
  ~~ (n + p)                ...(cong (+p) addEquation1)
  ~~ (Zero + (n + p))       ...(sym addEquation1)
addAssoc (Suc m) n p = Calc $
  |~ ((Suc m + n) + p)
  ~~ (Suc (m + n) + p)
  ~~ (Suc ((m + n) + p))
  ~~ (Suc (m + (n + p)))
  ~~ (Suc m + (n + p))
-}

{-
Our second proof: commutativity
m + n = n + m
-}

{-
The first lemma
m + zero = m
-}

export
addIdentityL : (n : N) -> Zero + n = n
addIdentityL n = Refl

-- addIdentityR1 : (n : N) -> n + Zero = n
-- addIdentityR1 Zero = Refl
-- addIdentityR1 (Suc m) = cong Suc (addIdentityR1 m)

export
addIdentityR : (n : N) -> n + Zero = n
addIdentityR Zero = Calc $
  |~ Zero + Zero
  ~~ Zero         ... (Refl)
addIdentityR (Suc m) = Calc $
  |~ (Suc m) + Zero
  ~~ Suc (m + Zero) ... (Refl)
  ~~ Suc m          ... (cong Suc (addIdentityR m))

{-
The second lemma
m + suc n = suc (m + n)
-}

export
addSuccL : (m, n : N) -> (Suc m) + n = Suc (m + n)
addSuccL m n = Refl

export
addSucR : (m, n : N) -> m + (Suc n) = Suc (m + n)
addSucR Zero n = Calc $
  |~ Zero + (Suc n)
  ~~ Suc n           ... (Refl)
  ~~ Suc (Zero + n)  ... (Refl)
addSucR (Suc m) n = Calc $
  |~ (Suc m) + (Suc n)
  ~~ Suc (m + Suc n)   ... (Refl)
  ~~ Suc (Suc (m + n)) ... (cong Suc (addSucR m n))
  ~~ Suc ((Suc m) + n) ... (Refl)

{-
The proposition
m + n = n + m
-}

export
addComm : (n, m : N) -> n + m = m + n
addComm Zero    m = sym (addIdentityR m)
addComm (Suc x) m = Calc $
  |~ (Suc x) + m
  ~~ Suc (x + m) ... (Refl)
  ~~ Suc (m + x) ... (cong Suc (addComm x m))
  ~~ m + (Suc x) ... (sym (addSucR m x))

{-
Our first corollary: rearranging
-}

export
addRearrange : (m,n,p,q : N) -> (m + n) + (p + q) = m + (n + p) + q
addRearrange m n p q = Calc $
  |~ (m + n) + (p + q)
  ~~ m + (n + (p + q)) ... (addAssoc m n (p + q))
  ~~ m + ((n + p) + q) ... (cong (m+) (sym (addAssoc n p q)))
  ~~ (m + (n + p)) + q ... (sym (addAssoc m (n+p) q))
  ~~ m + (n + p) + q   ... (Refl)

{-
Associativity with rewrite
addAssocRW : (m + n) + p = m + (n + p)
-}

addAssocWithRewrite : (m,n,p : N) -> (m + n) + p = m + (n + p)
addAssocWithRewrite Zero n p
  = Refl
addAssocWithRewrite (Suc m) n p
  = rewrite (addAssocWithRewrite m n p) in
    Refl

addAssocWithRewriteN : (m,n,p : N) -> (m + n) + p = m + (n + p)
addAssocWithRewriteN m Zero p
  = rewrite (addIdentityR m) in
    Refl
addAssocWithRewriteN m (Suc x) p
  = rewrite (addSucR m x) in
    rewrite (addSucR m (x + p)) in
    rewrite (addAssocWithRewriteN m x p) in
    Refl

addIdentityRWithRewrite : (n : N) -> n + Zero = n
addIdentityRWithRewrite Zero
  = Refl
addIdentityRWithRewrite (Suc m)
  = rewrite (addIdentityRWithRewrite m) in
    Refl

addSucWithRewrite : (m, n : N) -> m + (Suc n) = Suc (m + n)
addSucWithRewrite Zero n
  = Refl
addSucWithRewrite (Suc m) n
  = rewrite (addSucWithRewrite m n) in Refl

addCommWithRewrite : (n, m : N) -> n + m = m + n
addCommWithRewrite Zero m
  = rewrite (addIdentityRWithRewrite m) in
    Refl
addCommWithRewrite (Suc x) m
  = rewrite (addCommWithRewrite x m) in
    rewrite (addSucWithRewrite m x) in
    Refl

-- Exercise (recommended)

-- addAssoc : (m, n, p : N) -> (m + n) + p = m + (n + p)
-- addComm  : (n, m : N)    -> n + m = m + n

swap : (m,n,p : N) -> m + (n + p) = n + (m + p)
swap m n p = Calc $
  |~ m + (n + p)
  ~~ (m + n) + p ... (sym (addAssoc m n p))
  ~~ (n + m) + p ... (cong (+p) (addComm m n))
  ~~ n + (m + p) ... (addAssoc n m p)

-- Exercise (recommended)

multDistribAddR : (m,n,p : N) -> (m + n) * p = m * p + n * p
multDistribAddR Zero n p = Refl
multDistribAddR (Suc m) n p = Calc $
  |~ p + ((m + n) * p)
  ~~ p + ((m * p) + (n * p)) ... (cong (p+) (multDistribAddR m n p))
  ~~ (p + (m * p)) + (n * p) ... (sym (addAssoc p (m * p) (n * p)))

-- Exercise (recommended)

multAssoc : (m,n,p : N) -> (m * n) * p = m * (n * p)
multAssoc Zero n p = Refl
multAssoc (Suc m) n p = Calc $
  |~ (n + (m * n)) * p
  ~~ (n * p) + ((m * n) * p) ... (multDistribAddR n (m * n) p)
  ~~ (n * p) + (m * (n * p)) ... (cong ((n*p)+) (multAssoc m n p))

-- Exercise (practice)

multZeroR : (n : N) -> Zero = n * Zero
multZeroR Zero = Refl
multZeroR (Suc m) = multZeroR m

multOneL : (n : N) -> 1 * n = n
multOneL n = addIdentityR n

multOneR : (n : N) -> n = n * 1
multOneR Zero    = Refl
multOneR (Suc m) = cong Suc (multOneR m)

multDistribAddL : (m,n,p : N) -> p * (m + n) = p * m + p * n
multDistribAddL m n Zero = Refl
multDistribAddL m n (Suc p) = Calc $
  |~ (m + n) + (p * (m + n))
  ~~ (m + n) + (p * m + p * n)     ... (cong (\x => (m+n)+x) (multDistribAddL m n p))
  ~~ ((m + n) + (p * m)) + (p * n) ... (sym (addAssoc (m + n) (p * m) (p * n)))
  ~~ (m + (n + (p * m))) + (p * n) ... (cong (+(p*n)) (addAssoc m n (p * m)))
  ~~ (m + ((p * m) + n)) + (p * n) ... (cong (\x => (m+x)+(p*n)) (addComm n (p * m)))
  ~~ ((m + (p * m)) + n) + (p * n) ... (cong (\x => x+(p*n)) (sym (addAssoc m (p * m) n)))
  ~~ (m + (p * m)) + (n + (p * n)) ... (addAssoc (m + (p * m)) n (p * n))

multComm : (m,n : N) -> m * n = n * m
multComm Zero n = multZeroR n
multComm (Suc m) n = Calc $
  |~ n + (m * n)
  ~~ n + (n * m)        ... (cong (\x => n+x) (multComm m n))
  ~~ (n * 1) + (n * m)  ... (cong (\x => x+(n*m)) (multOneR n))
  ~~ n * (1 + m)        ... (sym (multDistribAddL 1 m n))
  ~~ n * (Suc m)        ... (Refl)

-- -- Exercise (practice)

-- zeroMonus : (n : N) -> Zero -* n = Zero

-- -- Exercise (practice)

-- monusAssoc : (m,n,p : N) -> m -* n -* p = m -* (n + p)

-- -- Exercise (strech)

-- expDistribLOverMult : (m,n,p : N) -> m ^ (n + p) = (m ^ n) * (m ^ p)
-- expDistribOverMult : (m,n,p : N) -> (m * n) ^ p = (m ^ p) * (n ^ p)
-- expAssoc : (m,n,p : N) -> (m ^ n) ^ p = m ^ (n ^ p)

-- -- Exercise (strech)

-- incFrom : (b : Bin) -> from (inc b) = Suc (from b)
-- fromTo  : (b : Bin) -> to (from b) = b
-- toFrom  : (b : Bin) -> (to n) = n

max_stars_repo_name: andorp/PLFI

max_issues_repo_name: andorp/PLFI

max_forks_repo_name: andorp/PLFI


text:
module Actors

%default total

data Request = Add Nat Nat

Response: Request -> Type
Response (Add x y ) = Nat

adder: ServerLoop Response ()
adder = do Action(PutStrLn "Waiting...")
           Accept( \msg => case msg of
                           Add x y => Pure ( x + y ))
           Loop adder

client: Server Response -> Client ()
client addServer = do Action(PutStr "Number :")
                      num <- Action getLine
                      answer <- Send addServer (cast num Nat) 94
                      Action(PutStrLn answer)

-- TODO define actor possible states as data type....
data Actor = Ready | Done

ext: idr

max_stars_repo_name: asmodehn/idris-playground

max_issues_repo_name: asmodehn/idris-playground

max_forks_repo_name: asmodehn/idris-playground


text:
import Data.IORef

count : Nat -> IORef Integer -> IO ()
count Z ref
    = do x <- readIORef ref
         printLn x
count (S k) ref
    = do modifyIORef ref (+1)
         count k ref

main : IO ()
main = do r <- newIORef 0
          count 100 r

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
> module SimpleProb.MonadicProperties

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

> import SimpleProb.SimpleProb
> import SimpleProb.BasicOperations
> import SimpleProb.BasicProperties
> import SimpleProb.MonadicOperations
> import NonNegRational.NonNegRational
> import NonNegRational.BasicOperations
> import NonNegRational.BasicProperties

> import Nat.Positive
> import Nat.Coprime
> import Fraction.Normal
> import Num.Refinements
> import Num.Properties
> import Fun.Operations
> import List.Operations
> import List.Properties
> import Unique.Predicates
> import Finite.Predicates
> import Sigma.Sigma

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

* Properties of |normalize|, |support| and |ret|:

> |||
> normalizeRetLemma : {A : Type} -> (a : A) -> normalize (ret a) = ret a
> normalizeRetLemma a = ( normalize (ret a) )
>                     ={ Refl }=
>                       ( normalize (MkSimpleProb ((a, 1) :: Nil) (sumMapSndSingletonLemma a 1)) )
>                     ={ Refl }=
>                       ( MkSimpleProb ((a, 1) :: Nil) (sumMapSndSingletonLemma a 1) )
>                     ={ Refl }=
>                       ( ret a )
>                     QED
> {-
> normalizeRetLemma a = s9 where
>   s1 : normalize (ret a) = normalize (MkSimpleProb ((a, 1) :: Nil) (sumMapSndSingletonLemma a 1))
>   s1 = Refl
>   s2 : normalize (MkSimpleProb ((a, 1) :: Nil) (sumMapSndSingletonLemma a 1))
>        =
>        MkSimpleProb (discardBySndZero ((a, 1) :: Nil))
>                     (trans (discardBySndZeroLemma ((a, 1) :: Nil)) (sumMapSndSingletonLemma a 1))
>   s2 = Refl
>   s3 : discardBySndZero ((a, 1) :: Nil) = (a, 1) :: Nil
>   s3 = discardBySndZeroLemma1 a 1 ?oneNotZero
>   s4 : discardBySndZeroLemma ((a, 1) :: Nil) = Refl {} {} {}
>   s4 = ?lika
>   s5 : MkSimpleProb (discardBySndZero ((a, 1) :: Nil))
>                     (trans (discardBySndZeroLemma ((a, 1) :: Nil)) (sumMapSndSingletonLemma a 1))
>        =
>        MkSimpleProb ((a, 1) :: Nil) (trans Refl (sumMapSndSingletonLemma a 1))
>   s5 = ?leka
>   s6 : MkSimpleProb ((a, 1) :: Nil) (trans Refl (sumMapSndSingletonLemma a 1))
>        =
>        MkSimpleProb ((a, 1) :: Nil) (sumMapSndSingletonLemma a 1)
>   s6 = Refl
>   s7 : MkSimpleProb ((a, 1) :: Nil) (sumMapSndSingletonLemma a 1) = ret a
>   s7 = Refl
>   s9 : normalize (ret a) = ret a
>   s9 = trans s1 (trans s2 (trans s5 (trans s6 s7)))
> -}

> |||
> supportRetLemma : {A : Type} ->
>                   (a : A) -> support (SimpleProb.MonadicOperations.ret a) = List.Operations.ret a
> supportRetLemma a = ( support (SimpleProb.MonadicOperations.ret a) )
>                   ={ Refl }=
>                     ( map fst (toList (normalize (SimpleProb.MonadicOperations.ret a))) )
>                   ={ cong {f = \ X => map Prelude.Basics.fst (toList X)} (normalizeRetLemma a) }=
>                     ( map fst (toList (SimpleProb.MonadicOperations.ret a)) )
>                   ={ Refl }=
>                     ( map fst (toList (MkSimpleProb ((a, 1) :: Nil) (sumMapSndSingletonLemma a 1))) )
>                   ={ Refl }=
>                     ( map fst ((a, 1) :: Nil) )
>                   ={ Refl }=
>                     ( a :: Nil )
>                   ={ Refl }=
>                     ( List.Operations.ret a )
>                   QED

* |SimpleProb| is a container monad:

> |||
> elemNonEmptySpec0 : {A : Type} ->
>                     (a : A) -> (sp : SimpleProb A) ->
>                     a `Elem` sp -> SimpleProb.MonadicOperations.NonEmpty sp
> elemNonEmptySpec0 {A} a sp aesp = List.Properties.elemNonEmptySpec0 a (support sp) aesp

> |||
> elemNonEmptySpec1 : {A : Type} ->
>                     (sp : SimpleProb A) ->
>                     SimpleProb.MonadicOperations.NonEmpty sp -> Sigma A (\ a => a `Elem` sp)
> elemNonEmptySpec1 {A} sp nesp = List.Properties.elemNonEmptySpec1 (support sp) nesp

> |||
> containerMonadSpec1 : {A : Type} -> {a : A} -> a `SimpleProb.MonadicOperations.Elem` (ret a)
> containerMonadSpec1 {A} {a} = s3 where
>   s1 : a `Data.List.Elem` (List.Operations.ret a)
>   s1 = List.Properties.containerMonadSpec1
>   s2 : a `Data.List.Elem` (support (SimpleProb.MonadicOperations.ret a))
>   s2 = replace {P = \ X => a `Data.List.Elem` X} (sym (supportRetLemma a)) s1
>   s3 : a `SimpleProb.MonadicOperations.Elem` (ret a)
>   s3 = s2

> |||
> containerMonadSpec3 : {A : Type} -> {P : A -> Type} ->
>                       (a : A) -> (sp : SimpleProb A) ->
>                       All P sp -> a `Elem` sp -> P a
> containerMonadSpec3 {A} {P} a sp allp elemp = List.Properties.containerMonadSpec3 a (support sp) allp elemp

* Specific container monad properties

> |||
> uniqueAllLemma : {A : Type} -> {P : A -> Type} ->
>                  Unique1 P -> (sp : SimpleProb A) -> Unique (All P sp)
> uniqueAllLemma u1P sp = List.Properties.uniqueAllLemma u1P (support sp)

> |||
> finiteAll : {A : Type} -> {P : A -> Type} ->
>             Finite1 P -> (sp : SimpleProb A) -> Finite (All P sp)
> finiteAll f1P sp = List.Properties.finiteAll f1P (support sp)

> ||| All is decidable
> decidableAll : {A : Type} -> {P : A -> Type} ->
>                (dec : (a : A) -> Dec (P a)) -> (sp : SimpleProb A) -> Dec (All P sp)
> decidableAll dec sp = List.Properties.decidableAll dec (support sp)

> ||| NotEmpty is finite
> finiteNonEmpty : {A : Type} -> (sp : SimpleProb A) -> Finite (SimpleProb.MonadicOperations.NonEmpty sp)
> finiteNonEmpty sp = List.Properties.finiteNonEmpty (support sp)

> ||| NotEmpty is decidable
> decidableNonEmpty : {A : Type} -> (sp : SimpleProb A) -> Dec (SimpleProb.MonadicOperations.NonEmpty sp)
> decidableNonEmpty sp = List.Properties.decidableNonEmpty (support sp)

* |SimpleProb|s are never empty

> |||
> nonEmptyLemma1 : {A : Type} -> (sp : SimpleProb A) -> List.Operations.NonEmpty (toList sp)
> nonEmptyLemma1 {A} (MkSimpleProb Nil s1p) = void s9 where
>   s1 : sumMapSnd {A = A} {B = NonNegRational} Nil = 0
>   s1 = sumMapSndNilLemma {A = A} {B = NonNegRational}
>   s2 : sumMapSnd {A = A} {B = NonNegRational} Nil = 1
>   s2 = s1p
>   s3 : (=) {A = NonNegRational} {B = NonNegRational} 1 0
>   s3 = trans (sym s2) s1
>   s9 : Void
>   s9 = not1Eq0 s3
> nonEmptyLemma1 (MkSimpleProb (ap :: aps) s1p) = ()

> |||
> nonEmptyLemma : {A : Type} -> (sp : SimpleProb A) -> NonEmpty sp
> nonEmptyLemma {A} sp = s4 where
>   s1 : List.Operations.NonEmpty (toList (normalize sp))
>   s1 = nonEmptyLemma1 (normalize sp)
>   s2 : List.Operations.NonEmpty (map fst (toList (normalize sp)))
>   s2 = mapPreservesNonEmpty fst (toList (normalize sp)) s1
>   s3 : List.Operations.NonEmpty (support sp)
>   s3 = s2
>   s4 : NonEmpty sp
>   s4 = s3

> |||
> toListFmapLemma : {A, B : Type} ->
>                   (f : A -> B) -> (sp : SimpleProb A) ->
>                   toList (fmap f sp) = fmap (cross f id) (toList sp)
> toListFmapLemma f (MkSimpleProb aps s1p) =
>     ( toList (fmap f (MkSimpleProb aps s1p)) )
>   ={ Refl }=
>     ( toList (MkSimpleProb
>               (fmap (cross f id) aps)
>               (trans Refl (trans (cong (mapSndMapCrossAnyIdLemma f aps)) s1p))) )
>   ={ Refl }=
>     ( fmap (cross f id) aps )
>   ={ Refl }=
>     ( fmap (cross f id) (toList (MkSimpleProb aps s1p)) )
>   QED

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Control.Monad.Id

%default total
%access public export

data Id : (a : Type)-> Type where
  IdF : (x : a) -> Id a

implementation Functor Id where
  map f (IdF a) = IdF (f a)

implementation Applicative Id where
    pure a = IdF a
    (IdF f) <*> (IdF a) = IdF $ f a

implementation Monad Id where
  (IdF x) >>= f = f x

implementation (Show a)=>Show (Id a) where
  show (IdF a) = show a

max_stars_repo_name: idris-industry/idris-free

max_issues_repo_name: idris-industry/idris-free

max_forks_repo_name: idris-industry/idris-free


text:
module Part2.Sec6_1_1_tyfunc
import Data.Vect

{-
Fewer concept == smaller conceptual complexity
type aliasing is simply a type level function!!!
-}

||| Type level function with no params
Position : Type
Position = (Double, Double)

testData : List (Double, Double)
testData = [(1,2),(1,3.1)]

testData' : List Position
testData' = [(1,2),(1,3.1)]

||| Naive test function
sumFirst : List Position -> Double
sumFirst list = sum (map fst list)

||| Type level function with one param
Polygon : Nat -> Type
Polygon n = Vect n Position

tri : Polygon 3
tri = [(0.0, 0.0), (3.0, 0.0), (0.0, 4.0)]

||| One param function acting as type synomym
MyList : Type -> Type
MyList = List

testMyList : MyList Integer -> MyList Integer
testMyList = map (+1)

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
import Data.Fin

data PowerSource = Petrol | Pedal

||| Vehicle here is a function from PowerSource to a type
data Vehicle : PowerSource -> Type where
  Bycicle : Vehicle Pedal
  Car : (fuel : Nat) -> Vehicle Petrol
  Bus : (fuel : Nat) -> Vehicle Petrol

wheels : Vehicle power -> Nat
wheels Bycicle = 2
wheels (Car fuel) = 4
wheels (Bus fuel) = 4

refuel : Vehicle Petrol -> Vehicle Petrol
refuel (Car fuel) = Car 100
refuel (Bus fuel) = Car 200
refuel Bycicle impossible

||| After looking into the definition of `integerToFin` in
||| https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/Fin.idr
||| it seems that my original approach wasn't that far off, but maybe...
integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
integerToFin x Z = Nothing
integerToFin x n = if x >= 0 then natToFin (cast x) n else Nothing

integerToFin' : Integer -> (n : Nat) -> Maybe (Fin n)
integerToFin' x Z = Nothing
integerToFin' x n  = case compare (cast x) n of
                          GT => Nothing
                          EQ => Nothing
                          -- LT => Just (the (Fin n) (cast x))
                          -- what's the way?

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
module Dollar

infixr 1 $
($) : Int -> Int -> Int
($) u x = x + 1

f : Int -> Int
f x = x $ 5

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Control.Applicative.Indexed

import Control.Functor.Indexed

infixl 3 <<*>>, <<*, *>>

public export
interface IndexedFunctor z z f => IndexedApplicative z f | f where
  total
  pure : {0 i : z} -> (x : a) -> f a i i

  total
  ap : {0 i,j,k : z} -> f (a -> b) i j -> f a j k -> f b i k

public export
(<<*>>) : IndexedApplicative z f => f (a -> b) i j -> f a j k -> f b i k
(<<*>>) = ap

public export
(<<*) : IndexedApplicative z f => f a i j -> f b j k -> f a i k
x <<* y = map const x <<*>> y

public export
(*>>) : IndexedApplicative z f => f a i j -> f b j k -> f b i k
x *>> y = map (const id) x <<*>> y

||| Conditionally execute an applicative expression when the boolean is true.
public export
when : IndexedApplicative z f => Bool -> Lazy (f () i i) -> f () i i
when True y  = y
when False y = pure ()

||| Execute an applicative expression unless the boolean is true.
%inline
public export
unless : IndexedApplicative z f => Bool -> Lazy (f () i i) -> f () i i
unless = when . not

||| Map each element of a structure to a computation, evaluate those
||| computations and discard the results.
public export
traverse_ : (Foldable t, IndexedApplicative z f) => (a -> f b i i) -> t a -> f () i i
traverse_ f = foldr ((*>>) . f) (pure ())

||| Evaluate each computation in a structure and discard the results.
public export
sequence_ : (Foldable t, IndexedApplicative z f) => t (f a i i) -> f () i i
sequence_ = foldr (*>>) (pure ())

||| Like `traverse_` but with the arguments flipped.
public export
for_ : (Foldable t, IndexedApplicative z f) => t a -> (a -> f b i i) -> f () i i
for_ = flip traverse_

max_stars_repo_name: mattpolzin/idris-indexed

max_issues_repo_name: mattpolzin/idris-indexed

max_forks_repo_name: mattpolzin/idris-indexed


text:
module Control.Eff.Choose

import Control.Eff.Internal

%default total

public export
data Choose : (a : Type) -> Type where
  Empty : Choose a
  Alt   : (lft, rgt : a) -> Choose a

export %inline
empty : Has Choose fs => Eff fs a
empty = send Empty

export %inline
alt : Has Choose fs => Eff fs a -> Eff fs a -> Eff fs a
alt x y = join $ send (Alt x y)

export %inline
guard : Has Choose fs => Bool -> Eff fs ()
guard False = empty
guard True  = pure ()

--------------------------------------------------------------------------------
--          Running Choose
--------------------------------------------------------------------------------

export
runChoose : Alternative f => Has Choose fs => Eff fs a -> Eff (fs - Choose) (f a)
runChoose fr = case toView fr of
  Pure val => pure (pure val)
  Bind x g => case handle (id {a = Choose _}) x of
    Left y  => assert_total $ lift y >>= runChoose . g
    Right Empty         => pure empty
    Right (Alt lft rgt) => assert_total $ do
      x <- runChoose (g lft)
      y <- runChoose (g rgt)
      pure (x <|> y)


text:
main : IO ()
main = putStrLn ?greeting

even : Nat -> Bool
even Z = True
even (S k) = ?even_rhs


text:
module Data.Array16Spec

import Data.Array16
import Data.List
import Data.String
import Hedgehog

export
Show a => Show (Array16 a) where
    showPrec prec arr = showCon prec "MkA16" $ fastConcat $ intersperse " "
        $ foldr (\elem, acc => showPrec App elem :: acc) [] arr

export
array16Gen : Gen a -> Gen (Array16 a)
array16Gen gen = [| MkA16 gen gen gen gen gen gen gen gen gen gen gen gen gen gen gen gen |]

propFoldable : Property
propFoldable = property $ do
    arr <- forAll $ array16Gen $ int $ linear (-100) 100
    null arr === False

export
specArray16 : IO Bool
specArray16 =
    checkGroup $ MkGroup "Array16"
        [ ("Foldable", propFoldable)
        ]


text:
import Data.Vect
import Data.Fin

matrix : Nat -> Nat -> Type -> Type
matrix k j x = Vect k (Vect j x)

addV : Num a => Vect n a -> Vect n a -> Vect n a
addV [] [] = []
addV (x :: xs) (y :: ys) = (x + y) :: (addV xs ys)

dot : Num a => Vect n a -> Vect n a -> a
dot [] [] = 0
dot (x :: xs) (y :: ys) = (x * y) + (dot xs ys)

add : Num a => matrix n m a -> matrix n m a -> matrix n m a
add [] [] = []
add (x :: xs) (y :: ys) = (addV x y) :: (add xs ys)

row : Fin n -> matrix n m a -> Vect m a
row = index

col : Fin m -> matrix n m a -> Vect n a
col x y = map (index x) y

promote : Fin n -> Fin (n + m)
promote FZ = FZ
promote (FS x) = FS (promote x)

inject : Fin n -> Fin (S n)
inject FZ = FZ
inject (FS x) = FS (inject x)

listFins : (n : Nat) -> Vect n (Fin n)
listFins Z = []
listFins (S k) = FZ :: (map FS (listFins k))

squareMatrix : Nat -> Type -> Type
squareMatrix n = matrix n n

det : Num a => squareMatrix n a -> a
det {n} x = sum $ map thing (listFins n)
    where thing ix = dot (row ix x) (col ix x)

max_stars_repo_name: clarissalittler/idris-practice

max_issues_repo_name: clarissalittler/idris-practice

max_forks_repo_name: clarissalittler/idris-practice


text:
module Language.LSP.Message.ClientCapabilities

import Language.JSON
import Language.LSP.Message.CallHierarchy
import Language.LSP.Message.Cancel
import Language.LSP.Message.CodeAction
import Language.LSP.Message.CodeLens
import Language.LSP.Message.Command
import Language.LSP.Message.Completion
import Language.LSP.Message.Declaration
import Language.LSP.Message.Definition
import Language.LSP.Message.Derive
import Language.LSP.Message.Diagnostics
import Language.LSP.Message.DocumentColor
import Language.LSP.Message.DocumentFormatting
import Language.LSP.Message.DocumentHighlight
import Language.LSP.Message.DocumentLink
import Language.LSP.Message.DocumentSymbols
import Language.LSP.Message.FoldingRange
import Language.LSP.Message.Hover
import Language.LSP.Message.Implementation
import Language.LSP.Message.LinkedEditingRange
import Language.LSP.Message.Location
import Language.LSP.Message.Markup
import Language.LSP.Message.Method
import Language.LSP.Message.Moniker
import Language.LSP.Message.Progress
import Language.LSP.Message.References
import Language.LSP.Message.Registration
import Language.LSP.Message.RegularExpressions
import Language.LSP.Message.Rename
import Language.LSP.Message.SelectionRange
import Language.LSP.Message.SemanticTokens
import Language.LSP.Message.SignatureHelp
import Language.LSP.Message.TextDocument
import Language.LSP.Message.Trace
import Language.LSP.Message.Utils
import Language.LSP.Message.Window
import Language.LSP.Message.Workspace
import Language.Reflection

%language ElabReflection
%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
public export
record TextDocumentClientCapabilities where
  constructor MkTextDocumentClientCapabilities
  synchronization    : Maybe TextDocumentSyncClientCapabilities
  completion         : Maybe CompletionClientCapabilities
  hover              : Maybe HoverClientCapabilities
  signatureHelp      : Maybe SignatureHelpClientCapabilities
  declaration        : Maybe DeclarationClientCapabilities
  definition         : Maybe DefinitionClientCapabilities
  typeDefinition     : Maybe TypeDefinitionClientCapabilities
  implementation_    : Maybe ImplementationClientCapabilities
  references         : Maybe ReferenceClientCapabilities
  documentHighlight  : Maybe DocumentHighlightClientCapabilities
  documentSymbol     : Maybe DocumentSymbolClientCapabilities
  codeAction         : Maybe CodeActionClientCapabilities
  codeLens           : Maybe CodeLensClientCapabilities
  documentLink       : Maybe DocumentLinkClientCapabilities
  colorProvider      : Maybe DocumentColorClientCapabilities
  formatting         : Maybe DocumentFormattingClientCapabilities
  rangeFormatting    : Maybe DocumentRangeFormattingClientCapabilities
  onTypeFormatting   : Maybe DocumentOnTypeFormattingClientCapabilities
  rename             : Maybe RenameClientCapabilities
  publishDiagnostics : Maybe PublishDiagnosticsClientCapabilities
  foldingRange       : Maybe FoldingRangeClientCapabilities
  selectionRange     : Maybe SelectionRangeClientCapabilities
  linkedEditingRange : Maybe LinkedEditingRangeClientCapabilities
  callHierarchy      : Maybe CallHierarchyClientCapabilities
  semanticTokens     : Maybe SemanticTokensClientCapabilities
  moniker            : Maybe MonikerClientCapabilities
%runElab deriveJSON ({renames := [("implementation_", "implementation")]} defaultOpts) `{TextDocumentClientCapabilities}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
public export
record FileOperationsWorkspaceClientCapabilities where
  constructor MkFileOperationsWorkspaceClientCapabilities
  dynamicRegistration : Maybe Bool
  didCreate           : Maybe Bool
  willCreate          : Maybe Bool
  didRename           : Maybe Bool
  willRename          : Maybe Bool
  didDelete           : Maybe Bool
  willDelete          : Maybe Bool
%runElab deriveJSON defaultOpts `{FileOperationsWorkspaceClientCapabilities}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
public export
record WorkspaceClientCapabilities where
  constructor MkWorkspaceClientCapabilities
  applyEdit              : Maybe Bool
  workspaceEdit          : Maybe WorkspaceEditClientCapabilities
  didChangeConfiguration : Maybe DidChangeConfigurationClientCapabilities
  didChangeWatchedFiles  : Maybe DidChangeWatchedFilesClientCapabilities
  symbol                 : Maybe WorkspaceSymbolClientCapabilities
  executeCommand         : Maybe ExecuteCommandClientCapabilities
  workspaceFolders       : Maybe Bool
  configuration          : Maybe Bool
  semanticTokens         : Maybe SemanticTokensWorkspaceClientCapabilities
  codeLens               : Maybe CodeLensWorkspaceClientCapabilities
  fileOperations         : Maybe FileOperationsWorkspaceClientCapabilities
%runElab deriveJSON defaultOpts `{WorkspaceClientCapabilities}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
public export
record WindowClientCapabilities where
  constructor MkWindowClientCapabilities
  workDoneProgress : Maybe Bool
  showMessage      : Maybe ShowMessageRequestClientCapabilities
  showDocument     : Maybe ShowDocumentClientCapabilities
%runElab deriveJSON defaultOpts `{WindowClientCapabilities}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
public export
record GeneralClientCapabilities where
  constructor MkGeneralClientCapabilities
  regularExpressions : Maybe RegularExpressionsClientCapabilities
  markdown           : Maybe MarkdownClientCapabilities
%runElab deriveJSON defaultOpts `{GeneralClientCapabilities}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
public export
record ClientCapabilities where
  constructor MkClientCapabilities
  workspace    : Maybe WorkspaceClientCapabilities
  textDocument : Maybe TextDocumentClientCapabilities
  window       : Maybe WindowClientCapabilities
  general      : Maybe GeneralClientCapabilities
  experimental : Maybe JSON
%runElab deriveJSON defaultOpts `{ClientCapabilities}


text:
module Compiler.Erlang.Codegen.ErlExprToAbstractFormat.Internal

import Compiler.Erlang.IR.AbstractFormat

%default total

export
genFunCall : Line -> String -> String -> List Expr -> Expr
genFunCall l modName fnName args =
  AEFunCall l (AERemoteRef l (AELiteral (ALAtom l modName)) (AELiteral (ALAtom l fnName))) args

export
genDataCtorExpr : Line -> (name : String) -> List Expr -> Expr
genDataCtorExpr l name exprs =
  AETuple l (AELiteral (ALAtom l name) :: exprs)

export
genStringLiteralExpr : Line -> String -> Expr
genStringLiteralExpr l str =
  AEBitstring l [MkBitSegment l (AELiteral (ALCharlist l str)) ABSDefault ABUtf8]

export
genStringLiteralPattern : Line -> String -> Pattern
genStringLiteralPattern l str =
  APBitstring l [MkBitSegment l (ABPCharlist l str) ABSDefault ABUtf8]


text:
module Algebra.Solver.Semiring

import public Algebra.Semiring
import public Algebra.Solver.Semiring.Expr
import public Algebra.Solver.Semiring.Prod
import public Algebra.Solver.Semiring.SolvableSemiring
import public Algebra.Solver.Semiring.Sum

%default total


text:
module ExampleDetectableErrors

import Data.Nat
import Data.Vect
import Data.List
import LinearTypes
import Control.Linear.LIO
import Unitary
import QStateT
import System.Random
import Injection
import Complex
import QuantumOp
import Examples

-------------------------------------- Impossible Unitaries ---------------------------------------
-- In this example, we try to apply a Hadamard gate on a non-existing wire (index 4 on a gate of size 3)

brokenH : Unitary 3
--brokenH = H 4 toffoli

-- Error: While processing right hand side of brokenH. Can't find an implementation for == (compare 4 3) LT = True.

-- In this example, we try to apply the control and the target of a CNOT on the same wire

brokenCNOT : Unitary 2
--brokenCNOT = CNOT 1 1 IdGate

-- Error: While processing right hand side of brokenCNOT. Can't find an implementation for not (== 1 1) = True.

-- In this example, we try to apply a circuit on a non existing wire (index 4 on a gate of size 3)

brokenApply1 : Unitary 3
--brokenApply1 = apply toBellBasis toffoli [1,4]

-- Error: While processing right hand side of brokenApply1. Can't find an implementation for allSmaller [1, 4] 3 && Delay (allDifferent [1, 4]) = True.

-- In this example, we try to apply a circuit twice on the same wire

brokenApply2 : Unitary 3
--brokenApply2 = apply toffoli IdGate [1,2,1]

-- Error: While processing right hand side of brokenApply2. Can't find an implementation for allSmaller [1, 2, 1] 3 && Delay (allDifferent [1, 2,1]) = True.

--------------------------------- BROKEN QUANTUM STATE OPERATIONS ---------------------------------

-- In this example, wew try to reuse a qubit that has be measured

brokenOp1 : IO (Vect 4 Bool)
{-brokenOp1  =
  run (do
      [q1,q2,q3,q4] <- newQubits {t = SimulatedOp} 4
      [b3] <- measure [q3]
      [r4,r3,r1] <- applyUnitary [q4,q3,q1] (X 0 IdGate) --trying to reuse q3
      [b1,b4,b2] <- measure [r1,r4,q2]
      pure ([b1,b2,b3,b4])
      )
      -}
-- Error: While processing right hand side of brokenOp1. q3 is not accessible in this context.

-- In this example, we try to copy a qubit

brokenOp2 : IO (Vect 5 Bool)
{-brokenOp2 =
  run (do
      [q1,q2,q3,q4] <- newQubits {t = SimulatedOp} 4
      [b3] <- measure [q3]
      [q4,q1,q5] <- applyUnitary [q4,q1,q4] (X 0 IdGate) --trying to copy q4
      [b1,b2,b5] <- measure [q1,q2,q5]
      pure [b1,b2,b3,b5,b5]
      )
      -}
--Error : While processing right hand side of brokenOp2. There are 2 uses of linear name q4.

-- In this example, we try to reuse a pointer to an old state of a qubit (the state of the qubit has been modified)

brokenOp3 : IO (Vect 4 Bool)
{-brokenOp3  =
  run (do
      [q1,q2,q3,q4] <- newQubits {t = SimulatedOp} 4
      [b3] <- measure [q3]
      [r4,r2,r1] <- applyUnitary [q4,q2,q1] (X 0 IdGate)
      [b1,b4,b2] <- measure [r1,r4,q2] --trying to reuse the name q2
      pure ([b1,b2,b3,b4])
      )
      -}
--Error: While processing right hand side of brokenOp2. q2 is not accessible in this context.

max_stars_repo_name: zamdzhiev/Qimaera

max_issues_repo_name: zamdzhiev/Qimaera

max_forks_repo_name: zamdzhiev/Qimaera


text:
module Twist.Rotation

import Control.Algebra

import Twist.Cycle
import Twist.Face
import Twist.Util

%default total
%access export

data Rotation : (f : Type) -> (c : Type) -> (face : f) -> Type where
  Rot : (face : (Face (S k))) -> (c : Cycle (S j)) -> Rotation (Face (S k)) (Cycle (S j)) face

Eq c => Eq (Rotation f c face) where
  (Rot face cx) == (Rot face cy) = cx == cy

Show (Rotation f c face) where
  show (Rot face x) = show face ++ show x

cw : (Rotation f c face) -> (Rotation f c face)
cw (Rot face cx) = Rot face (next cx)

ccw : (Rotation f c face) -> (Rotation f c face)
ccw (Rot face cx) = Rot face (prev cx)

Semigroup (Rotation f c face) where
  (Rot face cx) <+> (Rot face cy) = Rot face (cx <+> cy)

rotateZ : (face : Face (S k)) -> Rotation (Face (S k)) (Cycle (S j)) face
rotateZ x = Rot x neutral

rotate : (face : Face (S k)) -> Rotation (Face (S k)) (Cycle (S j)) face
rotate x = Rot x (next neutral)

rotate' : (face : Face (S k)) -> Rotation (Face (S k)) (Cycle (S j)) face
rotate' x = Rot x (prev neutral)

Monoid (Rotation (Face (S k)) (Cycle (S j)) face) where
  neutral = Rot face neutral

Group (Rotation (Face (S k)) (Cycle (S j)) face) where
  inverse (Rot face cx) = Rot face (inverse cx)

max_stars_repo_name: msmorgan/idris-twist

max_issues_repo_name: msmorgan/idris-twist

max_forks_repo_name: msmorgan/idris-twist


text:
module Network.Curl.Types.CurlMCode

import  Network.Curl.Types.Code

import Util

import Derive.Enum
%language ElabReflection

public export
data CurlMCode
  = CURLM_CALL_MULTI_PERFORM -- -1  /* please call curl_multi_perform() or
                                  -- curl_multi_socket*() soon */
  | CURLM_OK
  | CURLM_BAD_HANDLE      -- /* the passed-in handle is not a valid CURLM handle */
  | CURLM_BAD_EASY_HANDLE -- /* an easy handle was not good/valid */
  | CURLM_OUT_OF_MEMORY   -- /* if you ever get this, you're in deep sh*t */
  | CURLM_INTERNAL_ERROR  -- /* this is a libcurl bug */
  | CURLM_BAD_SOCKET      -- /* the passed in socket argument did not match */
  | CURLM_UNKNOWN_OPTION  -- /* curl_multi_setopt() with unsupported option */
  | CURLM_ADDED_ALREADY   -- /* an easy handle already added to a multi handle was
                             -- attempted to get added - again */
  | CURLM_RECURSIVE_API_CALL -- /* an api function was called from inside a
                          --   callback */
  | CURLM_WAKEUP_FAILURE  -- /* wakeup is unavailable or failed */
  | CURLM_BAD_FUNCTION_ARGUMENT  -- /* function called with a bad parameter */
  | CURLM_LAST

export
Show CurlMCode where
  show = showEnum

export
Eq CurlMCode where
  (==) = eqEnum

export
Ord CurlMCode where
  compare = compareEnum

curlMCodeEnumList : List Int
curlMCodeEnumList = [(-1)] ++ [0..11]

export
ToCode CurlMCode where
  toCode = enumTo curlMCodeEnumList

export
FromCode CurlMCode where
  unsafeFromCode = unsafeEnumFrom curlMCodeEnumList
  fromCode = enumFrom curlMCodeEnumList


text:
import Data.Vect

exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength {m} len input = case decEq m len of
                                 Yes Refl => Just input
                                 No contra => Nothing


text:
> module Fraction.BasicProperties

> import Syntax.PreorderReasoning

> import Fraction.Fraction
> import Fraction.BasicOperations
> import Fraction.Normal
> import Nat.LTProperties
> import PNat.PNat
> import PNat.Operations
> import PNat.Properties
> import Nat.Positive
> import Basic.Operations
> import Nat.Coprime
> import Nat.CoprimeProperties
> import Nat.OperationsProperties

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

Properties of |num|, |den|, |fromNat|:

> ||| Denominators of fractions are greater than zero
> denLTLemma : (x : Fraction) -> Z `LT` den x
> denLTLemma x = s2 where
>   s1 : Z `LT` toNat (snd x)
>   s1 = toNatLTLemma (snd x)
>   s2 : Z `LT` den x
>   s2 = replace {P = \ ZUZU => Z `LT` ZUZU} Refl s1

> |||
> fromNatNormal : {n : Nat} -> Normal (fromNat n)
> fromNatNormal = MkNormal anyCoprimeOne

> {-
> ||| Fraction is an instance of Show
> instance Show Fraction where
>   show q = show (num q) ++ "/" ++ show (den q)
> -}

> ||| Fraction is an instance of Num
> implementation Num Fraction where
>   (+) = plus
>   (*) = mult
>   fromInteger = fromNat . fromIntegerNat

Properties of |plus|:

> ||| Addition is commutative
> plusCommutative : (x : Fraction) -> (y : Fraction) -> x + y = y + x
> plusCommutative (m, d') (n, e') =
>   let d = toNat d' in
>   let e = toNat e' in
>     ( (m, d') + (n, e') )
>   ={ Refl }=
>     ( (m * e + n * d, d' * e') )
>   ={ cong2 (plusCommutative (m * e) (n * d)) (multCommutative d' e') }=
>     ( (n * d + m * e, e' * d') )
>   ={ Refl }=
>     ( (n, e') + (m, d') )
>   QED

> ||| 0 is neutral element of addition
> plusZeroRightNeutral : (x : Fraction) -> x + 0 = x
> plusZeroRightNeutral (n, d') =
>   let d = toNat d' in
>     ( (n, d') + 0 )
>   ={ Refl }=
>     ( (n, d') + fromNat (fromIntegerNat 0) )
>   ={ Refl }=
>     ( (n, d') + fromNat 0 )
>   ={ Refl }=
>     ( (n, d') + (0, Element 1 MkPositive) )
>   ={ Refl }=
>     ( (n * 1 + 0 * d, d' * (Element 1 MkPositive)) )
>   ={ cong2 (multOneRightNeutralPlusMultZeroLeftZero n d) (multOneRightNeutral d') }=
>     ( (n, d') )
>   QED

> ||| 0 is neutral element of addition
> plusZeroLeftNeutral  : (x : Fraction) -> 0 + x = x
> plusZeroLeftNeutral x =
>     ( 0 + x )
>   ={ plusCommutative 0 x }=
>     ( x + 0 )
>   ={ plusZeroRightNeutral x }=
>     ( x )
>   QED

> ||| Addition is associative
> plusAssociative : (x : Fraction) -> (y : Fraction) -> (z : Fraction) -> x + (y + z) = (x + y) + z
> plusAssociative (m, d') (n, e') (o, f') =
>   let d = toNat d' in
>   let e = toNat e' in
>   let f = toNat f' in
>     ( (m, d') + ((n, e') + (o, f')) )
>   ={ Refl }=
>     ( (m, d') + (n * f + o * e, e' * f') )
>   ={ Refl }=
>     ( (m * (toNat (e' * f')) + (n * f + o * e) * d, d' * (e' * f')) )
>   ={ cong {f = \ ZUZU => (m * (ZUZU) + (n * f + o * e) * d, d' * (e' * f'))}
>           toNatMultLemma }=
>     ( (m * (e * f) + (n * f + o * e) * d, d' * (e' * f')) )
>   ={ cong {f = \ ZUZU => (m * (e * f) + ZUZU, d' * (e' * f'))}
>           (multDistributesOverPlusLeft (n * f) (o * e) d) }=
>     ( (m * (e * f) + ((n * f) * d + (o * e) * d), d' * (e' * f')) )
>   ={ cong {f = \ ZUZU => (ZUZU, d' * (e' * f'))}
>           (plusAssociative (m * (e * f)) ((n * f) * d) ((o * e) * d)) }=
>     ( ((m * (e * f) + (n * f) * d) + (o * e) * d, d' * (e' * f')) )
>   ={ cong {f = \ ZUZU => ((ZUZU + (n * f) * d) + (o * e) * d, d' * (e' * f'))}
>           (multAssociative m e f) }=
>     ( (((m * e) * f + (n * f) * d) + (o * e) * d, d' * (e' * f')) )
>   ={ cong {f = \ ZUZU => (((m * e) * f + ZUZU) + (o * e) * d, d' * (e' * f'))}
>           (sym (multAssociative n f d)) }=
>     ( (((m * e) * f + n * (f * d)) + (o * e) * d, d' * (e' * f')) )
>   ={ cong {f = \ ZUZU => (((m * e) * f + n * (ZUZU)) + (o * e) * d, d' * (e' * f'))}
>           (multCommutative f d) }=
>     ( (((m * e) * f + n * (d * f)) + (o * e) * d, d' * (e' * f')) )
>   ={ cong {f = \ ZUZU => (((m * e) * f + ZUZU) + (o * e) * d, d' * (e' * f'))}
>           (multAssociative n d f) }=
>     ( (((m * e) * f + (n * d) * f) + (o * e) * d, d' * (e' * f')) )
>   ={ cong {f = \ ZUZU => (ZUZU + (o * e) * d, d' * (e' * f'))}
>           (sym (multDistributesOverPlusLeft (m * e) (n * d) f)) }=
>     ( ((m * e + n * d) * f + (o * e) * d, d' * (e' * f')) )
>   ={ cong {f = \ ZUZU => ((m * e + n * d) * f + ZUZU, d' * (e' * f'))}
>           (sym (multAssociative o e d)) }=
>     ( ((m * e + n * d) * f + o * (e * d), d' * (e' * f')) )
>   ={ cong {f = \ ZUZU => ((m * e + n * d) * f + o * (ZUZU), d' * (e' * f'))}
>           (multCommutative e d) }=
>     ( ((m * e + n * d) * f + o * (d * e), d' * (e' * f')) )
>   ={ cong {f = \ ZUZU => ((m * e + n * d) * f + o * (d * e), ZUZU)}
>           (multAssociative d' e' f')}=
>     ( ((m * e + n * d) * f + o * (d * e), (d' * e') * f') )
>   ={ cong {f = \ ZUZU => ((m * e + n * d) * f + o * (ZUZU), (d' * e') * f')}
>           (sym toNatMultLemma) }=
>     ( ((m * e + n * d) * f + o * (toNat (d' * e')), (d' * e') * f') )
>   ={ Refl }=
>     ( (m * e + n * d, d' * e') + (o, f') )
>   ={ Refl }=
>     ( ((m, d') + (n, e')) + (o, f') )
>   QED

Properties of |mult|:

> ||| Multiplication is commutative
> multCommutative : (x : Fraction) -> (y : Fraction) -> x * y = y * x
> multCommutative (m, d') (n, e') =
>     ( (m, d') * (n, e') )
>   ={ Refl }=
>     ( (m * n, d' * e') )
>   ={ cong2 (multCommutative m n) (multCommutative d' e') }=
>     ( (n * m, e' * d') )
>   ={ Refl }=
>     ( (n, e') * (m, d') )
>   QED

> ||| 1 is neutral element of multiplication
> multOneRightNeutral : (x : Fraction) -> x * 1 = x
> multOneRightNeutral (n, d') =
>   let d = toNat d' in
>     ( (n, d') * 1 )
>   ={ Refl }=
>     ( (n, d') * (fromNat (fromIntegerNat 1)) )
>   ={ Refl }=
>     ( (n, d') * (fromNat 1) )
>   ={ Refl }=
>     ( (n, d') * (1, Element 1 MkPositive) )
>   ={ Refl }=
>     ( (n * 1, d' * (Element 1 MkPositive)) )
>   ={ cong2 (multOneRightNeutral n) (multOneRightNeutral d') }=
>     ( (n, d') )
>   QED

> ||| 1 is neutral element of multiplication
> multOneLeftNeutral  : (x : Fraction) -> 1 * x = x
> multOneLeftNeutral x =
>     ( 1 * x )
>   ={ multCommutative 1 x }=
>     ( x * 1 )
>   ={ multOneRightNeutral x }=
>     ( x )
>   QED

> {-

> ---}


text:
module Derive.DecEq

import Data.Vect

import Language.Reflection.Elab
import Language.Reflection.Utils

import Derive.Kit
import Derive.Disjoint

decEqN : (tyn : TTName) -> TTName
decEqN tyn = SN $ MetaN tyn (UN "decEqImpl")

tyConArgName : TyConArg -> TTName
tyConArgName (Parameter n _) = n
tyConArgName (Index n _) = n

tyConArgTy : TyConArg -> Raw
tyConArgTy (Parameter _ t) = t
tyConArgTy (Index _ t) = t

tyConTy : List TyConArg -> Raw -> Raw
tyConTy [] res = res
tyConTy (Parameter n t :: args) res = RBind n (Pi t `(Type)) $ tyConTy args res
tyConTy (Index     n t :: args) res = RBind n (Pi t `(Type)) $ tyConTy args res

declareDecEq : TTName -> Datatype -> Elab ()
declareDecEq fn (MkDatatype tyn tyconArgs tyconRes cons) =
  do let tconT = tyConTy tyconArgs
     declareType $
       Declare fn
               [Implicit (tyConArgName arg) (tyConArgTy arg) | arg <- tyconArgs]
               `((x, y : ~(mkApp (Var tyn) (map (Var . tyConArgName) tyconArgs))) ->
                 Dec ((=) {A=~tyconRes} {B=~tyconRes} x y))

makeClause : TTName -> ((TTName, Raw), (TTName, Raw)) -> Elab (Maybe FunClause)
makeClause fn ((cn1, ct1), (cn2, ct2)) =
  if cn1 == cn2
    then pure Nothing
    else
      do (args1, res1) <- stealBindings ct1 (const Nothing)
         (args2, res2) <- stealBindings ct2 (const Nothing)
         let rhsGoal = bindPatTys (args1 ++ args2) $ RType --no
         pure Nothing

makeDecEqClauses : TTName -> List ((TTName, Raw), (TTName, Raw)) -> Elab (List FunClause)
makeDecEqClauses fn cases =
  do res <- traverse (makeClause fn) cases
     pure $ justs res
  where justs : List (Maybe a) -> List a
        justs [] = []
        justs (Nothing::xs) = justs xs
        justs (Just x :: xs) = x :: justs xs

deriveDecEq : (tyn : TTName) -> Elab ()
deriveDecEq tyn' =
  do MkDatatype tyn tyconArgs tyconRes cons <- lookupDatatypeExact tyn'
     mkDisjoint tyn
     let fn = (NS (UN "aaaaaa") ["DecEq", "Derive"]) --decEqN tyn
     declareDecEq fn (MkDatatype tyn tyconArgs tyconRes cons)
     defineFunction $ DefineFun fn !(makeDecEqClauses fn [(c1, c2) | c1 <- cons, c2 <- cons])

forEffect : ()
forEffect = %runElab (do deriveDecEq `{Vect}
                         trivial)

max_stars_repo_name: Garnasha/derive-all-the-instances

max_issues_repo_name: Garnasha/derive-all-the-instances

max_forks_repo_name: Garnasha/derive-all-the-instances


text:
module Common.Casts

import Common.Felt

-- Casts to Felt
%extern prim__cast_Int_to_Felt : Int -> Felt
public export %inline Cast Int Felt where cast = prim__cast_Int_to_Felt

%extern prim__cast_Int8_to_Felt : Int8 -> Felt
public export %inline Cast Int8 Felt where cast = prim__cast_Int8_to_Felt

%extern prim__cast_Int16_to_Felt : Int16 -> Felt
public export %inline Cast Int16 Felt where cast = prim__cast_Int16_to_Felt

%extern prim__cast_Int32_to_Felt : Int32 -> Felt
public export %inline Cast Int32 Felt where cast = prim__cast_Int32_to_Felt

%extern prim__cast_Int64_to_Felt : Int64 -> Felt
public export %inline Cast Int64 Felt where cast = prim__cast_Int64_to_Felt

%extern prim__cast_Bits8_to_Felt : Bits8 -> Felt
public export %inline Cast Bits8 Felt where cast = prim__cast_Bits8_to_Felt

%extern prim__cast_Bits16_to_Felt : Bits16 -> Felt
public export %inline Cast Bits16 Felt where cast = prim__cast_Bits16_to_Felt

%extern prim__cast_Bits32_to_Felt : Bits32 -> Felt
public export %inline Cast Bits32 Felt where cast = prim__cast_Bits32_to_Felt

%extern prim__cast_Bits64_to_Felt : Bits64 -> Felt
public export %inline Cast Bits64 Felt where cast = prim__cast_Bits64_to_Felt

-- Casts to Int
%extern prim__cast_Felt_to_Int : Felt -> Int
public export %inline Cast Felt Int where cast = prim__cast_Felt_to_Int

%extern prim__cast_Int8_to_Int : Int8 -> Int
public export %inline Cast Int8 Int where cast = prim__cast_Int8_to_Int

%extern prim__cast_Int16_to_Int : Int16 -> Int
public export %inline Cast Int16 Int where cast = prim__cast_Int16_to_Int

%extern prim__cast_Int32_to_Int : Int32 -> Int
public export %inline Cast Int32 Int where cast = prim__cast_Int32_to_Int

%extern prim__cast_Int64_to_Int : Int64 -> Int
public export %inline Cast Int64 Int where cast = prim__cast_Int64_to_Int

%extern prim__cast_Bits8_to_Int : Bits8 -> Int
public export %inline Cast Bits8 Int where cast = prim__cast_Bits8_to_Int

%extern prim__cast_Bits16_to_Int : Bits16 -> Int
public export %inline Cast Bits16 Int where cast = prim__cast_Bits16_to_Int

%extern prim__cast_Bits32_to_Int : Bits32 -> Int
public export %inline Cast Bits32 Int where cast = prim__cast_Bits32_to_Int

%extern prim__cast_Bits64_to_Int : Bits64 -> Int
public export %inline Cast Bits64 Int where cast = prim__cast_Bits64_to_Int

-- Casts to Int8
%extern prim__cast_Felt_to_Int8 : Felt -> Int8
public export %inline Cast Felt Int8 where cast = prim__cast_Felt_to_Int8

%extern prim__cast_Int_to_Int8 : Int -> Int8
public export %inline Cast Int Int8 where cast = prim__cast_Int_to_Int8

%extern prim__cast_Int16_to_Int8 : Int16 -> Int8
public export %inline Cast Int16 Int8 where cast = prim__cast_Int16_to_Int8

%extern prim__cast_Int32_to_Int8 : Int32 -> Int8
public export %inline Cast Int32 Int8 where cast = prim__cast_Int32_to_Int8

%extern prim__cast_Int64_to_Int8 : Int64 -> Int8
public export %inline Cast Int64 Int8 where cast = prim__cast_Int64_to_Int8

%extern prim__cast_Bits8_to_Int8 : Bits8 -> Int8
public export %inline Cast Bits8 Int8 where cast = prim__cast_Bits8_to_Int8

%extern prim__cast_Bits16_to_Int8 : Bits16 -> Int8
public export %inline Cast Bits16 Int8 where cast = prim__cast_Bits16_to_Int8

%extern prim__cast_Bits32_to_Int8 : Bits32 -> Int8
public export %inline Cast Bits32 Int8 where cast = prim__cast_Bits32_to_Int8

%extern prim__cast_Bits64_to_Int8 : Bits64 -> Int8
public export %inline Cast Bits64 Int8 where cast = prim__cast_Bits64_to_Int8

-- Casts to Int16
%extern prim__cast_Felt_to_Int16 : Felt -> Int16
public export %inline Cast Felt Int16 where cast = prim__cast_Felt_to_Int16

%extern prim__cast_Int_to_Int16 : Int -> Int16
public export %inline Cast Int Int16 where cast = prim__cast_Int_to_Int16

%extern prim__cast_Int8_to_Int16 : Int8 -> Int16
public export %inline Cast Int8 Int16 where cast = prim__cast_Int8_to_Int16

%extern prim__cast_Int32_to_Int16 : Int32 -> Int16
public export %inline Cast Int32 Int16 where cast = prim__cast_Int32_to_Int16

%extern prim__cast_Int64_to_Int16 : Int64 -> Int16
public export %inline Cast Int64 Int16  where cast = prim__cast_Int64_to_Int16

%extern prim__cast_Bits8_to_Int16 : Bits8 -> Int16
public export %inline Cast Bits8 Int16 where cast = prim__cast_Bits8_to_Int16

%extern prim__cast_Bits16_to_Int16 : Bits16 -> Int16
public export %inline Cast Bits16 Int16 where cast = prim__cast_Bits16_to_Int16

%extern prim__cast_Bits32_to_Int16 : Bits32 -> Int16
public export %inline Cast Bits32 Int16 where cast = prim__cast_Bits32_to_Int16

%extern prim__cast_Bits64_to_Int16 : Bits64 -> Int16
public export %inline Cast Bits64 Int16 where cast = prim__cast_Bits64_to_Int16

-- Casts to Int32
%extern prim__cast_Felt_to_Int32 : Felt -> Int32
public export %inline Cast Felt Int32 where cast = prim__cast_Felt_to_Int32

%extern prim__cast_Int_to_Int32 : Int -> Int32
public export %inline Cast Int Int32 where cast = prim__cast_Int_to_Int32

%extern prim__cast_Int8_to_Int32 : Int8 -> Int32
public export %inline Cast Int8 Int32 where cast = prim__cast_Int8_to_Int32

%extern prim__cast_Int16_to_Int32 : Int16 -> Int32
public export %inline Cast Int16 Int32 where cast = prim__cast_Int16_to_Int32

%extern prim__cast_Int64_to_Int32 : Int64 -> Int32
public export %inline Cast Int64 Int32 where cast = prim__cast_Int64_to_Int32

%extern prim__cast_Bits8_to_Int32 : Bits8 -> Int32
public export %inline Cast Bits8 Int32 where cast = prim__cast_Bits8_to_Int32

%extern prim__cast_Bits16_to_Int32 : Bits16 -> Int32
public export %inline Cast Bits16 Int32 where cast = prim__cast_Bits16_to_Int32

%extern prim__cast_Bits32_to_Int32 : Bits32 -> Int32
public export %inline Cast Bits32 Int32 where cast = prim__cast_Bits32_to_Int32

%extern prim__cast_Bits64_to_Int32 : Bits64 -> Int32
public export %inline Cast Bits64 Int32 where cast = prim__cast_Bits64_to_Int32

-- Casts to Int64
%extern prim__cast_Felt_to_Int64 : Felt -> Int64
public export %inline Cast Felt Int64 where cast = prim__cast_Felt_to_Int64

%extern prim__cast_Int_to_Int64 : Int -> Int64
public export %inline Cast Int Int64 where cast = prim__cast_Int_to_Int64

%extern prim__cast_Int8_to_Int64 : Int8 -> Int64
public export %inline Cast Int8 Int64 where cast = prim__cast_Int8_to_Int64

%extern prim__cast_Int16_to_Int64 : Int16 -> Int64
public export %inline Cast Int16 Int64 where cast = prim__cast_Int16_to_Int64

%extern prim__cast_Int32_to_Int64 : Int32 -> Int64
public export %inline Cast Int32 Int64 where cast = prim__cast_Int32_to_Int64

%extern prim__cast_Bits8_to_Int64 : Bits8 -> Int64
public export %inline Cast Bits8 Int64 where cast = prim__cast_Bits8_to_Int64

%extern prim__cast_Bits16_to_Int64 : Bits16 -> Int64
public export %inline Cast Bits16 Int64 where cast = prim__cast_Bits16_to_Int64

%extern prim__cast_Bits32_to_Int64 : Bits32 -> Int64
public export %inline Cast Bits32 Int64 where cast = prim__cast_Bits32_to_Int64

%extern prim__cast_Bits64_to_Int64 : Bits64 -> Int64
public export %inline Cast Bits64 Int64 where cast = prim__cast_Bits64_to_Int64

-- Casts to Bits8
%extern prim__cast_Felt_to_Bits8 : Felt -> Bits8
public export %inline Cast Felt Bits8 where cast = prim__cast_Felt_to_Bits8

%extern prim__cast_Int_to_Bits8 : Int -> Bits8
public export %inline Cast Int Bits8 where cast = prim__cast_Int_to_Bits8

%extern prim__cast_Int8_to_Bits8 : Int8 -> Bits8
public export %inline Cast Int8 Bits8 where cast = prim__cast_Int8_to_Bits8

%extern prim__cast_Int16_to_Bits8 : Int16 -> Bits8
public export %inline Cast Int16 Bits8 where cast = prim__cast_Int16_to_Bits8

%extern prim__cast_Int32_to_Bits8 : Int32 -> Bits8
public export %inline Cast Int32 Bits8 where cast = prim__cast_Int32_to_Bits8

%extern prim__cast_Int64_to_Bits8 : Int64 -> Bits8
public export %inline Cast Int64 Bits8 where cast = prim__cast_Int64_to_Bits8

%extern prim__cast_Bits16_to_Bits8 : Bits16 -> Bits8
public export %inline Cast Bits16 Bits8 where cast = prim__cast_Bits16_to_Bits8

%extern prim__cast_Bits32_to_Bits8 : Bits32 -> Bits8
public export %inline Cast Bits32 Bits8 where cast = prim__cast_Bits32_to_Bits8

%extern prim__cast_Bits64_to_Bits8 : Bits64 -> Bits8
public export %inline Cast Bits64 Bits8 where cast = prim__cast_Bits64_to_Bits8

-- Casts to Bits16
%extern prim__cast_Felt_to_Bits16 : Felt -> Bits16
public export %inline Cast Felt Bits16 where cast = prim__cast_Felt_to_Bits16

%extern prim__cast_Int_to_Bits16 : Int -> Bits16
public export %inline Cast Int Bits16 where cast = prim__cast_Int_to_Bits16

%extern prim__cast_Int8_to_Bits16 : Int8 -> Bits16
public export %inline Cast Int8 Bits16 where cast = prim__cast_Int8_to_Bits16

%extern prim__cast_Int16_to_Bits16 : Int16 -> Bits16
public export %inline Cast Int16 Bits16 where cast = prim__cast_Int16_to_Bits16

%extern prim__cast_Int32_to_Bits16 : Int32 -> Bits16
public export %inline Cast Int32 Bits16 where cast = prim__cast_Int32_to_Bits16

%extern prim__cast_Int64_to_Bits16 : Int64 -> Bits16
public export %inline Cast Int64 Bits16 where cast = prim__cast_Int64_to_Bits16

%extern prim__cast_Bits8_to_Bits16 : Bits8 -> Bits16
public export %inline Cast Bits8 Bits16 where cast = prim__cast_Bits8_to_Bits16

%extern prim__cast_Bits32_to_Bits16 : Bits32 -> Bits16
public export %inline Cast Bits32 Bits16 where cast = prim__cast_Bits32_to_Bits16

%extern prim__cast_Bits64_to_Bits16 : Bits64 -> Bits16
public export %inline Cast Bits64 Bits16 where cast = prim__cast_Bits64_to_Bits16

-- Casts to Bits32
%extern prim__cast_Felt_to_Bits32 : Felt -> Bits32
public export %inline Cast Felt Bits32 where cast = prim__cast_Felt_to_Bits32

%extern prim__cast_Int_to_Bits32 : Int -> Bits32
public export %inline Cast Int Bits32 where cast = prim__cast_Int_to_Bits32

%extern prim__cast_Int8_to_Bits32 : Int8 -> Bits32
public export %inline Cast Int8 Bits32 where cast = prim__cast_Int8_to_Bits32

%extern prim__cast_Int16_to_Bits32 : Int16 -> Bits32
public export %inline Cast Int16 Bits32 where cast = prim__cast_Int16_to_Bits32

%extern prim__cast_Int32_to_Bits32 : Int32 -> Bits32
public export %inline Cast Int32 Bits32 where cast = prim__cast_Int32_to_Bits32

%extern prim__cast_Int64_to_Bits32 : Int64 -> Bits32
public export %inline Cast Int64 Bits32 where cast = prim__cast_Int64_to_Bits32

%extern prim__cast_Bits8_to_Bits32 : Bits8 -> Bits32
public export %inline Cast Bits8 Bits32 where cast = prim__cast_Bits8_to_Bits32

%extern prim__cast_Bits16_to_Bits32 : Bits16 -> Bits32
public export %inline Cast Bits16 Bits32 where cast = prim__cast_Bits16_to_Bits32

%extern prim__cast_Bits64_to_Bits32 : Bits64 -> Bits32
public export %inline Cast Bits64 Bits32 where cast = prim__cast_Bits64_to_Bits32

-- Casts to Bits64
%extern prim__cast_Felt_to_Bits64 : Felt -> Bits64
public export %inline Cast Felt Bits64 where cast = prim__cast_Felt_to_Bits64

%extern prim__cast_Int_to_Bits64 : Int -> Bits64
public export %inline Cast Int Bits64 where cast = prim__cast_Int_to_Bits64

%extern prim__cast_Int8_to_Bits64 : Int8 -> Bits64
public export %inline Cast Int8 Bits64 where cast = prim__cast_Int8_to_Bits64

%extern prim__cast_Int16_to_Bits64 : Int16 -> Bits64
public export %inline Cast Int16 Bits64 where cast = prim__cast_Int16_to_Bits64

%extern prim__cast_Int32_to_Bits64 : Int32 -> Bits64
public export %inline Cast Int32 Bits64 where cast = prim__cast_Int32_to_Bits64

%extern prim__cast_Int64_to_Bits64 : Int64 -> Bits64
public export %inline Cast Int64 Bits64 where cast = prim__cast_Int64_to_Bits64

%extern prim__cast_Bits8_to_Bits64 : Bits8 -> Bits64
public export %inline Cast Bits8 Bits64 where cast = prim__cast_Bits8_to_Bits64

%extern prim__cast_Bits16_to_Bits64 : Bits16 -> Bits64
public export %inline Cast Bits16 Bits64 where cast = prim__cast_Bits16_to_Bits64

%extern prim__cast_Bits32_to_Bits64 : Bits32 -> Bits64
public export %inline Cast Bits32 Bits64 where cast = prim__cast_Bits32_to_Bits64

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module Main

import Core.Context
import Compiler.Common
import Idris.Driver

compile : Ref Ctxt Defs -> (tmpDir : String) -> (execDir : String) ->
          ClosedTerm -> (outfile : String) -> Core (Maybe String)
compile defs tmp dir term file = do coreLift $ putStrLn "I'd rather not."
                                    pure $ Nothing

execute : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> Core ()
execute defs dir term = do coreLift $ putStrLn "Maybe in an hour."

lazyCodegen : Codegen
lazyCodegen = MkCG compile execute

main : IO ()
main = mainWithCodegens [("lazy", lazyCodegen)]


text:
import Data.Vect
import Data.Nat

export
lemmaPlusOneRight : (n : Nat) -> n + 1 = S n
lemmaPlusOneRight n = rewrite plusCommutative n 1 in Refl

public export
consLin : (1 _ : Unit) -> (1 _ : Vect n Unit) -> Vect (S n) Unit
consLin () [] = [()]
consLin () (x :: xs) = () :: x :: xs

consNonLin : Unit -> Vect n Unit -> Vect (n+1) Unit
consNonLin u us = rewrite lemmaPlusOneRight n in u `consLin` us

consLin2 : (1 _ : Unit) -> (1 _ : Vect n Unit) -> Vect (n+1) Unit
consLin2 u us = rewrite lemmaPlusOneRight n in u `consLin` us


text:
module QCont

import Linear.Types
import Linear.Equality
import FunExt

import Syntax.PreorderReasoning

{-
   This file implements quantitative containers, and shows the
   equivalence of initiality and induction for them.

   For convenience, we use an Idris data type to implement the
   underlying algebra and pattern matching to implement the mediating
   morphism fold, as this gives us definitional commutation rules for it.
-}

-- We fix as parameters the shape and position types
parameters (S : Type, P : S -> Type)

  -- Quantative Container || S <| P || interpretation as a functor
  public export
  F : Type -> Type
  F x = Sigma1 S (\ s => P s -<> x)

  infix 10 <$#>

  -- F is functorial
  (<$#>) : (f : x -<> y) -> (F x -<> F y)
  f <$#> (a # h) = a # (\ z => f (h z))

  alg : Type -> Type
  alg x = F x -<> x

  -- Type for initial algebra; we only use pattern matching to define fold
  data W : Type where
    Con : F W -<> W

  -- F-algebra homomorphisms
  infix 10 ==>
  infix 10 #
  data (==>) : alg x -> alg y -> Type where
    (#) : {alpha : alg x} -> {beta : alg y} ->
          (1 fun : x -<> y) ->
          (0 commutes : (arg : F x) -> fun (alpha arg) = beta (fun <$#> arg)) ->
          alpha ==> beta

  -- extracting the underlying function of the morphism
  fun : {alpha : alg x} -> {beta : alg y} -> (1 h : alpha ==> beta) -> x -<> y
  fun (f # _) = f

  -- extracting the proof that it commutes
  0 commutes : {alpha : alg x} -> {beta : alg y} -> (h : alpha ==> beta) ->
             (arg : F x) -> fun h (alpha arg) = beta (fun h <$#> arg)
  commutes ( _ # c) = c

  -- Equality of morphisms
  infix 10 =@
  0  (=@) : {alpha : alg x} -> {beta : alg y} -> (f , g : alpha ==> beta) -> Type
  f =@ g  = (arg : x) -> fun f arg = fun g arg

  0 eq_H_from_fun : {alpha : alg x} -> {beta : alg y} ->
                    (h, g : alpha ==> beta) -> h =@ g -> h = g
  eq_H_from_fun (h # commh) (g # commg) eqp with (funextW eqp)
    eq_H_from_fun (h # commh) (h # commg) eqp | Refl = lcong (\comm => h # comm) eq_comm
      where
      0 eq_comm : commh = commg
      eq_comm = funextW (\x => uip (commh x) (commg x))

  -- composition of F-algebra homomorphisms is an F-algebra homomorphism
  infix 10 .&
  (.&) : {alpha : alg x} -> {beta : alg y} -> {gamma : alg z} ->
         (beta ==> gamma) -> (alpha ==> beta) -> alpha ==> gamma
  (h # commh) .& (g # commg) = (\ 1 x => h (g x)) # comm
    where
     0 comm : (x : F x) -> h (g (alpha x)) = gamma ((\1 x => h (g x)) <$#> x)
     comm x@(s # p) = rewrite commg x in commh (g <$#> x)

  -- identity homomorphism
  id_H : (alpha : alg x) -> alpha ==> alpha
  id_H alpha = (\1 x => x) # \ (s # p) => Refl

  -- mediating map out of mu F
  fold : (alpha : alg x) -> Con ==> alpha
  fold alpha = f # \ (s # h) => Refl
    where
     f : W -<> x
     f (Con (s # h)) = alpha (s # \ p => f (h p))

  -- uniqueness of the mediating map fold
  0 uniqueness : {alpha : alg x} -> (g : Con ==> alpha) -> g = fold alpha
  uniqueness {alpha} g = eq_H_from_fun g (fold alpha) (uniq_f g)
    where
    uniq_f : {alpha : alg x} -> (g : Con ==> alpha) -> g =@ fold alpha
    uniq_f {alpha} (g # comm) (Con (s # h)) =
      trans (comm (s # h)) (cong (\ h => alpha (s # h)) (funext pointwise))
        where
        0 pointwise : (1 x : P s) -> g (h x) = fun (fold alpha) (h x)
        pointwise p = uniq_f (g # comm) (h p)

  -- fold to muF is identity
  0 id_H_eq_foldW : id_H Con = fold Con
  id_H_eq_foldW = uniqueness (id_H Con)

  -- induction principle from initiality
  parameters (0 Q : W -> Type)

    ind_alg : ((1 s : S) -> (0 h : P s -<> W) ->
               ((1 p : P s) -> Q (h p)) -<> Q (Con (s # h))) -<>
             alg (Sigma0 W Q)
    ind_alg m (s # h) = Con (fst <$#> (s # h)) # m s _ (\1 p => snd (h p))

    0 fst_ind_alg : ((1 s : S) -> (0 h : P s -<> W) ->
                     ((1 p : P s) -> Q (h p)) -<> Q (Con (s # h))) -<>
                    Con ==> Con
    fst_ind_alg m =  (\1 w => fst (fun (fold (ind_alg m)) w)) # \(s # h) => Refl

    0 id_H_eq_fia : (1 m : (1 s : S) -> (0 h : P s -<> W) ->
                     ((1 p : P s) -> Q (h p)) -<> Q (Con (s # h))) ->
                  (id_H Con = fst_ind_alg m)
    id_H_eq_fia m = trans id_H_eq_foldW (sym (uniqueness (fst_ind_alg m)))

    0 id_P_eq_fia : (1 m : (1 s : S) -> (0 h : P s -<> W) ->
                     ((1 p : P s) -> Q (h p)) -<> Q (Con (s # h))) ->
                    (id_H Con =@ fst_ind_alg m)
    id_P_eq_fia m w = lcongApp (lcong fun (id_H_eq_fia m)) w

    public export
    induction : ((1 s : S) -> (0 h : P s -<> W) ->
                 ((1 p : P s) -> Q (h p)) -<> Q (Con (s # h))) ->
                (1 w : W) -> Q w
    induction m w = replace {p = Q} (sym (id_P_eq_fia m w)) (snd (fun (fold (ind_alg m)) w))

  -- computation rule
  0 ind_comp : (0 Q : W -> Type) ->
               (m : (1 s : S) -> (0 h : P s -<> W) ->
                 ((1 p : P s) -> Q (h p)) -<> Q (Con (s # h))) ->
               (1 s : S) -> (0 h : P s -<> W) ->
               induction Q m (Con (s # h)) = m s h (\1 p => induction Q m (h p))
  ind_comp q m s h =  Calc $
    |~ induction q m (Con (s # h))
    ~~ m s h (\p => induction q m (h p))  ...(fixQ eq snd_fold)
   where
     0 fixQ : {g : W -<> W} -> (eq : (\1 x => x) = g) -> (exp : (0 w : W) -> q (g w)) ->
               replace {p = q} (sym (cong (\ g => Con (s # (\z => g (h z)))) eq))
                        (m s (\ z => g (h z)) (\1 p => exp (h p)))
              = m s h (\1 p => replace {p = q} (sym (lcongApp eq (h p))) (exp (h p)))
     fixQ Refl v = Refl

     0 fst_fold : W -<> W
     fst_fold w = fst (fun (fold (ind_alg q m)) w)

     snd_fold : (0 w : W) -> q (fst_fold w)
     snd_fold w = snd (fun (fold (ind_alg q m)) w)

     0 eq : (\1 w => w) = (\1 w => fst_fold w)
     eq = lcong fun (id_H_eq_fia q m)

  -- initiality out of induction
  initiality : (alpha : alg x) -> Con ==> alpha
  initiality alpha = (induction (\ _ => x) (\ s , _ , ih  => alpha (s # ih))) # eq
    where
      0 eq : (w : F W) ->
             induction (\ _ => x) (\ s , _ , ih => alpha (s # ih)) (Con w) =
             alpha (induction (\ _ => x) (\ s , _, ih => alpha (s # ih)) <$#> w)
      eq (s # h) = ind_comp (\ _ => x) (\s, _, ih => alpha (s # ih)) s h

  0 uniq_morphism_f : (alpha : alg x) -> (f : Con ==> alpha) ->
                      fun f = fun (initiality alpha)
  uniq_morphism_f alpha (f # comm) = funext (induction (\ z => f z = fun (initiality alpha) z) m)
    where
      0 ihp : (1 s : S) -> (0 h : P s -<> W) ->
              (1 ih : (1 p : P s) -> f (h p) = fun (initiality alpha) (h p)) ->
              (1 p : P s) ->
              f (h p) =  induction (\ _ => x) (\ s, _, ih => alpha (s # ih)) (h p)
      ihp s h ih p = ih p

      0 m : (1 s : S) -> (0 h : P s -<> W) -> (1 ih : (1 p : P s) -> f (h p) = fun (initiality alpha) (h p)) ->
           f (Con (s # h)) = fun (initiality alpha) (Con (s # h))
      m s h ih = Calc $
       |~ f (Con (s # h))
       ~~ alpha (s # \1 x => f (h x))
          ...(comm (s # h))
       ~~ alpha (s # \p => fun (initiality alpha) (h p))
          ...( cong (\ u => alpha (s # u))
                    (funext (ihp s h ih)))
       ~~ fun (initiality alpha) (Con (s # h))
          ...( sym (ind_comp (\ _ => x) (\s , _ , h => alpha (s # h)) s h))

  0 uniq_morphism_h : (alpha : alg x) -> (f : Con ==> alpha) -> f = initiality alpha
  uniq_morphism_h alpha f = eq_H_from_fun f (initiality alpha) (lcongApp (uniq_morphism_f alpha f))

max_stars_repo_name: g-nakov/quantitative-poly

max_issues_repo_name: g-nakov/quantitative-poly

max_forks_repo_name: g-nakov/quantitative-poly


text:
module Data.List.Predicates.Interleaving

import Data.List

%access public export
%default total

data Interleaving : (xs, ys, zs : List type) -> Type where
  Empty   : Interleaving Nil Nil Nil
  LeftAdd : (x : type)
         -> (rest : Interleaving xs ys zs)
         -> Interleaving (x::xs) ys (x::zs)
  RightAdd : (y : type)
          -> (rest : Interleaving xs ys zs)
          -> Interleaving xs (y::ys) (y::zs)

leftEmpty : (ys : List type) -> Interleaving Nil ys ys
leftEmpty [] = Empty
leftEmpty (x :: xs) = RightAdd x (leftEmpty xs)

leftEmptyCons : (x : type) -> (xs : List type) -> Interleaving Nil (x::xs) (x::xs)
leftEmptyCons x [] = RightAdd x Empty
leftEmptyCons x (y :: xs) with (leftEmptyCons y xs)
  leftEmptyCons x (y :: xs) | (RightAdd y rest) = RightAdd x (RightAdd y rest)

rightEmpty : (xs : List type) -> Interleaving xs Nil xs
rightEmpty [] = Empty
rightEmpty (x :: xs) = LeftAdd x (rightEmpty xs)

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
module InsertionHelpers

import Data.Vect
import congruence
import Data.Fin
import Permutation
import PermCons
import Finite
-- import DecOrderNat
import LTE_Properties
import SortingWithProof
import InsertionSort

%access public export
%default total

||| Proof that one element list is always sorted

insertHelper8 : (y : Nat) -> (IsSorted (S Z) [y])
insertHelper8 y FZ = LTE_Property1 y

||| x :: xs is sorted . a < x . a :: x :: xs is sorted

insertHelper1 : (n : Nat) -> (a, x : Nat) ->
                (xs : (Vect n Nat)) -> (LTE a x) ->
                (IsSorted (S n) (x :: xs) ) ->
                (IsSorted (S (S n)) (a :: x :: xs) )

insertHelper1 Z a x Nil pfLTE pfSort FZ = (LTE_Property1 a)
insertHelper1 Z a x Nil pfLTE pfSort (FS FZ) = pfLTE
insertHelper1 (S k) a x xs pfLTE pfSort FZ = (LTE_Property1 a)
insertHelper1 (S k) a x xs pfLTE pfSort (FS FZ) = pfLTE
insertHelper1 (S k) a x xs pfLTE pfSort (FS (FS l)) =
    pfSort (FS l)

insertHelper9 : (k : Nat) -> (x : Nat) -> (xs : Vect k Nat) ->
                (IsSorted (S k) (x :: xs)) ->
                (IsSorted k xs)

insertHelper9 (S k) x xs pfSort FZ = LTE_Property1 (index FZ xs)
insertHelper9 (S k) x xs pfSort (FS l) = pfSort (FS (FS l))

vect_prp1 : (n : Nat) -> (xs : (Vect (S n) Nat)) ->
             (xs = ((head xs) :: (tail xs)))

vect_prp1 Z (a :: Nil) = Refl
vect_prp1 (S n) (a :: xs) = Refl

insertHelper10 : (n : Nat) -> (xs : (Vect (S n) Nat)) ->
                 (k : Fin (S n)) -> (LTE (index (pred k) xs) (index k xs)) ->
                 (LTE (index (pred k) ((head xs) :: (tail xs))) (index k ((head xs) :: (tail xs))))

insertHelper10 n (y :: ys) k pf = pf

transport : (typ : Type) -> (a, b : typ) -> (P : (typ -> Type)) -> (a = b) -> (P a) -> (P b)
transport typ a a P Refl pf = pf

insertHelper11 : (n : Nat) -> (u, v : (Vect (S n) Nat)) -> (u = v) -> (IsSorted (S n) u) ->
                (IsSorted (S n) v)

insertHelper11 n u v pfEq sort_pf k = let

    pf1 = congruence (Vect (S n) Nat) Nat u v (index (pred k)) pfEq -- u[k-1] = v[k-1]
    pf2 = congruence (Vect (S n) Nat) Nat u v (index k) pfEq -- u[k] = v[k]
    pf3 = sort_pf k -- u[k - 1] < u[k]
    u_k1 = index (pred k) u
    u_k = index k u
    v_k1 = index (pred k) v
    v_k = index k v
    pf4 = transport Nat u_k v_k (LTE u_k1) pf2 pf3 -- u_k1 < v_k
    pf5 = transport Nat u_k1 v_k1 (\l => LTE l v_k) pf1 pf4

    in
    pf5

--vect_prp_2 : (n : Nat) -> (v : (Vect (S n) Nat)) -> (index

----------------------------------------------------------------------------------------------------------------

insertHelper3 : (a : Nat) -> (x : Nat) -> (LTE x a) ->
                (IsSorted (S (S Z)) (x :: [a]) )

insertHelper3 a x pfLTE FZ = LTE_Property1 x
insertHelper3 a x pfLTE (FS FZ) = pfLTE

----------------------------------------------------------------------------------------------------------------

insertHelper12 : (n : Nat) -> (ys : (Vect (S n) Nat)) -> ((index FZ ys) = (head ys))
insertHelper12 n (y :: ys) = Refl

----------------------------------------------------------------------------------------------------------------

insertHelper13 : (n : Nat) -> (y : Nat) -> (ys : (Vect n Nat)) -> ( (tail (y :: ys)) = ys)
insertHelper13 n y ys = Refl


text:
-- Shamelessly stolen from Edwin Brady
module Main

pythagoras : Int -> List (Int, Int, Int)
pythagoras max = [
    (x, y, z)
    | z <- [1..max]
    , y <- [1..z]
    , x <- [1..y]
    , x * x + y *y == z * z
  ]

main : IO ()
main = do
  arg <- getLine
  printLn $ pythagoras (cast arg)

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean


text:
||| An Idealised HDL for linear wirings.
|||
||| Module    : Idealised.idr
||| Copyright : (c) Jan de Muijnck-Hughes
||| License   : see LICENSE
|||
module Circuits.Idealised

import public Circuits.Idealised.Core
import public Circuits.Idealised.Types
import public Circuits.Idealised.Terms
import public Circuits.Idealised.AST
import public Circuits.Idealised.Lexer
import public Circuits.Idealised.Parser
import public Circuits.Idealised.Check
import public Circuits.Idealised.Interp

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
module GaloisCh1

-- > idris -p base
import Data.Fin

%default total
-- %auto_implicits off

{--
/libs/prelude/Prelude/Algebra.idr
interface Semigroup ty where
  (<+>) : ty -> ty -> ty
interface Semigroup ty => Monoid ty where
  neutral : ty
/libs/contrib/Control/Algebra.idr
interface Monoid a => Group a where
  inverse : a -> a
/libs/contrib/Interfaces/Verified.idr
interface Semigroup a => VerifiedSemigroup a where
  semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
  monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l
  monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r
interface (VerifiedMonoid a, Group a) => VerifiedGroup a where
  groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral
  groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutrals
VerifiedGroup ZZ using PlusZZMonoidV where
  groupInverseIsInverseL k = rewrite sym $ multCommutativeZ (NegS 0) k in
                             rewrite multNegLeftZ 0 k in
                             rewrite multOneLeftNeutralZ k in
                             plusNegateInverseLZ k
  groupInverseIsInverseR k = rewrite sym $ multCommutativeZ (NegS 0) k in
                             rewrite multNegLeftZ 0 k in
                             rewrite multOneLeftNeutralZ k in
                             plusNegateInverseRZ k
--}

-- 群の定義
infixl 6 <+>
interface Group a where
  (<+>)  : a -> a -> a
  gUnit  : a
  gInv   : a -> a
  vAssoc : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
  vUnit  : (c : a) -> (c <+> gUnit = c, gUnit <+> c = c)
  vInv   : (c : a) -> (c <+> gInv c = gUnit, gInv c <+> c = gUnit)

-- 準同型
record Hom (g : Type)(h : Type)(grp : Group g)(hrp : Group h)(f : g -> h) where
  constructor MkHom
  -- 左辺の<+>はgrpのもの、右辺の<+>はhrpのもの
  hom : (a, b : g) -> f (a <+> b) = f a <+> f b

-- 単射
record Mono (g : Type)(h : Type)(f : g -> h) where
  constructor MkMono
  mono : (a, b : g) -> f a = f b -> a = b

-- 全射
record Epi (g : Type)(h : Type)(f : g -> h) where
  constructor MkEpi
  epi : (z : h) -> (a ** f a = z)

-- gはhの部分群である
record Subgroup (g : Type)(h : Type)(grp : Group g)(hrp : Group h)(f : g -> h) where
  constructor MkSubgroup
  sHom  : Hom g h grp hrp f
  sMono : Mono g h f

-- gとhは同型である
record Iso (g : Type)(h : Type)(grp : Group g)(hrp : Group h)(f : g -> h) where
  constructor MkIso
  iSubgroup : Subgroup g h grp hrp f
  iEpi      : Epi g h f
-- ----------------------------------

-- 巡回群
plusModN : (n : Nat) -> Fin n -> Fin n -> Fin n
plusModN Z     finZ    _ = absurd finZ
plusModN (S k) finX finY =
  let n = S k;
      x = toNat finX;
      y = toNat finY
  in fromNat $ modNatNZ (x + y) n SIsNotZ

invModN : (n : Nat) -> Fin n -> Fin n
invModN Z     finZ = absurd finZ
invModN (S k) finX =
  let n = S k;
      x = toNat finX
  in fromNat $ modNatNZ (minus n x) n SIsNotZ

implementation [CyN] Group (Fin n) where
  (<+>) {n = n}     = plusModN n
  gUnit {n = Z    } = idris_crash "no constructor!"
  gUnit {n = (S n)} = FZ
  gInv  {n = n}     = invModN n
  vAssoc l c r      = ?rhs1
  vUnit  r          = ?rhs2
  vInv   r          = ?rhs3
-- ----------------------------------

cyclicToCyclic : (n, k : Nat) -> Fin (S n) -> Fin (S (mult k (S n) + n))
cyclicToCyclic n Z     = id -- idにするところがミソ
cyclicToCyclic n (S k) = \_ =>
  let y = S (mult (S k) (S n) + n) in fromNat y

-- ◆定理1.5 巡回群の部分群は巡回群である
-- 部分群の位数(S n)が、元の群の位数(S k)*(S n)の約数である事を仮定した
-- S (mult k (S n) + n) = (S k) * (S n)
cyclicSubCyclic : (n : Nat)
  -> ((k : Nat) -> Subgroup (Fin (S n)) (Fin (S (mult k (S n) + n))) subGrp CyN (cyclicToCyclic n k))
    -> Iso (Fin (S n)) (Fin (S n)) subGrp CyN (cyclicToCyclic n Z)
cyclicSubCyclic n fSubG = MkIso (fSubG Z) (MkEpi (\z => (z ** Refl)))

-- 既約剰余類群
-- 元かどうかは、外からのBool値で判断する
data FinBool : (n : Nat) -> Type where
  Fb : Fin n -> Bool -> FinBool n

multModN : (n : Nat) -> Fin n -> Fin n -> Fin n
multModN Z     finZ    _ = absurd finZ
multModN (S k) finX finY =
  let n = S k;
      x = toNat finX;
      y = toNat finY
  in fromNat $ modNatNZ (x * y) n SIsNotZ

multModNFb : (n : Nat) -> FinBool n -> FinBool n -> FinBool n
multModNFb Z     (Fb finZ _    ) _               = absurd finZ
multModNFb (S _) (Fb _    False) _               = Fb FZ False
multModNFb (S _) (Fb _    True ) (Fb _    False) = Fb FZ False
multModNFb (S k) (Fb finX True ) (Fb finY True ) = Fb (multModN (S k) finX finY) True

invModNFb : (n : Nat) -> FinBool n -> FinBool n
invModNFb Z     (Fb finZ _    ) = absurd finZ
invModNFb (S _) (Fb _    False) = Fb FZ False
invModNFb (S k) (Fb finX True ) = Fb (invModN (S k) finX) True

implementation [Mgm] Group (FinBool n) where
  (<+>) {n = n}     = multModNFb n
  gUnit {n = Z    } = idris_crash "no constructor!"
  gUnit {n = (S n)} = Fb FZ True
  gInv  {n = n}     = invModNFb n
  vAssoc l c r      = ?rhs4
  vUnit    c        = ?rhs5
  vInv     c        = ?rhs6
-- ----------------------------------

-- 群の直積
implementation [GPr] (Group a, Group b) => Group (a, b) where
  (x, y) <+> (z, u) = (x <+> z, y <+> u)
  gUnit             = (gUnit, gUnit)
  gInv (x, y)       = (gInv x, gInv y)
  vAssoc l c r      = ?rhs7
  vUnit    c        = ?rhs8
  vInv     c        = ?rhs9
-- ----------------------------------

-- ◆定理1.9 (Z/(p^e)(q^f)Z)* ≡ (Z/(p^e)Z)* × (Z/(q^f)Z)*
fFinBoolToGPr : (p, q, e, f : Nat)
  -> (FinBool ((power (S (S p)) (S (S e)))*(power (S (S (S q))) (S f))))
    -> (FinBool (power (S (S p)) (S (S e))), FinBool (power (S (S (S q))) (S f)))
theorem1_9 : (p, q, e, f : Nat)
  -> (Group (FinBool (power (S (S p)) (S (S e))))
    -> Group (FinBool (power (S (S (S q))) (S f)))
      -> Iso
           (FinBool ((power (S (S p)) (S (S e)))*(power (S (S (S q))) (S f))))
           (FinBool (power (S (S p)) (S (S e))), FinBool (power (S (S (S q))) (S f))) Mgm GPr (fFinBoolToGPr p q e f))

-- ◆定理1.18 (Z/2^nZ)*は巡回群の直積に同型である
-- (Z/2^nZ)* ≡ (Z/2^(n-2)Z) × (Z/2Z)
fTheorem1_18 : (e : Nat)
  -> (FinBool (power 2 (S (S e)))) -> (Fin (power 2 e), Fin 2)
theorem1_18 : (e : Nat)
  -> (Group (Fin (power 2 e))
      -> Group (Fin 2)
        -> Iso
            (FinBool (power 2 (S (S e))))
            (Fin (power 2 e), Fin 2) Mgm GPr (fTheorem1_18 e))

-- ◆定理1.19 (Z/奇素数p^nZ)*は巡回群の直積に同型である
-- (Z/p^nZ)* ≡ (Z/p^(n-1)Z) × (Z/(p-1)Z)
fTheorem1_19 : (q, f : Nat)
  -> (FinBool (power (S (S (S q))) (S n))) -> (Fin (power (S (S (S q))) n), Fin p)
theorem1_19 : (q, f : Nat)
  -> (Group (Fin (power (S (S (S q))) f))
      -> Group (Fin (S (S q)))
        -> Iso
            (FinBool (power (S (S (S q))) (S f)))
            (Fin (power (S (S (S q))) f), Fin (S (S q))) Mgm GPr (fTheorem1_19 q f))

-- ◆定理1.20 既約剰余類群は巡回群の直積に同型である
mgmProduct : (p, q, e, f : Nat)
  -> Either ((Group (FinBool (power (S (S p)) (S (S e))))
      -> Group (FinBool (power (S (S (S q))) (S f)))
        -> Iso
            (FinBool ((power (S (S p)) (S (S e)))*(power (S (S (S q))) (S f))))
            (FinBool (power (S (S p)) (S (S e))), FinBool (power (S (S (S q))) (S f))) Mgm GPr (fFinBoolToGPr p q e f)),
      (Group (Fin (power 2 e))
      -> Group (Fin 2)
        -> Iso
            (FinBool (power 2 (S (S e))))
            (Fin (power 2 e), Fin 2) Mgm GPr (fTheorem1_18 e)),
      (Group (Fin (power (S (S (S q))) f))
      -> Group (Fin (S (S q)))
        -> Iso
            (FinBool (power (S (S (S q))) (S f)))
            (Fin (power (S (S (S q))) f), Fin (S (S q))) Mgm GPr (fTheorem1_19 q f))
     )
     ((Group (FinBool (power (S (S p)) (S (S e))))
      -> Group (FinBool (power (S (S (S q))) (S f)))
        -> Iso
            (FinBool ((power (S (S p)) (S (S e)))*(power (S (S (S q))) (S f))))
            (FinBool (power (S (S p)) (S (S e))), FinBool (power (S (S (S q))) (S f))) Mgm GPr (fFinBoolToGPr p q e f)),
      (Group (Fin (power (S (S (S p))) e))
      -> Group (Fin (S (S p)))
        -> Iso
            (FinBool (power (S (S (S p))) (S e)))
            (Fin (power (S (S (S p))) e), Fin (S (S p))) Mgm GPr (fTheorem1_19 p e)),
      (Group (Fin (power (S (S (S q))) f))
      -> Group (Fin (S (S q)))
        -> Iso
            (FinBool (power (S (S (S q))) (S f)))
            (Fin (power (S (S (S q))) f), Fin (S (S q))) Mgm GPr (fTheorem1_19 q f))
     )
mgmProduct Z     q e f = Left  ((theorem1_9 Z q e f), (theorem1_18 e), (theorem1_19 q f))
mgmProduct (S p) q e f = Right ((theorem1_9 (S p) q e f), (theorem1_19 (S p) e), (theorem1_19 q f))