Term reduction in type

Stream: lean4

[Tomas Skrivan]

Quite often I work with a type that has a number in its type. Some functions introduce simple arithmetic on this number which can lead to horrendous types and I would like to reduce this arithmetic. Example:

1. Array type like Fin n -> Float Summing consecutive numbers(average pooling) gives Fin n/2 -> Float. Chaining this leads to Fin n/2/2/2/2 -> Float. I would like to have Fin n/16 -> Float.
2. Geometrical object Prism dim represents basic geometrical objects of dimension dim. You can for example multiply P : Prism n with Q : Prism m obtaining Prism n + m. See mwe for further details
3. Dimensional quantities, for time t : ℝ[s] (real number with seconds as units) and velocity v : ℝ[m*s⁻¹] the expression v * t or tv should have the type ℝ[m] not ℝ[ms⁻¹s] or ℝ[sm*s⁻¹]`. I have partially solved this problem using custom elaborator, see this thread.

This reduction is doable with a custom elaborator, but I don't think it is the right approach. This way I would have to write a custom elaborator for every function involving Prim dim. So I'm curious if anyone has an idea how to tackle this problem?

---

Example with Prism n

inductive PrismBase where
  | point : PrismBase
  | cone (P : PrismBase) : PrismBase
  | prod (P Q : PrismBase) : PrismBase

def PrismBase.dim : PrismBase → Nat
| point => 0
| cone P => dim P + 1
| prod P Q => dim P + dim Q

structure Prism (n : Nat) where
  val : PrismBase
  property : val.dim = n

def Prism.cone (P : Prism n) : Prism (n+1) := ⟨P.1.cone, by simp[PrismBase.dim, P.2]⟩
def Prism.prod (P : Prism n) (Q : Prism m) : Prism (n+m) := ⟨P.1.prod Q.1, by simp[PrismBase.dim, P.2, Q.2]⟩

def point : Prism 0 := ⟨.point, rfl⟩
def segment := point.cone
def square := segment.prod segment

Now have a look at the types:

#check segment -- Prism (0 + 1)             ... should be Prism 1
#check square  -- Prism (0 + 1 + (0 + 1))   ... should be Prism 2
#check λ {n} (P : Prism n) => P.cone.cone -- Prism n → Prism (n + 1 + 1)  ... should be Prism n → Prism (n + 2)

My attempt to fix this using default arguments:

def Prism.cone' (P : Prism n) (m := (by let dim := n+1; (conv at dim => reduce); apply dim)) (h : m = n+1 := by rfl) : Prism m := ⟨P.1.cone, by simp[h,PrismBase.dim, P.2]⟩

def segment' := point.cone'
#check segment' --- Prism (let dim := 0 + 1; Eq.mp (_ : Nat = Nat) dim)

... this makes it even worse.

[Henrik Böving]

I tried a general elaborator along the lines of:

elab "reduce_type_of" t:term : term => do
  let val ← elabTerm t none
  let typ ← inferType val
  let reduced ← reduce typ (skipTypes := false)
  logInfo s!"Reduced to {reduced}"
  elabTerm t reduced

def segment2 := reduce_type_of (point.cone)
#check segment2

but while it is internally able to reduce the type this does somehow not get properly propagated upwards :(

[Tomas Skrivan]

Nice, I was thinking about writing an elaborator like that but didn't get around to it, plus it is still somewhat suboptimal solution.

Here is a fixed version that enforces the cast to the reduced type:

elab "reduce_type_of" t:term : term => do
  let val ← elabTerm t none
  let typ ← inferType val
  let reduced ← reduce typ (skipTypes := false)
  logInfo s!"Reduced to {reduced}"
  let proof ← mkAppOptM ``rfl #[mkSort levelOne, reduced]
  mkAppOptM ``cast #[typ, reduced, proof, val]

def segment2 := reduce_type_of (point.cone)

#check segment2

[Tomas Skrivan]

Also for more complicated cases I'm thinking about notation by convSeq ▸ term which would allow you to rewrite a type of a term using more advanced tactics like ring.

[Kevin Buzzard]

If you think these are problems, wait until you run into situations where the numbers in the types aren't defeq! I would imagine that prism 0+1 and prism 1 are equal by rfl. Can you solve your problem with type ascriptions, eg def segment : Prism 1 := point.cone? The problem we ran into in LTE was that Prism (a+b) and Prism (b+a) are not defeq so we defined functions between the types which were "morally the identity" and trained the simplifier to cancel them where possible.

[Henrik Böving]

Well you can use any proof producing function in place of reduce and rfl here if you want to really so I don't see an issue? IN theory we could also just run simp against the thing and it would give us a new expression + a proof for the cast we could use

[Tomas Skrivan]

Yes using type ascriptions is possible but useful only for predefined things. In my test, I wrote down a simple neural network and the resulting type contained

Fin 10 × Fin (10 / 2) × Fin (numOf (Fin (16 / 2)) * numOf (Fin (16 / 2)) / 2)

which is just

Fin 10 × Fin 5 × Fin 32

My main concern right now is user experience. When you chain bunch of functions together you really want to see human comprehensible type at the end.

Yes, I'm expecting that sooner or later I will run into cases which are not defeq. Thanks for pointing out that you dealt with this problem in LTE, I will look for inspiration there in the future.

[Tomas Skrivan]

Henrik Böving said:

Well you can use any proof producing function in place of reduce and rfl here if you want to really so I don't see an issue? IN theory we could also just run simp against the thing and it would give us a new expression + a proof for the cast we could use

I was just thinking aloud, there is no real issue. Only the fact that I do not know how to run a tactic during elaboration.

[James Gallicchio]

A closed term is always defeq to its normal form, right? I feel like as a user I have much lower expectations for expressions with variables, so it feels like a good first step to even just reduce closed terms

[Mario Carneiro]

not always: if you cast 2 : Nat by a proof of (True -> True) = True by propext, the resulting term is provably equal to 2 but fails to normalize

[James Gallicchio]

oh :/ that's unfortunate. is there a tactic that reduces terms with casts and such?

[Mario Carneiro]

no, at least not one that generates a proof

[Tomas Skrivan]

The conv => reduce is not doing everything you want?

[Mario Carneiro]

the example I just gave is one where even #reduce unfolding proofs and everything still fails

[Mario Carneiro]

it's the type theory itself that is deficient in this case

[Mario Carneiro]

I mean, you can't really fault it for not unfolding an axiom which has no definition

[Tomas Skrivan]

Can you give mwe? I fail to precisely understand your description.

[Mario Carneiro]

#reduce
  have : (True → True) = True := eq_true id
  this ▸ 2
-- not 2

[Tomas Skrivan]

Huh, I'm surprised that this ▸ 2 even typechecks

[Mario Carneiro]

why wouldn't it? We're rewriting the type Nat by replacing occurrences of True -> True with True, resulting in Nat

[Mario Carneiro]

even if \t decided to point out that it's useless I could do the same thing by calling Eq.rec directly

[James Gallicchio]

Mario Carneiro said:

no, at least not one that generates a proof

What does it take to generate the proof?

[Mario Carneiro]

HoTT

[Mario Carneiro]

doing this in general is an open research question, to put it mildly

[James Gallicchio]

wait but you said the term is provably equal to 2 :joy: I feel like i've gotten rid of casts in terms before

[Mario Carneiro]

you can do it in every individual case with some trickery or another

[Mario Carneiro]

it seems likely to be true in general, but constructing a tactic that does it is another matter altogether

[Mario Carneiro]

because you have to deal with casts and casts of casts ad infinitum

[Mario Carneiro]

hence HoTT

[James Gallicchio]

I see, makes sense. It seems like we'd want a best-effort tactic in mathlib for this? Or at least that knows the "trickery" for common cases?

[Mario Carneiro]

example : (have : (True → True) = True := eq_true id; this ▸ 2) = 2 := by
  suffices ∀ a, (h : (True → True) = a) → (h ▸ 2) = 2 from this True _
  intro | _, rfl => rfl

[Mario Carneiro]

the common case is that you don't do this

[Mario Carneiro]

Most tactics just don't deal with casts, or only handle them via congr which can rewrite some dependent functions

[Tomas Skrivan]

Yay! I have figured out how to do it without cast as cast is pain to deal with ...

The solution is to just use let binding.

open Lean Elab Term Meta in
elab "reduce_type_of" t:term : term => do
  let val ← elabTerm t none
  let typ ← inferType val
  let reduced ← reduce typ (skipTypes := false)
  Expr.letE `x reduced (val) (Expr.bvar 0) false |> pure

#check reduce_type_of point.cone -- Prism 1