Simple use of lemmas for preconditions (feature request?)

[BLepers]

Imagine I have the following lemma:

def lemma(l:List[A], e1:A, e2:A) = {
   e1.prop == e2.prop ==> cond(l, e1) == cond(l, e2)
}.holds;

and the following code:

case class B(l:List[A], e:A) {
   require(cond(l, e))
}

def f(b:B):B = {
   B(
        l,
        A(... with same .prop as b.e ...)
    ) // leon cannot prove that B can be built without the lemma
}

What is the best way to make sure that Leon can prove that the new B can be built ? (The precondition for creating B holds because of the lemma.)

if(lemma(l, b.e, A(...))) B(...) else error[]("...") // works but messes up postconditions

check(lemma(...)) //ok
B(...) // ko, lemma has been forgotten

I was wondering if it would be possible to write something such as:

B(...) because lemma(...) // or any better syntax

(Or have Leon remember what it "check(...)'ed" before.)

Sorry if a method already exists in Leon to do that or if the issue has already been raised! :)

[MikaelMayer]

B(...) because lemma(...) as you say can be represented as:

assert(lemma(...))
B(...)

But this would be nice to have the because statement. Would you think it would be clearer?

[BLepers]

assert would be a nice solution, but it doesn't seem to work on my code :(

Scheduler.txt

   def insertBack(c: Core, t: Task): Core = {
      require(!contains(c.tasks, t))
      if(containsEquivLemma(c.tasks, t, tick(t))) {
         Core(c.id, sortedIns(c.tasks, tick(t)), None[Task]())
      } else {
         error[Core]("Tick changes task id\n");
      }
   }

   def insertBack2(c: Core, t: Task): Core = {
      require(!contains(c.tasks, t))
      assert(containsEquivLemma(c.tasks, t, tick(t)));
      Core(c.id, sortedIns(c.tasks, tick(t)), None[Task]())
   }

   leon Scheduler.scala --functions=insertBack,insertBack2
   // verifies insertBack but does not finish (precondition of sortedIns) on insertBack2

Am I missing something?

[MikaelMayer]

@regb @colder @samarion @manoskouk Me too I want to use "assert" rather than if/else error. Anybody knows why it is not working? How did you implement assert?

[samarion]

@manoskouk disabled it (see TransformerWithPC). It's tagged with "to discuss", any reason we wouldn't want these?