intro with type specified

Stream: lean4

[Dan Velleman]

Consider this example:

import Mathlib
example (U : Type) (A B : Set U) : A ⊆ B → A ∩ B = A := by
  intro h

After intro h, I have h : A ⊆ B in the tactic state. But now suppose I change the example to this:

import Mathlib
example (U : Type) (A B : Set U) : A ⊆ B → A ∩ B = A := by
  intro (h : A ⊆ B)

Now I get an error message: type mismatch h has type A ⊆ B : Prop but is expected to have type ?m.49 ∈ A → ?m.49 ∈ B : Prop. Why? Shouldn't this work?

[Floris van Doorn]

The definition of Set.subset is
∀ {a}, a ∈ s₁ → a ∈ s₂
and so it seems like Lean interprets h as @h _.
This looks like a bug in intro (since h should not be applied to implicit arguments).

[Dan Velleman]

That's what I thought. Any idea how to fix it?

[Floris van Doorn]

If you don't specify the type, it will work:

example (U : Type) (A B : Set U) : A ⊆ B → A = A := by
  intro h

[Floris van Doorn]

Opened a (minimized) issue as leanprover/lean4#1759

[Dan Velleman]

Yes, I know. But I'm supposed to be able to specify the type, right?

I am trying to implement an assume tactic, for use by students. My tactic is essentially just a wrapper around intro. I want to encourage students to say explicitly what statement is being assumed, so that Lean can correct them if they are assuming the wrong thing. So I need to be able to pass the type to intro and have it make sure it's the right type. So this bug, if it is a bug, is a problem for me.

[Leonardo de Moura]

Pushed a fix for the issue above.

[Dan Velleman]

Thanks!

[Dan Velleman]

I'm a little puzzled by the following examples:

import Mathlib.Data.Set.Basic
attribute [default_instance] Set.instSingletonSet

example (x y : Nat) : y ∈ {x} → y = x := by
  intro h
  exact h
  done

example (x y : Nat) : y ∈ {x} → y = x := by
  intro (h : y ∈ {x})
  exact h
  done

example (x y : Nat) : y ∈ {x} → y = x := by
  intro (h : y ∈ ({x} : Set Nat))
  exact h
  done

The first and third examples work, but the second doesn't. The error message is

type mismatch at `intro h`has type
  y ∈ {x} : Prop
but is expected to have type
  y ∈ ?m.387 : Prop

If I don't include the line attribute [default_instance] Set.instSingletonSet, then Lean doesn't understand the example at all. I assume the problem is that the notation {x} becomes ambiguous because it could have several different types. With the line attribute [default_instance] Set.instSingletonSet, Lean interprets {x} in the statement of the example as denoting a singleton set. But it doesn't seem to understand it that way in intro. Is the default_instance specification ignored by intro?

[Eric Wieser]

Weirdly intro (h : y ∈ singleton x) works fine too

[Kyle Miller]

When I was implementing change ... at I noticed these sorts of unification errors occurring. I don't fully understand them, but I did find a workaround by using the show elaborator. I'll just leave this working implementation of intro with type ascriptions here in case anyone has any ideas (note that it works without the default instance as well, after suitably modifying the theorem statements):

import Lean
import Mathlib.Data.Set.Basic

open Lean Elab Elab.Tactic Meta

def introType (n : Name) (typeStx : TSyntax `term) : TacticM Unit := do
    let fvarId ← liftMetaTacticAux fun mvarId => do
      let (fvarId, mvarId) ← mvarId.intro n
      pure (fvarId, [mvarId])
    withMainContext do
      let fvarType ← fvarId.getType
      let mvar ← mkFreshExprMVar none
      _ ← Term.withSynthesize <|
            elabTerm (← `(term | show $typeStx from $(← Term.exprToSyntax mvar))) fvarType
      let type ← inferType mvar
      liftMetaTactic fun mvarId => return [← mvarId.replaceLocalDeclDefEq fvarId type]

syntax "my_intro" "(" ident " : " term ")" : tactic

elab_rules : tactic
  | `(tactic| my_intro ($h:ident : $type:term)) => introType h.getId type


attribute [default_instance] Set.instSingletonSet

example (x y : Nat) : y ∈ {x} → y = x := by
  my_intro (h : _)
  exact h
  done

example (x y : Nat) : y ∈ {x} → y = x := by
  my_intro (h : y ∈ {x})
  exact h
  done

example (x y : Nat) : y ∈ ({x} : Set Nat) → y = x := by
  my_intro (h : y ∈ ({x} : Set Nat))
  exact h
  done

[Dan Velleman]

Thanks @Kyle Miller for your suggestion.

Here's another idea: Do the same thing that evalIntro does for the pattern-matching case:

elab_rules : tactic
  | `tactic| my_intro ($h:ident : $type:term)) =>
    evalTactic (← `(tactic| intro h; match @h with | ($h : $type) => ?_; try clear h))

I'm not sure I entirely understand what's going on here, but it seems to work. Is there any possibility of the h in the intro h step conflicting with some other name? Is the try necessary?

[Patrick Massot]

I know this is an old thread but I have a new question about the same topic. The context of this question is this comment where a user laments that you cannot put type ascriptions in intros. I was about to answer that you can, but I decided to check just in case. Weirdly, you can with intro, thanks to those lines but not with intros (whose code is a few lines down). Is it intentional? In the spirit of getting rid of the plural versions universes and variables, wouldn't it make to get rid of intros? Or is it meant to have a really different meaning?

[Eric Wieser]

I guess the key difference is that intros intros all the binders but intro intros just one? Maybe intro .. could be the spelling for "intro everything", to match exact foo .. to use everything; which lets us eliminate intros.

[Patrick Massot]

By the way, the previous messages in this thread are also interesting and seem to be still relevant.

[Patrick Massot]

Eric, you can intro many things with intro.

[Patrick Massot]

But indeed if you don't specify any name then intro will intro only one, and intros will intro everything. But this isn't very useful since you get inaccessible names.

[Jireh Loreaux]

the intro .. spelling or intro a b c .. seems nice.

[Eric Wieser]

Sure, my point was that if we're going to combine the two commands into one (which I agree is a good idea), then we need to disambiguate intro from intros when they have no arguments, either by changing the spelling of one, or dropping one entirely

[Eric Wieser]

I guess even intro a .. b c could be legal

[Eric Rodriguez]

what is the exact .. syntax? I see it's used a couple times in mathlib

[Eric Wieser]

f .. means f _ _ _ for suitably many _