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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
