How to decide no loops in list of references

Stream: new members

[aron]

How do I write this function?

inductive LeafOrRef
  | leaf : LeafOrRef
  | ref : Nat → LeafOrRef
  deriving DecidableEq

instance : Membership Nat LeafOrRef where
  mem lor n :=
    match lor with
    | .leaf => False
    | .ref i => i = n


inductive NoLoop (list : List LeafOrRef) : (lor : LeafOrRef) → Prop
  | leaf : NoLoop list .leaf
  | ref {i} {prf : i < list.length} : NoLoop list list[i] → NoLoop list (.ref i)


def NoLoop.decide
  (list : List LeafOrRef)
  (hvalid_refs : ∀ item ∈ list, ∀ i ∈ item, i < list.length)
  (lor : LeafOrRef)
  (hvalid_lor : ∀ i ∈ lor, i < list.length)
  : Decidable (NoLoop list lor) := by
  sorry

I've tried so many different things but I can't work out how to do this. Especially because I keep having to prove termination, but the whole point of this type is that it tells you whether there are loops or not, and since the list is finite in length, it should always terminate.

[Aaron Liu]

what have you tried

[aron]

This is the point at which I grind (no pun intended) to a halt :sweat:

import Mathlib

inductive LeafOrRef
  | leaf : LeafOrRef
  | ref : Nat → LeafOrRef
  deriving DecidableEq, BEq

@[simp,grind] instance instMembershipNatLeafOrRef : Membership Nat LeafOrRef where
  mem lor n :=
    match lor with
    | .leaf => False
    | .ref i => i = n

@[simp,grind] def instMembershipNatLeafOrRef.decide (i : Nat) (lor : LeafOrRef) : Decidable (i ∈ lor) := by
  match h : lor with
  | .leaf =>
    refine .isFalse ?_
    simp
  | .ref j =>
    if hh : j = i then
      refine .isTrue ?_
      simp
      trivial
    else
      refine .isFalse ?_
      simp
      trivial


/-- Proves that `i` is not contained in `lor` or any of the items it points to. This prop also contains proofs for any refs we find along the way, so it indeed proves not only that `i` isn't contained along the paths, but there are no loops anywhere along the path. -/
inductive NoLoop (list : List LeafOrRef) : (i : Nat) → (lor : LeafOrRef) → Prop
  | leaf : NoLoop list i .leaf

  | ref {prf : j < list.length} :
    i ≠ j →
    NoLoop list i list[j] → -- doesn't contain the ref that this thing is about
    NoLoop list j list[j] → -- also doesn't contain the current ref, recursively
    NoLoop list i (.ref j)




@[grind] theorem List.rev_pigeonhole_principle {l : List Nat}
    (nodup : l.Nodup)
    (heach : ∀ item ∈ l, item < n)
    (hitemlen : item < n)
    (hitemin : item ∉ l)
    : l.length < n := by
  let s : Finset Nat := Finset.mk l nodup
  have hs1 (x) : x ∈ l ↔ x ∈ s := Iff.rfl
  have hs2 : l.length = s.card := rfl
  simp only [hs1, implies_true, hs2] at *
  have : s ⊂ Finset.range n := by
    constructor
    · intro a ha
      simp_all
    · intro hs
      exact hitemin (hs (by simpa using hitemlen))
  simpa using Finset.card_lt_card this



