defining the force applied to a mass pulling a string

Stream: Natural sciences

[Bulhwi Cha]

In an example @Tyler Josephson ⚛️ gives in his talk, the force applied to a mass pulling a string is defined as follows:

def force (k x : ℝ) : ℝ := -k * x

I can define the voltage measured across a conductor in a similar way:

def voltage (I R : ℝ) : ℝ := I * R

From these definitions, we can prove the following theorem, which doesn't make sense:

import Mathlib.Data.Real.Basic

def force (k x : ℝ) : ℝ := -k * x
def voltage (I R : ℝ) : ℝ := I * R

theorem force_eq_neg_voltage (a b : ℝ) : force a b = -voltage a b := by
  rw [force, voltage, neg_mul]

I don't think it's a good idea to define the force applied to the mass as above.

[Notification Bot]

This topic was moved here from #Natural sciences > defining the force applied to a string by Bulhwi Cha.

[David⚛️]

@Bulhwi Cha what are your thoughts when it comes to defining the force that acts on a string?

[Colin Jones ⚛️]

The problem above is that this is technically true as -ab = -ab. I solution would be to include units, but I haven’t found a method to do that.

[Tyler Josephson ⚛️]

We’re working on a dimensional analysis paper - that would fix this one, but wouldn’t solve the problem in general. Maybe the dimensions all match up, but the entities still aren’t supposed to be equal.

[Tyler Josephson ⚛️]

On the other hand, what if you have Newton’s law of universal gravitation and Coulomb’s law (which have the same structure), and you want to leverage their similar structure? E.g. reusing derivations in the general Coulomb case to save you trouble in the gravity case?

[Patrick Massot]

You could have neutral lemmas about real numbers and then use them to easily prove lemmas about physical quantities. If it becomes too tedious then you can use meta-programming to do it.

[Bulhwi Cha]

David⚛️ said:

Bulhwi Cha what are your thoughts when it comes to defining the force that acts on a string?

Here's my Lean code. It's just an attempt, so I won't say this is a correct formalization. Besides, it'd be possible to give a concrete definition of Hooke.IsEnd.

Another weird formalization done by me

import Mathlib.Data.Real.Basic

class Motion (n : ℕ) (PhysicalObject : Type u) (SomeObject : Set PhysicalObject) (obj : SomeObject)
    where
  refTime : ℝ
  RefRegion : Set (Fin n → ℝ)
  motion (p₀ : RefRegion) (t : ℝ) : Fin n → ℝ
  Region (t : ℝ) := {p : Fin n → ℝ | ∃ (p₀ : RefRegion), p = motion p₀ t}
  region_eq (t : ℝ) : Region t = {p : Fin n → ℝ | ∃ (p₀ : RefRegion), p = motion p₀ t} := by
    rfl
  refRegion_eq : RefRegion = Region refTime

class Hooke (PhysicalObject : Type u) (HelicalSpring : Set PhysicalObject) (str : HelicalSpring)
    extends Motion 1 PhysicalObject HelicalSpring str where
  IsEnd : RefRegion → Prop
  has_exactly_two_end : ∃ (p₀ q₀ : RefRegion), p₀ ≠ q₀ ∧ IsEnd p₀ ∧ IsEnd q₀ ∧
    ∀ (r₀ : RefRegion), r₀ = p₀ ∨ r₀ = q₀
  only_one_end_fixed : ∃ (p₀ q₀ : RefRegion), p₀ ≠ q₀ ∧ IsEnd p₀ ∧ IsEnd q₀ ∧
    ∀ (t : ℝ), motion p₀ t = p₀
  fixedEnd : RefRegion
  fixedEnd_isEnd : IsEnd fixedEnd
  fixedEnd_fixed (t : ℝ) : motion fixedEnd t = fixedEnd
  freeEnd : RefRegion
  freeEnd_isEnd : IsEnd freeEnd
  fixedEnd_ne_freeEnd : fixedEnd ≠ freeEnd
  relaxedTime : ℝ
  relaxedFreeEnd : Region relaxedTime
  relaxedFreeEnd_eq : relaxedFreeEnd = motion freeEnd relaxedTime
  springConstant : ℝ
  springConstant_pos : 0 < springConstant
  restoringForce (t : ℝ) : Fin 1 → ℝ :=
    let k := springConstant;
    let x := motion freeEnd t 0;
    let x₀ := relaxedFreeEnd.val 0;
    fun _ ↦ -(k * (x - x₀))
  restoringForce_eq (t : ℝ) :
    let Fₛ := restoringForce t 0;
    let k := springConstant;
    let x := motion freeEnd t 0;
    let x₀ := relaxedFreeEnd.val 0;
    Fₛ = -(k * (x - x₀)) := by rfl

