Theorem: LoVe.IsFull_mirror_struct_induct (LoVe/Lectures/LoVe06_InductivePredicates_Demo.lean)

State before:
α : Type
t : BTree α
⊢ IsFull t → IsFull (mirror t)
Tactic:
induction t with
| empty                =>
  { intro ht
    exact ht }
| node a l r ih_l ih_r =>
  { intro ht
    cases ht with
    | node _ _ _ hl hr hiff =>
      { rw [mirror]
        apply IsFull.node
        { exact ih_r hr }
        { apply ih_l hl }
        { simp [mirror_Eq_empty_Iff, *] } } }
State after:
no goals

State before:
case empty
α : Type
⊢ IsFull BTree.empty → IsFull (mirror BTree.empty)
Tactic:
intro ht
State after:
case empty
α : Type
ht : IsFull BTree.empty
⊢ IsFull (mirror BTree.empty)

State before:
case empty
α : Type
ht : IsFull BTree.empty
⊢ IsFull (mirror BTree.empty)
Tactic:
exact ht
State after:
no goals

State before:
case node
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
⊢ IsFull (BTree.node a l r) → IsFull (mirror (BTree.node a l r))
Tactic:
intro ht
State after:
case node
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
ht : IsFull (BTree.node a l r)
⊢ IsFull (mirror (BTree.node a l r))

State before:
case node
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
ht : IsFull (BTree.node a l r)
⊢ IsFull (mirror (BTree.node a l r))
Tactic:
cases ht with
| node _ _ _ hl hr hiff =>
  { rw [mirror]
    apply IsFull.node
    { exact ih_r hr }
    { apply ih_l hl }
    { simp [mirror_Eq_empty_Iff, *] } }
State after:
no goals

State before:
case node.node
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ IsFull (mirror (BTree.node a l r))
Tactic:
rw [mirror]
State after:
case node.node
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ IsFull (BTree.node a (mirror r) (mirror l))

State before:
case node.node
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ IsFull (BTree.node a (mirror r) (mirror l))
Tactic:
apply IsFull.node
State after:
case node.node.hl
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ IsFull (mirror r)

case node.node.hr
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ IsFull (mirror l)

case node.node.hiff
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty

State before:
case node.node.hl
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ IsFull (mirror r)

case node.node.hr
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ IsFull (mirror l)

case node.node.hiff
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty
Tactic:
{ exact ih_r hr }
State after:
case node.node.hr
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ IsFull (mirror l)

case node.node.hiff
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty

State before:
case node.node.hr
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ IsFull (mirror l)

case node.node.hiff
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty
Tactic:
{ apply ih_l hl }
State after:
case node.node.hiff
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty

State before:
case node.node.hiff
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty
Tactic:
{ simp [mirror_Eq_empty_Iff, *] }
State after:
no goals

State before:
case node.node.hl
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ IsFull (mirror r)
Tactic:
exact ih_r hr
State after:
no goals

State before:
case node.node.hr
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ IsFull (mirror l)
Tactic:
apply ih_l hl
State after:
no goals

State before:
case node.node.hiff
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty
Tactic:
simp [mirror_Eq_empty_Iff, *]
State after:
no goals