First of all, thanks to those who stayed on Wednesday for 15 additional min., and sorry for taking that extra time. I thought finishing that block was needed to start a new section next week. The lecture recording is already linked from the course webpage.

When I asked for the specification of a sorted list, some of you suggested

(1) ∀ i · [i ∈ 1..n-1 ⇒ f(i) ≤ f(i+1)]

instead of

(2) ∀ i,j · [(i ∈ dom(f) ∧ j ∈ dom(f) ∧ i ≤ j) ⇒ f(i) ≤ f(j)]

IIRC, I said that both should be equivalent, but that I was not sure whether the first one could be directly used in the proof obligations.

First of all, (1) is a particular case of the (2), and Rodin can prove that automatically: make (2) be an axiom and (1) a theorem; save, and should be proved.

But the proofs use repeatedly the f(r) > v hypotheses, where v = f(x) for some x, so that we can use f(r) > f(x). That matches the contraposition of (2), but not that of (1), because we do not know the distance between r and x. So axiom (1) cannot be directly used.

However, one "sees" clearly that if we have (1), then (2) should also be true. But that is because we in our minds apply (1) to position 1, then f(1) <= f(2); we repeat for f(2), then f(2) <= f(3) and therefore f(1) <= f(3), and so on. To really prove that this is the case, we have to find a formal proof.

Proving *formally* that (2) can be inferred from (1) needs using an induction scheme similar (only similar -- I did not work it out, but it does not look straightforward) to

P(0) ∧ ∀ n · n ∈ ℕ ∧ P(n) ⇒ P(n+1)

for some arbitrary property P. This induction scheme is not part of the standard theorem provers available for Rodin, so it is not going to work out of the box. Such induction schemes *can* be written in Rodin, and we'll see an example if we have time.

Bottom line: let's agree that (2) is a definition of a sorted list.

Cheers,