Theorem: normalize_correct (LoVe/Lectures/TacticStrategies.lean)

State before:
b : bexpr
⊢ normalize b = true ↔ interp b
Tactic:
induction b with
| atom a => cases' a <;> simp [normalize, interp]
| and a b iha ihb => simp [normalize, interp, *]
| or a b iha ihb => simp [normalize, interp, *]
| not b ih =>
  simp [normalize, interp]
  rw [Bool.eq_false_iff]
  tauto
| imp a b iha ihb =>
  simp [normalize, interp, ← iha, ← ihb]
  rw [Bool.eq_false_iff]
  tauto
State after:
no goals

State before:
case atom
a : Bool
⊢ normalize (atom a) = true ↔ interp (atom a)
Tactic:
cases' a <;> simp [normalize, interp]
State after:
no goals

State before:
case and
a b : bexpr
iha : normalize a = true ↔ interp a
ihb : normalize b = true ↔ interp b
⊢ normalize (bexpr.and a b) = true ↔ interp (bexpr.and a b)
Tactic:
simp [normalize, interp, *]
State after:
no goals

State before:
case or
a b : bexpr
iha : normalize a = true ↔ interp a
ihb : normalize b = true ↔ interp b
⊢ normalize (bexpr.or a b) = true ↔ interp (bexpr.or a b)
Tactic:
simp [normalize, interp, *]
State after:
no goals

State before:
case not
b : bexpr
ih : normalize b = true ↔ interp b
⊢ normalize (bexpr.not b) = true ↔ interp (bexpr.not b)
Tactic:
simp [normalize, interp]
State after:
case not
b : bexpr
ih : normalize b = true ↔ interp b
⊢ normalize b = false ↔ ¬interp b

State before:
case not
b : bexpr
ih : normalize b = true ↔ interp b
⊢ normalize b = false ↔ ¬interp b
Tactic:
rw [Bool.eq_false_iff]
State after:
case not
b : bexpr
ih : normalize b = true ↔ interp b
⊢ normalize b ≠ true ↔ ¬interp b

State before:
case not
b : bexpr
ih : normalize b = true ↔ interp b
⊢ normalize b ≠ true ↔ ¬interp b
Tactic:
tauto
State after:
no goals

State before:
case imp
a b : bexpr
iha : normalize a = true ↔ interp a
ihb : normalize b = true ↔ interp b
⊢ normalize (imp a b) = true ↔ interp (imp a b)
Tactic:
simp [normalize, interp, ← iha, ← ihb]
State after:
case imp
a b : bexpr
iha : normalize a = true ↔ interp a
ihb : normalize b = true ↔ interp b
⊢ normalize a = false ∨ normalize b = true ↔ normalize a = true → normalize b = true

State before:
case imp
a b : bexpr
iha : normalize a = true ↔ interp a
ihb : normalize b = true ↔ interp b
⊢ normalize a = false ∨ normalize b = true ↔ normalize a = true → normalize b = true
Tactic:
rw [Bool.eq_false_iff]
State after:
case imp
a b : bexpr
iha : normalize a = true ↔ interp a
ihb : normalize b = true ↔ interp b
⊢ normalize a ≠ true ∨ normalize b = true ↔ normalize a = true → normalize b = true

State before:
case imp
a b : bexpr
iha : normalize a = true ↔ interp a
ihb : normalize b = true ↔ interp b
⊢ normalize a ≠ true ∨ normalize b = true ↔ normalize a = true → normalize b = true
Tactic:
tauto
State after:
no goals