text:
module z where

-- http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf
{-
Dependently Typed Programming in Agda
Ulf Norell1   : Chalmers University, Gothenburg   : ulfn@chalmers.se
James Chapman : Institute of Cybernetics, Tallinn : james@cs.ioc.ee

------------------------------------------------------------------------------
1 Introduction

In Hindley-Milner languages (Haskell, ML) : separation between types and values.

Dependently typed : types can contain (depend on) arbitrary values and
                    appear as arguments and results of ordinary functions

Dependent types enables types to talk about values,
so can encode properties of values as types
whose elements are proofs that the property is true.

So dependently typed programming language can be used as a logic.

To be consistent programs must be total.

------------------------------------------------------------------------------
2 BASICS

based on intuitionistic type theory[4]

--------------------------------------------------
2.1 DATATYPES AND PATTERN MATCHING
-}

data Bool : Set where
  true  : Bool
  false : Bool

{-
type of Bool is
- Set, the type of small types
- There is hierarchy of increasingly large types
- type of Set is Set1, whose type is Set2, ...
-}

not : Bool → Bool
not true  = false
not false = true

data Nat : Set where
 zero :       Nat
 suc  : Nat → Nat
{-# BUILTIN NATURAL Nat #-}

_+_ : Nat → Nat → Nat
zero  + m =          m
suc n + m = suc (n + m)
infixl 40 _+_

_*_ : Nat → Nat → Nat
zero  * m = zero
suc n * m = m + n * m
infixl 60 _*_

{-
functions must not crash and must terminate

recursive calls have to be made on structurally smaller arguments

mixfix via  _ : args where the underscores are
-}

_or_ : Bool → Bool → Bool
false or x = x
true  or _ = true -- uses wildcard pattern on "don't care" args
infixr 20 _or_

-- polymorphic function over type A
if_then_else_ : {A : Set} → Bool → A → A → A
if  true then x else y = x
if false then x else y = y
infix 5 if_then_else_

-- types parameterize by other types
data List (A : Set) : Set where
  []   :                List A
  _::_ : A → List A → List A
infixr 40 _::_

-- liberal naming policy enables naming above
data _⋆ (α : Set) : Set where
  ε : α ⋆
  _C_ : α → α ⋆ → α ⋆

{-
whitespace important

--------------------------------------------------
2.2 DEPENDENT FUNCTIONS

result type depends on VALUE of an arg
  (x : A) → B for the
type of functions
- given   : arg x of type A
- returns : result of type B
  - where x may appear in B

special case is when x itself is a type, e.g.,
-}

identity : (A : Set) → A → A
identity A x = x

zero’ : Nat
zero’ = identity Nat zero

{-
identity is a dependent function
- given
  - a type argument A and
  - an element of A
- returns
  - the element

This is how polymorphic functions are encoded in Agda.

example : function which takes a dependent function and applies it to an argument:
-}

apply : (A : Set) (B : A → Set) → ((x : A) → B x) → (a : A) → B a
apply A B f a = f a

{-
shorthand for dependent function types:

        (x : A)   (y : B) → C
for     (x : A) → (y : B) → C

        (x y : A)       → B
for     (x : A) (y : A) → B

elements of dependent function types are lambda terms which may carry explicit type info

alternative ways to identity
identity function above are:
-}

identity2 : (A : Set) → A → A
identity2 = \A x → x

identity3 : (A : Set) → A → A
identity3 = \(A : Set) (x : A) → x

identity4 : (A : Set) → A → A
identity4 = \(A : Set) x → x

{-
--------------------------------------------------
2.3 IMPLICIT ARGUMENTS

Previous section showed how dependent functions taking types as
arguments used to model polymorphic types.

But it is not necessary to say at which point it is applied - that can be inferred.

The identity functions above explicitly provide the type argument.

Avoid explicit type arg via implicit arguments using {}
-}

id : {A : Set} → A → A
id x = x

true’ : Bool
true’ = id true

{-
No restrictions on what arguments can be made implicit.
Not guarantees that an implicit argument can be inferred.

E.g., make 2nd arg of identity function implicit as well:
-}

silly : {A : Set} {x : A} → A -- but type checker cannot figure out 2nd arg
silly {_} {x} = x

false’ : Bool
false’ = silly {x = false} -- must provide via named implicit application syntax f {v}
                           -- must use name if not in order
-- type checker fills in term
-- will not search, only looks at typing constraints and performs unification
one : Nat
one = identity _ (suc zero)

-- example of inferring the typing constraints
_◦_ : {A : Set}{B : A → Set}{C : (x : A) → B x → Set}
      (f : {x : A}(y : B x) → C x y)(g : (x : A) → B x)
      (x : A) → C x (g x)
(f ◦ g) x = f (g x)

plus-two = suc ◦ suc

-- other functions

map : {A B : Set} → (A → B) → List A → List B
map f       []  = []
map f (x :: xs) = f x :: map f xs

_++_ : {A : Set} → List A → List A → List A
[]        ++ ys =             ys
(x :: xs) ++ ys = x :: (xs ++ ys)

{-
--------------------------------------------------
-- 2.4 DATATYPE FAMILIES

So far, only used dependent types is to represent polymorphism
-}

data Vec (A : Set) : Nat → Set where
  []   :                           Vec A  zero
  _::_ : {n : Nat} → A → Vec A n → Vec A (suc n)

{-
type of Vec A is Nat → Set
- means that Vec A is a family of types indexed by natural numbers
- for each Nat n, Vec A n is a type
- []   constructs an element in Vec A zero
- _::_ constructs an element in Vec A (suc n) for some n

distinction between parameters and indices of a datatype
- parameterised by type A
- indexed over Nat

type of _::_ is a dependent function type
- 1st arg is an implicit Nat n
- returns type that depends on n 'suc n'

same constructor names for Vec as for List
-  constructor names are not required to be distinct between different datatypes
-}

-- safe head
head : {A : Set} {n : Nat} → Vec A (suc n) →     A
head (x :: xs) = x

tail : {A : Set} {n : Nat} → Vec A (suc n) → Vec A n
tail (x :: xs) = xs

{-
rule for when to include a particular case is:
  if it is type correct you have to include it
-}

--------------------------------------------------
-- DOT PATTERNS : indicate value of an arg deduced by type checking, not pattern matching

vmap : {A B : Set} {n : Nat} → (A → B) → Vec A n → Vec B n
vmap f       []  = []
vmap f (x :: xs) = f x :: vmap f xs

{-
map on Vec is exactly the same map on List
only change is the type

behind the scenes, what happens with the length argument when pattern matching

to see, define new versions of Vec and vmap with fewer implicit arguments:
-}

data Vec2 (A : Set) : Nat → Set where
  nil  :                            Vec2 A  zero
  cons : (n : Nat) → A → Vec2 A n → Vec2 A (suc n)

vmap2 : {A B : Set} (n : Nat) → (A → B) → Vec2 A n → Vec2 B n
vmap2 .zero    f  nil          = nil
vmap2 .(suc n) f (cons n x xs) = cons n (f x) (vmap2 n f xs)

{-
pattern matching on list argument reveals its length
- if nil  then zero
- if cons then suc n

to indicate value of an arg deduced by type checking,
rather than observed by pattern matching,
it is prefixed by a dot (.)

could choose to define vmap by first pattern matching on the length rather than on the list
-}

vmap3 : {A B : Set} (n : Nat) → (A → B) → Vec2 A n → Vec2 B n
vmap3  zero   f  nil           = nil
vmap3 (suc n) f (cons .n x xs) = cons n (f x) (vmap3 n f xs)

{-
rule for when arg should be dotted:
- if there is a unique type correct value for the argument it should be dotted

above, the terms under the dots were valid patterns
- in general they can be arbitrary terms
e.g.,
-}

data Image_el_ {A B : Set}(f : A → B) : B → Set where
  im : (x : A) → Image f el f x

{-
only way to construct an element in the image of f
is to pick an argument x and apply f to x

knowing  that a particular y is in the image of f enables computing the inverse of f on y:
-}

inv : {A B : Set} (f : A → B) (y : B) → Image f el y → A
inv f .(f x) (im x) = x

{-
--------------------------------------------------
ABSURD PATTERNS
-}

-- family of numbers smaller than a given natural number
data Fin : Nat → Set where
  fzero : {n : Nat} →         Fin (suc n) -- smaller than suc n for any n
  fsuc  : {n : Nat} → Fin n → Fin (suc n) -- if i smaller than n then fsuc i is smaller than suc n

-- Now way to construct a Fin smaller than zero.
-- When no possible constructor patterns for a given argument
-- then pattern match with absurd pattern ()

magic : {A : Set} → Fin zero → A
magic ()

{-
Using absurd pattern means no need to give a right hand side,
since no way anyting could given as an arg that would match.

Seems the clause not needed, that checker could tell.
But a case can only be omitted if no type correct way of writing it.

'magic a' has a type correct left hand side

absurd pattern can only be used if there are no valid constructor patterns for the arg.
It is not enough that there are no closed inhabitants of the type.
E.g.,
-}

data Empty : Set where
  empty : Fin zero → Empty

{-
Args of type Empty cannot be matched with absurd pattern,
since there is a valid constructor pattern: 'empty x'
So must write:
-}

magic’ : {A : Set} → Empty → A
magic’ (empty ()) -- magic’ () -- not accepted

-- Extract ith element of the list (starting from 0):
-- Turns a list into a function from indices to elements.
_!_ : {n : Nat} {A : Set} → Vec A n → Fin n → A
[]        ! ()
(x :: xs) !  fzero   = x
(x :: xs) ! (fsuc i) = xs ! i

{-
types ensure no danger of indexing outside the list

reflected in use of absurd in empty case : no possible values for the index
-}

-- constructing a list given a function from indices to elements
tabulate : {n : Nat} {A : Set} → (Fin n → A) → Vec A n
tabulate  {zero} f = []
tabulate {suc n} f = f fzero :: tabulate (f ◦ fsuc) -- recursive call implicitly gets 'n'

{-
tabulate is defined by recursion over the length of the result list,
even though it is an implicit argument.

In general, no correspondance between implicit data and computationally irrelevant data.

------------------------------------------------------------------------------
-- 2.5 PROGRAMS AS PROOFS

Type system can represent propositions as types whose elements are proofs of the proposition.
-}

data   False : Set where -- datatype with no constructors
record True  : Set where -- record type with no fields
                         -- has a single element : the empty record

{-
Could have defined True as datatype with a single element.
But using record def lets checker know there is a unique element of True
and will fill in any implicit arguments of type True with this element.

exploited in trivial:
-}

trivial : True
trivial = _

trivial' : True
trivial' = record {}

{-
where right hand is underscore,
instead of explicitly writing 'record {}'

The 'False' and 'True' propositions enable working with decidable propositions.
Can model decidable propositions as booleans and define
-}

-- takes a VALUE of type Bool
-- returns a Set (i.e., a TYPE)
isTrue : Bool → Set
isTrue true  = True
isTrue false = False

isFalse : Bool → Set
isFalse x = isTrue (not x)

{-
isTrue b is the type of proofs that b equals true.

This technique enables defining safe list lookup function in a different way,
working on simply typed lists and numbers.
-}

-- takes   Nat  VALUES
-- returns Bool VALUES
_<_ : Nat → Nat → Bool
_     < zero  = false
zero  < suc n = true
suc m < suc n = m < n

length : {A : Set} → List A → Nat
length        [] = zero
length (x :: xs) = suc (length xs)

--                                             |
--                                             v
lookup : {A : Set} (xs : List A) (n : Nat) → isTrue (n < length xs) → A
lookup       []       n ()
lookup (x :: xs)  zero   p = x
lookup (x :: xs) (suc n) p = lookup xs n p

{-
Rather than there being no index into the empty list,
there is no proof that a number n is smaller than zero.

In this example, using indexed types to capture the precondition,
as done in '_!_' above, is a little bit nicer,
since do not have to pass an explicit proof object
as done in 'lookup' above.

When properties cannot be easily captured by indexed types, this is a useful alternative.

--------------------------------------------------
DEFINE PROPOSITIONS USING DATATYPE FAMILIES
-}

-- family of proofs of “being equal to x”
-- specify the type by giving it two args
-- type can only be constructed when the two args reduce to the same thing
data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x -- only inhabited at index x where the single proof is refl

-- another exampla
-- compare to def of '_<_' above
data _≤_ : Nat → Nat → Set where
  leq-zero :   {n : Nat} →         zero  ≤     n
  leq-suc  : {m n : Nat} → m ≤ n → suc m ≤ suc n

{-
advantage of this approach
- PATTERN MATCH ON PROOF OBJECT
- makes proving properties of _≤_ easier
- e.g.,
-}

leq-trans : {l m n : Nat} → l ≤ m → m ≤ n → l ≤ n
leq-trans  leq-zero            _  = leq-zero
leq-trans (leq-suc p) (leq-suc q) = leq-suc (leq-trans p q)

{-
------------------------------------------------------------------------------
-- 2.6 WITH : PATTERN MATCH ON RESULT OF INTERMEDIATE COMPUTATION

Haskell : done on right hand side using case

when matching expression in dependently typed language, learn
- shape of expression
- things about other expressions
  - e.g., matching 'Vec A n' reveals info about n
- not captured by usual case expression

to pattern match on an expression e in the def of fun f
- abstract f over value of e
- effectively adding another argument to f
- can then be matched on in usual way
-}

min : Nat → Nat → Nat
min x y with x < y
min x y | true  = x
min x y | false = y

{-
Can abstract over multiple expressions at same time, separated by vertical bars.

Can nest with abstractions.

When matching on arg using WITH, no need to match on args again:
- use ...
-}

filter : {A : Set} → (A → Bool) → List A → List A
filter p [] = []
filter p (x :: xs) with p x
... | true  = x :: filter p xs
... | false =      filter p xs

{-
Example of revealing info via matching.

Compare numbers for equality.
Instead of returning boolean,
return proof of equality or
explanation of why they are not equal.
-}

data _≠_ : Nat → Nat → Set where
  z≠s :   {n : Nat} →          zero ≠ suc n -- different if one is zero and other suc
  s≠z :   {n : Nat} →         suc n ≠ zero  -- vice versa
  s≠s : {m n : Nat} → m ≠ n → suc m ≠ suc n -- both suc but their predecessors are different

data Equal? (n m : Nat) : Set where
  eq  : n ≡ m → Equal? n m
  neq : n ≠ m → Equal? n m

-- now function that returns the explanation

equal? : (n m : Nat) → Equal? n m
--                                  Equal? zero zero
--                                      zero ≡ zero
equal?  zero    zero             = eq  refl
equal?  zero   (suc _)           = neq z≠s
equal? (suc _)  zero             = neq s≠z
equal? (suc n) (suc m) with equal? n m -- matching on proof reveals if predecessors are equal
equal? (suc _) (suc _) | eq refl = eq refl
--                                 Equal? (suc n) (suc m)
--                                      suc n ≠ suc m
--                                          n ≠     m
equal? (suc _) (suc _) | neq p   = neq (s≠s p)

{-
using WITH : expression is abstracted from entire context

means that if expression occurs in type of arg to function or in result type,
occurrence is replaced by the with-argument on the left hand side.

e.g., prove 'filter' only removes some elements
-}

-- to make a sublist, each element can either be dropped or kept
infix 20 _⊆_
data _⊆_ {A : Set} : List A → List A → Set where
  stop :                                   [] ⊆      []
  drop : forall {xs y ys} → xs ⊆ ys →      xs ⊆ y :: ys
  keep : forall {x xs ys} → xs ⊆ ys → x :: xs ⊆ x :: ys

{-
When checker can infer type of an arg in fun type, then can use forall:
– forall {x y} a b → A    shorthand for   {x : _} {y : _} (a : _) (b : _) → A
-}

-- proof that filter computes a sublist of its argument:
lem-filter : {A : Set} (p : A → Bool) (xs : List A)
           → filter p xs ⊆ xs
lem-filter p       [] = stop
lem-filter p (x :: xs) with p x
... | true            = keep (lem-filter p xs)
... | false           = drop (lem-filter p xs)

{-
to prove     lem-filter p (x :: xs)

need to prove : (filter p (x :: xs) | p x) ⊆ x :: xs

when abstracting over p x it will be abstracted from goal type, giving
             lem-filter p (x :: xs) with p x
             ... | px = ?

where p x has been replaced by px in the goal type
                (filter p (x :: xs) | px) ⊆ x :: xs

match px reduce call to filter

             lem-filter p (x :: xs) with p x
             ... | true  = ? {- x :: filter p xs ⊆ x :: xs -}
             ... | false = ? {-      filter p xs ⊆ x :: xs -}

Sometimes WITH useful to abstract over expr that will not be matched,
e.g., expect expr to be instantiated by matching on something else
-}

lem-plus-zero : (n : Nat) → n + zero ≡ n
lem-plus-zero zero = refl
lem-plus-zero (suc n) with n + zero | lem-plus-zero n
... | _ | refl = refl -- suc n ≡ suc n

{-
In suc ("step" case) : match on induction hypothesis : n + zero ≡ n
to prove suc n + zero ≡ suc n

but n + zero does not unify with n

so abstract over n + zero, calling it _,
left with the induction hypothesis m ≡ n and goal suc m ≡ suc n
Now match on induction hypothesis, instantiating _ to n

--------------------------------------------------
-- 2.7 Modules TODO

--------------------------------------------------
-- 2.8 Records
-}

record Point : Set where
  field
    x : Nat
    y : Nat

mkPoint : Nat → Nat → Point
mkPoint a b = record { x = a; y = b }

{-
field projections via module of the same name.
- parameterised by element of record type
- contains projection functions for the fields
- i.e.,
   module Point (p : Point) where
     x : Nat
     y : Nat
- can be used as is or instantiated to a particular record
-}

getX : Point → Nat
getX = Point.x

abs2 : Point → Nat
abs2 p = let open Point p in x * x + y * y

-- TODO pattern match on records

-- can add functions to the module of a record

record Monad (M : Set → Set) : Set1 where
  field
    return :   {A : Set} →   A →             M A
    _>>=_  : {A B : Set} → M A → (A → M B) → M B

  mapM : {A B : Set} → (A → M B) → List A → M (List B)
  mapM f [] = return []
  mapM f (x :: xs) = f x >>= \y →
              mapM f xs >>= \ys →
              return (y :: ys)

mapM’ : {M : Set → Set}
      → Monad M
      → {A B : Set}
      → (A → M B)
      → List A
      → M (List B)
mapM’ Mon f xs = Monad.mapM Mon f xs

--------------------------------------------------
-- 2.9 Exercises

-------------------------
-- Exercise 2.1. Matrix transposition
-- inner vectors are rows
Matrix : Set → Nat → Nat → Set
Matrix A n m = Vec (Vec A n) m

-- (a) function to compute vector containing n copies of element x

vec : {n : Nat} {A : Set} → A → Vec A n
vec  {zero} x = []
vec {suc n} x = x :: vec {n} x

vecTest : Vec Nat 3
vecTest = vec zero

-- (b) point-wise application of vector of functions to vector of arguments

infixl 90 _$_
_$_ : {n : Nat} {A B : Set} → Vec (A → B) n → Vec A n → Vec B n
_$_       []        []  = []
_$_ (f :: fs) (x :: xs) = f x :: fs $ xs

$TestInputFs : Vec (Nat → Nat) 2
$TestInputFs = (_+ 1) :: (_* 2) :: []

$TestInputXs : Vec Nat 2
$TestInputXs =     0 ::      2  :: []

$TestOutput  : Vec Nat 2
$TestOutput  =     1 ::      4  :: []

$Test : $TestInputFs $ $TestInputXs ≡ $TestOutput
$Test = refl

-- (c) matrix transposition in terms of 'vec' and _$_

transpose : forall {A n m} → Matrix A n m → Matrix A m n
transpose         []  = vec []
transpose (xs :: xss) = (vmap _::_ xs) $ (transpose xss)

transposeTestInput : Matrix Nat 2 3
transposeTestInput = r1 :: r2 :: r3 :: []
 where
  r1 = 1 :: 2 :: []
  r2 = 3 :: 4 :: []
  r3 = 5 :: 6 :: []

transposeTestOuput : Matrix Nat 3 2
transposeTestOuput = r1 :: r2 :: []
 where
  r1 = 1 ::  3 :: 5 :: []
  r2 = 2  :: 4 :: 6 :: []

transposeTest : transpose transposeTestInput ≡ transposeTestOuput
transposeTest = refl

-------------------------
-- Exercise 2.2. Vector lookup

-- function composition
_∘_  : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
(g ∘ f) x = g (f x)

-- prove 'tabulate' and '!' are each other’s inverses

-- (a) relatively easy
lem-!-tab : ∀ {A n}
          → (f : Fin n → A) → (i : Fin n)
          → ((tabulate f) ! i) ≡ f i
lem-!-tab f  fzero   = refl                   -- (tabulate f ! fzero)  ≡ f  fzero
lem-!-tab f (fsuc i) = lem-!-tab (f ∘ fsuc) i -- (tabulate f ! fsuc i) ≡ f (fsuc i)

-- (b) trickier
lem-tab-! : forall {A n}
          → (xs : Vec A n)
          → tabulate (xs !_) ≡ xs
lem-tab-!       [] = refl
lem-tab-! (x :: xs) -- tabulate (_!_ (x :: xs)) ≡ (x :: xs)
  with tabulate (xs !_) | lem-tab-! xs
... | _y     | refl = refl -- (x :: _y) ≡ (x :: xs)
--    ^        ^
-- Vec A n     _y ≡ xs

-------------------------
-- Exercise 2.3. Sublists (see def above)

-- (a) prove reflexivity and transitivity of ⊆

-- need to name implicits since the interesting one does not come first
⊆-refl : {A : Set} {xs : List A}
       → xs ⊆ xs
⊆-refl {xs =       []} = stop
⊆-refl {xs = x :: xss} = keep (⊆-refl { xs = xss })

{-
   []    []    []
   []    []   [z]
   []   [z]   [z]
  [z]   [z]   [z]
  [z]   [z] [z,z]
  [z] [z,z] [z,z]
[z,z] [z,z] [z,z]
-}

⊆-trans : {A : Set} {xs ys zs : List A}
        → xs ⊆ ys
        →      ys ⊆ zs
        → xs ⊆      zs
--       []   []    []
⊆-trans  stop      stop     = stop

--       []   []   [z]
--      [z]  [z] [z,z]
⊆-trans       xy  (drop yz) = drop (⊆-trans xy yz)

--      []   [z]   [z]
--     [z] [z,z] [z,z]
⊆-trans (drop xy) (keep yz) = drop (⊆-trans xy yz)

--     [z]   [z]   [z]
⊆-trans (keep xy) (keep yz) = keep (⊆-trans xy yz)

⊆-trans' : {A : Set} {xs ys zs : List A}
        → xs ⊆ ys
        →      ys ⊆ zs
        → xs ⊆      zs
⊆-trans'  stop        stop     = stop
⊆-trans'  stop       (drop yz) = drop (⊆-trans'  stop     yz)
⊆-trans' (drop xy)   (drop yz) = drop (⊆-trans' (drop xy) yz)
⊆-trans' (drop xy)   (keep yz) = drop (⊆-trans'       xy  yz)
⊆-trans' (keep xy)   (drop yz) = drop (⊆-trans' (keep xy) yz)
⊆-trans' (keep xy)   (keep yz) = keep (⊆-trans'       xy  yz)

