From: Ken R. <ke...@cs...> - 2009-10-06 10:41:48
|
Dear Carine and Laurent. Thank you both for the explanation of what looked like a mystery for me. Now there is a second mystery, as you refer to Rodin 1.1. But I believe I am running under 1.0 having given 1.1. away for the moment as I experienced some other problems. Certainly the "about Rodin" says 1.0. What could be the explanation of this? Seems like I'm somehow running the newer release of the provers? Cheers, Ken On 06/10/2009, at 19:33 PM, Laurent Voisin wrote: > Hi Ken, > > here is a little expansion of Carine's answer. > > Le 6 oct. 09 à 05:32, Ken Robinson a écrit : > >> Here's the problematic case: >> > <pastedGraphic.png> >> >> >> I enter min(liftschedule(lift)) into the yellow box and click the >> red existential button. >> >> Instead of the normal behaviour, of simply running the >> instantiation, it gives me a menu >> > <pastedGraphic.png> >> >> >> >> A bit strange, but I choose instantiation. > > This is a new feature of Rodin 1.1: when you have to prove the > existence of a lower (resp. upper) bound, the prover now proposes > to use an argument of finiteness (which is the purpose of the second > tactic displayed). In practice, this means that when you have a > goal of form: > > ∃b·∀x·x∈E⇒b≤x > > if you select the second tactic, you will get the new goal > > finite(E) > > which is a sufficient condition for the existence of the lower > bound. Given the supposed intent of your model, this might be very > helpful (unless you don't have any ground floor ;-). You would need > to add the invariant > > !lift. lift : dom(liftschedule) => finite(liftschedule(lift)) > >> The provers whirl for a moment and then "Tactic applied >> successfully, but ... >> >> the existential goal remains (uninstantiated of course) > > This is because, when you introduce an expression to the prover, you > have to show that it is well-defined before the prover accepts to > use it (this might have not been fully implemented in previous > version of the platform). > > But, here, suggesting min(liftschedule(lift)) produces a WD sub-goal > which is exactly the same subgoal. You tried to use a circular > argument to discharge this WD sub-goal and the prover just reflects > that. > > Laurent. > |