def NoLoop.decideInner
  (list : List LeafOrRef)
  (lor : LeafOrRef)
  (ref : Nat)

  (hvalid_lor : ∀ i ∈ lor, i < list.length)
  (hvalid_refs : ∀ item ∈ list, ∀ i ∈ item, i < list.length)

  (seenRefs : List Nat)
  (refInSeens : ref ∈ seenRefs)
  (seensLen : seenRefs.length ≤ list.length)
  (seensNodup : seenRefs.Nodup)
  (seenEachSize : ∀ i ∈ seenRefs, i < list.length)
  (seenNinLor : ∀ i ∈ seenRefs, i ∉ lor)
  : Decidable (NoLoop list ref lor) := by
    cases hlor : lor with
    | leaf => refine .isTrue .leaf
    | ref i =>
      simp at hvalid_lor
      rw [hlor] at hvalid_lor
      replace hvalid_lor := hvalid_lor i rfl
      let refItem := list[i]'hvalid_lor
      match instMembershipNatLeafOrRef.decide i refItem, instMembershipNatLeafOrRef.decide ref refItem with
      | .isTrue prfI, _ =>
        refine .isFalse ?_
        intro nl
        cases nl
        expose_names
        unfold refItem at prfI
        cases hh : list[i] with
        | leaf =>
          rw [hh] at prfI
          simp at prfI
        | ref =>
          rw [hh] at prfI h_2
          simp at prfI
          subst_eqs
          simp at seenNinLor
          cases h_2
          expose_names
          rw [hh] at h_2
          cases h_2
          contradiction
      | _, .isTrue prfRef =>
        refine .isFalse ?_
        intro nl
        cases nl
        expose_names
        unfold refItem at prfRef
        cases hh : list[i] with
        | leaf =>
          rw [hh] at prfRef
          simp at prfRef
        | ref =>
          rw [hh] at prfRef h_2
          simp at prfRef
          subst_eqs
          simp at seenNinLor
          cases h_2
          contradiction

      | .isFalse prfI, .isFalse prfRef =>
        -- For proving termination
        have : seenRefs.length < list.length := by
          have : i ∉ seenRefs := by
            rw [hlor] at seenNinLor
            simp at seenNinLor
            grind
          have pig := List.rev_pigeonhole_principle (n:=list.length) seensNodup ?_ ?_ this
          grind
          grind
          trivial

        let decRef :=
          decideInner
            list
            refItem
            ref
            (by
            have : refItem ∈ list := by grind
            refine hvalid_refs refItem this)
            hvalid_refs
            (i :: seenRefs)
            (by tauto)
            (by
            have : i ∉ seenRefs := by
              rw [hlor] at seenNinLor
              simp at seenNinLor
              grind
            have pig := List.rev_pigeonhole_principle (n:=list.length) seensNodup ?_ ?_ this
            grind
            grind
            trivial)
            (by
            have : i ∈ lor := by simp [hlor]
            grind)
            (by
            simp
            refine ⟨hvalid_lor, ?_⟩
            tauto)
            (by
            simp only [List.mem_cons, forall_eq_or_imp]
            refine ⟨prfI,?_⟩
            sorry)


        match decRef with
        | .isTrue prfRef' =>
          have termin_proof : seenRefs.length < list.length := this

          let decI :=
            decideInner
              list
              refItem
              i
              (by
              have : refItem ∈ list := list.getElem_mem hvalid_lor
              refine hvalid_refs refItem this)
              hvalid_refs
              seenRefs
              (by tauto)
              (by
              have : ref ∉ seenRefs := by
                rw [hlor] at seenNinLor
                simp at seenNinLor
                grind
              have pig := List.rev_pigeonhole_principle (n:=list.length) seensNodup ?_ ?_ this
              grind
              grind
              trivial)
              (by
              have : ref ∈ lor := by simp [hlor]
              grind)
              (by
              simp
              have := seenEachSize ref refInSeens
              refine ⟨this, ?_⟩
              tauto)
              (by
              simp only [List.mem_cons, forall_eq_or_imp]
              refine ⟨prfRef,?_⟩
              sorry)

          match decI with
          | .isTrue prfI =>
            refine .isTrue ?_
            subst_eqs
            refine NoLoop.ref ?_ prfRef' prfI
            tauto
          | .isFalse prfI =>
            refine .isFalse ?_
            intro nl
            cases nl
            unfold refItem at prfRef
            contradiction

        | .isFalse prf =>
          refine .isFalse ?_
          intro nl
          cases nl
          unfold refItem at prf
          contradiction

  termination_by (list.length - seenRefs.length)

[aron]

For some reason grind stops working altogether in the second call to decideInner with this error:

tactic 'grind' failed, the goal mentions the declaration `decideInner`, which is being defined. To avoid circular reasoning, try rewriting the goal to eliminate `decideInner` before using `grind`.

Even though the goal is just Decidable (NoLoop list ref (LeafOrRef.ref i)) which doesn't mention decideInner at all?

[aron]

Plus I just don't even know if I'm going down the right track at all.

Intuitively what I'm doing is pretty simple: recurse down the list with refs, keeping a list of refs we've seen so far. If you come across a ref you've already seen, you know you've hit a loop. Otherwise keep going until you hit a .leaf. In which case you know there are no loops.

[aron]

But as you can see even just trying that approach is... a lot. I feel like there must be a simpler way to do this. I just can't figure out how

[Aaron Liu]

Tricky

[Aaron Liu]

Try writing a Bool-valued function and proving it correct

[aron]

