Proving linearity of Fourier Transform

[marta zhango]

Although TLAPS cannot handle reals, I would like to try using TLA

as a hierarchical proof.  Have done as follows

Constant t, omega, a, b

Constant h, f, g

Constant h \in [Real -> Real]

Constant f \in [Real -> Real]

Constant g \in [Real -> Real]

Constant F \in [Real -> Real]

<1>1. F(h(t)) == Integral ( h(t) * exp( -i * omega * t) , t)

<1>2. h(t) == a * f(t) + b * g(t)

Prove:  F(h(t)) = a * F(f(t)) + b * F (g(t))

Proof:

<1>3. F(h(t)) =  Integral ( (a * f(t) + b * g(t) ) * exp( -i * omega * t) , t)  [by <1>2, <1>1 ]

                      =  Integral ( (a * f(t) * exp( -i * omega * t))   + (b * g(t) * exp( -i * omega * t)) , t)

                      =   a * Integral ( f(t) * exp( -i * omega * t) , t ) 

                                 + b * Integral ( g(t) * exp( -i * omega * t) , t)

                      = a * F(f(t)) + b * F (g(t))     [ by <1>1 ]

<1>4 Q.E.D.

Would be grateful if other can comment and point out improvements

[Stephan Merz]

A couple of comments on the formal development and the proof:

- The operator Integral is not defined here, and it is not clear what is assumed about it. Intuitively, I would assume that it acts as a binder on the argument "t" and should really be of type [ [Real -> Real] -> Real ]. For example, the right-hand side of <1>1 would rather be something along the lines of "Integral (LAMBDA t : h(t) * exp(…))".

- I am assuming that the constants declared without type are expected to be real numbers, e.g. omega \in Real

- Steps <1>1 and <1>2 appear to be definitions (in particular you use "=="), not assertions of equations that require proof. But the symbols F and h that appear on the left-hand side have been declared. In particular, it is not clear if F is defined for all reals or only for those that are in the image of the function h. (And as said above, it should really be a definition of the form F(h(_)) == … because t is a bound variable.)

- In <1>3, no justifications are given for the second and third transformations. The second one uses the standard distributivity law whereas the third one relies on additivity of integrals, which appears to be assumed. In a more complete development, one would expect to see a definition of the Integral operator and proofs of laws about that operator. The fourth equality, supposedly justified by definition <1>1, substitutes the functions f and g for h used in <1>1. This shows that you really need <1>1 to assert the equality for all functions of type [Real -> Real], not just for the function h.

More generally, I do not really understand the added value of using a TLA-like notation for such proofs. TLA+ is mainly intended for describing and verifying algorithms. As others have already pointed out, its support tools will not allow you to check your developments, so there is no way for you to help you with getting your notation right. For purely mathematical developments, I would rather advise to use a mainstream proof assistant such as Isabelle, Lean or Rocq (formerly known as Coq) that come with extensive mathematical libraries. Also, Isabelle’s Isar proof language is not too dissimilar from Lamport’s hierarchical proof notation.

Regards,

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/f77e5ebc-ec7e-47ce-8f5c-6d8d090a335en%40googlegroups.com.

[marta zhango]

Could you show how the improvements you describe would look like when

specified as you suggest ?

Although TLA+ is primarily designed for specifying and verifying algorithms, I am

exploring its potential for structuring and organizing mathematical correctness proofs,

leveraging the hierarchically structured proof methodology introduced by Leslie Lamport.

To initiate this process, I have begun with straightforward Fourier transform formulations,

using them as a foundation to understand the practicalities of constructing such proofs.

My ultimate aim is to extend these methods to develop rigorous correctness proofs for

wavelet transforms, particularly in applications related to oceanography.

This discussion serves as an opportunity to refine the key concepts and approaches necessary

for the systematic development of mathematical correctness proofs in this context.

[marta zhango]

Stephan,

About the comment

Steps <1>1 and <1>2 appear to be definitions (in particular you use "=="), not assertions of

equations that require proof.

What would you suggest?  Placing them somewhere else, or use a different construct?