Iff tactic

Stream: mathlib4

[Antoine Chambert-Loir]

Is there a tactic which, for a theorem that states PiffQ : ∀ (x : …) (y : …), P x y \iff Q x y, reduces it to the proof of one implication, say PtoQ : ∀ (x : …) (y : …), P x y \to Q x y, and for the converse implication adds the hypothesis PtoQ?

[Michael]

Iff.intro?

[Yaël Dillies]

https://leanprover-community.github.io/mathlib4_docs/Std/Logic.html#forall%E2%82%82_congr

[Yaël Dillies]

docs#forall₂_congr sadly breaks the linkifier still

[Yaël Dillies]

Ah sorry, I misread

[Emilie (Shad Amethyst)]

What about docs#forall%E2%82%82_congr ?
Nevermind

[Michael]

Is that what he wants? It looks like the goal is

$$\forall x, y \left( p(x,y) \leftrightarrow q(x,y) \right)$$

and he wants to split it into two goals

$$\forall x, y \left( p(x,y) \to q(x,y) \right) \\ \forall x, y \left( q(x,y) \to p(x,y) \right)$$

[Emilie (Shad Amethyst)]

Well, not quite, in the second goal, they would like to have access to what they proved beforehand

[Michael]

I thought that was automatic; once you've proved one subgoal, is it not available?

[Emilie (Shad Amethyst)]

The way I've been solving this issue so far was to use suffices; the forward direction can then be proven separately, and the backward direction can be proven inside of the by:

example : ∀ (x: …) (y : …), P x y ↔ Q x y := by
  suffices ∀ (x : …) (y : …), P x y → Q x y by
    refine fun x y => ⟨this x y, ?rev_imp⟩
    -- Prove Q x y → P x y here, with `this` available for `P x y → Q x y`
  -- Prove P x y → Q x y

[Emilie (Shad Amethyst)]

Usually though in Mathlib there are enough theorems to transform P x y into Q x y with exclusively rw, or the step that is hard to prove is isolated enough. From a quick ripgrep search, I can see that this is what's done in docs#star_le_star_iff or in docs#Ideal.subset_union_prime'

[Antoine Chambert-Loir]

Yes, I also do it this way, see https://github.com/leanprover-community/mathlib4/blob/02eb46065af4d2a0e05ac81b5df631e43fd45840/Mathlib/GroupTheory/Perm/Cycle/Basic.lean#L1534 but I wondered whether a clean tactic could help.

[Emilie (Shad Amethyst)]

It would certainly help me too, especially when making atomical theorems isn't currently a priority

[Eric Wieser]

How about this?

example (P Q : Prop) : P ↔ Q := by
  refine ⟨?h, ?_⟩
  · sorry
  · have := ?h
    sorry

[Damiano Testa]

I find Eric's suggestion very clean and a great use of ?h!

Before this syntax was available, I think that quite a few of the situations where this was an issue, resolved in proving the implication ∀ (x : …) (y : …), P x y -> Q x y with weaker assumptions, so that it became just an implication, and the converse only followed with stronger assumptions. Once you have the separate, more general lemma, you can use it in the two branches, of course.

[Damiano Testa]

(This only works if you can find such a weakening, naturally.)

[Eric Wieser]

I can't get the ?h syntax to work if you need the quantification

[Michael]

Eric Wieser said:

I can't get the ?h syntax to work if you need the quantification

The quantification is around the $\leftrightarrow$, so will stripping it work?

example (α : Type) (β : Type) (p q : α → β → Prop) :
    ∀ x : α, ∀ y : β, p x y ↔ q x y := by
  intro x y
  -- special strategies

[Michael]

I guess not, when I fill in from your example, I see failed to infer 'let' declaration type.
Not sure what was wrong, but it does appear to work:

example (α : Type) (β : Type) (p q : α → β → Prop) :
    ∀ x : α, ∀ y : β, p x y ↔ q x y := by
  intro x y
  -- special strategies
  refine ⟨?hmp, ?hmpr⟩
  sorry
  have h := ?hmp
  sorry

But this only preserves p x y → q x y for the particular arbitrary x and y that are introduced.

[Eric Wieser]

Yes, that was my point, sorry for not being clearer; the quantification is absent from the extracted goal

[Michael]

the trick still works if you provide your own theorem:

