Porting Lean code to Lean 3.17.0

Stream: general

[Simon Hudon]

I have code working with 3.8.0 and I'm porting it to 3.17.0 and some of my rewrites break. I'm having a hard time identifying where the issue is coming from but someone understanding what happened to unify and rewrite (e.g. @Mario Carneiro or @Gabriel Ebner ) might be able to help.

I have a definition to_subtype that I'm unfolding using rw to_subtype. That rewrite doesn't work anymore and neither do dsimp, simp, unfold and dunfold. I can get the work done again by using either

    simp [to_subtype.equations._eqn_1 i_n α p i_a], -- or
    rw to_subtype.equations._eqn_1 i_n α p i_a,

That is to say that I'm providing all the arguments of the exact right equation. Here is the error message when I write:

    rw to_subtype.equations._eqn_1,

rewrite tactic failed, did not find instance of the pattern in the target expression
  @to_subtype (succ ?m_1) ?m_2 ?m_3 (@fin'.raise ?m_1 ?m_4) ?m_5
state:
2 goals
n i_n : ℕ,
i_a : fin' i_n,
i_ih :
  ∀ {α : typevec i_n} (p : α ⟹ repeat i_n Prop) (x : @subtype_ i_n α p i_a),
    @to_subtype i_n α p i_a (@of_subtype i_n α p i_a x) = @id i_n (@subtype_ i_n α p) i_a x,
α : typevec i_n.succ,
p : α ⟹ repeat i_n.succ Prop,
x : @subtype_ i_n.succ α p i_a.raise
⊢ @to_subtype i_n.succ α p i_a.raise (@of_subtype i_n α.drop (@drop_fun i_n α (repeat i_n.succ Prop) p) i_a x) =
    @id i_n.succ (@subtype_ i_n.succ α p) i_a.raise x

Any idea?

[Mario Carneiro]

Do you have a #mwe?

[Simon Hudon]

Not yet

[Mario Carneiro]

Maybe just something with the definition of to_subtype and fin'.raise and everything else stubbed out

[Simon Hudon]

Let's see

[Simon Hudon]

Ok, I got a small-ish example to type check and ... rw doesn't fail

[Simon Hudon]

Ok now I managed to fail:

inductive fin' : ℕ → Type
| raise {n : ℕ} : fin' n → fin' n.succ
| last {n : ℕ} : fin' n.succ

def fin'.elim0 {α} : fin' 0 → α .

universes u

def typevec (n : ℕ) := fin' n → Type*

def arrow {n} (α β : typevec n) := Π i : fin' n, α i → β i

infixl ` ⟹ `:40 := arrow
open nat

def append1 {n} (α : typevec n) (β : Type*) : typevec (n+1)
| (fin'.raise i) := α i
| fin'.last      := β

def repeat : Π (n : ℕ) (t : Sort*), typevec n
| 0 t := fin'.elim0
| (nat.succ i) t := append1 (repeat i t) t

def of_repeat : Π {n i} (x : repeat n Prop i), Prop
| (nat.succ n) (fin'.raise i) x := @of_repeat n i x
| (nat.succ n) fin'.last x := x

namespace typevec

def id {n} {α : typevec n} : α ⟹ α := λ i x, x

def drop {n} (α : typevec (n+1)) : typevec n := λ i, α i.raise

def last {n} (α : typevec (n+1)) : Type* := α fin'.last

end typevec

open typevec

def drop_fun {n} {α β : typevec (n+1)} (f : α ⟹ β) : drop α ⟹ drop β :=
λ i, f i.raise

infixl ` ::: `:67 := append1

def subtype_ : Π {n} {α : typevec.{u} n} (p : α ⟹ repeat n Prop), typevec n
| 0 α p := fin'.elim0
| (succ n) α p := @subtype_ n (drop α) (drop_fun p) ::: _root_.subtype (λ x, p fin'.last x)

def to_subtype : Π {n} {α : typevec.{u} n} (p : α ⟹ repeat n Prop), (λ (i : fin' n), { x // of_repeat $ p i x }) ⟹ subtype_ p
| (succ n) α p (fin'.raise i) x := to_subtype (drop_fun p) i x
| (succ n) α p fin'.last x := x

def of_subtype : Π {n} {α : typevec.{u} n} (p : α ⟹ repeat n Prop),
  subtype_ p ⟹ (λ (i : fin' n), { x // of_repeat $ p i x })
| (succ n) α p (fin'.raise i) x := of_subtype _ i x
| (succ n) α p fin'.last x := x

example {i_n : ℕ}
  (i_a : fin' i_n)
  {α : typevec i_n.succ}
  (p : α ⟹ repeat i_n.succ Prop)
  (x : subtype_ p i_a.raise) :
  to_subtype p i_a.raise (of_subtype p i_a.raise x) = id i_a.raise x :=
begin
  rw [of_subtype,to_subtype],
end

[Simon Hudon]

It works in 3.10.0 and breaks in 3.11.0

[Simon Hudon]

I think that where your rw PR came in but I don't see why it would break it

[Mario Carneiro]

which PR is that?

[Simon Hudon]

Instantiate meta vars before applying rw

[Mario Carneiro]

#?

[Bryan Gin-ge Chen]

lean#213

[Mario Carneiro]

You seem to have something funny going on with definitional equality, even before getting to the rw.

variables {m : ℕ} (i : fin' m) {α : typevec m.succ} (p : α ⟹ repeat m.succ Prop)
#check (rfl : subtype_ p i.raise = subtype_ (drop_fun p) i) -- works
#check λ (x : subtype_ p i.raise), show subtype_ (drop_fun p) i, from x -- fails

[Simon Hudon]

Does it fail also in Lean 3.10?

[Mario Carneiro]

This version of subtype_ makes it work:

def subtype_ {n} {α : typevec.{u} n} (p : α ⟹ repeat n Prop) : typevec n :=
λ i, begin
  induction i with n i IH generalizing α p,
  { exact @IH (drop α) (drop_fun p) },
  { exact _root_.subtype (λ x, p fin'.last x) }
end

[Simon Hudon]

Why does this make a difference?

[Mario Carneiro]

Well for one thing it's doing induction on the fin' instead of induction on nat and then cases on fin'

[Simon Hudon]

I see. That fixes your example but not mine though

[Mario Carneiro]

there seems to be a similar problem in of_subtype

[Mario Carneiro]

Adding this modification of of_repeat makes your example work

def of_repeat {n i} : repeat n Prop i → Prop :=
begin
  induction i with n i IH,
  { exact IH },
  { exact id }
end

[Simon Hudon]

uh

[Simon Hudon]

How did you zero in on of_repeat?

[Mario Carneiro]

I'm suspecting everything that uses the equation compiler right now

[Mario Carneiro]

because you need defeqs everything has to be clean inductive definitions

[Mario Carneiro]

None of this is to say that lean isn't being buggy

[Simon Hudon]

Has anything changed in the equation compiler lately?

[Mario Carneiro]

It is something in the elaborator I think

[Mario Carneiro]

As the rfl proof shows, it is actually defeq and lean knows it when asked directly

[Mario Carneiro]

but when it comes up in the application lean is using a different reducibility setting or something and refuses to accept it

[Mario Carneiro]

In your example, this means that the goal after the first rewrite is "not well typed" and this is causing some knock on effect in the second rw

[Simon Hudon]

I think @Gabriel Ebner changed the unification to prevent irreducible definitions from getting unfolded. I wonder if this could be a side effect

[Mario Carneiro]

For these type level recursive definitions, I suggest you stick to using rec_on directly or induction, and prove the equational lemmas yourself

[Simon Hudon]

Fun

[Simon Hudon]

I don't think have PRed the new API functions to register equational lemmas yet. Maybe this would be a good use for it

[Simon Hudon]

Thanks for helping me debug this