CODEWITHSUNDEEP
isabelleisar
Luiz Martins
Luiz Martins

Reputation: 1724

Accumulating results while using them in Isabelle/Isar

Sometimes in a proof I find myself needing to accumulate results, but also needing use the last result, so I end up using "also then" for that purpose:

proof
  have ...
  also then have ...
  also then have ...
  ultimately show ...
qed

I feel like there are more idiomatic ways to this that I don't know about. On the other hand, this might be the standard way to do it and encouraged by the community.

So in light of that, I have two questions:

  1. Is using "also then" discouraged?
  2. If so, what alternatives can I use to accumulate results while using them?

Upvotes: 0

Views: 169

Answers (1)

user9716869 - supports Ukraine
user9716869 - supports Ukraine

Reputation: 1941

I will start by providing some background. You have breached the subject known as calculational reasoning in Isabelle. Calculation reasoning is described in subsection 1.2 of the document The Isabelle/Isar Reference Manual.

Two of the most common patterns for calculational reasoning are

  have "a R b" sorry
  also have "b R c" sorry
  also have "c R d" sorry
  finally have "a R d" by assumption

(where R is a transitive relation, such as =, written using the infix notation) and

  have P sorry
  moreover have Q  sorry
  moreover have R sorry
  ultimately have S by (rule assms(1))

The commands like also and moreover use an additional fact calculation to store additional information. For example, as the calculation in the first example above proceeds, the fact calculation changes in the following manner

  have "a R b" sorry
  also have "b R c" (*calculation: a R b*) sorry 
  also have "c R d" (*calculation: a R c*) sorry
  finally have "a R d" by assumption

In this case, the transitivity rule of R is used for chaining the predicates. Thus, the final goal can be discharged by assumption. The situation is different for the moreover ... ultimately pattern:

  have P sorry
  moreover have Q (*calculation: P*) sorry
  moreover have R (*calculation: P, Q*) sorry
  ultimately have S (*P ⟹ Q ⟹ R ⟹ S*) by (rule assms(1))

In this case, the fact calculation merely accumulates all previous results.

The implementation of the calculational reasoning is explained in subsection 6.3 of the document The Isabelle/Isar Reference Manual. However, I omit the details in this post.

I will now make an attempt to answer your questions in the context of what was stated above.

Is using "also then" discouraged?

I believe that this is not, necessarily, discouraged and there are some instances of the use of this pattern in the AFP. However, I can imagine that for this specific pattern this would be a reasonably uncommon use case.

If so, what alternatives can I use to accumulate results while using them?

I believe that if you, indeed, need to merely accumulate results (while, possibly, using them in the intermittent steps), the best pattern to use would be moreover ... ultimately. However, of course, this depends on what exactly is meant by the "accumulation of results".

Remark 1

I hope that from the discussion above it is apparent that the use of also in conjunction with ultimately is very unconventional. In most cases, it makes little sense to use such a pattern.

Remark 2

The pattern also ... finally is often used in conjunction with the abbreviation ...:

  have "a R b" sorry
  also have "... R c" sorry
  also have "... R d" sorry
  finally have "a R d" by assumption

Of course, the benefits can only become apparent if b and c are sufficiently long subterms.

Upvotes: 1

Related Questions