I feel like that's going to be harder, no?

[Aaron Liu]

Since you have no dependent types

[Aaron Liu]

and you can delay the proof obligation

[aron]

Right so the implementation would be smoother, bc I can do it however I want. But I don't know how I'd prove that my implementation is equal to decidability

[Aaron Liu]

you can think about that after you have any working implementation

[aron]

well sure but the bool version shouldn't take too long. I'm working on it now

[aron]

I went with an allowlist approach instead of the disallowlist of the above approach. This is my Bool-valued version. Although ofc I'm not 100% it's correct yet.

def NoLoop.decideDumb
  (list : List LeafOrRef)
  (lor : LeafOrRef)
  (ref : Nat)

  (refValid : ref < list.length)
  (hvalid_lor : ∀ i ∈ lor, i < list.length)
  (hvalid_refs : ∀ item ∈ list, ∀ i ∈ item, i < list.length)

  (allowedRefs : List Nat)
  (allowedRefsNodup : allowedRefs.Nodup)
  (hrefNinAlloweds : ref ∉ allowedRefs)
  : Bool :=
    match hlor : lor with
    | .leaf => true
    | .ref i =>
      if i = ref then
        false
      else
        if hin : i ∈ allowedRefs then
          by
          simp at hvalid_lor
          let refItem := list[i]'hvalid_lor

          have : (allowedRefs.erase i).length < allowedRefs.length := by grind

          refine decideDumb list refItem i hvalid_lor ?_ hvalid_refs (allowedRefs.erase i) ?_ ?_
          refine hvalid_refs refItem (by grind)
          exact List.Nodup.erase i allowedRefsNodup
          exact List.Nodup.not_mem_erase allowedRefsNodup

        else
          false

  termination_by (allowedRefs.length)

[Aaron Liu]

great that works

[Aaron Liu]

now we prove it correct

[aron]

Like this, by filling out the two theorems?

theorem NoLoop.decideDumb_true_iff_NoLoop {ref refValid}
  : NoLoop.decideDumb list lor ref refValid hvalid_lor hvalid_refs = true ↔ NoLoop list ref lor
  := by sorry

theorem NoLoop.decideDumb_false_iff_NoLoop {ref refValid}
  : NoLoop.decideDumb list lor ref refValid hvalid_lor hvalid_refs = false ↔ ¬NoLoop list ref lor
  := by sorry

def NoLoop.decide
  (list : List LeafOrRef)
  (lor : LeafOrRef)
  (ref : Nat)

  (refValid : ref < list.length)
  (hvalid_lor : ∀ i ∈ lor, i < list.length)
  (hvalid_refs : ∀ item ∈ list, ∀ i ∈ item, i < list.length)
  : Decidable (NoLoop list ref lor) := by
  let dec := decideDumb list lor ref refValid hvalid_lor hvalid_refs

  if h : dec then
    refine .isTrue (NoLoop.decideDumb_true_iff_NoLoop.mp h)
  else
    simp at h
    refine .isFalse (NoLoop.decideDumb_false_iff_NoLoop.mp h)

[Aaron Liu]

well you only need one theorem

[Aaron Liu]

don't try proving both it's redundant

[Aaron Liu]

and the decidable definition can use docs#decidable_of_bool

[aron]

Ok nice. But then the way to do this is indeed to prove NoLoop.decideDumb_true_iff_NoLoop as I've defined the theorem statement?

[Aaron Liu]

probably yeah

[aron]

And would NoLoop.decideDumbInner.induct be a good way to prove it?

[Aaron Liu]

you should try out the fun_induction tactic I think it will be useful here

[aron]

ok this is as far as I got

import Mathlib

inductive LeafOrRef
  | leaf : LeafOrRef
  | ref : Nat → LeafOrRef
  deriving DecidableEq, BEq

@[simp,grind] instance instMembershipNatLeafOrRef : Membership Nat LeafOrRef where
  mem lor n :=
    match lor with
    | .leaf => False
    | .ref i => i = n

@[simp,grind] def instMembershipNatLeafOrRef.decide (i : Nat) (lor : LeafOrRef) : Decidable (i ∈ lor) := by
  match h : lor with
  | .leaf =>
    refine .isFalse ?_
    simp
  | .ref j =>
    if hh : j = i then
      refine .isTrue ?_
      simp
      trivial
    else
      refine .isFalse ?_
      simp
      trivial


