SMT.Examples.Advanced

module SMT.Examples.Advanced where

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

open import SMT.Core
open import SMT.Semantics
open import SMT.Syntax

zero one two three five ten : ℤ
zero = pos 0
one = pos 1
two = pos 2
three = pos 3
five = pos 5
ten = pos 10

minusOne minusTwo : ℤ
minusOne = negsuc 0
minusTwo = negsuc 1

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

x1 : Expr Gx sInt
x1 = var vz

Gxy : Ctx
Gxy = decl "x" sInt ∷ decl "y" sInt ∷ []

x2 : Expr Gxy sInt
x2 = var vz

y2 : Expr Gxy sInt
y2 = var (vs vz)

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

x3 : Expr Gxyz sInt
x3 = var vz

y3 : Expr Gxyz sInt
y3 = var (vs vz)

z3 : Expr Gxyz sInt
z3 = var (vs (vs vz))

Gpq : Ctx
Gpq = decl "p" sBool ∷ decl "q" sBool ∷ []

p2 : Expr Gpq sBool
p2 = var vz

q2 : Expr Gpq sBool
q2 = var (vs vz)

Gpqr : Ctx
Gpqr = decl "p" sBool ∷ decl "q" sBool ∷ decl "r" sBool ∷ []

p3 : Expr Gpqr sBool
p3 = var vz

q3 : Expr Gpqr sBool
q3 = var (vs vz)

r3 : Expr Gpqr sBool
r3 = var (vs (vs vz))

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

b3 : Expr Gbxy sBool
b3 = var vz

xb : Expr Gbxy sInt
xb = var (vs vz)

yb : Expr Gbxy sInt
yb = var (vs (vs vz))

Gbxyz : Ctx
Gbxyz =
  decl "b" sBool ∷ decl "x" sInt ∷ decl "y" sInt ∷ decl "z" sInt ∷ []

b4 : Expr Gbxyz sBool
b4 = var vz

xb4 : Expr Gbxyz sInt
xb4 = var (vs vz)

yb4 : Expr Gbxyz sInt
yb4 = var (vs (vs vz))

zb4 : Expr Gbxyz sInt
zb4 = var (vs (vs (vs vz)))

valid-subtract-back : Problem Gxy
valid-subtract-back =
  [] ⊢ x2 +ᵢ y2 -ᵢ y2 ≡ᵢ x2

valid-negated-subtraction : Problem Gxy
valid-negated-subtraction =
  [] ⊢ -ᵢ (x2 -ᵢ y2) ≡ᵢ y2 -ᵢ x2

valid-strict-chain : Problem Gxyz
valid-strict-chain =
  (x3 <ᵢ y3 ∷ y3 ≤ᵢ z3 ∷ []) ⊢ x3 <ᵢ z3

valid-diseq-from-strict : Problem Gxy
valid-diseq-from-strict =
  (x2 <ᵢ y2 ∷ []) ⊢ x2 ≠ᵢ y2

valid-absolute-value-nonnegative : Problem Gx
valid-absolute-value-nonnegative =
  [] ⊢ (ifᵉ x1 ≥ᵢ int zero then x1 else -ᵢ x1) ≥ᵢ int zero

valid-conditional-upper-bound : Problem Gbxyz
valid-conditional-upper-bound =
  ( xb4 ≤ᵢ zb4
    ∷ yb4 ≤ᵢ zb4
    ∷ []
  )
  ⊢ (ifᵉ b4 then xb4 else yb4) ≤ᵢ zb4

valid-branch-refinement : Problem Gbxy
valid-branch-refinement =
  ( b3 ⇒ᵇ xb ≥ᵢ int two
    ∷ ¬ᵇ b3 ⇒ᵇ yb ≥ᵢ int three
    ∷ []
  )
  ⊢ (ifᵉ b3 then xb -ᵢ int two else yb -ᵢ int three) ≥ᵢ int zero

valid-additive-upper-bound : Problem Gxyz
valid-additive-upper-bound =
  ( x3 ≤ᵢ y3
    ∷ z3 ≤ᵢ int zero
    ∷ []
  )
  ⊢ x3 +ᵢ z3 ≤ᵢ y3

