internlm/Lean-Github huggingface dataset:
Theorem: trivialNonZeroElem_trivial_nonzero
Proof state before:
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
⊢ ∀ (p : R[G]), trivialNonZeroElem p ↔ ∃ a, ∃ g, p = a * g ∧ a ≠ 0
Tactic:
apply Quotient.ind
Proof state after:
case a
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
⊢ ∀ (a : FormalSum R G),
    trivialNonZeroElem (Quotient.mk (formalSumSetoid R G) a) ↔
      ∃ a_1, ∃ g, Quotient.mk (formalSumSetoid R G) a = a_1 * g ∧ a_1 ≠ 0
Theorem: trivialNonZeroElem_trivial_nonzero
Proof state before:
case a
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
⊢ ∀ (a : FormalSum R G),
    trivialNonZeroElem (Quotient.mk (formalSumSetoid R G) a) ↔
      ∃ a_1, ∃ g, Quotient.mk (formalSumSetoid R G) a = a_1 * g ∧ a_1 ≠ 0
Tactic:
simp only [trivialNonZeroElem_trivial_nonzeroAux, ne_eq, exists_and_right, Quotient.eq, forall_const]
Proof state after:
no goals
Theorem: Cpdt.Chapter5.HasType_det
Proof state before:
e : Exp
t1 t2 : Ty
⊢ HasType e t1 → HasType e t2 → t1 = t2
Tactic:
intro h1 h2
Proof state after:
e : Exp
t1 t2 : Ty
h1 : HasType e t1
h2 : HasType e t2
⊢ t1 = t2
Theorem: Cpdt.Chapter5.HasType_det
Proof state before:
e : Exp
t1 t2 : Ty
h1 : HasType e t1
h2 : HasType e t2
⊢ t1 = t2
Tactic:
cases h1 <;> cases h2 <;> rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter5.Exp.typecheck_correct
Proof state before:
e : Exp
t : Ty
h : HasType e t
⊢ HasType e t → typecheck e ≠ Maybe.unknown → typecheck e = Maybe.found t h
Tactic:
intro ht1
Proof state after:
e : Exp
t : Ty
h ht1 : HasType e t
⊢ typecheck e ≠ Maybe.unknown → typecheck e = Maybe.found t h
Theorem: Cpdt.Chapter5.Exp.typecheck_correct
Proof state before:
e : Exp
t : Ty
h ht1 : HasType e t
⊢ typecheck e ≠ Maybe.unknown → typecheck e = Maybe.found t h
Tactic:
cases typecheck e with
| found t2 ht2 =>
  intros
  have h : t = t2 := HasType_det ht1 ht2
  simp [h]
| unknown =>
  intros
  contradiction
Proof state after:
no goals
Theorem: Cpdt.Chapter5.Exp.typecheck_correct
Proof state before:
case found
e : Exp
t : Ty
h ht1 : HasType e t
t2 : Ty
ht2 : HasType e t2
⊢ Maybe.found t2 ht2 ≠ Maybe.unknown → Maybe.found t2 ht2 = Maybe.found t h
Tactic:
intros
Proof state after:
case found
e : Exp
t : Ty
h ht1 : HasType e t
t2 : Ty
ht2 : HasType e t2
a✝ : Maybe.found t2 ht2 ≠ Maybe.unknown
⊢ Maybe.found t2 ht2 = Maybe.found t h
Theorem: Cpdt.Chapter5.Exp.typecheck_correct
Proof state before:
case found
e : Exp
t : Ty
h ht1 : HasType e t
t2 : Ty
ht2 : HasType e t2
a✝ : Maybe.found t2 ht2 ≠ Maybe.unknown
⊢ Maybe.found t2 ht2 = Maybe.found t h
Tactic:
have h : t = t2 := HasType_det ht1 ht2
Proof state after:
case found
e : Exp
t : Ty
h✝ ht1 : HasType e t
t2 : Ty
ht2 : HasType e t2
a✝ : Maybe.found t2 ht2 ≠ Maybe.unknown
h : t = t2
⊢ Maybe.found t2 ht2 = Maybe.found t h✝
Theorem: Cpdt.Chapter5.Exp.typecheck_correct
Proof state before:
case found
e : Exp
t : Ty
h✝ ht1 : HasType e t
t2 : Ty
ht2 : HasType e t2
a✝ : Maybe.found t2 ht2 ≠ Maybe.unknown
h : t = t2
⊢ Maybe.found t2 ht2 = Maybe.found t h✝
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Cpdt.Chapter5.Exp.typecheck_correct
Proof state before:
case unknown
e : Exp
t : Ty
h ht1 : HasType e t
⊢ Maybe.unknown ≠ Maybe.unknown → Maybe.unknown = Maybe.found t h
Tactic:
intros
Proof state after:
case unknown
e : Exp
t : Ty
h ht1 : HasType e t
a✝ : Maybe.unknown ≠ Maybe.unknown
⊢ Maybe.unknown = Maybe.found t h
Theorem: Cpdt.Chapter5.Exp.typecheck_correct
Proof state before:
case unknown
e : Exp
t : Ty
h ht1 : HasType e t
a✝ : Maybe.unknown ≠ Maybe.unknown
⊢ Maybe.unknown = Maybe.found t h
Tactic:
contradiction
Proof state after:
no goals
Theorem: Cpdt.Chapter5.Exp.typecheck_complete
Proof state before:
case add
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
⊢ (match typecheck l, typecheck r with
      | Maybe.found Ty.nat lth, Maybe.found Ty.nat rth => Maybe.found Ty.nat (_ : HasType (add l r) Ty.nat)
      | x, x_1 => Maybe.unknown) =
      Maybe.unknown →
    ∀ (t : Ty), ¬HasType (add l r) t
