Stream: General

Topic: Calculational chaining forgets original Left Hand Side

Gergely Buday (May 27 2025 at 11:08):

For pedagogical reasons I want to do elementary calculational proofs, without automation. Here is a silly example that works:

lemma calculation_silly: "(0::nat) * 3 = 3 * 0"
proof -
  have "(0::nat) * 3 = 0" unfolding Nat.times_nat.mult_0 ..
  also have "... = 0 * 0"  unfolding Nat.times_nat.mult_0 ..
  also have "... = 0"   unfolding Nat.times_nat.mult_0 ..
  also have "... = 3 * 0"   unfolding Nat.mult_0_right ..
  finally show ?thesis .
qed

but then if I prove this lemma:

lemma zero_one: "(0::nat) < 1"
    proof -
      have "0 < Suc 0" unfolding Nat.zero_less_Suc ..
      also have "Suc 0 = 1" by (rule One_nat_def[symmetric])
      finally show ?thesis .
    qed

and trying to prove the base case of an inductive goal similarly:

lemma "(∑i=1..n::nat. (2*i - 1)) = n * n"
proof (induct n)
  case 0
  then show "(∑i = 1..0::nat. 2 * i - 1)  = 0 * 0"
  proof -
    have "(∑i = 1..0::nat. 2 * i - 1) = (∑i∈ {1..0::nat}. 2 * i - 1)" ..
    also have "... = (∑ (i::nat)∈{}. 2*i-1)" unfolding atLeastatMost_empty[OF zero_one] ..
    also have "... = (0::nat)" unfolding  sum.empty ..
    also have "... = (0::nat) * 0"   unfolding Nat.mult_0_right ..
    finally show ?thesis .

Isabelle "forgets" the original Left Hand Side of the chain. Why is this and how could I prevent this? I cannot finish the finally show ?thesis by a dot as with the above two examples.

Mathias Fleury (May 27 2025 at 11:40):

Ah that one I discovered live in front of students

Mathias Fleury (May 27 2025 at 11:41):

also is not always chaining, it can also unfold

Mathias Fleury (May 27 2025 at 11:42):

and this leads to such weird things

Manuel Eberl (Jun 02 2025 at 18:33):

The also command is very general and not very smart. It just applies trans rules. And the trans rule for equality just does substitutes the left-hand side with the right-hand side in the entire calculation (the calculation being the fact accumulated so far). If that calculation is an equation, it substitutes the left-hand side and the right-hand side.

The only way I know of to avoid this is to change the equation that you are proving to something that only applies to the right-hand side but not the left-hand side, e.g. by putting more context around it. Or by hiding the left-hand side underneath a define.

Last updated: Jun 30 2025 at 01:55 UTC