module SMT.Examples.Progressive where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Bool.Base using (true; false)
open import Cubical.Data.Int.Base using (ℤ; negsuc; pos)
open import Cubical.Data.List.Base using ([]; _∷_)
open import Cubical.Data.Unit.Base using (tt)
open import Cubical.Relation.Nullary.Base using (¬_)

open import SMT.Core
open import SMT.Semantics

zeroInt oneInt twoInt threeInt fourInt fiveInt : ℤ
zeroInt = pos 0
oneInt = pos 1
twoInt = pos 2
threeInt = pos 3
fourInt = pos 4
fiveInt = pos 5

minusOne : ℤ
minusOne = negsuc 0

Γx : Ctx
Γx = decl "x" sInt ∷ []

x₁ : Expr Γx sInt
x₁ = var vz

Γxy : Ctx
Γxy = decl "x" sInt ∷ decl "y" sInt ∷ []

x₂ : Expr Γxy sInt
x₂ = var vz

y₂ : Expr Γxy sInt
y₂ = var (vs vz)

Γxyz : Ctx
Γxyz = decl "x" sInt ∷ decl "y" sInt ∷ decl "z" sInt ∷ []

x₃ : Expr Γxyz sInt
x₃ = var vz

y₃ : Expr Γxyz sInt
y₃ = var (vs vz)

z₃ : Expr Γxyz sInt
z₃ = var (vs (vs vz))

Γpq : Ctx
Γpq = decl "p" sBool ∷ decl "q" sBool ∷ []

p₂ : Expr Γpq sBool
p₂ = var vz

q₂ : Expr Γpq sBool
q₂ = var (vs vz)

Γbxy : Ctx
Γbxy = decl "b" sBool ∷ decl "x" sInt ∷ decl "y" sInt ∷ []

b₃ : Expr Γbxy sBool
b₃ = var vz

xᵇ : Expr Γbxy sInt
xᵇ = var (vs vz)

yᵇ : Expr Γbxy sInt
yᵇ = var (vs (vs vz))

valid-bool-id : Problem Γpq
valid-bool-id =
  problem [] (bImp p₂ p₂)

valid-xor-comm : Problem Γpq
valid-xor-comm =
  problem [] (bEq (bXor p₂ q₂) (bXor q₂ p₂))

valid-demorgan : Problem Γpq
valid-demorgan =
  problem [] (bEq (bNot (bAnd p₂ q₂)) (bOr (bNot p₂) (bNot q₂)))

invalid-or-left : Problem Γpq
invalid-or-left =
  problem (bOr p₂ q₂ ∷ []) p₂

invalid-or-left-counterexample : Counterexample invalid-or-left
invalid-or-left-counterexample =
  counterexample
    (false , (true , tt))
    (refl all∷ all[])
    refl

not-invalid-or-left : ¬ Statement invalid-or-left
not-invalid-or-left = refute invalid-or-left-counterexample

valid-linear-transitivity : Problem Γxyz
valid-linear-transitivity =
  problem
    ( iLe (int zeroInt) x₃
    ∷ iLe x₃ y₃
    ∷ iLe y₃ z₃
    ∷ []
    )
    (iLe (int zeroInt) z₃)

valid-linear-chain-equality : Problem Γxyz
valid-linear-chain-equality =
  problem
    ( iEq x₃ (iAdd y₃ (int twoInt))
    ∷ iEq y₃ (iAdd z₃ (int threeInt))
    ∷ []
    )
    (iEq x₃ (iAdd z₃ (int fiveInt)))

valid-affine-monotone : Problem Γxy
valid-affine-monotone =
  problem
    (iLe x₂ y₂ ∷ [])
    ( iLe
      (iAdd (iScale twoInt x₂) (int threeInt))
      (iAdd (iScale twoInt y₂) (int threeInt))
    )

valid-diseq-symmetry : Problem Γxy
valid-diseq-symmetry =
  problem (iNe x₂ y₂ ∷ []) (iNe y₂ x₂)

