English measure phrases

The English nouns that quantize a mass noun in a pseudo-partitive (three grams of salt, three glasses of water, three grains of rice) are measure terms, which name a unit quantity of a dimension, and the container nouns and atomizers of Scontras's classification. A measure term carries the size of its unit in the dimension's reference unit, so that a kilogram is a thousand grams (kilogram_quantity).

Implementation notes

• A unit's size is a convention, and the conventions are exact rationals: the SI prefixes are powers of ten, and the pound and the mile are exact decimals of the kilogram and the meter. The fragment stores them in ℚ, and a measure term denotes a quantity with real magnitude.

References

• [Sco14]
• [BS22]

structure English.MeasurePhrases.MeasureTerm : Type

A measure term, a noun naming a unit quantity of a dimension.

• form : String
• formPlural : String
• symbol : String

  The unit's symbol in the quantity calculus (g, mL, km).

• dimension : Degree.Dimension
• magnitude : ℚ

  The size of the unit in the dimension's reference unit (gram, milliliter, meter, second); a kilogram is 1000 grams and a mile 1609.344 meters.

• magnitude_pos : 0 < self.magnitude

@[instance_reducible]

instance English.MeasurePhrases.instReprMeasureTerm : Repr MeasureTerm

Equations

• English.MeasurePhrases.instReprMeasureTerm = { reprPrec := English.MeasurePhrases.instReprMeasureTerm.repr }

def English.MeasurePhrases.instReprMeasureTerm.repr : MeasureTerm → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def English.MeasurePhrases.MeasureTerm.quantity (t : MeasureTerm) : Degree.Quantity ℝ

The unit quantity a measure term denotes, its size in the reference unit times the unit quantity of its dimension.

Equations

• t.quantity = (↑t.magnitude, Degree.QuantityDimension.of t.dimension)

@[simp]

theorem English.MeasurePhrases.MeasureTerm.quantity_fst (t : MeasureTerm) : t.quantity.1 = ↑t.magnitude

@[simp]

theorem English.MeasurePhrases.MeasureTerm.quantity_snd (t : MeasureTerm) : t.quantity.2 = Degree.QuantityDimension.of t.dimension

theorem English.MeasurePhrases.MeasureTerm.cast_magnitude_pos (t : MeasureTerm) : 0 < ↑t.magnitude

A unit has positive size.

