diff options
author | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-09 14:56:11 +0000 |
---|---|---|
committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-09 14:56:11 +0000 |
commit | a3d58682b063dcf56c3712562a0263822bfac30b (patch) | |
tree | dafb24cea08f1d19073e366b5bd914151193250d /theories/MSets/MSetList.v | |
parent | ee540c98da75419c877d7c5444fa9487d8e67da7 (diff) |
Change definition of FSetList so that equality is Leibniz
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12913 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/MSets/MSetList.v')
-rw-r--r-- | theories/MSets/MSetList.v | 166 |
1 files changed, 121 insertions, 45 deletions
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v index d46803d75..0414e6eda 100644 --- a/theories/MSets/MSetList.v +++ b/theories/MSets/MSetList.v @@ -214,7 +214,19 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Section ForNotations. - Notation Sort := (sort X.lt). + Definition inf x l := + match l with + | nil => true + | y::_ => match X.compare x y with Lt => true | _ => false end + end. + + Fixpoint isok l := + match l with + | nil => true + | x::l => inf x l && isok l + end. + + Notation Sort l := (isok l = true). Notation Inf := (lelistA X.lt). Notation In := (InA X.eq). @@ -223,7 +235,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Hint Immediate (@Equivalence_Symmetric _ _ X.eq_equiv). Hint Resolve (@Equivalence_Transitive _ _ X.eq_equiv). - Definition IsOk := Sort. + Definition IsOk s := Sort s. Class Ok (s:t) : Prop := ok : Sort s. @@ -232,10 +244,48 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Instance Sort_Ok s `(Hs : Sort s) : Ok s := { ok := Hs }. + Lemma inf_iff : forall x l, Inf x l <-> inf x l = true. + Proof. + intros x l; split; intro H. + (* -> *) + destruct H; simpl in *. + reflexivity. + rewrite <- compare_lt_iff in H; rewrite H; reflexivity. + (* <- *) + destruct l as [|y ys]; simpl in *. + constructor; fail. + revert H; case_eq (X.compare x y); try discriminate; []. + intros Ha _. + rewrite compare_lt_iff in Ha. + constructor; assumption. + Qed. + + Lemma isok_iff : forall l, sort X.lt l <-> Ok l. + Proof. + intro l; split; intro H. + (* -> *) + elim H. + constructor; fail. + intros y ys Ha Hb Hc. + change (inf y ys && isok ys = true). + rewrite inf_iff in Hc. + rewrite andb_true_iff; tauto. + (* <- *) + induction l as [|x xs]. + constructor. + change (inf x xs && isok xs = true) in H. + rewrite andb_true_iff, <- inf_iff in H. + destruct H; constructor; tauto. + Qed. + + Hint Extern 1 (Ok _) => rewrite <- isok_iff. + Ltac inv_ok := match goal with - | H:Ok (_ :: _) |- _ => inversion_clear H; inv_ok - | H:Ok nil |- _ => clear H; inv_ok - | H:Sort ?l |- _ => change (Ok l) in H; inv_ok + | H:sort X.lt (_ :: _) |- _ => inversion_clear H; inv_ok + | H:sort X.lt nil |- _ => clear H; inv_ok + | H:sort X.lt ?l |- _ => change (Ok l) in H; inv_ok + | H:Ok _ |- _ => rewrite <- isok_iff in H; inv_ok + | |- Ok _ => rewrite <- isok_iff | _ => idtac end. @@ -248,42 +298,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X. | _ => fail end. - Definition inf x l := - match l with - | nil => true - | y::_ => match X.compare x y with Lt => true | _ => false end - end. - - Fixpoint isok l := - match l with - | nil => true - | x::l => inf x l && isok l - end. - - Lemma inf_iff : forall x l, Inf x l <-> inf x l = true. - Proof. - induction l as [ | y l IH]. - simpl; split; auto. - simpl. - elim_compare x y; intuition; try discriminate. - inv; order. - inv; order. - Qed. - - Lemma isok_iff : forall l, Ok l <-> isok l = true. - Proof. - induction l as [ | x l IH]. - simpl; split; auto; constructor. - simpl. - rewrite andb_true_iff, <- inf_iff, <- IH. - split. - intros; inv; auto. - constructor; intuition. - Qed. - Global Instance isok_Ok s `(isok s = true) : Ok s | 10. Proof. - intros. apply <- isok_iff. auto. + intros. assumption. Qed. Definition Equal s s' := forall a : elt, In a s <-> In a s'. @@ -295,7 +312,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Lemma mem_spec : forall (s : t) (x : elt) (Hs : Ok s), mem x s = true <-> In x s. Proof. - induction s; intros; inv; simpl. + induction s; intros x Hs; inv; simpl. intuition. discriminate. inv. elim_compare x a; rewrite InA_cons; intuition; try order. discriminate. @@ -315,6 +332,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Global Instance add_ok s x `(Ok s) : Ok (add x s). Proof. + intros s x; repeat rewrite <- isok_iff; revert s x. simple induction s; simpl. intuition. intros; elim_compare x a; inv; auto. @@ -342,6 +360,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Global Instance remove_ok s x `(Ok s) : Ok (remove x s). Proof. + intros s x; repeat rewrite <- isok_iff; revert s x. induction s; simpl. intuition. intros; elim_compare x a; inv; auto. @@ -384,6 +403,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Global Instance union_ok s s' `(Ok s, Ok s') : Ok (union s s'). Proof. + intros s s'; repeat rewrite <- isok_iff; revert s s'. induction2; constructors; try apply @ok; auto. apply Inf_eq with x'; auto; apply union_inf; auto; apply Inf_eq with x; auto. change (Inf x' (union (x :: l) l')); auto. @@ -410,6 +430,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Global Instance inter_ok s s' `(Ok s, Ok s') : Ok (inter s s'). Proof. + intros s s'; repeat rewrite <- isok_iff; revert s s'. induction2. constructors; auto. apply Inf_eq with x'; auto; apply inter_inf; auto; apply Inf_eq with x; auto. @@ -428,6 +449,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. forall (s s' : t) (Hs : Ok s) (Hs' : Ok s') (a : elt), Inf a s -> Inf a s' -> Inf a (diff s s'). Proof. + intros s s'; repeat rewrite <- isok_iff; revert s s'. induction2. apply Hrec; trivial. apply Inf_lt with x; auto. @@ -439,7 +461,8 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Global Instance diff_ok s s' `(Ok s, Ok s') : Ok (diff s s'). Proof. - induction2. constructors; auto. + intros s s'; repeat rewrite <- isok_iff; revert s s'. + induction2. Qed. Lemma diff_spec : @@ -524,14 +547,14 @@ Module MakeRaw (X: OrderedType) <: RawSets X. intuition. Qed. - Lemma elements_spec2 : forall (s : t) (Hs : Ok s), Sort (elements s). + Lemma elements_spec2 : forall (s : t) (Hs : Ok s), sort X.lt (elements s). Proof. - auto. + intro s; repeat rewrite <- isok_iff; auto. Qed. Lemma elements_spec2w : forall (s : t) (Hs : Ok s), NoDupA X.eq (elements s). Proof. - auto. + intro s; repeat rewrite <- isok_iff; auto. Qed. Lemma min_elt_spec1 : forall (s : t) (x : elt), min_elt s = Some x -> In x s. @@ -625,6 +648,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Global Instance filter_ok s f `(Ok s) : Ok (filter f s). Proof. + intros s f; repeat rewrite <- isok_iff; revert s f. simple induction s; simpl. auto. intros x l Hrec f Hs; inv. @@ -679,6 +703,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. forall (s : t) (f : elt -> bool) (x : elt) (Hs : Ok s), Inf x s -> Inf x (fst (partition f s)). Proof. + intros s f x; repeat rewrite <- isok_iff; revert s f x. simple induction s; simpl. intuition. intros x l Hrec f a Hs Ha; inv. @@ -692,6 +717,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. forall (s : t) (f : elt -> bool) (x : elt) (Hs : Ok s), Inf x s -> Inf x (snd (partition f s)). Proof. + intros s f x; repeat rewrite <- isok_iff; revert s f x. simple induction s; simpl. intuition. intros x l Hrec f a Hs Ha; inv. @@ -703,6 +729,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Global Instance partition_ok1 s f `(Ok s) : Ok (fst (partition f s)). Proof. + intros s f; repeat rewrite <- isok_iff; revert s f. simple induction s; simpl. auto. intros x l Hrec f Hs; inv. @@ -712,6 +739,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Global Instance partition_ok2 s f `(Ok s) : Ok (snd (partition f s)). Proof. + intros s f; repeat rewrite <- isok_iff; revert s f. simple induction s; simpl. auto. intros x l Hrec f Hs; inv. @@ -767,6 +795,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Proof. split. intros s (s1 & s2 & B1 & B2 & E1 & E2 & L). + repeat rewrite <- isok_iff in *. assert (eqlistA X.eq s1 s2). apply SortA_equivlistA_eqlistA with (ltA:=X.lt); auto using @ok with *. transitivity s; auto. symmetry; auto. @@ -774,7 +803,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X. apply (StrictOrder_Irreflexive s2); auto. intros s1 s2 s3 (s1' & s2' & B1 & B2 & E1 & E2 & L12) (s2'' & s3' & B2' & B3 & E2' & E3 & L23). - exists s1', s3'; do 4 (split; trivial). + exists s1', s3'. + repeat rewrite <- isok_iff in *. + do 4 (split; trivial). assert (eqlistA X.eq s2' s2''). apply SortA_equivlistA_eqlistA with (ltA:=X.lt); auto using @ok with *. transitivity s2; auto. symmetry; auto. @@ -821,3 +852,48 @@ Module Make (X: OrderedType) <: S with Module E := X. Module Raw := MakeRaw X. Include Raw2Sets X Raw. End Make. + +(** For this specific implementation, eq coincides with Leibniz equality *) + +Require Eqdep_dec. + +Module Type OrderedTypeWithLeibniz. + Include OrderedType. + Parameter eq_leibniz : forall x y, eq x y -> x = y. +End OrderedTypeWithLeibniz. + +Module Type SWithLeibniz. + Declare Module E : OrderedTypeWithLeibniz. + Include SetsOn E. + Parameter eq_leibniz : forall x y, eq x y -> x = y. +End SWithLeibniz. + +Module MakeWithLeibniz (X: OrderedTypeWithLeibniz) <: SWithLeibniz with Module E := X. + Module E := X. + Module Raw := MakeRaw X. + Include Raw2SetsOn X Raw. + + Lemma eq_leibniz_list : forall xs ys, eqlistA X.eq xs ys -> xs = ys. + Proof. + induction xs as [|x xs]; intros [|y ys] H; inversion H; [ | ]. + reflexivity. + f_equal. + apply X.eq_leibniz; congruence. + apply IHxs; subst; assumption. + Qed. + + Lemma eq_leibniz : forall s s', eq s s' -> s = s'. + Proof. + intros [xs Hxs] [ys Hys] Heq. + change (equivlistA X.eq xs ys) in Heq. + assert (H : eqlistA X.eq xs ys). + rewrite <- Raw.isok_iff in Hxs, Hys. + apply SortA_equivlistA_eqlistA with X.lt; auto with *. + apply eq_leibniz_list in H. + subst ys. + f_equal. + apply Eqdep_dec.eq_proofs_unicity. + intros x y; destruct (bool_dec x y); tauto. + Qed. + +End MakeWithLeibniz. |