/-- Proves that `i` is not contained in `lor` or any of the items it points to. This prop also contains proofs for any refs we find along the way, so it indeed proves not only that `i` isn't contained along the paths, but there are no loops anywhere along the path. -/
inductive NoLoop (list : List LeafOrRef) : (i : Nat) → (lor : LeafOrRef) → Prop
  | leaf : NoLoop list i .leaf

  | ref {prf : j < list.length} :
    i ≠ j →
    NoLoop list i list[j] → -- doesn't contain the ref that this thing is about
    NoLoop list j list[j] → -- also doesn't contain the current ref, recursively
    NoLoop list i (.ref j)





def NoLoop.decideDumbInner
  (list : List LeafOrRef)
  (lor : LeafOrRef)
  (ref : Nat)

  (refValid : ref < list.length)
  (hvalid_lor : ∀ i ∈ lor, i < list.length)
  (hvalid_refs : ∀ item ∈ list, ∀ i ∈ item, i < list.length)

  (allowedRefs : List Nat)
  (allowedRefsNodup : allowedRefs.Nodup)
  (allowedRefsInRange : ∀ i ∈ allowedRefs, i < list.length)
  (hrefNinAlloweds : ref ∉ allowedRefs)
  : Bool :=
    match hlor : lor with
    | .leaf => true
    | .ref i =>
      if i = ref then
        false
      else
        if hin : i ∈ allowedRefs then
          by
          simp at hvalid_lor
          let refItem := list[i]'hvalid_lor

          -- For termination proving
          have erased_len : (allowedRefs.erase i).length < allowedRefs.length := by grind

          -- This should be `false` both if we encounter `i` *or* `ref` again – because neither are present in `allowedRefs`!
          let innerI := decideDumbInner list refItem i hvalid_lor (hvalid_refs refItem (by grind)) hvalid_refs (allowedRefs.erase i) (List.Nodup.erase i allowedRefsNodup) (by grind) (List.Nodup.not_mem_erase allowedRefsNodup)

          refine innerI

        else
          false

  termination_by (allowedRefs.length)







theorem NoLoop.decideDumbInner_true_iff_NoLoop {ref refValid allowedRefs allowedRefsNodup allowedRefsInRange hrefNinAlloweds}
  : NoLoop.decideDumbInner list lor ref refValid hvalid_lor hvalid_refs allowedRefs allowedRefsNodup allowedRefsInRange hrefNinAlloweds = true ↔ (NoLoop list ref lor ∧ (∀ i, (h : i ∈ lor) → NoLoop list i (list[i]'(hvalid_lor i h)) ∧ NoLoop list ref (list[i]'(hvalid_lor i h))))
  := by
  apply Iff.intro
  ·

    have forward :
      NoLoop.decideDumbInner list lor ref refValid hvalid_lor hvalid_refs allowedRefs allowedRefsNodup allowedRefsInRange hrefNinAlloweds = true →
        -- NoLoop list ref lor ∧
        -- (∀ i ∈ lor, NoLoop list i (list[i]'(?_)) ∧ NoLoop list ref (list[i]'(?_))) ∧
        -- (∀ i < list.length, (hin : i ∉ allowedRefs) → (NoLoop list i lor ∧ NoLoop list i (list[i]'(?_)) ∧ NoLoop list ref (list[i]'(?_))))
        NoLoop list ref lor ∧
        (∀ i, (h : i ∈ lor) → NoLoop list i (list[i]'(hvalid_lor i h)) ∧ NoLoop list ref (list[i]'(hvalid_lor i h)))
        -- ∧
        -- (∀ i < list.length, (hin : i ∉ allowedRefs) → (NoLoop list i lor ∧ NoLoop list i (list[i]'(?_)) ∧ NoLoop list ref (list[i]'(?_))))
      := by
      fun_induction NoLoop.decideDumbInner list lor ref refValid hvalid_lor hvalid_refs allowedRefs allowedRefsNodup allowedRefsInRange hrefNinAlloweds with
      | case1 ref refValid allowedRefs allowedRefsNodup hrefNinAlloweds hvalid_lor =>
        intro _
        refine ⟨ .leaf, ?_ ⟩
        simp
      | case2 =>
        intro _
        contradiction
      | case3 =>
      --  ref refValid allowedRefs allowedRefsNodup hrefNinAlloweds hvalid_lor _ _ i hneq hin h refItem hvalid_lor erased_len innerI ih
        expose_names
        intro inner
        replace ih1 := ih1 inner
        unfold refItem at ih1

        have left := ih1.left
        have right := ih1.right

        refine ⟨ .ref (Ne.symm h) ?_ left, ?_ ⟩
        · sorry -- ???
        · intro j jin
          simp at jin
          subst_eqs
          refine ⟨left,?_⟩
          sorry -- ???

      | case4 =>
        expose_names
        intro _
        contradiction

    refine forward

  · sorry




