Hi, does anyone notice that, the 3 basic transcendental functions (sin, cos, exp) in HOL4 are only correctly defined on positive inputs?
I say this because all these definitions are based on suminf which gives desired results only for all positive summations: [exp] Definition ⊢ ∀x. exp x = suminf (λn. (λn. (&FACT n)⁻¹) n * x pow n) [sin] Definition ⊢ ∀x. sin x = suminf (λn. (λn. if EVEN n then 0 else -1 pow ((n − 1) DIV 2) / &FACT n) n * x pow n) [cos] Definition ⊢ ∀x. cos x = suminf (λn. (λn. if EVEN n then -1 pow (n DIV 2) / &FACT n else 0) n * x pow n) where suminf is the sup of partial sums of first n items: > suminf; val it = ⊢ ∀f. suminf f = @s. f sums s: thm > sums; val it = ⊢ ∀f s. f sums s ⇔ (λn. sum (0,n) f) ⟶ s: thm by definition, exp x = 1 + x + x^2/2! + x^3/3! + ..., but if x < 0, the summation will be alternatively positive and negative, the "sup" should be the first item, i.e. with some efforts one should be able to prove: !x. x < 0 ==> (exp(x) = 1) --Chun ------------- below are some background story ---------------- yesterday I started to need a small result of exponential function (exp), namely: |- !x. &0 <= x ==> (&1 - x) <= exp (-x) I noticed that, HOL Light has a theorem (REAL_EXP_LE_X) in its "Multivariate/transcendental.ml" saying: |- !x. &1 + x <= exp(x) this would be one I need (by instantiating `x` to `-x`) but in HOL4 I only see a restricted version (EXP_LE_X) with antecedents `0 <= x` in "src/real/transcScript.sml": |- !x. &0 <= x ==> (&1 + x) <= exp(x) Obviously this theorem (and the whole transcTheory) was ported from HOL Light's "Library/transc.ml" (REAL_EXP_LE_X), because all definitions and proofs are essentially identical. I can't easily port REAL_EXP_LE_X from HOL Light's "Multivariate/transcendental.ml", because the "exp" there was defined as the real part of complex-valued "exp". So I started to prove the full version of EXP_LE_X by myself. My idea was to use the existing EXP_LE_X for the case "0 <= x", and the case `x < -1` is trivial, because `1 + x < 0` and `0 <= exp(x)`. Thus I only need to prove for the case `-1 <= x < 0`: 0 ≤ f x ------------------------------------ 0. x < 0 1. -1 < x 2. Abbrev (f = (λx. exp x − (1 + x))) 3. Abbrev (g = (λx. exp x − 1)) 4. ∀x. (f diffl g x) x 5. ∀x. x ≤ 0 ⇒ g x ≤ 0 6. f 0 = 0 : proof so far so good, I have proved that, the differentiation 'g' of f(x) = exp(x) - (1+x) is negative in [-1,0], and f(0) = 0. Then I was going to look into my calculus books to find proofs that f() is mono-decreasing in [-1,0] to finish the entire proof. Then, I suddenly found the sad news, that HOL4's "exp" function is not correctly defined on negative inputs.
signature.asc
Description: OpenPGP digital signature
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info