valid-guarded-ite-nonnegative : Problem Γbxy
valid-guarded-ite-nonnegative =
  problem
    ( bImp b₃ (iGe xᵇ (int zeroInt))
    ∷ bImp (bNot b₃) (iGe yᵇ (int zeroInt))
    ∷ []
    )
    (iGe (ite b₃ xᵇ yᵇ) (int zeroInt))

valid-inconsistent-assumptions : Problem Γx
valid-inconsistent-assumptions =
  problem
    ( iGt x₁ (int zeroInt)
    ∷ iLe x₁ (int zeroInt)
    ∷ []
    )
    (bool false)

invalid-nonnegative-sum-positive : Problem Γxy
invalid-nonnegative-sum-positive =
  problem
    ( iGe x₂ (int zeroInt)
    ∷ iGe y₂ (int zeroInt)
    ∷ []
    )
    (iGt (iAdd x₂ y₂) (int zeroInt))

invalid-nonnegative-sum-positive-counterexample :
  Counterexample invalid-nonnegative-sum-positive
invalid-nonnegative-sum-positive-counterexample =
  counterexample
    (zeroInt , (zeroInt , tt))
    (refl all∷ refl all∷ all[])
    refl

not-invalid-nonnegative-sum-positive :
  ¬ Statement invalid-nonnegative-sum-positive
not-invalid-nonnegative-sum-positive =
  refute invalid-nonnegative-sum-positive-counterexample

invalid-negative-scale-monotone : Problem Γxy
invalid-negative-scale-monotone =
  problem
    (iLe x₂ y₂ ∷ [])
    (iLe (iScale minusOne x₂) (iScale minusOne y₂))

invalid-negative-scale-monotone-counterexample :
  Counterexample invalid-negative-scale-monotone
invalid-negative-scale-monotone-counterexample =
  counterexample
    (zeroInt , (oneInt , tt))
    (refl all∷ all[])
    refl

not-invalid-negative-scale-monotone :
  ¬ Statement invalid-negative-scale-monotone
not-invalid-negative-scale-monotone =
  refute invalid-negative-scale-monotone-counterexample

invalid-unguarded-ite-lower-bound : Problem Γbxy
invalid-unguarded-ite-lower-bound =
  problem [] (iGe (ite b₃ xᵇ yᵇ) xᵇ)

invalid-unguarded-ite-lower-bound-counterexample :
  Counterexample invalid-unguarded-ite-lower-bound
invalid-unguarded-ite-lower-bound-counterexample =
  counterexample
    (false , (oneInt , (zeroInt , tt)))
    all[]
    refl

not-invalid-unguarded-ite-lower-bound :
  ¬ Statement invalid-unguarded-ite-lower-bound
not-invalid-unguarded-ite-lower-bound =
  refute invalid-unguarded-ite-lower-bound-counterexample

invalid-linear-offset-cancel : Problem Γxyz
invalid-linear-offset-cancel =
  problem
    (iEq (iAdd x₃ y₃) z₃ ∷ [])
    (iEq x₃ z₃)

invalid-linear-offset-cancel-counterexample :
  Counterexample invalid-linear-offset-cancel
invalid-linear-offset-cancel-counterexample =
  counterexample
    (oneInt , (oneInt , (twoInt , tt)))
    (refl all∷ all[])
    refl

not-invalid-linear-offset-cancel :
  ¬ Statement invalid-linear-offset-cancel
not-invalid-linear-offset-cancel =
  refute invalid-linear-offset-cancel-counterexample

valid-ite-with-arithmetic-branches : Problem Γbxy
valid-ite-with-arithmetic-branches =
  problem
    ( iGe xᵇ (int zeroInt)
    ∷ iGe yᵇ (int zeroInt)
    ∷ []
    )
    ( iGe
      (ite b₃ (iAdd xᵇ (int oneInt)) (iAdd yᵇ (int oneInt)))
      (int oneInt)
    )

valid-nested-boolean-guard : Problem Γbxy
valid-nested-boolean-guard =
  problem
    ( bOr b₃ (bNot b₃)
    ∷ bImp b₃ (iGt xᵇ (int zeroInt))
    ∷ bImp (bNot b₃) (iGt yᵇ (int zeroInt))
    ∷ []
    )
    (iGt (ite b₃ xᵇ yᵇ) (int zeroInt))