Commit 1ebfb416 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Add a file on sorted lists of natural numbers

parent dfeed096
#NAME slist.
(; Lists of natural numbers sorted by construction ;)
Nat := dk_nat.Nat.
Bool := dk_bool.Bool.
true := dk_bool.true.
false := dk_bool.false.
and := dk_bool.and.
Istrue := b : Bool => dk_logic.eP (dk_logic.ebP b).
I : Istrue true := dk_logic.I.
slist : Type.
minor : Nat -> slist -> Bool. (; minor n l = true <-> n < min(l) ;)
snil : slist.
scons : n : Nat -> l : slist -> Istrue (minor n l) -> slist.
[] minor _ snil --> true.
[ n1 : Nat, n2 : Nat, l : slist ]
minor n1 (scons n2 l _) --> dk_nat.lt n1 n2.
eq : slist -> slist -> Bool.
[ l : slist ] eq l l --> true
[ n : Nat, l : slist ] eq snil (scons n l _) --> false
[ n : Nat, l : slist ] eq (scons n l _) snil --> false
[ n1 : Nat, n2 : Nat,
l1 : slist, l2 : slist ]
eq (scons n1 l1 _) (scons n2 l2 _)
-->
and (dk_nat.eq n1 n2)
(eq l2 l2).
min : slist -> Nat.
[ n : Nat, l : slist ] min (scons n l _) --> n.
min_lemma : n : Nat ->
l : slist ->
H : Istrue (dk_nat.lt n (min l)) ->
Istrue (minor n l).
[ n1 : Nat, n2 : Nat,
l : slist, H2 : Istrue (minor n2 l),
H : Istrue (dk_nat.lt n1 n2) ] min_lemma n1 (scons n2 l H2) H --> H.
insert : Nat -> slist -> slist.
insert_lemma_1 : n1 : Nat ->
n2 : Nat ->
l : slist ->
Istrue (minor n2 l) ->
Istrue (dk_nat.lt n2 n1) ->
Istrue (minor n2 (insert n1 l)).
insert_lemma_2 : n : Nat ->
l : slist ->
Istrue (dk_nat.leq (min (insert n l)) n).
insert_aux : n1 : Nat ->
n2 : Nat ->
l : slist ->
H : Istrue (minor n2 l) ->
b1 : Bool ->
b2 : Bool ->
b3 : Bool ->
Hb1 : (Istrue b1 -> Istrue (dk_nat.eq n1 n2)) ->
Hb2 : (Istrue b2 -> Istrue (dk_nat.lt n1 n2)) ->
Hb3 : (Istrue b3 -> Istrue (dk_nat.lt n2 n1)) ->
slist.
[ n : Nat ] insert n snil --> scons n snil I
[ n1 : Nat, n2 : Nat,
l : slist, H : Istrue (minor n2 l)]
insert n1 (scons n2 l H)
-->
insert_aux n1 n2 l H
(dk_nat.eq n1 n2)
(dk_nat.lt n1 n2)
(dk_nat.lt n2 n1)
(H1 : Istrue (dk_nat.eq n1 n2) => H1)
(H2 : Istrue (dk_nat.lt n1 n2) => H2)
(H3 : Istrue (dk_nat.lt n2 n1) => H3).
[ n1 : Nat, n2 : Nat,
l : slist, H : Istrue (minor n2 l), b2 : Bool, b3 : Bool ]
insert_aux n1 n2 l H dk_bool.true b2 b3 _ _ _
-->
scons n2 l H
[ n1 : Nat, n2 : Nat,
l : slist, H : Istrue (minor n2 l),
H2 : Istrue true -> Istrue (dk_nat.lt n1 n2), b1 : Bool, b3 : Bool ]
insert_aux n1 n2 l H b1 dk_bool.true b3 _ H2 _
-->
scons n1 (scons n2 l H) (H2 I)
[ n1 : Nat, n2 : Nat,
l : slist, H : Istrue (minor n2 l),
H3 : Istrue true -> Istrue (dk_nat.lt n2 n1), b1 : Bool, b2 : Bool ]
insert_aux n1 n2 l H b1 b2 dk_bool.true _ _ H3
-->
scons n2 (insert n1 l) (insert_lemma_1 n1 n2 l H (H3 I)).
(; Missing case: all booleans are false, never appears on values. ;)
(; Add a rule on min, cross fingers for confluence ;)
[n1 : Nat, n2 : Nat, l : slist, b1 : Bool, b2 : Bool, b3 : Bool ]
min (insert_aux n1 n2 l _ b1 b2 b3 _ _ _) --> dk_nat.min n1 n2.
nat_leq_refl : n : Nat -> Istrue (dk_nat.leq n n).
[] nat_leq_refl dk_nat.0 --> I
[ n : Nat ] nat_leq_refl (dk_nat.S n) --> nat_leq_refl n.
nat_leq_min_left : n1 : Nat -> n2 : Nat -> Istrue (dk_nat.leq (dk_nat.min n1 n2) n1).
[ n2 : Nat ] nat_leq_min_left dk_nat.O n2 --> nat_leq_refl dk_nat.0
[ n1 : Nat ] nat_leq_min_left (dk_nat.S n1) dk_nat.0 --> I
[ n1 : Nat, n2 : Nat ]
nat_leq_min_left (dk_nat.S n1) (dk_nat.S n2)
-->
nat_leq_min_left n1 n2.
nat_leq_min_left_lt : n1 : Nat ->
n2 : Nat ->
n3 : Nat ->
Istrue (dk_nat.lt n3 n1) ->
Istrue (dk_nat.lt n3 n2) ->
Istrue (dk_nat.lt n3 (dk_nat.min n1 n2)).
[ n1 : Nat, n2 : Nat ]
nat_leq_min_left_lt (dk_nat.S n1) (dk_nat.S n2) dk_nat.O _ _
-->
I
[ n1 : Nat, n2 : Nat, n3 : Nat,
H1 : Istrue (dk_nat.lt n3 n1),
H2 : Istrue (dk_nat.lt n3 n2) ]
nat_leq_min_left_lt (dk_nat.S n1) (dk_nat.S n2) (dk_nat.S n3) H1 H2
-->
nat_leq_min_left_lt n1 n2 n3 H1 H2.
[ n : Nat ] insert_lemma_2 n snil --> nat_leq_refl n
[ n1 : Nat, n2 : Nat,
l : slist, H : Istrue (minor n2 l) ]
insert_lemma_2 n1 (scons n2 l H) --> nat_leq_min_left n1 n2.
[ n1 : Nat, n2 : Nat, H : Istrue (dk_nat.lt n2 n1) ]
insert_lemma_1 n1 n2 snil _ H --> H.
[ n1 : Nat, n2 : Nat, H : Istrue (dk_nat.lt n2 n1),
n3 : Nat, l : slist, H3 : Istrue (minor n3 l),
H2 : Istrue (minor n2 (scons n3 l H3)) ]
insert_lemma_1 n1 n2 (scons n3 l H3) H2 H
-->
min_lemma
n2
(insert n1 (scons n3 l H3))
(nat_leq_min_left_lt n1 n3 n2 H H2).
#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.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment