Hi Ewa,
When reasoning about recursively defined functions,
you are probably going to have to do an induction,
and also expand out the definition(s) of the functions.
But in the example you have given, it may not even be
necessary to do that. I would separately prove
that function "i" is the identity function for numbers >= 1.
Then the proof just amounts to using the commutativity
of multiplication.
Konrad.
On Aug 31, 2008, at 6:14 PM, Ewa Rom wrote:
Hi all,
I'm trying to prove equality between 2 recursions (2 different way
of defining a factorial)
So far I have:
let i = define `i n = if n <= 1 then 1 else i ( n - 1 ) + 1`;;
let fac = define `fac n = if n <= 1 then 1 else fac ( n - 1 ) * i n`;;
let fact = define `fact n = if n <= 0 then 1 else n * fact(n - 1)`;;
Then I defined a goldstack:
g `!k. (( i k <= k) /\ 1 <= k) ==> (fac k = fact k)`;;
I used GEN_TAC and STRIP_TAC to get to subgoal: fac k = fact k
What should be the next step? Whatever I use gives me 'Exception:
Failure "linear_ineqs: no contradiction".'
I know the tutorial shows iformation on how to deal with Nonlinear
reasoning in Chapter 9.2. I tried the REAL_RING and it failed.
The other option is to use SOS_RULE, but it requires additional
module to be loaded. I want to check if there are any other
options for me to accomplish this that going with a module, or
maybe I'm just doing something wrong.
Thank you
Ewa Romanowicz
______________________________________________
Please visit http://www.EwaRomanowicz.com
----------------------------------------------------------------------
---
This SF.Net email is sponsored by the Moblin Your Move Developer's
challenge
Build the coolest Linux based applications with Moblin SDK & win
great prizes
Grand prize is a trip for two to an Open Source event anywhere in
the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