[Bulhwi Cha]

One thing is certain: it's not simple at all.

[Shreyas Srinivas]

A partial solution to this is to lift arithmetic operations to an inductive type with a constructor named after the quantity or unit you are dealing with and the measurement as a parameter to the constructor.

[Shreyas Srinivas]

It is partial because there is no notion of operations on constructors that automatically produces new constructors in the sense that you can't combine constructors for length and time into one for speed. Instead you have to define one separately. A trick to work around this could be : define an expression type on units and operate on those.

[Tyler Josephson ⚛️]

@Colin Jones ⚛️ and I put these examples together:

def force (k x : ℝ) : ℝ := -k * x
def force2 (m a : ℝ) : ℝ := m * a

-- Proof that's clearly wrong, but Lean says is okay
theorem force_eq_neg_ma (a b : ℝ) : force a b = -force2 a b := by
  dsimp [force, force2]
  ring

-- Better proof style - indeed, premises h1 and h2 imply the conjecture
theorem mass_spring_accel_force (kspring xposition mass accel: ℝ)
  (h1: F = force kspring xposition)
  (h2: F = force2 mass accel)
  :
  (-kspring*xposition = mass*accel) := by
  dsimp [force, force2] at h1 h2
  rw [← h1, ← h2]

The provability of the first proof shows this is still a bad setup, even with the units of force being consistent - partly, it's a problem because a and b in each function have different dimensions, but I think the issue goes deeper than that. It's unclear what the "system" is - sometimes, more than one force acts on an object, and there's no clear way to provide that information.

The second proof style is an answer to that - equality statements are used as propositions to form premises. You could easily imagine different theorems that invoke different systems. But overall, the setup isn't okay because the first proof is possible.

[Tyler Josephson ⚛️]

@Bulhwi Cha You may find this thesis interesting. There are other papers in the literature that explore ways to formalize physical objects, interactions, and events.

[Bulhwi Cha]

Tyler Josephson ⚛️ said:

The second proof style is an answer to that - equality statements are used as propositions to form premises. You could easily imagine different theorems that invoke different systems. But overall, the setup isn't okay because the first proof is possible.

I'm telling you that naming a real number variable as mass doesn't make it a mass. Do you think the variable banana : ℝ is a banana and also a real number?

[Bulhwi Cha]

Variable names are not important!

[Bulhwi Cha]

Tyler Josephson ⚛️ said:

Bulhwi Cha You may find this thesis interesting. There are other papers in the literature that explore ways to formalize physical objects, interactions, and events.

Variable body : Type.
Variable IB : body → Prop.
Variable Ph : body → Prop.
Variable W : body → body → v4 → Prop.

I want something else. Can anyone tell me how surfaces having the inside and the outside of them are defined in mathematics? In other words, how do you define surfaces like a sphere?

[Bulhwi Cha]

I'll study differential geometry in the future.

[Bulhwi Cha]

Bulhwi Cha said:

I'm telling you that naming a real number variable as mass doesn't make it a mass. Do you think the variable banana : ℝ is a banana and also a real number?

Variable names are not important!

See the following Lean code:

Naming something is irrelevant to defining it

import Mathlib.Data.Real.Basic

def force (k x : ℝ) : ℝ := -k * x
def force2 (m a : ℝ) : ℝ := m * a

theorem force_eq_neg_ma (a b : ℝ) : force a b = -force2 a b := by
  simp [force, force2]

theorem mass_spring_accel_force {F kspring xposition mass accel : ℝ}
    (h1 : F = force kspring xposition)
    (h2 : F = force2 mass accel) :
    -kspring * xposition = mass * accel := by
  unfold force at h1
  unfold force2 at h2
  rwa [← h1]

def voltage (I R : ℝ) : ℝ := I * R
def distance (v t : ℝ) : ℝ := v * t

theorem force_eq_neg_voltage (a b : ℝ) : force a b = -voltage a b := by
  rw [force, voltage, neg_mul]

