This file proposes an implementation of the non-dependant
interface FSetInterface.S using strictly ordered list.
|
Require Export FSetInterface.
Set Implicit Arguments.
| Usual syntax for lists. CAVEAT: the Coq cast "::" will no longer be available. |
Notation "[]" := (nil ?) (at level 1).
Notation "a :: l" := (cons a l) (at level 1, l at next level).
Module Raw [X : OrderedType].
Module E := X.
Module ME := MoreOrderedType X.
Definition elt := E.t.
Definition t := (list elt).
Definition is_empty : t -> bool := [l]if l then true else [_,_]false.
The set operations. |
Fixpoint mem [x:elt; s:t] : bool := Cases s of
nil => false
| (cons y l) => Cases (E.compare x y) of
(Lt _) => false
| (Eq _) => true
| (Gt _) => (mem x l)
end
end.
Fixpoint add [x:elt; s:t] : t := Cases s of
nil => x::[]
| (cons y l) => Cases (E.compare x y) of
(Lt _) => x::s
| (Eq _) => s
| (Gt _) => y::(add x l)
end
end.
Definition singleton : elt -> t := [x] x::[].
Fixpoint remove [x:elt; s:t] : t := Cases s of
nil => []
| (cons y l) => Cases (E.compare x y) of
(Lt _) => s
| (Eq _) => l
| (Gt _) => y::(remove x l)
end
end.
Fixpoint union [s:t] : t -> t := Cases s of
nil => [s']s'
| (cons x l) =>
Fix union_aux { union_aux / 1 : t -> t := [s']Cases s' of
nil => s
| (cons x' l') => Cases (E.compare x x') of
(Lt _ ) => x::(union l s')
| (Eq _ ) => x::(union l l')
| (Gt _) => x'::(union_aux l')
end
end}
end.
Fixpoint inter [s:t] : t -> t := Cases s of
nil => [_] []
| (cons x l) =>
Fix inter_aux { inter_aux / 1 : t -> t := [s']Cases s' of
nil => []
| (cons x' l') => Cases (E.compare x x') of
(Lt _ ) => (inter l s')
| (Eq _ ) => x::(inter l l')
| (Gt _) => (inter_aux l')
end
end}
end.
Fixpoint diff [s:t] : t -> t := Cases s of
nil => [_] []
| (cons x l) =>
Fix diff_aux { diff_aux / 1 : t -> t := [s']Cases s' of
nil => s
| (cons x' l') => Cases (E.compare x x') of
(Lt _ ) => x::(diff l s')
| (Eq _ ) => (diff l l')
| (Gt _) => (diff_aux l')
end
end}
end.
Fixpoint equal [s:t] : t -> bool := [s':t]Cases s s' of
nil nil => true
| (cons x l) (cons x' l') => Cases (E.compare x x') of
(Eq _) => (equal l l')
| _ => false
end
| _ _ => false
end.
Fixpoint subset [s,s':t] : bool := Cases s s' of
nil _ => true
| (cons x l) (cons x' l') => Cases (E.compare x x') of
(Lt _) => false
| (Eq _) => (subset l l')
| (Gt _) => (subset s l')
end
| _ _ => false
end.
Fixpoint fold [B:Set; f:elt->B->B; s:t] : B -> B := [i]Cases s of
nil => i
| (cons x l) => (f x (fold f l i))
end.
Fixpoint filter [f:elt->bool; s:t] : t := Cases s of
nil => []
| (cons x l) => if (f x) then x::(filter f l) else (filter f l)
end.
Fixpoint for_all [f:elt->bool; s:t] : bool := Cases s of
nil => true
| (cons x l) => if (f x) then (for_all f l) else false
end.
Fixpoint exists [f:elt->bool; s:t] : bool := Cases s of
nil => false
| (cons x l) => if (f x) then true else (exists f l)
end.
Fixpoint partition [f:elt->bool; s:t] : t*t := Cases s of
nil => ([],[])
| (cons x l) => let (s1,s2) = (partition f l) in
if (f x) then (x::s1,s2) else (s1,x::s2)
end.
Definition cardinal : t -> nat := [s](fold [_]S s O).
Definition elements : t -> (list elt) := [x]x.
Definition min_elt : t -> (option elt) := [s]Cases s of
nil => (None ?)
| (cons x _) => (Some ? x)
end.
Fixpoint max_elt [s:t] : (option elt) := Cases s of
nil => (None ?)
| (cons x nil) => (Some ? x)
| (cons _ l) => (max_elt l)
end.
Proofs of set operation specifications. |
Definition In : elt -> t -> Prop := (InList E.eq).
Notation "'Sort' l" := (sort E.lt l) (at level 10, l at level 8).
Notation "'Inf' x l" := (lelistA E.lt x l) (at level 10, x,l at level 8).
Notation "'In' x l" := (InList E.eq x l) (at level 10, x,l at level 8).
Definition Equal := [s,s'](a:elt)(In a s)<->(In a s').
Definition Subset := [s,s'](a:elt)(In a s)->(In a s').
Definition Add := [x:elt;s,s':t](y:elt)(In y s') <-> ((E.eq y x)\/(In y s)).
Definition Empty := [s](a:elt)~(In a s).
Definition For_all := [P:elt->Prop; s:t](x:elt)(In x s)->(P x).
Definition Exists := [P:elt->Prop; s:t](EX x:elt | (In x s)/\(P x)).
Definition In_eq: (s:t)(x,y:elt)(E.eq x y) -> (In x s) -> (In y s) := ME.In_eq.
Definition Inf_lt : (s:t)(x,y:elt)(E.lt x y) -> (Inf y s) -> (Inf x s) := ME.Inf_lt.
Definition Inf_eq : (s:t)(x,y:elt)(E.eq x y) -> (Inf y s) -> (Inf x s) := ME.Inf_eq.
Definition In_sort : (s:t)(x,a:elt)(Inf a s) -> (In x s) -> (Sort s) -> (E.lt a x) := ME.In_sort.
Hints Resolve Inf_lt Inf_eq.
Hints Immediate In_eq.
Lemma mem_1: (s:t)(Hs:(Sort s))(x:elt)(In x s) -> (mem x s)=true.
Lemma mem_2: (s:t)(x:elt)(mem x s)=true -> (In x s).
Lemma add_Inf : (s:t)(x,a:elt)(Inf a s)->(E.lt a x)->(Inf a (add x s)).
Hints Resolve add_Inf.
Lemma add_sort : (s:t)(Hs:(Sort s))(x:elt)(Sort (add x s)).
Lemma add_1 : (s:t)(Hs:(Sort s))(x,y:elt)(E.eq y x) -> (In y (add x s)).
Lemma add_2 : (s:t)(Hs:(Sort s))(x,y:elt)(In y s) -> (In y (add x s)).
Lemma add_3 : (s:t)(Hs:(Sort s))(x,y:elt)
~(E.eq x y) -> (In y (add x s)) -> (In y s).
Lemma remove_Inf : (s:t)(Hs:(Sort s))(x,a:elt)(Inf a s)->
(Inf a (remove x s)).
Hints Resolve remove_Inf.
Lemma remove_sort : (s:t)(Hs:(Sort s))(x:elt)(Sort (remove x s)).
Lemma remove_1 : (s:t)(Hs:(Sort s))(x,y:elt)(E.eq y x) -> ~(In y (remove x s)).
Lemma remove_2 : (s:t)(Hs:(Sort s))(x,y:elt)
~(E.eq x y) -> (In y s) -> (In y (remove x s)).
Lemma remove_3 : (s:t)(Hs:(Sort s))(x,y:elt)(In y (remove x s)) -> (In y s).
Lemma singleton_sort : (x:elt)(Sort (singleton x)).
Lemma singleton_1 : (x,y:elt)(In y (singleton x)) -> (E.eq x y).
Lemma singleton_2 : (x,y:elt)(E.eq x y) -> (In y (singleton x)).
Tactic Definition DoubleInd :=
Induction s;
[Simpl; Auto; Try Solve [ Intros; Inversion H ] |
Intros x l Hrec;
Induction s';
[Simpl; Auto; Try Solve [ Intros; Inversion H ] |
Intros x' l' Hrec' Hs Hs'; Inversion Hs; Inversion Hs'; Subst; Simpl]].
Lemma union_Inf : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(a:elt)
(Inf a s) -> (Inf a s') -> (Inf a (union s s')).
Hints Resolve union_Inf.
Lemma union_sort : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(Sort (union s s')).
Lemma union_1 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt)
(In x (union s s')) -> (In x s)\/(In x s').
Lemma union_2 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt)
(In x s) -> (In x (union s s')).
Lemma union_3 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt)
(In x s') -> (In x (union s s')).
Lemma inter_Inf : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(a:elt)
(Inf a s) -> (Inf a s') -> (Inf a (inter s s')).
Hints Resolve inter_Inf.
Lemma inter_sort : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(Sort (inter s s')).
Lemma inter_1 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt)
(In x (inter s s')) -> (In x s).
Lemma inter_2 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt)
(In x (inter s s')) -> (In x s').
Lemma inter_3 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt)
(In x s) -> (In x s') -> (In x (inter s s')).
Lemma diff_Inf : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(a:elt)
(Inf a s) -> (Inf a s') -> (Inf a (diff s s')).
Hints Resolve diff_Inf.
Lemma diff_sort : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(Sort (diff s s')).
Lemma diff_1 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt)
(In x (diff s s')) -> (In x s).
Lemma diff_2 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt)
(In x (diff s s')) -> ~(In x s').
Lemma diff_3 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt)
(In x s) -> ~(In x s') -> (In x (diff s s')).
Lemma equal_1: (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))
(Equal s s') -> (equal s s')=true.
Lemma equal_2: (s,s':t)(equal s s')=true -> (Equal s s').
Lemma subset_1: (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))
(Subset s s') -> (subset s s')=true.
Lemma subset_2: (s,s':t)(subset s s')=true -> (Subset s s').
Lemma empty_sort : (Sort empty).
Lemma empty_1 : (Empty empty).
Lemma is_empty_1 : (s:t)(Empty s) -> (is_empty s)=true.
Lemma is_empty_2 : (s:t)(is_empty s)=true -> (Empty s).
Lemma elements_1: (s:t)(x:elt)(In x s) -> (InList E.eq x (elements s)).
Lemma elements_2: (s:t)(x:elt)(InList E.eq x (elements s)) -> (In x s).
Lemma elements_3: (s:t)(Hs:(Sort s))(sort E.lt (elements s)).
Lemma min_elt_1: (s:t)(x:elt)(min_elt s) = (Some ? x) -> (In x s).
Lemma min_elt_2: (s:t)(Hs:(Sort s))(x,y:elt)
(min_elt s) = (Some ? x) -> (In y s) -> ~(E.lt y x).
Lemma min_elt_3: (s:t)(min_elt s) = (None ?) -> (Empty s).
Lemma max_elt_1: (s:t)(x:elt)(max_elt s) = (Some ? x) -> (In x s).
Lemma max_elt_2: (s:t)(Hs:(Sort s))(x,y:elt)
(max_elt s) = (Some ? x) -> (In y s) -> ~(E.lt x y).
Lemma max_elt_3: (s:t)(max_elt s) = (None ?) -> (Empty s).
Definition choose_1:
(s:t)(x:elt)(choose s)=(Some ? x) -> (In x s)
:= min_elt_1.
Definition choose_2: (s:t)(choose s)=(None ?) -> (Empty s)
:= min_elt_3.
Lemma fold_1 :
(s:t)(Hs:(Sort s))(A:Set)(i:A)(f:elt->A->A)
(EX l:(list elt) | (Unique E.eq l) /\
((x:elt)(In x s)<->(InList E.eq x l)) /\ (fold f s i)=(fold_right f i l)).
Lemma cardinal_1 :
(s:t)(Hs:(Sort s))(EX l:(list elt) | (Unique E.eq l) /\
((x:elt)(In x s)<->(InList E.eq x l)) /\ (cardinal s)=(length l)).
Lemma filter_Inf :
(s:t)(Hs:(Sort s))(x:elt)(f:elt->bool)(Inf x s) -> (Inf x (filter f s)).
Lemma filter_sort : (s:t)(Hs:(Sort s))(f:elt->bool)(Sort (filter f s)).
Lemma filter_1: (s:t)(x:elt)(f:elt->bool)(compat_bool E.eq f) ->
(In x (filter f s)) -> (In x s).
Lemma filter_2:
(s:t)(x:elt)(f:elt->bool)(compat_bool E.eq f) ->(In x (filter f s)) ->
(f x)=true.
Lemma filter_3:
(s:t)(x:elt)(f:elt->bool)(compat_bool E.eq f) ->
(In x s) -> (f x)=true -> (In x (filter f s)).
Lemma for_all_1:
(s:t)(f:elt->bool)(compat_bool E.eq f) ->
(For_all [x](f x)=true s) -> (for_all f s)=true.
Lemma for_all_2:
(s:t)(f:elt->bool)(compat_bool E.eq f) -> (for_all f s)=true ->
(For_all [x](f x)=true s).
Lemma exists_1:
(s:t)(f:elt->bool)(compat_bool E.eq f) -> (Exists [x](f x)=true s) ->
(exists f s)=true.
Lemma exists_2:
(s:t)(f:elt->bool)(compat_bool E.eq f) -> (exists f s)=true ->
(Exists [x](f x)=true s).
Lemma partition_Inf_1 :
(s:t)(Hs:(Sort s))(f:elt->bool)(x:elt)(Inf x s) ->
(Inf x (fst ? ? (partition f s))).
Lemma partition_Inf_2 :
(s:t)(Hs:(Sort s))(f:elt->bool)(x:elt)(Inf x s) ->
(Inf x (snd ? ? (partition f s))).
Lemma partition_sort_1 : (s:t)(Hs:(Sort s))(f:elt->bool)
(Sort (fst ? ? (partition f s))).
Lemma partition_sort_2 : (s:t)(Hs:(Sort s))(f:elt->bool)
(Sort (snd ? ? (partition f s))).
Lemma partition_1:
(s:t)(f:elt->bool)(compat_bool E.eq f) ->
(Equal (fst ? ? (partition f s)) (filter f s)).
Lemma partition_2:
(s:t)(f:elt->bool)(compat_bool E.eq f) ->
(Equal (snd ? ? (partition f s)) (filter [x](negb (f x)) s)).
Definition eq : t -> t -> Prop := Equal.
Lemma eq_sym: (s,s':t)(eq s s') -> (eq s' s).
Lemma eq_trans: (s,s',s'':t)(eq s s') -> (eq s' s'') -> (eq s s'').
Inductive lt : t -> t -> Prop :=
lt_nil : (x:elt)(s:t)(lt [] (x::s))
| lt_cons_lt : (x,y:elt)(s,s':t)(E.lt x y) -> (lt (x::s) (y::s'))
| lt_cons_eq : (x,y:elt)(s,s':t)(E.eq x y) -> (lt s s') -> (lt (x::s) (y::s')).
Hint lt := Constructors lt.
Lemma lt_trans : (s,s',s'':t)(lt s s') -> (lt s' s'') -> (lt s s'').
Lemma lt_not_eq : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(lt s s') -> ~(eq s s').
Definition compare : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(Compare lt eq s s').
End Raw.
Encapsulation
Now, in order to really provide a functor implementing |
Module Make [X:OrderedType] <: S with Module E := X.
Module E := X.
Module Raw := (Raw X).
Record slist : Set := { this :> Raw.t ; sorted : (sort E.lt this) }.
Definition t := slist.
Definition elt := X.t.
Definition In := [x:elt;s:t](Raw.In x s).
Definition Equal := [s,s'](a:elt)(In a s)<->(In a s').
Definition Subset := [s,s'](a:elt)(In a s)->(In a s').
Definition Add := [x:elt;s,s':t](y:elt)(In y s') <-> ((E.eq y x)\/(In y s)).
Definition Empty := [s](a:elt)~(In a s).
Definition For_all := [P:elt->Prop; s:t](x:elt)(In x s)->(P x).
Definition Exists := [P:elt->Prop; s:t](EX x:elt | (In x s)/\(P x)).
Definition In_1 := [s:t](!Raw.In_eq s).
Definition mem := [x:elt;s:t](Raw.mem x s).
Definition mem_1 := [s:t](Raw.mem_1 (sorted s)).
Definition mem_2 := [s:t](!Raw.mem_2 s).
Definition add := [x,s](Build_slist (Raw.add_sort (sorted s) x)).
Definition add_1 := [s:t](Raw.add_1 (sorted s)).
Definition add_2 := [s:t](Raw.add_2 (sorted s)).
Definition add_3 := [s:t](Raw.add_3 (sorted s)).
Definition remove := [x,s](Build_slist (Raw.remove_sort (sorted s) x)).
Definition remove_1 := [s:t](Raw.remove_1 (sorted s)).
Definition remove_2 := [s:t](Raw.remove_2 (sorted s)).
Definition remove_3 := [s:t](Raw.remove_3 (sorted s)).
Definition singleton := [x](Build_slist (Raw.singleton_sort x)).
Definition singleton_1 := Raw.singleton_1.
Definition singleton_2 := Raw.singleton_2.
Definition union := [s,s':t](Build_slist (Raw.union_sort (sorted s) (sorted s'))).
Definition union_1 := [s,s':t](Raw.union_1 (sorted s) (sorted s')).
Definition union_2 := [s,s':t](Raw.union_2 (sorted s) (sorted s')).
Definition union_3 := [s,s':t](Raw.union_3 (sorted s) (sorted s')).
Definition inter :=[s,s':t](Build_slist (Raw.inter_sort (sorted s) (sorted s'))).
End Make.