[Coq-Club] Certified insertion

[Klaus Ostermann]

I'm making a few experiments with using subset types for "certified
programming".

I'm stuck with a certified variants of the "insert" function as used in
insertion sort, that is,
it's type should say that the input list and output list are sorted and
that the output list
contains both the input list and the element to be inserted.

Could somebody tell me how to do this idiomatically in Coq, preferably
without using
"dependent destruction" and other tactics that require additional
axioms? I'm stuck on
how to make the case distinction on whether the element to be inserted
is less than or eqal
to the first element. Presumably this requires a fancy "return" annotation?

Inductive Sorted : list nat -> Prop :=
    | Sorted_nil : Sorted []
    | Sorted_cons1 a : Sorted [a]
    | Sorted_consn a b l :
        Sorted (b :: l) -> a <= b -> Sorted (a :: b :: l).

Definition sortedOf(l: list nat)(q: list nat) := Sorted q /\ forall m,
In m l <-> In m q.

Fixpoint insert(n: nat)(l: { q: list nat | Sorted q}) : { q: list nat |
sortedOf (cons n (proj1_sig l)) q}.   
refine(  match l return { q: list nat | sortedOf (cons n (proj1_sig l))
q} with
  | exist [] st =>  _
  | exist (cons x xs) st => _
  end).
- refine (exist _ [n] _). split.  constructor. intros. split; intros. 
simpl in H ; destruct H ; subst; constructor; auto. inversion H.
  constructor. inversion H ; subst; auto. inversion H0.
-  (* stuck here; how to make the case distinction on whether n <= x ? )


Klaus

[Jason -Zhong Sheng- Hu]

Hi Klaus,

In Appel's Software Foundations Vol. 3, there are two chapters proving insertion sort correct. Not sure if you've taken a look? https://softwarefoundations.cis.upenn.edu/vfa-current/toc.html
Table of contents - Software Foundations<https://softwarefoundations.cis.upenn.edu/vfa-current/toc.html>
Selection Sort, With Specification and Proof of Correctness ()Top; The Selection-Sort Program; Proof of Correctness of Selection sort; Recursive Functions That are Not Structurally Recursive
softwarefoundations.cis.upenn.edu


Regarding your original problem, this can be solved without invoking K, but it's kind of annoying to do all these work manually. To provide an initial refinement:

Require Import Coq.Arith.Compare_dec.