theorem univ_iff {α : Type} {β : Type} {p q : α → β → Prop} :
    (∀ x : α, ∀ y : β, p x y ↔ q x y) ↔
      (∀ x : α, ∀ y : β, p x y → q x y) ∧
      (∀ x : α, ∀ y : β, q x y → p x y) := by
  sorry

example (α : Type) (β : Type) (p q : α → β → Prop) :
    ∀ x : α, ∀ y : β, p x y ↔ q x y := by
  rw [univ_iff]
  refine ⟨?hmp, ?hmpr⟩
  sorry
  have h := ?hmp
  sorry

[Michael]

This doesn't work:

example (α : Type) (β : Type) (p q : α → β → Prop) :
    ∀ x : α, ∀ y : β, p x y ↔ q x y := by
  rw [univ_iff]
  refine ⟨?hmp, ?hmpr⟩
  case hmp => sorry
  have h := ?hmp
  sorry

I'd really like to know what the deep difference is between solving case hmp implicitly, because it's the first one in the default sequence, and solving it explicitly by calling it case hmp.

[Eric Wieser]

simp_rw [iff_iff_implies_and_implies, forall_and] removes the need for univ_iff

[Antoine Chambert-Loir]

I should have been clearer: in my application case, I need to retain the forall quantification, because the reverse implication is obtained by applying the forward one to other elements than the obvious ones.

[Eric Wieser]

I think this is a niche enough case that either using suffices or writing a standalone lemma for the implication is a reasonable choice.

[Eric Wieser]