def NoLoop.decide
  (list : List LeafOrRef)
  (lor : LeafOrRef)
  (ref : Nat)

  (refValid : ref < list.length)
  (hvalid_lor : ∀ i ∈ lor, i < list.length)
  (hvalid_refs : ∀ item ∈ list, ∀ i ∈ item, i < list.length)

  (allowedRefs : List Nat)
  (allowedRefsNodup : allowedRefs.Nodup)
  (allowedRefsInRange : ∀ i ∈ allowedRefs, i < list.length)
  (hrefNinAlloweds : ref ∉ allowedRefs)
  : Decidable (NoLoop list ref lor) := by
  let result :=
    decideDumbInner list lor ref refValid hvalid_lor hvalid_refs allowedRefs allowedRefsNodup allowedRefsInRange hrefNinAlloweds

  let dec :=
    decidable_of_bool result NoLoop.decideDumbInner_true_iff_NoLoop

  cases dec with
  | isTrue prf =>
    refine .isTrue prf.left

  | isFalse prf =>
    simp only [not_and, not_forall] at prf
    refine .isFalse ?_
    intro nl
    have ⟨x,h,bla⟩ := prf nl
    cases nl
    · simp at h
    · simp at h
      subst_eqs
      expose_names
      have := bla h
      contradiction

[aron]

I cannot work out how to tell Lean about the link between not being in allowedRefs and being able to construct a NoLoop for it :sweat:

[aron]

E.g. at this point:

      | case3 =>
        expose_names
        intro inner
        replace ih1 := ih1 inner
        unfold refItem at ih1

        have left := ih1.left
        have right := ih1.right

        refine ⟨ .ref (Ne.symm h) ?_ left, ?_ ⟩
        ·
          -- 👈 HERE
          sorry

the target is NoLoop list ref_1 list[i]. And I would indeed expect there to be one of these available in ih1. Because I specified it in the induction goal (see screenshot). But somehow there doesn't appear to be one of these available

Screenshot 2025-09-27 at 20.13.24.png

[aron]

Ok I modified the induction target a bit and now I can get further – but I still am left with one part I don't know how to solve

def NoLoop.decideDumbInner
  (list : List LeafOrRef)
  (lor : LeafOrRef)
  (ref : Nat)

  (refValid : ref < list.length)
  (hvalid_lor : ∀ i ∈ lor, i < list.length)
  (hvalid_refs : ∀ item ∈ list, ∀ i ∈ item, i < list.length)

  (allowedRefs : List Nat)
  (allowedRefsNodup : allowedRefs.Nodup)
  (allowedRefsInRange : ∀ i ∈ allowedRefs, i < list.length)
  (hrefNinAlloweds : ref ∉ allowedRefs)
  : Bool :=
    match hlor : lor with
    | .leaf => true
    | .ref i =>
      if i = ref then
        false
      else
        if hin : i ∈ allowedRefs then
          by
          simp at hvalid_lor
          let refItem := list[i]'hvalid_lor

          -- For termination proving
          have erased_len : (allowedRefs.erase i).length < allowedRefs.length := by grind

          -- This should be `false` both if we encounter `i` *or* `ref` again – because neither are present in `allowedRefs`!
          let innerI := decideDumbInner list refItem i hvalid_lor (hvalid_refs refItem (by grind)) hvalid_refs (allowedRefs.erase i) (List.Nodup.erase i allowedRefsNodup) (by grind) (List.Nodup.not_mem_erase allowedRefsNodup)

          refine innerI

        else
          false

  termination_by (allowedRefs.length)


