/- Clara Löh; 10/2023 -/

/- Syntax of propositional formulas -/

inductive Expr where
| eVar : Nat -> Expr  -- we enumerate the different variables by natural numbers
| eNot : Expr -> Expr
| eAnd : Expr -> Expr -> Expr
| eOr  : Expr -> Expr -> Expr
| eImp : Expr -> Expr -> Expr 
| eEqu : Expr -> Expr -> Expr 
deriving Repr -- so that we can display values of this type

open Expr 

def A := eVar 0
def B := eVar 1

-- Examples
#check eAnd (eOr A B) (eNot A) -- indeed an Expr
#check eAnd (eAnd A B)        -- (!)
-- #check And (And And)        -- uh-oh


/- Classical semantics of propositional formulas -/

inductive CBool where 
| cTrue  : CBool
| cFalse : CBool
deriving Repr

open CBool

-- The standard boolean operations:
def lnot (a : CBool) : CBool 
:= match a with 
| cTrue  => cFalse
| cFalse => cTrue 

def lor (a : CBool) (b : CBool) : CBool
:= match (a,b) with 
| (cTrue,  cTrue)  => cTrue
| (cTrue,  cFalse) => cTrue
| (cFalse, cTrue)  => cTrue
| (cFalse, cFalse) => cFalse

def land (a : CBool) (b : CBool) : CBool
:= match (a,b) with 
| (cTrue,  cTrue)  => cTrue 
| (cTrue,  cFalse) => cFalse
| (cFalse, cTrue)  => cFalse
| (cFalse, cFalse) => cFalse

def limp (a : CBool) (b : CBool) : CBool
:= match (a,b) with 
| (cTrue,  cTrue)  => cTrue
| (cTrue,  cFalse) => cFalse
| (cFalse, cTrue)  => cTrue
| (cFalse, cFalse) => cTrue

def lequ (a : CBool) (b : CBool) : CBool
:= match (a,b) with 
| (cTrue,  cTrue)  => cTrue
| (cTrue,  cFalse) => cFalse
| (cFalse, cTrue)  => cFalse
| (cFalse, cFalse) => cTrue


-- A valuation assigns to each (index of a) variable a classical boolean
def cVal := Nat -> CBool 

-- The classical semantics of propositional formulas
def cSemantics (v : cVal)  (e : Expr) : CBool
:= match e with  
| eVar n   => v n
| eNot a   => lnot (cSemantics v a)
| eAnd a b => land (cSemantics v a) (cSemantics v b)
| eOr  a b => lor  (cSemantics v a) (cSemantics v b)
| eImp a b => limp (cSemantics v a) (cSemantics v b)
| eEqu a b => lequ (cSemantics v a) (cSemantics v b)

-- Examples
def ft : cVal 
:= λ n 
=> match n with 
| 0 => cFalse 
| 1 => cTrue 
| _ => cTrue

def tf : cVal 
:= λ n 
=> match n with 
| 0 => cTrue 
| 1 => cFalse 
| _ => cTrue

def someExpr : Expr 
:= (eAnd (eOr A B) 
         (eNot A)) 

#check cSemantics ft someExpr
#eval cSemantics ft someExpr
#eval cSemantics tf someExpr

def tertiumNonDatur : Expr
:= eOr A (eNot A)

#eval cSemantics ft tertiumNonDatur
#eval cSemantics tf tertiumNonDatur

/- A strange semantics -/

def sVal := Nat -> Nat 

def sSemantics (v : sVal) (e : Expr) : Nat 
:= match e with 
| eVar n   => v n 
| eNot a   => 42
| eAnd a b => (sSemantics v a) + (sSemantics v b)
| eOr  a b => (sSemantics v a) * 2023
| eImp a b => (sSemantics v a) + (sSemantics v b)
| eEqu a b => (sSemantics v a) 

def incVal : sVal 
:= λ n => n + 2

#check sSemantics incVal someExpr 
#eval sSemantics incVal someExpr   -- 4088

#eval sSemantics incVal tertiumNonDatur -- 4046