internlm/Lean-Github huggingface dataset:
Theorem: Cpdt.Chapter4.even_contra
Proof state before:
case a
n : Nat
h : Even (Nat.succ (n + n))
⊢ Nat.succ (n + n) = Nat.succ (?n + ?n)

case n
n : Nat
h : Even (Nat.succ (n + n))
⊢ Nat
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.Binop.denote_plus
Proof state before:
⊢ denote plus = Nat.add
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.Binop.denote_times
Proof state before:
⊢ denote times = Nat.mul
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.Exp.denote_const
Proof state before:
n : Nat
⊢ denote (const n) = n
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.Exp.denote_binop
Proof state before:
op : Binop
l r : Exp
⊢ denote (binop op l r) = Binop.denote op (denote l) (denote r)
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.Instr.denote_iConst
Proof state before:
n : Nat
s : Stack
⊢ denote (iConst n) s = some (n :: s)
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.Instr.denote_iBinop_2args
Proof state before:
op b : Binop
s : Stack
arg1 arg2 : Nat
⊢ denote (iBinop op) (arg1 :: arg2 :: s) = some (Binop.denote op arg1 arg2 :: s)
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.Instr.denote_iBinop_1arg
Proof state before:
op b : Binop
arg : Nat
⊢ denote (iBinop op) [arg] = none
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.Instr.denote_iBinop_nil
Proof state before:
op b : Binop
arg : Nat
⊢ denote (iBinop op) [] = none
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.Prog.denote_nil
Proof state before:
s : Stack
⊢ denote [] s = some s
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.Prog.denote_iConst
Proof state before:
s : Stack
p : Prog
n : Nat
⊢ denote (Instr.iConst n :: p) s = denote p (n :: s)
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.Prog.denote_iBinop_2args
Proof state before:
s : Stack
p : Prog
op : Binop
arg1 arg2 : Nat
⊢ denote (Instr.iBinop op :: p) (arg1 :: arg2 :: s) = denote p (Binop.denote op arg1 arg2 :: s)
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.Prog.denote_iBinop_1args
Proof state before:
p : Prog
op : Binop
arg : Nat
⊢ denote (Instr.iBinop op :: p) [arg] = none
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.Prog.denote_iBinop_nil
Proof state before:
p : Prog
op : Binop
⊢ denote (Instr.iBinop op :: p) [] = none
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.Exp.compile_const
Proof state before:
n : Nat
⊢ compile (const n) = [Instr.iConst n]
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.Exp.compile_binop
Proof state before:
op : Binop
l r : Exp
⊢ compile (binop op l r) = compile r ++ compile l ++ [Instr.iBinop op]
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.compile_correct_help
Proof state before:
⊢ ∀ (e : Exp) (p : Prog) (s : Stack), Prog.denote (Exp.compile e ++ p) s = Prog.denote p (Exp.denote e :: s)
Tactic:
intro e p s
Proof state after:
e : Exp
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile e ++ p) s = Prog.denote p (Exp.denote e :: s)
Theorem: Cpdt.Chapter2.compile_correct_help
Proof state before:
e : Exp
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile e ++ p) s = Prog.denote p (Exp.denote e :: s)
Tactic:
induction e generalizing p s with
| const n =>
  rw [Exp.compile_const]
  rw [Exp.denote_const]
  simp
  rw [Prog.denote_iConst]
| binop b l r lih rih =>
  rw [Exp.compile_binop]
  rw [Exp.denote_binop]
  rw [List.append_assoc (Exp.compile r)]
  rw [List.append_assoc (Exp.compile r)]
  rw [rih]
  rw [List.append_assoc]
  rw [lih]
  simp
  rw [Prog.denote_iBinop_2args]
