internlm/Lean-Github huggingface dataset:
Theorem: LoVe.BTree.map_mirror
Proof state before:
case node.hr
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (map f r)

case node.hiff
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ map f l = empty ↔ map f r = empty
Tactic:
{ exact ihr }
Proof state after:
case node.hiff
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ map f l = empty ↔ map f r = empty
Theorem: LoVe.BTree.map_mirror
Proof state before:
case node.hiff
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ map f l = empty ↔ map f r = empty
Tactic:
{ simp [BTree.map_eq_empty_iff]
  assumption }
Proof state after:
no goals
Theorem: LoVe.BTree.map_mirror
Proof state before:
case node.hl
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (map f l)
Tactic:
exact ihl
Proof state after:
no goals
Theorem: LoVe.BTree.map_mirror
Proof state before:
case node.hr
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (map f r)
Tactic:
exact ihr
Proof state after:
no goals
Theorem: LoVe.BTree.map_mirror
Proof state before:
case node.hiff
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ map f l = empty ↔ map f r = empty
Tactic:
simp [BTree.map_eq_empty_iff]
Proof state after:
case node.hiff
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ l = empty ↔ r = empty
Theorem: LoVe.BTree.map_mirror
Proof state before:
case node.hiff
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ l = empty ↔ r = empty
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.proof_irrel
Proof state before:
a : Prop
h₁ h₂ : a
⊢ h₁ = h₂
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.FullBTree.mirror_mirror
Proof state before:
α : Type
t : FullBTree α
⊢ mirror (mirror t) = t
Tactic:
apply Subtype.eq
Proof state after:
case a
α : Type
t : FullBTree α
⊢ ↑(mirror (mirror t)) = ↑t
Theorem: LoVe.FullBTree.mirror_mirror
Proof state before:
case a
α : Type
t : FullBTree α
⊢ ↑(mirror (mirror t)) = ↑t
Tactic:
simp [FullBTree.mirror, LoVe.mirror_mirror]
Proof state after:
no goals
Theorem: LoVe.Vector.neg_neg
Proof state before:
n : ℕ
v : Vector ℤ n
⊢ neg (neg v) = v
Tactic:
apply Subtype.eq
Proof state after:
case a
n : ℕ
v : Vector ℤ n
⊢ ↑(neg (neg v)) = ↑v
Theorem: LoVe.Vector.neg_neg
Proof state before:
case a
n : ℕ
v : Vector ℤ n
⊢ ↑(neg (neg v)) = ↑v
Tactic:
simp [Vector.neg]
Proof state after:
no goals
Theorem: LoVe.Int.Setoid_Iff
Proof state before:
pn₁ pn₂ : ℕ × ℕ
⊢ pn₁ ≈ pn₂ ↔ pn₁.fst + pn₂.snd = pn₂.fst + pn₁.snd
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.Int.zero_Eq
Proof state before:
m : ℕ
⊢ zero = Quotient.mk Setoid (m, m)
Tactic:
rw [Int.zero]
Proof state after:
m : ℕ
⊢ Quotient.mk Setoid (0, 0) = Quotient.mk Setoid (m, m)
Theorem: LoVe.Int.zero_Eq
Proof state before:
m : ℕ
⊢ Quotient.mk Setoid (0, 0) = Quotient.mk Setoid (m, m)
Tactic:
apply Quotient.sound
Proof state after:
case a
m : ℕ
⊢ (0, 0) ≈ (m, m)
Theorem: LoVe.Int.zero_Eq
Proof state before:
case a
m : ℕ
⊢ (0, 0) ≈ (m, m)
Tactic:
rw [Int.Setoid_Iff]
Proof state after:
case a
m : ℕ
⊢ (0, 0).fst + (m, m).snd = (m, m).fst + (0, 0).snd
Theorem: LoVe.Int.zero_Eq
Proof state before:
case a
m : ℕ
⊢ (0, 0).fst + (m, m).snd = (m, m).fst + (0, 0).snd
Tactic:
simp
Proof state after:
no goals
Theorem: LoVe.Int.add_Eq
Proof state before:
p₁ n₁ p₂ n₂ : ℕ
⊢ add (Quotient.mk Setoid (p₁, n₁)) (Quotient.mk Setoid (p₂, n₂)) = Quotient.mk Setoid (p₁ + p₂, n₁ + n₂)
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.Int.add_zero
Proof state before:
i : Int
⊢ add zero i = i
Tactic:
induction i using Quotient.inductionOn with
| h pn =>
  cases pn with
  | mk p n => simp [Int.zero, Int.add_Eq]
