提交 #5

inductive Tree (A : Type) : Type where
  | leaf : Tree A
  | node : A → Tree A → Tree A → Tree A

def mirror {A : Type} : Tree A → Tree A
  | Tree.leaf => Tree.leaf
  | Tree.node x l r => Tree.node x (mirror r) (mirror l)

def is_symmetric {A : Type} (t : Tree A) : Prop :=
  t = mirror t

def check_mirror {A : Type} : Tree A → Tree A → Prop
  | Tree.leaf, Tree.leaf => True
  | Tree.node x1 l1 r1, Tree.node x2 l2 r2 =>
      (x1 = x2) ∧ check_mirror l1 r2 ∧ check_mirror r1 l2
  | _, _ => False

def check_symmetric {A : Type} : Tree A → Prop
  | Tree.leaf => True
  | Tree.node _ l r => check_mirror l r

theorem check_mirror_correct {A : Type} (t1 t2 : Tree A) :
    check_mirror t1 t2 ↔ t1 = mirror t2 := by
  induction t1 generalizing t2 with
  | leaf =>
    constructor
    · intro h
      cases t2 with
      | leaf => rfl
      | node => simp [check_mirror] at h
    · intro h
      cases t2 with
      | leaf => trivial
      | node => simp [mirror] at h
  | node x l1 r1 ih_l ih_r =>
    constructor
    · intro h
      cases t2 with
      | leaf => simp [check_mirror] at h
      | node y l2 r2 =>
        rcases h with ⟨hxy, hl, hr⟩
        rw [show x = y from hxy]
        simp [mirror]
        constructor
        · rw [<- ih_l]
          assumption
        · rw [<- ih_r]
          assumption
    · intro h
      cases t2 with
      | leaf => simp [mirror] at h
      | node y l2 r2 =>
        simp [mirror] at h
        rcases h with ⟨rfl, h1, h2⟩
        simp [check_mirror]
        constructor
        · rw [ih_l]
          assumption
        · rw [ih_r]
          assumption

theorem mirror_mirror_eq {A : Type} (t : Tree A) :
    t = mirror (mirror t) := by
  induction t with
  | leaf => rfl
  | node x l r ih_l ih_r =>
    simp [mirror]
    constructor <;> assumption


theorem check_symmetric_correct {A : Type} (t : Tree A) :
    check_symmetric t ↔ is_symmetric t := by
  constructor
  · intro h
    unfold is_symmetric
    cases t with
    | leaf => rfl
    | node x l r =>
      unfold check_symmetric at h
      have := (check_mirror_correct l r).mp h
      rw [this]
      simp [mirror]
      rw [<- mirror_mirror_eq]
  · intro h
    unfold is_symmetric at h
    cases t with
    | leaf => trivial
    | node x l r =>
      unfold check_symmetric
      apply (check_mirror_correct l r).mpr
      simp [mirror] at h
      rcases h with ⟨h1, h2⟩
      assumption