Fixpoint insert(n: nat)(l: { q: list nat | Sorted q})
: { q: list nat | sortedOf (cons n (proj1_sig l)) q}.
Proof.
refine (let (l', sorted_l') as l0
return { q: list nat | sortedOf (cons n (proj1_sig l0)) q} := l
in match l' as l0
return Sorted l0 ->
{ q: list nat | sortedOf (cons n l0) q} with
| nil => fun _ => exist _ [n] _
| cons x xs =>
fun sorted_l' =>
match le_lt_dec n x with
| left n_le_x => exist _ (n :: x :: xs) _
| right x_lt_n => _
end
end sorted_l').

To point out what's missing in your original solution:

1. Since dependent sum types in Coq has no definitional eta expansion, the extended let binding up front is needed to unpack the list and the evidence. The later is required in the recursive case. You originally attempted to use extended match directly, so it didn't work.
2. Extended match then can be used to split cases. But Sorted evidence needs to be carried in.
3. In the cons case, then you can use decision procedure (from Arith.Compare_dec) to decide ordering.

In the `right` case in `cons`, you need to do a recursive call, and you will have to use extended let to unpack the result again in order to expose the list and the evidence.

So it's not quite convenient. It's much better off to do the same as what Appel did in Vol 3. Additionally, you might fall into trouble proving additional theorems on this function, because `destruct` will have some trouble handling case analysis with the presence of dependent types. Another solution is to use Equations, which is much more friendly and more powerful in dependently typed settings. Equations also allows you to disable K, so if you are worried about your foundation, you are secured as well.

Sincerely Yours,

Jason Hu
________________________________
From: coq-club-***@inria.fr <coq-club-***@inria.fr> on behalf of Klaus Ostermann <***@uni-tuebingen.de>
Sent: December 8, 2018 9:22 AM
To: coq-***@inria.fr
Subject: [Coq-Club] Certified insertion

I'm making a few experiments with using subset types for "certified
programming".

I'm stuck with a certified variants of the "insert" function as used in
insertion sort, that is,
it's type should say that the input list and output list are sorted and
that the output list
contains both the input list and the element to be inserted.

Could somebody tell me how to do this idiomatically in Coq, preferably
without using
"dependent destruction" and other tactics that require additional
axioms? I'm stuck on
how to make the case distinction on whether the element to be inserted
is less than or eqal
to the first element. Presumably this requires a fancy "return" annotation?

Inductive Sorted : list nat -> Prop :=
| Sorted_nil : Sorted []
| Sorted_cons1 a : Sorted [a]
| Sorted_consn a b l :
Sorted (b :: l) -> a <= b -> Sorted (a :: b :: l).

Definition sortedOf(l: list nat)(q: list nat) := Sorted q /\ forall m,
In m l <-> In m q.

Fixpoint insert(n: nat)(l: { q: list nat | Sorted q}) : { q: list nat |
sortedOf (cons n (proj1_sig l)) q}.
refine( match l return { q: list nat | sortedOf (cons n (proj1_sig l))
q} with
| exist [] st => _
| exist (cons x xs) st => _
end).
- refine (exist _ [n] _). split. constructor. intros. split; intros.
simpl in H ; destruct H ; subst; constructor; auto. inversion H.
constructor. inversion H ; subst; auto. inversion H0.
- (* stuck here; how to make the case distinction on whether n <= x ? )


Klaus

[Xuanrui Qi]

Hi Klaus,




Program Fixpoint or Function will probably do the trick.  Usually, they will work much better than refine in the presence of subset types. There's a manual here: https://coq.inria.fr/refman/addendum/program.html.




You can also look at this program I've written, which uses subset types extensively: https://github.com/xuanruiqi/verified-data-structures/blob/master/twothree_dependent.v. This might give you some idea.




-Ray




On Sat, Dec 8, 2018 at 10:54 AM -0500, "Jason -Zhong Sheng- Hu" <***@hotmail.com> wrote:

















Hi Klaus,





In Appel's Software Foundations Vol. 3, there are two chapters proving insertion sort correct. Not sure if you've taken a look?

https://softwarefoundations.cis.upenn.edu/vfa-current/toc.html






Table of contents - Software Foundations

Selection Sort, With Specification and Proof of Correctness ()Top; The Selection-Sort Program; Proof of Correctness of Selection sort; Recursive Functions That are Not Structurally Recursive

softwarefoundations.cis.upenn.edu










Regarding your original problem, this can be solved without invoking K, but it's kind of annoying to do all these work manually. To provide an initial refinement:





Require Import Coq.Arith.Compare_dec.







Fixpoint insert(n: nat)(l: { q: list nat | Sorted q})


  : { q: list nat | sortedOf (cons n (proj1_sig l)) q}.


Proof.


  refine (let (l', sorted_l') as l0


              return { q: list nat | sortedOf (cons n (proj1_sig l0)) q} := l


          in match l' as l0


                   return Sorted l0 ->


                          { q: list nat | sortedOf (cons n l0) q} with


             | nil => fun _ => exist _ [n] _


             | cons x xs =>


               fun sorted_l' =>


                 match le_lt_dec n x with


                 | left n_le_x => exist _ (n :: x :: xs) _


                 | right x_lt_n => _


                 end


             end sorted_l').







To point out what's missing in your original solution:



Since dependent sum types in Coq has no definitional eta expansion, the extended let binding up front is needed to unpack the list and the evidence. The later is required in the recursive case. You originally attempted to use extended match directly, so it
didn't work.
Extended match then can be used to split cases. But Sorted evidence needs to be carried in.
In the cons case, then you can use decision procedure (from Arith.Compare_dec) to decide ordering.
In the `right` case in `cons`, you need to do a recursive call, and you will have to use extended let to unpack the result again in order to expose the list and the evidence.





So it's not quite convenient. It's much better off to do the same as what Appel did in Vol 3. Additionally, you might fall into trouble proving additional theorems on this function, because `destruct` will have some trouble handling case analysis with the presence
of dependent types. Another solution is to use Equations, which is much more friendly and more powerful in dependently typed settings. Equations also allows you to disable K, so if you are worried about your foundation, you are secured as well.








Sincerely Yours,




Jason Hu



From: coq-club-***@inria.fr <coq-club-***@inria.fr> on behalf of Klaus Ostermann <***@uni-tuebingen.de>

Sent: December 8, 2018 9:22 AM

To: coq-***@inria.fr

Subject: [Coq-Club] Certified insertion
 


I'm making a few experiments with using subset types for "certified

programming".



I'm stuck with a certified variants of the "insert" function as used in

insertion sort, that is,

it's type should say that the input list and output list are sorted and

that the output list

contains both the input list and the element to be inserted.



Could somebody tell me how to do this idiomatically in Coq, preferably

without using

"dependent destruction" and other tactics that require additional

axioms? I'm stuck on

how to make the case distinction on whether the element to be inserted

is less than or eqal

to the first element. Presumably this requires a fancy "return" annotation?



Inductive Sorted : list nat -> Prop :=

    | Sorted_nil : Sorted []

    | Sorted_cons1 a : Sorted [a]

    | Sorted_consn a b l :

        Sorted (b :: l) -> a <= b -> Sorted (a :: b :: l).



Definition sortedOf(l: list nat)(q: list nat) := Sorted q /\ forall m,

In m l <-> In m q.



Fixpoint insert(n: nat)(l: { q: list nat | Sorted q}) : { q: list nat |

sortedOf (cons n (proj1_sig l)) q}.   

refine(  match l return { q: list nat | sortedOf (cons n (proj1_sig l))

q} with

  | exist [] st =>  _

  | exist (cons x xs) st => _

  end).

- refine (exist _ [n] _). split.  constructor. intros. split; intros. 

simpl in H ; destruct H ; subst; constructor; auto. inversion H.

  constructor. inversion H ; subst; auto. inversion H0.

-  (* stuck here; how to make the case distinction on whether n <= x ? )





Klaus

[Adam Chlipala]

Post by Klaus Ostermann
I'm making a few experiments with using subset types for "certified
programming".
I'm stuck with a certified variants of the "insert" function as used in
insertion sort, that is,
it's type should say that the input list and output list are sorted and
that the output list
contains both the input list and the element to be inserted.
Could somebody tell me how to do this idiomatically in Coq, preferably
without using
"dependent destruction" and other tactics that require additional
axioms?

What follows is probably not the sort of answer you are looking for, but
I think it might nonetheless be the most useful one you receive.

It actually isn't idiomatic to program with subset types in Coq! I
recommend avoiding explicit dependently typed programming whenever
possible.  There should be a high standard of justification for any
explicit dependent types (which are sometimes the right tool for a
job).  It tends to be painful to define and reason about such programs. 
Experts generally avoid it.

[Klaus Ostermann]

Hi Adam,

Post by Adam Chlipala
It actually isn't idiomatic to program with subset types in Coq! I
recommend avoiding explicit dependently typed programming whenever
possible.  There should be a high standard of justification for any
explicit dependent types (which are sometimes the right tool for a
job).  It tends to be painful to define and reason about such
programs.  Experts generally avoid it.

thanks for your advice. I actually guessed that much by now. However, my
intention here was to experience and understand the nature of the pain :)

Klaus

[Xuanrui Qi]

Post by Adam Chlipala
There should be a high standard of justification for any
explicit dependent types (which are sometimes the right tool for a
job). It tends to be painful to define and reason about such
programs.
Experts generally avoid it.

Adam is definitely the expert here, and his words are very true.

I tend to use dependent types in Coq when (1) I want to encode
something using dependent types (usually just a type indexed by a few
nat's) and (2) the invariants are too complex to prove without tactics.

Subset types are difficult to reason with even with `Program Fixpoint`
or `Function`! Sometimes, you can't even define the functions you want
with `Program Fixpoint`, which makes it just a total mess. There are
various workarounds (like defining your program using tactics), but
it's totally not worth the trouble to get into, unless absolutely
necessary.

Besides, if you want a certified ML program, dependent types will
extract to really dirty code with `Obj.magic` everywhere, which is not
ideal. So, Coq is really not designed for dependently-typed programming
(although you can do it), and avoiding it would be the wise thing to
do. In my opinion, this is a serious flaw in the design Coq.

-Ray

Post by Adam Chlipala
Hi Adam,

Post by Adam Chlipala
It actually isn't idiomatic to program with subset types in Coq! I
recommend avoiding explicit dependently typed programming whenever
possible. There should be a high standard of justification for any
explicit dependent types (which are sometimes the right tool for a
job). It tends to be painful to define and reason about such
programs. Experts generally avoid it.

thanks for your advice. I actually guessed that much by now. However, my
intention here was to experience and understand the nature of the pain :)
Klaus

[Jonathan Leivent]

Klaus,


If you want to see decent sized fully-dependent types experiments in
certified code generation, you are welcome to examine my (somewhat out
of date) github developments:

https://github.com/jonleivent/mindless-coding-phase2

https://github.com/jonleivent/mindless-coding

The point of these was to experiment with how to make dependent-type
guided programming easy enough for non prover-experts.

They are based on the use of one somewhat controversial axiom that
allows the dependent type residue to be more thoroughly erased from the
certified code than is otherwise possible in Coq.

I abandoned these mostly due to Ltac causing me more pain than I could
tolerate.  I await Ltac 2's full implementation before considering
whether or not to re-attempt.

-- Jonathan

Post by Klaus Ostermann
Hi Adam,

Post by Adam Chlipala
It actually isn't idiomatic to program with subset types in Coq! I
recommend avoiding explicit dependently typed programming whenever
possible.  There should be a high standard of justification for any
explicit dependent types (which are sometimes the right tool for a
job).  It tends to be painful to define and reason about such
programs.  Experts generally avoid it.

thanks for your advice. I actually guessed that much by now. However, my
intention here was to experience and understand the nature of the pain :)
Klaus