Sub-variables

Stream: Is there code for X?

[Max Bobbin]

Hi, I'm currently learning Lean for applications in Chemical Engineering, and my group was wondering if it was possible to define only what I can describe as a "sub-variable." This is best described with an example. For instance, we want to define a variable, P for pressure, and then also have a P1 and P2 for the pressure of state 1 and state 2. I know in the theorem statement, we could define P, P1, and P2 all as real numbers each as a separate variable, but I was wondering if it's possible to define these sub-variables? One reason is, we have something called Boyle's law which states for an isothermal system, P*V = k where P is pressure, V is volume, and k is a constant. So we can show that for a system at two states 1 and 2, P1V1 = P2V2 since k is a constant. I was thinking this would involve some kind of existential and stuff, but I wanted to double-check this was something that was possible in Lean.

[Adam Topaz]

One approach would be, for example to define a structure modeling your state. In your example, the structure could have two fields, P and V, both reals, along with a proof that P * V = k where k is the constant that does not depend on the given state.

[Eric Wieser]

Another option would be P V : fin n → ℝ, where n is your number of states, and have h : ∃ k, ∀ s, P s * V s = k or equivalently h : ∃ k, P * V = function.const k