copilot-theorem: Make the kind2 connection handle both existentially and universally quantified properties correctly #594
Description
Description
Copilot.Language.Spec.prop and Copilot.Language.Spec.theorem are both reified into as a bare stream of booleans, and do not retain information about whether the Prop passed as argument was a Forall or an Exists. This makes the use of the Kind2 connection in copilot-theorem render incorrect results.
Type
- Bug: Information is lost, leading to unexpected results .
Additional context
- Issue
copilot-theorem: Make What4 backend refuse to prove existentially quantified properties #254 will introduce enough information in streams to know which quantifier has been used, and adjust the What4 connection to use the information accordingly and refuse to prove properties that it cannot prove. The scope of this ticket is how to use that information, once available, to ensure thatcopilot-theoremproduces correct results when Kind2 is used.
Requester
- Rob Dockins.
Method to check presence of bug
The issue can be detected with the following sample programs:
{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where
import Data.Functor
import Copilot.Theorem.Kind2
import Copilot.Theorem.Prove
import Language.Copilot
trueThenFalses :: Stream Bool
trueThenFalses = [True] ++ constant False
spec :: Spec
spec = do
void $ theorem "t1" (forAll trueThenFalses) (check (kind2Prover def))
void $ theorem "t2" (exists trueThenFalses) (check (kind2Prover def))
main :: IO ()
main = void $ reify specExpected result
Running the specs above or a similar variant via Kind2 should print proof checked successfully as part of its output if it can prove a theorem true, and proof failed otherwise, indicating that respects the quantifier is being respected. For the cases above, t1 should be falsified, but t2 should succeed.
If the prover is not able to prove a property of a given type, a suitable error message should be printed.
Desired result
Running the specs above or a similar variant via Kind2 should print proof checked successfully as part of its output if it can prove a theorem true, and proof failed otherwise, indicating that respects the quantifier is being respected. For the cases above, t1 should be falsified, but t2 should succeed.
If the prover is not able to prove a property of a given type, a suitable error message should be printed.
Proposed solution
Modify copilot-theorem to properly use the information about the which quantifier was used, and translate it appropriately before sending it to Kind2.
Further notes
None.