Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] lemma about finitely-branching finite sequences

Email Gateway (Aug 19 2022 at 14:47):

From: John Wickerson <johnwickerson@cantab.net>
Hi,

I have a relation "↝" representing the reductions of a small-step operational semantics. By construction, every configuration can only reduce to finitely-many next configurations.

Given an initial configuration C, I would like to prove that if every execution starting from C gets stuck after a finite number of steps, then there are only finitely-many executions of C0.

I'm having quite a bit of difficulty getting my head round how to prove this. I can do it if I assume that the entire "↝" relation is well-founded, but that's too strong an assumption, since I need it to be possible for some executions to diverge, just not those that start from C.

I have a sense that my lemma, if it is indeed true, will have been proven before, perhaps in the context of graph theory, or computability theory.

I'd really appreciate any hints the Isabelle community might have for how I might prove this, or where/whether it has already been proven.

Thanks!
John

ps. In case more precision is appropriate...

I'm defining executions like this:

definition executions :: "config ⇒ (nat ⇒ config option) set"
where
"executions C ≡ {π. π 0 = Some C ∧ (∀i.
case π i of None ⇒ π (i+1) = None | Some C ⇒
if reduce C=[] then π (i+1) = None
else π (i+1) ∈ Some ` set (reduce C))}"

and my lemma is:

lemma
assumes "∀π ∈ executions C. ∃i > 0. finite_seq i π"
shows "finite (executions C)"

and I define finite_seq like so:

fun finite_seq where
"finite_seq 0 π = (∀i. π i = None)"
| "finite_seq (Suc i) π = (π 0 ≠ None ∧ finite_seq i (λi. π (Suc i)))"

Email Gateway (Aug 19 2022 at 14:47):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi John,

On 16/06/14 14:00, John Wickerson wrote:

I have a relation "↝" representing the reductions of a small-step operational semantics. By construction, every configuration can only reduce to finitely-many next configurations.

Given an initial configuration C, I would like to prove that if every execution starting from C gets stuck after a finite number of steps, then there are only finitely-many executions of C0.

I'm having quite a bit of difficulty getting my head round how to prove this. I can do it if I assume that the entire "↝" relation is well-founded, but that's too strong an assumption,
Your assumption is that all executions starting in C eventually get stuck. You can prove
that this is equivalent to the well-foundedness of ↝ restricted to the states reachable
from C. Then, you can use well-founded induction to show finiteness, probably similar to
what you already have.

To show well-foundedness, you can take the length of the longest execution starting in a
state as measure function.

Hope this helps,
Andreas

since I need it to be possible for some executions to diverge, just not those that
start from C.

I have a sense that my lemma, if it is indeed true, will have been proven before, perhaps in the context of graph theory, or computability theory.

I'd really appreciate any hints the Isabelle community might have for how I might prove this, or where/whether it has already been proven.

Thanks!
John

ps. In case more precision is appropriate...

I'm defining executions like this:

definition executions :: "config ⇒ (nat ⇒ config option) set"
where
"executions C ≡ {π. π 0 = Some C ∧ (∀i.
case π i of None ⇒ π (i+1) = None | Some C ⇒
if reduce C=[] then π (i+1) = None
else π (i+1) ∈ Some ` set (reduce C))}"

and my lemma is:

lemma
assumes "∀π ∈ executions C. ∃i > 0. finite_seq i π"
shows "finite (executions C)"

and I define finite_seq like so:

fun finite_seq where
"finite_seq 0 π = (∀i. π i = None)"
| "finite_seq (Suc i) π = (π 0 ≠ None ∧ finite_seq i (λi. π (Suc i)))"

Email Gateway (Aug 19 2022 at 14:47):

From: John Wickerson <johnwickerson@cantab.net>
Thanks very much for your reply Andreas.

I had actually tried the idea of using "well-foundedness of ↝ restricted to the states reachable from C", but couldn't make it work. I've just tried it again, encouraged by your suggestion, but I'm still struggling.

Specifically, I'm phrasing my lemma like this (↝* is an abbreviation I defined for the reflexive transitive closure of ↝):

lemma
assumes "wf {(C2,C1). C ↝* C1 ∧ C1 ↝ C2}"
shows "finite (traces C)"

I use wf_induct:

proof (rule wf_induct[OF assms])

