test

import analysis.real 
import set_theory.zfc
import data.list
import data.fintype



namespace direct_graph


--open list
 
variables {α : Type }   







variables u v: α
variable graph: α × α → ℕ 



def vertices (graph: α × α → ℕ  ) : set α := λ u, ∃ v, graph(u,v)>0 ∨ graph(v,u)>0
def edges (graph: α × α → ℕ  ): set (α × α)  := λ e, graph e >0 

--def numbers_edges (graph: α × α → ℕ  ): ℕ   := λ e, graph e >0 




definition path : list (α × α)→ Prop  
| []              := tt
| [a]             := tt 
| (a :: b :: l) := a.2= b.1 









definition walk_in_graph :( α × α → ℕ  ) →  list (α × α × ℕ )→ Prop
| graph      []              := tt
| graph      [a]             := (graph (a.1,a.2.1)≥ a.2.2)/\ (a.2.2≥ 0) 
| graph      (a :: b :: l)   := (a.1= b.2.1)    
                               ∧ (graph (a.1,a.2.1)≥ a.2.2)/\ (a.2.2≥ 0) 
                               ∧ (graph (b.1,b.2.1)≥ b.2.2)/\ (b.2.2≥ 0)


definition cycle_in_graph [inhabited (α × α × ℕ )] (graph: α × α → ℕ ) (l : list (α × α × ℕ )) (h : l ≠ list.nil) : Prop 
 := walk_in_graph graph l  /\ (list.head l).1 = (list.last l h).2.1  








definition  count_in_list [decidable_eq α] : (α × α × ℕ ) → list (α × α × ℕ )→ ℕ  
| a     []        := 0
| a     (b :: l)   :=   if a = b then 
                      (count_in_list a l)+1 
                    else count_in_list a l 


definition  count_lists [decidable_eq α]:  list (α × α × ℕ )→ ℕ  
| []       := 0
| (a :: b) := count_in_list a (a::b) + count_lists b


definition  is_unique [decidable_eq α]:  list (α × α × ℕ )→ bool :=λ l, count_lists l= list.length l

def to_set : list α → set α 
|[] :=∅
| (h::t) := {h} ∪ to_set t


def Euler_walk [decidable_eq α] (graph: α × α → ℕ ) (l : list (α × α × ℕ )) : Prop
:= is_unique l ∧ walk_in_graph graph l ∧ 
   (∀ u v n, graph(u,v)≥ n ∧ n≥ 1 → (u,v,n)∈ to_set l ) 

def Euler_cycle [inhabited (α × α × ℕ )] [decidable_eq α] (graph: α × α → ℕ ) (l : list (α × α × ℕ ))  (h : l ≠ list.nil): Prop
:=  is_unique l ∧ cycle_in_graph graph l h ∧
    (∀ u v n, graph(u,v)≥ n ∧ n≥ 1 → (u,v,n)∈ to_set l ) 


def is_Eulerian [inhabited (α × α × ℕ )] [decidable_eq α](graph: α × α → ℕ ) :Prop 
:= ∃ l (h : l ≠ list.nil), Euler_cycle graph l h




definition undirected_graph ( graph:α × α → ℕ  ): Prop := 
       ∀ u v:α, graph(u,v)=graph(v,u)



def Euler_walk_in_undirected_graph [decidable_eq α](graph: α × α → ℕ ) (l : list (α × α × ℕ )) : Prop
:= is_unique l ∧ walk_in_graph graph l ∧ 
    (∀ u v n, (u,v,n)∈ to_set l → (u,v,n)∉  to_set l )  ∧
    (∀ u v n, graph(u,v)≥ n ∧ n≥ 1 → (u,v,n)∈ to_set l ∨ (v,u,n)∈ to_set l ) 
    

