equation compiler fails for inductive predicate

Stream: general

[Kenny Lau]

since they do not have a size

[Huỳnh Trần Khanh]

hmm i'm trying to prove a lemma and i'm pretty sure that my proof strategy is sound... but the equation compiler isn't convinced...

import tactic.slim_check

structure triple_t := (a b c cost : ℕ)
inductive reachable : triple_t → triple_t → Prop
| refl (x : triple_t) : reachable x x
| increment_a (a b c cost : ℕ) : reachable ⟨a, b, c, cost⟩ ⟨a + 1, b, c, cost + 1⟩
| increment_b (a b c cost : ℕ) : reachable ⟨a, b, c, cost⟩ ⟨a, b + 1, c, cost + 1⟩
| increment_c (a b c cost : ℕ) : reachable ⟨a, b, c, cost⟩ ⟨a, b, c + 1, cost + 1⟩
| trans (x y z : triple_t) : reachable x y → reachable y z → reachable x z

lemma real_meaning_of_reachable : ∀ a b c a1 b1 c1 cost cost1 : ℕ, reachable ⟨a, b, c, cost⟩ ⟨a1, b1, c1, cost1⟩ → a ≤ a1 ∧ b ≤ b1 ∧ c ≤ c1 ∧ cost ≤ cost1 ∧ (a1 - a) + (b1 - b) + (c1 - c) = cost1 - cost
| a b c a1 b1 c1 cost cost1 (reachable.refl x) := begin
  repeat {
    split,
    linarith,
  },
  norm_num,
end
| a b c a1 b1 c1 cost cost1 (reachable.increment_a a' b' c' cost') := begin
  repeat {
    split,
    linarith,
  },
  norm_num,
end
| a b c a1 b1 c1 cost cost1 (reachable.increment_b a' b' c' cost') := begin
  repeat {
    split,
    linarith,
  },
  norm_num,
end
| a b c a1 b1 c1 cost cost1 (reachable.increment_c a' b' c' cost') := begin
  repeat {
    split,
    linarith,
  },
  norm_num,
end
| a b c a1 b1 c1 cost cost1 (reachable.trans ⟨a', b', c', cost'⟩ ⟨a'', b'', c'', cost''⟩ ⟨a''', b''', c''', cost'''⟩ h1 h2) := begin
  -- failed to prove recursive application is decreasing, well founded relation
  have := real_meaning_of_reachable _ _ _ _ _ _ _ _ h1,
  have := real_meaning_of_reachable _ _ _ _ _ _ _ _ h2,
  repeat {
    split,
    linarith,
  },
  have : a''' - a' + (b''' - b') + (c''' - c') = cost''' - cost' := sorry,
  exact this,
end

how can i resolve this?

[Mario Carneiro]

Did you try using induction instead of the equation compiler? That is more reliable for structural inductive proofs over predicates

[Mario Carneiro]

@Huỳnh Trần Khanh

lemma real_meaning_of_reachable {a b c a1 b1 c1 cost cost1 : ℕ}
  (H : reachable ⟨a, b, c, cost⟩ ⟨a1, b1, c1, cost1⟩) :
  a ≤ a1 ∧ b ≤ b1 ∧ c ≤ c1 ∧ cost ≤ cost1 ∧ (a1 - a) + (b1 - b) + (c1 - c) = cost1 - cost :=
begin
  generalize_hyp h₁ : (⟨a, b, c, cost⟩ : triple_t) = e₁ at H,
  generalize_hyp h₂ : (⟨a1, b1, c1, cost1⟩ : triple_t) = e₂ at H,
  have succ_sub : ∀ n:ℕ, n.succ - n = 1 := λ n, by simp [nat.succ_sub],
  induction H generalizing a b c cost a1 b1 c1 cost1,
  case trans : _ y _ _ _ ih₁ ih₂ {
    cases y with a2 b2 c2 cost2,
    obtain ⟨aa₁, bb₁, cc₁, oo₁, ih₁⟩ := ih₁ h₁ rfl,
    obtain ⟨aa₂, bb₂, cc₂, oo₂, ih₂⟩ := ih₂ rfl h₂,
    refine ⟨aa₁.trans aa₂, bb₁.trans bb₂, cc₁.trans cc₂, oo₁.trans oo₂, _⟩,
    linarith [nat.sub_add_sub_cancel aa₂ aa₁, nat.sub_add_sub_cancel bb₂ bb₁,
      nat.sub_add_sub_cancel cc₂ cc₁, nat.sub_add_sub_cancel oo₂ oo₁] },
  all_goals { cases h₁; cases h₂; simp [nat.le_succ, succ_sub] }
end