On Apr 4, 2008, at 9:51 AM, Augusto Ribeiro wrote:
> Dear All,
>
> Sorry for the extensive background if you prefer please go straight
> to the PROBLEM that is a bit below in the mail.
>
> ------------> BACKGROUND <------------
>
> I'm trying to use HOL to prove termination of recursive functions
> with preconditions in VDM. What I plan to do is generate the
> termination conditions myself by inspecting the VDM source file and
> then trying to prove them in HOL. I know HOL doesn't support sub-
> typing so what I'm doing at the moment is for example:
>
> f(x) = if (x=3) then 3 else f(x-1)
> precondition: x >= 3
One trick for sneaking in subtyping is to define
the function as
f(x) =
if x >= 3 then
if x = 3 then 3
else f(x-1)
else ARB
With that, termination should be proved automatically
by Define. You can subsequently prove
|- x >= 3 ==> (f x = if x=3 then 3 else f(x-1))
>
>
> What is inserted into HOL is a goal like this:
>
> - g `?R. WF R /\ ( ~(x=3) /\ (x>=3) ==> R (x-1) x )`;
>
> The thing if I try to prove this using the command:
>
> e (WF_REL_TAC `measure (\x.x)`)
>
> I am successful because '<' is well founded and the rest of the
> equation is true. But the proof is unsound because inserting the
> '(x>=3)' assumption makes this statement "~(x=3) /\ (x>=3) ==> R
> (x-1) x" true. This could be solved if I use (\x.x-3) instead of
> '(\x.x)'. But what I'm trying to do is for use of general use so I
> don't want people to incur in the risk of making unsound proofs.
There is no danger of unsoundness using WF_REL_TAC, just
of providing a witness relation that doesn't actually lead to
provable termination conditions.
Konrad.
>
> ------------> PROBLEM <------------
>
> So what I tried to follow other approach and define the 'measure'
> relation myself, like this:
>
> - g `?R. WF R /\ ( ~(x=3) /\ (x>=3) ==> R (x-1) x )`;
> - val measure2 = Define `measure2 f x y = if (x>= 3 /\ y >= 3) then f
> x < f y else F`;
> - e (WF_REL_TAC `measure2 (\x.x)`)
> - e (RW_TAC arith_ss [measure2])
>
> And using this tactic all goes alright until I get stuck with:
>> val it =
> WF (measure2 (\x. x))
>
> : goalstack
> Although the relation is well founded because it's just a restriction
> of the Naturals. I couldn't prove it until now. Is there a tactic to
> prove this or at least to do some simplification. I couldn't do
> nothing to continue this proof yet. Or maybe there is other ways to
> do this. Thank you for your time and help.
>
> Cheers,
> Augusto Silva
>
>
>
> ----------------------------------------------------------------------
> ---
> This SF.net email is sponsored by the 2008 JavaOne(SM) Conference
> Register now and save $200. Hurry, offer ends at 11:59 p.m.,
> Monday, April 7! Use priority code J8TLD2.
> http://ad.doubleclick.net/clk;198757673;13503038;p?http://
> java.sun.com/javaone
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
-------------------------------------------------------------------------
This SF.net email is sponsored by the 2008 JavaOne(SM) Conference
Register now and save $200. Hurry, offer ends at 11:59 p.m.,
Monday, April 7! Use priority code J8TLD2.
http://ad.doubleclick.net/clk;198757673;13503038;p?http://java.sun.com/javaone
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
