Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

# [Proof Ground 2020] Good Nodes

We are given a list of natural numbers `L`, for instance: ``` 0 0 1 5 2 6 3 ``` We will denote list indices as "nodes". A node `i` is *good* iff: - `i = 0`, - or `L[i] = j` and `j` is a good node. In a programming problem, we would now ask you to find an algorithm that computes the minimal number of changes that need to be made to `L` such that every index is a good node. We are giving away the solution directly and instead ask you to prove the main ideas for its correctness. We can read `L` as a directed graph: ``` ------> 0<-1<-2 3 4 5->6 ^------ | ^--------- 0 0 1 5 2 6 3 ``` **Task 1**: Show that a node in the graph can reach `0` iff it is a good node. **Tasks 2&3**: The key insight for the algorithm is to see that any node either reaches or is part of a cycle, or it is a good node. Prove this. It should now also be clear how to compute the solution. Submitted by: Simon Wimmer Coq: Fabian Kunze | Lean: Simon Hudon & Kevin Kappelmann | Isabelle: Simon Wimmer

## Resources

### Definitions File

```theory Defs
imports Main
begin

axiomatization graph :: "nat list" where
wellformed: "\<forall>i < length graph. graph ! i < length graph"

definition
"n \<equiv> length graph"

definition
"E i j \<equiv> i < n \<and> j < n \<and> i > 0 \<and> graph ! i = j"

inductive good_node where
"good_node 0"
| "good_node i" if "good_node j" "E i j"

end```

### Template File

```theory Submission
imports Defs
begin

theorem good_node_def:
"good_node i \<longleftrightarrow> E\<^sup>*\<^sup>* i 0"
sorry

theorem good_node_characterization_1:
assumes "i < n" "i > 0" "good_node i"
shows "\<not> (\<exists>j. E\<^sup>*\<^sup>* i j \<and> E\<^sup>+\<^sup>+ j j)"
sorry

theorem good_node_characterization_2:
assumes "i < n" "i > 0" "\<not> (\<exists>j. E\<^sup>*\<^sup>* i j \<and> E\<^sup>+\<^sup>+ j j)"
shows "good_node i"
sorry

corollary good_node_characterization:
assumes "i < n" "i > 0"
shows "good_node i \<longleftrightarrow> \<not> (\<exists>j. E\<^sup>*\<^sup>* i j \<and> E\<^sup>+\<^sup>+ j j)"
using good_node_characterization_1 good_node_characterization_2 assms by blast

end```

### Check File

```theory Check
imports Submission
begin

theorem good_node_def:
"good_node i \<longleftrightarrow> E\<^sup>*\<^sup>* i 0"
by (rule Submission.good_node_def)

theorem good_node_characterization_1:
"i < n \<Longrightarrow> i > 0 \<Longrightarrow> good_node i \<Longrightarrow> \<not> (\<exists>j. E\<^sup>*\<^sup>* i j \<and> E\<^sup>+\<^sup>+ j j)"
by (rule Submission.good_node_characterization_1)

theorem good_node_characterization_2:
"i < n \<Longrightarrow> i > 0 \<Longrightarrow> \<not> (\<exists>j. E\<^sup>*\<^sup>* i j \<and> E\<^sup>+\<^sup>+ j j) \<Longrightarrow> good_node i"
by (rule Submission.good_node_characterization_2)

end```

### Definitions File

```import logic.relation

def wellformed (graph : list ℕ) : Prop :=
∀ {i : ℕ} (i_lt_length : i < graph.length), graph.nth_le i i_lt_length < graph.length

def E (graph : list ℕ) (i j : ℕ) : Prop :=
(i < graph.length) ∧ (j < graph.length) ∧ i > 0 ∧ graph.nth i = some j

inductive good_node (graph : list ℕ) : ℕ → Prop
| init : good_node 0
| step (i j : ℕ) : good_node j → E graph i j → good_node i

----------------------just some definitions to prevent cheating------------------------

def good_node_def_prop := ∀ {graph : list ℕ} (graph_wf : wellformed graph) (i : ℕ),
good_node graph i ↔ relation.refl_trans_gen (E graph) i 0

notation `good_node_def_prop` := good_node_def_prop

def good_node_characterization_1_prop := ∀ {graph : list ℕ} (graph_wf : wellformed graph) {i n : ℕ} (i_lt_n : i < n) (i_pos : 0 < i)
(good_node_i : good_node graph i), ¬∃ j, relation.refl_trans_gen (E graph) i j ∧ relation.trans_gen (E graph) j j

notation `good_node_characterization_1_prop` := good_node_characterization_1_prop

def good_node_characterization_2_prop := ∀ {graph : list ℕ} (graph_wf : wellformed graph) {i n : ℕ} (i_lt_n : i < n) (i_pos : 0 < i)
(hyp : ¬∃ j, relation.refl_trans_gen (E graph) i j ∧ relation.trans_gen (E graph) j j), good_node graph i

notation `good_node_characterization_2_prop` := good_node_characterization_2_prop```

### Template File

```import .defs

import tactic.finish

lemma good_node_def : ∀ (i : ℕ), good_node i ↔ relation.refl_trans_gen E i 0 :=
sorry

lemma good_node_characterization_1 : ∀ {i n : ℕ} (i_lt_n : i < n) (i_pos : 0 < i)
(good_node_i : good_node i), ¬∃ j, relation.refl_trans_gen E i j ∧ relation.trans_gen E j j :=
sorry

lemma good_node_characterization_2 : ∀ {i n : ℕ} (i_lt_n : i < n) (i_pos : 0 < i)
(hyp : ¬∃ j, relation.refl_trans_gen E i j ∧ relation.trans_gen E j j), good_node i :=
sorry```

### Check File

```import .defs
import .submission

lemma check_good_node_def : good_node_def_prop :=
@good_node_def

lemma check_good_node_characterization_1 : good_node_characterization_1_prop :=
@good_node_characterization_1

lemma check_good_node_characterization_2 : good_node_characterization_2_prop :=
@good_node_characterization_2```

### Definitions File

```From Coq Require Export Lists.List.
Export List.ListNotations.
From Coq Require Export Relations.

Parameter G : list nat.
Axiom wellformed : forall i j, nth_error G i = Some j -> j < length G.
Definition n := length G.

Definition E i j :=
i < n
/\ j < n
/\ i > 0 /\ nth_error G i = Some j.

Inductive good_node : nat -> Prop :=
gn_base : good_node 0
| gn_step i j: good_node j -> E i j -> good_node i.
```

### Template File

```Require Import Defs.

Lemma good_node_def i:
good_node i <-> clos_refl_trans_1n _ E i 0.

Lemma good_node_characterisation_1 i:
good_node i
-> i < n
-> ~ exists j, clos_refl_trans_1n _ E i j
/\ clos_trans_1n _ E j j.

Lemma good_node_characterisation_2 i:
i < n
-> (~ exists j, clos_refl_trans_1n _ E i j
/\ clos_trans_1n _ E j j)
-> good_node i.