valid-unsat-numeric-assumptions : Problem Gxy
valid-unsat-numeric-assumptions =
  (x2 <ᵢ y2 ∷ y2 ≤ᵢ x2 ∷ []) ⊢ ⊥ᵇ

valid-boolean-resolution : Problem Gpq
valid-boolean-resolution =
  (p2 ∨ᵇ q2 ∷ ¬ᵇ p2 ∷ []) ⊢ q2

semantic-valid-boolean-resolution :
  SemanticStatement valid-boolean-resolution
semantic-valid-boolean-resolution ρ (hor holds∷ (hnotp holds∷ allHolds[])) with
  or-sound {ρ = ρ} {p = p2} {q = q2} hor
... | inl hp = Empty.rec (holds-refutes-contradiction {ρ = ρ} {p = p2} hp hnotp)
... | inr hq = hq

statement-valid-boolean-resolution : Statement valid-boolean-resolution
statement-valid-boolean-resolution =
  semantic→statement {p = valid-boolean-resolution} semantic-valid-boolean-resolution

valid-xor-left-elim : Problem Gpq
valid-xor-left-elim =
  (p2 ⊕ᵇ q2 ∷ p2 ∷ []) ⊢ ¬ᵇ q2

semantic-valid-xor-left-elim : SemanticStatement valid-xor-left-elim
semantic-valid-xor-left-elim ρ (hxor holds∷ (hp holds∷ allHolds[])) with
  xor-sound {ρ = ρ} {p = p2} {q = q2} hxor
... | inl (_ , hnotq) = hnotq
... | inr (hnotp , _) = Empty.rec (holds-refutes-contradiction {ρ = ρ} {p = p2} hp hnotp)

statement-valid-xor-left-elim : Statement valid-xor-left-elim
statement-valid-xor-left-elim =
  semantic→statement {p = valid-xor-left-elim} semantic-valid-xor-left-elim

valid-implication-chain : Problem Gpqr
valid-implication-chain =
  (p3 ⇒ᵇ q3 ∷ q3 ⇒ᵇ r3 ∷ p3 ∷ []) ⊢ r3

semantic-valid-implication-chain : SemanticStatement valid-implication-chain
semantic-valid-implication-chain ρ (hpq holds∷ (hqr holds∷ (hp holds∷ allHolds[]))) =
  imp-sound {ρ = ρ} {p = q3} {q = r3} hqr
    (imp-sound {ρ = ρ} {p = p3} {q = q3} hpq hp)

statement-valid-implication-chain : Statement valid-implication-chain
statement-valid-implication-chain =
  semantic→statement {p = valid-implication-chain} semantic-valid-implication-chain

invalid-strict-from-nonstrict : Problem Gxy
invalid-strict-from-nonstrict =
  (x2 ≤ᵢ y2 ∷ []) ⊢ x2 <ᵢ y2

invalid-strict-from-nonstrict-counterexample :
  Counterexample invalid-strict-from-nonstrict
invalid-strict-from-nonstrict-counterexample =
  counterexample
    (zero , (zero , tt))
    (refl all∷ all[])
    refl

not-invalid-strict-from-nonstrict : ¬ Statement invalid-strict-from-nonstrict
not-invalid-strict-from-nonstrict =
  refute invalid-strict-from-nonstrict-counterexample

invalid-diseq-from-nonstrict : Problem Gxy
invalid-diseq-from-nonstrict =
  (x2 ≤ᵢ y2 ∷ []) ⊢ x2 ≠ᵢ y2

invalid-diseq-from-nonstrict-counterexample :
  Counterexample invalid-diseq-from-nonstrict
invalid-diseq-from-nonstrict-counterexample =
  counterexample
    (zero , (zero , tt))
    (refl all∷ all[])
    refl

not-invalid-diseq-from-nonstrict : ¬ Statement invalid-diseq-from-nonstrict
not-invalid-diseq-from-nonstrict =
  refute invalid-diseq-from-nonstrict-counterexample

invalid-drop-branch-guard : Problem Gbxy
invalid-drop-branch-guard =
  (b3 ⇒ᵇ xb ≥ᵢ int zero ∷ []) ⊢ (ifᵉ b3 then xb else yb) ≥ᵢ int zero

invalid-drop-branch-guard-counterexample :
  Counterexample invalid-drop-branch-guard
