English
If equality is decidable for vertices and arrows and for bounded paths of length n, then it is decidable for bounded paths of length n+1.
Русский
Если равенство вершин и стрел и ограниченных путей длины n разрешимо, то разрешимо и для путей длины n+1.
LaTeX
$$$\\mathrm{DecidableEq}(\\mathrm{BoundedPaths}(v,w,n+1)).$$$
Lean4
/-- Given decidable equality on paths of length up to `n`, we can construct
decidable equality on paths of length up to `n + 1`. -/
def decidableEqBddPathsOfDecidableEq (n : ℕ) (h₁ : DecidableEq V) (h₂ : ∀ (v w : V), DecidableEq (v ⟶ w))
(h₃ : ∀ (v w : V), DecidableEq (BoundedPaths v w n)) (v w : V) : DecidableEq (BoundedPaths v w (n + 1)) :=
fun ⟨p, hp⟩ ⟨q, hq⟩ =>
match v, w, p, q with
| _, _, .nil, .nil => isTrue rfl
| _, _, .nil, .cons _ _ => isFalse fun h => Quiver.Path.noConfusion <| Subtype.mk.inj h
| _, _, .cons _ _, .nil => isFalse fun h => Quiver.Path.noConfusion <| Subtype.mk.inj h
| _, _, .cons (b := v') p' α, .cons (b := v'') q' β =>
match v', v'', h₁ v' v'' with
| _, _, isTrue (Eq.refl _) =>
if h : α = β then
have hp' : p'.length ≤ n := by simp [Quiver.Path.length] at hp; cutsat
have hq' : q'.length ≤ n := by simp [Quiver.Path.length] at hq; cutsat
if h'' : (⟨p', hp'⟩ : BoundedPaths _ _ n) = ⟨q', hq'⟩ then
isTrue <| by
apply Subtype.ext
dsimp
rw [h, show p' = q' from Subtype.mk.inj h'']
else isFalse fun h => h'' <| Subtype.ext <| eq_of_heq <| (Quiver.Path.cons.inj <| Subtype.mk.inj h).2.1
else isFalse fun h' => h <| eq_of_heq (Quiver.Path.cons.inj <| Subtype.mk.inj h').2.2
| _, _, isFalse h => isFalse fun h' => h (Quiver.Path.cons.inj <| Subtype.mk.inj h').1
