insert_sort

import data.list
import data.list.sorted

open list
open list.sorted
open has_le

namespace list

inductive In (x : A) : list A -> Prop :=
| base {} : forall {l}, In x (x :: l)
| step {} : forall {l} {y}, In x l -> In x (y :: l)

definition subset l1 l2 := forall x, In x l1 -> In x l2
definition perm l1 l2 := and (subset l1 l2) (subset l2 l1)
local notation `~=`:60 := perm

lemma perm_sym [symm] : forall l l', l ~= l' -> l' ~= l :=
    begin
    now
    end

lemma hd_rel_perm : forall R y l1 l2
    , l1 ~= l2
    -> hd_rel R y l1
    -> hd_rel R y l2 :=
begin
now
end

lemma sorted_to_hd
    : forall x y l
    , sorted l
    -> not (x <= y)
    -> hd_rel le y (x l) :=
    begin
    now
    end

end list


section insert_sort

parameter {A : Type}
infix `<=` := has_le.le

definition insert
    [has_le A]
    [forall x y: A, decidable (x <= y)]
    : A -> list A -> list A
| x [] := [x]
| x (y :: ys) :=
    if x <= y
    then x :: (y :: ys)
    else y :: insert x ys

definition insert_sort
    [has_le A]
    [forall x y: A, decidable (x <= y)]
    : list A -> list A
| [] := []
| (x :: xs) := insert x (insert_sort xs)

print decidable

lemma ite_rec
    {T}  (P : T -> Prop) (t f : T) c [decidable c]
    : (c -> P t) -> (not c -> P f) -> P (ite c t f) :=
    begin
    intros Pt Pf
    , cases _inst_1
    , all_goals unfold ite
    , {apply Pt, assumption}
    , {apply Pf, assumption}
    , now
    end

print list.hd_rel

lemma insert_step_correct
    [has_le A]
    [forall x y: A, decidable (x <= y)]
    (x : A)
    (l : list A)
    : sorted le l -> sorted le (insert x l) :=
    begin
    induction l with y l IH
    , all_goals intros S
    , all_goals unfold insert
    , {repeat constructor}
    , apply ite_rec
    , all_goals intros H
    ,   { repeat1 constructor
        , all_goals assumption
        }
    ,   { constructor
        , now
        }
    , now
    end

end insert_sort