Associate value with goal

Stream: lean4

[Marcus Rossel]

I sometimes run into the situation that I have multiple subgoals that can all be solved the same way, except that they require a single different value in an application of a lemma or something.
As an example consider the following (non-mwe) real world example:

theorem ...
  ...
  refine ⟨?ports, ?state, ?reactions, ?reactors⟩ -- Splits an (_ ∧ _ ∧ _ ∧ _) into four subgoals

  -- Uses Cmp.prt
  case ports =>
    apply objFor_ext Cmp.prt
    intro j o
    byCases h : Cmp.prt = cmp
    case inl =>
      subst h
      byCases h' : j = i
      case inl =>
        simp [←h'] at ht₁ ht₂
        byCases h'' : o = v
        case inl => simp [h'', iff_of_true ht₁ ht₂]
        case inr =>
          exact Iff.intro
            (λ h => False.elim $ (not_and_self_iff _).mp ⟨h'', objFor_unique_obj h ht₁⟩)
            (λ h => False.elim $ (not_and_self_iff _).mp ⟨h'', objFor_unique_obj h ht₂⟩)
      case inr => simp [←(hi₁ j h'), hi₂ j h']
    case inr => simp [←(hc₁ Cmp.prt h), hc₂ Cmp.prt h]

  -- Uses Cmp.stv
  case state =>
    apply objFor_ext Cmp.stv
    intro j o
    byCases h : Cmp.stv = cmp
    case inl =>
      subst h
      byCases h' : j = i
      case inl =>
        simp [←h'] at ht₁ ht₂
        byCases h'' : o = v
        case inl => simp [h'', iff_of_true ht₁ ht₂]
        case inr =>
          exact Iff.intro
            (λ h => False.elim $ (not_and_self_iff _).mp ⟨h'', objFor_unique_obj h ht₁⟩)
            (λ h => False.elim $ (not_and_self_iff _).mp ⟨h'', objFor_unique_obj h ht₂⟩)
      case inr => simp [←(hi₁ j h'), hi₂ j h']
    case inr => simp [←(hc₁ Cmp.stv h), hc₂ Cmp.stv h]

  -- Uses Cmp.rcn
  case reactions =>
    apply objFor_ext Cmp.rcn
    intro j o
    byCases h : Cmp.rcn = cmp
    case inl =>
      subst h
      byCases h' : j = i
      case inl =>
        simp [←h'] at ht₁ ht₂
        byCases h'' : o = v
        case inl => simp [h'', iff_of_true ht₁ ht₂]
        case inr =>
          exact Iff.intro
            (λ h => False.elim $ (not_and_self_iff _).mp ⟨h'', objFor_unique_obj h ht₁⟩)
            (λ h => False.elim $ (not_and_self_iff _).mp ⟨h'', objFor_unique_obj h ht₂⟩)
      case inr => simp [←(hi₁ j h'), hi₂ j h']
    case inr => simp [←(hc₁ Cmp.rcn h), hc₂ Cmp.rcn h]

  -- Uses Cmp.rtr
  case reactors =>
    apply objFor_ext Cmp.rtr
    intro j o
    byCases h : Cmp.rtr = cmp
    case inl =>
      subst h
      byCases h' : j = i
      case inl =>
        simp [←h'] at ht₁ ht₂
        byCases h'' : o = v
        case inl => simp [h'', iff_of_true ht₁ ht₂]
        case inr =>
          exact Iff.intro
            (λ h => False.elim $ (not_and_self_iff _).mp ⟨h'', objFor_unique_obj h ht₁⟩)
            (λ h => False.elim $ (not_and_self_iff _).mp ⟨h'', objFor_unique_obj h ht₂⟩)
      case inr => simp [←(hi₁ j h'), hi₂ j h']
    case inr => simp [←(hc₁ Cmp.rtr h), hc₂ Cmp.rtr h]

Each of the four subgoals is identical in how it's solved, the only difference being each goal uses a different type of Cmp (Cmp.prt, Cmp.stv, Cmp.rcn and Cmp.rtr).

Is there some way to associate such a value with a goal?
Something like saying for c in #[Cmp.prt. Cmp.stv, Cmp.rcn, Cmp.rtr] { solve the goal using c }.

[Mario Carneiro]

It would be pretty easy to do that using runTac, or you can make a local macro tactic

[Mario Carneiro]

although, you should really consider making a lemma for that, since it looks like most of it doesn't actually depend on the choice of constructor

[Mario Carneiro]

like this:

local macro "foo" e:term : tactic => `((
  apply objFor_ext $e
  intro j o
  byCases h : $e = cmp
  case inl =>
    subst h
    byCases h' : j = i
    case inl =>
      simp [←h'] at ht₁ ht₂
      byCases h'' : o = v
      case inl => simp [h'', iff_of_true ht₁ ht₂]
      case inr =>
        exact Iff.intro
          (λ h => False.elim $ (not_and_self_iff _).mp ⟨h'', objFor_unique_obj h ht₁⟩)
          (λ h => False.elim $ (not_and_self_iff _).mp ⟨h'', objFor_unique_obj h ht₂⟩)
    case inr => simp [←(hi₁ j h'), hi₂ j h']
  case inr => simp [←(hc₁ $e h), hc₂ $e h]))