internlm/Lean-Github huggingface dataset:
Theorem: LoVe.Sorted_3_5
Proof state before:
⊢ Sorted [3, 5]
Tactic:
apply Sorted.two_or_more
Proof state after:
case hle

⊢ 3 ≤ 5

case hsorted

⊢ Sorted [5]
Theorem: LoVe.Sorted_3_5
Proof state before:
case hle

⊢ 3 ≤ 5

case hsorted

⊢ Sorted [5]
Tactic:
{ simp }
Proof state after:
case hsorted

⊢ Sorted [5]
Theorem: LoVe.Sorted_3_5
Proof state before:
case hsorted

⊢ Sorted [5]
Tactic:
{ exact Sorted.single _ }
Proof state after:
no goals
Theorem: LoVe.Sorted_3_5
Proof state before:
case hle

⊢ 3 ≤ 5
Tactic:
simp
Proof state after:
no goals
Theorem: LoVe.Sorted_3_5
Proof state before:
case hsorted

⊢ Sorted [5]
Tactic:
exact Sorted.single _
Proof state after:
no goals
Theorem: LoVe.Sorted_3_5_raw
Proof state before:
⊢ 3 ≤ 5
Tactic:
simp
Proof state after:
no goals
Theorem: LoVe.sorted_7_9_9_11
Proof state before:
⊢ 7 ≤ 9
Tactic:
simp
Proof state after:
no goals
Theorem: LoVe.sorted_7_9_9_11
Proof state before:
⊢ 9 ≤ 9
Tactic:
simp
Proof state after:
no goals
Theorem: LoVe.sorted_7_9_9_11
Proof state before:
⊢ 9 ≤ 11
Tactic:
simp
Proof state after:
no goals
Theorem: LoVe.Not_Sorted_17_13
Proof state before:
⊢ ¬Sorted [17, 13]
Tactic:
intro h
Proof state after:
h : Sorted [17, 13]
⊢ False
Theorem: LoVe.Not_Sorted_17_13
Proof state before:
h : Sorted [17, 13]
⊢ False
Tactic:
cases h with
| two_or_more _ _ hlet hsorted => simp at hlet
Proof state after:
no goals
Theorem: LoVe.Not_Sorted_17_13
Proof state before:
case two_or_more
hlet : 17 ≤ 13
hsorted : Sorted [13]
⊢ False
Tactic:
simp at hlet
Proof state after:
no goals
Theorem: LoVe.Palindrome_reverse
Proof state before:
α : Type
xs : List α
hxs : Palindrome xs
⊢ Palindrome (reverse xs)
Tactic:
induction hxs with
| nil                  => exact Palindrome.nil
| single x             => exact Palindrome.single x
| sandwich x xs hxs ih =>
  { simp [reverse, reverse_append]
    exact Palindrome.sandwich _ _ ih }
Proof state after:
no goals
Theorem: LoVe.Palindrome_reverse
Proof state before:
case nil
α : Type
xs : List α
⊢ Palindrome (reverse [])
Tactic:
exact Palindrome.nil
Proof state after:
no goals
Theorem: LoVe.Palindrome_reverse
Proof state before:
case single
α : Type
xs : List α
x : α
⊢ Palindrome (reverse [x])
Tactic:
exact Palindrome.single x
Proof state after:
no goals
Theorem: LoVe.Palindrome_reverse
Proof state before:
case sandwich
α : Type
xs✝ : List α
x : α
xs : List α
hxs : Palindrome xs
ih : Palindrome (reverse xs)
⊢ Palindrome (reverse ([x] ++ xs ++ [x]))
Tactic:
simp [reverse, reverse_append]
Proof state after:
case sandwich
α : Type
xs✝ : List α
x : α
xs : List α
hxs : Palindrome xs
ih : Palindrome (reverse xs)
⊢ Palindrome (x :: (reverse xs ++ [x]))
Theorem: LoVe.Palindrome_reverse
Proof state before:
case sandwich
α : Type
xs✝ : List α
x : α
xs : List α
hxs : Palindrome xs
ih : Palindrome (reverse xs)
⊢ Palindrome (x :: (reverse xs ++ [x]))
Tactic:
exact Palindrome.sandwich _ _ ih
Proof state after:
no goals
Theorem: LoVe.IsFull_singleton
Proof state before:
α : Type
a : α
⊢ IsFull (BTree.node a BTree.empty BTree.empty)
Tactic:
apply IsFull.node
Proof state after:
case hl
α : Type
a : α
⊢ IsFull BTree.empty