theorem ma_eq_distance (a b : ℝ) : force2 a b = distance a b := rfl

theorem neg_voltage_eq_distance {V I R v t : ℝ}
    (h1 : V = -voltage I R)
    (h2 : V = distance v t) :
    -I * R = v * t := by
  rw [← force_eq_neg_voltage] at h1
  rw [← ma_eq_distance] at h2
  exact mass_spring_accel_force h1 h2

example {a b c d e : ℝ} (h1 : a = -b * c) (h2 : a = d * e) :
    mass_spring_accel_force h1 h2 = neg_voltage_eq_distance (neg_mul b c ▸ h1) h2 := rfl

[Tyler Josephson ⚛️]

Helpful response, I've been ruminating over it.

For a while, I've held this general perspective on formalization:
Lean checks proof syntax (which includes not just code syntax, but logic, too). Syntax can be checked independently from semantics. "All swans are white. X is a swan. Therefore X is white." is syntactically true - the form of the argument is valid, even if a premise within is false (indeed, black swans exist on rare occasions).

The art and science of modeling physical phenomena necessitate assumptions and approximations. I've been thinking: we ought to be able to structure almost every physical model as "Here's how it is defined. Therefore, these properties follow." Lean can ensure that the syntax is valid. But, it's on the scientist, the formalizer, to use their due diligence in establishing the definition of the system in the first place. In Mathlib, Lean doesn't have the machinery to say "you stated the theorem incorrectly" - it only checks proofs. I could rename PythagoreanTriple to FermatsLastTheorem and everything would be valid, but the new name would be nonsense.

So - I agree with your point, insofar as that naming something is irrelevant syntactically - but I think it's important, semantically. Names matter.

This is what makes me actually comfortable with the style of this proof:

theorem neg_voltage_eq_distance {V I R v t : ℝ}
    (h1 : V = -voltage I R)
    (h2 : V = distance v t) :
    -I * R = v * t := by
  rw [← force_eq_neg_voltage] at h1
  rw [← ma_eq_distance] at h2
  exact mass_spring_accel_force h1 h2

I can look at the hypotheses h1 and h2 and conclude "the problem is in the premises - the first premise is fine, but the second premise doesn't go with it." I can judge this and say "V is a bad variable name, I don't know what it means." I can also judge this and say "if R is resistance, it shouldn't be allowed to be negative." These criticisms are pushed right up to the front because I know the scientist is responsible for defining the system correctly in the first place. I am unbothered that the theorem is syntactically valid, and Lean gives no error, because I can place the error in the semantics, and the proof style makes explicit the variables, their types, and the assumptions involved.

This proof bothers me a lot more:

def force (k x : ℝ) : ℝ := -k * x
def force2 (m a : ℝ) : ℝ := m * a

theorem force_eq_neg_ma (a b : ℝ) : force a b = -force2 a b := by
  simp [force, force2]

There are no premises! That makes this proof "system independent" - but this shouldn't be true for all systems. It's extremely sneaky in that it is semantically true for some systems - but we need to remember that Lean is only checking syntax.

The "nonsense" proof you provide is a helpful contrast:

def voltage (I R : ℝ) : ℝ := I * R
def distance (v t : ℝ) : ℝ := v * t

theorem force_eq_neg_voltage (a b : ℝ) : force a b = -voltage a b := by
  rw [force, voltage, neg_mul]

This proof is also "system independent" - but it's easier to see that the semantics are nonsense. Making the functions very different makes it easier for me to come to terms with it, by thinking about the syntax of how functions work. This is also what the previous proof is doing, it's only proving a property that the functions have, it's not proving anything about propositions relating them.

Now, we could get fancier, and try harder to encode semantics into Lean, so Lean rejects bad semantics, too. I spend a lot of time thinking about that.

[Bulhwi Cha]

Tyler Josephson ⚛️ said:

So - I agree with your point, insofar as that naming something is irrelevant syntactically - but I think it's important, semantically. Names matter.

This is what makes me actually comfortable with the style of this proof:

theorem neg_voltage_eq_distance {V I R v t : ℝ}
    (h1 : V = -voltage I R)
    (h2 : V = distance v t) :
    -I * R = v * t := by
  rw [← force_eq_neg_voltage] at h1
  rw [← ma_eq_distance] at h2
  exact mass_spring_accel_force h1 h2

