Help with simple proof

Stream: new members

[wuyoli]

hi, I'm stuck trying to prove something.
This is my code.
I want to prove Isomorphism of my own Quantity type and Batteries.Vector Rat 7.
I'm stuck on the proof of VectorQuantityRoundtrip.

[Martin Dvořák]

simp [toVector, fromVector, h]

[Derek Rhodes]

@wuyoli, I was tinkering with your code last night, but couldn't find a proof without cases repetition. Did simp [toVector, fromVector, h] resolve your issue? I couldn't find h. I was thinking that maybe Martin meant p, but that didn't work.

[Cob Cobson]

for sufficiently small n, you can match on each case of Fin n directly:

import Mathlib

structure Quantity (α) [Field α] where
 (time
  length
  mass
  current
  temperature
  luminousIntensity
  amount : α)

example [Field α] : Quantity α ≃ Mathlib.Vector α 7 where
  toFun x := ⟨[x.time, x.length, x.mass, x.current, x.temperature, x.luminousIntensity, x.amount], rfl⟩
  invFun x := ⟨x[0], x[1], x[2], x[3], x[4], x[5], x[6]⟩
  left_inv _ := rfl
  right_inv x := Mathlib.Vector.ext fun
  | 0 | 1 | 2 | 3 | 4 | 5 | 6 => rfl

[wuyoli]

@Derek Rhodes I was wondering about the h too.
@Cob Cobson why are you doing this with example instead of of theorem?

[Karthik 🦋]

Is it possible to rewrite i as a Fin 7 (using simp_rw?) and use fin_cases <;> refl to finish this?
I wasn't able to get the rewrite done.

theorem VectorQuantityRoundtrip (v: Batteries.Vector Rat 7) : toVector (fromVector v) = v := by
  ext i p
  simp [toVector, fromVector]

  let j : Fin 7 := Fin.mk i p
  have hj : i = j.val := rfl
  have hi := (Fin.val_cast_of_lt p)
  -- both the rewrites fail even with simp_rw
  -- rw [hj]
  -- rw [←hi]

[Timo Carlin-Burns]

It looks like you forgot to include the theorem statement?

[Karthik 🦋]

Ah sorry for that. Fixed it.

[Timo Carlin-Burns]

#mwe? Even after adding import Batteries I get an error that toVector is not defined

[Karthik 🦋]

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Help.20with.20simple.20proof/near/476595905

I was referring to the code in this message earlier.

[Timo Carlin-Burns]

Ohh got it. Here interval_cases is probably more direct than fin_cases:

import Batteries

example (v : Batteries.Vector ℚ 7) (i : ℕ) (p : i < 7) :
    [v[0], v[1], v[2], v[3], v[4], v[5], v[6]][i] = v[i] := by
  interval_cases i <;> rfl

But if you do want to use fin_cases, one way is to use subst hj rather than rw [hj].

import Batteries

example (v : Batteries.Vector ℚ 7) (i : ℕ) (p : i < 7) :
    [v[0], v[1], v[2], v[3], v[4], v[5], v[6]][i] = v[i] := by
  let j : Fin 7 := Fin.mk i p
  have hj : i = j.val := rfl
  clear_value j
  subst hj
  fin_cases j <;> rfl

The version with rw [hj] gives an error because the syntax v[i] is implicitly constructing a proof of i < 7, and then this proof becomes type-incorrect when i changes to↑j because it is not a proof of ↑j < 7. In general rw doesn't work for replacing subterms which are depended on in the type of another subterm in the goal.

[Karthik 🦋]

Thats great. Thanks.

Why do we have to use clear_value? I notice that if I define j using a have, we don't have to do that.

[Timo Carlin-Burns]

subst hj tries to replace all occurrences of i with ↑j but since j is defined as j := Fin.mk i p, then that would result in j := Fin.mk ↑j p which would not be a valid definition because it has endless recursion

[Karthik 🦋]

That makes sense. Thanks.

[wuyoli]

after experimenting a bit I came to this:

import Mathlib

structure Quantity where (
  time
  length
  mass
  current
  temperature
  luminousIntensity
  amountOfSubstance : ℚ)
deriving Repr

def toVector (q : Quantity) : (Batteries.Vector ℚ  7) :=
  #v[
    q.time,
    q.length,
    q.mass,
    q.current,
    q.temperature,
    q.luminousIntensity,
    q.amountOfSubstance
  ]