Proof state after:
no goals
Theorem: Cpdt.Chapter2.compile_correct_help
Proof state before:
case const
n : Nat
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile (Exp.const n) ++ p) s = Prog.denote p (Exp.denote (Exp.const n) :: s)
Tactic:
rw [Exp.compile_const]
Proof state after:
case const
n : Nat
p : Prog
s : Stack
⊢ Prog.denote ([Instr.iConst n] ++ p) s = Prog.denote p (Exp.denote (Exp.const n) :: s)
Theorem: Cpdt.Chapter2.compile_correct_help
Proof state before:
case const
n : Nat
p : Prog
s : Stack
⊢ Prog.denote ([Instr.iConst n] ++ p) s = Prog.denote p (Exp.denote (Exp.const n) :: s)
Tactic:
rw [Exp.denote_const]
Proof state after:
case const
n : Nat
p : Prog
s : Stack
⊢ Prog.denote ([Instr.iConst n] ++ p) s = Prog.denote p (n :: s)
Theorem: Cpdt.Chapter2.compile_correct_help
Proof state before:
case const
n : Nat
p : Prog
s : Stack
⊢ Prog.denote ([Instr.iConst n] ++ p) s = Prog.denote p (n :: s)
Tactic:
simp
Proof state after:
case const
n : Nat
p : Prog
s : Stack
⊢ Prog.denote (Instr.iConst n :: p) s = Prog.denote p (n :: s)
Theorem: Cpdt.Chapter2.compile_correct_help
Proof state before:
case const
n : Nat
p : Prog
s : Stack
⊢ Prog.denote (Instr.iConst n :: p) s = Prog.denote p (n :: s)
Tactic:
rw [Prog.denote_iConst]
Proof state after:
no goals
Theorem: Cpdt.Chapter2.compile_correct_help
Proof state before:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile (Exp.binop b l r) ++ p) s = Prog.denote p (Exp.denote (Exp.binop b l r) :: s)
Tactic:
rw [Exp.compile_binop]
Proof state after:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile r ++ Exp.compile l ++ [Instr.iBinop b] ++ p) s =
    Prog.denote p (Exp.denote (Exp.binop b l r) :: s)
Theorem: Cpdt.Chapter2.compile_correct_help
Proof state before:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile r ++ Exp.compile l ++ [Instr.iBinop b] ++ p) s =
    Prog.denote p (Exp.denote (Exp.binop b l r) :: s)
Tactic:
rw [Exp.denote_binop]
Proof state after:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile r ++ Exp.compile l ++ [Instr.iBinop b] ++ p) s =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)
Theorem: Cpdt.Chapter2.compile_correct_help
Proof state before:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile r ++ Exp.compile l ++ [Instr.iBinop b] ++ p) s =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)
Tactic:
rw [List.append_assoc (Exp.compile r)]
Proof state after:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile r ++ (Exp.compile l ++ [Instr.iBinop b]) ++ p) s =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)
Theorem: Cpdt.Chapter2.compile_correct_help
Proof state before:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile r ++ (Exp.compile l ++ [Instr.iBinop b]) ++ p) s =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)
Tactic:
rw [List.append_assoc (Exp.compile r)]
Proof state after:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile r ++ (Exp.compile l ++ [Instr.iBinop b] ++ p)) s =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)
Theorem: Cpdt.Chapter2.compile_correct_help
Proof state before:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile r ++ (Exp.compile l ++ [Instr.iBinop b] ++ p)) s =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)
Tactic:
rw [rih]
Proof state after:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile l ++ [Instr.iBinop b] ++ p) (Exp.denote r :: s) =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)
Theorem: Cpdt.Chapter2.compile_correct_help
Proof state before:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile l ++ [Instr.iBinop b] ++ p) (Exp.denote r :: s) =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)
Tactic:
rw [List.append_assoc]
Proof state after:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile l ++ ([Instr.iBinop b] ++ p)) (Exp.denote r :: s) =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)
Theorem: Cpdt.Chapter2.compile_correct_help
Proof state before:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile l ++ ([Instr.iBinop b] ++ p)) (Exp.denote r :: s) =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)
Tactic:
rw [lih]
Proof state after:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote ([Instr.iBinop b] ++ p) (Exp.denote l :: Exp.denote r :: s) =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)
Theorem: Cpdt.Chapter2.compile_correct_help
Proof state before:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote ([Instr.iBinop b] ++ p) (Exp.denote l :: Exp.denote r :: s) =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)
Tactic:
simp
Proof state after:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Instr.iBinop b :: p) (Exp.denote l :: Exp.denote r :: s) =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)
Theorem: Cpdt.Chapter2.compile_correct_help
Proof state before:
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Instr.iBinop b :: p) (Exp.denote l :: Exp.denote r :: s) =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)
Tactic:
rw [Prog.denote_iBinop_2args]
Proof state after:
no goals
Theorem: Cpdt.Chapter2.compile_correct
Proof state before:
⊢ ∀ (e : Exp), Prog.denote (Exp.compile e) [] = some [Exp.denote e]
Tactic:
intro e
Proof state after:
e : Exp
⊢ Prog.denote (Exp.compile e) [] = some [Exp.denote e]
Theorem: Cpdt.Chapter2.compile_correct
Proof state before:
e : Exp
⊢ Prog.denote (Exp.compile e) [] = some [Exp.denote e]
Tactic:
rw [←List.append_nil (Exp.compile e)]
Proof state after:
e : Exp
⊢ Prog.denote (Exp.compile e ++ []) [] = some [Exp.denote e]
Theorem: Cpdt.Chapter2.compile_correct
Proof state before:
e : Exp
⊢ Prog.denote (Exp.compile e ++ []) [] = some [Exp.denote e]
Tactic:
rw [compile_correct_help]
Proof state after:
e : Exp
⊢ Prog.denote [] [Exp.denote e] = some [Exp.denote e]
Theorem: Cpdt.Chapter2.compile_correct
Proof state before:
e : Exp
⊢ Prog.denote [] [Exp.denote e] = some [Exp.denote e]
Tactic:
rw [Prog.denote_nil]
Proof state after:
no goals
Theorem: Cpdt.Chapter7.split_wf_match
Proof state before:
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
⊢ let spl := split [x, y];
  List.length spl.fst < List.length [] + 2 ∧ List.length spl.snd < List.length [] + 2
