module exampleTrafficLight1 where

data ⊤ : Set where
  true : ⊤ 


data ⊥ : Set where
  

data Colour : Set where
  red   : Colour
  green : Colour


record PhysState : Set where 
 field
   sigA : Colour
   sigB : Colour

data ControlState : Set where
   allRed : ControlState
   onlyAGreen : ControlState
   onlyBGreen : ControlState


toSigA : ControlState -> Colour
toSigA allRed = red
toSigA onlyAGreen = green
toSigA onlyBGreen = red


toSigB : ControlState -> Colour
toSigB allRed = red
toSigB onlyAGreen = red
toSigB onlyBGreen = green

toPhysState : ControlState -> PhysState
toPhysState c = record{ sigA = toSigA c;
                        sigB = toSigB c}



CorAux : Colour -> Colour -> Set
CorAux red   _     = ⊤ 
CorAux green red   = ⊤ 
CorAux green green = ⊥ 


Cor : PhysState -> Set
Cor s = CorAux  (PhysState.sigA s) (PhysState.sigB s) 


corProof : (s : ControlState) -> Cor (toPhysState s)
corProof allRed = true
corProof onlyAGreen = true
corProof onlyBGreen = true