CODEWITHSUNDEEP
theorem-provinginductiondafny
fulem
fulem

Reputation: 43

Different "sorted" predicates should be equivalent in Dafny

According to Automating Induction with an SMT Solver the following should work on Dafny:

ghost method AdjacentImpliesTransitive(s: seq<int>)
requires ∀ i • 1 ≤ i < |s| ==> s[i-1] ≤ s[i];
ensures ∀ i,j {:induction j} • 0 ≤ i < j < |s| ==> s[i] ≤ s[j];
{ }

But Dafny rejects it (at least in my desktop and in Dafny online). Maybe something changed.

Questions:

Q1. Why?

Q2. Is induction over j, or both i and j, really needed?. I think induction over the length of seq should be enough.

Anyway, im more interested in the following: i want to prove this by manual induction, for learning. On paper i think induction over the length of seq is enough. Now im trying to do this on Dafny:

lemma {:induction false} AdjacentImpliesTransitive(s: seq<int>)
   ensures forall i :: 0 <= i <= |s|-2 ==> s[i] <= s[i+1] ==> forall l, r :: 0 <= l < r <= |s|-1 ==> s[l] <= s[r]
   decreases s
{
   if |s| == 0
   { 
     //explicit calc proof, not neccesary
     calc {
        (forall i :: 0 <= i <= 0-2 ==> s[i] <= s[i+1]) ==> (forall l, r :: 0 <= l < r <= 0-1 ==> s[l] <= s[r]);
     ==
        (forall i :: false ==> s[i] <= s[i+1])  ==>  (forall l, r :: false ==> s[l] <= s[r]);
     ==
        true ==> true;
     == 
        true;
     }
   } 
   else if |s| == 1
   { 
     //trivial for dafny
   }  
   else {

     AdjacentImpliesTransitive(s[..|s|-1]);
     assert (forall i :: 0 <= i <= |s|-3 ==> s[i] <= s[i+1]) ==> (forall l, r :: 0 <= l < r <= |s|-2 ==> s[l] <= s[r]);
    //What??

   }
}

Im stuck on the last case. I dont know how to combine a calculational proof style (like the one in the base case) with the inductive hyp.

Maybe is the implication that is tricky. On paper (an "informal" proof), when we need to prove an implication p(n) ==> q(n) by induction, we had something like:

Hyp: p(k-1) ==> q(k-1)

Tesis: p(k) ==> q(k)

But then this is proving:

(p(k-1) ==> q(k-1) && p(k)) ==> q(k)

Q3. Does my approach make sense? How can we do this kind of induction in dafny?

Upvotes: 3

Views: 240

Answers (1)

Daniel Ricketts
Daniel Ricketts

Reputation: 447

I don't know the answer to Q1 and Q2. However, your induction proof goes through if you add assert s[|s|-2] <= s[|s|-1] in the induction case (you don't need the other assert). Here's the full proof:

lemma {:induction false} AdjacentImpliesTransitive(s: seq<int>)
   requires forall i :: 0 <= i <= |s|-2 ==> s[i] <= s[i+1]
   ensures forall l, r :: 0 <= l < r <= |s|-1 ==> s[l] <= s[r]
   decreases s
{
   if |s| == 0
   { 
     //explicit calc proof, not neccesary
     calc {
        (forall i :: 0 <= i <= 0-2 ==> s[i] <= s[i+1]) ==> (forall l, r :: 0 <= l < r <= 0-1 ==> s[l] <= s[r]);
     ==
        (forall i :: false ==> s[i] <= s[i+1])  ==>  (forall l, r :: false ==> s[l] <= s[r]);
     ==
        true ==> true;
     == 
        true;
     }
   } 
   else if |s| == 1
   { 
     //trivial for dafny
   }  
   else {

     AdjacentImpliesTransitive(s[..|s|-1]);
     assert s[|s|-2] <= s[|s|-1];

   }
}

For some reason, I had to separate your ensures clause into requires and ensures clauses. Otherwise, Dafny complained about undeclared identifier: _t#0#0. I have no idea what that means.

And, in case it's interesting, here's a shorter proof:

lemma AdjacentImpliesTransitive(s: seq<int>)
requires forall i | 1 <= i < |s| :: s[i-1] <= s[i]
ensures forall i,j | 0 <= i < j < |s| :: s[i] <= s[j]
decreases s
{
  if |s| < 2
  {
    assert forall i,j | 0 <= i < j < |s| :: s[i] <= s[j];
  } else {
    AdjacentImpliesTransitive(s[..|s|-1]);
    assert s[|s|-2] <= s[|s|-1];
  }
}

Upvotes: 1

Related Questions