terrible_tree_code.lean

def followablePaths : Tree α → List Path
  | nil => []
  | node _ l r => List.map Path.right (followablePaths r)
                  ++ List.map Path.left (followablePaths l)
                  ++ [Path.here]

lemma followablePaths_order : ∀ (p q : Path) (t : Tree α),
    List.Sublist ({p, q} : List Path) (followablePaths t)
    ↔ (p.validFor t ∧ q.validFor t
      ∧ (q ≤ p ∨ (p ⊓ q ++ Path.left Path.here ≤ q
                  ∧ p ⊓ q ++ Path.right Path.here ≤ p))) :=
  have lem0 {t : Tree α} {p q : Path} :
      List.Sublist [p, q] (followablePaths t) → p.validFor t ∧ q.validFor t :=
    by refine ?_ ∘ List.Sublist.subset
       simp only [List.cons_subset, mem_followablePaths_iff_validFor,
                  List.nil_subset, and_true, imp_self]
  have lem1 (p q r : Path) : ¬ List.Sublist [p, q] [r]
    | List.Sublist.cons   x h => List.cons_ne_nil _ _ $ List.sublist_nil.mp h
    | List.Sublist.cons₂  x h => List.cons_ne_nil _ _ $ List.sublist_nil.mp h
  have lem2 (t : Tree α) p (h : p ≠ Path.here) :
      List.Sublist [p, Path.here] (followablePaths t)
      ↔ p.validFor t := by
    refine ⟨And.left ∘ lem0, ?_⟩
    intro h'; revert h; rw [← Decidable.or_iff_not_imp_left]; revert h'
    cases t <;> cases p
    <;> simp only [Path.validFor, true_or, false_or, forall_true_left,
                    IsEmpty.forall_iff, followablePaths]
    <;> rw [← List.singleton_append]
    <;> intro h <;> refine List.Sublist.append ?_ (List.Sublist.refl [Path.here])
    <;> simp only [List.singleton_sublist, List.mem_append, List.mem_map,
                  mem_followablePaths_iff_validFor, and_false, exists_const,
                  Path.left.injEq, Path.right.injEq, exists_eq_right,
                  false_or, or_false] <;> assumption
  have lem3 (t : Tree α) q :
      ¬ List.Sublist [Path.here, q] (followablePaths t) := by
    cases t
    <;> simp only [followablePaths, List.append_assoc, List.mem_map, or_self,
                   List.pair_sublist_append, and_false, exists_const, false_or,
                   List.mem_append, Path.left.injEq, exists_eq_right, not_or,
                   List.mem_singleton, or_false, false_and, and_self, lem1,
                   List.sublist_nil, not_false_eq_true]
    constructor
    <;> refine mt List.Sublist.subset ?_
    <;> simp only [List.cons_subset, List.mem_map, and_false, exists_const,
                   Path.left.injEq, exists_eq_right, List.nil_subset, and_true,
                   false_and, not_false_eq_true]
  have lem4 (t : Tree α) p q :
      ¬ List.Sublist [Path.left p, Path.right q] (followablePaths t) := by
    cases t
    <;> simp only [followablePaths, List.append_assoc, List.pair_sublist_append, List.mem_map,
                   and_false, exists_const, List.mem_append, List.mem_singleton, or_self, and_self,
                   Path.left.injEq, exists_eq_right, lem1, or_false, false_or, not_or, List.sublist_nil]
    constructor
    <;> refine mt List.Sublist.subset ?_
    <;> simp only [List.cons_subset, List.mem_map, Path.left.injEq, exists_eq_right, and_false,
                   exists_const, List.nil_subset, and_true, not_false_eq_true, false_and]
  have lem5 (t : Tree α) p q :
      List.Sublist [Path.right p, Path.left q] (followablePaths t)
      ↔ (Path.validFor (Path.right p) t ∧ Path.validFor (Path.left q) t) := by
    refine ⟨lem0, ?_⟩
    cases t
    <;> simp only [Path.validFor, followablePaths, List.pair_sublist_append,
                   List.mem_map, mem_followablePaths_iff_validFor, Path.right.injEq,
                   List.mem_append, Path.left.injEq, List.mem_singleton, or_false,
                   and_self, false_or, List.sublist_nil, IsEmpty.forall_iff, or_assoc,
                   exists_eq_right, and_false, exists_const]
    exact Or.inr ∘ Or.inl
  have lem6 a (l r : Tree α) p q :
      List.Sublist [Path.left p, Path.left q] (followablePaths (node a l r))
      ↔ List.Sublist [p, q] (followablePaths l) := by
    simp only [followablePaths, List.append_assoc, List.pair_sublist_append,
               List.mem_map, and_false, exists_const, List.mem_append,
               Path.left.injEq, exists_eq_right, List.mem_singleton, or_false,
               false_and, false_or, lem1]
    rw [or_iff_right]
    . refine @List.Sublist.map_inj _ _ Path.left ?_ [p, q] _
      intro _ _; exact Eq.mp (Path.left.injEq _ _)
    . refine mt List.Sublist.subset ?_
      simp only [List.cons_subset, List.mem_map, and_false, exists_const,
                 List.nil_subset, and_true, and_self, not_false_eq_true]
  have lem7 a (l r : Tree α) p q :
      List.Sublist [Path.right p, Path.right q] (followablePaths (node a l r))
      ↔ List.Sublist [p, q] (followablePaths r) := by
    simp only [followablePaths, List.append_assoc, List.pair_sublist_append,
               List.mem_map, and_false, exists_const, List.mem_append,
               Path.right.injEq, exists_eq_right, List.mem_singleton, or_false,
               false_and, false_or, lem1]
    rw [or_iff_left]
    . refine @List.Sublist.map_inj _ _ Path.right ?_ [p, q] _
      intro _ _; exact Eq.mp (Path.right.injEq _ _)
    . refine mt List.Sublist.subset ?_
      simp only [List.cons_subset, List.mem_map, and_false, exists_const,
                 List.nil_subset, and_true, and_self, not_false_eq_true]
  by dsimp only [Inf.inf]
     intros p q t
     rw [List.doubleton_eq']
     split_ifs with h
     . simp only [h, List.singleton_sublist, mem_followablePaths_iff_validFor,
                  le_refl, inf_of_le_left, true_or, and_true, and_self]
     rw [← and_assoc, ← and_iff_right_of_imp lem0, and_congr_right_iff, and_imp]
     revert h p q
     induction' t with a l r ihₗ ihᵣ <;> intro p q h
     . simp only [Path.validFor, IsEmpty.forall_iff, implies_true]
     . intro hp hq
       cases' q with q q
       . simp only [ne_eq, h, hp, not_false_eq_true, lem2, Path.here_le,
                    inf_of_le_right, Path.not_left_le_here, false_and,
                    or_false, true_iff, true_or]
       all_goals cases' p with p p
       all_goals simp only
         [Path.not_left_le_here, Path.longestCommonPrefix, false_or,
          Path.here_append, Path.left_le_left_iff_le, Path.not_right_le_left,
          and_false, or_self, Path.not_right_le_here, Path.not_left_le_right,
          Path.here_le, true_and, and_self, Path.right_le_right_iff_le,
          iff_true, true_iff, true_or, lem3, lem4, lem5, lem6, lem7]
       . refine Iff.trans (ihₗ p q (Path.left.injEq p q ▸ h) hp hq) (or_congr_right ?_)
         simp only [Path.left_append, Path.left_le_left_iff_le]
       . constructor <;> assumption
       . refine Iff.trans (ihᵣ p q (Path.right.injEq p q ▸ h) hp hq) (or_congr_right ?_)
         simp only [Path.right_append, Path.right_le_right_iff_le]