invalid-drop-branch-guard-counterexample =
  counterexample
    (false , (zero , (minusOne , tt)))
    (refl all∷ all[])
    refl

not-invalid-drop-branch-guard : ¬ Statement invalid-drop-branch-guard
not-invalid-drop-branch-guard =
  refute invalid-drop-branch-guard-counterexample

invalid-boolean-resolution : Problem Gpq
invalid-boolean-resolution =
  (p2 ∨ᵇ q2 ∷ []) ⊢ q2

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

semantic-invalid-boolean-resolution-counterexample :
  SemanticCounterexample invalid-boolean-resolution
semantic-invalid-boolean-resolution-counterexample =
  semanticCounterexample
    (true , (false , tt))
    (tt holds∷ allHolds[])
    tt

not-invalid-boolean-resolution : ¬ Statement invalid-boolean-resolution
not-invalid-boolean-resolution =
  refute invalid-boolean-resolution-counterexample

not-invalid-boolean-resolution-semantic : ¬ Statement invalid-boolean-resolution
not-invalid-boolean-resolution-semantic =
  refuteSemantic semantic-invalid-boolean-resolution-counterexample

invalid-xor-to-left : Problem Gpq
invalid-xor-to-left =
  (p2 ⊕ᵇ q2 ∷ []) ⊢ p2

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

not-invalid-xor-to-left : ¬ Statement invalid-xor-to-left
not-invalid-xor-to-left = refute invalid-xor-to-left-counterexample

invalid-additive-cancel : Problem Gxyz
invalid-additive-cancel =
  (x3 ≤ᵢ y3 +ᵢ z3 ∷ []) ⊢ x3 ≤ᵢ y3

invalid-additive-cancel-counterexample : Counterexample invalid-additive-cancel
invalid-additive-cancel-counterexample =
  counterexample
    (two , (one , (one , tt)))
    (refl all∷ all[])
    refl

not-invalid-additive-cancel : ¬ Statement invalid-additive-cancel
not-invalid-additive-cancel = refute invalid-additive-cancel-counterexample

invalid-absolute-value-positive : Problem Gx
invalid-absolute-value-positive =
  [] ⊢ (ifᵉ x1 ≥ᵢ int zero then x1 else -ᵢ x1) >ᵢ int zero

invalid-absolute-value-positive-counterexample :
  Counterexample invalid-absolute-value-positive
invalid-absolute-value-positive-counterexample =
  counterexample
    (zero , tt)
    all[]
    refl

not-invalid-absolute-value-positive :
  ¬ Statement invalid-absolute-value-positive
not-invalid-absolute-value-positive =
  refute invalid-absolute-value-positive-counterexample

invalid-subtraction-bound : Problem Gxyz
invalid-subtraction-bound =
  (x3 ≤ᵢ y3 ∷ z3 >ᵢ int zero ∷ []) ⊢ x3 ≤ᵢ y3 -ᵢ z3

invalid-subtraction-bound-counterexample :
  Counterexample invalid-subtraction-bound
invalid-subtraction-bound-counterexample =
  counterexample
    (zero , (zero , (one , tt)))
    (refl all∷ refl all∷ all[])
    refl

not-invalid-subtraction-bound : ¬ Statement invalid-subtraction-bound
not-invalid-subtraction-bound =
  refute invalid-subtraction-bound-counterexample

invalid-positive-sum-left : Problem Gxy
invalid-positive-sum-left =
  (x2 +ᵢ y2 >ᵢ int zero ∷ y2 >ᵢ int zero ∷ []) ⊢ x2 >ᵢ int zero

invalid-positive-sum-left-counterexample :
  Counterexample invalid-positive-sum-left
invalid-positive-sum-left-counterexample =
  counterexample
    (minusOne , (two , tt))
    (refl all∷ refl all∷ all[])
    refl

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

invalid-branch-equality : Problem Gbxy
invalid-branch-equality =
  [] ⊢ (ifᵉ b3 then xb else yb) ≡ᵢ xb

invalid-branch-equality-counterexample : Counterexample invalid-branch-equality
invalid-branch-equality-counterexample =
  counterexample
    (false , (zero , (one , tt)))
    all[]
    refl

not-invalid-branch-equality : ¬ Statement invalid-branch-equality
not-invalid-branch-equality =
  refute invalid-branch-equality-counterexample