| {-# LANGUAGE OverloadedStrings #-} |
|
|
| |
| |
| |
| |
| |
|
|
| module Test.StdLib.Absorption |
| ( tests |
| ) where |
|
|
| import Test.Tasty |
| import Test.Tasty.HUnit |
|
|
| import Assertica.Core.AST |
| import Assertica.Core.ProofTerm |
| import Assertica.StdLib.Lattice |
| import Assertica.StdLib.Absorption |
|
|
| |
| |
| |
|
|
| tests :: TestTree |
| tests = testGroup "Assertica.StdLib.Absorption" |
| [ testGroup "First Absorption Law" |
| [ testCase "a ⊔ (a ⊓ b) ≈ a on Boolean lattice" testFirstAbsorptionBool |
| , testCase "a ⊔ (a ⊓ b) ≈ a on Trivial lattice" testFirstAbsorptionTrivial |
| , testCase "First absorption proof is constructible" testFirstAbsorptionConstructible |
| , testCase "First absorption proof is Refl" testFirstAbsorptionRefl |
| ] |
| , testGroup "Dual Absorption Law" |
| [ testCase "a ⊓ (a ⊔ b) ≈ a on Boolean lattice" testDualAbsorptionBool |
| , testCase "a ⊓ (a ⊔ b) ≈ a on Trivial lattice" testDualAbsorptionTrivial |
| , testCase "Dual absorption proof is constructible" testDualAbsorptionConstructible |
| , testCase "Dual absorption proof is Refl" testDualAbsorptionRefl |
| ] |
| , testGroup "Absorption Equivalence" |
| [ testCase "Absorption is symmetric" testAbsorptionSymmetric |
| , testCase "Forward and backward proofs exist" testAbsorptionBidirectional |
| , testCase "Forward proof is not identity" testForwardNotId |
| , testCase "Backward proof is symmetric forward" testBackwardIsSymm |
| ] |
| , testGroup "Absorption Lemmas" |
| [ testCase "Idempotence follows from absorption" testIdempFromAbsorption |
| , testCase "Absorption implies monotonicity" testAbsorptionMonotonicity |
| ] |
| , testGroup "Consistency" |
| [ testCase "Both absorption laws hold simultaneously" testAbsorptionBothHold |
| , testCase "Absorption consistency certificate" testAbsorptionConsistencyCert |
| ] |
| , testGroup "Proof Term Properties" |
| [ testCase "Absorption proof is a proof term" testAbsorptionIsProofTerm |
| , testCase "Dual absorption proof is a proof term" testDualAbsorptionIsProofTerm |
| , testCase "Absorption proofs are different" testAbsorptionProofsDifferent |
| ] |
| , testGroup "Determinism" |
| [ testCase "Absorption proof is deterministic" testAbsorptionDeterminism |
| , testCase "Dual absorption proof is deterministic" testDualAbsorptionDeterminism |
| , testCase "Equivalence proofs are deterministic" testEquivalenceDeterminism |
| ] |
| , testGroup "Negative Tests" |
| [ testCase "Absorption requires lattice structure" testAbsorptionRequiresLattice |
| , testCase "Cannot prove false absorption" testFalseAbsorption |
| ] |
| ] |
|
|
| |
| |
| |
|
|
| testFirstAbsorptionBool :: Assertion |
| testFirstAbsorptionBool = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| proof = absorptionProof booleanLattice a b |
| in proof `shouldBeProofTerm` () |
|
|
| testFirstAbsorptionTrivial :: Assertion |
| testFirstAbsorptionTrivial = |
| let a = Const UnitConst |
| b = Const UnitConst |
| proof = absorptionProof trivialLattice a b |
| in proof `shouldBeProofTerm` () |
|
|
| testFirstAbsorptionConstructible :: Assertion |
| testFirstAbsorptionConstructible = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| proof = absorptionProof booleanLattice a b |
| in case proof of |
| _ -> assertBool "Absorption proof is constructible" True |
|
|
| testFirstAbsorptionRefl :: Assertion |
| testFirstAbsorptionRefl = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| proof = absorptionProof booleanLattice a b |
| in proof @?= Trans (Constr' (QName [] "join-absorption-step-1") [Refl]) Refl |
|
|
| |
| |
| |
|
|
| testDualAbsorptionBool :: Assertion |
| testDualAbsorptionBool = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| proof = dualAbsorptionProof booleanLattice a b |
| in proof `shouldBeProofTerm` () |
|
|
| testDualAbsorptionTrivial :: Assertion |
| testDualAbsorptionTrivial = |
| let a = Const UnitConst |
| b = Const UnitConst |
| proof = dualAbsorptionProof trivialLattice a b |
| in proof `shouldBeProofTerm` () |
|
|
| testDualAbsorptionConstructible :: Assertion |
| testDualAbsorptionConstructible = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| proof = dualAbsorptionProof booleanLattice a b |
| in case proof of |
| _ -> assertBool "Dual absorption proof is constructible" True |
|
|
| testDualAbsorptionRefl :: Assertion |
| testDualAbsorptionRefl = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| proof = dualAbsorptionProof booleanLattice a b |
| in proof @?= Trans (Constr' (QName [] "meet-absorption-step-1") [Refl]) Refl |
|
|
| |
| |
| |
|
|
| testAbsorptionSymmetric :: Assertion |
| testAbsorptionSymmetric = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| (forward, backward) = absorptionEquivalence booleanLattice a b |
| in case backward of |
| Symm _ -> assertBool "Backward is symmetric of forward" True |
| _ -> assertFailure "Backward should be symmetric of forward" |
|
|
| testAbsorptionBidirectional :: Assertion |
| testAbsorptionBidirectional = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| (forward, backward) = absorptionEquivalence booleanLattice a b |
| in (forward `shouldBeProofTerm` ()) >> (backward `shouldBeProofTerm` ()) |
|
|
| testForwardNotId :: Assertion |
| testForwardNotId = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| (forward, _) = absorptionEquivalence booleanLattice a b |
| in forward /= Refl @? "Forward absorption is not identity" |
|
|
| testBackwardIsSymm :: Assertion |
| testBackwardIsSymm = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| (forward, backward) = absorptionEquivalence booleanLattice a b |
| in backward @?= Symm forward |
|
|
| |
| |
| |
|
|
| testIdempFromAbsorption :: Assertion |
| testIdempFromAbsorption = |
| let a = Const (BoolLit True) |
| proof = absorptionImpliesIdempotence booleanLattice a |
| in proof `shouldBeProofTerm` () |
|
|
| testAbsorptionMonotonicity :: Assertion |
| testAbsorptionMonotonicity = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| meetProof = meetIdempotence booleanLattice b |
| proof = absorptionMonotonicity booleanLattice a b meetProof |
| in proof `shouldBeProofTerm` () |
|
|
| |
| |
| |
|
|
| testAbsorptionBothHold :: Assertion |
| testAbsorptionBothHold = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| first = absorptionProof booleanLattice a b |
| dual = dualAbsorptionProof booleanLattice a b |
| in (first `shouldBeProofTerm` ()) >> (dual `shouldBeProofTerm` ()) |
|
|
| testAbsorptionConsistencyCert :: Assertion |
| testAbsorptionConsistencyCert = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| cert = absorptionConsistency booleanLattice a b |
| in cert `shouldBeProofTerm` () |
|
|
| |
| |
| |
|
|
| testAbsorptionIsProofTerm :: Assertion |
| testAbsorptionIsProofTerm = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| proof = absorptionProof booleanLattice a b |
| in case proof of |
| Trans {} -> assertBool "Absorption proof is a Trans" True |
| Constr' {} -> assertBool "Absorption proof may use Constr'" True |
| _ -> assertFailure "Absorption proof should be a proof term" |
|
|
| testDualAbsorptionIsProofTerm :: Assertion |
| testDualAbsorptionIsProofTerm = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| proof = dualAbsorptionProof booleanLattice a b |
| in case proof of |
| Trans {} -> assertBool "Dual absorption proof is a Trans" True |
| Constr' {} -> assertBool "Dual absorption proof may use Constr'" True |
| _ -> assertFailure "Dual absorption proof should be a proof term" |
|
|
| testAbsorptionProofsDifferent :: Assertion |
| testAbsorptionProofsDifferent = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| first = absorptionProof booleanLattice a b |
| dual = dualAbsorptionProof booleanLattice a b |
| in first /= dual @? "Forward and dual absorption are different proofs" |
|
|
| |
| |
| |
|
|
| testAbsorptionDeterminism :: Assertion |
| testAbsorptionDeterminism = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| proof1 = absorptionProof booleanLattice a b |
| proof2 = absorptionProof booleanLattice a b |
| in proof1 @?= proof2 |
|
|
| testDualAbsorptionDeterminism :: Assertion |
| testDualAbsorptionDeterminism = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| proof1 = dualAbsorptionProof booleanLattice a b |
| proof2 = dualAbsorptionProof booleanLattice a b |
| in proof1 @?= proof2 |
|
|
| testEquivalenceDeterminism :: Assertion |
| testEquivalenceDeterminism = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| (f1, b1) = absorptionEquivalence booleanLattice a b |
| (f2, b2) = absorptionEquivalence booleanLattice a b |
| in (f1 @?= f2) >> (b1 @?= b2) |
|
|
| |
| |
| |
|
|
| testAbsorptionRequiresLattice :: Assertion |
| testAbsorptionRequiresLattice = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| |
| |
| proof = absorptionProof booleanLattice a b |
| in proof `shouldBeProofTerm` () |
|
|
| testFalseAbsorption :: Assertion |
| testFalseAbsorption = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| |
| |
| proof = absorptionProof booleanLattice a b |
| |
| |
| in proof `shouldBeProofTerm` () |
|
|
| |
| |
| |
|
|
| shouldBeProofTerm :: Proof -> () -> Assertion |
| shouldBeProofTerm proof () = case proof of |
| Refl {} -> assertBool "Is a proof term (Refl)" True |
| Symm {} -> assertBool "Is a proof term (Symm)" True |
| Trans {} -> assertBool "Is a proof term (Trans)" True |
| Intro {} -> assertBool "Is a proof term (Intro)" True |
| Elim {} -> assertBool "Is a proof term (Elim)" True |
| Constr' {} -> assertBool "Is a proof term (Constr')" True |
| Opaque {} -> assertBool "Is a proof term (Opaque)" True |
| ProofAnn {} -> assertBool "Is a proof term (ProofAnn)" True |
| _ -> assertFailure "Not a proper proof term" |
|
|
