module chap0 where

open import Data.List
open import Data.Nat hiding (_⊔_)
open import Data.Integer hiding (_⊔_)
open import Data.Product

A : List ℕ
A = 1 ∷ 2 ∷ []

data Literal : Set where
    x : Literal
    y : Literal
    z : Literal

B : List Literal
B = x ∷ y ∷ z ∷ []


ListProduct : {A B : Set } → List A → List B → List ( A × B )
ListProduct = {!!}

ex05 : List ( ℕ × Literal )
ex05 = ListProduct A B   -- (1 , x) ∷ (1 , y) ∷ (1 , z) ∷ (2 , x) ∷ (2 , y) ∷ (2 , z) ∷ [] 

ex06 : List ( ℕ × Literal × ℕ )
ex06 = ListProduct A (ListProduct B A)

ex07 : Set
ex07 =  ℕ × ℕ

data ex08-f : ℕ → ℕ → Set where
    ex08f0 : ex08-f 0 1
    ex08f1 : ex08-f 1 2
    ex08f2 : ex08-f 2 3
    ex08f3 : ex08-f 3 4
    ex08f4 : ex08-f 4 0

data ex09-g : ℕ → ℕ → ℕ → ℕ → Set where
    ex09g0 : ex09-g 0 1 2 3
    ex09g1 : ex09-g 1 2 3 0
    ex09g2 : ex09-g 2 3 0 1
    ex09g3 : ex09-g 3 0 1 2

open import Data.Nat.DivMod
open import Relation.Binary.PropositionalEquality

_≡7_ : ℕ → ℕ → Set
n ≡7 m = (n % 7) ≡ (m % 7 )

refl7 :  { n : ℕ} → n ≡7 n
refl7 = {!!}

sym7  : { n m : ℕ} → n ≡7 m → m ≡7 n
sym7  = {!!}

trans7 : { n m o : ℕ} → n ≡7 m → m ≡7 o → n ≡7 o
trans7 = {!!}

open import Level renaming ( zero to Zero ; suc to Suc )

record Graph  { v v' : Level } : Set (Suc v ⊔ Suc v' ) where
  field
    vertex : Set v
    edge : vertex  → vertex → Set v'

data edge012a :  ℕ → ℕ →  Set where
    e012a-1 : edge012a 1 2
    e012a-2 : edge012a 2 3
    e012a-3 : edge012a 3 4
    e012a-4 : edge012a 4 5
    e012a-5 : edge012a 5 1

graph012a : Graph {Zero} {Zero}
graph012a = record { vertex = ℕ  ; edge = edge012a }

data edge012b :  ℕ → ℕ →  Set where
    e012b-1 : edge012b 1 2
    e012b-2 : edge012b 1 3
    e012b-3 : edge012b 1 4
    e012b-4 : edge012b 2 3
    e012b-5 : edge012b 2 4
    e012b-6 : edge012b 3 4

graph012b : Graph {Zero} {Zero}
graph012b = record { vertex = ℕ  ; edge = edge012b }

data connected { V : Set } ( E : V -> V -> Set ) ( x y : V ) : Set  where
    direct :   E x y -> connected E x y 
    indirect :  { z : V  } -> E x z  ->  connected {V} E z y -> connected E x y

open import Data.Empty
open import Relation.Nullary

-- data Dec (P : Set) : Set where
--    yes :   P → Dec P
--    no  : ¬ P → Dec P

reachable :  { V : Set } ( E : V -> V -> Set ) ( x y : V ) -> Set
reachable {V} E X Y = Dec ( connected {V} E X Y )

dag :  { V : Set } ( E : V -> V -> Set ) ->  Set
dag {V} E =  ∀ (n : V)  →  ¬ ( connected E n n )