That reduces the problem to the following (I've made the assumption slightly more readable):

fix C1
assume 1: "∀C2. C ↝* C1 ∧ C1 ↝ C2 ⟶ finite (traces C2)"
show "finite (traces C1)"

My specific problem is that before I can exploit fact "1", I need to show that C1 is indeed reachable from C. I simply don't have that fact anywhere!

Do you have any further tips that might help me? Many many thanks!

John

On 16 Jun 2014, at 13:57, Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch> wrote:

Hi John,

On 16/06/14 14:00, John Wickerson wrote:

I have a relation "↝" representing the reductions of a small-step operational semantics. By construction, every configuration can only reduce to finitely-many next configurations.

Given an initial configuration C, I would like to prove that if every execution starting from C gets stuck after a finite number of steps, then there are only finitely-many executions of C0.

I'm having quite a bit of difficulty getting my head round how to prove this. I can do it if I assume that the entire "↝" relation is well-founded, but that's too strong an assumption,
Your assumption is that all executions starting in C eventually get stuck. You can prove that this is equivalent to the well-foundedness of ↝ restricted to the states reachable from C. Then, you can use well-founded induction to show finiteness, probably similar to what you already have.

To show well-foundedness, you can take the length of the longest execution starting in a state as measure function.

Hope this helps,
Andreas

since I need it to be possible for some executions to diverge, just not those that start from C.

I have a sense that my lemma, if it is indeed true, will have been proven before, perhaps in the context of graph theory, or computability theory.

I'd really appreciate any hints the Isabelle community might have for how I might prove this, or where/whether it has already been proven.

Thanks!
John

ps. In case more precision is appropriate...

I'm defining executions like this:

definition executions :: "config ⇒ (nat ⇒ config option) set"
where
"executions C ≡ {π. π 0 = Some C ∧ (∀i.
case π i of None ⇒ π (i+1) = None | Some C ⇒
if reduce C=[] then π (i+1) = None
else π (i+1) ∈ Some ` set (reduce C))}"

and my lemma is:

lemma
assumes "∀π ∈ executions C. ∃i > 0. finite_seq i π"
shows "finite (executions C)"

and I define finite_seq like so:

fun finite_seq where
"finite_seq 0 π = (∀i. π i = None)"
| "finite_seq (Suc i) π = (π 0 ≠ None ∧ finite_seq i (λi. π (Suc i)))"

Email Gateway (Aug 19 2022 at 14:48):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi John,

On 16/06/14 16:48, John Wickerson wrote:

Thanks very much for your reply Andreas.

I had actually tried the idea of using "well-foundedness of ↝ restricted to the states reachable from C", but couldn't make it work. I've just tried it again, encouraged by your suggestion, but I'm still struggling.

Specifically, I'm phrasing my lemma like this (↝* is an abbreviation I defined for the reflexive transitive closure of ↝):

lemma
assumes "wf {(C2,C1). C ↝* C1 ∧ C1 ↝ C2}"
shows "finite (traces C)"

I use wf_induct:

proof (rule wf_induct[OF assms])

That reduces the problem to the following (I've made the assumption slightly more readable):

fix C1
assume 1: "∀C2. C ↝* C1 ∧ C1 ↝ C2 ⟶ finite (traces C2)"
show "finite (traces C1)"

My specific problem is that before I can exploit fact "1", I need to show that C1 is indeed reachable from C. I simply don't have that fact anywhere!
At the moment, your induction predicate is "%C. finite (traces C)". You have to generalise
it to arbitrary states reachable from C, i.e.,

lemma
assumes "wf {(C2,C1). C ↝* C1 ∧ C1 ↝ C2}"
and "C ↝* C1"
shows "finite (traces C1)"
using assms
proof(induction C1 rule: wf_induct_rule)

Do you have any further tips that might help me? Many many thanks!
Do not use any of the basic proof rules for wf to establish the well-foundedness
assumption. The resulting proof oblications are usually too complicated. Rather show that
the relation "{(C2,C1). C ↝* C1 ∧ C1 ↝ C2}" is a subset of "measure f" for some measure
function f on states (like the longest execution starting in the state as I suggested in
my previous mail). Then, you get well-foundedness from the rules wf_subset and wf_measure.

Andreas

On 16 Jun 2014, at 13:57, Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch> wrote:

Hi John,

On 16/06/14 14:00, John Wickerson wrote:

I have a relation "↝" representing the reductions of a small-step operational semantics. By construction, every configuration can only reduce to finitely-many next configurations.

Given an initial configuration C, I would like to prove that if every execution starting from C gets stuck after a finite number of steps, then there are only finitely-many executions of C0.

I'm having quite a bit of difficulty getting my head round how to prove this. I can do it if I assume that the entire "↝" relation is well-founded, but that's too strong an assumption,
Your assumption is that all executions starting in C eventually get stuck. You can prove that this is equivalent to the well-foundedness of ↝ restricted to the states reachable from C. Then, you can use well-founded induction to show finiteness, probably similar to what you already have.

To show well-foundedness, you can take the length of the longest execution starting in a state as measure function.

Hope this helps,
Andreas

since I need it to be possible for some executions to diverge, just not those that start from C.

I have a sense that my lemma, if it is indeed true, will have been proven before, perhaps in the context of graph theory, or computability theory.

I'd really appreciate any hints the Isabelle community might have for how I might prove this, or where/whether it has already been proven.

Thanks!
John

ps. In case more precision is appropriate...

I'm defining executions like this:

definition executions :: "config ⇒ (nat ⇒ config option) set"
where
"executions C ≡ {π. π 0 = Some C ∧ (∀i.
case π i of None ⇒ π (i+1) = None | Some C ⇒
if reduce C=[] then π (i+1) = None
else π (i+1) ∈ Some ` set (reduce C))}"

and my lemma is:

lemma
assumes "∀π ∈ executions C. ∃i > 0. finite_seq i π"
shows "finite (executions C)"

and I define finite_seq like so:

fun finite_seq where
"finite_seq 0 π = (∀i. π i = None)"
| "finite_seq (Suc i) π = (π 0 ≠ None ∧ finite_seq i (λi. π (Suc i)))"

Email Gateway (Aug 19 2022 at 14:48):

From: John Wickerson <johnwickerson@cantab.net>
Ha, it works! Thanks so much Andreas. I knew I had to generalise the induction hypothesis somehow, but just hadn't massaged the statement into quite the right form.

John

Email Gateway (Aug 19 2022 at 14:48):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi John,

I had the same concern, but I think that you could avoid the circularity by defining the
longest execution recursively. However, I meanwhile realised that you can show
well-foundedness more easily with the lemma finite_acyclic_wf (without going over the
longest execution). Acyclicity of the reachable graph should be easy to show because
otherwise, you have a loop and you could construct an infinite execution by looping. For
finiteness, you will need something like a Koenig's lemma to go from traces to states (If
every node in a connected graph has finitely many successors and there are infinitely many
nodes, then there is an infinite path). You can find an example of such a lemma (for an
undirected graph) in my AFP entry Coinductive (theory Koenigslemma).

Best,
Andreas

Last updated: Nov 21 2024 at 12:39 UTC