Proof state after:
no goals
Theorem: LoVe.Int.add_zero
Proof state before:
case h
pn : ℕ × ℕ
⊢ add zero (Quotient.mk Setoid pn) = Quotient.mk Setoid pn
Tactic:
cases pn with
| mk p n => simp [Int.zero, Int.add_Eq]
Proof state after:
no goals
Theorem: LoVe.Int.add_zero
Proof state before:
case h.mk
p n : ℕ
⊢ add zero (Quotient.mk Setoid (p, n)) = Quotient.mk Setoid (p, n)
Tactic:
simp [Int.zero, Int.add_Eq]
Proof state after:
no goals
Theorem: LoVe.UPair.Setoid_Iff
Proof state before:
α : Type
ab₁ ab₂ : α × α
⊢ ab₁ ≈ ab₂ ↔ {ab₁.fst, ab₁.snd} = {ab₂.fst, ab₂.snd}
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.UPair.mk_symm
Proof state before:
α : Type
a b : α
⊢ Quotient.mk (Setoid α) (a, b) = Quotient.mk (Setoid α) (b, a)
Tactic:
apply Quotient.sound
Proof state after:
case a
α : Type
a b : α
⊢ (a, b) ≈ (b, a)
Theorem: LoVe.UPair.mk_symm
Proof state before:
case a
α : Type
a b : α
⊢ (a, b) ≈ (b, a)
Tactic:
rw [UPair.Setoid_Iff]
Proof state after:
case a
α : Type
a b : α
⊢ {(a, b).fst, (a, b).snd} = {(b, a).fst, (b, a).snd}
Theorem: LoVe.UPair.mk_symm
Proof state before:
case a
α : Type
a b : α
⊢ {(a, b).fst, (a, b).snd} = {(b, a).fst, (b, a).snd}
Tactic:
simp [Set.unordered_pair_comm]
Proof state after:
no goals
Theorem: LoVe.Alternative.Int.IsCanonical_normalize
Proof state before:
pn : ℕ × ℕ
⊢ IsCanonical (normalize pn)
Tactic:
cases pn with
| mk p n =>
  simp [Int.normalize]
  cases Classical.em (p ≥ n) with
  | inl hpn =>
    simp [*]
    exact Int.IsCanonical.nonneg
  | inr hpn =>
    simp [*]
    exact Int.IsCanonical.nonpos
Proof state after:
no goals
Theorem: LoVe.Alternative.Int.IsCanonical_normalize
Proof state before:
case mk
p n : ℕ
⊢ IsCanonical (normalize (p, n))
Tactic:
simp [Int.normalize]
Proof state after:
case mk
p n : ℕ
⊢ IsCanonical (if n ≤ p then (p - n, 0) else (0, n - p))
Theorem: LoVe.Alternative.Int.IsCanonical_normalize
Proof state before:
case mk
p n : ℕ
⊢ IsCanonical (if n ≤ p then (p - n, 0) else (0, n - p))
Tactic:
cases Classical.em (p ≥ n) with
| inl hpn =>
  simp [*]
  exact Int.IsCanonical.nonneg
| inr hpn =>
  simp [*]
  exact Int.IsCanonical.nonpos