Tactic:
simp[split]
Proof state after:
no goals
Theorem: Cpdt.Chapter7.split_wf_match
Proof state before:
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a : α
⊢ let spl := split [x, y, a];
  List.length spl.fst < List.length [a] + 2 ∧ List.length spl.snd < List.length [a] + 2
Tactic:
simp[split]
Proof state after:
no goals
Theorem: Cpdt.Chapter7.split_wf_match
Proof state before:
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
⊢ let spl := split (x :: y :: a :: b :: cs);
  List.length spl.fst < List.length (a :: b :: cs) + 2 ∧ List.length spl.snd < List.length (a :: b :: cs) + 2
Tactic:
have helper := split_wf_match a b cs
Proof state after:
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper :
  let spl := split (a :: b :: cs);
  List.length spl.fst < List.length cs + 2 ∧ List.length spl.snd < List.length cs + 2
⊢ let spl := split (x :: y :: a :: b :: cs);
  List.length spl.fst < List.length (a :: b :: cs) + 2 ∧ List.length spl.snd < List.length (a :: b :: cs) + 2
Theorem: Cpdt.Chapter7.split_wf_match
Proof state before:
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper :
  let spl := split (a :: b :: cs);
  List.length spl.fst < List.length cs + 2 ∧ List.length spl.snd < List.length cs + 2
⊢ let spl := split (x :: y :: a :: b :: cs);
  List.length spl.fst < List.length (a :: b :: cs) + 2 ∧ List.length spl.snd < List.length (a :: b :: cs) + 2
Tactic:
simp_all_arith[split]
Proof state after:
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length (split cs).fst ≤ List.length cs + 1 ∧ List.length (split cs).snd ≤ List.length cs + 1
Theorem: Cpdt.Chapter7.split_wf_match
Proof state before:
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length (split cs).fst ≤ List.length cs + 1 ∧ List.length (split cs).snd ≤ List.length cs + 1
Tactic:
constructor
Proof state after:
case left
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length (split cs).fst ≤ List.length cs + 1

case right
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length (split cs).snd ≤ List.length cs + 1
Theorem: Cpdt.Chapter7.split_wf_match
Proof state before:
case left
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length (split cs).fst ≤ List.length cs + 1

case right
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length (split cs).snd ≤ List.length cs + 1
Tactic:
apply Nat.le_trans helper.left
Proof state after:
case left
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length cs ≤ List.length cs + 1

case right
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length (split cs).snd ≤ List.length cs + 1
Theorem: Cpdt.Chapter7.split_wf_match
Proof state before:
case left
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length cs ≤ List.length cs + 1