case hr
α : Type
a : α
⊢ IsFull BTree.empty

case hiff
α : Type
a : α
⊢ BTree.empty = BTree.empty ↔ BTree.empty = BTree.empty
Theorem: LoVe.IsFull_singleton
Proof state before:
case hl
α : Type
a : α
⊢ IsFull BTree.empty

case hr
α : Type
a : α
⊢ IsFull BTree.empty

case hiff
α : Type
a : α
⊢ BTree.empty = BTree.empty ↔ BTree.empty = BTree.empty
Tactic:
{ exact IsFull.empty }
Proof state after:
case hr
α : Type
a : α
⊢ IsFull BTree.empty

case hiff
α : Type
a : α
⊢ BTree.empty = BTree.empty ↔ BTree.empty = BTree.empty
Theorem: LoVe.IsFull_singleton
Proof state before:
case hr
α : Type
a : α
⊢ IsFull BTree.empty

case hiff
α : Type
a : α
⊢ BTree.empty = BTree.empty ↔ BTree.empty = BTree.empty
Tactic:
{ exact IsFull.empty }
Proof state after:
case hiff
α : Type
a : α
⊢ BTree.empty = BTree.empty ↔ BTree.empty = BTree.empty
Theorem: LoVe.IsFull_singleton
Proof state before:
case hiff
α : Type
a : α
⊢ BTree.empty = BTree.empty ↔ BTree.empty = BTree.empty
Tactic:
{ rfl }
Proof state after:
no goals
Theorem: LoVe.IsFull_singleton
Proof state before:
case hl
α : Type
a : α
⊢ IsFull BTree.empty
Tactic:
exact IsFull.empty
Proof state after:
no goals
Theorem: LoVe.IsFull_singleton
Proof state before:
case hr
α : Type
a : α
⊢ IsFull BTree.empty
Tactic:
exact IsFull.empty
Proof state after:
no goals
Theorem: LoVe.IsFull_singleton
Proof state before:
case hiff
α : Type
a : α
⊢ BTree.empty = BTree.empty ↔ BTree.empty = BTree.empty
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.IsFull_mirror
Proof state before:
α : Type
t : BTree α
ht : IsFull t
⊢ IsFull (mirror t)
Tactic:
induction ht with
| empty                           => exact IsFull.empty
| node a l r hl hr hiff ih_l ih_r =>
  { rw [mirror]
    apply IsFull.node
    { exact ih_r }
    { exact ih_l }
    { simp [mirror_Eq_empty_Iff, *] } }
Proof state after:
no goals
Theorem: LoVe.IsFull_mirror
Proof state before:
case empty
α : Type
t : BTree α
⊢ IsFull (mirror BTree.empty)
Tactic:
exact IsFull.empty
Proof state after:
no goals
Theorem: LoVe.IsFull_mirror
Proof state before:
case node
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ IsFull (mirror (BTree.node a l r))
Tactic:
rw [mirror]
Proof state after:
case node
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ IsFull (BTree.node a (mirror r) (mirror l))
Theorem: LoVe.IsFull_mirror
Proof state before:
case node
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ IsFull (BTree.node a (mirror r) (mirror l))
Tactic:
apply IsFull.node
Proof state after:
case node.hl
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ IsFull (mirror r)

case node.hr
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ IsFull (mirror l)

case node.hiff
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty
Theorem: LoVe.IsFull_mirror
Proof state before:
case node.hl
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ IsFull (mirror r)

case node.hr
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ IsFull (mirror l)

case node.hiff
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty
Tactic:
{ exact ih_r }
Proof state after:
case node.hr
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ IsFull (mirror l)

case node.hiff
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty
Theorem: LoVe.IsFull_mirror
Proof state before:
case node.hr
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ IsFull (mirror l)

