4 ms·
Similar story in Isabelle/HOL - no special tactics required for this example: lemma fixes a :: "'a::comm_ring" shows "a + b + c + d = d + b + c + a"
by themulticaster 4y ago
Similar story in Isabelle/HOL - no special tactics required for this example:
lemma
fixes a :: "'a::comm_ring"
shows "a + b + c + d = d + b + c + a"
by fastforce
Just for fun, I wrote up an equivalent but completely manual proof where every proof step consist of just one application of an existing fact - this is extremely verbose, but still quite short for this example:
lemma
fixes a :: "'a::comm_ring"
shows "a + b + c + d = d + b + c + a"
proof -
note assoc = ab_semigroup_add_class.add_ac(1)
have "a + b + c + d = a + (b + c + d)"
unfolding assoc[of a] by rule
also have "… = a + (d + (b + c))"
unfolding add.commute[of d "b + c"] by rule
also have "… = d + (b + c) + a"
unfolding add.commute[of a "d + (b + c)"] by rule
also have "… = d + b + c + a"
unfolding assoc by rule
finally show ?thesis .
qed
- kmill 4y agoHere's a verbose Lean calc proof using single rewrites: import tactic example (R : Type*) [comm_ring R] (a b c d : R) : a + b + c + d = d + b + c + a := calc a + b + c + d = a + b + (c + d) : by rw add_assoc ... = a + (b + (c + d)) : by rw add_assoc ... = b + (c + d) + a : by rw add_comm ... = c + d + b + a : by rw add_comm b ... = d + c + b + a : by rw add_comm c ... = d + (c + b) + a : by rw add_assoc d ... = d + (b + c) + a : by rw add_comm c ... = d + b + c + a : by rw ← add_assoc (I didn't put any thought into trying to make it be efficient.)