parallel combinator

Stream: new members

[Olli]

is there a way to use the exact tactic with the parallel tactic combinator:

works:

example : p ∧ q ↔ q ∧ p :=
begin
  split,
  exact λ ⟨h1, h2⟩, ⟨h2, h1⟩,
  exact λ ⟨h1, h2⟩, ⟨h2, h1⟩,
end

fails:

example : p ∧ q ↔ q ∧ p :=
begin
  split;
  exact λ ⟨h1, h2⟩, ⟨h2, h1⟩,
end

with:

equation compiler failed to create auxiliary declaration '_example._match_1'
nested exception message:
invalid object declaration, environment already has an object named '_example._match_1'

[Kenny Lau]

does rintro work?

[Ali Sever]

This also works,

example : p ∧ q ↔ q ∧ p :=
begin
  split;
  exact and.symm
end

[Mario Carneiro]

@Sebastian Ullrich This seems to be indicative of a very strange dependency between parsing and creating definitions. Does this still behave the same way in lean 4?

[Mario Carneiro]

Oh wow, this is stranger than I thought.

open tactic

meta def mytac : tactic unit :=
do tgt ← target,
   i_to_expr_strict ``(λ ⟨h1, h2⟩, ⟨h2, h1⟩ : %%tgt) >>= exact

meta def twice (tac : tactic unit) : tactic unit := tac >> tac

example {p q : Prop} : p ∧ q ↔ q ∧ p := -- doesn't work
begin
  split,
  twice (do {
    tgt ← target,
    i_to_expr_strict ``(λ ⟨h1, h2⟩, ⟨h2, h1⟩ : %%tgt) >>= exact
  })
end

example {p q : Prop} : p ∧ q ↔ q ∧ p := -- works
begin
  split,
  do {
    tgt ← target,
    i_to_expr_strict ``(λ ⟨h1, h2⟩, ⟨h2, h1⟩ : %%tgt) >>= exact,
    tgt ← target,
    i_to_expr_strict ``(λ ⟨h1, h2⟩, ⟨h2, h1⟩ : %%tgt) >>= exact
  }
end

example {p q : Prop} : p ∧ q ↔ q ∧ p := -- works
begin
  split,
  twice mytac
end

My new theory is that it has something to do with the way a tactic is elaborated when it contains a subexpression with side effects like this

[Sebastian Ullrich]

Yeah, to_expr is creating a new elaborator. This is horrible, haha

[Sebastian Ullrich]

Well, I guess it could just skip auxiliary names that have already been taken