This module provides support for bindings, which are association
lists for which the keys are ordered and without duplicates.
Bindings are used as a representation for records and environments.
Require Import List.
Require Import ListSet.
Require Import Sumbool.
Require Import Arith.
Require Import Bool.
Require Import Permutation.
Require Import Equivalence.
Require Import EquivDec.
Require Import RelationClasses.
Require Import Orders.
Require Import Permutation.
Require Import LibUtilsCoqLibAdd.
Require Import LibUtilsListAdd.
Require Import LibUtilsSortingAdd.
Require Import LibUtilsAssoc.
Require Import LibUtilsSublist.
Require Import LibUtilsCompat.
Require Import String.
Require Import LibUtilsStringAdd.
Section Bindings.
Class ODT {
K:
Type}
:=
mkODT {
ODT_eqdec:>
EqDec K eq;
ODT_lt:
K ->
K ->
Prop;
ODT_lt_strorder:>
StrictOrder ODT_lt;
ODT_lt_dec:
forall (
a b:
K), {
ODT_lt a b} + {~
ODT_lt a b};
ODT_compare:
K ->
K ->
comparison;
ODT_compare_spec:
forall x y :
K,
CompareSpec (
eq x y) (
ODT_lt x y) (
ODT_lt y x) (
ODT_compare x y) }.
Generalizable Variables K.
Context `{
odt:@
ODT K}.
Lemma ODT_lt_irr (
k:
K) :
~(
ODT_lt k k).
Proof.
Ltac dest_strlt :=
match goal with
| [|-
context [
ODT_lt_dec ?
x ?
y]] =>
destruct (
ODT_lt_dec x y);
simpl
| [
H:
ODT_lt ?
x ?
x|-
_] => (
assert False by (
apply (
ODT_lt_irr x);
auto);
contradiction)
end.
Lemma trichotemy a b : {
ODT_lt a b} + {
eq a b} + {
ODT_lt b a}.
Proof.
generalize (
ODT_compare_spec a b);
intros nc.
destruct (
ODT_compare a b); [
left;
right|
left;
left|
right];
inversion nc;
trivial.
Defined.
Lemma compare_refl_eq a:
ODT_compare a a =
Eq.
Proof.
Lemma compare_eq_iff x y : (
ODT_compare x y) =
Eq <->
x=
y.
Proof.
Lemma ODT_lt_contr (
x y :
K) : ~
ODT_lt x y -> ~
ODT_lt y x ->
x =
y.
Proof.
destruct (
trichotemy x y)
as [[?|?]|?];
intuition.
Qed.
Definition rec_field_lt {
A} (
a b:
K*
A) :=
ODT_lt (
fst a) (
fst b).
Global Instance rec_field_lt_strict {
A} :
StrictOrder (@
rec_field_lt A).
Proof.
Lemma rec_field_lt_dec {
A} (
a b:
K*
A) :
{
rec_field_lt a b} + {~
rec_field_lt a b}.
Proof.
Lemma rec_field_lt_irr {
A} (
a:
K*
A) :
~(
rec_field_lt a a).
Proof.
Lemma Forall_rec_field_lt {
A} (
a:
K*
A)
l :
Forall (
rec_field_lt a)
l <->
Forall (
ODT_lt (
fst a)) (
domain l).
Proof.
destruct a; simpl.
induction l; simpl.
- intuition.
- destruct IHl as [H1 H2].
split; inversion 1; subst; constructor; eauto.
Qed.
Definition rec_cons_sort {
A} :=
@
insertion_sort_insert (
K*
A)
rec_field_lt rec_field_lt_dec.
Definition rec_sort {
A} :=
@
insertion_sort (
K*
A)
rec_field_lt rec_field_lt_dec.
Definition rec_concat_sort {
A} (
l1 l2:
list (
K*
A)) : (
list (
K*
A)) :=
rec_sort (
l1++
l2).
Lemma sorted_rec_nil {
A} :
is_list_sorted ODT_lt_dec (@
domain K A nil) =
true.
Proof.
reflexivity.
Qed.
Lemma sort_rec_single_type {
A} (
k:
K) (
a:
A):
is_list_sorted ODT_lt_dec (
domain ((
k,
a)::
nil)) =
true.
Proof.
reflexivity.
Defined.
Lemma field_less_is_neq (
a1 a2:
K) :
ODT_lt a1 a2 ->
a1 <>
a2.
Proof.
unfold not;
intros.
subst;
dest_strlt.
Qed.
Lemma field_less_is_not_more (
a1 a2:
K) :
ODT_lt a1 a2 -> ~(
ODT_lt a2 a1).
Proof.
Lemma field_not_less_and_neq_is_more (
a1 a2:
K) :
~(
ODT_lt a1 a2) -> ~(
eq a1 a2) ->
ODT_lt a2 a1.
Proof.
unfold not;
intros.
generalize (
ODT_compare_spec a1 a2).
intros.
inversion H1.
congruence.
assert False.
apply H.
assumption.
contradiction.
assumption.
Qed.
Lemma rec_cons_lt {
A} (
l1:
list (
K*
A)) (
a1 a2:
K*
A) :
is_list_sorted ODT_lt_dec (
domain (
a2 ::
l1)) =
true ->
ODT_lt (
fst a1) (
fst a2) ->
is_list_sorted ODT_lt_dec (
domain (
a1 ::
a2 ::
l1)) =
true.
Proof.
simpl;
intros.
revert H0;
elim (
ODT_lt_dec (
fst a1) (
fst a2));
intros.
assumption.
contradiction.
Qed.
Lemma rec_sorted_skip_first {
A} (
l1:
list (
K*
A)) (
a:
K*
A) :
is_list_sorted ODT_lt_dec (
domain (
a ::
l1)) =
true ->
is_list_sorted ODT_lt_dec (
domain l1) =
true.
Proof.
simpl.
intros.
revert H;
elim (
domain l1);
intros.
reflexivity.
destruct (
ODT_lt_dec (
fst a)
a0);
congruence.
Qed.
Lemma rec_sorted_skip_second {
A} (
l:
list (
K*
A)) (
a1 a2:
K*
A) :
is_list_sorted ODT_lt_dec (
domain (
a1 ::
a2 ::
l)) =
true ->
is_list_sorted ODT_lt_dec (
domain (
a1 ::
l)) =
true.
Proof.
Lemma rec_sorted_skip_third {
A} (
l:
list (
K*
A)) (
a1 a2 a3:
K*
A) :
is_list_sorted ODT_lt_dec (
domain (
a1 ::
a2 ::
a3 ::
l)) =
true ->
is_list_sorted ODT_lt_dec (
domain (
a1 ::
a2 ::
l)) =
true.
Proof.
Lemma rec_sorted_distinct {
A} (
l:
list (
K*
A)) (
a1 a2:
K*
A) :
is_list_sorted ODT_lt_dec (
domain (
a1 ::
a2 ::
l)) =
true ->
(
fst a1) <> (
fst a2).
Proof.
Lemma rec_sorted_lt {
A} (
l:
list (
K*
A)) (
a1 a2:
K*
A) :
is_list_sorted ODT_lt_dec (
domain (
a1 ::
a2 ::
l)) =
true ->
ODT_lt (
fst a1) (
fst a2).
Proof.
simpl.
elim (
ODT_lt_dec (
fst a1) (
fst a2));
intros.
assumption.
congruence.
Qed.
Lemma sorted_cons_in {
A} (
l:
list (
K*
A)) (
a a':
K*
A) :
is_list_sorted ODT_lt_dec (
domain (
a ::
l)) =
true ->
In a'
l ->
ODT_lt (
fst a) (
fst a').
Proof.
Lemma rec_cons_lt_first {
A} (
l1:
list (
K*
A)) (
a1 a2:
K*
A) :
is_list_sorted ODT_lt_dec (
domain (
a2 ::
l1)) =
true ->
ODT_lt (
fst a1) (
fst a2) ->
rec_cons_sort a1 (
a2 ::
l1) = (
a1 ::
a2 ::
l1).
Proof.
Lemma sort_sorted_is_id {
A} (
l:
list (
K*
A)) :
is_list_sorted ODT_lt_dec (
domain l) =
true ->
rec_sort l =
l.
Proof.
Lemma rec_concat_sort_concats {
A} (
l1 l2:
list (
K*
A)) :
rec_concat_sort l1 l2 =
rec_sort (
l1++
l2).
Proof.
reflexivity.
Qed.
Lemma rec_cons_sorted_id {
A} (
l:
list (
K*
A)) (
a:
K*
A) :
is_list_sorted ODT_lt_dec (
domain (
a ::
l)) =
true ->
rec_cons_sort a l =
a::
l.
Proof.
Lemma rec_sorted_id {
A} (
l:
list (
K*
A)) :
is_list_sorted ODT_lt_dec (
domain l) =
true ->
rec_sort l =
l.
Proof.
Lemma rec_cons_gt_first {
A} (
l'
l:
list (
K*
A)) (
a1 a2:
K*
A) :
rec_cons_sort a1 l =
l' ->
is_list_sorted ODT_lt_dec (
domain (
a2 ::
l)) =
true ->
ODT_lt (
fst a2) (
fst a1) ->
(
exists a3,
exists l'',
rec_cons_sort a1 l = (
a3 ::
l'')
/\
ODT_lt (
fst a2) (
fst a3)).
Proof.
revert a1 a2 l'.
induction l;
intros.
-
simpl in *;
intros;
exists a1,
nil;
split; [
reflexivity|
assumption].
-
simpl in *.
revert H;
elim (
rec_field_lt_dec a1 a);
intros.
inversion H.
exists a1,(
a::
l).
split; [
reflexivity|
assumption].
revert H;
elim (
rec_field_lt_dec a a1);
intros.
destruct l';
try congruence.
rewrite H in *.
exists p,
l'.
+
split;
try reflexivity.
inversion H.
rewrite <-
H3 in *;
clear H3.
revert H0.
elim (
ODT_lt_dec (
fst a2) (
fst a));
intros.
assumption.
congruence.
+
exists a,
l.
split.
reflexivity.
revert H0.
elim (
ODT_lt_dec (
fst a2) (
fst a));
intros.
assumption.
congruence.
Qed.
Lemma rec_cons_sorted {
A} (
l1 l2:
list (
K*
A)) (
a:
K*
A) :
is_list_sorted ODT_lt_dec (
domain l1) =
true ->
rec_cons_sort a l1 =
l2 ->
is_list_sorted ODT_lt_dec (
domain l2) =
true.
Proof.
Lemma rec_sort_sorted {
A} (
l1 l2:
list (
K*
A)) :
rec_sort l1 =
l2 ->
is_list_sorted ODT_lt_dec (
domain l2) =
true.
Proof.
revert l2.
induction l1;
intros.
simpl;
inversion H;
reflexivity.
simpl in *.
assert (
exists l'',
rec_sort l1 =
l'').
revert H.
elim (
rec_sort l1);
intros.
exists nil;
reflexivity.
exists (
a0::
l);
reflexivity.
elim H0;
intros;
clear H0.
rewrite H1 in H.
assert (
is_list_sorted ODT_lt_dec (
domain x) =
true).
apply (
IHl1 x H1);
assumption.
apply (
rec_cons_sorted x l2 a);
assumption.
Qed.
Lemma rec_sort_pf {
A} {
l1:
list (
K*
A)} :
is_list_sorted ODT_lt_dec (
domain (
rec_sort l1)) =
true.
Proof.
Lemma rec_concat_sort_sorted {
A} (
l1 l2 x:
list (
K*
A)) :
rec_concat_sort l1 l2 =
x ->
is_list_sorted ODT_lt_dec (
domain x) =
true.
Proof.
Lemma same_domain_same_sorted {
A} {
B} (
l1:
list (
K*
A)) (
l2:
list (
K*
B)) :
domain l1 =
domain l2 ->
is_list_sorted ODT_lt_dec (
domain l1) =
true ->
is_list_sorted ODT_lt_dec (
domain l2) =
true.
Proof.
intros.
rewrite <- H; assumption.
Qed.
Lemma same_domain_insert {
A} {
B}
(
l1:
list (
K*
A)) (
l2:
list (
K*
B))
(
a:
K*
A) (
b:
K*
B):
domain l1 =
domain l2 ->
fst a =
fst b ->
domain (
rec_cons_sort a l1) =
domain (
rec_cons_sort b l2).
Proof.
intros.
revert l2 H.
induction l1.
induction l2;
simpl in *;
congruence.
intros;
simpl in *.
induction l2;
simpl in *;
try congruence.
clear IHl2.
inversion H.
elim (
rec_field_lt_dec a a0);
intros.
elim (
rec_field_lt_dec b a1);
intros.
simpl.
rewrite H2;
rewrite H0;
rewrite H3;
reflexivity.
unfold rec_field_lt in *.
destruct a;
destruct a0;
destruct b;
destruct a1;
simpl in *.
subst.
congruence.
unfold rec_field_lt in *.
destruct a;
destruct a0;
destruct b;
destruct a1;
simpl in *.
subst.
inversion H.
destruct (
ODT_lt_dec k1 k2);
try congruence.
destruct (
ODT_lt_dec k2 k1);
try congruence;
simpl.
-
rewrite (
IHl1 l2 H1);
reflexivity.
-
rewrite H1;
reflexivity.
Qed.
Lemma same_domain_rec_sort {
A} {
B}
(
l1:
list (
K*
A)) (
l2:
list (
K*
B)) :
domain l1 =
domain l2 ->
domain (
rec_sort l1) =
domain (
rec_sort l2).
Proof.
Lemma insertion_sort_insert_nin_perm {
A:
Type}
l a :
~
In (
fst a) (@
domain _ A l) ->
Permutation (
a::
l) (
insertion_sort_insert rec_field_lt_dec a l).
Proof.
Lemma insertion_sort_perm_proper {
A:
Type} (
l l':
list (
K*
A))
a :
~
In (
fst a) (
domain l) ->
Permutation l l' ->
Permutation
(
insertion_sort_insert rec_field_lt_dec a l)
(
insertion_sort_insert rec_field_lt_dec a l').
Proof.
Lemma rec_sort_perm {
A:
Type}
l :
NoDup (@
domain _ A l) ->
Permutation l (
rec_sort l).
Proof.
Lemma insertion_sort_insert_insertion_nin {
A} (
a:
K*
A)
a0 l :
~
rec_field_lt a0 a ->
~
rec_field_lt a a0 ->
insertion_sort_insert rec_field_lt_dec a0
(
insertion_sort_insert rec_field_lt_dec a l)
=
insertion_sort_insert rec_field_lt_dec a l.
Proof.
Lemma insertion_sort_insert_cons_app {
A} (
a:
K*
A)
l l2 :
insertion_sort rec_field_lt_dec (
insertion_sort_insert rec_field_lt_dec a l ++
l2) =
insertion_sort rec_field_lt_dec (
a::
l ++
l2).
Proof.
Lemma insertion_sort_insertion_sort_app1 {
A}
l1 l2 :
insertion_sort rec_field_lt_dec (
insertion_sort (@
rec_field_lt_dec A)
l1 ++
l2) =
insertion_sort rec_field_lt_dec (
l1 ++
l2).
Proof.
Lemma insertion_sort_insertion_sort_app {
A}
l1 l2 l3 :
insertion_sort rec_field_lt_dec (
l1 ++
insertion_sort (@
rec_field_lt_dec A)
l2 ++
l3) =
insertion_sort rec_field_lt_dec (
l1 ++
l2 ++
l3).
Proof.
Lemma insertion_sort_eq_app1 {
A l1 l1'}
l2 :
insertion_sort (@
rec_field_lt_dec A)
l1 =
insertion_sort rec_field_lt_dec l1' ->
insertion_sort rec_field_lt_dec (
l1 ++
l2) =
insertion_sort rec_field_lt_dec (
l1' ++
l2).
Proof.
Lemma rec_sort_rec_sort_app1 {
A}
l1 l2 :
rec_sort ((@
rec_sort A)
l1 ++
l2) =
rec_sort (
l1 ++
l2).
Proof.
Lemma rec_sort_rec_sort_app {
A}
l1 l2 l3 :
rec_sort (
l1 ++ (@
rec_sort A)
l2 ++
l3) =
rec_sort (
l1 ++
l2 ++
l3).
Proof.
Lemma rec_sort_rec_sort_app2 {
A}
l1 l2 :
rec_sort (
l1 ++ (@
rec_sort A)
l2) =
rec_sort (
l1 ++
l2).
Proof.
Lemma rec_sort_eq_app1 {
A l1 l1'}
l2 :
(@
rec_sort A)
l1 =
rec_sort l1' ->
rec_sort (
l1 ++
l2) =
rec_sort (
l1' ++
l2).
Proof.
Lemma rec_cons_sort_Forall2 {
A B}
P l1 l2 a b :
Forall2 P l1 l2 ->
P a b ->
(
domain l1) = (
domain l2) ->
fst a =
fst b ->
Forall2 P
(
insertion_sort_insert (@
rec_field_lt_dec A)
a l1)
(
insertion_sort_insert (@
rec_field_lt_dec B)
b l2).
Proof.
Lemma rec_sort_Forall2 {
A B}
P l1 l2 :
(
domain l1) = (
domain l2) ->
Forall2 P l1 l2 ->
Forall2 P (@
rec_sort A l1) (@
rec_sort B l2).
Proof.
Lemma rec_concat_sort_nil_r {
A}
g :
@
rec_concat_sort A g nil =
rec_sort g.
Proof.
Lemma rec_concat_sort_nil_l {
A}
g :
@
rec_concat_sort A nil g =
rec_sort g.
Proof.
Lemma drec_sort_idempotent {
A}
l : @
rec_sort A (
rec_sort l) =
rec_sort l.
Proof.
Lemma insertion_sort_insert_equiv_domain {
A:
Type}
x a (
l:
list (
K*
A)) :
In x
(
domain (
LibUtilsSortingAdd.insertion_sort_insert rec_field_lt_dec a l)) <->
fst a =
x \/
In x (
domain l).
Proof.
induction l;
simpl; [
intuition|].
destruct a;
destruct a0;
simpl in *.
destruct (
ODT_lt_dec k k0);
simpl; [
intuition|].
destruct (
ODT_lt_dec k0 k);
simpl;
intuition.
subst;
clear H.
destruct (
trichotemy x k0);
intuition.
Qed.
Lemma drec_sort_equiv_domain {
A}
l :
equivlist (
domain (@
rec_sort A l)) (
domain l).
Proof.
Hint Resolve ODT_lt_strorder :
fml.
Lemma insertion_sort_insert_swap_neq {
A}
a1 (
b1:
A)
a2 b2 l :
~(
eq a1 a2) ->
insertion_sort_insert rec_field_lt_dec (
a1,
b1)
(
insertion_sort_insert rec_field_lt_dec
(
a2,
b2)
l) =
insertion_sort_insert rec_field_lt_dec (
a2,
b2)
(
insertion_sort_insert rec_field_lt_dec
(
a1,
b1)
l).
Proof.
revert a1 b1 a2 b2.
induction l;
simpl;
intros.
-
destruct (
ODT_lt_dec a1 a2);
destruct (
ODT_lt_dec a2 a1);
trivial.
+
eelim @
asymmetry;
eauto.
unfold Asymmetric;
intros.
apply (@
asymmetry _ _ _ x y);
assumption.
+
destruct (
trichotemy a1 a2)
as [[?|?]|?];
intuition.
-
destruct a;
simpl.
Ltac t :=
try (
solve[
eelim @
asymmetry;
eauto]);
intuition.
repeat dest_strlt;
intuition;
try solve[
rewrite o0 in *;
t
|
destruct (
trichotemy a1 a2)
as [[?|?]|?];
intuition].
rewrite o0 in o2.
dest_strlt.
rewrite IHl; [
reflexivity|
assumption].
Qed.
Lemma insertion_sort_insert_middle {
A}
l1 l2 a (
b:
A) :
~
In a (
domain l1) ->
LibUtilsSortingAdd.insertion_sort_insert rec_field_lt_dec (
a,
b)
(
LibUtilsSortingAdd.insertion_sort rec_field_lt_dec (
l1 ++
l2)) =
LibUtilsSortingAdd.insertion_sort rec_field_lt_dec (
l1 ++ (
a,
b) ::
l2).
Proof.
revert l2 a b.
induction l1;
simpl;
trivial;
intros.
intuition.
rewrite <-
IHl1;
auto.
destruct a;
simpl in *.
apply insertion_sort_insert_swap_neq;
auto.
Qed.
Lemma drec_sort_perm_eq {
A}
l l' :
NoDup (@
domain _ A l) ->
Permutation l l' ->
rec_sort l =
rec_sort l'.
Proof.
Lemma drec_sorted_perm_eq {
A :
Type} (
l l' :
list (
K *
A)) :
is_list_sorted ODT_lt_dec (
domain l) =
true ->
is_list_sorted ODT_lt_dec (
domain l') =
true ->
Permutation l l' ->
l =
l'.
Proof.
Lemma drec_concat_sort_app_comm {
A}
l l':
NoDup (@
domain _ A (
l ++
l')) ->
rec_concat_sort l l' =
rec_concat_sort l'
l.
Proof.
Lemma in_dom_rec_sort {
B} {
l x}:
In x (
domain (
rec_sort l)) <->
In x (@
domain _ B l).
Proof.
Lemma drec_sort_sorted {
A}
l :
LibUtilsSortingAdd.is_list_sorted ODT_lt_dec
(@
domain _ A
(
rec_sort l)) =
true.
Proof.
Lemma drec_concat_sort_sorted {
A}
l l' :
LibUtilsSortingAdd.is_list_sorted ODT_lt_dec
(@
domain _ A
(
rec_concat_sort l l')) =
true.
Proof.
Lemma drec_sort_drec_sort_concat {
A}
l l' :
(
rec_sort (@
rec_concat_sort A l l')) =
rec_concat_sort l l'.
Proof.
Lemma assoc_lookupr_insertion_sort_insert_neq {
B:
Type}
a x (
b:
B)
l :
~(
eq x a)->
assoc_lookupr ODT_eqdec
(
LibUtilsSortingAdd.insertion_sort_insert rec_field_lt_dec (
a,
b)
l)
x
=
assoc_lookupr ODT_eqdec l x.
Proof.
Lemma assoc_lookupr_insertion_sort_fresh {
B:
Type}
x (
d:
B)
b :
~
In x (
domain b) ->
assoc_lookupr ODT_eqdec
(
LibUtilsSortingAdd.insertion_sort rec_field_lt_dec (
b ++ (
x,
d) ::
nil))
x =
Some d.
Proof.
Lemma is_list_sorted_NoDup_strlt {
A}
l :
is_list_sorted ODT_lt_dec (@
domain _ A l) =
true ->
NoDup (
domain l).
Proof.
Lemma rec_sort_self_cons_middle {
A} (
l:
list (
K*
A)) (
a:
K*
A):
is_list_sorted ODT_lt_dec (
domain (
a::
l)) =
true ->
rec_sort (
l ++
a ::
l) =
rec_sort ((
a ::
l) ++
l).
Proof.
Lemma rec_field_anti {
A}
a:
~ (@
rec_field_lt A)
a a.
Proof.
Lemma lt_not_not k1 k2:
~
ODT_lt k1 k2 -> ~
ODT_lt k2 k1 ->
eq k1 k2.
Proof.
unfold not;
intros.
generalize (
trichotemy k1 k2);
intros.
inversion H1.
elim H2;
intros.
congruence.
assumption.
congruence.
Qed.
Lemma rec_concat_sort_self {
A} (
l:
list (
K*
A)):
is_list_sorted ODT_lt_dec (
domain l) =
true ->
rec_concat_sort l l =
l.
Proof.
Lemma insert_first_into_app {
A} (
l l0:
list (
K*
A)) (
a:
K*
A):
is_list_sorted ODT_lt_dec (
domain (
a ::
l)) =
true ->
rec_sort (
l ++
insertion_sort_insert rec_field_lt_dec a (
rec_sort (
l ++
l0))) =
insertion_sort_insert rec_field_lt_dec a (
rec_sort (
l ++
rec_sort (
l ++
l0))).
Proof.
Lemma rec_concat_sort_idem {
A} (
l l0:
list (
K*
A)):
is_list_sorted ODT_lt_dec (
domain l) =
true ->
is_list_sorted ODT_lt_dec (
domain l0) =
true ->
rec_concat_sort l (
rec_concat_sort l l0) =
rec_concat_sort l l0.
Proof.
Instance In_equivlist_proper {
A}:
Proper (
eq ==>
equivlist ==>
iff) (@
In A).
Proof.
Lemma assoc_lookupr_insert B s (
d:
B)
l x :
assoc_lookupr ODT_eqdec
(
LibUtilsSortingAdd.insertion_sort_insert rec_field_lt_dec (
s,
d)
l)
x =
match assoc_lookupr ODT_eqdec l x with
|
Some d' =>
Some d'
|
None =>
if ODT_eqdec x s then Some d else None
end.
Proof.
Lemma assoc_lookupr_drec_sort {
A}
l x :
assoc_lookupr ODT_eqdec (@
rec_sort A l)
x =
assoc_lookupr ODT_eqdec l x.
Proof.
revert x.
induction l;
simpl;
trivial;
intros.
destruct a;
simpl.
rewrite assoc_lookupr_insert,
IHl.
trivial.
Qed.
Lemma assoc_lookupr_drec_sort_app_nin {
A}
l l'
x:
~
In x (
domain l') ->
assoc_lookupr ODT_eqdec (@
rec_sort A (
l ++
l'))
x
=
assoc_lookupr ODT_eqdec (
rec_sort l)
x.
Proof.
Lemma insertion_sort_insert_domain {
B:
Type}
x a (
b:
B)
l :
In x (
domain
(
LibUtilsSortingAdd.insertion_sort_insert rec_field_lt_dec
(
a,
b)
l)) ->
a =
x \/
In x (
domain l).
Proof.
revert x a b.
induction l;
simpl;
intuition.
destruct (
ODT_lt_dec a a0);
simpl in *; [
intuition|].
destruct (
ODT_lt_dec a0 a);
simpl in *; [|
intuition].
intuition.
destruct (
IHl _ _ _ H0);
auto.
Qed.
Lemma drec_sort_domain {
A}
x l :
In x (
domain (@
rec_sort A l)) ->
In x (
domain l).
Proof.
Lemma drec_concat_sort_pullout {
A}
b x xv y yv :
NoDup (
x::
y::(
domain b)) ->
(@
rec_concat_sort A (
rec_concat_sort b ((
x,
xv) ::
nil))
((
y,
yv) ::
nil))
=
(
rec_concat_sort (
rec_concat_sort b ((
y,
yv) ::
nil))
((
x,
xv) ::
nil)).
Proof.
Lemma sorted_cons_filter_in_domain {
A} (
l l':
list (
K*
A))
f a :
filter f l =
a ::
l' ->
In a l.
Proof.
induction l; intros.
simpl in H; congruence.
simpl in *.
destruct (f a0).
- inversion H; left; reflexivity.
- right; apply (IHl H).
Qed.
Lemma filter_choice {
A} (
l:
list(
K*
A))
f:
filter f l =
nil \/ (
exists a,
exists l',
filter f l =
a ::
l').
Proof.
induction l.
left;
reflexivity.
simpl in *.
elim IHl;
clear IHl;
intros.
rewrite H.
destruct (
f a).
right;
exists a;
exists nil;
reflexivity.
left;
reflexivity.
elim H;
clear H;
intros.
elim H;
clear H;
intros.
rewrite H.
destruct (
f a).
right;
exists a;
exists (
x ::
x0);
reflexivity.
right;
exists x;
exists x0;
reflexivity.
Qed.
Lemma sorted_over_filter {
A} (
l:
list (
K*
A))
f:
is_list_sorted ODT_lt_dec (
domain l) =
true ->
is_list_sorted ODT_lt_dec (
domain (
filter f l)) =
true.
Proof.
intros.
induction l.
reflexivity.
simpl.
case_eq (
f a);
intros.
-
generalize (
filter_choice l f);
intros.
elim H1;
clear H1;
intros.
+
rewrite H1 in *.
reflexivity.
+
elim H1;
clear H1;
intros.
elim H1;
clear H1;
intros.
rewrite H1 in *.
assert (
In x l)
by (
apply (
sorted_cons_filter_in_domain l x0 f);
assumption).
assert (
ODT_lt (
fst a) (
fst x))
by (
apply (
sorted_cons_in l a x);
assumption).
apply rec_cons_lt.
apply IHl.
simpl in H.
destruct (
domain l).
reflexivity.
destruct (
ODT_lt_dec (
fst a)
k);
try congruence;
assumption.
assumption.
-
apply IHl.
simpl in H.
destruct (
domain l).
reflexivity.
destruct (
ODT_lt_dec (
fst a)
k).
assumption.
congruence.
Qed.
Lemma rec_sort_insert_filter_fst_true {
A:
Type}
f
(
a:
K*
A) (
l:
list (
K*
A))
(
fstonly:
forall a b c,
f (
a,
b) =
f (
a,
c)) :
StronglySorted rec_field_lt l ->
f a =
true ->
filter f (
insertion_sort_insert rec_field_lt_dec a l)
=
insertion_sort_insert rec_field_lt_dec a (
filter f l).
Proof.
revert a.
induction l;
simpl;
intros b lsort fb.
-
rewrite fb;
trivial.
-
inversion lsort;
subst.
case_eq (
f a);
simpl;
intros fa.
+
destruct (
rec_field_lt_dec b a);
simpl.
*
rewrite fb.
simpl.
match_destr.
*
rewrite <-
IHl;
trivial.
match_destr;
simpl;
rewrite fa;
trivial.
+
match_destr.
*
simpl.
rewrite fb,
fa.
rewrite insertion_sort_insert_forall_lt;
trivial.
apply Forall_filter.
revert H2.
apply Forall_impl_in;
intros.
etransitivity;
eauto.
*
rewrite <-
IHl;
trivial.
match_destr;
simpl;
rewrite fa;
trivial.
unfold rec_field_lt in *.
destruct (
trichotemy (
fst a) (
fst b))
as [[?|?]|?];
try congruence.
destruct a;
destruct b;
simpl in *;
subst.
specialize (
fstonly k0 a a0).
congruence.
Qed.
Lemma rec_sort_insert_filter_fst_false {
A:
Type}
f
(
a:
K*
A) (
l:
list (
K*
A))
(
fstonly:
forall a b c,
f (
a,
b) =
f (
a,
c)) :
f a =
false ->
filter f (
insertion_sort_insert rec_field_lt_dec a l) =
filter f l.
Proof.
revert a.
induction l; simpl; intros ? fa.
- rewrite fa; trivial.
- match_destr; simpl.
+ rewrite fa; trivial.
+ match_destr; simpl.
rewrite IHl; trivial.
Qed.
Lemma rec_sort_filter_fst_commute {
A:
Type}
f (
l:
list (
K*
A))
(
fstonly:
forall a b c,
f (
a,
b) =
f (
a,
c)) :
filter f (
rec_sort l)
=
rec_sort (
filter f l).
Proof.
Lemma forallb_rec_sort {
A}
f (
l:
list (
K*
A)) :
forallb f l =
true ->
forallb f (
rec_sort l) =
true.
Proof.
Lemma forallb_rec_sort_inv {
A}
f (
l:
list (
K*
A)) :
NoDup (
domain l) ->
forallb f (
rec_sort l) =
true ->
forallb f l =
true.
Proof.
Lemma domain_rec_sort_insert {
B} (
a:
K*
B)
l :
domain (
insertion_sort_insert rec_field_lt_dec a l) =
insertion_sort_insert ODT_lt_dec (
fst a) (
domain l).
Proof.
revert a.
induction l; simpl; trivial; intros.
destruct a; destruct a0.
simpl.
match_destr.
match_destr.
simpl. rewrite IHl; trivial.
Qed.
Lemma domain_rec_sort {
B} (
l:
list (
K*
B)) :
domain (
rec_sort l) =
insertion_sort ODT_lt_dec (
domain l).
Proof.
Lemma is_list_sorted_domain_rec_field {
B} (
l:
list (
K*
B)) :
is_list_sorted rec_field_lt_dec l
=
is_list_sorted ODT_lt_dec (
domain l).
Proof.
induction l; simpl; trivial.
match_destr.
destruct a; destruct p; simpl.
match_destr.
Qed.
Lemma rec_sort_insert_in_dom {
B}
a (
l:
list (
K*
B)) :
In (
fst a) (
domain l) ->
is_list_sorted ODT_lt_dec (
domain l) =
true ->
insertion_sort_insert rec_field_lt_dec a l =
l.
Proof.
induction l.
-
intuition.
-
intros.
destruct a;
destruct a0;
simpl.
simpl in H.
destruct H.
+
subst.
match_destr.
apply ODT_lt_irr in o.
intuition.
+
rewrite IHl;
trivial.
{
match_destr.
-
assert (
is_list_sorted ODT_lt_dec (
domain ((
k,
b)::(
k0,
b0) ::
l)) =
true).
+
simpl;
match_destr;
intuition.
+
eapply is_list_sorted_NoDup_strlt in H1.
simpl in H1.
inversion H1;
subst.
elim H4.
simpl;
intuition.
-
match_destr.
}
apply is_list_sorted_cons_inv in H0;
trivial.
Qed.
Lemma in_rec_sort_insert {
A} `{
EqDec A eq} (
x:
K*
A) (
k:
K) (
a:
A)
l:
In x (
insertion_sort_insert rec_field_lt_dec (
k,
a)
l) ->
x = (
k,
a) \/
In x l.
Proof.
revert x a.
induction l;
simpl; [
intuition | ].
intros x a0.
destruct a;
simpl in *.
destruct (
ODT_lt_dec k k0);
simpl;
intros;
trivial.
-
elim H0;
clear H0;
intros; [
left|];
auto.
-
destruct (
ODT_lt_dec k0 k);
simpl;
intros;
intuition.
simpl in H0.
elim H0;
clear H0;
intros.
+
intuition.
+
destruct (
IHl _ _ H0);
intuition.
Qed.
Lemma rec_sort_filter_latter_from_former {
B}
s (
l1 l2:
list (
K*
B)) :
In s (
domain l2) ->
rec_sort (
l1 ++
l2) =
rec_sort (
filter (
fun x :
K *
B =>
s <>
b fst x)
l1 ++
l2).
Proof.
Section Forall.
Lemma Forall_sorted {
A} (
P:(
K*
A) ->
Prop) (
l:
list (
K*
A)):
Forall P l ->
Forall P (
rec_sort l).
Proof.
End Forall.
Section CompatSort.
Lemma compatible_app_compatible {
A} `{
EqDec A eq} {
l1 l2:
list (
K*
A)} :
is_list_sorted ODT_lt_dec (
domain l1) =
true ->
is_list_sorted ODT_lt_dec (
domain l2) =
true ->
compatible l1 l2 =
true ->
compatible (
l1++
l2) (
l1++
l2) =
true.
Proof.
Lemma compatible_asymmetric_over {
A} `{
EqDec A eq} {
l:
list(
K*
A)} :
compatible l l =
true ->
asymmetric_over rec_field_lt l.
Proof.
Lemma compatible_sort_equivlist {
A} `{
EqDec A eq} {
l:
list(
K*
A)} :
compatible l l =
true ->
equivlist l (
rec_sort l).
Proof.
End CompatSort.
Section sublist.
Lemma sublist_rec_concat_sort_bounded {
A}
r srl :
incl (
domain r) (
domain srl) ->
domain (@
rec_concat_sort A r srl) =
domain (
rec_sort srl).
Proof.
Lemma domain_rec_concat_sort_app_comm:
forall (
A :
Type) (
l l' :
list (
K *
A)),
domain (
rec_concat_sort l l') =
domain (
rec_concat_sort l'
l).
Proof.
Lemma incl_sort_sublist {
A B}
a b :
incl (@
domain _ A a) (@
domain _ B b) ->
sublist (
domain (
rec_sort a)) (
domain (
rec_sort b)).
Proof.
Lemma rec_concat_sort_sublist {
B}
l1 l2 :
sublist (@
domain _ B (
rec_sort l1)) (
domain (
rec_concat_sort l1 l2)).
Proof.
Lemma rec_concat_sort_sublist_sorted {
B}
l1 l2 :
is_list_sorted ODT_lt_dec (
domain l1) =
true ->
sublist (@
domain _ B l1) (
domain (
rec_concat_sort l1 l2)).
Proof.
End sublist.
Global Instance assoc_lookupr_equiv_rec_sort {
A :
Type} :
Proper (
assoc_lookupr_equiv ==>
assoc_lookupr_equiv) (@
rec_sort A).
Proof.
Section rev.
Lemma lookup_rev_rec_sort {
B} (
x:
K) (
l:
list (
K*
B)) :
lookup ODT_eqdec (
rev (
rec_sort l))
x =
lookup ODT_eqdec (
rec_sort l)
x.
Proof.
End rev.
Lemma insertion_sort_nin_inv {
B} (
s:
K) (
x₁:
B)
l₁
x₂
l₂:
~
In s (
domain l₁) ->
~
In s (
domain l₂) ->
insertion_sort_insert rec_field_lt_dec (
s,
x₁)
l₁ =
insertion_sort_insert rec_field_lt_dec (
s,
x₂)
l₂ ->
x₁ =
x₂ /\
l₁ =
l₂.
Proof.
Lemma rec_sort_cons_nin_inv {
B} (
s:
K) (
x₁:
B)
l₁
x₂
l₂:
~
In s (
domain l₁) ->
~
In s (
domain l₂) ->
rec_sort ((
s,
x₁) ::
l₁) =
rec_sort ((
s,
x₂) ::
l₂) ->
x₁ =
x₂ /\
rec_sort l₁ =
rec_sort l₂.
Proof.
Lemma domains_with_map {
A B} (
r:
list (
string*
A)) (
f:
A->
B):
domain (
map (
fun x :
string *
A => (
fst x,
f (
snd x)))
r) =
domain r.
Proof.
induction r. reflexivity.
simpl.
rewrite IHr; reflexivity.
Qed.
End Bindings.
Section Map.
Lemma map_rec_sort {
A B C D} `{
odta:
ODT A} `{
odtb:
ODT B} (
f:
A*
C->
B*
D) (
l:
list(
A*
C))
(
consistent:
forall x y,
rec_field_lt x y <->
rec_field_lt (
f x) (
f y)) :
map f (
rec_sort l) =
rec_sort (
map f l).
Proof.
Lemma no_assoc_with_map {
A B} (
r:
list (
string*
A)) (
f:
A->
B) (
s:
string):
assoc_lookupr string_dec r s =
None ->
assoc_lookupr string_dec (
map (
fun x => (
fst x,
f (
snd x)))
r)
s =
None.
Proof.
intros.
induction r.
reflexivity.
destruct a;
simpl in *.
case_eq (
assoc_lookupr string_dec r s);
intros.
rewrite H0 in H;
congruence.
rewrite H0 in H.
rewrite (
IHr H0).
destruct (
string_dec s s0);
congruence.
Qed.
Lemma assoc_lookupr_skip {
A} (
a:
string*
A) (
l:
list (
string*
A)) (
s:
string):
assoc_lookupr string_dec (
a::
l)
s =
None ->
assoc_lookupr string_dec l s =
None.
Proof.
End Map.
Section BindingsString.
Global Program Instance ODT_string : (@
ODT string)
:=
mkODT _ _ StringOrder.lt _ StringOrder.lt_dec StringOrder.compare StringOrder.compare_spec.
End BindingsString.
Section Edot.
Definition edot {
A} (
r:
list (
string*
A)) (
a:
string) :
option A :=
assoc_lookupr ODT_eqdec r a.
Lemma edot_nodup_perm {
A:
Type} (
l l':
list (
string*
A))
x :
NoDup (
domain l) ->
Permutation l l' ->
edot l x =
edot l'
x.
Proof.
Lemma edot_fresh_concat_right_single {
A}
x (
d:
A)
b :
edot (
rec_concat_sort b ((
x,
d)::
nil))
x =
Some d.
Proof.
Lemma edot_concat_right {
A}
x (
d:
A)
b c :
edot c x =
Some d ->
edot (
rec_concat_sort b c)
x =
Some d.
Proof.
End Edot.
Hint Unfold rec_sort rec_concat_sort :
fml.
Hint Resolve drec_sort_sorted drec_concat_sort_sorted :
fml.
Hint Resolve is_list_sorted_NoDup_strlt :
fml.
Section MergeBindings.
Definition merge_bindings {
A} `{
EqDec A eq} (
l₁
l₂:
list (
string *
A)) :
option (
list (
string *
A)) :=
if compatible l₁
l₂
then Some (
rec_concat_sort l₁
l₂)
else None.
Lemma merge_bindings_nil_l {
A} `{
EqDec A eq}
l :
merge_bindings nil l =
Some (
rec_sort l).
Proof.
Lemma merge_bindings_nil_r {
A} `{
EqDec A eq}
l :
merge_bindings l nil =
Some (
rec_sort l).
Proof.
Lemma merge_bindings_single_nin {
A} `{
EqDec A eq}
b x d :
~
In x (
domain b) ->
merge_bindings b ((
x,
d)::
nil) =
Some (
rec_concat_sort b ((
x,
d)::
nil)).
Proof.
Lemma merge_bindings_sorted {
A} `{
EqDec A eq} {
g g1 g2} :
Some g =
merge_bindings g1 g2 ->
is_list_sorted ODT_lt_dec (@
domain string A g) =
true.
Proof.
Lemma edot_merge_bindings {
A} `{
EqDec A eq} (
l1 l2:
list (
string*
A)) (
s:
string) (
x:
A) :
merge_bindings l1 ((
s,
x)::
nil) =
Some l2 ->
edot l2 s =
Some x.
Proof.
Lemma merge_bindings_nodup {
A} `{
EqDec A eq} (
l l0 l1:
list (
string*
A)):
merge_bindings l l0 =
Some l1 ->
NoDup (
domain l1).
Proof.
Lemma merge_bindings_compatible {
A} `{
EqDec A eq} (
l l0 l1:
list (
string*
A)):
merge_bindings l l0 =
Some l1 ->
compatible l l0 =
true.
Proof.
Lemma sorted_cons_is_compatible {
A} `{
EqDec A eq} (
l:
list (
string*
A)) (
a:
string*
A):
is_list_sorted ODT_lt_dec (
domain (
a ::
l)) =
true ->
compatible_with (
fst a) (
snd a)
l =
true.
Proof.
Lemma compatible_self {
A} `{
EqDec A eq} (
l:
list (
string*
A)):
is_list_sorted ODT_lt_dec (
domain l) =
true ->
compatible l l =
true.
Proof.
Lemma merge_self_sorted {
A} `{
EqDec A eq} (
l:
list (
string*
A)):
is_list_sorted ODT_lt_dec (
domain l) =
true ->
merge_bindings l l =
Some l.
Proof.
Lemma merge_self_sorted_r {
A} `{
EqDec A eq} (
l:
list (
string*
A)):
is_list_sorted ODT_lt_dec (
domain l) =
true ->
merge_bindings l (
rec_sort l) =
Some (
rec_sort l).
Proof.
Lemma same_domain_merge_bindings_eq
{
A} `{
EqDec A eq} (
l₁
l₂
l₃:
list (
string*
A)) :
NoDup (
domain l₁) ->
domain l₁ =
domain l₂ ->
merge_bindings l₁
l₂ =
Some l₃ ->
l₁ =
l₂.
Proof.
Definition compatible {
A:
Type} `{
x:
EqDec A eq} := @
compatible string A _ _ _ _.
Lemma merge_returns_compatible {
A} `{
equiv:
EqDec A eq} (
l1 l2 l3:
list (
string*
A)):
is_list_sorted ODT_lt_dec (
domain l1) =
true ->
is_list_sorted ODT_lt_dec (
domain l2) =
true ->
compatible l1 l2 =
true ->
rec_concat_sort l1 l2 =
l3 ->
compatible l1 l3 =
true.
Proof.
Lemma merge_idem {
A} `{
EqDec A eq} (
l l0 l1:
list (
string*
A)):
is_list_sorted ODT_lt_dec (
domain l) =
true ->
is_list_sorted ODT_lt_dec (
domain l0) =
true ->
merge_bindings l l0 =
Some l1 ->
merge_bindings l l1 =
Some l1.
Proof.
End MergeBindings.
Section RecProject.
Import ListNotations.
Definition rproject {
A} (
l:
list (
string*
A)) (
s:
list string) :
list (
string*
A) :=
filter (
fun x =>
if in_dec string_dec (
fst x)
s then true else false)
l.
Lemma rproject_nil_l {
A} (
s:
list string) :
@
rproject A []
s = [].
Proof.
reflexivity.
Qed.
Lemma rproject_nil_r {
A} (
l:
list (
string*
A)) :
@
rproject A l [] = [].
Proof.
induction l. reflexivity.
simpl. apply IHl.
Qed.
Lemma rproject_rec_sort_commute {
B} (
l1:
list (
string*
B))
sl:
rproject (
rec_sort l1)
sl =
rec_sort (
rproject l1 sl).
Proof.
Lemma rproject_map_fst_same {
B C} (
f:
string*
B->
string*
C) (
l:
list (
string*
B))
sl
(
samedom:
forall a,
In a l ->
fst (
f a) =
fst a) :
rproject (
map f l)
sl =
map f (
rproject l sl).
Proof.
induction l;
simpl;
trivial.
simpl in samedom.
destruct (
in_dec string_dec (
fst (
f a))
sl);
destruct (
in_dec string_dec (
fst a)
sl).
-
rewrite IHl;
intuition.
-
rewrite samedom in i;
intuition.
-
rewrite <-
samedom in i;
intuition.
-
rewrite IHl;
intuition.
Qed.
Lemma rproject_app {
B} (
l1 l2:
list (
string*
B))
sl:
rproject (
l1 ++
l2)
sl = (
rproject l1 sl) ++ (
rproject l2 sl).
Proof.
Lemma rproject_rproject {
B} (
l:
list (
string*
B))
sl1 sl2:
rproject (
rproject l sl2)
sl1 =
rproject l (
set_inter string_dec sl2 sl1).
Proof.
Lemma rproject_Forall2_same_domain {
B C}
P (
l1:
list(
string*
B)) (
l2:
list (
string*
C))
ls :
Forall2 P l1 l2 ->
domain l1 =
domain l2 ->
Forall2 P (
rproject l1 ls) (
rproject l2 ls).
Proof.
unfold rproject;
intros.
apply filter_Forall2_same;
trivial.
revert H0;
clear.
revert l2.
induction l1;
destruct l2;
simpl;
trivial;
try discriminate.
inversion 1.
rewrite H1.
match_destr;
f_equal;
auto.
Qed.
Lemma sublist_rproject {
A} (
l:
list(
string*
A))
sl:
sublist (
rproject l sl)
l.
Proof.
Lemma rproject_remove_all {
B}
s sl (
l1:
list(
string*
B)):
rproject l1 (
remove_all s sl) =
filter (
fun x =>
nequiv_decb s (
fst x)) (
rproject l1 sl).
Proof.
Lemma rec_sort_rproject_remove_all_in {
B}
s sl l1 l2 :
In s sl ->
In s (@
domain _ B l2) ->
rec_sort (
rproject l1 sl ++
l2) =
rec_sort (
rproject l1 (
remove_all s sl) ++
l2).
Proof.
Lemma rec_sort_rproject_remove_in {
B}
s sl l1 l2 :
In s sl ->
In s (@
domain _ B l2) ->
rec_sort (
rproject l1 sl ++
l2) =
rec_sort (
rproject l1 (
remove string_dec s sl) ++
l2).
Proof.
Lemma rproject_with_lookup {
A} (
l1 l2:
list (
string *
A)) (
s:
list string):
is_list_sorted ODT_lt_dec (
domain l1) =
true ->
is_list_sorted ODT_lt_dec (
domain l2) =
true ->
sublist l1 l2 ->
(
forall x,
In x s ->
assoc_lookupr string_dec l1 x =
assoc_lookupr string_dec l2 x) ->
rproject l1 s =
rproject l2 s.
Proof.
Lemma rproject_sublist {
A} (
l1 l2:
list (
string *
A)) (
s:
list string) :
is_list_sorted ODT_lt_dec (
domain l1) =
true ->
is_list_sorted ODT_lt_dec (
domain l2) =
true ->
sublist s (
domain l1) ->
sublist l1 l2 ->
rproject l1 s =
rproject l2 s.
Proof.
Lemma rproject_equivlist {
B} (
l:
list (
string*
B))
sl1 sl2 :
equivlist sl1 sl2 ->
rproject l sl1 =
rproject l sl2.
Proof.
induction l;
simpl;
trivial.
intros eqq.
rewrite (
IHl eqq).
destruct (
in_dec string_dec (
fst a)
sl1);
destruct (
in_dec string_dec (
fst a)
sl2);
trivial.
-
apply eqq in i;
intuition.
-
apply eqq in i;
intuition.
Qed.
Lemma rproject_sortfilter {
B} (
l:
list (
string*
B))
sl1 :
rproject l (
insertion_sort ODT_lt_dec sl1) =
rproject l sl1.
Proof.
Lemma rproject_concat_dist {
A} (
l1 l2:
list (
string *
A)) (
s:
list string) :
rproject (
rec_concat_sort l1 l2)
s =
rec_concat_sort (
rproject l1 s) (
rproject l2 s).
Proof.
Lemma rproject_domain_in {
A}
s (
l1:
list (
string*
A))
l2 :
In s (
domain l1) /\
In s l2 <->
In s (
domain (
rproject l1 l2)).
Proof.
split;
intros.
-
destruct H as [
inn1 inn2].
unfold rproject.
apply in_domain_in in inn1.
destruct inn1 as [
x inn1].
apply (
in_dom (
b:=
x)).
apply filter_In;
split;
trivial;
simpl.
match_destr.
tauto.
-
apply in_domain_in in H.
destruct H as [
x inn].
unfold rproject in inn.
apply filter_In in inn.
simpl in inn.
destruct inn as [
inn1 inn2].
match_destr_in inn2.
split;
trivial.
eapply in_dom;
eauto.
Qed.
End RecProject.
Section RecRemove.
Definition rremove {
A} (
l:
list (
string*
A)) (
s:
string) :
list (
string*
A) :=
filter (
fun x =>
if string_dec s (
fst x)
then false else true)
l.
Lemma is_sorted_rremove {
A} (
l:
list (
string *
A)) (
s:
string):
is_list_sorted ODT_lt_dec (
domain l) =
true ->
is_list_sorted ODT_lt_dec (
domain (
rremove l s)) =
true.
Proof.
Lemma domain_rremove {
A}
s (
l:
list (
string*
A)) :
domain (
rremove l s) =
remove_all s (
domain l).
Proof.
Lemma rremove_rec_sort_commute {
B} (
l1:
list (
string*
B))
s:
rremove (
rec_sort l1)
s =
rec_sort (
rremove l1 s).
Proof.
Lemma rremove_app {
B} (
l1 l2:
list (
string*
B))
s:
rremove (
l1 ++
l2)
s =
rremove l1 s ++
rremove l2 s.
Proof.
Lemma nin_rremove {
B} (
l:
list (
string*
B))
s :
~
In s (
domain l) ->
rremove l s =
l.
Proof.
intros nin.
apply true_filter;
intros ?
inn.
destruct x.
apply in_dom in inn.
simpl.
match_destr.
congruence.
Qed.
End RecRemove.
Hint Resolve merge_bindings_sorted :
fml.