[Proof Ground 2020] Good Nodes

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.

(** * task 1*)
Lemma good_node_def i:
  good_node i <-> clos_refl_trans_1n _ E i 0.
Admitted.

(** * task 2*)
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.
Admitted.

(** * task 3*)
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.
Admitted.


Lemma good_node_characterization i:
  i < n
  -> good_node i <-> ~ (exists j, clos_refl_trans_1n _ E i j
                          /\ clos_trans_1n _ E j j).
Proof.
  split;eauto using good_node_characterisation_1,good_node_characterisation_2.
Qed.

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