提交 #18

import Mathlib.Tactic.Convert

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

variable {A : Type}

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

def is_symmetric (t : Tree A) : Prop := t = mirror t

def check_mirror : 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 : Tree A → Prop
  | Tree.leaf => True
  | Tree.node _ l r => check_mirror l r

lemma involutive_mirror : (@mirror A).Involutive := by
  intro t
  induction t with
  | leaf => rfl
  | node x l r hl hr =>
    change Tree.node x _ _ = _
    rw [hl, hr]

theorem check_mirror_correct (t₁ t₂ : Tree A) : check_mirror t₁ t₂ ↔ t₁ = mirror t₂ := by
  induction t₂ generalizing t₁ with
  | leaf =>
    change check_mirror t₁ Tree.leaf ↔ t₁ = Tree.leaf
    cases t₁ with
    | leaf => simp; trivial
    | node x₁ l₁ r₁ => simp; exact id
  | node x₂ l₂ r₂ hl₂ hr₂ =>
    cases t₁ with
    | leaf => change False ↔ _; simp [mirror]
    | node x₁ l₁ r₁ =>
      change x₁ = x₂ ∧ _ ↔ (_ = Tree.node x₂ _ _)
      rw [hl₂ r₁, hr₂ l₁]
      simp

theorem check_symmetric_correct (t : Tree A) : check_symmetric t ↔ is_symmetric t := by
  convert check_mirror_correct t t using 1
  cases t with
  | leaf => rfl
  | node x l r =>
    change check_mirror l r ↔ _ ∧ _ ∧ _
    simp [check_mirror_correct]
    intro lr
    rw [lr, involutive_mirror r]