case node.hiff
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty
Tactic:
{ exact ih_l }
Proof state after:
case node.hiff
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty
Theorem: LoVe.IsFull_mirror
Proof state before:
case node.hiff
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty
Tactic:
{ simp [mirror_Eq_empty_Iff, *] }
Proof state after:
no goals
Theorem: LoVe.IsFull_mirror
Proof state before:
case node.hl
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ IsFull (mirror r)
Tactic:
exact ih_r
Proof state after:
no goals
Theorem: LoVe.IsFull_mirror
Proof state before:
case node.hr
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ IsFull (mirror l)
Tactic:
exact ih_l
Proof state after:
no goals
Theorem: LoVe.IsFull_mirror
Proof state before:
case node.hiff
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty
Tactic:
simp [mirror_Eq_empty_Iff, *]
Proof state after:
no goals
Theorem: LoVe.IsFull_mirror_struct_induct
Proof state before:
α : Type
t : BTree α
⊢ IsFull t → IsFull (mirror t)
Tactic:
induction t with
| empty                =>
  { intro ht
    exact ht }
| node a l r ih_l ih_r =>
  { intro ht
    cases ht with
    | node _ _ _ hl hr hiff =>
      { rw [mirror]
        apply IsFull.node
        { exact ih_r hr }
        { apply ih_l hl }
        { simp [mirror_Eq_empty_Iff, *] } } }
Proof state after:
no goals
Theorem: LoVe.IsFull_mirror_struct_induct
Proof state before:
case empty
α : Type
⊢ IsFull BTree.empty → IsFull (mirror BTree.empty)
Tactic:
intro ht
Proof state after:
case empty
α : Type
ht : IsFull BTree.empty
⊢ IsFull (mirror BTree.empty)
Theorem: LoVe.IsFull_mirror_struct_induct
Proof state before:
case empty
α : Type
ht : IsFull BTree.empty
⊢ IsFull (mirror BTree.empty)
Tactic:
exact ht
Proof state after:
no goals
Theorem: LoVe.IsFull_mirror_struct_induct
Proof state before:
case node
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
⊢ IsFull (BTree.node a l r) → IsFull (mirror (BTree.node a l r))
Tactic:
intro ht
Proof state after:
case node
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
ht : IsFull (BTree.node a l r)
⊢ IsFull (mirror (BTree.node a l r))
Theorem: LoVe.IsFull_mirror_struct_induct
Proof state before:
case node
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
ht : IsFull (BTree.node a l r)
⊢ IsFull (mirror (BTree.node a l r))
Tactic:
cases ht with
| node _ _ _ hl hr hiff =>
  { rw [mirror]
    apply IsFull.node
    { exact ih_r hr }
    { apply ih_l hl }
    { simp [mirror_Eq_empty_Iff, *] } }
Proof state after:
no goals
Theorem: LoVe.IsFull_mirror_struct_induct
Proof state before:
case node.node
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ IsFull (mirror (BTree.node a l r))
Tactic:
rw [mirror]
Proof state after:
case node.node
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ IsFull (BTree.node a (mirror r) (mirror l))
Theorem: LoVe.IsFull_mirror_struct_induct
Proof state before:
case node.node
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ IsFull (BTree.node a (mirror r) (mirror l))
Tactic:
apply IsFull.node
Proof state after:
case node.node.hl
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ IsFull (mirror r)

case node.node.hr
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ IsFull (mirror l)

case node.node.hiff
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty
Theorem: LoVe.IsFull_mirror_struct_induct
Proof state before:
case node.node.hl
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ IsFull (mirror r)

case node.node.hr
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ IsFull (mirror l)

case node.node.hiff
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty
Tactic:
{ exact ih_r hr }
Proof state after:
case node.node.hr
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ IsFull (mirror l)

case node.node.hiff
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty
Theorem: LoVe.IsFull_mirror_struct_induct
Proof state before:
case node.node.hr
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ IsFull (mirror l)

