slist.dk

#NAME slist.
(; Lists of natural numbers sorted by construction ;)

def Nat := dk_nat.Nat.
def Bool := dk_bool.Bool.
def true := dk_bool.true.
def Istrue (b : Bool) := dk_logic.eP (dk_logic.ebP b).
def I : Istrue dk_bool.true := dk_logic.I.
def lt := dk_nat.lt.
def eq := dk_nat.eq.
def 0 := dk_nat.O.
def S := dk_nat.S.

Order : Nat -> Nat -> Type.
Lt : n1 : Nat -> n2 : Nat -> Istrue (lt n1 n2) -> Order n1 n2.
Gt : n1 : Nat -> n2 : Nat -> Istrue (lt n2 n1) -> Order n1 n2.
Eq : n1 : Nat -> n2 : Nat -> Istrue (eq n1 n2) -> Order n1 n2.
def compare : n1 : Nat -> n2 : Nat -> Order n1 n2.

def order_S : n1 : Nat -> n2 : Nat -> Order n1 n2 -> Order (S n1) (S n2).
[n1,n2,H] order_S n1 n2 (Lt _ _ H) --> Lt (S n1) (S n2) H
[n1,n2,H] order_S n1 n2 (Gt _ _ H) --> Gt (S n1) (S n2) H
[n1,n2,H] order_S n1 n2 (Eq _ _ H) --> Eq (S n1) (S n2) H.

[] compare dk_nat.O dk_nat.O --> Eq 0 0 I.
[n] compare (dk_nat.S n) dk_nat.O --> Gt (S n) 0 I.
[n] compare dk_nat.O (dk_nat.S n) --> Lt 0 (S n) I.
[n1,n2] compare (dk_nat.S n1) (dk_nat.S n2) --> order_S n1 n2 (compare n1 n2).

(; This is an inductive-recursive definition of sorted lists: cons has
   an extra argument of type Istrue (minors n l) which proves that the
   head of the list minors the rest of the list. However, since we
   only need to look at the head of a sorted list to prove that
   something minors it, the minors function is not really recursive.
;)

slist : Type.
def minors : Nat -> slist -> Bool.
snil : slist.
scons : n : Nat -> l : slist -> Istrue (minors n l) -> slist.

[] minors _ snil --> true
[n1,n2] minors n1 (scons n2 _ _) --> lt n1 n2.


(; To use sorted lists in practice, we need an insert function that is
   going to put its argument at the right position in the list and
   provide the required proof. ;)

def insert : Nat -> slist -> slist.
def insert_aux : n1 : Nat ->
                 n2 : Nat ->
                 l : slist ->
                 Istrue (minors n2 l) ->
                 Order n1 n2 ->
                 slist.
def insert_lemma : n1 : Nat ->
                   n2 : Nat ->
                   l : slist ->
                   Istrue (lt n1 n2) ->
                   Istrue (minors n1 l) ->
                   Istrue (minors n1 (insert n2 l)).
def insert_lemma_2 : n1 : Nat ->
                     n2 : Nat ->
                     n3 : Nat ->
                     l : slist ->
                     H : Istrue (minors n3 l) ->
                     Hlt : Istrue (lt n1 n2) ->
                     Istrue (lt n1 n3) ->
                     Ho : Order n2 n3 ->
                     Istrue (minors n1 (insert_aux n2 n3 l H Ho)).


[n] insert n snil --> scons n snil I
[n1,n2,l,H] insert n1 (scons n2 l H) --> insert_aux n1 n2 l H (compare n1 n2).

[n1,n2,l,H,Hlt] insert_aux n1 n2 l H (Lt _ _ Hlt) --> scons n1 (scons n2 l H) Hlt
[n1,n2,l,H,Hgt] insert_aux n1 n2 l H (Gt _ _ Hgt) --> scons n2 (insert n1 l) (insert_lemma n2 n1 l Hgt H)
[n1,n2,l,H]     insert_aux n1 n2 l H (Eq _ _ _) --> scons n2 l H.

[Hlt] insert_lemma _ _ snil Hlt _ --> Hlt
[n1,n2,n3,l,H,Hlt,H1] insert_lemma n1 n2 (scons n3 l H) Hlt H1 --> insert_lemma_2 n1 n2 n3 l H Hlt H1 (compare n2 n3).

[H] insert_lemma_2 _ _ _ _ _ H _ (Lt _ _ _) --> H
[H] insert_lemma_2 _ _ _ _ _ _ H (Gt _ _ _) --> H
[H] insert_lemma_2 _ _ _ _ _ _ H (Eq _ _ _) --> H.


(; Simple test, if we insert 7, then 8, then 9, we get [7, 8, 9].
   On concrete numbers, the logical arguments compute to I : Istrue true. ;)

#CONV insert dk_nat.9 (insert dk_nat.8 (insert dk_nat.7 snil)), scons dk_nat.7 (scons dk_nat.8 (scons dk_nat.9 snil I) I) I.