The Coq mailing list

[Xuanrui Qi <xqi01 AT cs.tufts.edu>]

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" <fdhzs2010 AT 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:

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-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>
Sent: December 8, 2018 9:22 AM
To: coq-club AT 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