internlm/Lean-Github huggingface dataset:
Theorem: Etch.Verification.Stream.mul_spec
Proof state before:
case h.e'_2.h.e'_6.h.e'_4.h.a
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (mul a b).σ
ih : ∀ (y : (mul a b).σ), WfRel (mul a b) y q → eval (mul a b) y = eval a y.1 * eval b y.2
hv : (mul a b).valid q = true
x✝ : ι
⊢ toOrder (mul a b) { val := q, property := hv } ≤ (x✝, false) ↔
    ¬(x✝, false) < toOrder (mul a b) { val := q, property := hv }
Tactic:
simp
Proof state after:
no goals
Theorem: Etch.Verification.Stream.mul_seek_spec
Proof state before:
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
i : Lex (ι × Bool)
j : ι
h : i ≤ (j, false)
⊢ (eval (mul a b) ((mul a b).seek q i)) j = (eval (mul a b) ↑q) j
Tactic:
simp only [Finsupp.mul_apply, mul_spec]
Proof state after:
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
i : Lex (ι × Bool)
j : ι
h : i ≤ (j, false)
⊢ (eval a ((mul a b).seek q i).1) j * (eval b ((mul a b).seek q i).2) j = (eval a (↑q).1) j * (eval b (↑q).2) j
Theorem: Etch.Verification.Stream.mul_seek_spec
Proof state before:
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
i : Lex (ι × Bool)
j : ι
h : i ≤ (j, false)
⊢ (eval a ((mul a b).seek q i).1) j * (eval b ((mul a b).seek q i).2) j = (eval a (↑q).1) j * (eval b (↑q).2) j
Tactic:
congr 1 <;> dsimp <;> rw [IsLawful.seek_spec] <;> aesop
Proof state after:
ι : Type
inst : LinearOrder ι
α : Type u
inst_1 : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst_2 : IsStrictLawful a
inst_3 : IsStrictLawful b
i : Lex (ι × Bool)
j : ι
h : i ≤ (j, false)
val : (mul a b).σ
property : (mul a b).valid val = true
⊢ (eval a (a.seek (mul.valid.fst { val := val, property := property }) i)) j = (eval a val.1) j