case node.node.hiff
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty
Tactic:
{ apply ih_l hl }
Proof state after:
case node.node.hiff
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty
Theorem: LoVe.IsFull_mirror_struct_induct
Proof state before:
case node.node.hiff
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty
Tactic:
{ simp [mirror_Eq_empty_Iff, *] }
Proof state after:
no goals
Theorem: LoVe.IsFull_mirror_struct_induct
Proof state before:
case node.node.hl
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ IsFull (mirror r)
Tactic:
exact ih_r hr
Proof state after:
no goals
Theorem: LoVe.IsFull_mirror_struct_induct
Proof state before:
case node.node.hr
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ IsFull (mirror l)
Tactic:
apply ih_l hl
Proof state after:
no goals
Theorem: LoVe.IsFull_mirror_struct_induct
Proof state before:
case node.node.hiff
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty
Tactic:
simp [mirror_Eq_empty_Iff, *]
Proof state after:
no goals
Theorem: LoVe.neq_fin4_of_neq
Proof state before:
a b : ℕ
ha : a < 4
hb : b < 4
⊢ a ≠ b → { val := a, isLt := ha } ≠ { val := b, isLt := hb }
Tactic:
intro _ h
Proof state after:
a b : ℕ
ha : a < 4
hb : b < 4
a✝ : a ≠ b
h : { val := a, isLt := ha } = { val := b, isLt := hb }
⊢ False
Theorem: LoVe.neq_fin4_of_neq
Proof state before:
a b : ℕ
ha : a < 4
hb : b < 4
a✝ : a ≠ b
h : { val := a, isLt := ha } = { val := b, isLt := hb }
⊢ False
Tactic:
cases h
Proof state after:
case refl
a : ℕ
ha hb : a < 4
a✝ : a ≠ a
⊢ False
Theorem: LoVe.neq_fin4_of_neq
Proof state before:
case refl
a : ℕ
ha hb : a < 4
a✝ : a ≠ a
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LoVe.exist_distinct_fin4_of_neq
Proof state before:
isLt✝¹ : 0 < 4
isLt✝ : 1 < 4
x✝ : { val := 0, isLt := isLt✝¹ } ≠ { val := 1, isLt := isLt✝ }
⊢ { val := 0, isLt := isLt✝¹ } ≠ 2 ∧
    2 ≠ { val := 1, isLt := isLt✝ } ∧ { val := 0, isLt := isLt✝¹ } ≠ 3 ∧ 3 ≠ { val := 1, isLt := isLt✝ } ∧ 2 ≠ 3
Tactic:
fin_neq
Proof state after:
no goals
Theorem: LoVe.exist_distinct_fin4_of_neq
Proof state before:
isLt✝¹ : 0 < 4
isLt✝ : 2 < 4
x✝ : { val := 0, isLt := isLt✝¹ } ≠ { val := 2, isLt := isLt✝ }
⊢ { val := 0, isLt := isLt✝¹ } ≠ 1 ∧
    1 ≠ { val := 2, isLt := isLt✝ } ∧ { val := 0, isLt := isLt✝¹ } ≠ 3 ∧ 3 ≠ { val := 2, isLt := isLt✝ } ∧ 1 ≠ 3
Tactic:
fin_neq
Proof state after:
no goals
Theorem: LoVe.exist_distinct_fin4_of_neq
Proof state before:
isLt✝¹ : 0 < 4
isLt✝ : 3 < 4
x✝ : { val := 0, isLt := isLt✝¹ } ≠ { val := 3, isLt := isLt✝ }
⊢ { val := 0, isLt := isLt✝¹ } ≠ 1 ∧
    1 ≠ { val := 3, isLt := isLt✝ } ∧ { val := 0, isLt := isLt✝¹ } ≠ 2 ∧ 2 ≠ { val := 3, isLt := isLt✝ } ∧ 1 ≠ 2
Tactic:
fin_neq
Proof state after:
no goals
Theorem: LoVe.exist_distinct_fin4_of_neq
Proof state before:
isLt✝¹ : 1 < 4
isLt✝ : 0 < 4
x✝ : { val := 1, isLt := isLt✝¹ } ≠ { val := 0, isLt := isLt✝ }
⊢ { val := 1, isLt := isLt✝¹ } ≠ 2 ∧
    2 ≠ { val := 0, isLt := isLt✝ } ∧ { val := 1, isLt := isLt✝¹ } ≠ 3 ∧ 3 ≠ { val := 0, isLt := isLt✝ } ∧ 2 ≠ 3
