module Main where

import Prelude

data Formula = Var String
             | And Formula Formula
             | Or Formula Formula
             | Not Formula
             | Implies Formula Formula

data Value = Value String Bool

lookup' :: [ Value ] -> String -> Maybe Bool
lookup' [] _ = Nothing
lookup' ((Value s b) : tail) t = if s==t then Just b else lookup' tail t

eval :: [ Value ] -> Formula -> Maybe Bool
eval vals (Var s) = lookup' vals s
eval vals (Not p) = do
  result <- eval vals p
  pure $ not result
eval vals (And p q) = do
  pp <- eval vals p
  qq <- eval vals q
  pure $ pp && qq
eval vals (Or p q)  = do
  pp <- eval vals p
  qq <- eval vals q
  pure $ pp || qq
eval vals (Implies p q) = do
  pp <- eval vals p
  qq <- eval vals q
  pure $ not pp || qq

--  here is a formula

f :: Formula
f = And (Var "p") (Or (Var "q") (And (Not (Var "r")) (Var "p")))

-- and here are values for the propositional variables

values =  [ Value "p" True
          , Value "q" False
          , Value "r" True
          ]

-- and this will evaluate the formula

result :: Maybe Bool
result = eval values f

-- should evaluate to: Just False

-- λ> result
-- Just False
-- λ> 

main :: IO ()
main =
  putStrLn ""

module talk where

-- define the natural numbers


data ℕ : Set where
  zero : ℕ
  succ : ℕ -> ℕ

{-# BUILTIN NATURAL ℕ #-}


-- additional of natural numbers

_+_ : ℕ → ℕ → ℕ
zero + b = b
succ n + b = succ (n + b)


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

-- Cartesian product

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

-- example of an ordered pair

pair : ℕ × ℕ
pair = < 1 , 2 >

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

-- "vectors" of some type A of length n

data Vec ( A : Set) : ℕ -> Set where
  [] : Vec A zero
  _::_ : { n : ℕ } -> A -> Vec A n -> Vec A (succ n)


-- "zip" two vectors of length n

zip : { A B : Set } -> ( n : ℕ ) -> Vec A n -> Vec B n -> Vec (A × B) n
zip zero [] [] = []
zip (succ n) (x :: xs) (y :: ys) = < x , y > :: (zip n xs ys)

-- examples of vetors & zip

a : Vec ℕ 2
a = 1 :: (2 :: [])

b : Vec ℕ 2
b = 0 :: (3 :: [])

--------------------------------------------------------------------------------
-- conjuction

_&_ : Set -> Set -> Set 
A & B = A × B

-- here is a "proof" that A & B -> A

first : { A B : Set } -> A & B -> A
first < a , b > = a

-- the observation is that if a : A and b : B
-- then first < a , b > : A is a "non-canonical"
-- proof of A

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

-- Martin-Löf defines equality in predicate logic [19] as the set
-- inductively generated by the reflexive rule

data _≡_ {A : Set} : A -> A -> Set where
  refl : (a : A) -> a ≡ a


-- the constructor refl a amounts a canonical proof of the reflexive law a ≡ a


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

-- here is a proof that 0 + x = x

+-identity-left : ∀ (x : ℕ) -> (0 + x) ≡ x
+-identity-left x = refl x

-- notice: this "function" takes as input a natural number x, and returns
-- a term of a type whose definition *depends on x*.

-- this proof amounts to the reflexive law the point is that on the
-- left hand side, 0 + x is "definitionally equal" to x (see the
-- definition of the term _+_, above )

-- to prove x + 0 = x is slightly more difficult because this equality
-- doesn't result directly from the defn of _+_


-- we use the following natural recursion "combinator"

natrec : {C : ℕ -> Set}       -- view C as a family of propositions indexed by ℕ
         -> (C zero)          -- base case
         -> ( (m : ℕ)         -- ind step {
            -> C m          --          {   induction hyp
            -> C (succ m) ) --          {
         -> (n : ℕ) 
        -> C n               -- conclusion
natrec p h zero = p
natrec p h (succ n) = h n (natrec p h n)  

-- and we'll use the following term in our induction step below.  For
-- natural numbers n,m this transforms a proof of n ≡ m into a proof
-- of (n+1) ≡ (m+1)

eq-succ : { n m : ℕ } -> n ≡ m -> succ n ≡ succ m
eq-succ  (refl m) = refl (succ m)

-- finally here is our proof that x + 0 = x

+-identity-right : (x : ℕ) -> (x + 0) ≡ x
+-identity-right x = natrec
     {\k -> (k + 0) ≡ k }
     (refl 0)
     (\k ih -> eq-succ ih)
     x