Theorem: Cpdt.Chapter8.Exp.cfold_correct (Cpdt/Chapter8/Tagless.lean)

State before:
a✝ : Ty
e : Exp a✝
⊢ denote e = denote (cfold e)
Tactic:
induction e with simp[denote, cfold]
| plus l r => split <;> simp_all[denote, cfold]
| eq l r => split <;> simp_all[denote, cfold]
| and l r => split <;> simp_all[denote, cfold]
| if_ d l r dih lih rih =>
  rw[dih, lih, rih]
  cases cfold d with simp[denote]
  | bConst b => cases b <;> simp
| pair l r => simp_all[denote]
| fst p ih => 
  rw[ih]
  cases cfold p <;> simp[pairOut, denote]
| snd p ih =>
  rw[ih]
  cases cfold p <;> simp[pairOut, denote]
State after:
no goals

State before:
case plus
a✝ : Ty
l r : Exp Ty.nat
a_ih✝¹ : denote l = denote (cfold l)
a_ih✝ : denote r = denote (cfold r)
⊢ denote l + denote r =
    denote
      (match cfold l, cfold r with
      | nConst n, nConst m => nConst (n + m)
      | x, x_1 => plus (cfold l) (cfold r))
Tactic:
split <;> simp_all[denote, cfold]
State after:
no goals

State before:
case eq
a✝ : Ty
l r : Exp Ty.nat
a_ih✝¹ : denote l = denote (cfold l)
a_ih✝ : denote r = denote (cfold r)
⊢ (denote l == denote r) =
    denote
      (match cfold l, cfold r with
      | nConst n, nConst m => bConst (n == m)
      | x, x_1 => eq (cfold l) (cfold r))
Tactic:
split <;> simp_all[denote, cfold]
State after:
no goals

State before:
case and
a✝ : Ty
l r : Exp Ty.bool
a_ih✝¹ : denote l = denote (cfold l)
a_ih✝ : denote r = denote (cfold r)
⊢ (denote l && denote r) =
    denote
      (match cfold l, cfold r with
      | bConst n, bConst m => bConst (n && m)
      | x, x_1 => and (cfold l) (cfold r))
Tactic:
split <;> simp_all[denote, cfold]
State after:
no goals

State before:
case if_
a✝ α✝ : Ty
d : Exp Ty.bool
l r : Exp α✝
dih : denote d = denote (cfold d)
lih : denote l = denote (cfold l)
rih : denote r = denote (cfold r)
⊢ (if denote d = true then denote l else denote r) =
    denote
      (match cfold d with
      | bConst true => cfold l
      | bConst false => cfold r
      | x => if_ (cfold d) (cfold l) (cfold r))
Tactic:
rw[dih, lih, rih]
State after:
case if_
a✝ α✝ : Ty
d : Exp Ty.bool
l r : Exp α✝
dih : denote d = denote (cfold d)
lih : denote l = denote (cfold l)
rih : denote r = denote (cfold r)
⊢ (if denote (cfold d) = true then denote (cfold l) else denote (cfold r)) =
    denote
      (match cfold d with
      | bConst true => cfold l
      | bConst false => cfold r
      | x => if_ (cfold d) (cfold l) (cfold r))

State before:
case if_
a✝ α✝ : Ty
d : Exp Ty.bool
l r : Exp α✝
dih : denote d = denote (cfold d)
lih : denote l = denote (cfold l)
rih : denote r = denote (cfold r)
⊢ (if denote (cfold d) = true then denote (cfold l) else denote (cfold r)) =
    denote
      (match cfold d with
      | bConst true => cfold l
      | bConst false => cfold r
      | x => if_ (cfold d) (cfold l) (cfold r))
Tactic:
cases cfold d with simp[denote]
| bConst b => cases b <;> simp
State after:
no goals

State before:
case if_.bConst
a✝ α✝ : Ty
d : Exp Ty.bool
l r : Exp α✝
dih : denote d = denote (cfold d)
lih : denote l = denote (cfold l)
rih : denote r = denote (cfold r)
b : Bool
⊢ (if b = true then denote (cfold l) else denote (cfold r)) =
    denote
      (match bConst b with
      | bConst true => cfold l
      | bConst false => cfold r
      | x => if_ (bConst b) (cfold l) (cfold r))
Tactic:
cases b <;> simp
State after:
no goals

State before:
case pair
a✝ α✝ β✝ : Ty
l : Exp α✝
r : Exp β✝
a_ih✝¹ : denote l = denote (cfold l)
a_ih✝ : denote r = denote (cfold r)
⊢ denote l = denote (cfold l) ∧ denote r = denote (cfold r)
Tactic:
simp_all[denote]
State after:
no goals

State before:
case fst
a✝ α✝ β✝ : Ty
p : Exp (Ty.prod α✝ β✝)
ih : denote p = denote (cfold p)
⊢ (denote p).fst =
    denote
      (match pairOut (cfold p) with
      | some p => p.fst
      | none => fst (cfold p))
Tactic:
rw[ih]
State after:
case fst
a✝ α✝ β✝ : Ty
p : Exp (Ty.prod α✝ β✝)
ih : denote p = denote (cfold p)
⊢ (denote (cfold p)).fst =
    denote
      (match pairOut (cfold p) with
      | some p => p.fst
      | none => fst (cfold p))

State before:
case fst
a✝ α✝ β✝ : Ty
p : Exp (Ty.prod α✝ β✝)
ih : denote p = denote (cfold p)
⊢ (denote (cfold p)).fst =
    denote
      (match pairOut (cfold p) with
      | some p => p.fst
      | none => fst (cfold p))
Tactic:
cases cfold p <;> simp[pairOut, denote]
State after:
no goals

State before:
case snd
a✝ α✝ β✝ : Ty
p : Exp (Ty.prod α✝ β✝)
ih : denote p = denote (cfold p)
⊢ (denote p).snd =
    denote
      (match pairOut (cfold p) with
      | some p => p.snd
      | none => snd (cfold p))
Tactic:
rw[ih]
State after:
case snd
a✝ α✝ β✝ : Ty
p : Exp (Ty.prod α✝ β✝)
ih : denote p = denote (cfold p)
⊢ (denote (cfold p)).snd =
    denote
      (match pairOut (cfold p) with
      | some p => p.snd
      | none => snd (cfold p))

State before:
case snd
a✝ α✝ β✝ : Ty
p : Exp (Ty.prod α✝ β✝)
ih : denote p = denote (cfold p)
⊢ (denote (cfold p)).snd =
    denote
      (match pairOut (cfold p) with
      | some p => p.snd
      | none => snd (cfold p))
Tactic:
cases cfold p <;> simp[pairOut, denote]
State after:
no goals