Tactic:
fin_neq
Proof state after:
no goals
Theorem: LoVe.exist_distinct_fin4_of_neq
Proof state before:
isLt✝¹ : 1 < 4
isLt✝ : 2 < 4
x✝ : { val := 1, isLt := isLt✝¹ } ≠ { val := 2, isLt := isLt✝ }
⊢ { val := 1, isLt := isLt✝¹ } ≠ 0 ∧
    0 ≠ { val := 2, isLt := isLt✝ } ∧ { val := 1, isLt := isLt✝¹ } ≠ 3 ∧ 3 ≠ { val := 2, isLt := isLt✝ } ∧ 0 ≠ 3
Tactic:
fin_neq
Proof state after:
no goals
Theorem: LoVe.exist_distinct_fin4_of_neq
Proof state before:
isLt✝¹ : 1 < 4
isLt✝ : 3 < 4
x✝ : { val := 1, isLt := isLt✝¹ } ≠ { val := 3, isLt := isLt✝ }
⊢ { val := 1, isLt := isLt✝¹ } ≠ 0 ∧
    0 ≠ { val := 3, isLt := isLt✝ } ∧ { val := 1, isLt := isLt✝¹ } ≠ 2 ∧ 2 ≠ { val := 3, isLt := isLt✝ } ∧ 0 ≠ 2
Tactic:
fin_neq
Proof state after:
no goals
Theorem: LoVe.exist_distinct_fin4_of_neq
Proof state before:
isLt✝¹ : 2 < 4
isLt✝ : 0 < 4
x✝ : { val := 2, isLt := isLt✝¹ } ≠ { val := 0, isLt := isLt✝ }
⊢ { val := 2, isLt := isLt✝¹ } ≠ 1 ∧
    1 ≠ { val := 0, isLt := isLt✝ } ∧ { val := 2, isLt := isLt✝¹ } ≠ 3 ∧ 3 ≠ { val := 0, isLt := isLt✝ } ∧ 1 ≠ 3
Tactic:
fin_neq
Proof state after:
no goals
Theorem: LoVe.exist_distinct_fin4_of_neq
Proof state before:
isLt✝¹ : 2 < 4
isLt✝ : 1 < 4
x✝ : { val := 2, isLt := isLt✝¹ } ≠ { val := 1, isLt := isLt✝ }
⊢ { val := 2, isLt := isLt✝¹ } ≠ 0 ∧
    0 ≠ { val := 1, isLt := isLt✝ } ∧ { val := 2, isLt := isLt✝¹ } ≠ 3 ∧ 3 ≠ { val := 1, isLt := isLt✝ } ∧ 0 ≠ 3
Tactic:
fin_neq
Proof state after:
no goals
Theorem: LoVe.exist_distinct_fin4_of_neq
Proof state before:
isLt✝¹ : 2 < 4
isLt✝ : 3 < 4
x✝ : { val := 2, isLt := isLt✝¹ } ≠ { val := 3, isLt := isLt✝ }
⊢ { val := 2, isLt := isLt✝¹ } ≠ 0 ∧
    0 ≠ { val := 3, isLt := isLt✝ } ∧ { val := 2, isLt := isLt✝¹ } ≠ 1 ∧ 1 ≠ { val := 3, isLt := isLt✝ } ∧ 0 ≠ 1
Tactic:
fin_neq
Proof state after:
no goals
Theorem: LoVe.exist_distinct_fin4_of_neq
Proof state before:
isLt✝¹ : 3 < 4
isLt✝ : 0 < 4
x✝ : { val := 3, isLt := isLt✝¹ } ≠ { val := 0, isLt := isLt✝ }
⊢ { val := 3, isLt := isLt✝¹ } ≠ 1 ∧
    1 ≠ { val := 0, isLt := isLt✝ } ∧ { val := 3, isLt := isLt✝¹ } ≠ 2 ∧ 2 ≠ { val := 0, isLt := isLt✝ } ∧ 1 ≠ 2
