Circumventing "motive not type-correct"

Stream: lean4

[James Gallicchio]

Since this has been a continuous issue for me, asking for some guidance on how to avoid issues with rewriting terms appearing in dependent positions.

Here's an example:

  @[simp]
  theorem length_rangeAux : (rangeAux n L).length = L.length + n := by
    induction n generalizing L <;> simp [length, rangeAux, *]
    case succ n ih =>
    rw [←Nat.add_one, Nat.add_comm n 1, Nat.add_assoc]

  @[simp]
  theorem length_range : (range n).length = n := by
    simp [range]

  theorem rangeAux_eq_append
    : rangeAux n (x :: L) = rangeAux n [] ++ (x :: L)
    := by
    suffices ∀ L, rangeAux n L = rangeAux n [] ++ L from
      this (cons x L)
    intro L
    induction n generalizing L
    simp [rangeAux]
    case succ n ih =>
    simp [get, rangeAux]
    rw [@ih (n :: L), @ih [n]]
    simp [List.append_assoc]

  @[simp]
  theorem get_range (i : Fin n) : (range n).get (cast (by simp) i) = i
    := by
    induction n
    exact i.elim0
    case succ n ih =>
    unfold range
    simp [rangeAux]
    rw [rangeAux_eq_append]

Here, I want to rewrite but the term occurs as the argument to get. I've tried manually generalizing the term here but failed to make progress

[Mario Carneiro]

best thing is to eliminate references to get asap by replacing them with get?

[Mario Carneiro]

