internlm/Lean-Github huggingface dataset:
Theorem: Cpdt.Chapter7.Computation.bind_fun_computation
Proof state before:
case some
α β : Type
m1 : Computation α
m2 : α → Computation β
n : Nat
v : β
n' : Nat
x : α
h1 : Subtype.val (m2 x) n = some v
h : n' ≥ n
h2 : Subtype.val m1 n = some x
m1_n'_runs : Subtype.val m1 n' = some x
m2_n'_runs : Subtype.val (m2 x) n' = some v
⊢ (match Subtype.val m1 n' with
    | none => none
    | some a => Subtype.val (m2 a) n') =
    some v
Tactic:
simp[m1_n'_runs, m2_n'_runs]
Proof state after:
no goals
Theorem: Cpdt.Chapter7.Computation.fix'_ok
Proof state before:
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
⊢ ∀ (steps n : Nat) (x : α) (v : β),
    Subtype.val (fix' f n x) steps = some v → ∀ (n' : Nat), n' ≥ n → Subtype.val (fix' f n' x) steps = some v
Tactic:
intro steps n x v h1 n' h2
Proof state after:
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
steps n : Nat
x : α
v : β
h1 : Subtype.val (fix' f n x) steps = some v
n' : Nat
h2 : n' ≥ n
⊢ Subtype.val (fix' f n' x) steps = some v
Theorem: Cpdt.Chapter7.Computation.fix'_ok
Proof state before:
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
steps n : Nat
x : α
v : β
h1 : Subtype.val (fix' f n x) steps = some v
n' : Nat
h2 : n' ≥ n
⊢ Subtype.val (fix' f n' x) steps = some v
Tactic:
induction n with
| zero => simp_all_arith[fix', bottom]
| succ m ih =>
  simp_all[fix', runTo]
  sorry
Proof state after:
no goals
Theorem: Cpdt.Chapter7.Computation.fix'_ok
Proof state before:
case zero
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
steps : Nat
x : α
v : β
n' : Nat
h1 : Subtype.val (fix' f Nat.zero x) steps = some v
h2 : n' ≥ Nat.zero
⊢ Subtype.val (fix' f n' x) steps = some v
Tactic:
simp_all_arith[fix', bottom]
Proof state after:
no goals
Theorem: Cpdt.Chapter7.Computation.fix'_ok
Proof state before:
case succ
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
steps : Nat
x : α
v : β
n' m : Nat
ih : Subtype.val (fix' f m x) steps = some v → n' ≥ m → Subtype.val (fix' f n' x) steps = some v
h1 : Subtype.val (fix' f (Nat.succ m) x) steps = some v
h2 : n' ≥ Nat.succ m
⊢ Subtype.val (fix' f n' x) steps = some v
Tactic:
simp_all[fix', runTo]
Proof state after:
case succ
α β : Type
f : (α → Computation β) → α → Computation β
steps : Nat
x : α
v : β
n' m : Nat
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    Subtype.val (f v1 x) n = some v →
      ∀ (v2 : α → Computation β),
        (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → Subtype.val (f v2 x) n = some v
ih : Subtype.val (fix' f m x) steps = some v → n' ≥ m → Subtype.val (fix' f n' x) steps = some v
h1 : Subtype.val (f (fix' f m) x) steps = some v
h2 : n' ≥ Nat.succ m
⊢ Subtype.val (fix' f n' x) steps = some v
Theorem: Cpdt.Chapter7.Computation.fix'_ok
Proof state before:
case succ
α β : Type
f : (α → Computation β) → α → Computation β
steps : Nat
x : α
v : β
n' m : Nat
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    Subtype.val (f v1 x) n = some v →
      ∀ (v2 : α → Computation β),
        (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → Subtype.val (f v2 x) n = some v
ih : Subtype.val (fix' f m x) steps = some v → n' ≥ m → Subtype.val (fix' f n' x) steps = some v
h1 : Subtype.val (f (fix' f m) x) steps = some v
h2 : n' ≥ Nat.succ m
⊢ Subtype.val (fix' f n' x) steps = some v
Tactic:
sorry
Proof state after:
no goals
Theorem: Cpdt.Chapter7.Computation.run_fix
Proof state before:
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
⊢ ∀ (x : α) (v : β), run (f (fix f) x) v → run (fix f x) v
Tactic:
intro x v h
Proof state after:
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
x : α
v : β
h : run (f (fix f) x) v
⊢ run (fix f x) v
Theorem: Cpdt.Chapter7.Computation.run_fix
Proof state before:
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
x : α
v : β
h : run (f (fix f) x) v
⊢ run (fix f x) v
Tactic:
cases h with
| intro n h =>
  exists n.succ
  apply f_continious
  sorry
  sorry
  sorry
Proof state after:
no goals
Theorem: Cpdt.Chapter7.Computation.run_fix
Proof state before:
case intro
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ run (fix f x) v
Tactic:
exists n.succ
Proof state after:
case intro
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ Subtype.val (fix f x) (Nat.succ n) = some v
Theorem: Cpdt.Chapter7.Computation.run_fix
Proof state before:
case intro
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ Subtype.val (fix f x) (Nat.succ n) = some v
Tactic:
apply f_continious
Proof state after:
case intro.a
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ runTo (f ?intro.v1 x) (Nat.succ n) v

case intro.a
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ ∀ (x : α), Subtype.val (?intro.v1 x) (Nat.succ n) ⊑ Subtype.val (fix' f n x) (Nat.succ n)

case intro.v1
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ α → Computation β
Theorem: Cpdt.Chapter7.Computation.run_fix
Proof state before:
case intro.a
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ runTo (f ?intro.v1 x) (Nat.succ n) v

case intro.a
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ ∀ (x : α), Subtype.val (?intro.v1 x) (Nat.succ n) ⊑ Subtype.val (fix' f n x) (Nat.succ n)

case intro.v1
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ α → Computation β
Tactic:
sorry
Proof state after:
case intro.a
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ ∀ (x : α), Subtype.val (?intro.v1 x) (Nat.succ n) ⊑ Subtype.val (fix' f n x) (Nat.succ n)

case intro.v1
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ α → Computation β
Theorem: Cpdt.Chapter7.Computation.run_fix
Proof state before:
case intro.a
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ ∀ (x : α), Subtype.val (?intro.v1 x) (Nat.succ n) ⊑ Subtype.val (fix' f n x) (Nat.succ n)

case intro.v1
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ α → Computation β
Tactic:
sorry
Proof state after:
case intro.v1
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ α → Computation β
Theorem: Cpdt.Chapter7.Computation.run_fix
Proof state before:
case intro.v1
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ α → Computation β
Tactic:
sorry
Proof state after:
no goals
Theorem: Cpdt.Chapter3.Formula.denote_eq
Proof state before:
l r : Nat
⊢ denote (eq l r) = (l = r)
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter3.Formula.denote_and
Proof state before:
l r : Formula
⊢ denote (and l r) = (denote l ∧ denote r)
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter3.Formula.denote_universal
Proof state before:
p : Nat → Formula
⊢ denote (universal p) = ∀ (x : Nat), denote (p x)
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter3.Formula.swapper_eq
Proof state before:
l r : Nat
⊢ swapper (eq l r) = eq r l
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter3.Formula.swapper_and
Proof state before:
l r : Formula
⊢ swapper (and l r) = and r l
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter3.Formula.swapper_universal
Proof state before:
p : Nat → Formula
⊢ swapper (universal p) = universal fun x => swapper (p x)
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter3.Formula.swapper_of_normal
Proof state before:
⊢ ∀ (f : Formula), denote f → denote (swapper f)
Tactic:
intro f
Proof state after:
f : Formula
⊢ denote f → denote (swapper f)
Theorem: Cpdt.Chapter3.Formula.swapper_of_normal
Proof state before:
f : Formula
⊢ denote f → denote (swapper f)
Tactic:
induction f <;> simp_all
Proof state after:
no goals
Theorem: Cpdt.Chapter8.Exp.cfold_correct
Proof 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]
Proof state after:
no goals
Theorem: Cpdt.Chapter8.Exp.cfold_correct
Proof 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]
Proof state after:
no goals
Theorem: Cpdt.Chapter8.Exp.cfold_correct
Proof 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]
Proof state after:
no goals
Theorem: Cpdt.Chapter8.Exp.cfold_correct
Proof 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]
Proof state after:
no goals
Theorem: Cpdt.Chapter8.Exp.cfold_correct
Proof 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]
Proof 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))
Theorem: Cpdt.Chapter8.Exp.cfold_correct
Proof 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
Proof state after:
no goals
Theorem: Cpdt.Chapter8.Exp.cfold_correct
Proof 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
Proof state after:
no goals
Theorem: Cpdt.Chapter8.Exp.cfold_correct
Proof 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]
Proof state after:
no goals
Theorem: Cpdt.Chapter8.Exp.cfold_correct
Proof 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]
Proof 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))
Theorem: Cpdt.Chapter8.Exp.cfold_correct
Proof 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]
Proof state after:
no goals
Theorem: Cpdt.Chapter8.Exp.cfold_correct
Proof 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]
Proof 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))
Theorem: Cpdt.Chapter8.Exp.cfold_correct
Proof 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]
Proof state after:
no goals
Theorem: Cpdt.Chapter3.all_cons
Proof state before:
α✝ : Type u_1
p : α✝ → Prop
x : α✝
xs : List α✝
⊢ all p (x :: xs) = (p x ∧ all p xs)
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter3.NatTree.size_tree
Proof state before:
x : Nat
ts : List NatTree
⊢ size (node x ts) = 1 + nodeListSize ts
Tactic:
rw [size]
Proof state after:
no goals
Theorem: Cpdt.Chapter3.NatTree.nodeListSize_nil
Proof state before:
⊢ nodeListSize [] = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter3.NatTree.nodeListSize_cons
Proof state before:
t : NatTree
ts : List NatTree
⊢ nodeListSize (t :: ts) = size t + nodeListSize ts
Tactic:
rw[nodeListSize]
Proof state after:
no goals
Theorem: Cpdt.Chapter3.NatTree.splice_node_nil
Proof state before:
x : Nat
t2 : NatTree
⊢ splice (node x []) t2 = node x [t2]
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter3.NatTree.splice_node_cons
Proof state before:
x : Nat
t : NatTree
ts : List NatTree
t2 : NatTree
⊢ splice (node x (t :: ts)) t2 = node x (splice t t2 :: ts)
Tactic:
rw[splice]
Proof state after:
no goals
Theorem: Cpdt.Chapter3.NatTree.splice_size
Proof state before:
⊢ ∀ (t1 t2 : NatTree), size (splice t1 t2) = size t1 + size t2
Tactic:
intro t1
Proof state after:
t1 : NatTree
⊢ ∀ (t2 : NatTree), size (splice t1 t2) = size t1 + size t2
Theorem: Cpdt.Chapter3.NatTree.splice_size
Proof state before:
t1 : NatTree
⊢ ∀ (t2 : NatTree), size (splice t1 t2) = size t1 + size t2
Tactic:
induction t1 using nat_tree_ind with
| node_case x ts ih =>
  cases ts <;> simp_all
  simp_arith
Proof state after:
no goals
Theorem: Cpdt.Chapter3.NatTree.splice_size
Proof state before:
case node_case
x : Nat
ts : List NatTree
ih : all (fun t1 => ∀ (t2 : NatTree), size (splice t1 t2) = size t1 + size t2) ts
⊢ ∀ (t2 : NatTree), size (splice (node x ts) t2) = size (node x ts) + size t2
Tactic:
cases ts <;> simp_all
Proof state after:
case node_case.cons
x : Nat
head✝ : NatTree
tail✝ : List NatTree
ih :
  (∀ (t2 : NatTree), size (splice head✝ t2) = size head✝ + size t2) ∧
    all (fun t1 => ∀ (t2 : NatTree), size (splice t1 t2) = size t1 + size t2) tail✝
⊢ ∀ (t2 : NatTree), 1 + (size head✝ + size t2 + nodeListSize tail✝) = 1 + (size head✝ + nodeListSize tail✝) + size t2
Theorem: Cpdt.Chapter3.NatTree.splice_size
Proof state before:
case node_case.cons
x : Nat
head✝ : NatTree
tail✝ : List NatTree
ih :
  (∀ (t2 : NatTree), size (splice head✝ t2) = size head✝ + size t2) ∧
    all (fun t1 => ∀ (t2 : NatTree), size (splice t1 t2) = size t1 + size t2) tail✝
⊢ ∀ (t2 : NatTree), 1 + (size head✝ + size t2 + nodeListSize tail✝) = 1 + (size head✝ + nodeListSize tail✝) + size t2
Tactic:
simp_arith
Proof state after:
no goals
Theorem: Cpdt.Chapter8.IList.inject_unject_inv
Proof state before:
α✝ : Type
xs : List α✝
⊢ (unject (inject xs)).val = xs
Tactic:
induction xs <;> simp_all[unject, inject]
Proof state after:
no goals
Theorem: Cpdt.Chapter3.EvenList.elength_nil
Proof state before:
⊢ elength nil = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter3.EvenList.elength_econs
Proof state before:
x : Nat
xs : OddList
⊢ elength (eCons x xs) = 1 + olength xs
Tactic:
rw[elength]
Proof state after:
no goals
Theorem: Cpdt.Chapter3.EvenList.nil_eappend
Proof state before:
ys : EvenList
⊢ eappend nil ys = ys
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter3.EvenList.eCons_eappend
Proof state before:
x : Nat
xs : OddList
ys : EvenList
⊢ eappend (eCons x xs) ys = eCons x (oappend xs ys)
Tactic:
rw[eappend]
Proof state after:
no goals
Theorem: Cpdt.Chapter3.OddList.olength_oCons
Proof state before:
x : Nat
xs : EvenList
⊢ olength (oCons x xs) = 1 + elength xs
Tactic:
rw [olength]
Proof state after:
no goals
Theorem: Cpdt.Chapter3.OddList.oCons_oappend
Proof state before:
x : Nat
xs ys : EvenList
⊢ oappend (oCons x xs) ys = oCons x (eappend xs ys)
Tactic:
rw[oappend]
Proof state after:
no goals
Theorem: Cpdt.Chapter3.elength_eappend
Proof state before:
xs ys : EvenList
⊢ elength (eappend xs ys) = elength xs + elength ys
Tactic:
apply @EvenList.rec
  (fun xs => ∀ ys, elength (eappend xs ys) = elength xs + elength ys)
  (fun ol => ∀ el, olength (oappend ol el) = olength ol + elength el)
<;> simp_all[Nat.add_assoc]
Proof state after:
no goals
Theorem: my_first_theorem
Proof state before:
p q r : Prop
⊢ p ∧ q → q ∧ p
Tactic:
intro hpq
Proof state after:
p q r : Prop
hpq : p ∧ q
⊢ q ∧ p
Theorem: my_first_theorem
Proof state before:
p q r : Prop
hpq : p ∧ q
⊢ q ∧ p
Tactic:
cases' hpq with hp hq
Proof state after:
case intro
p q r : Prop
hp : p
hq : q
⊢ q ∧ p
Theorem: my_first_theorem
Proof state before:
case intro
p q r : Prop
hp : p
hq : q
⊢ q ∧ p
Tactic:
apply And.intro
Proof state after:
case intro.left
p q r : Prop
hp : p
hq : q
⊢ q

case intro.right
p q r : Prop
hp : p
hq : q
⊢ p
Theorem: my_first_theorem
Proof state before:
case intro.left
p q r : Prop
hp : p
hq : q
⊢ q

case intro.right
p q r : Prop
hp : p
hq : q
⊢ p
Tactic:
. exact hq
Proof state after:
case intro.right
p q r : Prop
hp : p
hq : q
⊢ p
Theorem: my_first_theorem
Proof state before:
case intro.right
p q r : Prop
hp : p
hq : q
⊢ p
Tactic:
. exact hp
Proof state after:
no goals
Theorem: false_context
Proof state before:
p q r : Prop
⊢ 1 = 2 → 1 = 2
Tactic:
intro h12
Proof state after:
p q r : Prop
h12 : 1 = 2
⊢ 1 = 2
Theorem: false_context
Proof state before:
p q r : Prop
h12 : 1 = 2
⊢ 1 = 2
Tactic:
exact h12
Proof state after:
no goals
Theorem: flip_ors
Proof state before:
p q r : Prop
⊢ p ∨ q → q ∨ p
Tactic:
sorry
Proof state after:
no goals