Expr.isProp not picking up a Prop

Stream: lean4

[Heather Macbeth]

I'm trying to get a list of the Prop hypotheses in context. I tried this, but it misses some:

import Lean.Elab.Tactic.Basic

open Lean Meta Elab Tactic

elab "test_tactic" : tactic => withMainContext do
  liftMetaTactic <| fun g => do
  -- collect the nontrivial hypotheses
  let mut hyps : Array Expr := #[]
  for h in ← getLCtx do
    if !h.isImplementationDetail then
      hyps := hyps.push h.type
  -- find their types
  let hyp_types ← hyps.mapM (fun a => do pure (←whnfR (← inferType a)))
  trace `debug (fun _ => m!"found hypotheses {hyps} of types {hyp_types}")
  -- run `Expr.isProp`
  trace `debug (fun _ => m!"These ones are Props according to Expr.isProp: {hyp_types.map Expr.isProp}")
  pure [g]

[Heather Macbeth]

For example, here it finds h but not h':

set_option trace.debug true

example (h : P ∧ Q) : P ∨ Q := by
  refine Classical.byContradiction fun h' => ?_
  test_tactic
  sorry
/-
[debug] found hypotheses [Prop, Prop, P ∧ Q, ¬(P ∨ Q)] of types [Type, Type, Prop, Prop]

[debug] These ones are Props according to Expr.isProp: [false, false, true, false]
-/

[Eric Wieser]

instantiateMVars fixes it

[Eric Wieser]

elab "test_tactic" : tactic => withMainContext do
  liftMetaTactic <| fun g => do
  -- collect the nontrivial hypotheses
  let mut hyps : Array Expr := #[]
  for h in ← getLCtx do
    if !h.isImplementationDetail then
      hyps := hyps.push h.type
  -- find their types
  let hyp_types ← hyps.mapM (fun a => return (←instantiateMVars (←whnfR (← inferType a))))
  trace[debug] "found hypotheses {hyps} of types {hyp_types}"
  -- run `Expr.isProp`
  trace[debug]  "These ones are Props according to Expr.isProp: {hyp_types.map Expr.isProp}"
  pure [g]

[Heather Macbeth]

Thanks! Is there a preferred order, instantiateMVars before or after whnfR?

[Eric Wieser]

That is definitely beyond my paygrade!

[Eric Wieser]

My preferred approach would be through Qq:

open Qq
elab "test_tactic" : tactic => withMainContext do
  liftMetaTactic <| fun g => do
  -- collect the nontrivial hypotheses
  let mut hyps : Array Expr := #[]
  for h in ← getLCtx do
    if !h.isImplementationDetail then
      hyps := hyps.push h.type
  -- find their types
  let hyp_props : Array (Option Q(Prop)) ← hyps.mapM (fun a => do
    let a ← instantiateMVars a
    if let ⟨1, ~q(Prop), P⟩ := ← inferTypeQ a then
      pure (some P)
    else pure none)
  trace[debug] "Found props: {hyp_props}"
  pure [g]

[Eric Wieser]

Which I guess forced my hand into calling instantiateMVars before

[Eric Wieser]

(note that this let matching on inferTypeQ was broken until a month ago, so this pattern isn't very common yet)

[Kyle Miller]

If you're doing whnf, you don't need instantiateMVars before but you do need it after.

[Kyle Miller]

docs#Lean.Meta.isProp is the function that handles everything for you

[Kyle Miller]

My rule of thumb is "be suspicious about matching/recognition functions from Lean.Expr, and try to look for a Lean.Meta version that handles whnf and metavariables for you". There's not a perfect correspondence between these namespaces unfortunately.

[Eric Wieser]

This sounds like a great use-case for docstrings on the Expr versions that recommend the Meta versions where possible