[Agda] Re: A puzzle with "with"

[Stevan Andjelkovic]

James McKinna <james.mckinna at ...> writes:
> So, we are now very confused about the implementation and
> semantics of "with" in Agda. Can you please explain
> how one might solve such a problem and learn how to avoid it in the future.

Hi,

I think in general when you are proving properties about functions in an
external logic fashion, as below, you want the proof to have the same
structure as the function. In this case; sorted_insert to have the same
structure as insert.

As the implementation of insert is now, the proof would indeed be the
way you first tried in sorted_insert -- using "with (Order.comp o x y)"
in both the function and the proof.

But as you point out you need inspect! So I think the easiest way would
be change the structure of the insert function to reflect the needed
structure of the proof -- define insert in terms of inspect:

  insert x (y :: ys) with inspect (Order.comp o x y)

And then use the structure of sorted_insert2:

  sorted_insert2 x (y :: ys) prf with inspect (Order.comp o x y)
  sorted_insert2 x (y :: ys) prf | Lt with-== p = insert_lt x y ys prf (sym p)

But I think the way you defined Order or Sorted complicates things. If
check the goal of:

  sorted_insert2 x (y :: ys) prf = ?0

It is:

  ?0 : Sorted (insert x (y ∷ ys))  

Which doesn't give you any help at all. Compare that to the External
version here:

  http://web.student.chalmers.se/groups/datx02-dtp/html/SortedList.html

If you do the same thing there and look at the following hole's goal:

  sorted a (x :: y :: xs) (x<=y , sorted-y::xs) = ?

It will say:

  ?0 : Sorted (insert a (x :: y :: xs) | total a x)

>From which we know we have to "with total a x" and then we get two new
goals which are again very helpful. Take a look at the comments in the
definition of lemma, those are the goals of the definitions under them!

I hope that helps with the how-to-do-it question. Exactly why some ways
of defining the functions give more helpful goals when doing the proofs
for them, I don't know.

You might also be interested in some other properties of insert:

  http://web.student.chalmers.se/groups/datx02-dtp/html/SLInsertProps.html

As it says in the comments; it's not really complete. An other question
is if the three properties really are sufficient to prove that the
insertion sort really returns a permutation of its input.

Here is a Coq version of the permutation proof for insertion sort:

  http://www.cs.nott.ac.uk/~txa/g54cfr/l14.v

I haven't figured out how to do that in Agda yet tho.