Tactic:
split
Proof state after:
case add.h_1
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
lth✝ : HasType l Ty.nat
rth✝ : HasType r Ty.nat
heq✝¹ : typecheck l = Maybe.found Ty.nat lth✝
heq✝ : typecheck r = Maybe.found Ty.nat rth✝
⊢ Maybe.found Ty.nat (_ : HasType (add l r) Ty.nat) = Maybe.unknown → ∀ (t : Ty), ¬HasType (add l r) t

case add.h_2
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝² : {{t|HasType l t}}
x✝¹ : {{t|HasType r t}}
x✝ :
  ∀ (lth : HasType l Ty.nat) (rth : HasType r Ty.nat),
    typecheck l = Maybe.found Ty.nat lth → typecheck r = Maybe.found Ty.nat rth → False
⊢ Maybe.unknown = Maybe.unknown → ∀ (t : Ty), ¬HasType (add l r) t
Theorem: Cpdt.Chapter5.Exp.typecheck_complete
Proof state before:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
htl : HasType l Ty.nat
htr : HasType r Ty.nat
rl : typecheck l = Maybe.found Ty.nat htl
rr : typecheck r = Maybe.found Ty.nat htr
⊢ Maybe.found Ty.nat (_ : HasType (add l r) Ty.nat) = Maybe.unknown → ∀ (t : Ty), ¬HasType (add l r) t
Tactic:
case add.h_1 _ _ htl htr rl rr =>
  intros
  contradiction
Proof state after:
no goals
Theorem: Cpdt.Chapter5.Exp.typecheck_complete
Proof state before:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
htl : HasType l Ty.nat
htr : HasType r Ty.nat
rl : typecheck l = Maybe.found Ty.nat htl
rr : typecheck r = Maybe.found Ty.nat htr
⊢ Maybe.found Ty.nat (_ : HasType (add l r) Ty.nat) = Maybe.unknown → ∀ (t : Ty), ¬HasType (add l r) t
Tactic:
intros
Proof state after:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
htl : HasType l Ty.nat
htr : HasType r Ty.nat
rl : typecheck l = Maybe.found Ty.nat htl
rr : typecheck r = Maybe.found Ty.nat htr
a✝ : Maybe.found Ty.nat (_ : HasType (add l r) Ty.nat) = Maybe.unknown
t✝ : Ty
⊢ ¬HasType (add l r) t✝
Theorem: Cpdt.Chapter5.Exp.typecheck_complete
Proof state before:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
htl : HasType l Ty.nat
htr : HasType r Ty.nat
rl : typecheck l = Maybe.found Ty.nat htl
rr : typecheck r = Maybe.found Ty.nat htr
a✝ : Maybe.found Ty.nat (_ : HasType (add l r) Ty.nat) = Maybe.unknown
t✝ : Ty
⊢ ¬HasType (add l r) t✝
Tactic:
contradiction
Proof state after:
no goals
Theorem: Cpdt.Chapter5.Exp.typecheck_complete
Proof state before:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
hnp :
  ∀ (lth : HasType l Ty.nat) (rth : HasType r Ty.nat),
    typecheck l = Maybe.found Ty.nat lth → typecheck r = Maybe.found Ty.nat rth → False