Proof state after:
no goals
Theorem: LoVe.Alternative.Int.IsCanonical_normalize
Proof state before:
case mk.inl
p n : ℕ
hpn : p ≥ n
⊢ IsCanonical (if n ≤ p then (p - n, 0) else (0, n - p))
Tactic:
simp [*]
Proof state after:
case mk.inl
p n : ℕ
hpn : p ≥ n
⊢ IsCanonical (p - n, 0)
Theorem: LoVe.Alternative.Int.IsCanonical_normalize
Proof state before:
case mk.inl
p n : ℕ
hpn : p ≥ n
⊢ IsCanonical (p - n, 0)
Tactic:
exact Int.IsCanonical.nonneg
Proof state after:
no goals
Theorem: LoVe.Alternative.Int.IsCanonical_normalize
Proof state before:
case mk.inr
p n : ℕ
hpn : ¬p ≥ n
⊢ IsCanonical (if n ≤ p then (p - n, 0) else (0, n - p))
Tactic:
simp [*]
Proof state after:
case mk.inr
p n : ℕ
hpn : ¬p ≥ n
⊢ IsCanonical (0, n - p)
Theorem: LoVe.Alternative.Int.IsCanonical_normalize
Proof state before:
case mk.inr
p n : ℕ
hpn : ¬p ≥ n
⊢ IsCanonical (0, n - p)
Tactic:
exact Int.IsCanonical.nonpos
Proof state after:
no goals
Theorem: LoVe.repeat'_example
Proof state before:
⊢ Even 4 ∧ Even 7 ∧ Even 3 ∧ Even 0
Tactic:
repeat' apply And.intro
Proof state after:
case left

⊢ Even 4

case right.left

⊢ Even 7

case right.right.left

⊢ Even 3

case right.right.right

⊢ Even 0
Theorem: LoVe.repeat'_example
Proof state before:
case left

⊢ Even 4

case right.left

⊢ Even 7

case right.right.left

⊢ Even 3

case right.right.right

⊢ Even 0
Tactic:
repeat' apply Even.add_two
Proof state after:
case left.a.a

⊢ Even 0

case right.left.a.a.a

⊢ Even 1

case right.right.left.a

⊢ Even 1

case right.right.right

⊢ Even 0
Theorem: LoVe.repeat'_example
Proof state before:
case left.a.a

⊢ Even 0

case right.left.a.a.a

⊢ Even 1

case right.right.left.a

⊢ Even 1

case right.right.right

⊢ Even 0
Tactic:
repeat' sorry
Proof state after:
no goals
Theorem: LoVe.repeat'_example
Proof state before:
case right.right

⊢ Even 3 ∧ Even 0
Tactic:
apply And.intro
Proof state after:
case right.right.left

⊢ Even 3

case right.right.right

⊢ Even 0
Theorem: LoVe.repeat'_example
Proof state before:
case right.right.left

⊢ Even 3
Tactic:
apply Even.add_two
Proof state after:
case right.right.left.a

⊢ Even 1
Theorem: LoVe.repeat'_example
Proof state before:
case right.right.right

⊢ Even 0
Tactic:
sorry
Proof state after:
no goals
Theorem: LoVe.repeat'_first_example
Proof state before:
⊢ Even 4 ∧ Even 7 ∧ Even 3 ∧ Even 0
Tactic:
repeat' apply And.intro
Proof state after:
case left

⊢ Even 4

case right.left

⊢ Even 7

case right.right.left

⊢ Even 3

case right.right.right

⊢ Even 0
Theorem: LoVe.repeat'_first_example
Proof state before:
case left

⊢ Even 4

case right.left

⊢ Even 7

case right.right.left

⊢ Even 3

case right.right.right

⊢ Even 0
Tactic:
repeat'
  first
  | apply Even.add_two
  | apply Even.zero
Proof state after:
case right.left.a.a.a

⊢ Even 1

case right.right.left.a

⊢ Even 1
Theorem: LoVe.repeat'_first_example
Proof state before:
case right.left.a.a.a

⊢ Even 1

case right.right.left.a

⊢ Even 1
Tactic:
repeat' sorry
Proof state after:
no goals
Theorem: LoVe.repeat'_first_example
Proof state before:
case right.right

⊢ Even 3 ∧ Even 0
Tactic:
apply And.intro
Proof state after:
case right.right.left