Tactic:
fin_neq
Proof state after:
no goals
Theorem: LoVe.exist_distinct_fin4_of_neq
Proof state before:
isLt✝¹ : 3 < 4
isLt✝ : 1 < 4
x✝ : { val := 3, isLt := isLt✝¹ } ≠ { val := 1, isLt := isLt✝ }
⊢ { val := 3, isLt := isLt✝¹ } ≠ 0 ∧
    0 ≠ { val := 1, isLt := isLt✝ } ∧ { val := 3, isLt := isLt✝¹ } ≠ 2 ∧ 2 ≠ { val := 1, isLt := isLt✝ } ∧ 0 ≠ 2
Tactic:
fin_neq
Proof state after:
no goals
Theorem: LoVe.exist_distinct_fin4_of_neq
Proof state before:
isLt✝¹ : 3 < 4
isLt✝ : 2 < 4
x✝ : { val := 3, isLt := isLt✝¹ } ≠ { val := 2, isLt := isLt✝ }
⊢ { val := 3, isLt := isLt✝¹ } ≠ 0 ∧
    0 ≠ { val := 2, isLt := isLt✝ } ∧ { val := 3, isLt := isLt✝¹ } ≠ 1 ∧ 1 ≠ { val := 2, isLt := isLt✝ } ∧ 0 ≠ 1
Tactic:
fin_neq
Proof state after:
no goals
Theorem: LoVe.sillyLoop_from_1_BigStep
Proof state before:
⊢ (sillyLoop, State.update "x" 1 fun x => 0) ⟹ fun x => 0
Tactic:
rw [sillyLoop]
Proof state after:
⊢ (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      State.update "x" 1 fun x => 0) ⟹
    fun x => 0
Theorem: LoVe.sillyLoop_from_1_BigStep
Proof state before:
⊢ (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      State.update "x" 1 fun x => 0) ⟹
    fun x => 0
Tactic:
apply BigStep.while_true
Proof state after:
case hcond

⊢ State.update "x" 1 (fun x => 0) "x" > State.update "x" 1 (fun x => 0) "y"

case hbody

⊢ (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⟹ ?t

case hrest

⊢ (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1), ?t) ⟹ fun x => 0

case t

⊢ State
Theorem: LoVe.sillyLoop_from_1_BigStep
Proof state before:
case hcond

⊢ State.update "x" 1 (fun x => 0) "x" > State.update "x" 1 (fun x => 0) "y"

case hbody

⊢ (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⟹ ?t

case hrest

⊢ (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1), ?t) ⟹ fun x => 0

case t

⊢ State
Tactic:
{ simp }
Proof state after:
case hbody

⊢ (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⟹ ?t

case hrest

⊢ (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1), ?t) ⟹ fun x => 0

case t

⊢ State
Theorem: LoVe.sillyLoop_from_1_BigStep
Proof state before:
case hbody

⊢ (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⟹ ?t

case hrest

⊢ (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1), ?t) ⟹ fun x => 0

case t

⊢ State
Tactic:
{ apply BigStep.seq
  { apply BigStep.skip }
  { apply BigStep.assign } }
Proof state after:
case hrest

⊢ (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0)) ⟹
    fun x => 0
Theorem: LoVe.sillyLoop_from_1_BigStep
Proof state before:
case hrest

⊢ (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0)) ⟹
    fun x => 0
Tactic:
{ simp
  apply BigStep.while_false
  simp }
Proof state after:
no goals
Theorem: LoVe.sillyLoop_from_1_BigStep
Proof state before:
case hcond

⊢ State.update "x" 1 (fun x => 0) "x" > State.update "x" 1 (fun x => 0) "y"
Tactic:
simp
Proof state after:
no goals
Theorem: LoVe.sillyLoop_from_1_BigStep
Proof state before:
case hbody

⊢ (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⟹ ?t
Tactic:
apply BigStep.seq
Proof state after:
case hbody.hS

⊢ (Stmt.skip, State.update "x" 1 fun x => 0) ⟹ ?hbody.t

case hbody.hT

⊢ (Stmt.assign "x" fun s => s "x" - 1, ?hbody.t) ⟹ ?t

case hbody.t

⊢ State