{-# OPTIONS --postfix-projections #-}

open import Data.Product using (∃; _×_; _,_)

-- Graph representation of classical propositional formulæ (Walicki).


-- Example graph
--
-- a ↔ ¬b ∧ ¬c
-- b ↔ ¬c
-- c ↔ ¬a


-- Atoms (nodes).

data A : Set where
  a b c : A

-- Successor (edge)  R x xᵢ  if  (x ↔ ¬x₁ ∧ ... ∧ ¬xₙ).

data R : A → A → Set where
  a→b : R a b
  a→c : R a c
  b→c : R b c
  c→a : R c a


-- Sound valuations.

mutual

  -- All successors of a true node must be false.

  record True (x : A) : Set where
    coinductive
    field all : ∀ y → R x y → False y

  -- A false node must have a true successor.

  record False (x : A) : Set where
    coinductive
    field any : ∃ λ y → R x y × True y


-- A sound valuation of the example graph.

mutual

  aFalse : False a
  bFalse : False b
  cTrue  : True  c

  aFalse = {!!}
  bFalse = {!!}
  cTrue  = {!!}







{-
  aFalse .any       = _ , a→c , cTrue
  bFalse .any       = _ , b→c , cTrue
  cTrue  .all _ c→a = aFalse


-- -}
-- -}
-- -}
-- -}
-- -}