def Euler_cycle_in_undirected_graph [inhabited (α × α × ℕ )] [decidable_eq α](graph: α × α → ℕ ) (l : list (α × α × ℕ ))  (h : l ≠ list.nil): Prop
:= is_unique l ∧ cycle_in_graph graph l h ∧
   (∀ u v n, (u,v,n)∈ to_set(l) → (u,v,n)∉  to_set(l) ) ∧ 
   (∀ u v n, graph(u,v)≥ n ∧ n≥ 1 → (u,v,n)∈ to_set l ∨ (v,u,n)∈ to_set l )  


def is_Eulerian_in_undirected_graph [inhabited (α × α × ℕ )] [decidable_eq α](graph: α × α → ℕ ) :Prop 
:= ∃ l (h : l ≠ list.nil), Euler_cycle_in_undirected_graph graph l h

def invertex (graph: α × α → ℕ ) (u:α ): set (α × α × ℕ )  
:= λ e,  graph(e.1,e.2.1)≥ e.2.2 ∧ e.2.2≥ 1 ∧  e.2.1=u




def outvertex (graph: α × α → ℕ ) (u:α ): set (α × α × ℕ )  
:= λ e,  graph(e.1,e.2.1)≥ e.2.2 ∧ e.2.2≥ 1 ∧  e.1=u


def same_degree (graph: α × α → ℕ ) (u:α ):Prop
:= ∃ (f:outvertex graph u → invertex graph u) (g: invertex graph u → outvertex graph u), (∀ v, f (g v) =v)∧ (∀ v, g (f v)= v) 

def orientation (graph:α × α → ℕ ) :set(α × α → ℕ) 
:=  λ f, ∀e, f e +f (e.2,e.1) = graph e 



def Eulerian_orientation [inhabited (α × α × ℕ )] [decidable_eq α](graph: α × α → ℕ ): Prop 
:= undirected_graph graph ∧ 
   (∃ G:α × α → ℕ, G ∈ orientation graph ∧  
                (∀ u:vertices G, same_degree G u) ∧ 
                is_Eulerian G 
    )
                 




definition strong_orientation [inhabited (α × α × ℕ )] (graph:α × α → ℕ ):Prop 
:= undirected_graph graph ∧
   (∃ G:α × α → ℕ, G ∈ orientation graph ∧  
        (∀ u v:vertices G, 
                 ∃ l (h : l ≠ list.nil), walk_in_graph G l ∧ 
                                   (list.head l).1=u /\ 
                                   (list.last l h).2.1=v
        )
   )    









#check invertex

#check Euler_walk_in_undirected_graph
#check walk_in_graph
#check Euler_walk
#check Euler_cycle
#check count_in_list 




#reduce ((λ   (x y:α),  x=y) u u )∨ true     

#check walk_in_graph 
#check path




#check graph
#check  ∃ v, graph(u,v)>0 ∨ graph(v,u)>0
#check tt 
#check   vertices




end direct_graph














--import data.fintype

variables {α : Type}

def invertex (graph: α × α → ℕ ) (u:α ): set (α × α × ℕ )  
:= λ e,  graph(e.1,e.2.1)≥ e.2.2 ∧ e.2.2≥ 1 ∧  e.2.1=u


instance [fintype  (α × α × ℕ ) ] [decidable_eq α ] (graph : α × α  → ℕ) (u : α ) : fintype (invertex graph u) :=
by unfold invertex; apply_instance

def indegree [fintype  (α × α × ℕ ) ] [decidable_eq α ] (graph : α × α  → ℕ) (u : α ) : ℕ :=
fintype.card (invertex graph u)

def outvertex (graph: α × α → ℕ ) (u:α ): set (α × α × ℕ )  
:= λ e,  graph(e.1,e.2.1)≥ e.2.2 ∧ e.2.2≥ 1 ∧  e.1=u


instance [fintype  (α × α × ℕ ) ] [decidable_eq α ] (graph : α × α  → ℕ) (u : α ) : fintype (outvertex graph u) :=
by unfold outvertex; apply_instance

def outdegree [fintype  (α × α × ℕ ) ] [decidable_eq α ] (graph : α × α  → ℕ) (u : α ) : ℕ :=
fintype.card (outvertex graph u)