⊢ Even 3

case right.right.right

⊢ Even 0
Theorem: LoVe.repeat'_first_example
Proof state before:
case right.right.right

⊢ Even 0
Tactic:
first
| apply Even.add_two
| apply Even.zero
Proof state after:
no goals
Theorem: LoVe.repeat'_first_example
Proof state before:
case right.right.left

⊢ Even 3
Tactic:
apply Even.add_two
Proof state after:
case right.right.left.a

⊢ Even 1
Theorem: LoVe.repeat'_first_example
Proof state before:
case right.right.right

⊢ Even 0
Tactic:
apply Even.zero
Proof state after:
no goals
Theorem: LoVe.repeat'_first_example
Proof state before:
case right.right.left.a

⊢ Even 1
Tactic:
sorry
Proof state after:
no goals
Theorem: LoVe.all_goals_try_example
Proof state before:
⊢ Even 4 ∧ Even 7 ∧ Even 3 ∧ Even 0
Tactic:
repeat' apply And.intro
Proof state after:
case left

⊢ Even 4

case right.left

⊢ Even 7

case right.right.left

⊢ Even 3

case right.right.right

⊢ Even 0
Theorem: LoVe.all_goals_try_example
Proof state before:
case left

⊢ Even 4

case right.left

⊢ Even 7

case right.right.left

⊢ Even 3

case right.right.right

⊢ Even 0
Tactic:
all_goals try apply Even.add_two
Proof state after:
case left.a

⊢ Even 2

case right.left.a

⊢ Even 5

case right.right.left.a

⊢ Even 1

case right.right.right

⊢ Even 0
Theorem: LoVe.all_goals_try_example
Proof state before:
case left.a

⊢ Even 2

case right.left.a

⊢ Even 5

case right.right.left.a

⊢ Even 1

case right.right.right

⊢ Even 0
Tactic:
repeat sorry
Proof state after:
no goals
Theorem: LoVe.all_goals_try_example
Proof state before:
case right.right

⊢ Even 3 ∧ Even 0
Tactic:
apply And.intro
Proof state after:
case right.right.left

⊢ Even 3

case right.right.right

⊢ Even 0
Theorem: LoVe.all_goals_try_example
Proof state before:
case right.right.left

⊢ Even 3
Tactic:
try apply Even.add_two
Proof state after:
case right.right.left.a

⊢ Even 1
Theorem: LoVe.all_goals_try_example
Proof state before:
case right.right.left

⊢ Even 3
Tactic:
apply Even.add_two
Proof state after:
case right.right.left.a

⊢ Even 1
Theorem: LoVe.all_goals_try_example
Proof state before:
case right.right.right

⊢ Even 0
Tactic:
sorry
Proof state after:
no goals
Theorem: LoVe.any_goals_example
Proof state before:
⊢ Even 4 ∧ Even 7 ∧ Even 3 ∧ Even 0
Tactic:
repeat' apply And.intro
Proof state after:
case left

⊢ Even 4

case right.left

⊢ Even 7

case right.right.left

⊢ Even 3

case right.right.right

⊢ Even 0
Theorem: LoVe.any_goals_example
Proof state before:
case left

⊢ Even 4

case right.left

⊢ Even 7

case right.right.left

⊢ Even 3

case right.right.right

⊢ Even 0
Tactic:
any_goals apply Even.add_two
Proof state after:
case left.a

⊢ Even 2

case right.left.a

⊢ Even 5

case right.right.left.a

⊢ Even 1

case right.right.right

⊢ Even 0
Theorem: LoVe.any_goals_example
Proof state before:
case left.a

⊢ Even 2

case right.left.a

⊢ Even 5

case right.right.left.a

⊢ Even 1

case right.right.right

⊢ Even 0
Tactic:
repeat' sorry
Proof state after:
no goals
Theorem: LoVe.any_goals_example
Proof state before:
case right.right

⊢ Even 3 ∧ Even 0
Tactic:
apply And.intro
Proof state after:
case right.right.left

⊢ Even 3

case right.right.right

