HumanEval8

[shaazib-tanvir]

No description provided.

[datokrat]

Thanks for your help! :)

[datokrat]

If you want, you could also use grind, which saves you some of the annoying manual changes:

Suggested change

	case vc1.step pref x suff h' result hi =>
	obtain ⟨ hi₀, hi₁⟩ := hi
	constructor
	rw [hi₀, List.sum_append]
	change List.sum pref + x = List.sum pref + (x + 0)
	omega
	rw [hi₁, List.product_append]
	change List.product pref * x = List.product pref * (x * 1)
	rw [Int.mul_one]
	case vc3.a.post.success result h' =>
	obtain ⟨ left, right ⟩ := h'
	rw [left, right]
	rfl
	case vc1.step pref x suff h' result hi =>
	rw [List.sum_append, List.product_append]
	grind [List.product]
	case vc3.a.post.success result h' =>
	grind [sumProduct]

[datokrat]

This is just a very minor remark, but in this repository we usually put the colon at the end of the line:

Suggested change

	theorem List.sum_append (xs : List Int) (ys : List Int)
	: sum (xs ++ ys) = sum xs + sum ys := by
	theorem List.sum_append (xs : List Int) (ys : List Int) :
	sum (xs ++ ys) = sum xs + sum ys := by

[datokrat]

Similarly:

Suggested change

	theorem List.product_append (xs : List Int) (ys : List Int)
	: product (xs ++ ys) = product xs * product ys := by
	theorem List.product_append (xs : List Int) (ys : List Int) :
	product (xs ++ ys) = product xs * product ys := by