theorem English.MeasurePhrases.MeasureTerm.quantity_eq_pure_mul_iff {t t' : MeasureTerm} {k : ℝ} : t'.quantity = Degree.Quantity.pure k * t.quantity ↔ ↑t'.magnitude = k * ↑t.magnitude ∧ t'.dimension = t.dimension

One unit is k of another when its size is k times the other's in their common dimension.

def English.MeasurePhrases.gram : MeasureTerm

gram.

Equations

• English.MeasurePhrases.gram = { form := "gram", formPlural := "grams", symbol := "g", dimension := Degree.Dimension.mass, magnitude_pos := English.MeasurePhrases.gram._proof_2 }

def English.MeasurePhrases.kilogram : MeasureTerm

kilogram.

Equations

• One or more equations did not get rendered due to their size.

def English.MeasurePhrases.kilo : MeasureTerm

kilo.

Equations

• One or more equations did not get rendered due to their size.

def English.MeasurePhrases.pound : MeasureTerm

pound.

Equations

• One or more equations did not get rendered due to their size.

def English.MeasurePhrases.milliliter : MeasureTerm

milliliter.

Equations

• One or more equations did not get rendered due to their size.

def English.MeasurePhrases.liter : MeasureTerm

liter.

Equations

• One or more equations did not get rendered due to their size.

def English.MeasurePhrases.mile : MeasureTerm

mile.

Equations

• One or more equations did not get rendered due to their size.

def English.MeasurePhrases.kilometer : MeasureTerm

kilometer.

Equations

• One or more equations did not get rendered due to their size.

def English.MeasurePhrases.meter : MeasureTerm

meter.

Equations

• English.MeasurePhrases.meter = { form := "meter", formPlural := "meters", symbol := "m", dimension := Degree.Dimension.distance, magnitude_pos := English.MeasurePhrases.gram._proof_2 }

def English.MeasurePhrases.hour : MeasureTerm

hour.

Equations

• One or more equations did not get rendered due to their size.

def English.MeasurePhrases.second_ : MeasureTerm

second.

Equations

• English.MeasurePhrases.second_ = { form := "second", formPlural := "seconds", symbol := "s", dimension := Degree.Dimension.time, magnitude_pos := English.MeasurePhrases.gram._proof_2 }

theorem English.MeasurePhrases.kilogram_quantity : kilogram.quantity = Degree.Quantity.pure 1000 * gram.quantity

A kilogram is a thousand grams.

theorem English.MeasurePhrases.liter_quantity : liter.quantity = Degree.Quantity.pure 1000 * milliliter.quantity

A liter is a thousand milliliters.

def English.MeasurePhrases.allMeasureTerms : List MeasureTerm

The measure terms.

Equations

• One or more equations did not get rendered due to their size.

def English.MeasurePhrases.measureTerm? (s : String) : Option MeasureTerm

The measure term with singular or plural form s.

Equations

• English.MeasurePhrases.measureTerm? s = List.find? (fun (t : English.MeasurePhrases.MeasureTerm) => decide (t.form = s ∨ t.formPlural = s)) English.MeasurePhrases.allMeasureTerms

structure English.MeasurePhrases.QuantizingNoun : Type

A quantizing noun turns a mass term into a countable expression, as a measure term, a container noun or an atomizer.

• form : String
• formPlural : String
• nounClass : Degree.QuantizingNounClass
• dimension : Option Degree.Dimension

  The dimension a measure term names, or that a container noun measures on its measure reading; atomizers name no measure function.

def English.MeasurePhrases.instReprQuantizingNoun.repr : QuantizingNoun → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance English.MeasurePhrases.instReprQuantizingNoun : Repr QuantizingNoun

Equations

• English.MeasurePhrases.instReprQuantizingNoun = { reprPrec := English.MeasurePhrases.instReprQuantizingNoun.repr }

def English.MeasurePhrases.instBEqQuantizingNoun.beq : QuantizingNoun → QuantizingNoun → Bool

Equations

• One or more equations did not get rendered due to their size.
• English.MeasurePhrases.instBEqQuantizingNoun.beq x✝¹ x✝ = false

@[instance_reducible]

instance English.MeasurePhrases.instBEqQuantizingNoun : BEq QuantizingNoun

Equations

• English.MeasurePhrases.instBEqQuantizingNoun = { beq := English.MeasurePhrases.instBEqQuantizingNoun.beq }

def English.MeasurePhrases.MeasureTerm.toQuantizingNoun (t : MeasureTerm) : QuantizingNoun

A measure term as a quantizing noun.

Equations

• t.toQuantizingNoun = { form := t.form, formPlural := t.formPlural, nounClass := Degree.QuantizingNounClass.measureTerm, dimension := some t.dimension }

@[instance_reducible]

instance English.MeasurePhrases.instCoeMeasureTermQuantizingNoun : Coe MeasureTerm QuantizingNoun

Equations

• English.MeasurePhrases.instCoeMeasureTermQuantizingNoun = { coe := English.MeasurePhrases.MeasureTerm.toQuantizingNoun }

def English.MeasurePhrases.glass : QuantizingNoun

glass.

Equations

• English.MeasurePhrases.glass = { form := "glass", formPlural := "glasses", nounClass := Degree.QuantizingNounClass.containerNoun, dimension := some Degree.Dimension.volume }

def English.MeasurePhrases.box : QuantizingNoun

box.

Equations

• English.MeasurePhrases.box = { form := "box", formPlural := "boxes", nounClass := Degree.QuantizingNounClass.containerNoun, dimension := some Degree.Dimension.volume }

def English.MeasurePhrases.cup : QuantizingNoun

cup.

Equations

• English.MeasurePhrases.cup = { form := "cup", formPlural := "cups", nounClass := Degree.QuantizingNounClass.containerNoun, dimension := some Degree.Dimension.volume }

def English.MeasurePhrases.bag : QuantizingNoun

bag.

Equations

• English.MeasurePhrases.bag = { form := "bag", formPlural := "bags", nounClass := Degree.QuantizingNounClass.containerNoun, dimension := some Degree.Dimension.volume }

def English.MeasurePhrases.bottle : QuantizingNoun

bottle.

Equations

• English.MeasurePhrases.bottle = { form := "bottle", formPlural := "bottles", nounClass := Degree.QuantizingNounClass.containerNoun, dimension := some Degree.Dimension.volume }

def English.MeasurePhrases.grain : QuantizingNoun

grain.

Equations

• English.MeasurePhrases.grain = { form := "grain", formPlural := "grains", nounClass := Degree.QuantizingNounClass.atomizer }

def English.MeasurePhrases.piece : QuantizingNoun

piece.

Equations

• English.MeasurePhrases.piece = { form := "piece", formPlural := "pieces", nounClass := Degree.QuantizingNounClass.atomizer }

def English.MeasurePhrases.drop : QuantizingNoun

drop.

Equations

• English.MeasurePhrases.drop = { form := "drop", formPlural := "drops", nounClass := Degree.QuantizingNounClass.atomizer }

def English.MeasurePhrases.slice : QuantizingNoun

slice.

Equations

• English.MeasurePhrases.slice = { form := "slice", formPlural := "slices", nounClass := Degree.QuantizingNounClass.atomizer }

def English.MeasurePhrases.chunk : QuantizingNoun

chunk.

Equations

• English.MeasurePhrases.chunk = { form := "chunk", formPlural := "chunks", nounClass := Degree.QuantizingNounClass.atomizer }

def English.MeasurePhrases.allQuantizingNouns : List QuantizingNoun

The quantizing nouns.

Equations

• One or more equations did not get rendered due to their size.