⊢ Even 0
Theorem: LoVe.any_goals_example
Proof state before:
case right.right.left

⊢ Even 3
Tactic:
apply Even.add_two
Proof state after:
case right.right.left.a

⊢ Even 1
Theorem: LoVe.any_goals_example
Proof state before:
case right.right.right

⊢ Even 0
Tactic:
sorry
Proof state after:
no goals
Theorem: LoVe.any_goals_solve_repeat_first_example
Proof state before:
⊢ Even 4 ∧ Even 7 ∧ Even 3 ∧ Even 0
Tactic:
repeat' apply And.intro
Proof state after:
case left

⊢ Even 4

case right.left

⊢ Even 7

case right.right.left

⊢ Even 3

case right.right.right

⊢ Even 0
Theorem: LoVe.any_goals_solve_repeat_first_example
Proof state before:
case left

⊢ Even 4

case right.left

⊢ Even 7

case right.right.left

⊢ Even 3

case right.right.right

⊢ Even 0
Tactic:
any_goals
  solve
  | repeat'
      first
      | apply Even.add_two
      | apply Even.zero
Proof state after:
case right.left

⊢ Even 7

case right.right.left

⊢ Even 3
Theorem: LoVe.any_goals_solve_repeat_first_example
Proof state before:
case right.left

⊢ Even 7

case right.right.left

⊢ Even 3
Tactic:
repeat' sorry
Proof state after:
no goals
Theorem: LoVe.any_goals_solve_repeat_first_example
Proof state before:
case right.right

⊢ Even 3 ∧ Even 0
Tactic:
apply And.intro
Proof state after:
case right.right.left

⊢ Even 3

case right.right.right

⊢ Even 0
Theorem: LoVe.any_goals_solve_repeat_first_example
Proof state before:
case right.right.right

⊢ Even 0
Tactic:
solve
| repeat'
    first
    | apply Even.add_two
    | apply Even.zero
Proof state after:
no goals
Theorem: LoVe.any_goals_solve_repeat_first_example
Proof state before:
case right.right.right

⊢ Even 0
Tactic:
repeat'
  first
  | apply Even.add_two
  | apply Even.zero
Proof state after:
no goals
Theorem: LoVe.any_goals_solve_repeat_first_example
Proof state before:
case right.right.right

⊢ Even 0
Tactic:
first
| apply Even.add_two
| apply Even.zero
Proof state after:
no goals
Theorem: LoVe.any_goals_solve_repeat_first_example
Proof state before:
case right.right.left

⊢ Even 3
Tactic:
apply Even.add_two
Proof state after:
case right.right.left.a

⊢ Even 1
Theorem: LoVe.any_goals_solve_repeat_first_example
Proof state before:
case right.right.right

⊢ Even 0
Tactic:
apply Even.zero
Proof state after:
no goals
Theorem: LoVe.any_goals_solve_repeat_first_example
Proof state before:
case right.right.left

⊢ Even 3
Tactic:
sorry
Proof state after:
no goals
Theorem: LoVe.intro_and_even_example
Proof state before:
⊢ Even 4 ∧ Even 7 ∧ Even 3 ∧ Even 0
Tactic:
intro_and_even
Proof state after:
case right.left

⊢ Even 7

case right.right.left

⊢ Even 3
Theorem: LoVe.intro_and_even_example
Proof state before:
case right.left

⊢ Even 7

case right.right.left

⊢ Even 3
Tactic:
repeat' sorry
Proof state after:
no goals
Theorem: LoVe.intro_and_even_example
Proof state before:
case right.right.left

⊢ Even 3
Tactic:
sorry
Proof state after:
no goals
Theorem: LoVe.Even_18_and_Even_20
Proof state before:
α : Type
a : α
⊢ Even 18 ∧ Even 20
Tactic:
apply And.intro
Proof state after:
case left
α : Type
a : α
⊢ Even 18

case right
α : Type
a : α
⊢ Even 20
Theorem: LoVe.Even_18_and_Even_20
Proof state before:
case left
α : Type
a : α
⊢ Even 18