⊢ Maybe.unknown = Maybe.unknown → ∀ (t : Ty), ¬HasType (add l r) t
Tactic:
intro h t ht
Proof state after:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
hnp :
  ∀ (lth : HasType l Ty.nat) (rth : HasType r Ty.nat),
    typecheck l = Maybe.found Ty.nat lth → typecheck r = Maybe.found Ty.nat rth → False
h : Maybe.unknown = Maybe.unknown
t : Ty
ht : HasType (add l r) t
⊢ False
Theorem: Cpdt.Chapter5.Exp.typecheck_complete
Proof state before:
case and
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
⊢ (match typecheck l, typecheck r with
      | Maybe.found Ty.bool lth, Maybe.found Ty.bool rth => Maybe.found Ty.bool (_ : HasType (and l r) Ty.bool)
      | x, x_1 => Maybe.unknown) =
      Maybe.unknown →
    ∀ (t : Ty), ¬HasType (and l r) t
Tactic:
split
Proof state after:
case and.h_1
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
lth✝ : HasType l Ty.bool
rth✝ : HasType r Ty.bool
heq✝¹ : typecheck l = Maybe.found Ty.bool lth✝
heq✝ : typecheck r = Maybe.found Ty.bool rth✝
⊢ Maybe.found Ty.bool (_ : HasType (and l r) Ty.bool) = Maybe.unknown → ∀ (t : Ty), ¬HasType (and l r) t

case and.h_2
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝² : {{t|HasType l t}}
x✝¹ : {{t|HasType r t}}
x✝ :
  ∀ (lth : HasType l Ty.bool) (rth : HasType r Ty.bool),
    typecheck l = Maybe.found Ty.bool lth → typecheck r = Maybe.found Ty.bool rth → False
⊢ Maybe.unknown = Maybe.unknown → ∀ (t : Ty), ¬HasType (and l r) t
Theorem: Cpdt.Chapter5.Exp.typecheck_complete
Proof state before:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
htl : HasType l Ty.bool
htr : HasType r Ty.bool
rl : typecheck l = Maybe.found Ty.bool htl
rr : typecheck r = Maybe.found Ty.bool htr
⊢ Maybe.found Ty.bool (_ : HasType (and l r) Ty.bool) = Maybe.unknown → ∀ (t : Ty), ¬HasType (and l r) t
Tactic:
case and.h_1 _ _ htl htr rl rr =>
  intros
  contradiction
Proof state after:
no goals
Theorem: Cpdt.Chapter5.Exp.typecheck_complete
Proof state before:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
htl : HasType l Ty.bool
htr : HasType r Ty.bool
rl : typecheck l = Maybe.found Ty.bool htl
rr : typecheck r = Maybe.found Ty.bool htr
⊢ Maybe.found Ty.bool (_ : HasType (and l r) Ty.bool) = Maybe.unknown → ∀ (t : Ty), ¬HasType (and l r) t
Tactic:
intros
Proof state after:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
htl : HasType l Ty.bool
htr : HasType r Ty.bool
rl : typecheck l = Maybe.found Ty.bool htl
rr : typecheck r = Maybe.found Ty.bool htr
a✝ : Maybe.found Ty.bool (_ : HasType (and l r) Ty.bool) = Maybe.unknown
t✝ : Ty
⊢ ¬HasType (and l r) t✝
Theorem: Cpdt.Chapter5.Exp.typecheck_complete
Proof state before:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
htl : HasType l Ty.bool
htr : HasType r Ty.bool
rl : typecheck l = Maybe.found Ty.bool htl
rr : typecheck r = Maybe.found Ty.bool htr
a✝ : Maybe.found Ty.bool (_ : HasType (and l r) Ty.bool) = Maybe.unknown
t✝ : Ty
⊢ ¬HasType (and l r) t✝
Tactic:
contradiction
Proof state after:
no goals
Theorem: Cpdt.Chapter5.Exp.typecheck_complete
Proof state before:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
hnp :
  ∀ (lth : HasType l Ty.bool) (rth : HasType r Ty.bool),
    typecheck l = Maybe.found Ty.bool lth → typecheck r = Maybe.found Ty.bool rth → False