Are you also comfortable with the last example in my code?

example {a b c d e : ℝ} (h1 : a = -b * c) (h2 : a = d * e) :
    mass_spring_accel_force h1 h2 = neg_voltage_eq_distance (neg_mul b c ▸ h1) h2 := rfl

[Bulhwi Cha]

Tyler Josephson ⚛️ said:

Now, we could get fancier, and try harder to encode semantics into Lean, so Lean rejects bad semantics, too. I spend a lot of time thinking about that.

I agree with this point, but I also expect classical mechanics formalized in Lean will resemble Mathlib a lot. Perhaps it'll be a part of Mathlib.

[Bulhwi Cha]

If Lean tells me that two things are the same, they're the same in my perspective, at least when I'm formalizing a theory with Lean. I don't think there are two objects in Mathlib that mathematicians using Lean should view as different "semantically," even though they can prove these objects are equal to each other.

[Kevin Buzzard]

I think polynomials over the reals and finitely supported functions from the naturals to the reals might secretly be equal, even though they multiply in different ways

[Bulhwi Cha]

Secretly, right? Not explicitly.

[Kevin Buzzard]

docs#Polynomial

[Bulhwi Cha]

By the way, I'm planning to learn algebra with Mathlib after I prove all the remaining theorems on the TODO list in Std.Data.String.Lemmas. Right now, I don't understand that definition.

[Kevin Buzzard]

I just translated it for you above :-)

[Bulhwi Cha]

Then I guess they're not explicitly equal in Mathlib.

[Eric Wieser]

The multivariate version is

[Bulhwi Cha]

Can you show me the proof written in Lean?

[Bulhwi Cha]

Tyler Josephson ⚛️ said:

@Colin Jones :atom: and I put these examples together:

def force (k x : ℝ) : ℝ := -k * x
def force2 (m a : ℝ) : ℝ := m * a

We can show that force2 in the above code equals Real.mul, the multiplication of real numbers:

import Mathlib.Data.Real.Basic
import Batteries.Tactic.OpenPrivate

open Real
open private mul from Mathlib.Data.Real.Basic

def force (m a : ℝ) : ℝ := m * a
theorem force_eq_mul : force = mul := rfl

It's a category mistake to say that a force as a physical concept is the multiplication of real numbers.

[Kevin Buzzard]

As was pointed out above, there are well-established examples in mathlib where two different things are equal, for example multivariable polynomials are finitely-supported functions (but the equality does not commute with multiplication, which is defined differently on the two types):

import Mathlib.Algebra.MvPolynomial.Basic

variable (σ R : Type) [CommSemiring R]

example : MvPolynomial σ R = ((σ →₀ ℕ) →₀ R) := rfl

In the cardinality model of Lean, the naturals are equal to the integers. I don't think you can apply philosophy to type theory in this way.

[Bulhwi Cha]

Kevin Buzzard said:

As was pointed out above, there are well-established examples in mathlib where two different things are equal, for example multivariable polynomials are finitely-supported functions (but the equality does not commute with multiplication, which is defined differently on the two types):

I can't comment on this because I don't understand what you're saying. I know I should learn more mathematics. I'll do it in the future.

[Bulhwi Cha]

Kevin Buzzard said:

In the cardinality model of Lean, the naturals are equal to the integers.

I don't think this is a category mistake; it's just that a layperson's natural numbers are different from their integers. I believe most laypeople are happy with their conception of numbers.

[Shreyas Srinivas]

Mathlib's approach is great for mathematics, but I think people in the sciences need to be sure that one can't compare and combine entirely different quantities. Basic dimensionality analysis is necessary which is a kind of type safety check.

[Shreyas Srinivas]

My gut feeling says that what we call a "physical quantity" is a typeclass which resides in Sort 2 and has a type in Type 2 and which has a Group instance or even perhaps a Field instance or something similar to allow us to operate on them. Quantities are good-old types which are instances of this typeclass. They are defined inductively with constructors which represent units.

[Shreyas Srinivas]

But there are a few issues: Are we distinguishing quantities from units? Is that necessary? How do we define an inverse for units and link them to inverses of quantities? I mentioned Groups as an example of an algebraic structure on quantities/units but it might not be adequate. Perhaps a field is needed?

[Bulhwi Cha]

Bulhwi Cha said:

