Lean: Walk implies Path

This is some code I wrote as part of a "formalize something in Lean" assignment for CMU's Interactive Theorem Proving course in Spring 2019. It wouldn't have been possible without the assistance of Professor Jeremy Avigad and course TA Mario Carneiro during office hours.

After setting up Lean on my Mac OS system I created a new Lean project using the directions from the Lean Community's Using leanproject page. The name of the project doesn't really matter.

I put the code below in a file graph.lean within the project's src directory.

import data.list.basic
import data.list.nodup
import data.nat.basic

/- 
I defined a *graph* as a binary relation between elements of a vertex set α. I
believe this definition corresponds to infinite directed graphs where self-edges
are possible.

Then I defined the notion of a *walk* from vertex a to vertex b, which is just a
sequence of movements along edges that one can follow to reach vertex b from
vertex a. 

Next, I defined a *path* as a walk with no repeated vertices.

The main theorem that I proved was "if there is a walk from vertex a to vertex b
in graph g then there is also a path from vertex a to vertex b in g", the others
are intermediate results. 
-/

def graph (α : Type) [decidable_eq α] := (α → α → Prop)

inductive walk {α : Type} [decidable_eq α] (g : graph α) (a : α) : list α → α → Prop
| one  : walk [] a
| cons {b c : α} {l : list α} : walk l b → g b c → walk (b :: l) c

def path {α : Type} [decidable_eq α] (g : graph α) (a : α) (l : list α) (b : α) : Prop := 
  walk g a l b ∧ (b :: l).nodup

def walk_of_walk_mem_drop_index_of {α : Type} [decidable_eq α] 
  {g : graph α} {a : α} {l : list α} {d : α} :
    walk g a l d → ∀ (c : α), c ∈ l → walk g a (list.drop (1 + list.index_of c l) l) c := 
begin
  intros w_ad c c_in_l
, induction w_ad
, case walk.one :
  { simp * at * }
, case walk.cons :
  { rename l      l_ad 
  , rename w_ad_b b
  , rename w_ad_l l_ab
  , rename w_ad_a w_ab
  , rw list.index_of
  , rw list.find_index
  , by_cases (c = b)
  , { simp * at * }
  , { simp * at * 
    , rw list.index_of at w_ad_ih
    , assumption
    }
  }
end

def not_mem_of_nodup_mem_drop_index_of {α : Type} [decidable_eq α] {l : list α} {b : α} : 
  list.nodup l → b ∈ l → b ∉ list.drop (1 + list.index_of b l) l :=
  begin
    assume nodup_l
  , assume in_l
  , induction l with x xs
  , case list.nil : 
    { simp }
  , case list.cons : 
    { have b_eq_x_or_neq_x_and_in_xs, from list.eq_or_ne_mem_of_mem in_l
    , apply or.elim b_eq_x_or_neq_x_and_in_xs
    , { assume eq_b_x
      , rw list.index_of
      , rw list.find_index
      , apply list.not_mem_of_nodup_cons
      , simp * at *
      }
    , { assume b_neq_x_and_in_xs
      , have b_in_xs, from b_neq_x_and_in_xs.right
      , have nodup_xs, from and.right (list.nodup_cons.mp nodup_l)
      , have ih, from l_ih nodup_xs b_in_xs
      , simp * at *
      }
    }
  end

def sublist_path {α : Type} [decidable_eq α] {g : graph α} {a : α} {l : list α} {c : α} :
  path g a l c → ∀ (b : α), b ∈ l → ∃ (l' : list α), l' <:+ l ∧ path g a l' b :=
  begin
    assume path_ac
  , intro b
  , assume in_l_b
  , existsi (list.drop (1 + list.index_of b l) l)
  , split
  , { apply list.drop_suffix }
  , { rw path
    , split
    , { apply walk_of_walk_mem_drop_index_of path_ac.left
      , assumption
      }
    , { simp [list.nodup]
      , split
      , { apply not_mem_of_nodup_mem_drop_index_of
        , { exact and.right (list.nodup_cons.mp path_ac.right) }
        , assumption
        }
      , { apply list.nodup_of_sublist  
        , { apply list.sublist_of_suffix 
          , apply list.drop_suffix
          }
        , { exact and.right (list.nodup_cons.mp path_ac.right)
          }
        }
      }
    }
  end

def path_walk {α : Type} [decidable_eq α] {g : graph α} {a : α} : Π {l : list α} {c : α}, 
  walk g a l c → ∃ l', path g a l' c := 
  begin
    intros l_ac c walk_ac
  , induction walk_ac
  , case walk.one :
    { existsi ([] : list α)
    , rw path
    , constructor
    , { exact walk.one }
    , { simp }
    }
  , case walk.cons :
    { rename walk_ac_c c, rename walk_ac_b b, rename walk_ac_a_1 edge_bc
    , rename walk_ac_l l_ab, rename walk_ac_a walk_ab, rename walk_ac_ih ih
    , cases ih with l_ab' path_ab
    , by_cases c ∈ (b :: l_ab')
    , { simp [(∈)] at h
      , rw [list.mem] at h
      , apply or.elim h
      , { assume eq_b_c
        , rw eq_b_c
        , existsi l_ab' 
        , exact path_ab
        }
      , { assume mem_l_ab'_c
        , have anonymous, from sublist_path path_ab c mem_l_ab'_c 
        , cases anonymous with l_ac' path_ac
        , existsi l_ac'
        , rw path
        , split
        , { exact path_ac.right.left }
        , { apply path_ac.right.right }
        }
      }
    , { existsi (b :: l_ab')
      , rw path at path_ab
      , rw path
      , constructor 
      , { exact walk.cons path_ab.left edge_bc }
      , { simp * at * }
      }
    }
  end