Cookies disclaimer

I agree 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

Resources

Download Files

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
Download Files

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
Download Files

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.

Terms and Conditions