ι : Type
inst : LinearOrder ι
α : Type u
inst_1 : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst_2 : IsStrictLawful a
inst_3 : IsStrictLawful b
i : Lex (ι × Bool)
j : ι
h : i ≤ (j, false)
val : (mul a b).σ
property : (mul a b).valid val = true
⊢ (eval b (b.seek (mul.valid.snd { val := val, property := property }) i)) j = (eval b val.2) j
Theorem: Std.RBNode.min?_mem
Proof state before:
α : Type u_1
a : α
t : RBNode α
h : RBNode.min? t = some a
⊢ a ∈ t
Tactic:
rw [min?_eq_toList_head?] at h
Proof state after:
α : Type u_1
a : α
t : RBNode α
h : List.head? (toList t) = some a
⊢ a ∈ t
Theorem: Std.RBNode.min?_mem
Proof state before:
α : Type u_1
a : α
t : RBNode α
h : List.head? (toList t) = some a
⊢ a ∈ t
Tactic:
rw [← mem_toList]
Proof state after:
α : Type u_1
a : α
t : RBNode α
h : List.head? (toList t) = some a
⊢ a ∈ toList t
Theorem: Std.RBNode.min?_mem
Proof state before:
α : Type u_1
a : α
t : RBNode α
h : List.head? (toList t) = some a
⊢ a ∈ toList t
Tactic:
revert h
Proof state after:
α : Type u_1
a : α
t : RBNode α
⊢ List.head? (toList t) = some a → a ∈ toList t
Theorem: Std.RBNode.min?_mem
Proof state before:
α : Type u_1
a : α
t : RBNode α
⊢ List.head? (toList t) = some a → a ∈ toList t
Tactic:
cases toList t <;> rintro ⟨⟩
Proof state after:
case cons.refl
α : Type u_1
a : α
t : RBNode α
tail✝ : List α
⊢ a ∈ a :: tail✝
Theorem: Std.RBNode.min?_mem
Proof state before:
case cons.refl
α : Type u_1
a : α
t : RBNode α
tail✝ : List α
⊢ a ∈ a :: tail✝
Tactic:
constructor
Proof state after:
no goals
Theorem: Std.RBNode.Ordered.min?_le
Proof state before:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
h : RBNode.min? t = some a
x : α
hx : x ∈ t
⊢ cmp a x ≠ Ordering.gt
Tactic:
rw [min?_eq_toList_head?] at h
Proof state after:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
h : List.head? (toList t) = some a
x : α
hx : x ∈ t
⊢ cmp a x ≠ Ordering.gt
Theorem: Std.RBNode.Ordered.min?_le
Proof state before:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
h : List.head? (toList t) = some a
x : α
hx : x ∈ t
⊢ cmp a x ≠ Ordering.gt
Tactic:
rw [← mem_toList] at hx
Proof state after:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
h : List.head? (toList t) = some a
x : α
hx : x ∈ toList t
⊢ cmp a x ≠ Ordering.gt
Theorem: Std.RBNode.Ordered.min?_le
Proof state before:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
h : List.head? (toList t) = some a
x : α
hx : x ∈ toList t
⊢ cmp a x ≠ Ordering.gt
Tactic:
have := ht.toList_sorted
Proof state after:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
h : List.head? (toList t) = some a
x : α
hx : x ∈ toList t
this : List.Pairwise (cmpLT cmp) (toList t)
⊢ cmp a x ≠ Ordering.gt
Theorem: Std.RBNode.Ordered.min?_le
Proof state before:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
h : List.head? (toList t) = some a
x : α
hx : x ∈ toList t
this : List.Pairwise (cmpLT cmp) (toList t)
⊢ cmp a x ≠ Ordering.gt
Tactic:
revert h hx this
Proof state after:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
x : α
⊢ List.head? (toList t) = some a → x ∈ toList t → List.Pairwise (cmpLT cmp) (toList t) → cmp a x ≠ Ordering.gt
Theorem: Std.RBNode.Ordered.min?_le
Proof state before:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
x : α
⊢ List.head? (toList t) = some a → x ∈ toList t → List.Pairwise (cmpLT cmp) (toList t) → cmp a x ≠ Ordering.gt
Tactic:
cases toList t <;> rintro ⟨⟩ (_ | ⟨_, hx⟩) (_ | ⟨h1,h2⟩)
Proof state after:
case cons.refl.head.cons
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
tail✝ : List α
h2 : List.Pairwise (cmpLT cmp) tail✝
h1 : ∀ (a' : α), a' ∈ tail✝ → cmpLT cmp a a'
⊢ cmp a a ≠ Ordering.gt

case cons.refl.tail.cons
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
x : α
tail✝ : List α
hx : List.Mem x tail✝
h2 : List.Pairwise (cmpLT cmp) tail✝
h1 : ∀ (a' : α), a' ∈ tail✝ → cmpLT cmp a a'
⊢ cmp a x ≠ Ordering.gt
Theorem: Std.RBNode.Ordered.min?_le
Proof state before:
case cons.refl.head.cons
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
tail✝ : List α
h2 : List.Pairwise (cmpLT cmp) tail✝
h1 : ∀ (a' : α), a' ∈ tail✝ → cmpLT cmp a a'
⊢ cmp a a ≠ Ordering.gt
Tactic:
rw [OrientedCmp.cmp_refl (cmp := cmp)]
Proof state after:
case cons.refl.head.cons
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
tail✝ : List α
h2 : List.Pairwise (cmpLT cmp) tail✝
h1 : ∀ (a' : α), a' ∈ tail✝ → cmpLT cmp a a'
⊢ Ordering.eq ≠ Ordering.gt
Theorem: Std.RBNode.Ordered.min?_le
Proof state before:
case cons.refl.head.cons
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
tail✝ : List α
h2 : List.Pairwise (cmpLT cmp) tail✝
h1 : ∀ (a' : α), a' ∈ tail✝ → cmpLT cmp a a'
⊢ Ordering.eq ≠ Ordering.gt
Tactic:
decide
Proof state after:
no goals
Theorem: Std.RBNode.Ordered.min?_le
Proof state before:
case cons.refl.tail.cons
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
x : α
tail✝ : List α
hx : List.Mem x tail✝
h2 : List.Pairwise (cmpLT cmp) tail✝
h1 : ∀ (a' : α), a' ∈ tail✝ → cmpLT cmp a a'
⊢ cmp a x ≠ Ordering.gt
Tactic:
rw [(h1 _ hx).1]
Proof state after:
case cons.refl.tail.cons
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
x : α
tail✝ : List α
hx : List.Mem x tail✝
h2 : List.Pairwise (cmpLT cmp) tail✝
h1 : ∀ (a' : α), a' ∈ tail✝ → cmpLT cmp a a'
⊢ Ordering.lt ≠ Ordering.gt
Theorem: Std.RBNode.Ordered.min?_le
Proof state before:
case cons.refl.tail.cons
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
x : α
tail✝ : List α
hx : List.Mem x tail✝
h2 : List.Pairwise (cmpLT cmp) tail✝
h1 : ∀ (a' : α), a' ∈ tail✝ → cmpLT cmp a a'
⊢ Ordering.lt ≠ Ordering.gt
Tactic:
decide
Proof state after:
no goals
Theorem: Std.RBNode.max?_mem
Proof state before:
α : Type u_1
a : α
t : RBNode α
h : RBNode.max? t = some a
⊢ a ∈ t
Tactic:
simpa using min?_mem ((min?_reverse _).trans h)
Proof state after:
no goals
Theorem: Std.RBNode.Ordered.le_max?
Proof state before:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
h : RBNode.max? t = some a
x : α
hx : x ∈ t
⊢ x ∈ reverse t
Tactic:
simpa using hx
Proof state after:
no goals
Theorem: Std.RBSet.isEmpty_iff_toList_eq_nil
Proof state before:
α : Type u_1
cmp : α → α → Ordering
t : RBSet α cmp
⊢ isEmpty t = true ↔ toList t = []
Tactic:
obtain ⟨⟨⟩, _⟩ := t <;> simp [toList, isEmpty]
Proof state after:
no goals
Theorem: Std.RBSet.findP?_some
Proof state before:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
⊢ y ∈ t.val ∧ cut y = Ordering.eq ↔ y ∈ toList t ∧ cut y = Ordering.eq
Tactic:
simp [mem_toList]
Proof state after:
no goals
Theorem: Std.RBSet.findP?_insert_of_ne
Proof state before:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h : cut v ≠ Ordering.eq
⊢ findP? (insert t v) cut = findP? t cut
Tactic:
refine Option.ext fun u =>
  findP?_some.trans <| .trans (and_congr_left fun h' => ?_) findP?_some.symm
Proof state after:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h : cut v ≠ Ordering.eq
u : α
h' : cut u = Ordering.eq
⊢ u ∈ toList (insert t v) ↔ u ∈ toList t
Theorem: Std.RBSet.findP?_insert_of_ne
Proof state before:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h : cut v ≠ Ordering.eq
u : α
h' : cut u = Ordering.eq
⊢ u ∈ toList (insert t v) ↔ u ∈ toList t
Tactic:
rw [mem_toList_insert, or_iff_left, and_iff_left]
Proof state after:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h : cut v ≠ Ordering.eq
u : α
h' : cut u = Ordering.eq
⊢ find? t v ≠ some u

α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h : cut v ≠ Ordering.eq
u : α
h' : cut u = Ordering.eq
⊢ ¬u = v
Theorem: Std.RBSet.findP?_insert_of_ne
Proof state before:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h : cut v ≠ Ordering.eq
u : α
h' : cut u = Ordering.eq
⊢ find? t v ≠ some u
Tactic:
exact mt (fun h => by rwa [IsCut.congr (cut := cut) (find?_some_eq_eq h)]) h
Proof state after:
no goals
Theorem: Std.RBSet.findP?_insert_of_ne
Proof state before:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h✝ : cut v ≠ Ordering.eq
u : α
h' : cut u = Ordering.eq
h : find? t v = some u
⊢ cut v = Ordering.eq
Tactic:
rwa [IsCut.congr (cut := cut) (find?_some_eq_eq h)]
Proof state after:
no goals
Theorem: Std.RBSet.findP?_insert_of_ne
Proof state before:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h : cut v ≠ Ordering.eq
u : α
h' : cut u = Ordering.eq
⊢ ¬u = v
Tactic:
rintro rfl
Proof state after:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
u : α
h' : cut u = Ordering.eq
h : cut u ≠ Ordering.eq
⊢ False
Theorem: Std.RBSet.findP?_insert_of_ne
Proof state before:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
u : α
h' : cut u = Ordering.eq
h : cut u ≠ Ordering.eq
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Std.RBSet.findP?_insert
Proof state before:
α : Type u_1
cmp : α → α → Ordering
inst✝¹ : TransCmp cmp
t : RBSet α cmp
v : α
cut : α → Ordering
inst✝ : IsStrictCut cmp cut
⊢ findP? (insert t v) cut = if cut v = Ordering.eq then some v else findP? t cut
Tactic:
split <;> [exact findP?_insert_of_eq t ‹_›; exact findP?_insert_of_ne t ‹_›]
Proof state after:
no goals
Theorem: Std.RBSet.isEmpty_iff_eq_empty
Proof state before:
α : Type u_1
cmp : α → α → Ordering
t : RBSet α cmp
⊢ isEmpty t = true ↔ t = ∅
Tactic:
obtain ⟨⟨⟩, _⟩ := t <;>
simp [isEmpty]
Proof state after:
case mk.nil
α : Type u_1
cmp : α → α → Ordering
property✝ : RBNode.WF cmp RBNode.nil
⊢ { val := RBNode.nil, property := property✝ } = ∅

case mk.node
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
property✝ : RBNode.WF cmp (RBNode.node c✝ l✝ v✝ r✝)
⊢ ¬{ val := RBNode.node c✝ l✝ v✝ r✝, property := property✝ } = ∅
Theorem: Std.RBSet.isEmpty_iff_eq_empty
Proof state before:
case mk.nil
α : Type u_1
cmp : α → α → Ordering
property✝ : RBNode.WF cmp RBNode.nil
⊢ { val := RBNode.nil, property := property✝ } = ∅
Tactic:
rfl
Proof state after:
no goals
Theorem: Std.RBSet.isEmpty_iff_eq_empty
Proof state before:
case mk.node
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
property✝ : RBNode.WF cmp (RBNode.node c✝ l✝ v✝ r✝)
⊢ ¬{ val := RBNode.node c✝ l✝ v✝ r✝, property := property✝ } = ∅
Tactic:
change _ ≠ Subtype.mk _ _
Proof state after:
case mk.node
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
property✝ : RBNode.WF cmp (RBNode.node c✝ l✝ v✝ r✝)
⊢ { val := RBNode.node c✝ l✝ v✝ r✝, property := property✝ } ≠ { val := RBNode.nil, property := ⋯ }
Theorem: Std.RBSet.isEmpty_iff_eq_empty
Proof state before:
case mk.node
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
property✝ : RBNode.WF cmp (RBNode.node c✝ l✝ v✝ r✝)
⊢ { val := RBNode.node c✝ l✝ v✝ r✝, property := property✝ } ≠ { val := RBNode.nil, property := ⋯ }
Tactic:
simp
Proof state after:
no goals
Theorem: Std.RBMap.find?_some_mem_toList
Proof state before:
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
x : α
v : β
t : RBMap α β cmp
h : find? t x = some v
⊢ ∃ y, (y, v) ∈ toList t ∧ cmp x y = Ordering.eq
Tactic:
obtain ⟨⟨y, v⟩, h', rfl⟩ := Option.map_eq_some'.1 h
Proof state after:
case intro.mk.intro
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
x : α
t : RBMap α β cmp
y : α
v : β
h' : findEntry? t x = some (y, v)
h : find? t x = some (y, v).snd
⊢ ∃ y_1, (y_1, (y, v).snd) ∈ toList t ∧ cmp x y_1 = Ordering.eq
Theorem: Std.RBMap.find?_some_mem_toList
Proof state before:
case intro.mk.intro
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
x : α
t : RBMap α β cmp
y : α
v : β
h' : findEntry? t x = some (y, v)
h : find? t x = some (y, v).snd
⊢ ∃ y_1, (y_1, (y, v).snd) ∈ toList t ∧ cmp x y_1 = Ordering.eq
Tactic:
exact ⟨_, findEntry?_some_mem_toList h', findEntry?_some_eq_eq h'⟩
Proof state after:
no goals
Theorem: Std.RBMap.find?_some
Proof state before:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ find? t x = some v ↔ ∃ y, (y, v) ∈ toList t ∧ cmp x y = Ordering.eq
Tactic:
simp [find?, findEntry?_some]
Proof state after:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ (∃ a, (a ∈ toList t ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v) ↔ ∃ y, (y, v) ∈ toList t ∧ cmp x y = Ordering.eq
Theorem: Std.RBMap.find?_some
Proof state before:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ (∃ a, (a ∈ toList t ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v) ↔ ∃ y, (y, v) ∈ toList t ∧ cmp x y = Ordering.eq
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ (∃ a, (a ∈ toList t ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v) → ∃ y, (y, v) ∈ toList t ∧ cmp x y = Ordering.eq

case mpr
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ (∃ y, (y, v) ∈ toList t ∧ cmp x y = Ordering.eq) → ∃ a, (a ∈ toList t ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v
Theorem: Std.RBMap.find?_some
Proof state before:
case mp
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ (∃ a, (a ∈ toList t ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v) → ∃ y, (y, v) ∈ toList t ∧ cmp x y = Ordering.eq
Tactic:
rintro ⟨_, h, rfl⟩
Proof state after:
case mp.intro.intro
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
inst✝ : TransCmp cmp
t : RBMap α β cmp
w✝ : α × β
h : w✝ ∈ toList t ∧ cmp x w✝.fst = Ordering.eq
⊢ ∃ y, (y, w✝.snd) ∈ toList t ∧ cmp x y = Ordering.eq
Theorem: Std.RBMap.find?_some
Proof state before:
case mp.intro.intro
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
inst✝ : TransCmp cmp
t : RBMap α β cmp
w✝ : α × β
h : w✝ ∈ toList t ∧ cmp x w✝.fst = Ordering.eq
⊢ ∃ y, (y, w✝.snd) ∈ toList t ∧ cmp x y = Ordering.eq
Tactic:
exact ⟨_, h⟩
Proof state after:
no goals
Theorem: Std.RBMap.find?_some
Proof state before:
case mpr
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ (∃ y, (y, v) ∈ toList t ∧ cmp x y = Ordering.eq) → ∃ a, (a ∈ toList t ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v
Tactic:
rintro ⟨b, h⟩
Proof state after:
case mpr.intro
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
b : α
h : (b, v) ∈ toList t ∧ cmp x b = Ordering.eq
⊢ ∃ a, (a ∈ toList t ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v
Theorem: Std.RBMap.find?_some
Proof state before:
case mpr.intro
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
b : α
h : (b, v) ∈ toList t ∧ cmp x b = Ordering.eq
⊢ ∃ a, (a ∈ toList t ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v
Tactic:
exact ⟨_, h, rfl⟩
Proof state after:
no goals
Theorem: Std.RBMap.contains_iff_find?
Proof state before:
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
x : α
t : RBMap α β cmp
⊢ contains t x = true ↔ ∃ v, find? t x = some v
Tactic:
simp [contains_iff_findEntry?, find?, and_comm, exists_comm]
Proof state after:
no goals
Theorem: Std.RBMap.findEntry?_congr
Proof state before:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
k₁ k₂ : α
inst✝ : TransCmp cmp
t : RBMap α β cmp
h : cmp k₁ k₂ = Ordering.eq
⊢ findEntry? t k₁ = findEntry? t k₂
Tactic:
simp [findEntry?, TransCmp.cmp_congr_left' h]
Proof state after:
no goals
Theorem: Std.RBMap.find?_congr
Proof state before:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
k₁ k₂ : α
inst✝ : TransCmp cmp
t : RBMap α β cmp
h : cmp k₁ k₂ = Ordering.eq
⊢ find? t k₁ = find? t k₂
Tactic:
simp [find?, findEntry?_congr _ h]
Proof state after:
no goals
Theorem: Std.RBMap.find?_insert_of_eq
Proof state before:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
k' k : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
h : cmp k' k = Ordering.eq
⊢ find? (insert t k v) k' = some v
Tactic:
rw [find?, findEntry?_insert_of_eq _ h]
Proof state after:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
k' k : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
h : cmp k' k = Ordering.eq
⊢ Option.map (fun x => x.snd) (some (k, v)) = some v
Theorem: Std.RBMap.find?_insert_of_eq
Proof state before:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
k' k : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
h : cmp k' k = Ordering.eq
⊢ Option.map (fun x => x.snd) (some (k, v)) = some v
Tactic:
rfl
Proof state after:
no goals
Theorem: Std.RBMap.find?_insert_of_ne
Proof state before:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
k' k : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
h : cmp k' k ≠ Ordering.eq
⊢ find? (insert t k v) k' = find? t k'
Tactic:
simp [find?, findEntry?_insert_of_ne _ h]
Proof state after:
no goals
Theorem: Std.RBMap.find?_insert
Proof state before:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
inst✝ : TransCmp cmp
t : RBMap α β cmp
k : α
v : β
k' : α
⊢ find? (insert t k v) k' = if cmp k' k = Ordering.eq then some v else find? t k'
Tactic:
split <;> [exact find?_insert_of_eq t ‹_›; exact find?_insert_of_ne t ‹_›]
Proof state after:
no goals
Theorem: Std.RBMap.find?_insert_self
Proof state before:
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
k : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ find? (insert t k v) k = some v
Tactic:
rw [find?_insert_of_eq]
Proof state after:
case h
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
k : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ cmp k k = Ordering.eq
Theorem: Std.RBMap.find?_insert_self
Proof state before:
case h
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
k : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ cmp k k = Ordering.eq
Tactic:
rw [OrientedCmp.cmp_refl (cmp := cmp)]
Proof state after:
no goals
Theorem: Std.RBMap.findD_insert
Proof state before:
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
inst✝ : TransCmp cmp
t : RBMap α β cmp
k : α
v : β
k' : α
d : β
⊢ findD (insert t k v) k' d = if cmp k' k = Ordering.eq then v else findD t k' d
Tactic:
simp only [findD, find?_insert]
Proof state after:
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
inst✝ : TransCmp cmp
t : RBMap α β cmp
k : α
v : β
k' : α
d : β
⊢ Option.getD (if cmp k' k = Ordering.eq then some v else find? t k') d =
    if cmp k' k = Ordering.eq then v else Option.getD (find? t k') d
Theorem: Std.RBMap.findD_insert
Proof state before:
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
inst✝ : TransCmp cmp
t : RBMap α β cmp
k : α
v : β
k' : α
d : β
⊢ Option.getD (if cmp k' k = Ordering.eq then some v else find? t k') d =
    if cmp k' k = Ordering.eq then v else Option.getD (find? t k') d
Tactic:
split <;> rfl
Proof state after:
no goals
Theorem: Std.RBMap.findD_insert_self
Proof state before:
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
k : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
d : β
⊢ findD (insert t k v) k d = v
Tactic:
simp [findD]
Proof state after:
no goals
Theorem: Std.RBMap.findD_insert_of_ne
Proof state before:
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
k' k : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
h : cmp k' k ≠ Ordering.eq
d : β
⊢ findD (insert t k v) k' d = findD t k' d
Tactic:
simp [findD_insert, h]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.eval₀_map
Proof state before:
ι : Type
α : Type u_2
a b s : Stream ι α
β : Type u_1
q : { q // s.valid q = true }
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
hf : f 0 = 0
⊢ eval₀ (map f s) q = Finsupp.mapRange f hf (eval₀ s q)
Tactic:
dsimp [Stream.eval₀]
Proof state after:
ι : Type
α : Type u_2
a b s : Stream ι α
β : Type u_1
q : { q // s.valid q = true }
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
hf : f 0 = 0
⊢ (if h₂ : s.ready q = true then fun₀ | s.index q => f (s.value { val := q, property := h₂ }) else 0) =
    Finsupp.mapRange f hf
      (if h₂ : s.ready q = true then fun₀ | s.index q => s.value { val := q, property := h₂ } else 0)
Theorem: Etch.Verification.Stream.eval₀_map
Proof state before:
ι : Type
α : Type u_2
a b s : Stream ι α
β : Type u_1
q : { q // s.valid q = true }
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
hf : f 0 = 0
⊢ (if h₂ : s.ready q = true then fun₀ | s.index q => f (s.value { val := q, property := h₂ }) else 0) =
    Finsupp.mapRange f hf
      (if h₂ : s.ready q = true then fun₀ | s.index q => s.value { val := q, property := h₂ } else 0)
Tactic:
split_ifs <;> simp
Proof state after:
no goals
Theorem: Etch.Verification.Stream.map_zero
Proof state before:
ι : Type
α : Type u_2
a b s : Stream ι α
β : Type u_1
f : α → β
⊢ map f 0 = 0
Tactic:
ext <;> try rfl
Proof state after:
case value
ι : Type
α : Type u_2
a b s : Stream ι α
β : Type u_1
f : α → β
⊢ HEq (map f 0).value 0.value
Theorem: Etch.Verification.Stream.map_zero
Proof state before:
case value
ι : Type
α : Type u_2
a b s : Stream ι α
β : Type u_1
f : α → β
⊢ HEq (map f 0).value 0.value
Tactic:
rw [heq_iff_eq]
Proof state after:
case value
ι : Type
α : Type u_2
a b s : Stream ι α
β : Type u_1
f : α → β
⊢ (map f 0).value = 0.value