scilib documentation

LeanChemicalTheories / thermodynamics.basic

The Thermodynamic System and Models #

We define a thermodynamic system to be over a general field, which we require to be an albelian group for multiplication. This class has five properties to describe the system, pressure, volume, temperature, amount of substance, and energy. Each property is defined as a function from the natural numbers to our field. This function represents the equillibrium states of the system.

We also define six properties of a thermodynamic system: isobaric, isochoric, isothermal, adiabatic, closed system, and isolated system. These take in a thermodynamic system and have the type Prop, so they can be thought of as assertation about the system.

We finally define an ideal gas, which extends the thermodynamic system by providing a model for the systems properties. So far, the ideal gas only defines the unviersal gas constant and the ideal gas law. Then we show how the boyles law follows form the ideal gas law and the assumption of isothermal and a closed system

To Do #

Add more parameters to the ideal gas model, including ideal models of energy.
Define more for energy: heat capacity as a function of temeperature, the first and second law of thermodynamics

structure thermo_system (α : Type u_1) [nontrivial α] :

Type u_1

pressure : α → ℝ
volume : α → ℝ
temperature : α → ℝ
substance_amount : α → ℝ
internal_energy : α → ℝ

Instances for thermo_system

thermo_system.has_sizeof_inst

def isobaric {α : Type u_1} [nontrivial α] (M : thermo_system α) :

Prop

Equations

isobaric M = ∀ (n m : α), M.pressure n = M.pressure m

def isochoric {α : Type u_1} [nontrivial α] (M : thermo_system α) :

Prop

Equations

isochoric M = ∀ (n m : α), M.volume n = M.volume m

def isothermal {α : Type u_1} [nontrivial α] (M : thermo_system α) :

Prop

Equations

isothermal M = ∀ (n m : α), M.temperature n = M.temperature m

def adiabatic {α : Type u_1} [nontrivial α] (M : thermo_system α) :

Prop

Equations

adiabatic M = ∀ (n m : α), M.internal_energy n = M.internal_energy m

def closed_system {α : Type u_1} [nontrivial α] (M : thermo_system α) :

Prop

Equations

closed_system M = ∀ (n m : α), M.substance_amount n = M.substance_amount m

def isolated_system {α : Type u_1} [nontrivial α] (M : thermo_system α) :

Prop

Equations

isolated_system M = (adiabatic M ∧ closed_system M)

Gas Laws #

def boyles_law {α : Type u_1} [nontrivial α] (M : thermo_system α) :

Prop

Equations

boyles_law M = ∃ (k : ℝ), ∀ (n : α), M.pressure n * M.volume n = k

def charles_law {α : Type u_1} [nontrivial α] (M : thermo_system α) :

Prop

Equations

charles_law M = ∃ (k : ℝ), ∀ (n : α), M.volume n = k * M.temperature n

def avogadros_law {α : Type u_1} [nontrivial α] (M : thermo_system α) :

Prop

Equations

avogadros_law M = ∃ (k : ℝ), ∀ (n : α), M.volume n = k * M.substance_amount n

theorem boyles_law_relation {α : Type u_1} [nontrivial α] (M : thermo_system α) :

boyles_law M → ∀ (n m : α), M.pressure n * M.volume n = M.pressure m * M.volume m

theorem boyles_law_relation' {α : Type u_1} [nontrivial α] (M : thermo_system α) :

(∀ (n m : α), M.pressure n * M.volume n = M.pressure m * M.volume m) → boyles_law M

theorem charles_law_relation {α : Type u_1} [nontrivial α] (M : thermo_system α) :

charles_law M → ∀ (n m : α), M.volume n * M.temperature m = M.volume m * M.temperature n

theorem charles_law_relation' {α : Type u_1} [nontrivial α] (M : thermo_system α) (hT : ∀ (n : α), M.temperature n ≠ 0) :

(∀ (n m : α), M.volume n * M.temperature m = M.volume m * M.temperature n) → charles_law M

theorem avogadros_law_relation {α : Type u_1} [nontrivial α] (M : thermo_system α) :

avogadros_law M → ∀ (n m : α), M.volume n * M.substance_amount m = M.volume m * M.substance_amount n

theorem avogadros_law_relation' {α : Type u_1} [nontrivial α] (M : thermo_system α) (hN : ∀ (n : α), M.substance_amount n ≠ 0) :

(∀ (n m : α), M.volume n * M.substance_amount m = M.volume m * M.substance_amount n) → avogadros_law M

System models #

structure ideal_gas (α : Type u_2) [nontrivial α] :

Type u_2

to_thermo_system : thermo_system α
R : ℝ
ideal_gas_law : ∀ (n : α), self.to_thermo_system.pressure n * self.to_thermo_system.volume n = self.to_thermo_system.substance_amount n * self.R * self.to_thermo_system.temperature n

Instances for ideal_gas

ideal_gas.has_sizeof_inst

Properties about the ideal gas law #

theorem ideal_gas_law_relation {α : Type u_1} [nontrivial α] (M : ideal_gas α) (n m : α) :

M.to_thermo_system.pressure n * M.to_thermo_system.volume n * (M.to_thermo_system.substance_amount m * M.to_thermo_system.temperature m) = M.to_thermo_system.pressure m * M.to_thermo_system.volume m * (M.to_thermo_system.substance_amount n * M.to_thermo_system.temperature n)

theorem boyles_from_ideal_gas {α : Type u_1} [nontrivial α] (M : ideal_gas α) (iso1 : isothermal M.to_thermo_system) (iso2 : closed_system M.to_thermo_system) (hT : ∀ (n : α), M.to_thermo_system.temperature n ≠ 0) (hn : ∀ (n : α), M.to_thermo_system.substance_amount n ≠ 0) :

boyles_law M.to_thermo_system

theorem charles_from_ideal_gas {α : Type u_1} [nontrivial α] (M : ideal_gas α) (iso1 : isobaric M.to_thermo_system) (iso2 : closed_system M.to_thermo_system) (hT : ∀ (n : α), M.to_thermo_system.temperature n ≠ 0) (hn : ∀ (n : α), M.to_thermo_system.substance_amount n ≠ 0) (hP : ∀ (n : α), M.to_thermo_system.pressure n ≠ 0) :

charles_law M.to_thermo_system

theorem avogadros_from_ideal_gas {α : Type u_1} [nontrivial α] (M : ideal_gas α) (iso1 : isothermal M.to_thermo_system) (iso2 : isobaric M.to_thermo_system) (hT : ∀ (n : α), M.to_thermo_system.temperature n ≠ 0) (hn : ∀ (n : α), M.to_thermo_system.substance_amount n ≠ 0) (hP : ∀ (n : α), M.to_thermo_system.pressure n ≠ 0) :

avogadros_law M.to_thermo_system

System Energy #

def enthalpy {α : Type u_1} [nontrivial α] (M : thermo_system α) :

α → ℝ

Equations

enthalpy M = M.internal_energy + M.pressure * M.volume

def change (f : ℕ → ℝ) (n : ℕ) :

Equations

Δ f = λ (n : ℕ), f (n + 1) - f n