theorem NoLoop.decideDumbInner_true_iff_NoLoop {ref refValid allowedRefs allowedRefsNodup allowedRefsInRange hrefNinAlloweds}
  : NoLoop.decideDumbInner list lor ref refValid hvalid_lor hvalid_refs allowedRefs allowedRefsNodup allowedRefsInRange hrefNinAlloweds = true ↔ NoLoop list ref lor ∧
        (∀ old ∉ allowedRefs, NoLoop list old lor) ∧
        (∀ i, (h : i ∈ lor) →
          (NoLoop list i (list[i]'(hvalid_lor i h)) ∧
           NoLoop list ref (list[i]'(hvalid_lor i h))))
  := by
  apply Iff.intro
  ·
    have forward :
      NoLoop.decideDumbInner list lor ref refValid hvalid_lor hvalid_refs allowedRefs allowedRefsNodup allowedRefsInRange hrefNinAlloweds = true →
        NoLoop list ref lor ∧
        (∀ old ∉ allowedRefs, NoLoop list old lor) ∧
        (∀ i, (h : i ∈ lor) →
          (NoLoop list i (list[i]'(hvalid_lor i h)) ∧
           NoLoop list ref (list[i]'(hvalid_lor i h))))
      := by
      fun_induction NoLoop.decideDumbInner list lor ref refValid hvalid_lor hvalid_refs allowedRefs allowedRefsNodup allowedRefsInRange hrefNinAlloweds with
      | case1 ref refValid allowedRefs allowedRefsNodup hrefNinAlloweds hvalid_lor =>
        intro _
        refine ⟨ .leaf, ?_ ⟩
        simp
        tauto
      | case2 =>
        intro _
        contradiction
      | case3 =>
        expose_names
        intro inner
        replace ih1 := ih1 inner
        unfold refItem at ih1

        have left := ih1.left
        have right := ih1.right

        refine ⟨ .ref (Ne.symm h) ?_ left, ?_ ⟩
        · have rl := right.left
          refine rl ref_1 (by grind)
        · simp [*]
          constructor
          · have rl := right.left
            intro j jin
            refine .ref (prf:=by grind) (by grind) (by grind) (by grind)
          · intro _ h
            subst_eqs
            constructor
            · grind
            · grind

      | case4 =>
        expose_names
        intro _
        contradiction

    refine forward

  ·
    have backward :
      NoLoop list ref lor ∧
      (∀ old ∉ allowedRefs, NoLoop list old lor) ∧
      (∀ i, (h : i ∈ lor) →
        (NoLoop list i (list[i]'(hvalid_lor i h)) ∧
          NoLoop list ref (list[i]'(hvalid_lor i h)))) →
          NoLoop.decideDumbInner list lor ref refValid hvalid_lor hvalid_refs allowedRefs allowedRefsNodup allowedRefsInRange hrefNinAlloweds = true
      := by
      fun_induction NoLoop.decideDumbInner list lor ref refValid hvalid_lor hvalid_refs allowedRefs allowedRefsNodup allowedRefsInRange hrefNinAlloweds with
      | case1 =>
        intro _
        rfl
      | case2 =>
        intro prem
        have := prem.left
        cases this
        contradiction
      | case3 =>
        intro prem
        expose_names
        apply ih1
        have ⟨ll,lr,r⟩ := prem
        constructor
        · simp at r
          refine r i rfl |>.left
        · constructor
          · simp at r
            replace r := r i rfl
            unfold refItem
            intro old oldnin
            have : (old ∉ allowedRefs_1.erase i) = (old = i ∨ old ∉ allowedRefs_1) := by grind
            rw [this] at oldnin
            cases oldnin
            · subst_eqs
              exact r.left
            · rename_i h
              cases lr old h
              trivial
          · intro j jin
            simp at r
            unfold refItem at jin
            -- replace r := r i rfl
            -- cases lr ref_1 hrefNinAlloweds
            -- cases ll

            sorry -- <-- STUCK HERE

      | case4 =>
        intro prem
        have ⟨ll,lr,r⟩ := prem
        simp at r
        expose_names
        cases lr i h_1
        contradiction

    refine backward

[aron]

The whole #mwe (for anyone keeping up)

import Mathlib

inductive LeafOrRef
  | leaf : LeafOrRef
  | ref : Nat → LeafOrRef
  deriving DecidableEq, BEq

@[simp,grind] instance instMembershipNatLeafOrRef : Membership Nat LeafOrRef where
  mem lor n :=
    match lor with
    | .leaf => False
    | .ref i => i = n

@[simp,grind] def instMembershipNatLeafOrRef.decide (i : Nat) (lor : LeafOrRef) : Decidable (i ∈ lor) := by
  match h : lor with
  | .leaf =>
    refine .isFalse ?_
    simp
  | .ref j =>
    if hh : j = i then
      refine .isTrue ?_
      simp
      trivial
    else
      refine .isFalse ?_
      simp
      trivial


/-- Proves that `i` is not contained in `lor` or any of the items it points to. This prop also contains proofs for any refs we find along the way, so it indeed proves not only that `i` isn't contained along the paths, but there are no loops anywhere along the path. -/
inductive NoLoop (list : List LeafOrRef) : (i : Nat) → (lor : LeafOrRef) → Prop
  | leaf : NoLoop list i .leaf

  | ref {prf : j < list.length} :
    i ≠ j →
    NoLoop list i list[j] → -- doesn't contain the ref that this thing is about
    NoLoop list j list[j] → -- also doesn't contain the current ref, recursively
    NoLoop list i (.ref j)



@[grind] theorem NoLoop.self_ref_impossible {prf} (hlor : lor = list[i]'prf) (hinlor : i ∈ lor) : ¬NoLoop list i lor := by
  intro nl
  cases h : lor
  · rw [h] at nl hinlor
    simp at hinlor
  · rw [h] at nl hinlor
    simp at hinlor
    subst_eqs
    cases nl
    contradiction









def NoLoop.decideDumbInner
  (list : List LeafOrRef)
  (lor : LeafOrRef)
  (ref : Nat)

  (refValid : ref < list.length)
  (hvalid_lor : ∀ i ∈ lor, i < list.length)
  (hvalid_refs : ∀ item ∈ list, ∀ i ∈ item, i < list.length)

  (allowedRefs : List Nat)
  (allowedRefsNodup : allowedRefs.Nodup)
  (allowedRefsInRange : ∀ i ∈ allowedRefs, i < list.length)
  (hrefNinAlloweds : ref ∉ allowedRefs)
  : Bool :=
    match hlor : lor with
    | .leaf => true
    | .ref i =>
      if i = ref then
        false
      else
        if hin : i ∈ allowedRefs then
          by
          simp at hvalid_lor
          let refItem := list[i]'hvalid_lor

          -- For termination proving
          have erased_len : (allowedRefs.erase i).length < allowedRefs.length := by grind

          -- This should be `false` both if we encounter `i` *or* `ref` again – because neither are present in `allowedRefs`!
          let innerI := decideDumbInner list refItem i hvalid_lor (hvalid_refs refItem (by grind)) hvalid_refs (allowedRefs.erase i) (List.Nodup.erase i allowedRefsNodup) (by grind) (List.Nodup.not_mem_erase allowedRefsNodup)

          refine innerI

        else
          false

  termination_by (allowedRefs.length)







theorem NoLoop.decideDumbInner_true_iff_NoLoop {ref refValid allowedRefs allowedRefsNodup allowedRefsInRange hrefNinAlloweds}
  : NoLoop.decideDumbInner list lor ref refValid hvalid_lor hvalid_refs allowedRefs allowedRefsNodup allowedRefsInRange hrefNinAlloweds = true ↔ NoLoop list ref lor ∧
        (∀ old ∉ allowedRefs, NoLoop list old lor) ∧
        (∀ i, (h : i ∈ lor) →
          (NoLoop list i (list[i]'(hvalid_lor i h)) ∧
           NoLoop list ref (list[i]'(hvalid_lor i h))))
  := by
  apply Iff.intro
  ·
    have forward :
      NoLoop.decideDumbInner list lor ref refValid hvalid_lor hvalid_refs allowedRefs allowedRefsNodup allowedRefsInRange hrefNinAlloweds = true →
        NoLoop list ref lor ∧
        (∀ old ∉ allowedRefs, NoLoop list old lor) ∧
        (∀ i, (h : i ∈ lor) →
          (NoLoop list i (list[i]'(hvalid_lor i h)) ∧
           NoLoop list ref (list[i]'(hvalid_lor i h))))
      := by
      fun_induction NoLoop.decideDumbInner list lor ref refValid hvalid_lor hvalid_refs allowedRefs allowedRefsNodup allowedRefsInRange hrefNinAlloweds with
      | case1 ref refValid allowedRefs allowedRefsNodup hrefNinAlloweds hvalid_lor =>
        intro _
        refine ⟨ .leaf, ?_ ⟩
        simp
        tauto
      | case2 =>
        intro _
        contradiction
      | case3 =>
        expose_names
        intro inner
        replace ih1 := ih1 inner
        unfold refItem at ih1

        have left := ih1.left
        have right := ih1.right

        refine ⟨ .ref (Ne.symm h) ?_ left, ?_ ⟩
        · have rl := right.left
          refine rl ref_1 (by grind)
        · simp [*]
          constructor
          · have rl := right.left
            intro j jin
            refine .ref (prf:=by grind) (by grind) (by grind) (by grind)
          · intro _ h
            subst_eqs
            constructor
            · grind
            · grind

      | case4 =>
        expose_names
        intro _
        contradiction

    refine forward

  ·
    have backward :
      NoLoop list ref lor ∧
      (∀ old ∉ allowedRefs, NoLoop list old lor) ∧
      (∀ i, (h : i ∈ lor) →
        (NoLoop list i (list[i]'(hvalid_lor i h)) ∧
          NoLoop list ref (list[i]'(hvalid_lor i h)))) →
          NoLoop.decideDumbInner list lor ref refValid hvalid_lor hvalid_refs allowedRefs allowedRefsNodup allowedRefsInRange hrefNinAlloweds = true
      := by
      fun_induction NoLoop.decideDumbInner list lor ref refValid hvalid_lor hvalid_refs allowedRefs allowedRefsNodup allowedRefsInRange hrefNinAlloweds with
      | case1 =>
        intro _
        rfl
      | case2 =>
        intro prem
        have := prem.left
        cases this
        contradiction
      | case3 =>
        intro prem
        expose_names
        apply ih1
        have ⟨ll,lr,r⟩ := prem
        constructor
        · simp at r
          refine r i rfl |>.left
        · constructor
          · simp at r
            replace r := r i rfl
            unfold refItem
            intro old oldnin
            have : (old ∉ allowedRefs_1.erase i) = (old = i ∨ old ∉ allowedRefs_1) := by grind
            rw [this] at oldnin
            cases oldnin
            · subst_eqs
              exact r.left
            · rename_i h
              cases lr old h
              trivial
          · intro j jin
            simp at r
            unfold refItem at jin
            -- replace r := r i rfl
            -- cases lr ref_1 hrefNinAlloweds
            -- cases ll

            sorry -- <-- STUCK HERE

      | case4 =>
        intro prem
        have ⟨ll,lr,r⟩ := prem
        simp at r
        expose_names
        cases lr i h_1
        contradiction

    refine backward

[aron]

In short: I don't have any way to prove anything about the item at list[j]

Screenshot 2025-09-27 at 22.12.53.png

[aron]

I wonder if I need to add something explicit about the relationship between allowedRefs and NoLoopness in the induction target :thinking:

[aron]

because I've managed to prove the forward direction of the iff (:tada:) but I'm stuck on this part in the backward direction. And I'm not sure I can prove it without saying something about j being in allowedRefs

[Aaron Liu]

When I'm back at a keyboard I'll try helping

[aron]

@Aaron Liu any ideas?

[Aaron Liu]

oh I forgot about this sorry

[Aaron Liu]

let's see...

[Aaron Liu]

sorry I don't have any ideas

[aron]

are you familiar with the stuff in Mathlib? any idea if some of the theorems and/or decidable instances in SimpleGraph would be useful to me?

[Aaron Liu]

not simple graphs this is a thing with directed graphs

[aron]

ah right. and SimpleGraph can't handle those? is there anything in Mathlib for directed graphs?

[Aaron Liu]

docs#Digraph

[Aaron Liu]

can't find anything about cycles

[aron]

hm yeah Digraphs doesn't seem to have that much in it. Is that it for graph types in mathlib? surely not?

[Aaron Liu]

docs#Graph

[aron]

hm ok. looks promising. but i can't see anything in there to decide loop-ness

[Matt Diamond]

I don't understand what you're trying to model... LeafOrRef seems identical to Option Nat, how do loops come into play here? How would a list of Option Nat have or not have a loop?

[aron]

@Matt Diamond the Nats reference other LeafOrRefs by their index in the list

[Aaron Liu]

Matt Diamond said:

I don't understand what you're trying to model... LeafOrRef seems identical to Option Nat, how do loops come into play here? How would a list of Option Nat have or not have a loop?

You can interpret it as a directed graph on Fin l.length using Adj i j := l[i] = some j

[Robert Maxton]

mm, is the Matrix library still mostly noncomputable? I remember having trouble working with it back in January
If not, then since you basically have the adjacency matrix you can prove that a walk of length n exists between two vertices iff the nth power of the adjacency matrix has a nonzero entry at that point; so if there are V vertices, then the graph has a cycle iff the Vth power has any nonzero entries along its diagonal, which is certainly decidable.