Klaus Ostermann

2018-12-08 14:22:10 UTC

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

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