⊢ Maybe.unknown = Maybe.unknown → ∀ (t : Ty), ¬HasType (and l r) t
Tactic:
intro h t ht
Proof state after:
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
hnp :
  ∀ (lth : HasType l Ty.bool) (rth : HasType r Ty.bool),
    typecheck l = Maybe.found Ty.bool lth → typecheck r = Maybe.found Ty.bool rth → False
h : Maybe.unknown = Maybe.unknown
t : Ty
ht : HasType (and l r) t
⊢ False
Theorem: Cpdt.Chapter2.TExp.denote_nConst
Proof state before:
n : Nat
⊢ denote (nConst n) = n
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.TExp.denote_bConst
Proof state before:
b : Bool
⊢ denote (bConst b) = b
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.TExp.denote_binop
Proof state before:
a✝² a✝¹ a✝ : Ty
op : TBinop a✝² a✝¹ a✝
arg1 : TExp a✝²
arg2 : TExp a✝¹
⊢ denote (binop op arg1 arg2) = TBinop.denote op (denote arg1) (denote arg2)
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.TInstr.denote_inConst
Proof state before:
n : Nat
a✝ : TStack
s : VStack a✝
⊢ denote (inConst n) s = (n, s)
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.TInstr.denote_ibConst
Proof state before:
b : Bool
a✝ : TStack
s : VStack a✝
⊢ denote (ibConst b) s = (b, s)
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.TInstr.denote_iBinop
Proof state before:
a✝³ a✝² a✝¹ : Ty
op : TBinop a✝³ a✝² a✝¹
arg1 : Ty.denote a✝³
arg2 : Ty.denote a✝²
a✝ : List Ty
s' : VStack a✝
⊢ denote (iBinop op) (arg1, arg2, s') = (TBinop.denote op arg1 arg2, s')
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.TProg.denote_nil
Proof state before:
a✝ : TStack
s : VStack a✝
⊢ denote nil s = s
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.TProg.denote_cons
Proof state before:
a✝² a✝¹ : TStack
i : TInstr a✝² a✝¹
a✝ : TStack
p : TProg a✝¹ a✝
s : VStack a✝²
⊢ denote (cons i p) s = denote p (TInstr.denote i s)
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.TProg.concat_nil
Proof state before:
a✝¹ a✝ : TStack
ps : TProg a✝¹ a✝
⊢ concat nil ps = ps
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.TProg.concat_cons
Proof state before:
a✝³ a✝² : TStack
i : TInstr a✝³ a✝²
a✝¹ : TStack
ps : TProg a✝² a✝¹
a✝ : TStack
rs : TProg a✝¹ a✝
⊢ concat (cons i ps) rs = cons i (concat ps rs)
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.TExp.compile_nConst
Proof state before:
n : Nat
ts : TStack
⊢ compile (nConst n) ts = cons (inConst n) nil
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.TExp.compile_bConst
Proof state before:
b : Bool
ts : TStack
⊢ compile (bConst b) ts = cons (ibConst b) nil
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.TExp.compile_binop
Proof state before:
r a✝ : Ty
op : TBinop a✝ r r
arg1 : TExp a✝
arg2 : TExp r
ts : TStack
⊢ compile (binop op arg1 arg2) ts = concat (compile arg2 ts) (concat (compile arg1 (r :: ts)) (cons (iBinop op) nil))
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter2.TExp.concat_correct
Proof state before:
ts1 ts2 ts3 : TStack
⊢ ∀ (p1 : TProg ts1 ts2) (p2 : TProg ts2 ts3) (s : VStack ts1),
    TProg.denote (concat p1 p2) s = TProg.denote p2 (TProg.denote p1 s)