case right
α : Type
a : α
⊢ Even 20
Tactic:
intro_and_even
Proof state after:
no goals
Theorem: LoVe.hypothesis_example
Proof state before:
α : Type
p : α → Prop
a : α
hpa : p a
⊢ p a
Tactic:
hypothesis
Proof state after:
no goals
Theorem: LoVe.abc_a_again
Proof state before:
a b c : Prop
h : a ∧ b ∧ c
⊢ a
Tactic:
destruct_and h
Proof state after:
no goals
Theorem: LoVe.abc_b_again
Proof state before:
a b c : Prop
h : a ∧ b ∧ c
⊢ b
Tactic:
destruct_and h
Proof state after:
no goals
Theorem: LoVe.abc_bc_again
Proof state before:
a b c : Prop
h : a ∧ b ∧ c
⊢ b ∧ c
Tactic:
destruct_and h
Proof state after:
no goals
Theorem: LoVe.abc_c_again
Proof state before:
a b c : Prop
h : a ∧ b ∧ c
⊢ c
Tactic:
destruct_and h
Proof state after:
no goals
Theorem: LoVe.Nat.Eq_symm
Proof state before:
x y : ℕ
h : x = y
⊢ y = x
Tactic:
prove_direct
Proof state after:
no goals
Theorem: LoVe.Nat.Eq_symm_manual
Proof state before:
x y : ℕ
h : x = y
⊢ y = x
Tactic:
apply symm
Proof state after:
case a
x y : ℕ
h : x = y
⊢ x = y
Theorem: LoVe.Nat.Eq_symm_manual
Proof state before:
case a
x y : ℕ
h : x = y
⊢ x = y
Tactic:
hypothesis
Proof state after:
no goals
Theorem: LoVe.Nat.Eq_trans
Proof state before:
x y z : ℕ
hxy : x = y
hyz : y = z
⊢ x = z
Tactic:
prove_direct
Proof state after:
no goals
Theorem: LoVe.List.reverse_twice
Proof state before:
xs : List ℕ
⊢ List.reverse (List.reverse xs) = xs
Tactic:
prove_direct
Proof state after:
no goals
Theorem: LoVe.List.reverse_twice_library_search
Proof state before:
xs : List ℕ
⊢ List.reverse (List.reverse xs) = xs
Tactic:
library_search
Proof state after:
no goals
Theorem: LoVe.reverseAccu_Eq_reverse_append
Proof state before:
α : Type
as : List α
⊢ reverseAccu as [] = reverse [] ++ as
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.reverseAccu_Eq_reverse_append
Proof state before:
α : Type
as : List α
x : α
xs : List α
⊢ reverseAccu as (x :: xs) = reverse (x :: xs) ++ as
Tactic:
simp [reverse, reverseAccu, reverseAccu_Eq_reverse_append _ xs]
Proof state after:
no goals
Theorem: LoVe.reverseAccu_eq_reverse
Proof state before:
α : Type
xs : List α
⊢ reverseAccu [] xs = reverse xs
Tactic:
simp [reverseAccu_Eq_reverse_append]
Proof state after:
no goals
Theorem: LoVe.reverseAccu_reverseAccu
Proof state before:
α : Type
xs : List α
⊢ reverseAccu [] (reverseAccu [] xs) = xs
Tactic:
simp [reverseAccu_eq_reverse, reverse_reverse]
Proof state after:
no goals
Theorem: LoVe.Vec.meld_append
Proof state before:
α β γ : Type
m n : ℕ
f : α → β → γ
xs : Vec α m
ys : Vec β m
⊢ meld f (append V[] xs) (append V[] ys) = append (meld f V[] V[]) (meld f xs ys)
Tactic:
simp [append, meld]
Proof state after:
no goals
Theorem: LoVe.Vec.meld_append
Proof state before:
α β γ : Type
m n : ℕ
f : α → β → γ
v : α
n✝ : ℕ
vs : Vec α n✝
w : β
ws : Vec β n✝
xs : Vec α m
ys : Vec β m
ih : meld f (append vs xs) (append ws ys) = append (meld f vs ws) (meld f xs ys)
⊢ cons (f v w) (meld f (append vs xs) (append ws ys)) = cons (f v w) (append (meld f vs ws) (meld f xs ys))
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: LoVe.drop_nil
Proof state before:
α : Type
⊢ drop 0 [] = []
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.drop_nil
Proof state before:
α : Type
n✝ : ℕ
⊢ drop (n✝ + 1) [] = []
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.take_nil
Proof state before:
α : Type
⊢ take 0 [] = []
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.take_nil
Proof state before:
α : Type
n✝ : ℕ
⊢ take (n✝ + 1) [] = []
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.drop_drop
Proof state before:
α : Type
n : ℕ
xs : List α
⊢ drop n (drop 0 xs) = drop (n + 0) xs
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.drop_drop
Proof state before:
α : Type
n✝ x✝ : ℕ
⊢ drop x✝ (drop (n✝ + 1) []) = drop (x✝ + (n✝ + 1)) []
Tactic:
simp [drop]
Proof state after:
no goals
Theorem: LoVe.drop_drop
Proof state before:
α : Type
m n : ℕ
head✝ : α
xs : List α
⊢ drop n (drop (m + 1) (head✝ :: xs)) = drop (n + (m + 1)) (head✝ :: xs)
Tactic:
simp [drop, drop_drop m n xs, ← add_assoc]
Proof state after:
no goals
Theorem: LoVe.take_take
Proof state before:
α : Type
x✝ : List α
⊢ take 0 (take 0 x✝) = take 0 x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.take_take
Proof state before:
α : Type
n✝ : ℕ
⊢ take (n✝ + 1) (take (n✝ + 1) []) = take (n✝ + 1) []
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.take_take
Proof state before:
α : Type
m : ℕ
x : α
xs : List α
⊢ take (m + 1) (take (m + 1) (x :: xs)) = take (m + 1) (x :: xs)
Tactic:
simp [take, take_take m xs]
Proof state after:
no goals
Theorem: LoVe.take_drop
Proof state before:
α : Type
x✝ : List α
⊢ take 0 x✝ ++ drop 0 x✝ = x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.take_drop
Proof state before:
α : Type
n✝ : ℕ
⊢ take (n✝ + 1) [] ++ drop (n✝ + 1) [] = []
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.take_drop
Proof state before:
α : Type
m : ℕ
x : α
xs : List α
⊢ take (m + 1) (x :: xs) ++ drop (m + 1) (x :: xs) = x :: xs
Tactic:
simp [take, drop, take_drop m]
Proof state after:
no goals
Theorem: Container.M.construct_destruct
Proof state before:
C : Container
x : M C
⊢ construct (destruct x) = x
Tactic:
let R (x y: M C) := x = construct (destruct y)
Proof state after:
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ construct (destruct x) = x
Theorem: Container.M.construct_destruct
Proof state before:
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ construct (destruct x) = x
Tactic:
apply bisim R
Proof state after:
case h₀
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)

case a
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x
Theorem: Container.M.construct_destruct
Proof state before:
case h₀
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)

case a
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x
Tactic:
. intro x y h₀
  have h₀ := congrArg destruct h₀
  cases h₁:destruct y
  case mk node k₂ =>
    rw [h₁] at h₀
    simp only [construct, destruct_corec, Map] at h₀
    simp only [construct.automaton, Map] at h₀
    exists node
    exists construct ∘ destruct ∘ k₂
    exists k₂
    constructor
    . exact h₀
    . constructor
      . rfl
      . intro i
        rfl
Proof state after:
case a
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x
Theorem: Container.M.construct_destruct
Proof state before:
case a
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x
Tactic:
. rfl
Proof state after:
no goals
Theorem: Container.M.construct_destruct
Proof state before:
case h₀
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
Tactic:
intro x y h₀
Proof state after:
case h₀
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀ : R x y
⊢ ∃ node k₁ k₂,
    destruct x = { fst := node, snd := k₁ } ∧
      destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)