MWE for Pattern Matching Timeout

mwe.lean

import data.pnat.basic

structure resultAt (x : list ℕ) : Type :=
(f : fin x.length → option ℕ+)
(g : fin x.length → option ℕ)
(g_to_fin :
  Π {i : fin x.length} (h : (g i).is_some),
    {k : fin x.length // k.val = @option.get _ (g i) h})
(f_is_some_of_g_is_some :
  ∀ {i : fin x.length}, (g i).is_some → (f i).is_some)
(f_comp_g_is_some_of_g_is_some :
  ∀ {i : fin x.length} (h : (g i).is_some), (f (@g_to_fin i h)).is_some)
(f_comp_g_lt_f :
  ∀ {i : fin x.length} (h : (g i).is_some),
    @option.get _ (f (@g_to_fin i h)) (f_comp_g_is_some_of_g_is_some h) <
    @option.get _ (f i)                      (f_is_some_of_g_is_some h))

-- Works fine (even before stripping out the details and even some fields)
def recursive_function_rec (x : list ℕ) : ℕ → resultAt x :=
@nat.rec (λ _, resultAt x) sorry (λ j prev,
  let f : fin x.length → option ℕ+ := λ i,
      dite (prev.g i).is_some
        (assume h, some
          ⟨@option.get _ (prev.f i) sorry -
            @option.get _ (prev.f (prev.g_to_fin /- i -/ h).val) sorry,
            begin
              simp only [pnat.coe_lt_coe, tsub_pos_iff_lt],
              exact prev.f_comp_g_lt_f /- i -/ h
            end⟩)
        (assume _, none),
    g : fin x.length → option ℕ := λ i,
      f i >>= (λ v, dite (v.val < x.length)
        (assume h, coe <$> (pnat.has_sub.sub v <$> (f ⟨v.val, h⟩)))
        (assume _, none)),
    g_to_fin :
      Π {i : fin x.length} (h : (g i).is_some),
        {k : fin x.length // k.val = @option.get _ (g i) h} := sorry in
    have f_is_some_of_g_is_some :
      ∀ {i : fin x.length}, (g i).is_some → (f i).is_some := sorry,
    have f_comp_g_is_some_of_g_is_some :
      ∀ {i : fin x.length} (h : (g i).is_some), (f (@g_to_fin i h)).is_some := sorry,
    have f_comp_g_lt_f :
      ∀ {i : fin x.length} (h : (g i).is_some),
        @option.get _ (f (@g_to_fin i h)) (f_comp_g_is_some_of_g_is_some h) <
        @option.get _ (f i)                      (f_is_some_of_g_is_some h) := sorry,
  { f := @f,
    g := @g,
    g_to_fin := @g_to_fin,
    f_is_some_of_g_is_some := @f_is_some_of_g_is_some,
    f_comp_g_is_some_of_g_is_some := @f_comp_g_is_some_of_g_is_some,
    f_comp_g_lt_f := @f_comp_g_lt_f })

-- timeout!
-- Removing the last field or further simplifying `f` or `g` will make it work
-- but still strange when the other style is fine with it
def recursive_function_pattern_match (x : list ℕ) : ℕ → resultAt x
| 0 := sorry
| (j + 1) := let prev := recursive_function_pattern_match j in
  let f : fin x.length → option ℕ+ := λ i,
      dite (prev.g i).is_some
        (assume h, some
          ⟨@option.get _ (prev.f i) sorry -
            @option.get _ (prev.f (prev.g_to_fin /- i -/ h).val) sorry,
            begin
              simp only [pnat.coe_lt_coe, tsub_pos_iff_lt],
              exact prev.f_comp_g_lt_f /- i -/ h
            end⟩)
        (assume _, none),
    g : fin x.length → option ℕ := λ i,
      f i >>= (λ v, dite (v.val < x.length)
        (assume h, coe <$> (pnat.has_sub.sub <$> (f i) <*> (f ⟨v.val, h⟩)))
        (assume _, none)),
    g_to_fin :
      Π {i : fin x.length} (h : (g i).is_some),
        {k : fin x.length // k.val = @option.get _ (g i) h} := sorry in
    have f_is_some_of_g_is_some :
      ∀ {i : fin x.length}, (g i).is_some → (f i).is_some := sorry,
    have f_comp_g_is_some_of_g_is_some :
      ∀ {i : fin x.length} (h : (g i).is_some), (f (@g_to_fin i h)).is_some := sorry,
    have f_comp_g_lt_f :
      ∀ {i : fin x.length} (h : (g i).is_some),
        @option.get _ (f (@g_to_fin i h)) (f_comp_g_is_some_of_g_is_some h) <
        @option.get _ (f i)                      (f_is_some_of_g_is_some h) := sorry,
  { f := @f,
    g := @g,
    g_to_fin := @g_to_fin,
    f_is_some_of_g_is_some := @f_is_some_of_g_is_some,
    f_comp_g_is_some_of_g_is_some := @f_comp_g_is_some_of_g_is_some,
    f_comp_g_lt_f := @f_comp_g_lt_f }