Tactic:
intro p1
Proof state after:
ts1 ts2 ts3 : TStack
p1 : TProg ts1 ts2
⊢ ∀ (p2 : TProg ts2 ts3) (s : VStack ts1), TProg.denote (concat p1 p2) s = TProg.denote p2 (TProg.denote p1 s)
Theorem: Cpdt.Chapter2.TExp.concat_correct
Proof state before:
ts1 ts2 ts3 : TStack
p1 : TProg ts1 ts2
⊢ ∀ (p2 : TProg ts2 ts3) (s : VStack ts1), TProg.denote (concat p1 p2) s = TProg.denote p2 (TProg.denote p1 s)
Tactic:
induction p1 <;> simp_all
Proof state after:
no goals
Theorem: Cpdt.Chapter2.TExp.compile_correct_helper
Proof state before:
t : Ty
⊢ ∀ (e : TExp t) (ts : TStack) (s : VStack ts), TProg.denote (compile e ts) s = (denote e, s)
Tactic:
intro e
Proof state after:
t : Ty
e : TExp t
⊢ ∀ (ts : TStack) (s : VStack ts), TProg.denote (compile e ts) s = (denote e, s)
Theorem: Cpdt.Chapter2.TExp.compile_correct_helper
Proof state before:
t : Ty
e : TExp t
⊢ ∀ (ts : TStack) (s : VStack ts), TProg.denote (compile e ts) s = (denote e, s)
Tactic:
induction e <;> simp_all[compile, concat_correct]
Proof state after:
no goals
Theorem: Cpdt.Chapter2.TExp.compile_correct
Proof state before:
t : Ty
⊢ ∀ (e : TExp t), TProg.denote (compile e []) () = (denote e, ())
Tactic:
simp [compile_correct_helper]
Proof state after:
no goals
Theorem: Cpdt.Chapter4.add_IsZero
Proof state before:
m n : Nat
⊢ IsZero m → n + m = n
Tactic:
intro h
Proof state after:
m n : Nat
h : IsZero m
⊢ n + m = n
Theorem: Cpdt.Chapter4.add_IsZero
Proof state before:
m n : Nat
h : IsZero m
⊢ n + m = n
Tactic:
cases h
Proof state after:
case zero
n : Nat
⊢ n + 0 = n
Theorem: Cpdt.Chapter4.add_IsZero
Proof state before:
case zero
n : Nat
⊢ n + 0 = n
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter4.IsZero_contra
Proof state before:
⊢ IsZero 1 → False
Tactic:
intro h
Proof state after:
h : IsZero 1
⊢ False
Theorem: Cpdt.Chapter4.IsZero_contra
Proof state before:
h : IsZero 1
⊢ False
Tactic:
cases h
Proof state after:
no goals
Theorem: Cpdt.Chapter3.Bool.toProp_false
Proof state before:
⊢ toProp false = False
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter3.Bool.toProp_true
Proof state before:
⊢ toProp true = True
Tactic:
rfl
Proof state after:
no goals
Theorem: Cpdt.Chapter3.true_neq_false
Proof state before:
⊢ true ≠ false
Tactic:
intro h
Proof state after:
h : true = false
⊢ False
Theorem: Cpdt.Chapter3.true_neq_false
Proof state before:
h : true = false
⊢ False
Tactic:
rw [←Bool.toProp_false]
Proof state after:
h : true = false
⊢ Bool.toProp false
Theorem: Cpdt.Chapter3.true_neq_false
Proof state before:
h : true = false
⊢ Bool.toProp false
Tactic:
rw [←h]
Proof state after:
h : true = false
⊢ Bool.toProp true
Theorem: Cpdt.Chapter3.true_neq_false
Proof state before:
h : true = false
⊢ Bool.toProp true
Tactic:
rw [Bool.toProp_true]
Proof state after:
h : true = false
⊢ True
Theorem: Cpdt.Chapter3.true_neq_false
Proof state before:
h : true = false
⊢ True
Tactic:
exact True.intro
Proof state after:
no goals
Theorem: Cpdt.Chapter3.s_inj
Proof state before:
n m : Nat
⊢ Nat.succ n = Nat.succ m → n = m
Tactic:
intro h
Proof state after:
n m : Nat
h : Nat.succ n = Nat.succ m
⊢ n = m
Theorem: Cpdt.Chapter3.s_inj
Proof state before:
n m : Nat
h : Nat.succ n = Nat.succ m
⊢ n = m
Tactic:
rw [←Nat.pred_succ n]
Proof state after:
n m : Nat
h : Nat.succ n = Nat.succ m
⊢ Nat.pred (Nat.succ n) = m
Theorem: Cpdt.Chapter3.s_inj
Proof state before:
n m : Nat
h : Nat.succ n = Nat.succ m
⊢ Nat.pred (Nat.succ n) = m
Tactic:
rw [←Nat.pred_succ m]
Proof state after:
n m : Nat
h : Nat.succ n = Nat.succ m
⊢ Nat.pred (Nat.succ n) = Nat.pred (Nat.succ m)
Theorem: Cpdt.Chapter3.s_inj
Proof state before:
n m : Nat
h : Nat.succ n = Nat.succ m
⊢ Nat.pred (Nat.succ n) = Nat.pred (Nat.succ m)
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Cpdt.Chapter4.even4
Proof state before:
⊢ Even 4
Tactic:
simp[Even.succSucc, Even.zero]
Proof state after:
no goals
Theorem: Cpdt.Chapter4.even_3_contra
Proof state before:
⊢ Even 3 → False
Tactic:
intro h
Proof state after:
h : Even 3
⊢ False
Theorem: Cpdt.Chapter4.even_3_contra
Proof state before:
h : Even 3
⊢ False
Tactic:
cases h with
| succSucc _ h => cases h
Proof state after:
no goals
Theorem: Cpdt.Chapter4.even_3_contra
Proof state before:
case succSucc
h : Even 1
⊢ False
Tactic:
cases h
Proof state after:
no goals
Theorem: Cpdt.Chapter4.even_add
Proof state before:
n m : Nat
⊢ Even n → Even m → Even (n + m)
Tactic:
intro h1
Proof state after:
n m : Nat
h1 : Even n
⊢ Even m → Even (n + m)
Theorem: Cpdt.Chapter4.even_add
Proof state before:
n m : Nat
h1 : Even n
⊢ Even m → Even (n + m)
Tactic:
induction h1 with
| zero =>
  intro h
  simp_arith
  assumption
