Nested unfolding

Stream: lean4

[Siddhartha Gadgil]

I had hoped (perhaps unreasonably) that the following should unfold and be proved by reflexivity (actually a little more complicated case, but this is after minimization. Could someone help me with the best approach (lean 4 stable build)?

def shiftAtNat : (n : Nat) →  (k: Nat) → Nat → Nat :=
      fun n =>
        match n with
        | 0 =>
          fun k =>
                  fun _ =>
                    0
        | m + 1 =>
          fun k =>
            match k with
            | 0 =>
                fun i =>
                  i + 1
            | l+1 =>
                fun j =>
                  match j with
                  | 0 => 0
                  | i + 1 =>
                      (shiftAtNat m l i) + 1

theorem seqShiftNatLemma: (m: Nat) → (l: Nat) → (i : Nat) →
     (shiftAtNat (m + 1) (l + 1)  (i + 1)) =
      (shiftAtNat m l  i) + 1 := sorry

Thanks.

[Mario Carneiro]

I believe this to be a bug, leanprover/lean4#445

[Mario Carneiro]

The proof is rfl but you have to circumvent the elaborator to get the proof to be accepted

[Siddhartha Gadgil]

Thanks. How do I circumvent the elaborator?

[Mario Carneiro]

Actually, I tested this and the generated smart unfolding lemma is fine; the only issue is you didn't intro the arguments

[Mario Carneiro]

theorem seqShiftNatLemma (m l i : Nat) :
     (shiftAtNat (m + 1) (l + 1)  (i + 1)) =
      (shiftAtNat m l  i) + 1 := rfl

[Siddhartha Gadgil]

Thanks a lot. I now see that fun m => fun l => fun i => rfl also works.

[Mario Carneiro]

you can also write fun m l i => rfl fyi

[Mario Carneiro]

same thing with the (m l i : Nat) → ... binder

[Siddhartha Gadgil]

Yes, thanks. I am learning lean and so tend to be very verbose.