From 832e8de15bedbb8e67b74891bd0363350f6dc14b Mon Sep 17 00:00:00 2001 From: Frederik Krogsdal Jacobsen Date: Wed, 10 Apr 2024 10:57:40 +0200 Subject: [PATCH] Fix bug in proof extraction of consecutive Delta rules. The bug occurred when several Delta rules were applied in the same prover round, and caused generated function names to not be fresh beginning with the second Delta rule of the round. The remainder of the proof was unaffected, starting with the first Ext rule after the Alpha-Delta phase. The bug was due to the fact that the fresh name generated by each Delta rule was not carried forward internally in the round, but only "re-discovered" after the end of the phase. The bug did not affect the prover algorithm, only the generation of proof certificates. Verification of proof certificates for formulas affected by the bug would fail despite the prover finding a proof, since the proof certificate would not contain a valid proof. --- haskell/lib/ProofExtractor.hs | 32 ++++++++++++++++++-------------- 1 file changed, 18 insertions(+), 14 deletions(-) diff --git a/haskell/lib/ProofExtractor.hs b/haskell/lib/ProofExtractor.hs index 2441a18..01a915c 100644 --- a/haskell/lib/ProofExtractor.hs +++ b/haskell/lib/ProofExtractor.hs @@ -53,23 +53,27 @@ second (_ : xs) = first xs -- Expansion of the alpha, delta, and double negation elimination rules expandAlphaDelta :: Tree (([Tm], [Fm]), Rule) -> Int -> Tree ([Fm], SeCaVRule) expandAlphaDelta (Node ((terms, f : fs), rule) (Abs_fset (Set [current]))) n = - let (srule, applied) = case (rule, f) of - (AlphaDis, Dis p q) -> (RAlphaDis, [p, q]) - (AlphaCon, Neg (Con p q)) -> (RAlphaCon, [Neg p, Neg q]) - (AlphaImp, Imp p q) -> (RAlphaImp, [Neg p, q]) - (NegNeg, Neg (Neg p)) -> (RNeg, [p]) - (DeltaUni, Uni p) -> (RDeltaUni, [SeCaV.sub Arith.zero_nat (SeCaV.Fun (generateNew terms) []) p]) - (DeltaExi, Neg (Exi p)) -> (RDeltaExi, [Neg (SeCaV.sub Arith.zero_nat (SeCaV.Fun (generateNew terms) []) p)]) - (AlphaDis, x) -> (RAlphaDis, [x]) - (AlphaCon, x) -> (RAlphaCon, [x]) - (AlphaImp, x) -> (RAlphaImp, [x]) - (DeltaUni, x) -> (RDeltaUni, [x]) - (DeltaExi, x) -> (RDeltaExi, [x]) - (NegNeg, x) -> (RNeg, [x]) + let (srule, applied, newTerms) = case (rule, f) of + (AlphaDis, Dis p q) -> (RAlphaDis, [p, q], []) + (AlphaCon, Neg (Con p q)) -> (RAlphaCon, [Neg p, Neg q], []) + (AlphaImp, Imp p q) -> (RAlphaImp, [Neg p, q], []) + (NegNeg, Neg (Neg p)) -> (RNeg, [p], []) + (DeltaUni, Uni p) -> + let newFun = SeCaV.Fun (generateNew terms) [] in + (RDeltaUni, [SeCaV.sub Arith.zero_nat newFun p], [newFun]) + (DeltaExi, Neg (Exi p)) -> + let newFun = SeCaV.Fun (generateNew terms) [] in + (RDeltaExi, [Neg (SeCaV.sub Arith.zero_nat newFun p)], [newFun]) + (AlphaDis, x) -> (RAlphaDis, [x], []) + (AlphaCon, x) -> (RAlphaCon, [x], []) + (AlphaImp, x) -> (RAlphaImp, [x], []) + (DeltaUni, x) -> (RDeltaUni, [x], []) + (DeltaExi, x) -> (RDeltaExi, [x], []) + (NegNeg, x) -> (RNeg, [x], []) _ -> error "expandAlphaDelta must only be called on Alpha, Neg or Delta rules." in let extRule = if n == 1 then Node (applied ++ fs, RExt) (Abs_fset (Set [expandMultiRules current])) - else Node (applied ++ fs, RExt) (Abs_fset (Set [expandAlphaDelta (Node ((terms, fs ++ applied), rule) (Abs_fset (Set [current]))) (n - 1)])) in + else Node (applied ++ fs, RExt) (Abs_fset (Set [expandAlphaDelta (Node ((terms ++ newTerms, fs ++ applied), rule) (Abs_fset (Set [current]))) (n - 1)])) in Node (f : fs, srule) (Abs_fset (Set [extRule])) expandAlphaDelta (Node ((_, []), _) _) _ = error "The sequent must never be empty." expandAlphaDelta (Node ((_, _), _) (Abs_fset (Coset _))) _ = error "The proof tree must not include cosets."