unknown identifier after it was introduced

Stream: lean4

[Jireh Loreaux]

Can someone explain why I'm getting this error in the last example? Clearly my metaprogramming skills are still horrendous.

import Std.Logic

open Lean Expr Meta

/-
Ensures that `goal` and `e` are proofs of some proposition.
If both have the form `∀ x : myType, _`, this should do, effectively, `refine forall_imp ?_ e`.
-/
def peelForall (goal : MVarId) (e : Expr) : MetaM (List MVarId) := do
  goal.withContext do
    let ty ← whnfR (← inferType e)
    let target ← whnfR (← goal.getType)
    -- check that everything is a `Prop`
    unless (← isProp ty) && (← isProp target) do
      dbg_trace s!"`peelForall` only works for propositions"
      return [goal]
    -- match `ty` and `target` as `∀` expressions.
    match ty, target with
      | .forallE n₁ t₁ b₁ c₁, .forallE _ t₂ b₂ _ => do
        dbg_trace s!"matched forall expressions"
        -- make sure they are quantified over the same type
        unless ← isDefEq (← whnfR t₁) (← whnfR t₂) do
          dbg_trace s!"forall statements don't have the same type"
          return [goal]
        withLocalDecl n₁ c₁ t₁ fun x => do
          let type₁ := b₁.instantiate1 x
          let type₂ := b₂.instantiate1 x
          -- apply `forall_imp` and return the resulting goal list.
          let all_imp ← mkFreshExprMVar (← mkForallFVars #[x] (← mkArrow type₁ type₂))
          goal.assign (← mkAppM ``forall_imp #[all_imp, e])
          return[all_imp.mvarId!]
      | _, _ => do
        -- if they aren't `forall` expressions, error.
        dbg_trace s!"couldn't match forall expressions"
        return [goal]

elab "peel" e:term : tactic => do
  let e ← Elab.Term.elabTerm e none
  Elab.Tactic.liftMetaTactic (peelForall · e)

example (p q : Nat → Prop) (h : ∀ y, p y) (h₁ : ∀ z, p z → q z) : ∀ x, q x := by
  peel h
  exact h₁
  done
  -- the above works as expected.

example (q : Nat → Prop) (r : Prop) (h : Nat → r) : ∀ x, q x := by
  peel h
  -- success
  sorry
  done

example (p q : Nat → Nat → Prop) (h : ∀ x y, p x y) (h₁ : ∀ w z, p w z → q w z) : ∀ i j, q i j := by
  refine forall_imp ?_ h
  intro n hp
  refine forall_imp ?_ hp
  -- this is what I expect to happen below, but it fails.
  sorry
  done
example (p q : Nat → Nat → Prop) (h : ∀ x y, p x y) (h₁ : ∀ w z, p w z → q w z) : ∀ i j, q i j := by
  peel h
  intro n hp
  peel hp -- unknown identifier `hp`
  -- what did I do wrong?
  sorry
  done

[Damiano Testa]

I wonder if you should embrace that e should be an ident and go via getId and finding the corresponding LocalDecl. It seems that newly introduced decls are ignored, even with the withContext. Anyway, I can't properly debug this now, sorry!

[Jireh Loreaux]

Well, it would be nice to supply a term as well, not just something from the local context, which is why I was taking this approach.

[Adam Topaz]

It's a context issue again, I think:

elab "peel" e:term : tactic => Elab.Tactic.withMainContext do
  let e ← Elab.Term.elabTerm e none
  Elab.Tactic.liftMetaTactic (peelForall · e)

[Jireh Loreaux]

Perfect, thanks!