Re: [tlaplus] Proving linearity of Fourier Transform

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

On 21 Nov 2024, at 23:52, marta zhango <martazhango@xxxxxxxxx> wrote:

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

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/f77e5ebc-ec7e-47ce-8f5c-6d8d090a335en%40googlegroups.com.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/72EDC4C3-DE5C-4D54-B789-D027AC0A2C5C%40gmail.com.