-- sublist TYPE of a specific list (compare to existing sublist RELATION above)
infixr 30 _:::_
data SubList {A : Set} : List A → Set where
  []    : SubList []
  _:::_ : forall x {xs} → SubList xs → SubList (x :: xs)
  skip  : forall {x xs} → SubList xs → SubList (x :: xs)

-- (b) extract list corresponding to a sublist
forget : {A : Set} {xs : List A}
       → SubList xs
       → List A
forget       []  = []
forget (x ::: s) = x :: forget s
forget  (skip s) =      forget s

-- (c) prove SubList is a sublist in the sense of ⊆
lem-forget : {A : Set} {xs : List A}
           → (zs : SubList xs)
           → forget zs ⊆ xs
lem-forget        []  = stop
lem-forget (x ::: zs) = keep (lem-forget zs)
lem-forget  (skip zs) = drop (lem-forget zs)

-- (d) alternative def of filter : satisfies sublist property by construction
filter' : {A : Set}
        → (A → Bool) → (xs : List A)
        → SubList xs
filter' p       []  = []
filter' p (x :: xs) with p x
... | true  = x ::: filter' p xs
... | false = skip (filter' p xs)

-- (e) complement of a sublist
complement : {A : Set} {xs : List A}
           → SubList xs
           → SubList xs
complement              []  = []
complement       (x ::: xs) = skip (complement xs)
complement (skip {x}    xs) = x ::: complement xs

module ComplementTest where
  ll : List Nat
  ll = 1 :: 2 :: 3 :: 4 :: []

  p1 : Nat → Bool
  p1 2 = true
  p1 3 = true
  p1 4 = true
  p1 _ = false

  p2 : Nat → Bool
  p2 2 = true
  p2 4 = true
  p2 _ = false

  sl1 : SubList ll
  sl1 = filter' p1 ll

  sl2 : SubList ll
  sl2 = filter' p2 ll

  sl1Test : sl1 ≡ skip (2 ::: 3 ::: 4 ::: [])
  sl1Test = refl

  sl2Test : sl2 ≡ skip (2 ::: skip (4 ::: []))
  sl2Test = refl

  c1 : SubList ll
  c1 = complement sl1

  c2 : SubList ll
  c2 = complement sl2

  cTest1 : c1 ≡ 1 ::: skip (skip (skip []))
  cTest1 = refl

  cTest2 : c2 ≡ 1 ::: skip (3 ::: skip [])
  cTest2 = refl

-- https://medium.com/@angerman/powersets-in-haskell-1df9684db52a
-- (f) compute all sublists of a given list
sublists : {A : Set}
         → (xs : List A)
         → List (SubList xs)
sublists        [] = [] :: []
sublists (x :: xs) = map (x :::_) (sublists xs) ++ (map skip (sublists xs))

-- 2^3 elements - expected output MUST be in same element ORDER as function result
sublistsTest : sublists (1 :: 2 :: 3 :: []) ≡
  (1 ::: 2 ::: 3 ::: [])  ::
  (1 ::: 2 ::: skip  [])  ::
  (1 ::: skip (3 ::: [])) ::
  (1 ::: skip (skip  [])) ::
  skip  (2 ::: 3 ::: [])  ::
  skip  (2 ::: skip  [])  ::
  skip  (skip (3 ::: [])) ::
  skip  (skip (skip  [])) ::
  []
sublistsTest = refl

{-
------------------------------------------------------------------------------
3 Programming Techniques : VIEWS and UNIVERSE constructions

--------------------------------------------------
3.1 VIEWS

matching can reveal info about term being matched AND terms INSIDE the type matched term

VIEW[5]: datatypes whose purpose is to reveal info about its indices

to use a view, define a view function
- computes an element of the view for arbitrary indices
-}

-- view datatype expressing
-- any Nat can be expressed as 2k or 2k + 1 for some k
-- element of Parity n says if n is even or odd and what k is
data Parity : Nat → Set where
  even : (k : Nat) → Parity     (k * 2)
  odd  : (k : Nat) → Parity (1 + k * 2)

parity : (n : Nat) → Parity n
parity  zero = even zero
parity (suc n) with parity n
...  | even k = odd k
...  | odd  k = even (suc k)
{-
parity (suc     .(k * 2)) | even k = odd k
parity (suc .(1 + k * 2)) | odd  k = even (suc k)
-}

half : Nat → Nat
half n with parity n
...  | even k = k
...  | odd  k = k
{-
-- Note that k is bound in the pattern for the view,
-- not in the dotted pattern for the natural number.
half     .(k * 2) | even k = k
half .(1 + k * 2) | odd  k = k
-}

-------------------------
-- FINDING AN ELEMENT IN A LIST

-- given predicate and list
-- returns if P holds for all elements
-- A proof of All P xs is a list of proofs of P x for each element x of xs.
-- P does not have to be a decidable predicate.
infixr 30 _:all:_
data All {A : Set} (P : A → Set) : List A → Set where
  all[]   :                                  All P       []
  _:all:_ : forall {x xs} → P x → All P xs → All P (x :: xs)

-- to turn a decidable predicate into a general predicate, define:
satisfies : {A : Set} → (A → Bool) → A → Set
satisfies p x = isTrue (p x)

-------------------------
-- exercise : use All to prove 2nd part of correctness of filter
-- - all elements of result satisfies the predicate
--    All (satisfies p) (filter p xs)

-- https://www.javaer101.com/en/article/18631037.html
{-
open import Relation.Binary.PropositionalEquality

filter-lem-b : {A : Set} → (p : A → Bool) → (xs : List A) → All (satisfies p) (filter p xs)
filter-lem-b p []        = vacuo
filter-lem-b p (x :: xs) with p x | inspect p x
... | true  | [ eq ] = holds _ _ (subst isTrue (sym eq) _) (filter-lem-b p xs)
... | false | [ eq ] = filter-lem-b p xs
-}

-- https://stackoverflow.com/questions/38572464/agda-type-isnt-simplified-in-with-block
lem-all-filter : {A : Set}
               → (p : A → Bool) → (xs : List A)
               → All (satisfies p) (filter p xs)
lem-all-filter p [] = all[]
--                                           isTrue   (p x)
lem-all-filter p (x :: xs) with p x | λ (y : satisfies p x) → y :all: lem-all-filter p xs
-- onTrue : (y : True) → All (λ x₁ → isTrue (p x₁)) (x :: filter p xs)
... | true  | onTrue = onTrue _
... | false |      _ = lem-all-filter p xs

-------------------------
-- VIEWS ON LISTS

-- given : decidable predicate on elements of list
-- find element in list that satisfies  predicate,
--  or else all elements satifies negation of the predicate

data Find {A : Set} (p : A → Bool) : List A → Set where
  -- does NOT specify which element to use as a witness in the found case.
  -- (If the view was always to return first (or last) matching element,
  -- force elements of xs (or ys) to satisfy the negation of p.)
  found     : (xs : List A) → (y : A) → satisfies p y → (ys : List A)
            → Find p (xs ++ y :: ys)
  not-found : forall {xs} → All (satisfies (not ◦ p)) xs
            → Find p  xs

-- view function computing an element of Find p xs for any p and xs

-- 1st attempt
{-
find1 : {A : Set} (p : A → Bool) (xs : List A) → Find p xs
find1 p [] = not-found all[]
find1 p (x :: xs) with p x
-- Need to return found on first match.
-- ({ }) is isTrue (p x), even though already matched on p x and found out that it was true.
-- Problem : when abstracting over p x did not know that needed to use the found constructor,
--    so there were no p x to abstract over.
-- WITH does not remember connection between the with-term and the pattern.
... | true  = found [] x {! !} xs
... | false = {! !}
-}

{-
A solution : make this connection explicit with a proof object.
Do NOT abstract over the term itself
- instead rather over arbitrary term of same type
  AND a proof that it is equal to the original term
-}

-- type of elements of type A AND proofs they are equal to some given x in A
data Inspect {A : Set} (x : A) : Set where
  it : (y : A) → x ≡ y → Inspect x

-- construct an element of Inspect x by picking x as thing which is equal to x.
inspect : {A : Set} → (x : A) → Inspect x
inspect x = it x refl

-- lemmas
trueIsTrue   : {x : Bool} → x ≡ true  → isTrue  x
falseIsFalse : {x : Bool} → x ≡ false → isFalse x
trueIsTrue   refl = _
falseIsFalse refl = _

{-
now define find by abstracting over inspect (p x) rather than p x
provide either a proof of p x == true or a proof of p x == false
- can be use in args to 'found' and 'not-found
-}

find : {A : Set}
     → (p : A → Bool) → (xs : List A)
     → Find p xs
find p       [] = not-found all[]
find p (x :: xs) with inspect (p x)
-- When p x is true, inspect (p x) matches 'it true prf' where prf : p x == true.
-- Use lemma to turn into proof of isTrue (p x) needed by 3rd arg of 'found'
... | it true  prf = found [] x (trueIsTrue prf) xs
... | it false prf with find p xs
find p (x :: ._) | it false _   | found xs y py ys = found (x :: xs) y py ys
-- p x is false : use lemma
find p (x :: xs) | it false prf | not-found npxs   = not-found (falseIsFalse prf :all: npxs)

-------------------------
-- INDEXING INTO A LIST

{-
Previously showed two ways of safely indexing into a list.
Both cases used type system to guarantee the index didn’t point outside the list.

In situations where there is no control over value of index (i.e., it might be outside)
a solution is to wrap result of lookup in MAYBE, but MAYBE provides no info.
-}

-- type of proofs that an element x is in a list xs.
data _∈_ {A : Set} (x : A) : List A → Set where
  hd : forall   {xs} →          x ∈ x :: xs -- 1st el is a member
  tl : forall {y xs} → x ∈ xs → x ∈ y :: xs -- any el in tail is member

-- Given proof of x ∈ xs, compute index where x occurs.
-- Count number of tls in proof.
index : forall {A} {x : A} {xs} → x ∈ xs → Nat
index  hd    = zero
index (tl p) = suc (index p)

-- view on Nat with respect to list
data Lookup {A : Set} (xs : List A) : Nat → Set where
  inside  : (x : A) → (p : x ∈ xs) → Lookup xs (index p)
  outside : (m : Nat)              → Lookup xs (length xs + m)

{-
When n is valid, get element at that position and guarantee that element is returned.
No way for 'lookup' to cheat.

When n is outside, get out-of-bounds proof showing by how much.
-}

-- now, guaranteed 'lookup' function
_!'_ : {A : Set}
     → (xs : List A) → (n : Nat)
     → Lookup xs n
[] !' n           = outside n
(x :: xs) !' zero = inside x hd
(x :: xs) !' suc n with xs !' n
...                               | inside y p = inside y (tl p)
(x :: xs) !' suc .(length xs + n) | outside n  = outside n
{-
(x :: xs) !' suc .(index p)       | inside y p = inside y (tl p)
(x :: xs) !' suc .(length xs + n) | outside n  = outside n
-}

--------------------------------------------------
-- TYPE CHECKER FOR λ-CALCULUS

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Localization.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.PathSplitEquiv
open isPathSplitEquiv

module _ {ℓα ℓs ℓt} {A : Type ℓα} {S : A → Type ℓs} {T : A → Type ℓt} where

  isLocal : ∀ (F : ∀ α → S α → T α) {ℓ} (X : Type ℓ) → Type _
  isLocal F X = ∀ α → isPathSplitEquiv (λ (g : T α → X) → g ∘ F α)

  data Localize (F : ∀ α → S α → T α) {ℓ} (X : Type ℓ) : Type (ℓ-max ℓ (ℓ-max ℓα (ℓ-max ℓs ℓt))) where
    ∣_∣ : X → Localize F X
    -- (_∘ F α) : (T α → Localize F X) → (S α → Localize F X) is a path-split equivalence ∀ α
    ext   : ∀ α → (S α → Localize F X) → (T α → Localize F X)
    isExt : ∀ α (f : S α → Localize F X) (s : S α) → ext α f (F α s) ≡ f s
    ≡ext   : ∀ α (g h : T α → Localize F X) → ((s : S α) → g (F α s) ≡ h (F α s)) → ((t : T α) → g t ≡ h t)
    ≡isExt : ∀ α g h (p : (s : S α) → g (F α s) ≡ h (F α s)) (s : S α) → ≡ext α g h p (F α s) ≡ p s

  isLocal-Localize : ∀ (F : ∀ α → S α → T α) {ℓ} (X : Type ℓ) → isLocal F (Localize F X)
  fst (sec (isLocal-Localize F X α)) f t   = ext   α f t
  snd (sec (isLocal-Localize F X α)) f i s = isExt α f s i
  fst (secCong (isLocal-Localize F X α) g h) p i t   = ≡ext   α g h (funExt⁻ p) t i
  snd (secCong (isLocal-Localize F X α) g h) p i j t = ≡isExt α g h (funExt⁻ p) t i j

ext: agda

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
module Oscar.Category.SemigroupoidAction where

open import Oscar.Category.Action
open import Oscar.Category.Setoid
open import Oscar.Category.Semigroupoid
open import Oscar.Function
open import Oscar.Level

module _ {𝔊𝔬 𝔊𝔪 𝔊𝔮} (semigroupoid : Semigroupoid 𝔊𝔬 𝔊𝔪 𝔊𝔮) where
  open Semigroupoid semigroupoid

  module _ {𝔄𝔬 𝔄𝔮} (action : Action ⋆ 𝔄𝔬 𝔄𝔮) where
    open Action action

    record IsSemigroupoidAction
      (_◂_ : ∀ {x y} → x ↦ y → ↥ x → ↥ y)
      : Set (𝔊𝔬 ⊔ 𝔊𝔪 ⊔ 𝔊𝔮 ⊔ 𝔄𝔬 ⊔ 𝔄𝔮)
      where
      field
        extensionality :
          ∀ {x} {s₁ s₂ : ↥ x} →
          s₁ ≋ s₂ →
          ∀ {y} {f₁ f₂ : x ↦ y} →
          (let instance _ = IsSetoid↦) →
          f₁ ≋ f₂ → f₁ ◂ s₁ ≋ f₂ ◂ s₂
        associativity :
          ∀ {x}
          (s : ↥ x)
          {y}
          (f : x ↦ y)
          {z}
          (g : y ↦ z) →
          (g ∙ f) ◂ s ≋ g ◂ (f ◂ s)

open IsSemigroupoidAction ⦃ … ⦄ public

record SemigroupoidAction 𝔊𝔬 𝔊𝔪 𝔊𝔮 𝔄𝔬 𝔄𝔮 : Set (lsuc (𝔊𝔬 ⊔ 𝔊𝔪 ⊔ 𝔊𝔮 ⊔ 𝔄𝔬 ⊔ 𝔄𝔮)) where
  constructor [_/_]
  field
    semigroupoid : Semigroupoid 𝔊𝔬 𝔊𝔪 𝔊𝔮
  open Semigroupoid semigroupoid public

  field
    action : Action ⋆ 𝔄𝔬 𝔄𝔮
  open Action action public

  field
    _◂_ : ∀ {x y} → x ↦ y → ↥ x → ↥ y
    ⦃ isSemigroupoidAction ⦄ : IsSemigroupoidAction semigroupoid action _◂_


text:
{-# NON_TERMINATING #-}

mutual

  record R : Set where
    inductive
    field
      x : T

  T : Set
  T = T → R

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Everything

module Test.SurjidentityI where

module _
    {𝔬₁} {𝔒₁ : Ø 𝔬₁}
    {𝔯₁} (_∼₁_ : 𝔒₁ → 𝔒₁ → Ø 𝔯₁)
    {𝔬₂} {𝔒₂ : Ø 𝔬₂}
    {𝔯₂} (_∼₂_ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂)
         (_∼₂2_ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂)
    {𝔯₂'} (_∼₂'_ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂')
    {ℓ₂} (_∼̇₂_ : ∀ {x y} → x ∼₂ y → x ∼₂ y → Ø ℓ₂)
         (_∼̇₂'_ : ∀ {x y} → x ∼₂' y → x ∼₂' y → Ø ℓ₂)
         (_∼̇₂2_ : ∀ {x y} → x ∼₂2 y → x ∼₂2 y → Ø ℓ₂)
  where
  postulate
    instance `𝓢urjection : Surjection.class 𝔒₁ 𝔒₂
    instance `𝓢urjectivity : Smap!.class _∼₁_ _∼₂_
    instance `𝓢urjectextensivity : Smap!.class _∼₁_ _∼₂'_
    instance `𝓢urjectivity2 : Smap!.class _∼₁_ _∼₂2_
    instance `𝓡eflexivity₁ : Reflexivity.class _∼₁_
    instance `𝓡eflexivity₂ : Reflexivity.class _∼₂_
    instance `𝓡eflexivity₂' : Reflexivity.class _∼₂'_
    instance `𝓡eflexivity₂2 : Reflexivity.class _∼₂2_
    instance `𝒮urjidentity : Surjidentity!.class _∼₁_ _∼₂_ _∼̇₂_
    instance `𝒮urjidentity' : Surjidentity!.class _∼₁_ _∼₂'_ _∼̇₂'_
    instance `𝒮urjidentity2 : Surjidentity!.class _∼₁_ _∼₂2_ _∼̇₂2_

  test-surj : Surjidentity!.type _∼₁_ _∼₂_ _∼̇₂_
  test-surj = surjidentity


text:
data Nat : Set where
  zero : Nat
  suc : Nat → Nat

data ⊥ : Set where

⊥-elim : {A : Set} → ⊥ → A
⊥-elim = λ where ()

⊥-elim₂ : {A : Set} → ⊥ → A → A
⊥-elim₂ = λ where () _

⊥-elim₃ : {A : Set} → A → ⊥ → A
⊥-elim₃ = λ where _ ()

data D : Set where
  c₁ : ⊥ → D
  c₂ : D

Parses : D → Set₁
Parses = λ where
  c₂      → Set
  (c₁ ())

Does-not-parse : D → Set₁
Does-not-parse = λ where
  (c₁ ())
  c₂      → Set

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Natural number types and operations requiring the axiom K.
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Data.Nat.WithK where

open import Data.Nat.Base
open import Relation.Binary.PropositionalEquality.WithK

≤″-erase : ∀ {m n} → m ≤″ n → m ≤″ n
≤″-erase (less-than-or-equal eq) = less-than-or-equal (≡-erase eq)

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.18

erase = ≤″-erase
{-# WARNING_ON_USAGE erase
"Warning: erase was deprecated in v0.18.
Please use ≤″-erase instead."
#-}


text:
{-# OPTIONS --safe --warning=error #-}

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import LogicalFormulae
open import Logic.PropositionalLogic
open import Functions.Definition
open import Numbers.Naturals.Naturals
open import Vectors
open import Boolean.Definition

module Logic.PropositionalAxiomsTautology where

axiomKTaut : {a : _} {A : Set a} (P Q : Propositions A) → Tautology (implies P (implies Q P))
axiomKTaut P Q v with inspect (Valuation.v v P)
axiomKTaut P Q v | BoolTrue with≡ pT with inspect (Valuation.v v Q)
axiomKTaut P Q v | BoolTrue with≡ pT | BoolTrue with≡ qT = Valuation.vImplicationT v (Valuation.vImplicationT v pT)
axiomKTaut P Q v | BoolTrue with≡ pT | BoolFalse with≡ qF = Valuation.vImplicationT v (Valuation.vImplicationVacuous v qF)
axiomKTaut P Q v | BoolFalse with≡ pF = Valuation.vImplicationVacuous v pF

axiomSTaut : {a : _} {A : Set a} (P Q R : Propositions A) → Tautology (implies (implies P (implies Q R)) (implies (implies P Q) (implies P R)))
axiomSTaut P Q R v with inspect (Valuation.v v P)
axiomSTaut P Q R v | BoolTrue with≡ pT with inspect (Valuation.v v Q)
axiomSTaut P Q R v | BoolTrue with≡ pT | BoolTrue with≡ qT with inspect (Valuation.v v R)
axiomSTaut P Q R v | BoolTrue with≡ pT | BoolTrue with≡ qT | BoolTrue with≡ rT = Valuation.vImplicationT v (Valuation.vImplicationT v (Valuation.vImplicationT v rT))
axiomSTaut P Q R v | BoolTrue with≡ pT | BoolTrue with≡ qT | BoolFalse with≡ rF = Valuation.vImplicationVacuous v (Valuation.vImplicationF v pT (Valuation.vImplicationF v qT rF))
axiomSTaut P Q R v | BoolTrue with≡ pT | BoolFalse with≡ qF = Valuation.vImplicationT v (Valuation.vImplicationVacuous v (Valuation.vImplicationF v pT qF))
axiomSTaut P Q R v | BoolFalse with≡ pF = Valuation.vImplicationT v (Valuation.vImplicationT v (Valuation.vImplicationVacuous v pF))

excludedMiddleTaut : {a : _} {A : Set a} (P : Propositions A) → Tautology (implies (prNot (prNot P)) P)
excludedMiddleTaut P v with inspect (Valuation.v v P)
excludedMiddleTaut P v | BoolTrue with≡ pT = Valuation.vImplicationT v pT
excludedMiddleTaut P v | BoolFalse with≡ pF = Valuation.vImplicationVacuous v (Valuation.vImplicationF v (Valuation.vImplicationVacuous v pF) (Valuation.vFalse v))

propositionalAxiomsTautology : {a : _} {A : Set a} (x : Sg ThreeElements (indexAxiom A)) → Tautology (IsSubset.ofElt propositionalAxioms x)
propositionalAxiomsTautology (One , (fst ,, snd)) = axiomKTaut fst snd
propositionalAxiomsTautology (Two , record { one = one ; two = two ; three = three }) = axiomSTaut one two three
propositionalAxiomsTautology (Three , b) = excludedMiddleTaut b


text:
-- Andreas, 2016-11-18, issue #2174
-- report and test case by Nisse

postulate
  F : Set → Set → Set

G : Set
G = {!!}

-- WAS: giving first F ? and then F ? ? lead to one of the metas not goalified.

-- Should succeed now, see script Issue2174a.sh


text:
{-# OPTIONS --without-K  #-}
module algebra.group.classifying where

open import level
open import algebra.group.core
open import algebra.group.morphism
open import equality.core
open import function.isomorphism
open import pointed.core
open import sets.unit
open import sum
open import hott.level.core
open import hott.loop.core
open import hott.truncation.core
open import hott.equivalence

module _ {i}(G : Set i) ⦃ gG : IsGroup G ⦄ where
  open import algebra.group.gset G
  open IsGroup ⦃ ... ⦄

  -- G as a G-Set
  G' : GSet i
  G' = (G , GisGSet)

  -- G as a pointed set
  G* : PSet i
  G* = (G , e)

  𝑩 : Set (lsuc i)
  𝑩 = Σ (GSet i) λ X → Trunc 1 (X ≡ G')

  base : 𝑩
  base = (G' , [ refl ])

  𝑩* : PSet (lsuc i)
  𝑩* = (𝑩 , base)

  𝑩-Ω : (base ≡ base) ≅ G
  𝑩-Ω = begin
      (base ≡ base)
    ≅⟨ sym≅ Σ-split-iso ⟩
      ( Σ (G' ≡ G') λ p
      → subst (λ X → Trunc 1 (X ≡ G')) p [ refl ] ≡ [ refl ] )
    ≅⟨ (Σ-ap-iso refl≅ λ p → contr-⊤-iso (Trunc-level 1 _ _)) ·≅ ×-right-unit ⟩
      (G' ≡ G')
    ≅⟨ GSet-univalence G ⦃ xG = GisGSet ⦄ G ⦃ yG = GisGSet ⦄ ⟩
      ( Σ (GSetMorphism G ⦃ xG = GisGSet ⦄ G ⦃ yG = GisGSet ⦄) λ { (f , _)
        → weak-equiv f } )
    ≅⟨ (Σ-ap-iso' (GSet-repr-iso is-set ⦃ xG = GisGSet ⦄) λ _ → refl≅) ⟩
      ( Σ G λ { g → weak-equiv (λ x → x * g) } )
    ≅⟨ ( Σ-ap-iso refl≅ λ g → contr-⊤-iso ( lem g , h1⇒prop (we-h1 _) _ ) )
        ·≅ ×-right-unit ⟩
      G
    ∎
    where
      open ≅-Reasoning
      lem : (g : G) → weak-equiv (λ x → x * g)
      lem g = proj₂ (≅'⇒≈ (≅⇒≅' (right-translation-iso g)))

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
{-# OPTIONS -v treeless.opt:20 #-}
module _ where

open import Agda.Builtin.Nat using (_<_)
open import Common.Prelude
open import Common.Integer

-- Should compile to
--   λ a b → case a of
--              "neg" → 0 - b
--              _     → b
match-on-lit : String → Integer → Integer
match-on-lit "neg" x with x
...                     | pos (suc n) = negsuc n
...                     | pos 0       = pos 0
...                     | negsuc n    = pos (suc n)
match-on-lit _     x = x

-- This doesn't compile as nicely, since the match on "neg"
-- ends up between the match on the int and the nat (not sure why).
match-on-lit₂ : String → Integer → Integer
match-on-lit₂ "neg" (pos (suc n)) = negsuc n
match-on-lit₂ "neg" (negsuc n)    = pos (suc n)
match-on-lit₂ _     x             = x

-- Should compile to a flat case
nested-match : Integer → String
nested-match (pos 0) = "zero"
nested-match (pos 1) = "one"
nested-match (pos (suc (suc n))) = "lots"
nested-match (negsuc 0) = "minus one"
nested-match (negsuc 1) = "minus two"
nested-match (negsuc (suc (suc n))) = "minus lots"

data Diff : Set where
  less : Nat → Diff
  equal : Diff
  greater : Nat → Diff

compareNat : Nat → Nat → Diff
compareNat a b with a < b
... | true = less (b ∸ suc a)
... | false with b < a
...   | true  = greater (a ∸ suc b)
...   | false = equal
{-# INLINE compareNat #-}

-- Should compile to 0 - a
neg : Nat → Integer
neg zero    = pos zero
neg (suc a) = negsuc a
{-# INLINE neg #-}

-- Should compile to a - b
_-N_ : Nat → Nat → Integer
a -N b with compareNat a b
... | less k    = negsuc k
... | equal     = pos (a ∸ b)
... | greater k = pos (suc k)
{-# INLINE _-N_ #-}

-- Should compile to a + b
_+Z_ : Integer → Integer → Integer
pos    a +Z pos    b = pos (a + b)
pos    a +Z negsuc b = a -N suc b
negsuc a +Z pos    b = b -N suc a
negsuc a +Z negsuc b = negsuc (suc a + b)
{-# INLINE _+Z_ #-}

-- Should compile to a * b
_*Z_ : Integer → Integer → Integer
pos    a *Z pos    b = pos (a * b)
pos    a *Z negsuc b = neg (a * suc b)
negsuc a *Z pos    b = neg (suc a * b)
negsuc a *Z negsuc b = pos (suc a * suc b)
{-# INLINE _*Z_ #-}

printInt : Integer → IO Unit
printInt x = putStrLn (intToString x)

main : IO Unit
main = printInt (match-on-lit "neg" (pos 42))
    ,, printInt (match-on-lit₂ "neg" (pos 42))
    ,, putStrLn (nested-match (negsuc 5))


text:
{-# OPTIONS --cubical --no-import-sorts #-}

module Spaces where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)

private
  variable
    ℓ ℓ' ℓ'' : Level

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Structures.CommRing
open import Cubical.Relation.Nullary.Base -- ¬_
open import Cubical.Relation.Binary.Base
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Empty renaming (elim to ⊥-elim) -- `⊥` and `elim`
-- open import Cubical.Structures.Poset
open import Cubical.Foundations.Function
open import Cubical.Structures.Ring
open import Cubical.Structures.AbGroup
open import Cubical.Foundations.Logic renaming (¬_ to ¬ᵖ_)

open import Function.Base using (_∋_)
-- open import Function.Reasoning using (∋-syntax)
open import Function.Base using (it) -- instance search

{-
| name                                    | carrier | module | metric | norm | inner | basis | cauchy |
|-----------------------------------------|---------|--------|--------|------|-------|-------|--------|
| VectorSpace                             |   any   |   K    |        |      |       |       |        |
| FiniteDimVectorSpace                    |   any   |   K    |        |      |       |   ✓   |        |
| NormedVectorSpace                       |   any   |   K    |   (✓)  |   ✓  |       |       |        |
| FiniteDimNormedVectorSpace              |   any   |   K    |   (✓)  |   ✓  |       |   ✓   |        |
| CompleteNormedVectorSpace               |   any   |   K    |   (✓)  |   ✓  |       |       |   ✓    |
| FiniteDimCompleteNormedVectorSpace      |   any   |   K    |   (✓)  |   ✓  |       |   ✓   |   ✓    |
| InnerProductSpace                       |   any   |   K    |   (✓)  |  (✓) |   ✓   |       |        |
| FiniteDimInnerProductSpace              |   any   |   K    |   (✓)  |  (✓) |   ✓   |   ✓   |        |
| CompleteInnerProductSpace               |   any   |   K    |   (✓)  |  (✓) |   ✓   |       |   ✓    |
| FiniteDimCompleteInnerProductSpace      |   any   |   K    |   (✓)  |  (✓) |   ✓   |   ✓   |   ✓    |
| FiniteDimCompleteInnerProductSpaceOverℝ |    ℝ    |   ℝ    |   (✓)  |  (✓) |   ✓   |   ✓   |   ✓    |
-}

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
{-# OPTIONS --cubical --no-import-sorts #-}

open import Bundles

module Properties.AlmostOrderedField {ℓ ℓ'} (AOF : AlmostOrderedField {ℓ} {ℓ'}) where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)

private
  variable
    ℓ'' : Level

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Relation.Nullary.Base -- ¬_
open import Cubical.Relation.Binary.Base
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Empty renaming (elim to ⊥-elim) -- `⊥` and `elim`

open import Function.Base using (_∋_)
open import Function.Base using (it) -- instance search

import MoreLogic
open MoreLogic.Reasoning
import MoreAlgebra

-- Lemma 4.1.11.
-- In the presence of the first five axioms of Definition 4.1.10, conditions (†) and (∗) are together equivalent to the condition that for all x, y, z : F,
--  1. x ≤ y ⇔ ¬(y < x),
--  2. x # y ⇔ (x < y) ∨ (y < x)
--  3. x ≤ y ⇔ x + z ≤ y + z,
--  4. x < y ⇔ x + z < y + z,
--  5. 0 < x + y ⇒ 0 < x ∨ 0 < y,
--  6. x < y ≤ z ⇒ x < z,
--  7. x ≤ y < z ⇒ x < z,
--  8. x ≤ y ∧ 0 ≤ z ⇒ x z ≤ y z,
--  9. 0 < z ⇒ (x < y ⇔ x z < y z),
-- 10. 0 < 1.

open AlmostOrderedField AOF renaming (Carrier to F)
import Cubical.Structures.Ring
open Cubical.Structures.Ring.Theory (record {AlmostOrderedField AOF})
open MoreAlgebra.Properties.Group   (record {AlmostOrderedField AOF renaming (+-isGroup to isGroup )})

-- NOTE: ported from Cubical.Structures.Group.GroupLemmas
-- NOTE: these versions differ from the Group-versions because they are defined w.r.t. an appartness relation _#_ that is not present for the Group
simplR : {a b : F} (c : F) {{_ : c # 0f}} → a · c ≡ b · c → a ≡ b
simplR {a} {b} c {{_}} a·c≡b·c =
   a                ≡⟨ sym (fst (·-identity a)) ∙ cong (a ·_) (sym (·-rinv c it)) ∙ ·-assoc _ _ _ ⟩
  (a · c) · (c ⁻¹ᶠ) ≡⟨ cong (_· c ⁻¹ᶠ) a·c≡b·c ⟩
  (b · c) · (c ⁻¹ᶠ) ≡⟨ sym (·-assoc _ _ _) ∙ cong (b ·_) (·-rinv c it) ∙ fst (·-identity b)  ⟩
   b ∎

·-preserves-≡ʳ : {a b : F} (c : F) {{_ : c # 0f}} → a · c ≡ b · c → a ≡ b
·-preserves-≡ʳ = simplR

-- ·-linv-unique : (x y : F) (x·y≡1 : (x ·₁ y) ≡ 1f) → x ≡ (y ⁻¹ᶠ₁)
module _ (x y : F) (x·y≡1 : x · y ≡ 1f) where
  y#0 = snd (·-inv-back _ _ x·y≡1) -- duplicated inhabitant (see notes)
  instance _ = y # 0f ∋ y#0
  import Cubical.Structures.Group

  -- NOTE: ported from Cubical.Structures.Group.GroupLemmas
  abstract
    ·-linv-unique' : Σ[ p ∈ y # 0f ] (x ≡ _⁻¹ᶠ y {{p}})
    ·-linv-unique' = it , (
      x · y ≡ 1f        ⇒⟨ transport (λ i → x · y ≡ ·-linv y it (~ i)) ⟩
      x · y ≡ y ⁻¹ᶠ · y ⇒⟨ simplR _  ⟩
      x     ≡ y ⁻¹ᶠ     ◼) x·y≡1

·-linv-unique : (x y : F) → ((x · y) ≡ 1f) → Σ[ p ∈ y # 0f ] x ≡ (_⁻¹ᶠ y {{p}})
·-linv-unique = ·-linv-unique'

-- ⁻¹ᶠ-involutive : (x : F) (z#0 : x #' 0f) → ((x ⁻¹ᶠ₁) ⁻¹ᶠ₁) ≡ x
module _ (z : F) (z#0 : z # 0f) where
  private
    instance _ = z#0
    z⁻¹ = z ⁻¹ᶠ -- NOTE: interestingly, the instance argument is not applied and y remains normalized in terms of z
              --       so we get `y : {{ _ : z #' 0f }} → F` here
    z⁻¹#0 = snd (·-inv-back z z⁻¹ (·-rinv z it))
    -- NOTE: for some reason I get "There are instances whose type is still unsolved when checking that the expression it has type z #' 0f"
    --       typing `y : F` did not help much. therefore this goes in two lines
    instance _ = z⁻¹#0
    z⁻¹⁻¹ = z⁻¹ ⁻¹ᶠ

  -- NOTE: this should be similar to `right-helper` + `-involutive`
  ⁻¹ᶠ-involutive : (z ⁻¹ᶠ) ⁻¹ᶠ ≡ z
  ⁻¹ᶠ-involutive = (
     z⁻¹⁻¹              ≡⟨ sym (fst (·-identity _)) ⟩
     z⁻¹⁻¹ ·      1f    ≡⟨ (λ i →  z⁻¹⁻¹ · ·-linv _ it (~ i)) ⟩
     z⁻¹⁻¹ · (z⁻¹  · z) ≡⟨ ·-assoc _ _ _ ⟩
    (z⁻¹⁻¹ ·  z⁻¹) · z  ≡⟨ (λ i → ·-linv z⁻¹ it i · z) ⟩
          1f       · z  ≡⟨  snd (·-identity _)  ⟩
                     z  ∎)

module forward -- 6. ⇒ 1. 2. 3. 4. 5.
  -- 6. (†)
  (+-<-extensional : ∀ w x y z → (x + y) < (z + w) → (x < z) ⊎ (y < w))
  -- 6. (∗)
  (·-preserves-< : ∀ x y z → 0f < z → x < y → (x · z) < (y · z))
  where
  -- abstract
    --  1. x ≤ y ⇔ ¬(y < x),
    item-1 : ∀ x y → x ≤ y → ¬(y < x)
    item-1 = λ _ _ x≤y → x≤y -- holds definitionally

    item-1-back : ∀ x y → ¬(y < x) → x ≤ y
    item-1-back = λ _ _ ¬[y<x] → ¬[y<x]

    --  2. x # y ⇔ (x < y) ∨ (y < x)
    item-2 : ∀ x y → x # y → (x < y) ⊎ (y < x)
    item-2 = λ _ _ x#y → x#y -- holds definitionally

    item-2-back : ∀ x y → (x < y) ⊎ (y < x) → x # y
    item-2-back = λ _ _ [x<y]⊎[y<x] → [x<y]⊎[y<x] -- holds definitionally

    -- NOTE: just a plain copy of the previous proof
    +-preserves-< : ∀ a b x → a < b → a + x < b + x
    +-preserves-< a b x a<b = (
       a            <  b            ⇒⟨ transport (λ i → sym (fst (+-identity a)) i < sym (fst (+-identity b)) i) ⟩
       a +    0f    <  b +    0f    ⇒⟨ transport (λ i → a + sym (+-rinv x) i < b + sym (+-rinv x) i) ⟩
       a + (x  - x) <  b + (x  - x) ⇒⟨ transport (λ i → +-assoc a x (- x) i < +-assoc b x (- x) i) ⟩
      (a +  x) - x  < (b +  x) - x  ⇒⟨ +-<-extensional (- x) (a + x) (- x) (b + x) ⟩
      (a + x < b + x) ⊎ (- x < - x) ⇒⟨ (λ{ (inl a+x<b+x) → a+x<b+x -- somehow ⊥-elim needs a hint in the next line
                                         ; (inr  -x<-x ) → ⊥-elim {A = λ _ → (a + x < b + x)} (<-irrefl (- x) -x<-x) }) ⟩
       a + x < b + x ◼) a<b

    +-preserves-<-back : ∀ x y z → x + z < y + z → x < y
    +-preserves-<-back x y z =
      ( x + z < y + z              ⇒⟨ +-preserves-< _ _ (- z) ⟩
        (x + z) - z  < (y + z) - z ⇒⟨ transport (λ i → +-assoc x z (- z) (~ i) < +-assoc y z (- z) (~ i)) ⟩
        x + (z - z) < y + (z - z)  ⇒⟨ transport (λ i → x + +-rinv z i < y + +-rinv z i) ⟩
        x + 0f < y + 0f            ⇒⟨ transport (λ i → fst (+-identity x) i < fst (+-identity y) i) ⟩
        x < y ◼)

    --  3. x ≤ y ⇔ x + z ≤ y + z,
    item-3 : ∀ x y z → x ≤ y → x + z ≤ y + z
    item-3 x y z = (
       x     ≤ y          ⇒⟨ (λ z → z) ⟩ -- unfold the definition
      (y     < x     → ⊥) ⇒⟨ (λ f → f ∘ (+-preserves-<-back y x z) ) ⟩
      (y + z < x + z → ⊥) ⇒⟨ (λ z → z) ⟩ -- refold the definition
       x + z ≤ y + z ◼)

    item-3-back : ∀ x y z → x + z ≤ y + z → x ≤ y
    item-3-back x y z = (
       x + z ≤ y + z      ⇒⟨ (λ z → z) ⟩ -- unfold the definition
      (y + z < x + z → ⊥) ⇒⟨ (λ f p → f (+-preserves-< y x z p)) ⟩ -- just a variant of the above
      (y     < x     → ⊥) ⇒⟨ (λ z → z) ⟩ -- refold the definition
       x     ≤ y ◼)

    --  4. x < y ⇔ x + z < y + z,
    item-4 : ∀ x y z → x < y → x + z < y + z
    item-4 = +-preserves-<

    item-4-back : ∀ x y z → x + z < y + z → x < y
    item-4-back = +-preserves-<-back

    --  5. 0 < x + y ⇒ 0 < x ∨ 0 < y,
    item-5 : ∀ x y → 0f < x + y → (0f < x) ⊎ (0f < y)
    item-5 x y = (
      (0f      < x + y) ⇒⟨ transport (λ i → fst (+-identity 0f) (~ i) < x + y) ⟩
      (0f + 0f < x + y) ⇒⟨ +-<-extensional y 0f 0f x ⟩
      (0f < x) ⊎ (0f < y) ◼)

    --  6. x < y ≤ z ⇒ x < z,
    item-6 : ∀ x y z → x < y → y ≤ z → x < z
    item-6 x y z x<y y≤z = (
       x      <  y      ⇒⟨ +-preserves-< _ _ _ ⟩
       x + z  <  y + z  ⇒⟨ transport (λ i → x + z < +-comm y z i) ⟩
       x + z  <  z + y  ⇒⟨ +-<-extensional y x z z  ⟩
      (x < z) ⊎ (z < y) ⇒⟨ (λ{ (inl x<z) → x<z
                             ; (inr z<y) → ⊥-elim (y≤z z<y) }) ⟩
       x < z  ◼) x<y

    --  7. x ≤ y < z ⇒ x < z,
    item-7 : ∀ x y z → x ≤ y → y < z → x < z
    item-7 x y z x≤y = ( -- very similar to the previous one
       y      <  z      ⇒⟨ +-preserves-< y z x ⟩
       y + x  <  z + x  ⇒⟨ transport (λ i → +-comm y x i < z + x) ⟩
       x + y  <  z + x  ⇒⟨ +-<-extensional x x y z ⟩
      (x < z) ⊎ (y < x) ⇒⟨ (λ{ (inl x<z) → x<z
                             ; (inr y<x) → ⊥-elim (x≤y y<x)}) ⟩
       x < z  ◼)

    item-10 : 0f < 1f

    module _ (z : F) (0<z : 0f < z) where
      private
        instance _ = z # 0f ∋ inr 0<z
        z⁻¹ = z ⁻¹ᶠ
        z⁻¹#0 = snd (·-inv-back z z⁻¹ (·-rinv z it))
      abstract
        ⁻¹ᶠ-preserves-sign : 0f < z ⁻¹ᶠ
        ⁻¹ᶠ-preserves-sign with z⁻¹#0
        ... | inl z⁻¹<0 = (
          z⁻¹     < 0f     ⇒⟨ ·-preserves-< _ _ z 0<z ⟩
          z⁻¹ · z < 0f · z ⇒⟨ transport (λ i → ·-linv z it i <  0-leftNullifies z i) ⟩
          1f      < 0f     ⇒⟨ <-trans _ _ _ item-10 ⟩
          0f      < 0f     ⇒⟨ <-irrefl _ ⟩
                  ⊥        ⇒⟨ ⊥-elim ⟩ _ ◼) z⁻¹<0
        ... | inr 0<z⁻¹ = 0<z⁻¹

    --  8. x ≤ y ∧ 0 ≤ z ⇒ x z ≤ y z,
    item-8 : ∀ x y z → x ≤ y → 0f ≤ z → x · z ≤ y · z
    -- For item 8, suppose x ≤ y and 0 ≤ z and yz < xz.
    item-8 x y z x≤y 0≤z y·z<x·z = let
      -- Then 0 < z (x − y) by (†),
      i   = (  y · z            <  x · z                ⇒⟨ transport (λ i → ·-comm y z i < ·-comm x z i) ⟩
               z · y            <  z · x                ⇒⟨ +-preserves-< _ _ _ ⟩
              (z · y) - (z · y) < (z · x) - (z ·    y ) ⇒⟨ transport (cong₂ _<_ (+-rinv (z · y))
                                                             ( λ i → (z · x) + sym (-commutesWithRight-· z y) i )) ⟩
                             0f < (z · x) + (z · (- y)) ⇒⟨ transport (cong₂ _<_ refl (sym (fst (dist z x (- y))))) ⟩ -- [XX]
                             0f <  z · (x - y) ◼) y·z<x·z
      instance _ = z · (x - y) # 0f ∋ inr i
      -- and so, being apart from 0, z (x − y) has a multiplicative inverse w.
      w   = (z · (x - y)) ⁻¹ᶠ
      ii  : 1f ≡ (z · (x - y)) · w
      ii  = sym (·-rinv _ _)
      -- Hence z itself has a multiplicative inverse w (x − y),
      iii : 1f ≡ z · ((x - y) · w)
      iii = transport (λ i → 1f ≡ ·-assoc z (x - y) w (~ i)) ii
      instance z#0f = z # 0f ∋ fst (·-inv-back _ _ (sym iii))
      -- and so 0 < z ∨ z < 0, where the latter case contradicts the assumption 0 ≤ z, so that we have 0 < z.
      instance _    = 0f < z ∋ case z#0f of λ where
                      (inl z<0) → ⊥-elim (0≤z z<0)
                      (inr 0<z) → 0<z
      -- Now w (x − y) has multiplicative inverse z, so it is apart from 0,
      iv  :  (x - y) · w # 0f
      iv  = snd (·-inv-back _ _ (sym iii))
      -- that is (0 < w (x − y)) ∨ (w (x − y) < 0).
      in case iv of λ where
        -- By (∗), from 0 < w (x − y) and yz < xz we get yzw (x − y) < xzw (x − y), so y < x, contradicting our assumption that x ≤ y.
        (inr 0<[x-y]·w) → (
           y ·  z                   <  x ·  z                    ⇒⟨ ·-preserves-< _ _ _ 0<[x-y]·w ⟩
          (y ·  z) · ((x - y) · w)  < (x ·  z) · ((x - y) · w)   ⇒⟨ transport (λ i →
                                                                        (·-assoc y z ((x - y) · w)) (~ i)
                                                                      < (·-assoc x z ((x - y) · w)) (~ i)) ⟩
           y · (z  · ((x - y) · w)) <  x · (z  · ((x - y) · w))  ⇒⟨ transport (λ i →
                                                                       y · (iii (~ i)) < x · (iii (~ i))) ⟩
           y · 1f                   <  x · 1f                    ⇒⟨ transport (cong₂ _<_
                                                                      (fst (·-identity y)) (fst (·-identity x))) ⟩
           y                        <  x                         ⇒⟨ x≤y ⟩
          ⊥ ◼) y·z<x·z
        -- In the latter case, from (∗) we get zw (x − y) < 0, i.e.
        -- 1 < 0 which contradicts item 10, so that we have 0 < w (x − y).
        (inl p) → (
               (x - y) · w      < 0f     ⇒⟨ ·-preserves-< _ _ _ it ⟩
              ((x - y) · w) · z < 0f · z ⇒⟨ transport (cong₂ _<_ (·-comm _ _) (0-leftNullifies z)) ⟩
          z · ((x - y) · w)     < 0f     ⇒⟨ ( transport λ i → iii (~ i) < 0f) ⟩
                             1f < 0f     ⇒⟨ <-trans _ _ _  item-10 ⟩
                             0f < 0f     ⇒⟨ <-irrefl _ ⟩
          ⊥ ◼) p

    --  9. 0 < z ⇒ (x < y ⇔ x z < y z),
    item-9 : ∀ x y z → 0f < z → (x < y → x · z < y · z)
    item-9 = ·-preserves-<

    item-9-back : ∀ x y z → 0f < z → (x · z < y · z → x < y)
    -- For the other direction of item 9, assume 0 < z and xz < yz,
    item-9-back x y z 0<z x·z<y·z = let
      instance _ = (          x · z  <  y · z            ⇒⟨ +-preserves-< _ _ _ ⟩
                   (x · z) - (x · z) < (y · z) - (x · z) ⇒⟨ transport (cong₂ _<_ (+-rinv (x · z)) refl) ⟩
                                  0f < (y · z) - (x · z) ◼) x·z<y·z
               _ = (y · z) - (x · z) # 0f ∋ inr it
      -- so that yz − xz has a multiplicative inverse w,
      w = ((y · z) - (x · z)) ⁻¹ᶠ
      o = ( (y · z) - (   x  · z) ≡⟨ ( λ i → (y · z) + (-commutesWithLeft-· x z) (~ i)) ⟩
            (y · z) + ((- x) · z) ≡⟨ sym (snd (dist y (- x) z)) ⟩
            (y - x) · z ∎)
      instance _ = (y - x) · z # 0f ∋  transport (λ i → o i # 0f) it
      -- and so z itself has multiplicative inverse w (y − x).
      1≡z·[w·[y-x]] = γ
      iii = 1≡z·[w·[y-x]]
      1≡[w·[y-x]]·z : 1f ≡ (w · (y - x)) · z
      1≡[w·[y-x]]·z = transport (λ i → 1f ≡ ·-comm z (w · (y - x)) i) 1≡z·[w·[y-x]]
      -- Then since 0 < z and xz < yz, by (∗), we get xzw (y − x) < yzw (y − x), and hence x < y.
      instance _ = z # 0f ∋ inr 0<z
      z⁻¹ = w · (y - x)
      z⁻¹≡w·[y-x] : z ⁻¹ᶠ ≡ (w · (y - x))
      z⁻¹≡w·[y-x] = let tmp = sym (snd (·-linv-unique (w · (y - x)) z (sym 1≡[w·[y-x]]·z)))
                    in transport (cong (λ z#0 → _⁻¹ᶠ z {{z#0}} ≡ (w · (y - x))) (#-isProp z 0f _ _)) tmp
      0<z⁻¹ : 0f < z ⁻¹ᶠ
      0<z⁻¹ = ⁻¹ᶠ-preserves-sign z 0<z
      instance _ = 0f < w · (y - x) ∋ transport (λ i → 0f < z⁻¹≡w·[y-x] i) 0<z⁻¹
      -- instance _ = 0f < z⁻¹ ∋ ?
      in (  x ·  z         <  y ·  z         ⇒⟨ ·-preserves-< _ _ z⁻¹ it ⟩
           (x ·  z) · z⁻¹  < (y ·  z) · z⁻¹  ⇒⟨ transport (λ i → ·-assoc x z z⁻¹ (~ i) < ·-assoc y z z⁻¹ (~ i)) ⟩
            x · (z  · z⁻¹) <  y · (z  · z⁻¹) ⇒⟨ transport (λ i → x · iii (~ i) < y · iii (~ i)) ⟩
            x · 1f         <  y · 1f         ⇒⟨ transport (cong₂ _<_ (fst (·-identity x)) (fst (·-identity y))) ⟩
            x              <  y              ◼) x·z<y·z
      where
        abstract -- NOTE: `abstract` is only allowed in `where` blocks and `where` blocks are not allowed in `let` blocks
          γ =
            let -- NOTE: for some reason the instance resolution does only work in let-blocks
            -- I get a "Terms marked as eligible for instance search should end with a name, so `instance' is ignored here. when checking the definition of my-instance"
            instance my-instance = (          x · z  <  y · z            ⇒⟨ +-preserves-< _ _ _ ⟩
                         (x · z) - (x · z) < (y · z) - (x · z) ⇒⟨ transport (cong₂ _<_ (+-rinv (x · z)) refl) ⟩
                                        0f < (y · z) - (x · z) ◼) x·z<y·z
                     _ = (y · z) - (x · z) # 0f ∋ inr it
            -- so that yz − xz has a multiplicative inverse w,
            w = ((y · z) - (x · z)) ⁻¹ᶠ
            o = ( (y · z) - (   x  · z) ≡⟨ ( λ i → (y · z) + (-commutesWithLeft-· x z) (~ i)) ⟩
                  (y · z) + ((- x) · z) ≡⟨ sym (snd (dist y (- x) z)) ⟩
                  (y - x) · z ∎)
            instance _ = (y - x) · z # 0f ∋  transport (λ i → o i # 0f) it
            in (
              1f                      ≡⟨ (λ i → ·-linv ((y · z) - (x · z)) it (~ i)) ⟩
              w · ((y · z) - (x · z)) ≡⟨ (λ i → w · o i) ⟩
              w · ((y - x) · z)       ≡⟨ (λ i → w · ·-comm (y - x) z i ) ⟩
              w · (z · (y - x))       ≡⟨ (λ i → ·-assoc w z (y - x) i) ⟩
              (w · z) · (y - x)       ≡⟨ (λ i → ·-comm w z i · (y - x)) ⟩
              (z · w) · (y - x)       ≡⟨ (λ i → ·-assoc z w (y - x) (~ i)) ⟩
              z · (w · (y - x))       ∎)

    -- 10. 0 < 1.
    item-10 with snd (·-inv-back _ _ (fst (·-identity 1f)))
    -- For item 10, since 1 has multiplicative inverse 1, it is apart from 0, hence 0 < 1 ∨ 1 < 0.
    ... | inl 1<0 =
      -- If 1 < 0 then by item 4 we have 0 < −1 and so by (∗) we get 0 < (−1) · (−1), that is, 0 < 1, so by transitivity 1 < 1, contradicting irreflexivity of <.
       (1f          < 0f                ⇒⟨ +-preserves-< 1f 0f (- 1f) ⟩
        1f    - 1f  < 0f - 1f           ⇒⟨ transport (λ i → +-rinv 1f i < snd (+-identity (- 1f)) i) ⟩
        0f          <    - 1f           ⇒⟨ ( λ 0<-1 → ·-preserves-< 0f (- 1f) (- 1f) 0<-1 0<-1) ⟩
        0f · (- 1f) <   (- 1f) · (- 1f) ⇒⟨ transport (cong₂ _<_ (0-leftNullifies (- 1f)) refl) ⟩
        0f          <   (- 1f) · (- 1f) ⇒⟨ transport (λ i → 0f < -commutesWithRight-· (- 1f) (1f)   i ) ⟩
        0f          < -((- 1f) ·    1f )⇒⟨ transport (λ i → 0f < -commutesWithLeft-·  (- 1f)  1f (~ i)) ⟩
        0f          < (-(- 1f))·    1f  ⇒⟨ transport (λ i → 0f < -involutive 1f i · 1f) ⟩
        0f          <      1f  ·    1f  ⇒⟨ transport (λ i → 0f < fst (·-identity 1f) i) ⟩
        0f          <      1f           ⇒⟨ <-trans _ _ _ 1<0 ⟩
        1f          <      1f           ⇒⟨ <-irrefl 1f ⟩
                    ⊥                   ⇒⟨ ⊥-elim ⟩ _ ◼) 1<0
    ... | inr 0<1 = 0<1

-- Conversely, assume the 10 listed items—in particular, items 4, 5 and 9.
module back -- 1. 2. 3. 4. 5. ⇒ 6.
  -- (item-1      : ∀ x y → x ≤ y → ¬(y < x))
  -- (item-1-back : ∀ x y → ¬(y < x) → x ≤ y)
  -- (item-2      : ∀ x y → x # y → (x < y) ⊎ (y < x))
  -- (item-2-back : ∀ x y → (x < y) ⊎ (y < x) → x # y)
  -- (item-3      : ∀ x y z → x ≤ y → x + z ≤ y + z)
  -- (item-3-back : ∀ x y z → x + z ≤ y + z → x ≤ y)
     (item-4      : ∀ x y z → x < y → x + z < y + z)
  -- (item-4-back : ∀ x y z → x + z < y + z → x < y)
     (item-5      : ∀ x y → 0f < x + y → (0f < x) ⊎ (0f < y))
  -- (item-6      : ∀ x y z → x < y → y ≤ z → x < z)
  -- (item-7      : ∀ x y z → x ≤ y → y < z → x < z)
  -- (item-8      : ∀ x y z → x ≤ y → 0f ≤ z → x · z ≤ y · z)
     (item-9      : ∀ x y z → 0f < z → (x < y → x · z < y · z))
  -- (item-9-back : ∀ x y z → 0f < z → (x · z < y · z → x < y))
  -- (item-10     : 0f < 1f)
  where

  item-4' : ∀ x y → 0f < x - y → y < x
  item-4' x y = (
    0f     <  x - y         ⇒⟨ item-4 0f (x + (- y)) y ⟩
    0f + y < (x - y) + y    ⇒⟨ transport (λ i → snd (+-identity y) i < sym (+-assoc x (- y) y) i) ⟩
         y <  x + (- y + y) ⇒⟨ transport (λ i → y < x + snd (+-inv y) i) ⟩
         y <  x + 0f        ⇒⟨ transport (λ i → y < fst (+-identity x) i)  ⟩
         y <  x ◼)

  lemma : ∀ x y z w → (z +   w) + ((- x)  + (- y)) ≡ (z - x) + (w - y)
  lemma x y z w = (
    -- NOTE: there has to be a shorter way to to this kind of calculations ...
    --       also I got not much introspection while creating the paths
    (z +   w) + ((- x)  + (- y))   ≡⟨ ( λ i → +-assoc z w ((- x)  + (- y)) (~ i)) ⟩
    (z + ( w  + ((- x)  + (- y)))) ≡⟨ ( λ i → z + (+-assoc w (- x) (- y) i)) ⟩
    (z + ((w  +  (- x)) + (- y)))  ≡⟨ ( λ i → z + ((+-comm w (- x) i) + (- y)) ) ⟩
    (z + (((- x) +  w)  + (- y)))  ≡⟨ ( λ i → z + (+-assoc (- x) w (- y) (~ i))) ⟩
    (z + (( - x) + (w - y)))       ≡⟨ ( λ i → +-assoc z (- x) (w  - y) i ) ⟩
    (z - x) + (w - y) ∎)

  -- 6. (†)
  -- In order to show (†), suppose x + y < z + w.
  -- So, by item 4, we get (x + y) − (x + y) < (z + w) − (x + y), that is, 0 < (z − x) + (w − y).
  -- By item 5, (0 < z − x) ∨ (0 < w − y), and so by item 4 in either case, we get x < z ∨ y < w.
  +-<-extensional : ∀ w x y z → (x + y) < (z + w) → (x < z) ⊎ (y < w)
  +-<-extensional w x y z = (
    (x + y)           < (z + w)           ⇒⟨ item-4 (x + y) (z + w) (- (x + y)) ⟩
    (x + y) - (x + y) < (z + w) - (x + y)
      ⇒⟨ transport (λ i → +-rinv (x + y) i < (z + w) + (-isDistributive x y) (~ i))    ⟩

                   0f < (z +   w) + ((- x)  + (- y))   ⇒⟨ transport (λ i → 0f < lemma x y z w i) ⟩
                   0f < (z - x) + (w - y) ⇒⟨ item-5 (z - x) (w - y) ⟩
    (0f < z - x) ⊎ (0f < w - y)           ⇒⟨ (λ{ (inl p) → inl (item-4' z x p)
                                               ; (inr p) → inr (item-4' w y p)}) ⟩
    ( x < z    ) ⊎ ( y < w    ) ◼)

  -- 6. (∗)
  ·-preserves-< : ∀ x y z → 0f < z → x < y → (x · z) < (y · z)
  ·-preserves-< = item-9


text:
module Oscar.Property.Transitivity where

open import Oscar.Level

record Transitivity {𝔬} {⋆ : Set 𝔬} {𝔮} (_↦_ : ⋆ → ⋆ → Set 𝔮) : Set (𝔬 ⊔ 𝔮) where
  field
    transitivity : ∀ {x y} → x ↦ y → ∀ {z} → y ↦ z → x ↦ z

open Transitivity ⦃ … ⦄ public


text:
------------------------------------------------------------------------
-- Sums (disjoint unions)
------------------------------------------------------------------------

module Data.Sum where

open import Data.Function
open import Data.Maybe.Core

------------------------------------------------------------------------
-- Definition

infixr 1 _⊎_

data _⊎_ (A B : Set) : Set where
  inj₁ : (x : A) → A ⊎ B
  inj₂ : (y : B) → A ⊎ B

------------------------------------------------------------------------
-- Functions

[_,_] : ∀ {A B} {C : A ⊎ B → Set} →
        ((x : A) → C (inj₁ x)) → ((x : B) → C (inj₂ x)) →
        ((x : A ⊎ B) → C x)
[ f , g ] (inj₁ x) = f x
[ f , g ] (inj₂ y) = g y

[_,_]′ : ∀ {A B C : Set} → (A → C) → (B → C) → (A ⊎ B → C)
[_,_]′ = [_,_]

map : ∀ {a b c d} → (a → c) → (b → d) → (a ⊎ b → c ⊎ d)
map f g = [ inj₁ ∘ f , inj₂ ∘ g ]

infixr 1 _-⊎-_

_-⊎-_ : ∀ {a b} → (a → b → Set) → (a → b → Set) → (a → b → Set)
f -⊎- g = f -[ _⊎_ ]₁- g

isInj₁ : ∀ {A B} → A ⊎ B → Maybe A
isInj₁ (inj₁ x) = just x
isInj₁ (inj₂ y) = nothing

isInj₂ : ∀ {A B} → A ⊎ B → Maybe B
isInj₂ (inj₁ x) = nothing
isInj₂ (inj₂ y) = just y

max_issues_repo_name: larrytheliquid/Lemmachine


text:
-- Andreas, 2019-04-10, issue #3683 reported by akaposi.

-- Regression in the termination checker introduced together
-- with collecting function calls also in the type signatures
-- (fix of #1556).

data A : Set
data B : A → Set

data A where
  a : A
  f : B a → A

data B where

module _
  (A' : Set)(B' : A' → Set)
  (a' : A')(f' : B' a' → A')
  where

  mutual
    elimA : (x : A) → A'
    elimA a     = a'
    elimA (f y) = f' (elimB a y)
    -- Call elimA (f y) --> elimB a y

    -- Call elimB x y --> elimA x in the type signature
    elimB : (x : A) (y : B x) → B' (elimA x)
    elimB x ()

-- With counting calls in the type signature as well, we get
--
--   elimA (f _) --> elimB a _ --> elimA a
--
-- which does not pass the naive termination checker, since
-- `a` and `f _` are unrelated in size.
--
-- However a more sophisticated type checker (Hyvernat)
-- will see that the composed call
--
--   elimA (f _) --> elimA a
--
-- is not idempotent; it cannot be composed with itself.
--
-- Thus, it is to be discounted during termination checking.
--
-- Verdict: this test case should pass.


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of operations on the Colist type
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe --sized-types #-}

module Codata.Colist.Properties where

open import Size
open import Codata.Thunk using (Thunk; force)
open import Codata.Conat
open import Codata.Colist
open import Codata.Colist.Bisimilarity
open import Function
open import Relation.Binary.PropositionalEquality as Eq

-- Functor laws

module _ {a} {A : Set a} where

 map-identity : ∀ (as : Colist A ∞) {i} → i ⊢ map id as ≈ as
 map-identity []       = []
 map-identity (a ∷ as) = Eq.refl ∷ λ where .force → map-identity (as .force)

module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where

 map-map-fusion : ∀ (f : A → B) (g : B → C) as {i} → i ⊢ map g (map f as) ≈ map (g ∘ f) as
 map-map-fusion f g []       = []
 map-map-fusion f g (a ∷ as) = Eq.refl ∷ λ where .force → map-map-fusion f g (as .force)


text:
module BadCon where

data D : Set where
  d : D

data E : Set where
  d : E

postulate
  F : D -> Set

test : (x : D) -> F x
test = d

-- Bad error (unbound de Bruijn index):
-- the constructor d does not construct an element of F @0
-- when checking that the expression d has type (x : D) → F x


text:
{-# OPTIONS --copatterns --sized-types #-}

module Streams where

open import Size
open import Function
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P
open ≡-Reasoning

open import Data.List using (List; module List; []; _∷_; _++_; length)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product using (_,_; _×_; proj₁; proj₂)

-- | Streams (with size annotations to ease definitions).
record Stream {i : Size} (A : Set) : Set where
  coinductive
  constructor _∷_
  field
    hd : A
    tl : ∀ {j : Size< i} → Stream {j} A
open Stream public

-- | Stream equality is bisimilarity
record _~_ {A : Set} (s t : Stream A) : Set where
  coinductive
  field
    hd~ : hd s ≡ hd t
    tl~ : (tl s) ~ (tl t)
open _~_ public

-- | Functoriality
map : ∀ {i A B} (f : A → B) (s : Stream {i} A) → Stream {i} B
hd (map     f s)     = f (hd s)
tl (map {i} f s) {j} = map {j} f (tl s {j})

-- | Coalgebra structure
str-out : ∀{A} → Stream A → A × Stream A
str-out s = (hd s , tl s)

-- | (Weak) Finality
corec : ∀ {A X : Set} → (X → A × X) → (∀ {i} → X → Stream {i} A)
hd (corec f x) = proj₁ (f x)
tl (corec f x) = corec f (proj₂ (f x))

-- | Direct access to elements
_<_> : ∀{A} → Stream A → ℕ → A
s < 0 >     = hd s
s < suc n > = (tl s) < n >

-- | Correctness of bisimlarity
~→pw-equal : ∀{A} {s t : Stream A} →
             s ~ t → ∀ n → s < n > ≡ t < n >
~→pw-equal p zero    = hd~ p
~→pw-equal p (suc n) = ~→pw-equal (tl~ p) n

-- | The usual definition of a bisimulation on streams.
Is-Bisim : ∀{A} → Rel (Stream A) _ → Set
Is-Bisim _R_ = ∀ x y → x R y → hd x ≡ hd y × (tl x) R (tl y)

-- | If R is a bisimulation then all elements related by R are bisimilar.
ex-bisimulation→bisim : ∀{A R} → Is-Bisim {A} R → ∀ {x y} → R x y → x ~ y
hd~ (ex-bisimulation→bisim p {x} {y} xRy) = proj₁ (p x y xRy)
tl~ (ex-bisimulation→bisim p {x} {y} xRy) =
  ex-bisimulation→bisim p (proj₂ (p x y xRy))

-- | Generalised bisimulations between arbitrary stream coalgebras.
Is-Bisim' : ∀{A X Y : Set} → (c : X → A × X) (d : Y → A × Y) → REL X Y _ → Set
Is-Bisim' c d _R_ = ∀ x y → x R y →
                  proj₁ (c x) ≡ proj₁ (d y) ×
                  (proj₂ (c x)) R (proj₂ (d y))

ex-bisimulation→bisim' : ∀{A X Y R c d} → Is-Bisim' {A} {X} {Y} c d R →
                         ∀ {x y} → R x y → corec c x ~ corec d y
hd~ (ex-bisimulation→bisim' p {x} {y} xRy) = proj₁ (p x y xRy)
tl~ (ex-bisimulation→bisim' p {x} {y} xRy) =
  ex-bisimulation→bisim' p (proj₂ (p x y xRy))

~trans : ∀{A} {r s t : Stream A} → r ~ s → s ~ t → r ~ t
hd~ (~trans p q) = trans  (hd~ p) (hd~ q)
tl~ (~trans p q) = ~trans (tl~ p) (tl~ q)

~sym : ∀{A} {s t : Stream A} → s ~ t → t ~ s
hd~ (~sym p) = sym  (hd~ p)
tl~ (~sym p) = ~sym (tl~ p)

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Greatest common divisor
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.Nat.GCD where

open import Data.Nat
open import Data.Nat.Divisibility
open import Data.Nat.GCD.Lemmas
open import Data.Nat.Properties using (+-suc)
open import Data.Product
open import Function
open import Induction
open import Induction.Nat using (<′-Rec; <′-recBuilder)
open import Induction.Lexicographic
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_; subst)
open import Relation.Nullary using (Dec; yes; no)

------------------------------------------------------------------------
-- Greatest common divisor

module GCD where

  -- Specification of the greatest common divisor (gcd) of two natural
  -- numbers.

  record GCD (m n gcd : ℕ) : Set where
    constructor is
    field
      -- The gcd is a common divisor.
      commonDivisor : gcd ∣ m × gcd ∣ n

      -- All common divisors divide the gcd, i.e. the gcd is the
      -- greatest common divisor according to the partial order _∣_.
      greatest : ∀ {d} → d ∣ m × d ∣ n → d ∣ gcd

  open GCD public

  -- The gcd is unique.

  unique : ∀ {d₁ d₂ m n} → GCD m n d₁ → GCD m n d₂ → d₁ ≡ d₂
  unique d₁ d₂ = ∣-antisym (GCD.greatest d₂ (GCD.commonDivisor d₁))
                           (GCD.greatest d₁ (GCD.commonDivisor d₂))

  -- The gcd relation is "symmetric".

  sym : ∀ {d m n} → GCD m n d → GCD n m d
  sym g = is (swap $ GCD.commonDivisor g) (GCD.greatest g ∘ swap)

  -- The gcd relation is "reflexive".

  refl : ∀ {n} → GCD n n n
  refl = is (∣-refl , ∣-refl) proj₁

  -- The GCD of 0 and n is n.

  base : ∀ {n} → GCD 0 n n
  base {n} = is (n ∣0 , ∣-refl) proj₂

  -- If d is the gcd of n and k, then it is also the gcd of n and
  -- n + k.

  step : ∀ {n k d} → GCD n k d → GCD n (n + k) d
  step g with GCD.commonDivisor g
  step {n} {k} {d} g | (d₁ , d₂) = is (d₁ , ∣m∣n⇒∣m+n d₁ d₂) greatest′
    where
    greatest′ : ∀ {d′} → d′ ∣ n × d′ ∣ n + k → d′ ∣ d
    greatest′ (d₁ , d₂) = GCD.greatest g (d₁ , ∣m+n∣m⇒∣n d₂ d₁)

open GCD public using (GCD) hiding (module GCD)

------------------------------------------------------------------------
-- Calculating the gcd

-- The calculation also proves Bézout's lemma.

module Bézout where

  module Identity where

    -- If m and n have greatest common divisor d, then one of the
    -- following two equations is satisfied, for some numbers x and y.
    -- The proof is "lemma" below (Bézout's lemma).
    --
    -- (If this identity was stated using integers instead of natural
    -- numbers, then it would not be necessary to have two equations.)

    data Identity (d m n : ℕ) : Set where
      +- : (x y : ℕ) (eq : d + y * n ≡ x * m) → Identity d m n
      -+ : (x y : ℕ) (eq : d + x * m ≡ y * n) → Identity d m n

    -- Various properties about Identity.

    sym : ∀ {d} → Symmetric (Identity d)
    sym (+- x y eq) = -+ y x eq
    sym (-+ x y eq) = +- y x eq

    refl : ∀ {d} → Identity d d d
    refl = -+ 0 1 P.refl

    base : ∀ {d} → Identity d 0 d
    base = -+ 0 1 P.refl

    private
      infixl 7 _⊕_

      _⊕_ : ℕ → ℕ → ℕ
      m ⊕ n = 1 + m + n

    step : ∀ {d n k} → Identity d n k → Identity d n (n + k)
    step {d}     (+-  x  y       eq) with compare x y
    step {d}     (+- .x .x       eq) | equal x     = +- (2 * x)     x       (lem₂ d x   eq)
    step {d}     (+- .x .(x ⊕ i) eq) | less x i    = +- (2 * x ⊕ i) (x ⊕ i) (lem₃ d x   eq)
    step {d} {n} (+- .(y ⊕ i) .y eq) | greater y i = +- (2 * y ⊕ i) y       (lem₄ d y n eq)
    step {d}     (-+  x  y       eq) with compare x y
    step {d}     (-+ .x .x       eq) | equal x     = -+ (2 * x)     x       (lem₅ d x   eq)
    step {d}     (-+ .x .(x ⊕ i) eq) | less x i    = -+ (2 * x ⊕ i) (x ⊕ i) (lem₆ d x   eq)
    step {d} {n} (-+ .(y ⊕ i) .y eq) | greater y i = -+ (2 * y ⊕ i) y       (lem₇ d y n eq)

  open Identity public using (Identity; +-; -+) hiding (module Identity)

  module Lemma where

    -- This type packs up the gcd, the proof that it is a gcd, and the
    -- proof that it satisfies Bézout's identity.

    data Lemma (m n : ℕ) : Set where
      result : (d : ℕ) (g : GCD m n d) (b : Identity d m n) → Lemma m n

    -- Various properties about Lemma.

    sym : Symmetric Lemma
    sym (result d g b) = result d (GCD.sym g) (Identity.sym b)

    base : ∀ d → Lemma 0 d
    base d = result d GCD.base Identity.base

    refl : ∀ d → Lemma d d
    refl d = result d GCD.refl Identity.refl

    stepˡ : ∀ {n k} → Lemma n (suc k) → Lemma n (suc (n + k))
    stepˡ {n} {k} (result d g b) =
      subst (Lemma n) (+-suc n k) $
        result d (GCD.step g) (Identity.step b)

    stepʳ : ∀ {n k} → Lemma (suc k) n → Lemma (suc (n + k)) n
    stepʳ = sym ∘ stepˡ ∘ sym

  open Lemma public using (Lemma; result) hiding (module Lemma)

  -- Bézout's lemma proved using some variant of the extended
  -- Euclidean algorithm.

  lemma : (m n : ℕ) → Lemma m n
  lemma m n = build [ <′-recBuilder ⊗ <′-recBuilder ] P gcd (m , n)
    where
    P : ℕ × ℕ → Set
    P (m , n) = Lemma m n

    gcd : ∀ p → (<′-Rec ⊗ <′-Rec) P p → P p
    gcd (zero  , n                 ) rec = Lemma.base n
    gcd (suc m , zero              ) rec = Lemma.sym (Lemma.base (suc m))
    gcd (suc m , suc n             ) rec with compare m n
    gcd (suc m , suc .m            ) rec | equal .m     = Lemma.refl (suc m)
    gcd (suc m , suc .(suc (m + k))) rec | less .m k    =
                      -- "gcd (suc m) (suc k)"
      Lemma.stepˡ $ proj₁ rec (suc k) (lem₁ k m)
    gcd (suc .(suc (n + k)) , suc n) rec | greater .n k =
                      -- "gcd (suc k) (suc n)"
      Lemma.stepʳ $ proj₂ rec (suc k) (lem₁ k n) (suc n)

  -- Bézout's identity can be recovered from the GCD.

  identity : ∀ {m n d} → GCD m n d → Identity d m n
  identity {m} {n} g with lemma m n
  ... | result d g′ b with GCD.unique g g′
  ...   | P.refl = b

-- Calculates the gcd of the arguments.

gcd : (m n : ℕ) → ∃ λ d → GCD m n d
gcd m n with Bézout.lemma m n
... | Bézout.result d g _ = (d , g)

-- gcd as a proposition is decidable

gcd? : (m n d : ℕ) → Dec (GCD m n d)
gcd? m n d with gcd m n
... | d′ , p with d′ ≟ d
...   | no ¬g = no (¬g ∘ GCD.unique p)
...   | yes g = yes (subst (GCD m n) g p)


text:
------------------------------------------------------------------------------
-- Properties of the Collatz function
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOTC.Program.Collatz.PropertiesI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.PropertiesI
open import FOTC.Data.Nat
open import FOTC.Data.Nat.PropertiesI
open import FOTC.Data.Nat.UnaryNumbers
open import FOTC.Data.Nat.UnaryNumbers.TotalityI
open import FOTC.Program.Collatz.Collatz
open import FOTC.Program.Collatz.Data.Nat
open import FOTC.Program.Collatz.Data.Nat.PropertiesI

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

collatzCong : ∀ {m n} → m ≡ n → collatz m ≡ collatz n
collatzCong refl = refl

helper : ∀ {n} → N n → collatz (2' ^ succ₁ n) ≡ collatz (2' ^ n)
helper nzero =
  collatz (2' ^ 1')   ≡⟨ collatzCong (x^1≡x 2-N) ⟩
  collatz 2'          ≡⟨ collatz-even 2-Even ⟩
  collatz (div 2' 2') ≡⟨ collatzCong (div-x-x≡1 2-N S≢0) ⟩
  collatz (1')        ≡⟨ collatzCong (sym (^-0 2')) ⟩
  collatz (2' ^ 0')   ∎

helper (nsucc {n} Nn) =
  collatz (2' ^ succ₁ (succ₁ n))
    ≡⟨ collatzCong prf ⟩
  collatz (succ₁ (succ₁ (2' ^ succ₁ (succ₁ n) ∸ 2')))
    ≡⟨ collatz-even (x-Even→SSx-Even
                       (∸-N (^-N 2-N (nsucc (nsucc Nn))) 2-N)
                       (∸-Even (^-N 2-N (nsucc (nsucc Nn))) 2-N
                               (2^[x+1]-Even (nsucc Nn)) 2-Even)) ⟩
  collatz (div (succ₁ (succ₁ ((2' ^ succ₁ (succ₁ n)) ∸ 2'))) 2')
    ≡⟨ collatzCong (divLeftCong (sym prf)) ⟩
  collatz (div (2' ^ succ₁ (succ₁ n)) 2')
    ≡⟨ collatzCong (div-2^[x+1]-2≡2^x (nsucc Nn)) ⟩
  collatz (2' ^ succ₁ n) ∎
  where
  prf : 2' ^ succ₁ (succ₁ n) ≡ succ₁ (succ₁ (2' ^ succ₁ (succ₁ n) ∸ 2'))
  prf = (+∸2 (^-N 2-N (nsucc (nsucc Nn)))
             (2^x≢0 (nsucc (nsucc Nn)))
             (2^[x+1]≢1 (nsucc Nn)))

collatz-2^x : ∀ {n} → N n → collatz (2' ^ n) ≡ 1'
collatz-2^x nzero =
  collatz (2' ^ 0') ≡⟨ collatzCong (^-0 2') ⟩
  collatz 1'        ≡⟨ collatz-1 ⟩
  1'                ∎

collatz-2^x (nsucc {n} Nn) =
  collatz (2' ^ succ₁ n) ≡⟨ helper Nn ⟩
  collatz (2' ^ n)       ≡⟨ collatz-2^x Nn ⟩
  1'                     ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --without-K  #-}

module sets.unit where

record ⊤ : Set where
  constructor tt

⊤-elim : (P : ⊤ → Set) → P tt → (x : ⊤) → P x
⊤-elim P ptt tt = ptt

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
-- Andreas, 2015-09-12

open import Common.Product
open import Common.Equality

module _ (A : Set) where

mutual
  X : A × A → A
  X = _

  test : (x y : A × A) → X (proj₁ x , proj₁ y) ≡ proj₁ x
  test _ _ = refl

-- This worked even before the fix of #1316,
-- since _ record variables are expanded (see #473).


text:
------------------------------------------------------------------------
-- Some substitution lemmas
------------------------------------------------------------------------

open import Atom

module Substitution (atoms : χ-atoms) where

open import Equality.Propositional
open import Prelude hiding (const)

open import Bag-equivalence equality-with-J using (_∈_)

open import Chi atoms

open χ-atoms atoms

private
  variable
    c       : Const
    e e′ e″ : Exp
    x y     : Var
    xs      : List Var

-- Some simplification lemmas for the substitution functions.

var-step-≡ : x ≡ y → var y [ x ← e ] ≡ e
var-step-≡ {x = x} {y = y} x≡y with x V.≟ y
… | yes _  = refl
… | no x≢y = ⊥-elim (x≢y x≡y)

var-step-≢ : x ≢ y → var y [ x ← e ] ≡ var y
var-step-≢ {x = x} {y = y} x≢y with x V.≟ y
… | no _    = refl
… | yes x≡y = ⊥-elim (x≢y x≡y)

lambda-step-≡ : x ≡ y → lambda y e [ x ← e′ ] ≡ lambda y e
lambda-step-≡ {x = x} {y = y} x≡y with x V.≟ y
… | yes _  = refl
… | no x≢y = ⊥-elim (x≢y x≡y)

lambda-step-≢ :
  x ≢ y → lambda y e [ x ← e′ ] ≡ lambda y (e [ x ← e′ ])
lambda-step-≢ {x = x} {y = y} x≢y with x V.≟ y
… | no _    = refl
… | yes x≡y = ⊥-elim (x≢y x≡y)

rec-step-≡ : x ≡ y → rec y e [ x ← e′ ] ≡ rec y e
rec-step-≡ {x = x} {y = y} x≡y with x V.≟ y
… | yes _  = refl
… | no x≢y = ⊥-elim (x≢y x≡y)

rec-step-≢ :
  x ≢ y → rec y e [ x ← e′ ] ≡ rec y (e [ x ← e′ ])
rec-step-≢ {x = x} {y = y} x≢y with x V.≟ y
… | no _    = refl
… | yes x≡y = ⊥-elim (x≢y x≡y)

branch-step-∈ :
  x ∈ xs →
  branch c xs e [ x ← e′ ]B ≡ branch c xs e
branch-step-∈ {x = x} {xs = xs} x∈xs with V.member x xs
… | yes _   = refl
… | no x∉xs = ⊥-elim (x∉xs x∈xs)

branch-step-∉ :
  ¬ x ∈ xs →
  branch c xs e [ x ← e′ ]B ≡ branch c xs (e [ x ← e′ ])
branch-step-∉ {x = x} {xs = xs} x∉xs with V.member x xs
… | no _     = refl
… | yes x∈xs = ⊥-elim (x∉xs x∈xs)

-- A "fusion" lemma.

mutual

  fusion : ∀ e → e [ x ← e′ ] [ x ← e″ ] ≡ e [ x ← e′ [ x ← e″ ] ]
  fusion (apply e₁ e₂) =
    cong₂ apply (fusion e₁) (fusion e₂)

  fusion {x = x} {e′ = e′} {e″ = e″} (lambda y e) with x V.≟ y
  … | yes _ = refl
  … | no _  =
    lambda y (e [ x ← e′ ] [ x ← e″ ])  ≡⟨ cong (lambda _) $ fusion e ⟩∎
    lambda y (e [ x ← e′ [ x ← e″ ] ])  ∎

  fusion (case e bs) =
    cong₂ case (fusion e) (fusion-B⋆ bs)

  fusion {x = x} {e′ = e′} {e″ = e″} (rec y e) with x V.≟ y
  … | yes _ = refl
  … | no _  =
    rec y (e [ x ← e′ ] [ x ← e″ ])  ≡⟨ cong (rec _) $ fusion e ⟩∎
    rec y (e [ x ← e′ [ x ← e″ ] ])  ∎

  fusion {x = x} {e″ = e″} (var y) with x V.≟ y
  … | yes _  = refl
  … | no x≢y =
    var y [ x ← e″ ]  ≡⟨ var-step-≢ x≢y ⟩∎
    var y             ∎

  fusion (const c es) =
    cong (const c) (fusion-⋆ es)

  fusion-B :
    ∀ b → b [ x ← e′ ]B [ x ← e″ ]B ≡ b [ x ← e′ [ x ← e″ ] ]B
  fusion-B {x = x} {e′ = e′} {e″ = e″} (branch c xs e)
    with V.member x xs
  … | yes x∈xs =
    branch c xs e [ x ← e″ ]B  ≡⟨ branch-step-∈ x∈xs ⟩∎
    branch c xs e              ∎
  … | no x∉xs =
    branch c xs (e [ x ← e′ ]) [ x ← e″ ]B  ≡⟨ branch-step-∉ x∉xs ⟩
    branch c xs (e [ x ← e′ ] [ x ← e″ ])   ≡⟨ cong (branch _ _) $ fusion e ⟩∎
    branch c xs (e [ x ← e′ [ x ← e″ ] ])   ∎

  fusion-⋆ :
    ∀ es → es [ x ← e′ ]⋆ [ x ← e″ ]⋆ ≡ es [ x ← e′ [ x ← e″ ] ]⋆
  fusion-⋆ []       = refl
  fusion-⋆ (e ∷ es) = cong₂ _∷_ (fusion e) (fusion-⋆ es)

  fusion-B⋆ :
    ∀ bs → bs [ x ← e′ ]B⋆ [ x ← e″ ]B⋆ ≡ bs [ x ← e′ [ x ← e″ ] ]B⋆
  fusion-B⋆ []       = refl
  fusion-B⋆ (b ∷ bs) = cong₂ _∷_ (fusion-B b) (fusion-B⋆ bs)

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi


text:
module Base where

postulate String : Set
          Char   : Set
{-# BUILTIN STRING String #-}
{-# BUILTIN CHAR   Char   #-}

data Unit : Set where
  unit : Unit

{-# COMPILED_DATA Unit () #-}

data Bool : Set where
  true  : Bool
  false : Bool

data False  : Set where
record True : Set where

IsTrue : Bool -> Set
IsTrue true = True
IsTrue false = False

{-# COMPILED_DATA Bool True False #-}

infixr 40 _::_
data List (A : Set) : Set where
  [] : List A
  _::_ : A -> List A -> List A

{-# COMPILED_DATA List [] (:) #-}

data _×_ (A B : Set) : Set where
  _,_ : A -> B -> A × B

{-# COMPILED_DATA _×_ (,) #-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Base.Partial where

open import Data.String using (String)

open import Base.Free   using (Free)

record Partial (S : Set) (P : S → Set) : Set₁ where
  field
    undefined : {A : Set} → Free S P A
    error     : {A : Set} → String → Free S P A
open Partial ⦃ ... ⦄ public

max_stars_repo_name: FreeProving/free-compiler

max_issues_repo_name: FreeProving/free-compiler

max_forks_repo_name: FreeProving/free-compiler