wip on gfp strategy for nu, base case for ltl ind rule goes through

Author: lucaspena

prover/lang/kore-lang.md

@@ -163,6 +163,7 @@ only in this scenario*.
                    | "\\forall" "{" Patterns "}" Pattern        [klabel(forall)]
 
                    | "\\mu" SetVariable "." Pattern             [klabel(mu)]
+                   | "\\nu" SetVariable "." Pattern             [klabel(nu)]
                      /* Sugar for \iff, \mu and application */
                    | "\\iff-lfp" "(" Pattern "," Pattern ")"    [klabel(ifflfp)]
 
@@ -354,6 +355,7 @@ module KORE-HELPERS
        requires getReturnSort(P) =/=K S
 
   rule getReturnSort(\mu _ . Phi) => getReturnSort(Phi)
+  rule getReturnSort(\nu _ . Phi) => getReturnSort(Phi)
   rule getReturnSort(\or(P, Ps)) => unionSort(getReturnSort(P), getReturnSort(\or(Ps)))
   rule getReturnSort(\or(.Patterns)) => BottomSort
   rule getReturnSort(\and(P, Ps)) => intersectSort(getReturnSort(P), getReturnSort(\and(Ps)))
@@ -604,6 +606,8 @@ where the term being unfolded has been replace by `#hole`.
   rule subst(X:Variable,Y:Variable,V) => X    requires X =/=K Y
   rule subst(X:SetVariable,Y:SetVariable,V) => X requires X =/=K Y
   rule subst(X:Variable,P:Pattern, V) => X    requires notBool(isVariable(P) orBool isVariableName(P))
+  rule subst(X:SetVariable,P:Pattern, V) => X
+    requires notBool(isSetVariable(P))
   rule subst(I:Int, X, V) => I
   rule subst(\top(),_,_)=> \top()
   rule subst(\bottom(),_,_) => \bottom()
@@ -680,6 +684,7 @@ Alpha renaming: Rename all bound variables. Free variables are left unchanged.
   rule alphaRename(\exists { Fs:Patterns } P:Pattern)
     => #fun(RENAMING => \exists { Fs[RENAMING] } alphaRename(substMap(P,RENAMING))) ( makeFreshSubstitution(Fs) )
   rule alphaRename(\mu X . P:Pattern) => \mu !X . alphaRename(subst(P, X, !X))
+  rule alphaRename(\nu X . P:Pattern) => \nu !X . alphaRename(subst(P, X, !X))
   rule alphaRename(\equals(L, R)) => \equals(alphaRename(L), alphaRename(R))
   rule alphaRename(\not(Ps)) => \not(alphaRename(Ps))
   rule alphaRename(\functionalPattern(Ps)) => \functionalPattern(alphaRename(Ps))
@@ -753,12 +758,14 @@ single symbol applied to multiple arguments.
   rule #nnf(S:Symbol(Args)) => S(#nnfPs(Args))
   rule #nnf( \or(Ps)) =>  \or(#nnfPs(Ps))
   rule #nnf(\and(Ps)) => \and(#nnfPs(Ps))
+  rule #nnf(\implies(L, R)) => #nnf(\or(\not(L), R))
 
   rule #nnf(\not(P)) => \not(P) requires isDnfAtom(P)
   rule #nnf(\not(S:Symbol(Args))) => \not(S(#nnfPs(Args)))
   rule #nnf(\not( \or(Ps))) => \and(#nnfPs(#not(Ps)))
   rule #nnf(\not(\and(Ps))) => \or(#nnfPs(#not(Ps)))
   rule #nnf(\not(\not(P))) => #nnf(P)
+  rule #nnf(\not(\implies(L, R))) => #nnf(\not(\or(\not(L), R)))
 
   syntax Bool ::= isDnfAtom(Pattern) [function]
   rule isDnfAtom(V:Variable) => true
@@ -768,9 +775,11 @@ single symbol applied to multiple arguments.
   rule isDnfAtom(\exists{Vs}_) => true
   rule isDnfAtom(\forall{Vs}_) => true
   rule isDnfAtom(\mu X . _) => true
+  rule isDnfAtom(\nu X . _) => true
   rule isDnfAtom(implicationContext(_, _)) => true
   rule isDnfAtom(\and(_)) => false
   rule isDnfAtom(\or(_)) => false
