How let-such-that expressions could be done in Dafny 3.1.0?

user_7957944 0
Viewed 56

Expressions let-such-that that worked in previous releases of Dafny do not work in Dafny 3.1.0. For example, the following code (also in https://rise4fun.com/Dafny/ABZpf) raise the error: "to be compilable, the value of a let-such-that expression must be uniquely determined".

datatype NNF_Formula =   F 
                       | T
                       | V(prop:string) 
                       | NegV(prop:string) 
                       | EX(f:NNF_Formula) 
                       | AX(f:NNF_Formula) 
                       | EG(f:NNF_Formula) 
                       | AG(f:NNF_Formula) 
                       | ER(f1:NNF_Formula,f2:NNF_Formula) 
                       | AR(f1:NNF_Formula,f2:NNF_Formula) 
                       | EF(f:NNF_Formula)  
                       | AF(f:NNF_Formula) 
                       | EU(f1:NNF_Formula,f2:NNF_Formula) 
                       | AU(f1:NNF_Formula,f2:NNF_Formula) 
                       | EUsel(f1:NNF_Formula,f2:NNF_Formula) 
                       | AUsel(f1:NNF_Formula,f2:NNF_Formula) 
                       | Or(f1:NNF_Formula,f2:NNF_Formula)
                       | And(f1:NNF_Formula,f2:NNF_Formula) 

function method family(alpha: NNF_Formula): nat {
  match alpha
  case F => 0
  case T => 1
  case V(_) => 2
  case NegV(_) => 3
  case AX(_) => 4
  case EX(_) => 5
  case AG(_) => 6
  case EG(_) => 7
  case AR(_, _) => 8
  case ER(_, _) => 9
  case AF(_) => 10
  case EF(_) => 11
  case AU(_, _) => 12
  case EU(_, _) => 13
  case AUsel(_, _) => 14
  case EUsel(_, _) => 15
  case Or(_, _) => 16
  case And(_, _) => 17
}

// ORDER IN NNF FORMULAS

predicate method leq_string(s1:string,s2:string) { 
s1 == "" || (s2 != "" && s1[0] <= s2[0] && ( s1[0] == s2[0] ==> leq_string(s1[1..],s2[1..])))
}

lemma antisym_leq_string_Lemma (s1:string, s2:string)
requires leq_string(s1,s2)  && leq_string(s2,s1) 
ensures s1 == s2
{
if s1 != "" && s2 != "" { antisym_leq_string_Lemma(s1[1..],s2[1..]); }
}


predicate method leq_NNF_Formula (alpha:NNF_Formula, beta:NNF_Formula)
{
if family(alpha) < family(beta) then true
else if family(alpha) > family(beta) then false
else if family(alpha) <= 1 then true
else if 2 <= family(alpha) <= 3 then leq_string(alpha.prop,beta.prop) 
else if 4 <= family(alpha) <= 7 || 10 <= family(alpha) <= 11 then leq_NNF_Formula(alpha.f,beta.f) 
else leq_NNF_Formula(alpha.f1,beta.f1) && (alpha.f1 == beta.f1 ==> leq_NNF_Formula(alpha.f2,beta.f2)) 
}

lemma minimum_formula_Lemma (s:set<NNF_Formula>)
requires s != {}
ensures exists phi :: phi in s && forall psi :: psi in s-{phi}  ==> (leq_NNF_Formula(phi,psi) && psi != phi)

function method pick_minimum_formula(s: set<NNF_Formula>): NNF_Formula
requires s != {}
{
minimum_formula_Lemma(s); 
var phi :| phi in s && forall psi :: psi in s-{phi}  ==> (leq_NNF_Formula(phi,psi) && psi != phi);
phi
}

For clarity, I have omitted the proof of the lemma, but it can be proved. I have also complicated a bit the ensures of the lemma for ensured uniqueness. In previous releases of Dafny also this works: ensures exists phi :: phi in s && forall psi :: psi in s ==> leq_NNF_Formula(phi,psi).

I need some way of iteration on sets of NNF_Formula, is there a different way to do this on Dafny 3.1.0?

dafny
1 Answers

This error could certainly serve to be clearer.

This scenario is only disallowed for function methods. However, you could write it in an ordinary method and it would be fine.

method pick_minimum_formula(s: set<NNF_Formula>) returns (nnf: NNF_Formula)
requires s != {}
{
minimum_formula_Lemma(s); 
var phi :| phi in s && forall psi :: psi in s-{phi}  ==> (leq_NNF_Formula(phi,psi) && psi != phi);
nnf := phi;
}

You could also write it as a function, and it would be fine.

However, a function method does require that any let-such-that expression be unique. The reason is that a compiled let-such-that expression might be non-deterministic; on the other hand, any function must to be deterministic. But a function method must be a method whose output matches the result of the function! This cannot be guaranteed if the method would be nondeterministic.

user_30400980
Related