(As @Damiano Testa comments, it is very common that the implication is true more generally. Even cases where it isn't, the implication is often handy to have for dot notation)

[Kyle Miller]

I just made a prototype of a constructor! generalizing x y tactic. It looks like this:

example (P Q : Nat → Int → Prop) : ∀ x y, P x y ↔ Q x y := by
  intros x y
  constructor! generalizing x y
  /-
  case mp
  P Q : ℕ → ℤ → Prop
  x : ℕ
  y : ℤ
  ⊢ P x y → Q x y

  case mpr
  P Q : ℕ → ℤ → Prop
  h✝ : ∀ (x : ℕ) (y : ℤ), P x y → Q x y
  x : ℕ
  y : ℤ
  ⊢ Q x y → P x y
  -/

[Kyle Miller]

code v1

import Mathlib

section
open Lean Elab Tactic

elab "constructor!" genArg?:(Mathlib.Tactic.generalizingClause)? : tactic => do
  withMainContext do
    let gens ←
      match genArg? with
      | none => pure #[]
      | some genArg =>
        match genArg with
        | `(Mathlib.Tactic.generalizingClause| generalizing $args*) => getFVarIds args
        | _ => pure #[]
    liftMetaTactic fun g => do
      let gs ← g.constructor (cfg := {newGoals := .all, allowSynthFailures := true})
      let gs ← gs.toArray.mapM (fun g => g.revert gens)
      -- Now, theoretically, each goal has the same local context,
      -- so we can feed them into each other as additional hypotheses.
      -- This is sort of a hack, and it yields quadratically large proof terms.
      let mut gs' := #[]
      for i in [0:gs.size] do
        let (fvars, g) := gs[i]!
        let mut g' := g
        for j in [0:i] do
          let gj := gs[j]!.2
          g' ← g.assert `h (← gj.getType) (.mvar gj)
          g' ← Prod.snd <$> g'.intro1
        g' ← Prod.snd <$> g'.introNP fvars.size
        gs' := gs'.push g'
      return gs'.toList

end

example (P Q : Nat → Int → Prop) : ∀ x y, P x y ↔ Q x y := by
  intros x y
  constructor! generalizing x y
  /-
  case mp
  P Q : ℕ → ℤ → Prop
  x : ℕ
  y : ℤ
  ⊢ P x y → Q x y

  case mpr
  P Q : ℕ → ℤ → Prop
  h✝ : ∀ (x : ℕ) (y : ℤ), P x y → Q x y
  x : ℕ
  y : ℤ
  ⊢ Q x y → P x y
  -/

[Kyle Miller]

A nice extension to this would be a with clause to name the hypotheses for successive goals. It also is missing code to link up variables for the unused variable checker (see how docs#Lean.MVarId.withReverted uses pushInfoLeaf)

[Kyle Miller]

Here's an extension that handles @Antoine Chambert-Loir's original case.

It will auto-intro, apply constructors, and revert:

example (P Q : Nat → Int → Prop) : ∀ x y, P x y ↔ Q x y := by
  constructor!
  /-
  case mp
  P Q : ℕ → ℤ → Prop
  ⊢ ∀ (x : ℕ) (y : ℤ), P x y → Q x y

  case mpr
  P Q : ℕ → ℤ → Prop
  h✝: ∀ (x : ℕ) (y : ℤ), P x y → Q x y
  ⊢ ∀ (x : ℕ) (y : ℤ), Q x y → P x y
  -/

It also interacts with this generalizing clause:

example (P Q : Nat → Int → Prop) : ∀ x y, P x y ↔ Q x y := by
  intro x
  constructor! generalizing x
  /-
  case mp
  P Q : ℕ → ℤ → Prop
  x : ℕ
  ⊢ ∀ (y : ℤ), P x y → Q x y

  case mpr
  P Q : ℕ → ℤ → Prop
  h✝: ∀ (x : ℕ) (y : ℤ), P x y → Q x y
  x : ℕ
  ⊢ ∀ (y : ℤ), Q x y → P x y
  -/

[Kyle Miller]

code v2

import Mathlib

section
open Lean Elab Tactic

elab "constructor!" genArg?:(Mathlib.Tactic.generalizingClause)? : tactic => do
  withMainContext do
    let gens ←
      match genArg? with
      | none => pure #[]
      | some genArg =>
        match genArg with
        | `(Mathlib.Tactic.generalizingClause| generalizing $args*) => getFVarIds args
        | _ => pure #[]
    liftMetaTactic fun g => do
      let (fvars, g) ← g.intros
      let gs ← g.constructor (cfg := {newGoals := .all, allowSynthFailures := true})
      let gs ← gs.toArray.mapM (fun g => Prod.snd <$> g.revert fvars)
      let gs ← gs.mapM (fun g => g.revert gens)
      -- Now, theoretically, each goal has the same local context,
      -- so we can feed them into each other as additional hypotheses.
      -- This is sort of a hack, and it yields quadratically large proof terms.
      let mut gs' := #[]
      for i in [0:gs.size] do
        let (rfvars, g) := gs[i]!
        let mut g' := g
        for j in [0:i] do
          let gj := gs[j]!.2
          g' ← g.assert `h (← gj.getType) (.mvar gj)
          g' ← Prod.snd <$> g'.intro1
        g' ← Prod.snd <$> g'.introNP rfvars.size
        gs' := gs'.push g'
      return gs'.toList

end

example (P Q : Nat → Int → Prop) : ∀ x y, P x y ↔ Q x y := by
  constructor!
  /-
  case mp
  P Q : ℕ → ℤ → Prop
  ⊢ ∀ (x : ℕ) (y : ℤ), P x y → Q x y

  case mpr
  P Q : ℕ → ℤ → Prop
  h✝: ∀ (x : ℕ) (y : ℤ), P x y → Q x y
  ⊢ ∀ (x : ℕ) (y : ℤ), Q x y → P x y
  -/

example (P Q : Nat → Int → Prop) : ∀ x y, P x y ↔ Q x y := by
  intro x
  constructor!
  /-
  case mp
  P Q : ℕ → ℤ → Prop
  x : ℕ
  ⊢ ∀ (y : ℤ), P x y → Q x y

  case mpr
  P Q : ℕ → ℤ → Prop
  x : ℕ
  h✝: ∀ (y : ℤ), P x y → Q x y
  ⊢ ∀ (y : ℤ), Q x y → P x y
  -/

example (P Q : Nat → Int → Prop) : ∀ x y, P x y ↔ Q x y := by
  intro x
  constructor! generalizing x
  /-
  case mp
  P Q : ℕ → ℤ → Prop
  x : ℕ
  ⊢ ∀ (y : ℤ), P x y → Q x y

  case mpr
  P Q : ℕ → ℤ → Prop
  h✝: ∀ (x : ℕ) (y : ℤ), P x y → Q x y
  x : ℕ
  ⊢ ∀ (y : ℤ), Q x y → P x y
  -/

[Yaël Dillies]

What's the ! in the name referring to?

[Jireh Loreaux]

It means "Lean, try hard to construct it!" :laughing:

[Kyle Miller]

Yeah, and it's constructor with bells and whistles, which tend to be loud!