## Stream: lean4

### Topic: Smart unfolding produces ununfoldable terms

#### Mario Carneiro (Apr 07 2021 at 00:59):

It appears that smart unfolding can put the idRhs quite deep in the term, in particular behind a if, which can cause the term to be blocked for unfolding in a generic context:

def foo (i j : Nat) : Nat :=
if i < 5 then 0 else
match j with
| Nat.zero => 1
| Nat.succ j => foo i j

#print foo._sunfold
-- def foo._sunfold : Nat → Nat → Nat :=
-- fun (i j : Nat) =>
--   if i < 5 then 0 else
--     match j with
--     | Nat.zero => idRhs Nat 1
--     | Nat.succ j => idRhs Nat (foo i j)

example (h : i < 5) : foo i j = 0 := by
simp [foo, h] -- fails to unfold foo


#### Mario Carneiro (Apr 07 2021 at 01:24):

In fact, there is no delta or dsimp or dunfold or unfold tactic to use instead, and the elaborator outright rejects a straight unfolding of this definition by rfl:

theorem foo_eq : foo = fun (i j : Nat) =>
@Nat.brecOn.{1} (fun (j : Nat) => Nat) j
fun (j : Nat) (f : @Nat.below.{1} (fun (j : Nat) => Nat) j) =>
@ite.{1} Nat (@HasLess.Less.{0} Nat instHasLessNat i (@OfNat.ofNat.{0} Nat 5 (instOfNatNat 5)))
(Nat.decLt i (@OfNat.ofNat.{0} Nat 5 (instOfNatNat 5))) (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))
(foo.match_1.{1} (fun (j : Nat) => @Nat.below.{1} (fun (j : Nat) => Nat) j → Nat) j
(fun (a : Unit) (x : @Nat.below.{1} (fun (j : Nat) => Nat) Nat.zero) =>
@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))
(fun (j : Nat) (x : @Nat.below.{1} (fun (j : Nat) => Nat) (Nat.succ j)) =>
@PProd.fst.{1, 1} ((fun (j : Nat) => Nat) j)
(@Nat.rec.{2} (fun (t : Nat) => Type) PUnit.{1}
(fun (n : Nat) (v_0 : Type) => PProd.{1, 1} (PProd.{1, 1} ((fun (j : Nat) => Nat) n) v_0) PUnit.{1}) j)
(@PProd.fst.{1, 1}
(PProd.{1, 1} ((fun (j : Nat) => Nat) j)
(@Nat.rec.{2} (fun (t : Nat) => Type) PUnit.{1}
(fun (n : Nat) (v_0 : Type) => PProd.{1, 1} (PProd.{1, 1} ((fun (j : Nat) => Nat) n) v_0) PUnit.{1})
j))
PUnit.{1} x))
f) := rfl -- failed


Last updated: May 18 2021 at 23:14 UTC