Decidability of TransGen in Lean 4 with Bounded Relation

Stream: new members

[Zhiyang Wang]

Dear all,

I am exploring the decidability of Relation.TransGen in Lean 4. As currently defined, TransGen is undecidable due to the potentially infinite number of pairs under a given relation r.

My question is: If we constrain the relation r to a finite set or list (e.g., by defining r as fun x y => x ∈ bound ∧ y ∈ bound ∧ r x y), is it then possible to implement a decision procedure for TransGen?

I've attempted to define such a procedure, check_trans', as follows:

def check_trans'
   {α : Type}
   [DecidableEq α]
   (r : α -> α -> Prop)
   [DecidableRel r]
   (input : List α)
   (a b : α)
   (visited : List α)
   (hv : input.Nodup)
   : Bool :=
   if a ∉ input ∨ b ∉ input then
     false
   else if r a b then
     true
   else if visited.length >= input.length then
     -- Which means we already tried all the imm edges.
     false
   else
     let v := b::visited
     input.any (fun x => r x b ∧ check_trans' r input a x v (by aesop))
termination_by input.length - visited.length
decreasing_by {
  simp
  omega
}

My goal is to prove the following lemma:

lemma tc_towards_comp'
   (a c : Event)
   (r : Event -> Event -> Prop)
   [DecidableRel r]
   (input : List Event)
   (visited : List Event)
   (hin : input.Nodup)
   (hnodup : visited.Nodup)
   (hsub : visited ⊆ input)
   (htrans : Relation.TransGen (fun x y ↦ x ∈ input ∧ y ∈ input ∧ r x y) a c)
   : check_trans' r input a c visited hin :=
   by
     unfold check_trans'
     split
     {
       rename_i h
       induction htrans with
       | single => {
         aesop
       }
       | tail => {
         aesop
       }
     }
     {
       rename_i h
       push_neg at h
       split
       {
         simp
       }
       {
         split
         {
           induction htrans with
           | single hrel => {
             simp_all
           }
           | tail => {
             simp_all
             contradiction
           }
         }
         {
           rename_i hrac
           simp
           induction htrans with
           | single hrel => {
             rename_i b hnrab
             have rab : r a b := by
               aesop

             contradiction
           }
           | tail htrans hrel ihts => {
             rename_i b c' hnac'
             use b
             apply And.intro
             {
               aesop
             }
             {
               apply And.intro
               {
                 aesop
               }
               {
                 let tc : List Event := c'::visited
                 apply tc_towards_comp' a b r input tc (by aesop)
                 {

                 }
                 {
                   aesop
                 }
                 exact htrans
               }
             }
           }
         }
       }
     }
termination_by (input.length - visited.length)
decreasing_by {
  simp
  omega
}

Despite my efforts, I'm consistently encountering issues with edge cases during the proof. I'm trying to determine if my algorithm of DFS for check_trans' is flawed, or if there are specific conditions or assumptions I might have overlooked.

Any insights or suggestions would be greatly appreciated!

Thank you for your time and help.

[Kenny Lau]

The mathematician in me is saying that you can define r^n of a relation r, and then r^(Fintype.card α) will be TransGen r

[Kenny Lau]

also i'm not seeing any finiteness constraint in your code

[Edward van de Meent]

Kenny Lau said:

The mathematician in me is saying that you can define r^n of a relation r, and then r^(Fintype.card α) will be TransGen r

unfortunately, the mathematician in me says that r^n of a relation r (judging from the notation alone) is the relation given by "there is a r-chain of length n" rather than "there is a r-chain of length at most n".

[Edward van de Meent]

which would not result in r^(Fintype.card α) being TransGen r

[Kenny Lau]

I see, the union of r^1 to r^n will be TransGen r then

[Edward van de Meent]

yes, that seems to be the "right" way to state it

[Andrés Goens]

Kenny Lau said:

also i'm not seeing any finiteness constraint in your code

I guess that finiteness constraint is not "explicit", but comes from the input : List α being a list

[Aaron Liu]

Doesn't α have to be finite too?

[Andrés Goens]

so Fintype.ofList

[Aaron Liu]

Oh are you only searching on the finite subset of α given by input?

[Andrés Goens]

Aaron Liu said:

Doesn't α have to be finite too?

I don't see why it would? ( he has to restrict the relation before taking the transitive closure)

[Andrés Goens]

yeah, this would not be the same as TransGen r restricted to input, because there might be an element outside of input that transitively relates two elements inside of it

[Kenny Lau]

@Andrés Goens (let's not speak for the author of the post), if s/he wants finiteness, s/he cannot allow for an element outside of input relating two elements inside input; and then s/he'll find him/herself in a situation where s/he should have declared finiteness in the first place

[Andrés Goens]

Kenny Lau said:

Andrés Goens (let's not speak for the author of the post), if s/he wants finiteness, s/he cannot allow for an element outside of input relating two elements inside input; and then s/he'll find him/herself in a situation where s/he should have declared finiteness in the first place

@Kenny Lau (oh, I know him and we discussed this issue before DM)

I guess that's exactly what fun x y => x ∈ bound ∧ y ∈ bound ∧ r x y is supposed to do, but I am confused now too why it says ∈ bound and not ∈ input

[Edward van de Meent]

the use of bound is before introducing a concrete attempt with different naming, where input seems to be used consistently instead

[Zhiyang Wang]

Edward van de Meent said:

Kenny Lau said:

The mathematician in me is saying that you can define r^n of a relation r, and then r^(Fintype.card α) will be TransGen r

unfortunately, the mathematician in me says that r^n of a relation r (judging from the notation alone) is the relation given by "there is a r-chain of length n" rather than "there is a r-chain of length at most n".

Thanks a lot to all of you! It helps a lot! Even though I don't feel like I have a mathematician in me, haha. I will try to state it as this.