bhavik.lean

import tactic

inductive word₀
| blank : word₀
| concat : word₀ → word₀ → word₀

open word₀
infixr ` □ `:80 := concat

@[simp] lemma ne_concat_self_left : ∀ u v, u ≠ u □ v
| blank    v h := word₀.no_confusion h
| (u □ u') v h := ne_concat_self_left u u' (by injection h)

@[simp] lemma ne_concat_self_right : ∀ u v, v ≠ u □ v
| u blank    h := word₀.no_confusion h
| u (v □ v') h := ne_concat_self_right v v' (by injection h)

@[simp] lemma concat_ne_self_right (u v : word₀) : u □ v ≠ v :=
(ne_concat_self_right _ _).symm

@[simp] lemma concat_ne_self_left (u v : word₀) : u □ v ≠ u :=
(ne_concat_self_left _ _).symm

inductive hom₀ : word₀ → word₀ → Sort*
| α_hom : ∀ (u v w : word₀), hom₀ ((u □ v) □ w) (u □ (v □ w))
| α_inv : ∀ (u v w : word₀), hom₀ (u □ (v □ w)) ((u □ v) □ w)
| tensor_id : ∀ {u v} (w), hom₀ u v → hom₀ (u □ w) (v □ w)
| id_tensor : ∀ (u) {v w}, hom₀ v w → hom₀ (u □ v) (u □ w)

inductive hom₀.is_directed : ∀ {v w}, hom₀ v w → Prop
| α : ∀ {u v w}, hom₀.is_directed (hom₀.α_hom u v w)
| tensor_id : ∀ (u) {v w} (s : hom₀ v w), hom₀.is_directed s → 
  hom₀.is_directed (hom₀.tensor_id u s) 
| id_tensor : ∀ {u v} (w) (s : hom₀ u v), hom₀.is_directed s → 
  hom₀.is_directed (hom₀.id_tensor w s) 

lemma hom₀.ne {u v} (s : hom₀ u v) : u ≠ v :=
begin
  induction s,
  { simp },
  { simp },
  { simp * },
  { simp * }
end 

lemma hom₀.subsingleton :
  ∀ {u v u' v'} (hu : u = u') (hv : v = v') 
    (s : hom₀ u v) (s' : hom₀ u' v'), s.is_directed → 
    s'.is_directed → s == s' :=
begin
  assume u v u' v' hu hv s s' hs hs',
  induction hs generalizing u' v',
  { cases hs',
    { simp only at hu hv,
      rcases hu with ⟨⟨rfl, rfl⟩, rfl⟩,
      refl },
    { simp only at hu hv,
      rcases hu with ⟨rfl, rfl⟩,
      simp * at * },
    { simp only at hu hv,
      rcases hu with ⟨rfl, rfl⟩,
      simp * at * } },
  { cases hs',
    { simp only at hu hv,
      rcases hu with ⟨⟨rfl, rfl⟩, rfl⟩,
      simp * at * },
    { simp only at hu hv,
      rcases hu with ⟨rfl, rfl⟩,
      rcases hv with ⟨rfl, _⟩,
      simp only [heq_iff_eq],
      rw [← heq_iff_eq],
      exact hs_ih rfl rfl _ (by assumption) },
    { simp only at hu hv,
      rcases hu with ⟨rfl, rfl⟩,
      rcases hv with ⟨rfl, rfl⟩,
      exact (hom₀.ne hs'_s rfl).elim } },
  { cases hs',
    { simp only at hu hv,
      rcases hu with ⟨⟨rfl, rfl⟩, rfl⟩,
      simp * at * },
    { simp only at hu hv,
      rcases hu with ⟨rfl, rfl⟩,
      rcases hv with ⟨rfl, rfl⟩,
      exact (hom₀.ne hs'_s rfl).elim },
    { simp only at hu hv,
      rcases hu with ⟨rfl, rfl⟩,
      rcases hv with ⟨_, rfl⟩,
      simp only [heq_iff_eq],
      rw [← heq_iff_eq],
      exact hs_ih rfl rfl _ (by assumption) } }
end