+  rule isDnfAtom(\implies(_, _)) => false
   rule isDnfAtom(S:Symbol(ARGS)) => false
   rule isDnfAtom(\not(P)) => false
 ```

prover/prover.md

@@ -56,7 +56,7 @@ module STRATEGIES-EXPORTED-SYNTAX
                     | "right-unfold"      "(" "symbols" ":" Patterns "," "bound" ":" Int ")"
                     | "kt"     | "kt"     "#" KTFilter
                     | "kt-unf" | "kt-unf" "#" KTFilter
-                    | "kt-gfp" | "kt-gfp" "#" KTFilter
+                    | "gfp"
                     | "kt-solve-implications" "(" Strategy ")"
                     | "instantiate-universals-with-ground-terms"
                     | "instantiate-separation-logic-axioms" | "pto-is-injective"

prover/strategies/core.md

@@ -26,7 +26,7 @@ module PROVER-CORE-SYNTAX
                           | Strategy "&" Strategy [right, format(%1%n%2  %3)]
                           | Strategy "|" Strategy [right, format(%1%n%2  %3)]
   syntax Strategy ::= "or-split" | "and-split" | "or-split-rhs" | "and-split-rhs"
-  syntax Strategy ::= "rhs-top"
+  syntax Strategy ::= "rhs-top" | "contradiction"
   syntax Strategy ::= "prune" "(" Patterns ")"
 
   syntax Strategy ::= Strategy "{" Int "}"
@@ -294,6 +294,14 @@ Internal strategy used to implement `or-split` and `and-split`.
        <k> rhs-top => success ... </k>
 ```
 
+`contradiction` evaluates to success if the second clause is the negation of the first
+clause in the LHS conjunction
+
+```k
+  rule <claim> \implies(\and(P, \not(P), REST), RHS) </claim>
+       <k> contradiction => success ... </k>
+```
+
 If-then-else-fi strategy is useful for implementing other strategies:
 
 ```k

prover/strategies/knaster-tarski.md

@@ -249,6 +249,12 @@ for guessing an instantiation of the inductive hypothesis.
        </k>
   rule <k> kt-subst(.Patterns, ARGs) => noop ... </k>
 
+  // TODO: combine with other kt-unfold rules
+  rule <claim> \implies(LHS, \nu X . P)
+        => \implies(LHS, subst(P, X, alphaRename(LHS)))
+       </claim>
+       <k> gfp => noop ... </k>
+
                              // unfolded fixed point, HEAD, LRP variables, RHS
   syntax Pattern ::= substituteBRPs(Pattern,  Symbol, Patterns, Pattern) [function]
   rule substituteBRPs(P:Int, RP, Vs, RHS) => P

prover/strategies/matching.md

@@ -206,6 +206,17 @@ Recurse over assoc-only constructors (including `pto`):
                   , rest:      REST
                   )
 
+  // Both term and pattern are a nu:
+  // Recurse over pattern with same fresh variable for each nu term
+  rule #matchAssoc( terms:     (\nu X . T), Ts
+                            => subst(T, X, !F:SetVariable), Ts
+                  , pattern:   (\nu Y . P), Ps
+                            => subst(P, Y, !F), Ps
+                  , variables: Vs
+                  , subst:     SUBST
+                  , rest:      REST
+                  )
+
   // ground variable: identical
   rule #matchAssoc( terms:     P:Variable, Ts => Ts
                   , pattern:   P, Ps => Ps

prover/strategies/unfolding.md

@@ -13,6 +13,7 @@ module STRATEGY-UNFOLDING
        <declaration> axiom _: \forall { Vs } \iff-lfp(S(Vs), DEF) </declaration>
     requires getFreeVariables(DEF) -Patterns Vs =/=K .Patterns
   rule unfold(\mu X . P) => subst(P, X, alphaRename(\mu X . P))
+  rule unfold(\nu X . P) => subst(P, X, alphaRename(\nu X . P))
 
   syntax SymbolDeclaration ::= getSymbolDeclaration(Symbol) [function]
   rule [[ getSymbolDeclaration(S) => DECL ]]
@@ -33,6 +34,8 @@ module STRATEGY-UNFOLDING
     requires isUnfoldable(R)
   rule getUnfoldables(\mu X . P, REST)
     => \mu X . P, getUnfoldables(REST)
+  rule getUnfoldables(\nu X . P, REST)
+    => \nu X . P, getUnfoldables(REST)
   rule getUnfoldables(S:Symbol, REST)
     => getUnfoldables(REST)
     requires notBool isUnfoldable(S)
@@ -44,6 +47,8 @@ module STRATEGY-UNFOLDING
     => getUnfoldables(REST)
   rule getUnfoldables(V:Variable, REST)
     => getUnfoldables(REST)
+  rule getUnfoldables(X:SetVariable, REST)
+    => getUnfoldables(REST)
   rule getUnfoldables(\not(Ps), REST)
     => getUnfoldables(Ps) ++Patterns getUnfoldables(REST)
   rule getUnfoldables(\and(Ps), REST)
@@ -88,7 +93,7 @@ module STRATEGY-UNFOLDING
        </claim>
        <k> left-unfold-oneBody(LRP, \exists { _ } \and(BODY)) => noop ... </k>
        <trace> .K => left-unfold-oneBody(LRP, \and(BODY)) ... </trace>
-    requires #hole { getReturnSort(LRP) } in getFreeVariables(subst(LHS, LRP, #hole { getReturnSort(LRP) }))
+    requires #hole { TopSort } in getFreeVariables(subst(LHS, LRP, #hole { TopSort }))
 ```
 
 ### Left Unfold Nth