Issue writing a tactic

Stream: metaprogramming / tactics

[Brendan Seamas Murphy]

I noticed that the inhabit tactic uses Classical.choice even if the goal is a Prop (I would think we can just use Nonempty.elim?). This seemed weird to me since the tactic already attempts to avoid classical reasoning if the target is a Prop. I noticed this because unique_iff_subsingleton_and_nonempty relies on Classical.choice, which doesn't seem necessary (I was checking this because I wanted to understand the principle of unique choice better). I tried to modify the tactic to avoid choice if the goal is a Prop, but I'm not very familiar with metaprogramming (especially in Lean 4) and now I'm getting the error "(kernel) declaration has metavariables 'unique_iff_subsingleton_and_nonempty'" when I try and define

theorem unique_iff_subsingleton_and_nonempty (α : Sort u) :
    Nonempty (Unique α) ↔ Subsingleton α ∧ Nonempty α :=
  ⟨fun ⟨u⟩ ↦ by constructor <;> exact inferInstance,
   fun ⟨hs, hn⟩ ↦ by inhabit α; constructor; exact Unique.mk' α⟩

My modified version of the inhabit tactic is

theorem nonempty_elim_to_inhabited
  (α : Sort*) (α_nonempty : Nonempty α) {p : Prop} (f : Inhabited α → p) : p :=
  α_nonempty.elim <| f ∘ Inhabited.mk

def evalInhabit (goal : MVarId) (h_name : Option Ident) (term : Syntax) : TacticM MVarId := do
  goal.withContext do
    let e ← Tactic.elabTerm term none
    let e_lvl ← Meta.getLevel e
    let inhabited_e := mkApp (mkConst ``Inhabited [e_lvl]) e
    let nonempty_e := mkApp (mkConst ``Nonempty [e_lvl]) e
    let nonempty_e_pf ← synthInstance nonempty_e
    let h_name : Name :=
      match h_name with
      | some h_name => h_name.getId
      | none => `inhabited_h
-- start of new code
    let e_isprop ← isProp e
    let g_type ← getMainTarget
    let g_isprop ← isProp g_type
    let inhab_imp_g_type := Expr.forallE `a inhabited_e g_type .default
    if g_isprop
    then do
      let n := `temp
      let pf ← mkFreshExprMVar inhab_imp_g_type MetavarKind.syntheticOpaque n
      let pf' ← Meta.mkAppM ``nonempty_elim_to_inhabited #[e, nonempty_e_pf, pf]
      let (_, r) ← (← goal.assert h_name inhabited_e pf').intro1P
      return r
    else
-- end of new code
      let pf ←
        if e_isprop
        then Meta.mkAppM ``nonempty_prop_to_inhabited #[e, nonempty_e_pf]
        else Meta.mkAppM ``nonempty_to_inhabited #[e, nonempty_e_pf]
      let (_, r) ← (← goal.assert h_name inhabited_e pf).intro1P
      return r

[Kevin Buzzard]

unique_iff_subsingleton_and_nonempty needs choice because subsingleton and nonempty live in the Prop universe, and unique lives in the Type universe, and the axiom of choice is precisely Lean's route from the Prop universe to the Type universe. Having looked at docs#unique_iff_subsingleton_and_nonempty I see that the unique part doesn't live in Type so my claim is incorrect!

[Timo Carlin-Burns]

But the left hand side of unique_iff_subsingleton_and_nonempty is Nonempty (Unique α) which does live in Prop

[Brendan Seamas Murphy]

For reference, here's a modified version of unique_iff_subsingleton_and_nonempty that doesn't depend on choice or the inhabit tactic

theorem unique_iff_subsingleton_and_nonempty (α : Sort u) :
    Nonempty (Unique α) ↔ Subsingleton α ∧ Nonempty α :=
    ⟨fun ⟨u⟩ ↦ by constructor <;> exact inferInstance,
   fun ⟨hs, hn⟩ ↦ by induction hn; constructor; apply uniqueOfSubsingleton; assumption⟩

[Kevin Buzzard]

yeah I've just proved it too. But why do you care about any of this? Mathlib is a classical library. I'm sure there are many uses of classical axioms which are unnecessary.

[Brendan Seamas Murphy]

Why does the inhabit tactic avoid using classical.choice at all?

[Kevin Buzzard]

I guess that's a question for whoever wrote that specific tactic?

[Brendan Seamas Murphy]

To answer your question directly, I wanted to work out some stuff about anafunctors without rebuilding a ton of basic definitions of category theory. Afaict apart from the choices of limits/colimits or choosing an inverse to an equivalence, most of the category theory implemented in mathlib already doesn't rely on classical reasoning. Reimplementing all that would be a pain and I would prefer to work with an existing codebase