def fromVector (v : Batteries.Vector ℚ 7) : Quantity :=
  {
    time              := v[0],
    length            := v[1],
    mass              := v[2],
    current           := v[3],
    temperature       := v[4],
    luminousIntensity := v[5],
    amountOfSubstance := v[6]
  }


theorem QuantityVectorRoundtrip (q : Quantity) : fromVector (toVector q) = q := by
  rfl

theorem VectorQuantityRoundtrip (v : Batteries.Vector ℚ 7) : toVector (fromVector v) = v := by
  ext i p
  interval_cases i <;>
  rfl

this works. Is this generally OK or is there still some problem?

[wuyoli]

hi, I continued on this and hit another Problem: I can't implement hDiv for another type I defined called physicalUnit. This is the current version of my code. there seems to be a colliding name of the definition of hDiv. how can I avoid this?

[Edward van de Meent]

the colon is in the wrong place.

[Edward van de Meent]

it should be after instance

[Edward van de Meent]

here's the fixed instance:

instance : HDiv (PhysicalUnit aq) (PhysicalUnit bq) (PhysicalUnit (aq/bq)) where
  hDiv (a : PhysicalUnit aq) (b : PhysicalUnit bq) : PhysicalUnit (aq/bq) :=
    match a, b with
      | PhysicalUnit.mk av, PhysicalUnit.mk bv => (PhysicalUnit.mk (av / bv) : PhysicalUnit (aq/bq))

[Edward van de Meent]

