## Stream: general

### Topic: equation compiler fails for inductive predicate

#### Kenny Lau (Apr 01 2018 at 22:07):

since they do not have a size

#### Huỳnh Trần Khanh (Jul 20 2021 at 09:20):

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 (Jul 20 2021 at 10:29):

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

#### Mario Carneiro (Jul 20 2021 at 13:03):

@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₂, _⟩,