case right
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length (split cs).snd ≤ List.length cs + 1
Tactic:
simp_arith
Proof state after:
case right
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length (split cs).snd ≤ List.length cs + 1
Theorem: Cpdt.Chapter7.split_wf_match
Proof state before:
case right
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length (split cs).snd ≤ List.length cs + 1
Tactic:
apply Nat.le_trans helper.right
Proof state after:
case right
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length cs ≤ List.length cs + 1
Theorem: Cpdt.Chapter7.split_wf_match
Proof state before:
case right
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length cs ≤ List.length cs + 1
Tactic:
simp_arith
Proof state after:
no goals
Theorem: Cpdt.Chapter7.Computation.run_bottom
Proof state before:
α : Type
⊢ ∀ (v : α), ¬run bottom v
Tactic:
intro v
Proof state after:
α : Type
v : α
⊢ ¬run bottom v
Theorem: Cpdt.Chapter7.Computation.run_bottom
Proof state before:
α : Type
v : α
⊢ ¬run bottom v
Tactic:
simp[run, bottom]
Proof state after:
α : Type
v : α
⊢ ¬∃ n, False
Theorem: Cpdt.Chapter7.Computation.run_bottom
Proof state before:
α : Type
v : α
⊢ ¬∃ n, False
Tactic:
intro h
Proof state after:
α : Type
v : α
h : ∃ n, False
⊢ False
Theorem: Cpdt.Chapter7.Computation.run_bottom
Proof state before:
α : Type
v : α
h : ∃ n, False
⊢ False
Tactic:
cases h
Proof state after:
case intro
α : Type
v : α
w✝ : Nat
h✝ : False
⊢ False
Theorem: Cpdt.Chapter7.Computation.run_bottom
Proof state before:
case intro
α : Type
v : α
w✝ : Nat
h✝ : False
⊢ False
Tactic:
assumption
Proof state after:
no goals
Theorem: Cpdt.Chapter7.Computation.run_return
Proof state before:
α : Type
⊢ ∀ (v : α), run (ret v) v
Tactic:
intro v
Proof state after:
α : Type
v : α
⊢ run (ret v) v
Theorem: Cpdt.Chapter7.Computation.run_return
Proof state before:
α : Type
v : α
⊢ run (ret v) v
Tactic:
simp [run, ret]
Proof state after:
α : Type
v : α
⊢ ∃ n, True
Theorem: Cpdt.Chapter7.Computation.run_return
Proof state before:
α : Type
v : α
⊢ ∃ n, True
Tactic:
exact Exists.intro 0 True.intro
Proof state after:
no goals
Theorem: Cpdt.Chapter7.Computation.bind_fun_computation
Proof state before:
α β : Type
m1 : Computation α
m2 : α → Computation β
⊢ ∀ (n : Nat) (v : β), bind_fun m1 m2 n = some v → ∀ (n' : Nat), n' ≥ n → bind_fun m1 m2 n' = some v
Tactic:
intro n v h1 n' h
Proof state after:
α β : Type
m1 : Computation α
m2 : α → Computation β
n : Nat
v : β
h1 : bind_fun m1 m2 n = some v
n' : Nat
h : n' ≥ n
⊢ bind_fun m1 m2 n' = some v
Theorem: Cpdt.Chapter7.Computation.bind_fun_computation
Proof state before:
α β : Type
m1 : Computation α
m2 : α → Computation β
n : Nat
v : β
h1 : bind_fun m1 m2 n = some v
n' : Nat
h : n' ≥ n
⊢ bind_fun m1 m2 n' = some v
Tactic:
cases h2 : m1.val n with
| none => simp_all[bind_fun]
| some x =>
  simp_all[bind_fun]
  have m1_n'_runs : m1.val n' = some x := m1.property n x h2 n' h
  have m2_n'_runs : (m2 x).val n' = some v := (m2 x).property n v h1 n' h
  simp[m1_n'_runs, m2_n'_runs]
Proof state after:
no goals
Theorem: Cpdt.Chapter7.Computation.bind_fun_computation
Proof state before:
case none
α β : Type
m1 : Computation α
m2 : α → Computation β
n : Nat
v : β
h1 : bind_fun m1 m2 n = some v
n' : Nat
h : n' ≥ n
h2 : Subtype.val m1 n = none
⊢ bind_fun m1 m2 n' = some v
Tactic:
simp_all[bind_fun]
Proof state after:
no goals
Theorem: Cpdt.Chapter7.Computation.bind_fun_computation
Proof state before:
case some
α β : Type
m1 : Computation α
m2 : α → Computation β
n : Nat
v : β
h1 : bind_fun m1 m2 n = some v
n' : Nat
h : n' ≥ n
x : α
h2 : Subtype.val m1 n = some x
⊢ bind_fun m1 m2 n' = some v
Tactic:
simp_all[bind_fun]
Proof state after:
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
⊢ (match Subtype.val m1 n' with
    | none => none
    | some a => Subtype.val (m2 a) n') =
    some v
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
⊢ (match Subtype.val m1 n' with
    | none => none
    | some a => Subtype.val (m2 a) n') =
    some v
Tactic:
have m1_n'_runs : m1.val n' = some x := m1.property n x h2 n' h
Proof state after:
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
⊢ (match Subtype.val m1 n' with
    | none => none
    | some a => Subtype.val (m2 a) n') =
    some v
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
⊢ (match Subtype.val m1 n' with
    | none => none
    | some a => Subtype.val (m2 a) n') =
    some v
Tactic:
have m2_n'_runs : (m2 x).val n' = some v := (m2 x).property n v h1 n' h
Proof state after:
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