mutate subgoal environment

Stream: lean4

[Enrico Borba]

I'm in the middle of a tactic proof that looks like this:

match s with
| .or =>
  have hff₁₂ : ∀ b, f b = Bool.or (f₁ b) (f₂ b) := sorry
  simp only [Model.value, Interpretation.fns]
  conv at ih₁ => lhs; simp only [Dual.dual]
  conv at ih₂ => lhs; simp only [Dual.dual]
  rw [ih₁, ih₂]
  simp only [Dual.dual, Signature.Formula.function]
  rw [(by rfl : ~w.vec = (~w).vec), hf₁ (~w), hf₂ (~w), hff₁₂]
  simp only [Bool.not_or, Bool.not_and]

| .and =>
  have hff₁₂ : ∀ b, f b = Bool.and (f₁ b) (f₂ b) := sorry
  simp only [Model.value, Interpretation.fns]
  conv at ih₁ => lhs; simp only [Dual.dual]
  conv at ih₂ => lhs; simp only [Dual.dual]
  rw [ih₁, ih₂]
  simp only [Dual.dual, Signature.Formula.function]
  rw [(by rfl : ~w.vec = (~w).vec), hf₁ (~w), hf₂ (~w), hff₁₂]
  simp only [Bool.not_or, Bool.not_and]

Notice the proofs in each of the two arms are the same except for the first line. This first line in each arm introduces a new term into each of the arms' environments. Is there a way to do this and then "return" to the top level? I'm imagining some code like this:

match s with
| .or => have hff₁₂ : ∀ b, f b = Bool.or (f₁ b) (f₂ b) := sorry
| .and => have hff₁₂ : ∀ b, f b = Bool.and (f₁ b) (f₂ b) := sorry

/-
  The two cases `and` and `or` would then return to being subgoals as they
  are not resolved(?) yet.
-/

all_goals {
  simp only [Model.value, Interpretation.fns]
  conv at ih₁ => lhs; simp only [Dual.dual]
  conv at ih₂ => lhs; simp only [Dual.dual]
  rw [ih₁, ih₂]
  simp only [Dual.dual, Signature.Formula.function]
  rw [(by rfl : ~w.vec = (~w).vec), hf₁ (~w), hf₂ (~w), hff₁₂]
  simp only [Bool.not_or, Bool.not_and]
}

[Joachim Breitner]

May not apply in your case, but if the goals are the same after these lines(not just the tactics), and it's not too bad to spell it out, you can manually have the goal before the case, and then use assumption in the cases.

[Kyle Miller]

Or, rather than using match, you could use cases followed by case' blocks.

Maybe something like this:

cases s
case' or =>
  have hff₁₂ : ∀ b, f b = Bool.or (f₁ b) (f₂ b) := sorry
case' and =>
  have hff₁₂ : ∀ b, f b = Bool.and (f₁ b) (f₂ b) := sorry
all_goals
  simp only [Model.value, Interpretation.fns]
  conv at ih₁ => lhs; simp only [Dual.dual]
  conv at ih₂ => lhs; simp only [Dual.dual]
  rw [ih₁, ih₂]
  simp only [Dual.dual, Signature.Formula.function]
  rw [(by rfl : ~w.vec = (~w).vec), hf₁ (~w), hf₂ (~w), hff₁₂]
  simp only [Bool.not_or, Bool.not_and]

[Kyle Miller]

If you're using match for recursion, maybe you could use induction instead of cases. You might also be able to set up using some named metavariables in conjunction with refine match s with ... and do something like this case' option.

[Enrico Borba]

oh does case' not fail if the sub goals aren't resolved?

[Kyle Miller]

Yes. Here's its docstring:

case' is similar to the case tag => tac tactic, but does not ensure the goal has been solved after applying tac, nor admits the goal if tac failed. Recall that case closes the goal using sorry when tac fails, and the tactic execution is not interrupted.

[Enrico Borba]

Sweet, that's basically what I was looking for. Thanks!