note that it needs brackets around aq/bq as otherwise it interprets it as (PhysicalUnit aq)/bq (which ofc doesn't make sense).

[wuyoli]

I still can't do this:

#eval Diameter / Period
#check Diameter / Period

Is there some magic I have to do to make this possible?

[wuyoli]

I thought this would be taken care of automatically. This worked for my Implementation of the Muland Div interface. Does this maybe not work automatically for HDiv?

[Derek Rhodes]

Hi, changing def to abbrev helps it #check:

abbrev Meter : Type := PhysicalUnit  length
abbrev Second : Type := PhysicalUnit  time

[wuyoli]

yeah, that works great, but #check gives Diameter / Period : PhysicalUnit (length / length) which should be equivalent to PhysicalUnit #{0,0,0,0,0,0,0} which is basically a number instead of meters/second which is what I would expect.

[Derek Rhodes]

yeah, your code has a bug :smile: :

def Second : Type := PhysicalUnit  length  -- <-- length should be time

[wuyoli]

Bruh, thank you

[wuyoli]

as you can see in the macro_rules part (line 50-70) I Made My own Notation. is this a sane way to do this? It feels a bit cumbersome to do it this way. (as you can see I did some experiments but It didn't work.) Is there a better way to do this?

[Derek Rhodes]

There is a mk constructor that structure provides which allows for:

def time              := Quantity.mk 1 0 0 0 0 0 0
def length            := Quantity.mk 0 1 0 0 0 0 0
def mass              := Quantity.mk 0 0 1 0 0 0 0
def current           := Quantity.mk 0 0 0 1 0 0 0
def temperature       := Quantity.mk 0 0 0 0 1 0 0
def luminousIntensity := Quantity.mk 0 0 0 0 0 1 0
def amountOfSubstance := Quantity.mk 0 0 0 0 0 0 1

There is another way using with syntax for updating structures

def default := Quantity.mk 0 0 0 0 0 0 0
-- ...
def amountOfSubstance : Quantity := { default with amountOfSubstance := 1 }

[wuyoli]

aah, ok, this makes it pretty simple

[wuyoli]

I have a Type for which i automatically derived the Ord class. but I still can't use > and < with it. I saw a class LT and LEexist for this, but I can't generate those implementations using deriving LE, LT what's the difference here?

[Alex Mobius]

It's just not implemented. You can do

instance: LT myThing := ltOfOrd
instance: LE myThing := leOfOrd

but I had trouble subsequently proving lemmas about my LT/LE. Maybe someone more experienced will chime in and explain it better.

[wuyoli]

Th have the following definitions:

def Energy : Type := BasicUnit (Quantity.mk (-2) 2 1 0 0)
def Torque : Type := BasicUnit (Quantity.mk (-2) 2 1 0 0)
#eval (BasicUnit.mk 5 : Energy) == (BasicUnit.mk 5 : Torque)

as you can see when doing it this way I get two values which lean considers to be the same, but I don't want them to be the same. How can I convince lean five Newton-meter are not equal to five Joules?

[Derek Rhodes]

Hi @wuyoli, could you please paste a link to the updated code you have for this now? I could not find a definition for BasicUnit.

[wuyoli]

here is my current version. as you can see there are some other experiments going on, but the current problem is in line 88

[Niels Voss]

Unfortunately, this is not possible the way you have it currently set up, since in Lean (and more generally, in math) if two objects are constructed exactly the same way, they are equal.

If you really want N*m to differ from J, the only thing I can think of is adding an 8th dimension for angles, and then doing N*m*radian instead. However, even though I know very little about physics, I think angles are supposed to be dimensionless so this might not be very appealing.

Maybe instead of drawing the distinction at the actual units, you could split the BasicUnit type into ScalarWithDimension and VectorWithDimension (or whatever you want to call them) types, with the latter having a vector space as a parameter. So that way Energy could be a scalar, while Torque is a dimensional vector in R^3 or the exterior power of R^3, depending on whether you like working with cross products or wedge products.

[Niels Voss]

I guess it depends on how much of a problem you think it is that 5 newton-meters = 5 joules. I mean, at some point someone might want to ask "How much energy does it take to apply 5 newton-meters of torque over an angle of 1 radian" and because radians are unitless, that's basically like multiplying by 1.

[Derek Rhodes]

Aside from "the torque being a vector issue", haskell has a newtype feature that allows for something like:

newtype Int1 = Int1 Int
newtype Int2 = Int2 Int

, so that passing an Int1 in place of Int2 is a type error. But, I could not find a Lean4 version of newtype.

[Niels Voss]

In practice, we either use

@[irreducible]
def Int1 : Type := Int

which is a relatively weak sort of encapsulation, since some things go through it and others don't. A stronger version is

structure Int1 : Type where
    value : Int

Maybe you would also include a deriving statement at the bottom, for things like DecidableEq and Repr

[Niels Voss]

The latter is, for example, used by String to require explicit conversions between String and List Char (and also to allow the compiler to represent strings in UTF-8 while the programming representation is a list of unicode codepoints)

[Derek Rhodes]

Nice! Thanks for the insight Niels. It looks like including @[irreducible] addresses @wuyoli's immediate concern. It sounds like you are seeing some future hurdles.

@[irreducible]
def Energy : Type := BasicUnit (Quantity.mk (-2) 2 1 0 0)

[Niels Voss]

Do note that @[irreducible] doesn't actually change the mathematics behind the theory, it just encourages certain parts of Lean to not unfold the definition in some circumstances. So it's still technically possible to prove Int1 = Int, it's just more difficult.
The structure definition on the other hand does actually make it impossible to prove Int1 = Int. It's also not possible to prove Int1 ≠ Int, because in Lean if types A, B defined in distinct locations have the same cardinality, then the statement A = B is neither provable nor disprovable in Lean. (Although usually most people don't care about equality between types)

[wuyoli]

my main concern is not only equality between types but also somehow making it impossible to do "illegal" operations with them (e.g. adding a angle to a natural number even tough their dimensions are equal)

[wuyoli]

when doing it with

Niels Voss said:

[...] A stronger version is

structure Int1 : Type where
    value : Int

[...]

when doing it this way I can't implement any classes for the derived types, right?
would it be possible to do something like:

inductive BasicUnit (q : Quantity) (n : ℕ) where
  | mk : ℚ → BasicUnit q n

with n being somehow guaranteed to be unique every time an new type is generated with BasicUnit?

[Niels Voss]

What do you mean by derived types? You can certainly implement typeclass instances for Int1, but you have to do so manually. And if you wanted to be able to add Int and Int1 you would have to derive an instance of HAdd Int1 Int Int1 or maybe allow Int to be coerced into Int1.

As for your example with n, afaik this is only possible with metaprogramming, where you can derive your own def_unit command to replace def.

[Niels Voss]

Maybe an isAngular : Bool parameter would be better than a n : Nat parameter?

[wuyoli]

I'm not sure if there are really no physical kinds which differ in more aspects than "angularity"

[wuyoli]

Niels Voss said:

What do you mean by derived types? You can certainly implement typeclass instances for Int1, but you have to do so manually. And if you wanted to be able to add Int and Int1 you would have to derive an instance of HAdd Int1 Int Int1 or maybe allow Int to be coerced into Int1.

I meant exactly this automatic generation of implementations especially since I Intend to introduce a new "level" in this tree with toleranced Units something like this:

structure TolerancedUnit (q : Quantity) where
  toTuple : (BasicUnit q) × (BasicUnit q)
  min_lt_max: compare toTuple.1 toTuple.2 == Ordering.lt

(this is inspired by the Implementation of the Vector type)

[Yan Yablonovskiy]

I meant exactly this automatic generation of implementations especially since I Intend to introduce a new "level" in this tree with toleranced Units something like this:

structure TolerancedUnit (q : Quantity) where
  toTuple : (BasicUnit q) × (BasicUnit q)
  min_lt_max: compare toTuple.1 toTuple.2 == Ordering.lt

This part is i think whats a bit ambiguous.

You also said

with n being somehow guaranteed to be unique every time an new type is generated with BasicUnit?

This is actually similar to what a dependent arrow type already does. This paragraph from 'Theorem Proving in Lean' could help:

"Given α : Type and β : α → Type, think of β as a family of types over α, that is, a type β a for each a : α. In that case, the type (a : α) → β a denotes the type of functions f with the property that, for each a : α, f a is an element of β a. In other words, the type of the value returned by f depends on its input.

Notice that (a : α) → β makes sense for any expression β : Type. When the value of β depends on a (as does, for example, the expression β a in the previous paragraph), (a : α) → β denotes a dependent function type. When β doesn't depend on a, (a : α) → β is no different from the type α → β. Indeed, in dependent type theory (and in Lean), α → β is just notation for (a : α) → β when β does not depend on a."

Taken from https://leanprover.github.io/theorem_proving_in_lean4/dependent_type_theory.html

Edit: And more specifically, maybe dependent products are helpful:
"Just as dependent function types (a : α) → β a generalize the notion of a function type α → β by allowing β to depend on α, dependent Cartesian product types (a : α) × β a generalize the Cartesian product α × β in the same way. Dependent products are also called sigma types, and you can also write them as Σ a : α, β a. You can use ⟨a, b⟩ or Sigma.mk a b to create a dependent pair. "

[wuyoli]

is there a good way to implement a vectorspace? I would like to implement the Quantity type as a vectorspace, but there doesn't seem to be a vectorspace typeclass. There seems to be the Mathlib.LinearAlgebra.Basis but I don't understand how to use this.

[Rishi Mathur]

You'd be implementing Module

[Riccardo Brasca]

variable {K M : Type*} [Field K] [AddCommGroup M] [Module K M] says that M is a vector space over K. If you want ℝ-vector spaces, just remove K and use variable {M : Type*} [AddCommGroup M] [Module ℝ M].

[wuyoli]

I Don't understand. what is this language construct with [...] called?
Do you mean something similar to:

inductive BasicUnit (q : Quantity) {M : Type*} [AddCommGroup M] [Module ℝ M] where
  | mk : ℚ → BasicUnit q

(I realized I probably can't make Quantity into a vector space because addition is not defined for all pairs of values. (only defined if both elements are equal.))

[Riccardo Brasca]

I just mean that

variable {M : Type*} [AddCommGroup M] [Module ℝ M]

is the translation in Lean of the English sentence "Let $M$ be an $\mathbb{R}$-vector space".

[Riccardo Brasca]

Can you explain in words what you want to formalize?

[wuyoli]

I have the type Family BasicUnit, which is parametrized by a Quantity. I Implemented Multiplication and Division for all combinations of this family, but addition and subtraction only for BasicUnits with the same Quantity.

[Riccardo Brasca]

Without knowing what Quantity is and a precise definition of BasicUnit it seems difficult to help. Also, I don't understand exactly what you want to do.

[wuyoli]

here is the current version of my code

[wuyoli]

I continued working on this, and now this is my current code:

import Mathlib.Data.Rat.Init
import Mathlib.MeasureTheory.Integral.IntervalIntegral

import Batteries.Data.Vector

/--
Quantity Represents a Basic Quantity in a 6-Dimensional Vectorspace.
Each coordiante is a exponent for a base Unit.
Inspired by <https://www.youtube.com/watch?v=bI-FS7aZJpY&t=335s>

Time, length, mass, current and temperature are self-explanatory.

Angle is needed to allow for differentiation between e.g. Energy
and Torque.

Luminous Intensity is not in this structure even though it is
one of the 7 SI-base units because its analogous to radiant Intensity
which is in turn not linearly independent to the other Units

Amount of substance is not here either because it is just a conversion
factor and its Dimension is the null vector.
--/
structure Quantity where (
  time
  length
  mass
  current
  temperature
  angle : ℚ)
deriving DecidableEq, Repr, BEq

def toVector (q : Quantity) : (Vector ℚ  6) :=
  #v[
    q.time,
    q.length,
    q.mass,
    q.current,
    q.temperature,
    q.angle
  ]

def fromVector (v : Vector ℚ 6) : Quantity :=
  {
    time        := v[0],
    length      := v[1],
    mass        := v[2],
    current     := v[3],
    temperature := v[4],
    angle       := v[5]
  }

theorem QuantityVectorRoundtrip (q : Quantity) : fromVector (toVector q) = q := by
  rfl

theorem VectorQuantityRoundtrip (v : Vector ℚ 6) : toVector (fromVector v) = v := by
  ext i p
  interval_cases i <;>
  rfl

def scalar      : Quantity := Quantity.mk 0 0 0 0 0 0
def time        : Quantity := Quantity.mk 1 0 0 0 0 0
def length      : Quantity := Quantity.mk 0 1 0 0 0 0
def mass        : Quantity := Quantity.mk 0 0 1 0 0 0
def current     : Quantity := Quantity.mk 0 0 0 1 0 0
def temperature : Quantity := Quantity.mk 0 0 0 0 1 0
def angle       : Quantity := Quantity.mk 0 0 0 0 0 1

instance : Mul Quantity where
  mul a b := fromVector (Vector.zipWith (toVector a) (toVector b) Add.add)

instance : Div Quantity where
  div a b := fromVector (Vector.zipWith (toVector a) (toVector b) Sub.sub)

class ToTypst (α : Type) where
  toTypst : α → String

--TODO: units are curently not formatted correctly
instance : ToTypst (Quantity) where
  toTypst a :=
    let f (unit : String) (exp : ℚ) : String :=
      if exp == 0.0 then
        ""
      else if exp == 1.0 then
        s!"{unit} "
      else
        s!"{unit}^{exp} ";
      (f "s"  a.time) ++
      (f "m"  a.length) ++
      (f "g" a.mass) ++
      (f "A"  a.current) ++
      (f "K"  a.temperature) ++
      (f "tr" a.angle)

/--
The naming is inspired by ASME Y14.5, which uses "basic dimension"
and "directly toleranced dimension". Here "unit" is used instead of
"dimension" to avoid confusion with the "dimension" of a physical
quantity.
--/
inductive BasicUnit (q : Quantity) where
  | mk : ℚ → BasicUnit q
  --| mk : Float → BasicUnit q
deriving Repr, BEq, Ord

instance : HAdd (BasicUnit q) (BasicUnit q) (BasicUnit q) where
  hAdd (a : BasicUnit q) (b : BasicUnit q) : BasicUnit q :=
    match a, b with
      | BasicUnit.mk av, BasicUnit.mk bv => (BasicUnit.mk (av + bv) : BasicUnit q)

instance : HSub (BasicUnit q) (BasicUnit q) (BasicUnit q) where
  hSub (a : BasicUnit q) (b : BasicUnit q) : BasicUnit q :=
    match a, b with
      | BasicUnit.mk av, BasicUnit.mk bv => (BasicUnit.mk (av - bv) : BasicUnit q)

instance : HMul (BasicUnit aq) (BasicUnit bq) (BasicUnit (aq * bq)) where
  hMul (a : BasicUnit aq) (b : BasicUnit bq) : BasicUnit (aq * bq) :=
    match a, b with
      | BasicUnit.mk av, BasicUnit.mk bv => (BasicUnit.mk (av * bv) : BasicUnit (aq * bq))

instance : HDiv (BasicUnit aq) (BasicUnit bq) (BasicUnit (aq / bq)) where
  hDiv (a : BasicUnit aq) (b : BasicUnit bq) : BasicUnit (aq / bq) :=
    match a, b with
      | BasicUnit.mk av, BasicUnit.mk bv => (BasicUnit.mk (av / bv) : BasicUnit (aq / bq))

def myMod (a: Float) (b : Float) : Float :=
  (a - Float.floor (a / b) * b)

instance : HMod (BasicUnit aq) (BasicUnit bq) (BasicUnit (aq / bq)) where
  hMod (a : BasicUnit aq) (b : BasicUnit bq) : BasicUnit (aq / bq) :=
    match a, b with
      | BasicUnit.mk av, BasicUnit.mk bv => (BasicUnit.mk (av % bv) : BasicUnit (aq / bq))
      --| BasicUnit.mk av, BasicUnit.mk bv => (BasicUnit.mk (myMod av bv) : BasicUnit (aq / bq))

instance : ToTypst (BasicUnit q) where
  toTypst a :=
    match a, q with
      | (BasicUnit.mk a), q => s!"{a} {ToTypst.toTypst q}"

abbrev Second : Type  := BasicUnit time
abbrev Meter  : Type  := BasicUnit length
abbrev Gram   : Type  := BasicUnit mass
abbrev Ampere : Type  := BasicUnit current
abbrev Kelvin : Type  := BasicUnit temperature
abbrev Turn   : Type  := BasicUnit angle

def Diameter      : Meter := BasicUnit.mk 4.8
def DiameterSmall : Meter := BasicUnit.mk 3.5
def Period        : Second := BasicUnit.mk 4.8

#eval DiameterSmall / Period
#check (Diameter / Period)

-- Torque ≠ Energy
abbrev Joule       : Type := BasicUnit (Quantity.mk (-2) 2 1 0 0 0)
abbrev NewtonMeter : Type := BasicUnit (Quantity.mk (-2) 2 1 0 0 (-1))
#check_failure (BasicUnit.mk 5 : Joule) == (BasicUnit.mk 5 : NewtonMeter)

#eval ToTypst.toTypst Diameter

def exampleTorque : NewtonMeter := BasicUnit.mk 44.8
#eval exampleTorque
#eval ToTypst.toTypst exampleTorque

def Rotations : Turn := BasicUnit.mk (4.0 : ℚ)
def MyEnergy  : Joule := exampleTorque / Rotations
#check exampleTorque / Rotations
#eval ToTypst.toTypst (exampleTorque / Rotations)

[Kevin Buzzard]

The preferred way to post code here is within triple back-ticks, like this for example:

(duplicate code now removed)

That way people can (a) see the code instantly (even on mobile) (b) jump to the live.lean-lang.org web page if they like (by clicking on the "View in Lean 4 playground" link at the top right of the code) and (c) copy the code into their clipboard and paste it locally into VS Code (by clicking on the other link in the top right).

[wuyoli]

Kevin Buzzard said:

The preferred way to post code here is within triple back-ticks, like this for example:

thank you, did that.

[wuyoli]

I'm currently wondering why the #check in line 151 doesn't evaluate the type further?
In line 166 the type is at least unfolded a step further, but still in line 165 the definiton does not work even though the type ({ time := -2, length := 2, mass := 1, current := 0, temperature := 0, angle := -1 } / angle) should be the same as Joule

[Mitchell Lee]

The types BasicUnit ({ time := -2, length := 2, mass := 1, current := 0, temperature := 0, angle := -1 } / angle) and Joule are indeed (propositionally) equal. However, it takes some computation to prove that they are equal, so they aren't definitionally equal (https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2023/Part_B/equality.html). Thus, Lean's type checking system, which only unfolds definitions and does not do any computations or reasoning, is not able to determine that they are equal.

Lean's type checking system does not attempt to check whether types are propositionally equal because propositional equality is undecidable. It is even undecidable whether basic types like ℕ and ℤ are equal to each other: #new members > Newbie question : Equality of Types

The solution to this problem is to include the Quantity as a field of the BasicUnit, rather than as an argument.
This will allow the user to write down illegal expressions such as $2\text{ seconds} + 5\text{ meters}$, which you can assign the "junk value" $0$ (or $7\text{ seconds}$, or whatever is most convenient). See https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/ for why this design is preferable, even though it may seem inelegant at first.

[wuyoli]

Isn't the whole point of a type system like this not to allow "illegal" operations? I thought about this and it seems really easy to accidentally add two values of different units and get unexpected results this way. from the xenaproject blogpost I understand I have to define Theorems to help with this, but I don't understand how this helps.

[Mitchell Lee]

It's just not possible to prevent "illegal" operations in the way that you're asking for. For example, consider the effect of the following lines to the end of your code. By Fermat's last theorem, length' is the same thing as length, therefore Meter is the same thing as Meter', therefore it should be possible to perform the addition in the last line below. However, it is not reasonable to expect the Lean compiler to know that it is possible. This is obviously an extreme example, but it the same problem you are running into when you try to reinterpret exampleTorque / Rotations as type Joule.

open Classical
noncomputable def length' : Quantity :=
  if (∃ (n a b c : ℕ), n ≥ 3 ∧ a > 0 ∧ b > 0 ∧ a ^ n + b ^ n = c ^ n) then time else length

abbrev Meter'  : Type  := BasicUnit length'

#check (BasicUnit.mk 2 : Meter) + (BasicUnit.mk 2 : Meter')

You could prevent "illegal" operations by throwing an error at runtime, but you cannot do it using type checking.

[Andrew Yang]

You can write unseal Rat.sub in to make lean see through some things.
But this still won't make your example work because NewtonMeter has angle := -1 so exampleTorque / Rotations has angle := -2 but a term of type Joule should have angle := 0.
Shouldn't angles be dimensionless anyway?

[Andrew Yang]

For example if NewtonMeter is changed to angle := 1 then

unseal Rat.sub in
def MyEnergy : Joule :=  exampleTorque / Rotations

just works

[wuyoli]

Yeah, thanks the unseal worked.

Shouldn't angles be dimensionless anyway?

usually yes, but doing it this way allows me to draw a distinction between Torque and energy, which would otherwise have the same Dimension.

For example if NewtonMeter is changed to angle := 1 then [...] just works

yeah, my bad this is the correct Dimension of NewtonMeter.

Is there a way to make the unseal a part of the HDiv implementation for BasicUnit?

[Andrew Yang]

The unseal Rat.sub in is abusing the fact that 2 - 1 = 1 definitionally so that you won't run into the issues that Mitchell pointed out above. These issues occur when you want to show that $s^{2-1}$ is defeq to $s^1$ so you need to explicitly add that line in your applications.

Alternatively, you can do attribute [local reducible] Rat.add Rat.sub at the top of the file to effectively achieve the same thing for the whole file, but as the warning indicates, this might cause some automation to not function correctly.

[wuyoli]

In that case I don't get the point of lean. I understand that this creates undecidable statemants, but Isn't the point of this to enable automatic generation of types and implementations for those types?

[Mitchell Lee]

I am not really sure what you want the type checking system to do. You cannot expect it to prevent the user from writing down undefined expressions in all possible cases. For example, $2 / (3 \cdot 2 - 6)$ is undefined, but you can still write down (2 / (3 * 2 - 6) : ℝ)in Lean. The compiler won't complain because there's no way to know that it's undefined without actually computing it, which is not what the type checking system is designed to do. We get around this issue by assigning a junk value to division by 0, so that (2 / (3 * 2 - 6) : ℝ) = 0 in Lean.

Similarly, there's no way to know that an expression like (BasicUnit.mk 5 : Joule) + (BasicUnit.mk 5 : NewtonMeter) / (BasicUnit.mk 4 : Turn) is well-defined without actually computing the Quantity of each term. This is why the type system rejects it unless you unseal Rat.sub. The solution to this issue is to make a single type that keeps track of both the value and the Quantity.

[Matt Diamond]

I mean, in theory you could define Real division as requiring that the 2nd argument be of type

{ r : ℝ // r ≠ 0 }

but the point is that the downsides would outweigh the benefits... it would make things unmanageable

[Matt Diamond]

In the field of software engineering, "make illegal states unrepresentable" is a good rule of thumb, but in Lean it turns out that allowing "illegal" states is actually much easier to work with, as mathematicians often care less about the exact value of a variable and more about what properties the value has... when they try to prove those properties, that's when the restrictions come in.

[wuyoli]

A friend of mine who knows some Agda tried helping me with this and we got here (the rest of the code is the same):
this is the code
we got to the error :"cannot evaluate, types are not computationally relevant " is this just another way of looking a the same plroblem we were discussing before or is there some way to do this?

[Aaron Liu]

What do you expect the #eval to do? Remember it needs to print a string.

[wuyoli]

didn't I do deriving Repr for just that?

[Aaron Liu]

wuyoli said:

didn't I do deriving Repr for just that?

Doing deriving Repr on X means that objects of type X can be printed. But X does not have type X: usually X : Prop or X : Type, but never X : X.

[wuyoli]

but #check doesn't evaluate the expression I give it. is there another command like that?

[Aaron Liu]

You can #reduce (types := true)