(that's not a #mwe)

[James Gallicchio]

Mario Carneiro said:

(that's not a #mwe)

Thought I could get away with it cuz this is a useful lemma to have around :joy:

[Mario Carneiro]

the important thing about #mwe is to put the right imports at the top

[Mario Carneiro]

in this case

import Mathlib.Data.List.Basic

namespace List

[James Gallicchio]

Oh, sorry! I think it just needs namespace List, everything else is Prelude material I think

[James Gallicchio]

Rewriting the get is a good idea, I can definitely give that a shot. But it doesn't apply in general, right? I was reading through an old thread in Lean3 world and I think at the time you suggested just using simp_rw or something which would insert casts as needed

[James Gallicchio]

(But which we don't have yet in Lean 4)

[Mario Carneiro]

it kind of applies in general, the general technique is to reduce dependent types to nondependent types + predicates

[James Gallicchio]

Ah, which is what you showed me last time with generalizing to forall o h, etc

[James Gallicchio]

Okay, I did try something like that with this example but it didn't seem to be helping, let me see if I can re-derive that...

[Mario Carneiro]

here's a proof (modulo the part I assume you know how to handle). I think that get_range as stated is just a really hard theorem to work with and I would suggest alternatives like get_range'

  theorem get?_range (n) (i : Nat) (h : i < n) : (range n).get? i = some i := by
    induction n with
    | zero => cases h
    | succ n ih =>
      unfold range
      simp [rangeAux]
      rw [rangeAux_eq_append]
      sorry

  theorem get_range' (n) (i : Nat) (h) : (range n).get ⟨i, h⟩ = i := by
    rw [← Option.some_inj, ← get?_eq_get]
    exact get?_range _ _ (by simp at h; exact h)

  @[simp]
  theorem get_range (i : Fin n) : (range n).get (cast (by simp) i) = i := by
    have : ∀ m (h : m = n) h', (cast (h ▸ rfl) i : Fin m) = ⟨i, h'⟩ := by
      intros m h h'; cases h; rfl
    rw [this]; apply get_range'; simp; simp [i.2]

[Leonardo de Moura]

BTW, we should probably use the TR + csimp trick to hide rangeAux. We have done it for a few List functions, but not for range. https://github.com/leanprover/lean4/blob/master/src/Init/Data/List/Basic.lean#L145

[James Gallicchio]

As in define range via

def range : Nat → List Nat
  | 0 => []
  | n+1 => range n ++ [n]

and then prove equivalence to the TR one?

[Mario Carneiro]

I think the best definition for proofs is one that uses :: and does not use tail recursion

[James Gallicchio]

It has the same problem as reverse in that it can't really be defined that way

[Mario Carneiro]

not quite like reverse, you can do it but you need an aux which specifies the starting point

[Mario Carneiro]

def rangeAux₂ : Nat → Nat → List Nat
  | 0,   a => []
  | n+1, a => a :: rangeAux₂ n (a+1)

def range₂ (n : Nat) : List Nat :=
  rangeAux₂ n 0

[Marcus Rossel]

What is the "TR + csimp trick"?

[Leonardo de Moura]

Marcus Rossel said:

What is the "TR + csimp trick"?

Here is the List.map instance

• We first define the non-tail-recursive version that is more convenient to use in proofs

def map (f : α → β) : List α → List β
  | []    => []
  | a::as => f a :: map f as

• Then, we define the tail-recursive version which is better for code generation

@[specialize] def mapTRAux (f : α → β) : List α → List β → List β
  | [],    bs => bs.reverse
  | a::as, bs => mapTRAux f as (f a :: bs)

@[inline] def mapTR (f : α → β) (as : List α) : List β :=
  mapTRAux f as []

• We prove they are equal and mark the theorem with [csimp]. After that, the code generator replaces any occurrence of map with mapTR.

[Leonardo de Moura]

theorem mapTRAux_eq (f : α → β) (as : List α) (bs : List β) : mapTRAux f as bs =  bs.reverse ++ map f as := by
  induction as generalizing bs with
  | nil => simp [mapTRAux, map]
  | cons a as ih =>
    simp [mapTRAux, map]
    rw [ih (f a :: bs), reverse_cons, append_assoc]
    rfl

@[csimp] theorem map_eq_mapTR : @map = @mapTR := by
  apply funext; intro α; apply funext; intro β; apply funext; intro f; apply funext; intro as
  simp [mapTR, mapTRAux_eq]

[Jake Levinson]

This is very interesting. Does this situation / trick also come up for Lean 3?

Also, once the two definitions are set up and the second one equality theorem is marked [csimp], is the non-tail-recursive definition still available if we want to use it for further proofs?

[Henrik Böving]

From looking at the implementation https://github.com/leanprover/lean4/blob/master/src/Lean/Compiler/CSimpAttr.lean the "marking" only causes the two to be added into a Name -> Name map, it doesnt touch the declarations at all. ANd the fact that replaceConstants is exported here: https://github.com/leanprover/lean4/blob/master/src/Lean/Compiler/CSimpAttr.lean#L53, makes me think that it's probably gonna be used by the C parts of the compiler after the registration process.

[Henrik Böving]

Also both the export and csimp attributes are missing from doc-gen I'll add them right away...

[Henrik Böving]

@Leonardo de Moura there doesn't seem to be an obvious way to gain access to the theorem that declares this type of replacement is valid right now since it's not implemented as a regular tag attribute but this custom extension based on the name map, could we maybe have a tag attribute that marks the theorem in addition to this map? Or some other way to recover it?

Also since it is not obvious from the declaration that it will be replaced later on I guess it would make sense to mark the declaration that is getting replaced by the compiler later on as well in the docs right? (which is possible right now)

[Mario Carneiro]

Jake Levinson said:

This is very interesting. Does this situation / trick also come up for Lean 3?

Also, once the two definitions are set up and the second one equality theorem is marked [csimp], is the non-tail-recursive definition still available if we want to use it for further proofs?

This approach makes the "official" one not tail recursive, and when you definitionally unfold it and use it in proofs that's what you see. The @[csimp] lemma rewrites the non-tail-recursive function into a tail recursive version (which is also available for proofs, but is not recommended outside the map_eq_mapTR theorem itself) which is intended primarily for compilation. This means that when you use map you get the mapTR implementation in the compiler, but when you reason about it you see only map. This gives us the best of both worlds, and the equality is proven so there is no expansion of the TCB either.

[Mario Carneiro]

This trick is not done in lean 3, but I think the lean 3 interpreter doesn't do TCO so there isn't much point in formulating things as tail recursive

[Henrik Böving]

Henrik Böving said:

Leonardo de Moura there doesn't seem to be an obvious way to gain access to the theorem that declares this type of replacement is valid right now since it's not implemented as a regular tag attribute but this custom extension based on the name map, could we maybe have a tag attribute that marks the theorem in addition to this map? Or some other way to recover it?

Also since it is not obvious from the declaration that it will be replaced later on I guess it would make sense to mark the declaration that is getting replaced by the compiler later on as well in the docs right? (which is possible right now)

I could also try and add this myself if the compiler folks are busy doing other stuff (and its desired) of course.

[Leonardo de Moura]

@Henrik Böving Sorry for not responding earlier, I was a bit overwhelmed in the last few days. I will add the missing feature today.

[Henrik Böving]

No worries^^ Usually you just add something the next day whenever you are asked for something, it's perfectly fine to take a bit longer of course xd

[Leonardo de Moura]

@Henrik Böving Added hasCSimpAttribute

[Henrik Böving]

\o/