Unfolding the type of a variable creates a new variable

Stream: lean4

[Alex Keizer]

I'm working on a proof that requires me to unfold the type of some variable x, so that I can do a cases on the internal definition.
However, when doing this unfold, lean adds a new variable to the context, of the required unfolded type, but all other occurences of x still refer to the now inaccessible original variable.

def Wrapper (n : Nat) : Type × Type := (Fin n, Fin n)

def some_property {n} (x : Fin n) : Prop
:= True


example {n} (x : (Wrapper n).1) (h : some_property x) : True :=
by
  /-
    n : Nat
    x : (Wrapper n).fst
    h : some_property x
    ⊢ True
  -/
  unfold Wrapper at x
  /-
    n : Nat
    x✝ : (Wrapper n).fst
    h : some_property x✝
    x : (Fin n, Fin n).fst
    ⊢ True
  -/
  rename_i x';
  have : x = x' := by sorry
  sorry

I've tried to prove that x and x✝ are equal, without much success.

I want to do this unfold because I need to a cases on something that uses x, which fails with the error tactic 'generalize' failed, result is not type correct unless I unfold the type of x. Sadly have not managed to find a MWE that has this behaviour.

[Leonardo de Moura]

@Alex Keizer Thanks for raising this issue. We will improve the unfold tactic. It is currently using the simp infrastructure which creates auxiliary declarations instead of replacing them when there are dependencies. It the meantime, here are two possible workarounds.

def Wrapper (n : Nat) : Type × Type := (Fin n, Fin n)

def some_property {n} (x : Fin n) : Prop
:= True

example {n} (x : (Wrapper n).1) (h : some_property x) : True :=
by
  delta Wrapper at x
  sorry

example {n} (x : (Wrapper n).1) (h : some_property x) : True :=
by
  revert x h
  unfold Wrapper
  intro x h
  sorry

BTW, the delta tactic preserves definitional equality, and it will expose the internal encoding used to justify the termination of recursive functions. It is not an issue in the example above because Wrapper is not recursive.

[Leonardo de Moura]

BTW, the second workaround only works if the unfold is preserving definitional equality. This is the case for your example, but it is not true in the following one.

def NatTuple : Nat → Type
  | 0 => Unit
  | 1 => Nat
  | n+1 => Nat × NatTuple n

def NatTuple.property (x : NatTuple n) : Prop := True

example (x : NatTuple 3) (h : x.property) : True := by
  revert x h
  unfold NatTuple -- Did not unfold `NatTuple`.

[Alex Keizer]

Thanks, I hadn't heard of delta before, but it seems to do exactly what I need!
My more complicated unfold does preserve definition equality as well (at least, the types can be proven equal with a rfl), hence my surprise with unfolds behaviour.

Turns out my actual issue was something else, as soon as I used delta, the tactic 'generalize' failed error popped up again.
Managed to fix it by introducing a new variable with a let-binding, rather than doing cases directly on an expression.

[Leonardo de Moura]

Turns out my actual issue was something else, as soon as I used delta, the tactic 'generalize' failed error popped up again.

Could you please send us the example that triggered the problem?

[Alex Keizer]

It's in this file: https://github.com/alexkeizer/qpf4/blob/master/Qpf/PFunctor/Multivariate/M.lean
The working code is

theorem M.bisim_lemma {α : TypeVec n}
                      {a₁ : (Mp P).A}
                      {f₁ : (Mp P).B a₁ ⟹ α}
                      {a' : P.A} {f' : (P.B a').drop ⟹ α}
                      {f₁' : (P.B a').last → M P α}
                      (e₁ : M.dest P ⟨a₁, f₁⟩ = ⟨a', splitFun f' f₁'⟩)
                    :
    ∃ (g₁' : _) (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩),
      f' = M.pathDestLeft P e₁' f₁
      ∧ f₁' = fun x : (last P).B a' => ⟨g₁' x, M.pathDestRight P e₁' f₁ x⟩
:= by
  revert e₁
  generalize ef : @splitFun n _ (append1 α (M P α)) f' f₁' = ff ;
  intro e₁;
  -- \/ HERE
  let he₁' := PFunctor.M.dest a₁;
  rcases e₁' : he₁' with ⟨a₁', g₁'⟩;
  -- /\ HERE
  rw [M.dest_eq_dest' P e₁'] at e₁
  cases e₁
  exact ⟨_, e₁', split_fun_inj ef⟩

I originally used

rcases e₁' : PFunctor.M.dest a₁ with ⟨a₁', g₁'⟩;

Which triggered the error

This is on nightly-2022-03-17, btw. I tried to update to the most recent nightly but that broke some other stuff.

I was trying to unfold Mp at variable a1, but it seems that wasn't even necessary after I introduced the let-binding

[Leonardo de Moura]

I pushed a fix for unfold and simp. They do not create the auxiliary declaration anymore when the result is definitionally equal.
Thanks for posting the full example above. It would be great if we could create a #mwe for it. It would help us to diagnose the problem.
Does the issue also happen when you use match-tactic?

match e₁' : PFunctor.M.dest a₁ with | ⟨a₁', g₁'⟩ =>

[Alex Keizer]

The match fails also, but with a more descriptive error

application type mismatch
  pathDestLeft P e₁'
argument
  e₁'
has type
  { fst := a₁', snd := g₁' } = { fst := a', snd := g₁' } : Prop
but is expected to have type
  PFunctor.M.dest a₁ = { fst := a', snd := g₁' } : Prop

Marking PFunctor.M.dest as an abbrev rather than a def makes the error go away.
Interestingly, with the abbrev version of M.dest the original rcases also works