cases on nested pattern match

Stream: Is there code for X?

[Paige Thomas]

Is there a tactic that will split the cases on a nested match? I can't seem to split this:

⊢ is_equation_list_unifier
  ((match unify (equation_list_replace_var_one_rec X rhs tl) with
      | none => none
      | some τ => some (Function.updateITE τ X (replace_var_all_rec τ rhs))).get
    ⋯)
  ({ lhs := var_ X, rhs := rhs } :: tl)

[Aaron Liu]

the tactic is called split

[Aaron Liu]

sometimes it fails though

[Paige Thomas]

yeah, it is failing on this.

[Paige Thomas]

Is there a way to work around this, or do I need to set something up differently? I'm doing a proof by induction on

def unify :
  List Equation → Option (String → Formula_)
  | [] => Option.some var_
  | ⟨false_, false_⟩ :: Γ
  | ⟨true_, true_⟩ :: Γ => unify Γ
  | ⟨var_ X, F⟩ :: Γ
  | ⟨F, var_ X⟩ :: Γ =>
    if var_ X = F
    then unify Γ
    else
      if var_occurs_in_formula X F
      then Option.none
      else
        match unify (equation_list_replace_var_one_rec X F Γ) with
        | Option.none => Option.none
        | Option.some τ => Option.some (Function.updateITE τ X (replace_var_all_rec τ F))
  | ⟨not_ phi, not_ phi'⟩ :: Γ =>
      unify (⟨phi, phi'⟩ :: Γ)
  | ⟨and_ phi psi, and_ phi' psi'⟩ :: Γ
  | ⟨or_ phi psi, or_ phi' psi'⟩ :: Γ
  | ⟨imp_ phi psi, imp_ phi' psi'⟩ :: Γ
  | ⟨iff_ phi psi, iff_ phi' psi'⟩ :: Γ =>
      unify (⟨phi, phi'⟩ :: ⟨psi, psi'⟩ :: Γ)
  | _ => Option.none

[Aaron Liu]

have you considered docs#Option.map

[Paige Thomas]

No, I'll give it a try.

[Paige Thomas]

That, along with Option.get_map worked. Thank you.