| succSucc x xh ih =>
  intro h
  simp_arith
  constructor
  simp_arith
  apply ih
  assumption
Proof state after:
no goals
Theorem: Cpdt.Chapter4.even_add
Proof state before:
case zero
n m : Nat
⊢ Even m → Even (0 + m)
Tactic:
intro h
Proof state after:
case zero
n m : Nat
h : Even m
⊢ Even (0 + m)
Theorem: Cpdt.Chapter4.even_add
Proof state before:
case zero
n m : Nat
h : Even m
⊢ Even (0 + m)
Tactic:
simp_arith
Proof state after:
case zero
n m : Nat
h : Even m
⊢ Even m
Theorem: Cpdt.Chapter4.even_add
Proof state before:
case zero
n m : Nat
h : Even m
⊢ Even m
Tactic:
assumption
Proof state after:
no goals
Theorem: Cpdt.Chapter4.even_add
Proof state before:
case succSucc
n m x : Nat
xh : Even x
ih : Even m → Even (x + m)
⊢ Even m → Even (Nat.succ (Nat.succ x) + m)
Tactic:
intro h
Proof state after:
case succSucc
n m x : Nat
xh : Even x
ih : Even m → Even (x + m)
h : Even m
⊢ Even (Nat.succ (Nat.succ x) + m)
Theorem: Cpdt.Chapter4.even_add
Proof state before:
case succSucc
n m x : Nat
xh : Even x
ih : Even m → Even (x + m)
h : Even m
⊢ Even (Nat.succ (Nat.succ x) + m)
Tactic:
simp_arith
Proof state after:
case succSucc
n m x : Nat
xh : Even x
ih : Even m → Even (x + m)
h : Even m
⊢ Even (x + m + 2)
Theorem: Cpdt.Chapter4.even_add
Proof state before:
case succSucc
n m x : Nat
xh : Even x
ih : Even m → Even (x + m)
h : Even m
⊢ Even (x + m + 2)
Tactic:
constructor
Proof state after:
case succSucc.a
n m x : Nat
xh : Even x
ih : Even m → Even (x + m)
h : Even m
⊢ Even (x + m)
Theorem: Cpdt.Chapter4.even_contra_helper
Proof state before:
⊢ ∀ (n' : Nat), Even n' → ∀ (n : Nat), n' ≠ Nat.succ (n + n)
Tactic:
intro n' hn'
Proof state after:
n' : Nat
hn' : Even n'
⊢ ∀ (n : Nat), n' ≠ Nat.succ (n + n)
Theorem: Cpdt.Chapter4.even_contra_helper
Proof state before:
n' : Nat
hn' : Even n'
⊢ ∀ (n : Nat), n' ≠ Nat.succ (n + n)
Tactic:
induction hn' with
| zero => simp_all
| succSucc x hx ih =>
  intro n hn
  cases x <;> cases n <;> simp_all <;> simp_arith at *
  case succSucc.succ.succ y m =>
    apply ih m
    assumption
Proof state after:
no goals
Theorem: Cpdt.Chapter4.even_contra_helper
Proof state before:
case zero
n' : Nat
⊢ ∀ (n : Nat), 0 ≠ Nat.succ (n + n)
Tactic:
simp_all
Proof state after:
no goals
Theorem: Cpdt.Chapter4.even_contra_helper
Proof state before:
case succSucc
n' x : Nat
hx : Even x
ih : ∀ (n : Nat), x ≠ Nat.succ (n + n)
⊢ ∀ (n : Nat), Nat.succ (Nat.succ x) ≠ Nat.succ (n + n)
Tactic:
intro n hn
Proof state after:
case succSucc
n' x : Nat
hx : Even x
ih : ∀ (n : Nat), x ≠ Nat.succ (n + n)
n : Nat
hn : Nat.succ (Nat.succ x) = Nat.succ (n + n)
⊢ False
Theorem: Cpdt.Chapter4.even_contra_helper
Proof state before:
case succSucc
n' x : Nat
hx : Even x
ih : ∀ (n : Nat), x ≠ Nat.succ (n + n)
n : Nat
hn : Nat.succ (Nat.succ x) = Nat.succ (n + n)
⊢ False
Tactic:
cases x <;> cases n <;> simp_all <;> simp_arith at *
Proof state after:
case succSucc.succ.succ
n' n✝¹ : Nat
hx : Even (Nat.succ n✝¹)
n✝ : Nat
ih : ∀ (n : Nat), ¬n✝¹ = 2 * n
hn : n✝¹ = 2 * n✝
⊢ False
Theorem: Cpdt.Chapter4.even_contra_helper
Proof state before:
n' y : Nat
hx : Even (Nat.succ y)
m : Nat
ih : ∀ (n : Nat), ¬y = 2 * n
hn : y = 2 * m
⊢ False
Tactic:
case succSucc.succ.succ y m =>
  apply ih m
  assumption
Proof state after:
no goals
Theorem: Cpdt.Chapter4.even_contra_helper
Proof state before:
n' y : Nat
hx : Even (Nat.succ y)
m : Nat
ih : ∀ (n : Nat), ¬y = 2 * n
hn : y = 2 * m
⊢ False
Tactic:
apply ih m
Proof state after:
n' y : Nat
hx : Even (Nat.succ y)
m : Nat
ih : ∀ (n : Nat), ¬y = 2 * n
hn : y = 2 * m
⊢ y = 2 * m
Theorem: Cpdt.Chapter4.even_contra_helper
Proof state before:
n' y : Nat
hx : Even (Nat.succ y)
m : Nat
ih : ∀ (n : Nat), ¬y = 2 * n
hn : y = 2 * m
⊢ y = 2 * m
Tactic:
assumption
Proof state after:
no goals
Theorem: Cpdt.Chapter4.even_contra
Proof state before:
n : Nat
⊢ Even (Nat.succ (n + n)) → False
Tactic:
intro h
Proof state after:
n : Nat
h : Even (Nat.succ (n + n))
⊢ False
Theorem: Cpdt.Chapter4.even_contra
Proof state before:
n : Nat
h : Even (Nat.succ (n + n))
⊢ False
Tactic:
apply even_contra_helper
Proof state after:
case a
n : Nat
h : Even (Nat.succ (n + n))
⊢ Even ?n'

case a
n : Nat
h : Even (Nat.succ (n + n))
⊢ ?n' = Nat.succ (?n + ?n)

case n'
n : Nat
h : Even (Nat.succ (n + n))
⊢ Nat

case n
n : Nat
h : Even (Nat.succ (n + n))
⊢ Nat
Theorem: Cpdt.Chapter4.even_contra
Proof state before:
case a
n : Nat
h : Even (Nat.succ (n + n))
⊢ Even ?n'

case a
n : Nat
h : Even (Nat.succ (n + n))
⊢ ?n' = Nat.succ (?n + ?n)

case n'
n : Nat
h : Even (Nat.succ (n + n))
⊢ Nat

case n
n : Nat
h : Even (Nat.succ (n + n))
⊢ Nat
Tactic:
assumption
Proof state after:
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