We can show that force2 in the above code equals Real.mul, the multiplication of real numbers:

We can also show that forces and voltages are the same:

def voltage (I R : ℝ) : ℝ := I * R
theorem voltage_eq_mul : voltage = mul := rfl

theorem force_eq_voltage : force = voltage := rfl

[Eric Wieser]

Bulhwi Cha said:

We can show that force2 in the above code equals Real.mul, the multiplication of real numbers:

open private mul from Mathlib.Data.Real.Basic

Just to note that you should not do this; Real.mul is an implementation detail, and open private is not appropriate here. The canonical name for multiplication is the (ugly) HMul.hMul, or the shorter (· * ·)

[Bulhwi Cha]

Okay, I'll use (· * ·) instead. HMul.hMul is indeed an ugly name.

import Mathlib.Data.Real.Basic

def force (m a : ℝ) : ℝ := m * a
theorem force_eq_mul : force = (· * ·) := rfl

def voltage (I R : ℝ) : ℝ := I * R
theorem voltage_eq_mul : voltage = (· * ·) := rfl

theorem force_eq_voltage : force = voltage := rfl

[Scott Carnahan]

Terry Tao's blog has a long discussion on mathematical treatments of "dimensionful" quantities. His "treatment 2" putting quantities of length, mass, etc. into distinct one-dimensional real (or NNReal) vector spaces, with units being linear maps to the reals, may be helpful for eliminating "garbage theorems".

[Tyler Josephson ⚛️]

Scott Carnahan said:

Terry Tao's blog has a long discussion on mathematical treatments of "dimensionful" quantities. His "treatment 2" putting quantities of length, mass, etc. into distinct one-dimensional real (or NNReal) vector spaces, with units being linear maps to the reals, may be helpful for eliminating "garbage theorems".

Two of my students are writing a paper on formalizing dimensional analysis in Lean! We definitely got some inspiration from this blog (though he does cover a lot more than we formalized). We define it, prove it's an abelian group, and prove it satisfies the Buckingham Pi Theorem. Hoping to wrap it up soon to share here.

[Tyler Josephson ⚛️]

Shreyas Srinivas said:

But there are a few issues: Are we distinguishing quantities from units? Is that necessary? How do we define an inverse for units and link them to inverses of quantities? I mentioned Groups as an example of an algebraic structure on quantities/units but it might not be adequate. Perhaps a field is needed?

Dimensions do work differently from units. (time + time) has to be treated differently than (seconds + hours). There's also a question of what form would be most useful for people in different contexts. Automatically convert seconds + hours to get a correct result, or flag it as a problem so the user makes sure the units match?

[Tomas Skrivan]

When playing around with units I got exactly into this problem. I'm curious, if you decide to automatically convert would seconds+hours result in seconds or in hours? I'm not sure if there is a good argument for one or the other.

[Shreyas Srinivas]

How do you produce inverse units for inverted quantities?

[Scott Carnahan]

As I understand it, inverted quantities live in the dual space. Say we have a one dimensional space of Lengths, and a unit of length (seen as a basis element of the dual space). Then the space of Inverse Lengths is the dual one dimensional space, and there is a unique basis element of the Length space that is dual to the chosen unit of length.

[Jason Rute]

@Tyler Josephson ⚛️ are your students familiar with something like Scala’s squants which in my opinion is a good take on units and dimension in functional programming. I think it uses inheritance (which Scala has but Lean doesn’t), but I think you could use type classes for the same effect.

[Jason Rute]

Of course, squants is for practical programming where you want the type system to prevent you from making a dimension analysis error, and not for formal science.

[Jason Rute]

In squants you can add hours and seconds, they are both type Time if I recall, but when you want to get a float in the end, then you specify the units to extract the float. (Would work the same with reals instead of floats.)

[Christian Tzurcanu]

I've contributed with my own take on Units, Measure:

https://github.com/ctzurcanu/lean-measure/blob/main/LeanMeasure.lean

some nice properties:

• you can add your own units
• you can derive new types of units by operations like * and /
• you can compare the nature of your units with those defined by SI
• has many derived SI units already: those with custom names for units
• has some constants defined. user can extend

I am a beginner to Lean and the math vocabulary it requires. I have tried defining Measure as monoid_algebra and failed.

Would love to learn more about how to do it. (Or what needs to change to make that even possible.)