content: {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE FlexibleInstances     #-}
  {-# LANGUAGE TypeFamilies          #-}
  {-# LANGUAGE IncoherentInstances   #-}
  
  module ProofCombinators (
  
    -- ATTENTION! `Admit` and `(==!)` are UNSAFE: they should not belong the final proof term
  
    -- * Proof is just a () alias
    Proof
    , toProof 
  
    -- * Proof constructors
    , trivial, unreachable, (***), QED(..)
  
    -- * "Because" combinator 
    , (?)
  
    -- * These two operators check all intermediate equalities
    , (===) -- proof of equality is implicit eg. x === y
    , (=<=) -- proof of equality is implicit eg. x <= y
    , (=>=)  -- proof of equality is implicit eg. x =>= y 
  
    -- * This operator does not check intermediate equalities
    , (==.) 
  
    -- Uncheck operator used only for proof debugging
    , (==!) -- x ==! y always succeds
  
    -- * Combining Proofs
    , (&&&)
    , withProof 
    , impossible 
  
  
  ) where
  
  -------------------------------------------------------------------------------
  -- | Proof is just a () alias -------------------------------------------------
  -------------------------------------------------------------------------------
  
  type Proof = ()
  
  toProof :: a -> Proof
  toProof _ = ()
  
  -------------------------------------------------------------------------------
  -- | Proof Construction -------------------------------------------------------
  -------------------------------------------------------------------------------
  
  -- | trivial is proof by SMT
  
  trivial :: Proof
  trivial =  ()
  
  -- {-@ unreachable :: {v : Proof | False } @-}
  unreachable :: Proof
  unreachable =  ()
  
  -- All proof terms are deleted at runtime.
  {- RULE "proofs are irrelevant" forall (p :: Proof). p = () #-}
  
  -- | proof casting
  -- | `x *** QED`: x is a proof certificate* strong enough for SMT to prove your theorem
  -- | `x *** Admit`: x is an unfinished proof
  
  infixl 3 ***
  {-@ assume (***) :: a -> p:QED -> { if (isAdmit p) then false else true } @-}
  (***) :: a -> QED -> Proof
  _ *** _ = ()
  
  data QED = Admit | QED
  
  {-@ measure isAdmit :: QED -> Bool @-}
  isAdmit :: QED -> Bool
  isAdmit Admit = True
  isAdmit QED   = False
  
  
  -------------------------------------------------------------------------------
  -- | * Checked Proof Certificates ---------------------------------------------
  -------------------------------------------------------------------------------
  
  -- Any (refined) carries proof certificates.
  -- For example 42 :: {v:Int | v == 42} is a certificate that
  -- the value 42 is equal to 42.
  -- But, this certificate will not really be used to proof any fancy theorems.
  
  -- Below we provide a number of equational operations
  -- that constuct proof certificates.
  
  -- | Implicit equality
  
  -- x === y returns the proof certificate that
  -- result value is equal to both x and y
  -- when y == x (as assumed by the operator's precondition)
  
  infixl 3 ===
  {-@ (===) :: x:a -> y:{a | y == x} -> {v:a | v == x && v == y} @-}
  (===) :: a -> a -> a
  _ === y  = y
  
  infixl 3 =<=
  {-@ (=<=) :: x:a -> y:{a | x <= y} -> {v:a | x <= y && v == y} @-}
  (=<=) :: a -> a -> a
  _ =<= y  = y
  
  infixl 3 =>=
  {-@ (=>=) :: x:a -> y:{a | x >= y}  -> {v:a | x >= y && v == y} @-}
  (=>=) :: a -> a -> a
  _ =>= y  = y
  
  -------------------------------------------------------------------------------
  -- | `?` is basically Haskell's $ and is used for the right precedence
  -- | `?` lets you "add" some fact into a proof term
  -------------------------------------------------------------------------------
  
  infixl 3 ?
  
  {-@ (?) :: forall a b <pa :: a -> Bool, pb :: b -> Bool>. a<pa> -> b<pb> -> a<pa> @-}
  (?) :: a -> b -> a 
  x ? _ = x 
  {-# INLINE (?)   #-} 
  
  -------------------------------------------------------------------------------
  -- | Assumed equality
  -- 	`x ==! y `
  --   returns the admitted proof certificate that result value is equals x and y
  -------------------------------------------------------------------------------
  
  infixl 3 ==!
  {-@ assume (==!) :: x:a -> y:a -> {v:a | v == x && v == y} @-}
  (==!) :: a -> a -> a
  (==!) _ y = y
  
  
  -- | To summarize:
  --
  -- 	- (==!) is *only* for proof debugging
  --	- (===) does not require explicit proof term
  -- 	- (?)   lets you insert "lemmas" as other `Proof` values
  
  -------------------------------------------------------------------------------
  -- | * Unchecked Proof Certificates -------------------------------------------
  -------------------------------------------------------------------------------
  
  -- | The above operators check each intermediate proof step.
  --   The operator `==.` below accepts an optional proof term
  --   argument, but does not check intermediate steps.
  --   TODO: What is it USEFUL FOR?
  
  infixl 3 ==.
  
  {-# DEPRECATED (==.) "Use (===) instead" #-}
  
  {-# INLINE (==.) #-} 
  (==.) :: a -> a -> a 
  _ ==. x = x 
  
  -------------------------------------------------------------------------------
  -- | * Combining Proof Certificates -------------------------------------------
  -------------------------------------------------------------------------------
  
  (&&&) :: Proof -> Proof -> Proof
  x &&& _ = x
  
  
  {-@ withProof :: x:a -> b -> {v:a | v = x} @-}
  withProof :: a -> b -> a
  withProof x _ = x
  
  {-@ impossible :: {v:a | false} -> b @-}
  impossible :: a -> b
  impossible _ = undefined
  
  -------------------------------------------------------------------------------
  -- | Convenient Syntax for Inductive Propositions 
  -------------------------------------------------------------------------------
  
  {-@ measure prop :: a -> b           @-}
  {-@ type Prop E = {v:_ | prop v = E} @-}
  
  
  
  