(**************************************************************************) (* *) (* SMTCoq *) (* Copyright (C) 2011 - 2021 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) (* This file is distributed under the terms of the CeCILL-C licence *) (* *) (**************************************************************************) Require Import SetoidList Bool OrderedType OrdersLists RelationPairs Orders. (* Require Import List Bool NArith Psatz Int63. *) Require Import RelationClasses. Class DecType T := { eq_refl : forall x : T, x = x; eq_sym : forall x y : T, x = y -> y = x; eq_trans : forall x y z : T, x = y -> y = z -> x = z; eq_dec : forall x y : T, { x = y } + { x <> y } }. Hint Immediate eq_sym. Hint Resolve eq_refl eq_trans. Class OrdType T := { lt: T -> T -> Prop; lt_trans : forall x y z : T, lt x y -> lt y z -> lt x z; lt_not_eq : forall x y : T, lt x y -> ~ eq x y (* compare : forall x y : T, Compare lt eq x y *) }. Hint Resolve lt_not_eq lt_trans. (* Global Instance Comparable T `(OrdType T) : *) Class Comparable T {ot:OrdType T} := { compare : forall x y : T, Compare lt eq x y }. Set Implicit Arguments. Module Raw. Section Array. Variable key : Type. Variable elt : Type. Variable key_dec : DecType key. Variable key_ord : OrdType key. Variable key_comp : Comparable key. Variable elt_dec : DecType elt. Variable elt_ord : OrdType elt. Definition eqb_key (x y : key) : bool := if eq_dec x y then true else false. Definition eqb_elt (x y : elt) : bool := if eq_dec x y then true else false. Lemma eqb_key_eq x y : eqb_key x y = true <-> x = y. Proof. unfold eqb_key. case (eq_dec x y); split; easy. Qed. Lemma eqb_elt_eq x y : eqb_elt x y = true <-> x = y. Proof. unfold eqb_elt. case (eq_dec x y); split; easy. Qed. Hint Immediate eqb_key_eq eqb_elt_eq. Definition farray := list (key * elt). Definition eqk (a b : (key * elt)) := fst a = fst b. Definition eqe (a b : (key * elt)) := snd a = snd b. Definition eqke (a b : (key * elt)) := fst a = fst b /\ snd a = snd b. Definition ltk (a b : (key * elt)) := lt (fst a) (fst b). (* Definition ltke (a b : (key * elt)) := *) (* lt (fst a) (fst b) \/ ( (fst a) = (fst b) /\ lt (snd a) (snd b)). *) Hint Unfold ltk (* ltke *) eqk eqke. Hint Extern 2 (eqke ?a ?b) => split. Global Instance StrictOrder_OrdType T `(OrdType T) : StrictOrder (lt : T -> T -> Prop). Proof. split. unfold Irreflexive, Reflexive, complement. intros. apply lt_not_eq in H0; auto. unfold Transitive. intros x y z. apply lt_trans. Qed. Check (lt : key -> key -> Prop). Global Instance lt_key_strorder : StrictOrder (lt : key -> key -> Prop). Proof. apply StrictOrder_OrdType. Qed. Global Instance lt_elt_strorder : StrictOrder (lt : elt -> elt -> Prop). Proof. apply StrictOrder_OrdType. Qed. Global Instance ke_dec : DecType (key * elt). Proof. split; auto. intros; destruct x, y, z. inversion H. inversion H0. trivial. intros; destruct x, y. destruct (eq_dec k k0). destruct (eq_dec e e0). left; rewrite e1, e2; auto. right; unfold not in *. intro; inversion H. exact (n H2). right; unfold not in *. intro; inversion H. exact (n H1). Qed. Global Instance ke_ord: OrdType (key * elt). Proof. exists ltk; unfold ltk; intros. apply (lt_trans _ (fst y)); auto. destruct x, y. simpl in H. unfold not. intro. inversion H0. apply (lt_not_eq k k0); auto. Qed. (* ltk ignore the second components *) Lemma ltk_right_r : forall x k e e', ltk x (k,e) -> ltk x (k,e'). Proof. auto. Qed. Lemma ltk_right_l : forall x k e e', ltk (k,e) x -> ltk (k,e') x. Proof. auto. Qed. Hint Immediate ltk_right_r ltk_right_l. Notation Sort := (sort ltk). Notation Inf := (lelistA (ltk)). Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). Definition In k m := exists e:elt, MapsTo k e m. Notation NoDupA := (NoDupA eqk). Hint Unfold MapsTo In. (* Instance ke_ord: OrdType (key * elt). *) (* Proof. *) (* exists ltke. *) (* unfold ltke. intros. *) (* destruct H, H0. *) (* left; apply (lt_trans _ (fst y)); auto. *) (* destruct H0. left. rewrite <- H0. assumption. *) (* destruct H. left. rewrite H. assumption. *) (* destruct H, H0. *) (* right. split. *) (* apply (eq_trans _ (fst y)); trivial. *) (* apply (lt_trans _ (snd y)); trivial. *) (* unfold ltke. intros. *) (* destruct x, y. simpl in H. *) (* destruct H. *) (* apply lt_not_eq in H. *) (* unfold not in *. intro. inversion H0. apply H. trivial. *) (* destruct H. apply lt_not_eq in H0. unfold not in *. intro. *) (* inversion H1. apply H0; trivial. *) (* intros. *) (* unfold ltke. *) (* destruct (compare (fst x) (fst y)). *) (* apply LT. left; assumption. *) (* destruct (compare (snd x) (snd y)). *) (* apply LT. right; split; assumption. *) (* apply EQ. destruct x, y. simpl in *. rewrite e, e0; trivial. *) (* apply GT. right; symmetry in e; split; assumption. *) (* apply GT. left; assumption. *) (* Qed. *) (* Hint Immediate ke_ord. *) (* Let ke_ord := ke_ord. *) (* Instance keyelt_ord: OrdType (key * elt). *) (* Variable keyelt_ord : OrdType (key * elt). *) (* eqke is stricter than eqk *) Lemma eqke_eqk : forall x x', eqke x x' -> eqk x x'. Proof. unfold eqk, eqke; intuition. Qed. (* eqk, eqke are equalities *) Lemma eqk_refl : forall e, eqk e e. Proof. auto. Qed. Lemma eqke_refl : forall e, eqke e e. Proof. auto. Qed. Lemma eqk_sym : forall e e', eqk e e' -> eqk e' e. Proof. auto. Qed. Lemma eqke_sym : forall e e', eqke e e' -> eqke e' e. Proof. unfold eqke; intuition. Qed. Lemma eqk_trans : forall e e' e'', eqk e e' -> eqk e' e'' -> eqk e e''. Proof. eauto. Qed. Lemma eqke_trans : forall e e' e'', eqke e e' -> eqke e' e'' -> eqke e e''. Proof. unfold eqke; intuition; [ eauto | congruence ]. Qed. Lemma ltk_trans : forall e e' e'', ltk e e' -> ltk e' e'' -> ltk e e''. Proof. eauto. Qed. Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'. Proof. unfold ltk, eqk. intros. apply lt_not_eq; auto. Qed. Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'. Proof. unfold eqke, ltk; intuition; simpl in *; subst. apply lt_not_eq in H. auto. Qed. Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl. Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke. Hint Immediate eqk_sym eqke_sym. Global Instance eqk_equiv : Equivalence eqk. Proof. split; eauto. Qed. Global Instance eqke_equiv : Equivalence eqke. Proof. split; eauto. Qed. Global Instance ltk_strorder : StrictOrder ltk. Proof. split. unfold Irreflexive, Reflexive, complement. intros. apply lt_not_eq in H; auto. unfold Transitive. intros x y z. apply lt_trans. Qed. (* Instance ltke_strorder : StrictOrder ltke. *) (* Proof. *) (* split. *) (* unfold Irreflexive, Reflexive, complement. *) (* intros. apply lt_not_eq in H; auto. *) (* unfold Transitive. apply lt_trans. *) (* Qed. *) Global Instance eq_equiv : @Equivalence (key * elt) eq. Proof. split; auto. unfold Transitive. apply eq_trans. Qed. (* Instance ltke_compat : Proper (eq ==> eq ==> iff) ltke. *) (* Proof. *) (* split; rewrite H, H0; trivial. *) (* Qed. *) Global Instance ltk_compat : Proper (eq ==> eq ==> iff) ltk. Proof. split; rewrite H, H0; trivial. Qed. Global Instance ltk_compatk : Proper (eqk==>eqk==>iff) ltk. Proof. intros (x,e) (x',e') Hxx' (y,f) (y',f') Hyy'; compute. compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto. Qed. Global Instance ltk_compat' : Proper (eqke==>eqke==>iff) ltk. Proof. intros (x,e) (x',e') (Hxx',_) (y,f) (y',f') (Hyy',_); compute. compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto. Qed. Global Instance ltk_asym : Asymmetric ltk. Proof. apply (StrictOrder_Asymmetric ltk_strorder). Qed. (* Additional facts *) Lemma eqk_not_ltk : forall x x', eqk x x' -> ~ltk x x'. Proof. unfold eqk, ltk. unfold not. intros x x' H. destruct x, x'. simpl in *. intro. symmetry in H. apply lt_not_eq in H. auto. subst. auto. Qed. Lemma ltk_eqk : forall e e' e'', ltk e e' -> eqk e' e'' -> ltk e e''. Proof. unfold ltk, eqk. destruct e, e', e''. simpl. intros; subst; trivial. Qed. Lemma eqk_ltk : forall e e' e'', eqk e e' -> ltk e' e'' -> ltk e e''. Proof. intros (k,e) (k',e') (k'',e''). unfold ltk, eqk; simpl; intros; subst; trivial. Qed. Hint Resolve eqk_not_ltk. Hint Immediate ltk_eqk eqk_ltk. Lemma InA_eqke_eqk : forall x m, InA eqke x m -> InA eqk x m. Proof. unfold eqke; induction 1; intuition. Qed. Hint Resolve InA_eqke_eqk. (* Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. *) (* Proof. *) (* intros; apply InA_eqA with p; auto with *. *) (* Qed. *) (* Lemma In_eq : forall l x y, eq x y -> InA eqke x l -> InA eqke y l. *) (* Proof. intros. rewrite <- H; auto. Qed. *) (* Lemma ListIn_In : forall l x, List.In x l -> InA eqk x l. *) (* Proof. apply In_InA. split; auto. unfold Transitive. *) (* unfold eqk; intros. rewrite H, <- H0. auto. *) (* Qed. *) (* Lemma Inf_lt : forall l x y, ltk x y -> Inf y l -> Inf x l. *) (* Proof. exact (InfA_ltA ltk_strorder). Qed. *) (* Lemma Inf_eq : forall l x y, x = y -> Inf y l -> Inf x l. *) (* Proof. exact (InfA_eqA eq_equiv ltk_compat). Qed. *) (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *) Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l. Proof. firstorder. exists x; auto. induction H. destruct y. exists e; auto. destruct IHInA as [e H0]. exists e; auto. Qed. Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. Proof. intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto with *. Qed. Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. Proof. destruct 2 as (e,E); exists e; eapply MapsTo_eq; eauto. Qed. Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l. Proof. exact (InfA_eqA eqk_equiv ltk_compatk). Qed. Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l. Proof. exact (InfA_ltA ltk_strorder). Qed. Hint Immediate Inf_eq. Hint Resolve Inf_lt. Lemma Sort_Inf_In : forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p. Proof. exact (SortA_InfA_InA eqk_equiv ltk_strorder ltk_compatk). Qed. Lemma Sort_Inf_NotIn : forall l k e, Sort l -> Inf (k,e) l -> ~In k l. Proof. intros; red; intros. destruct H1 as [e' H2]. elim (@ltk_not_eqk (k,e) (k,e')). eapply Sort_Inf_In; eauto. red; simpl; auto. Qed. Hint Resolve Sort_Inf_NotIn. Lemma Sort_NoDupA: forall l, Sort l -> NoDupA l. Proof. exact (SortA_NoDupA eqk_equiv ltk_strorder ltk_compatk). Qed. Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'. Proof. inversion 1; intros; eapply Sort_Inf_In; eauto. Qed. Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) -> ltk e e' \/ eqk e e'. Proof. inversion_clear 2; auto. left; apply Sort_In_cons_1 with l; auto. Qed. Lemma Sort_In_cons_3 : forall x l k e, Sort ((k,e)::l) -> In x l -> ~eq x k. Proof. inversion_clear 1; red; intros. destruct (Sort_Inf_NotIn H0 H1 (In_eq H2 H)). Qed. Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l. Proof. inversion 1. inversion_clear H0; eauto. destruct H1; simpl in *; intuition. Qed. Lemma In_inv_2 : forall k k' e e' l, InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l. Proof. inversion_clear 1; compute in H0; intuition. Qed. Lemma In_inv_3 : forall x x' l, InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l. Proof. inversion_clear 1; compute in H0; intuition. Qed. Hint Resolve In_inv_2 In_inv_3. (** * FMAPLIST interface implementaion *) (** * [empty] *) Definition empty : farray := nil. Definition Empty m := forall (a : key)(e:elt) , ~ MapsTo a e m. Lemma empty_1 : Empty empty. Proof. unfold Empty,empty. intros a e. intro abs. inversion abs. Qed. Hint Resolve empty_1. Lemma empty_sorted : Sort empty. Proof. unfold empty; auto. Qed. (** * [is_empty] *) Definition is_empty (l : farray) : bool := if l then true else false. Lemma is_empty_1 :forall m, Empty m -> is_empty m = true. Proof. unfold Empty, MapsTo. intros m. case m;auto. intros (k,e) l inlist. absurd (InA eqke (k, e) ((k, e) :: l));auto. Qed. Lemma is_empty_2 : forall m, is_empty m = true -> Empty m. Proof. intros m. case m;auto. intros p l abs. inversion abs. Qed. (** * [mem] *) Function mem (k : key) (s : farray) {struct s} : bool := match s with | nil => false | (k',_) :: l => match compare k k' with | LT _ => false | EQ _ => true | GT _ => mem k l end end. Lemma mem_1 : forall m (Hm:Sort m) x, In x m -> mem x m = true. Proof. intros m Hm x; generalize Hm; clear Hm. functional induction (mem x m);intros sorted belong1;trivial. inversion belong1. inversion H. absurd (In x ((k', _x) :: l));try assumption. apply Sort_Inf_NotIn with _x;auto. apply IHb. elim (sort_inv sorted);auto. elim (In_inv belong1);auto. intro abs. absurd (eq x k'); auto. symmetry in abs. apply lt_not_eq in abs; auto. Qed. Lemma mem_2 : forall m (Hm:Sort m) x, mem x m = true -> In x m. Proof. intros m Hm x; generalize Hm; clear Hm; unfold In,MapsTo. functional induction (mem x m); intros sorted hyp;try ((inversion hyp);fail). exists _x; auto. induction IHb; auto. exists x0; auto. inversion_clear sorted; auto. Qed. (** * [find] *) Function find (k:key) (s: farray) {struct s} : option elt := match s with | nil => None | (k',x)::s' => match compare k k' with | LT _ => None | EQ _ => Some x | GT _ => find k s' end end. Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. Proof. intros m x. unfold MapsTo. functional induction (find x m);simpl;intros e' eqfind; inversion eqfind; auto. Qed. Lemma find_1 : forall m (Hm:Sort m) x e, MapsTo x e m -> find x m = Some e. Proof. intros m Hm x e; generalize Hm; clear Hm; unfold MapsTo. functional induction (find x m);simpl; subst; try clear H_eq_1. inversion 2. inversion_clear 2. clear e1;compute in H0; destruct H0. apply lt_not_eq in H; auto. now contradict H. clear e1;generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute. (* order. *) intros. apply (lt_trans k') in _x; auto. apply lt_not_eq in _x. now contradict _x. clear e1;inversion_clear 2. compute in H0; destruct H0; intuition congruence. generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute. (* order. *) intros. apply lt_not_eq in H. now contradict H. clear e1; do 2 inversion_clear 1; auto. compute in H2; destruct H2. (* order. *) subst. apply lt_not_eq in _x. now contradict _x. Qed. (** * [add] *) Function add (k : key) (x : elt) (s : farray) {struct s} : farray := match s with | nil => (k,x) :: nil | (k',y) :: l => match compare k k' with | LT _ => (k,x)::s | EQ _ => (k,x)::l | GT _ => (k',y) :: add k x l end end. Lemma add_1 : forall m x y e, eq x y -> MapsTo y e (add x e m). Proof. intros m x y e; generalize y; clear y. unfold MapsTo. functional induction (add x e m);simpl;auto. Qed. Lemma add_2 : forall m x y e e', ~ eq x y -> MapsTo y e m -> MapsTo y e (add x e' m). Proof. intros m x y e e'. generalize y e; clear y e; unfold MapsTo. functional induction (add x e' m) ;simpl;auto; clear e0. subst;auto. intros y' e'' eqky'; inversion_clear 1; destruct H0; simpl in *. (* order. *) subst. now contradict eqky'. auto. auto. intros y' e'' eqky'; inversion_clear 1; intuition. Qed. Lemma add_3 : forall m x y e e', ~ eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m. Proof. intros m x y e e'. generalize y e; clear y e; unfold MapsTo. functional induction (add x e' m);simpl; intros. apply (In_inv_3 H0); compute; auto. apply (In_inv_3 H0); compute; auto. constructor 2; apply (In_inv_3 H0); compute; auto. inversion_clear H0; auto. Qed. Lemma add_Inf : forall (m:farray)(x x':key)(e e':elt), Inf (x',e') m -> ltk (x',e') (x,e) -> Inf (x',e') (add x e m). Proof. induction m. simpl; intuition. intros. destruct a as (x'',e''). inversion_clear H. compute in H0,H1. simpl; case (compare x x''); intuition. Qed. Hint Resolve add_Inf. Lemma add_sorted : forall m (Hm:Sort m) x e, Sort (add x e m). Proof. induction m. simpl; intuition. intros. destruct a as (x',e'). simpl; case (compare x x'); intuition; inversion_clear Hm; auto. constructor; auto. apply Inf_eq with (x',e'); auto. Qed. (** * [remove] *) Function remove (k : key) (s : farray) {struct s} : farray := match s with | nil => nil | (k',x) :: l => match compare k k' with | LT _ => s | EQ _ => l | GT _ => (k',x) :: remove k l end end. Lemma remove_1 : forall m (Hm:Sort m) x y, eq x y -> ~ In y (remove x m). Proof. intros m Hm x y; generalize Hm; clear Hm. functional induction (remove x m);simpl;intros;subst. red; inversion 1; inversion H0. apply Sort_Inf_NotIn with x0; auto. clear e0. inversion Hm. subst. apply Sort_Inf_NotIn with x0; auto. (* clear e0;inversion_clear Hm. *) (* apply Sort_Inf_NotIn with x0; auto. *) (* apply Inf_eq with (k',x0);auto; compute; apply eq_trans with x; auto. *) clear e0;inversion_clear Hm. assert (notin:~ In y (remove y l)) by auto. intros (x1,abs). inversion_clear abs. compute in H1; destruct H1. subst. apply lt_not_eq in _x; now contradict _x. apply notin; exists x1; auto. Qed. Lemma remove_2 : forall m (Hm:Sort m) x y e, ~ eq x y -> MapsTo y e m -> MapsTo y e (remove x m). Proof. intros m Hm x y e; generalize Hm; clear Hm; unfold MapsTo. functional induction (remove x m);subst;auto; match goal with | [H: compare _ _ = _ |- _ ] => clear H | _ => idtac end. inversion_clear 3; auto. compute in H1; destruct H1. subst; now contradict H. inversion_clear 1; inversion_clear 2; auto. Qed. Lemma remove_3 : forall m (Hm:Sort m) x y e, MapsTo y e (remove x m) -> MapsTo y e m. Proof. intros m Hm x y e; generalize Hm; clear Hm; unfold MapsTo. functional induction (remove x m);subst;auto. inversion_clear 1; inversion_clear 1; auto. Qed. Lemma remove_Inf : forall (m:farray)(Hm : Sort m)(x x':key)(e':elt), Inf (x',e') m -> Inf (x',e') (remove x m). Proof. induction m. simpl; intuition. intros. destruct a as (x'',e''). inversion_clear H. compute in H0. simpl; case (compare x x''); intuition. inversion_clear Hm. apply Inf_lt with (x'',e''); auto. Qed. Hint Resolve remove_Inf. Lemma remove_sorted : forall m (Hm:Sort m) x, Sort (remove x m). Proof. induction m. simpl; intuition. intros. destruct a as (x',e'). simpl; case (compare x x'); intuition; inversion_clear Hm; auto. Qed. (** * [elements] *) Definition elements (m: farray) := m. Lemma elements_1 : forall m x e, MapsTo x e m -> InA eqke (x,e) (elements m). Proof. auto. Qed. Lemma elements_2 : forall m x e, InA eqke (x,e) (elements m) -> MapsTo x e m. Proof. auto. Qed. Lemma elements_3 : forall m (Hm:Sort m), sort ltk (elements m). Proof. auto. Qed. Lemma elements_3w : forall m (Hm:Sort m), NoDupA (elements m). Proof. intros. apply Sort_NoDupA. apply elements_3; auto. Qed. (** * [fold] *) Function fold (A:Type)(f:key->elt->A->A)(m:farray) (acc:A) {struct m} : A := match m with | nil => acc | (k,e)::m' => fold f m' (f k e acc) end. Lemma fold_1 : forall m (A:Type)(i:A)(f:key->elt->A->A), fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i. Proof. intros; functional induction (fold f m i); auto. Qed. (** * [equal] *) Function equal (cmp:elt->elt->bool)(m m' : farray) {struct m} : bool := match m, m' with | nil, nil => true | (x,e)::l, (x',e')::l' => match compare x x' with | EQ _ => cmp e e' && equal cmp l l' | _ => false end | _, _ => false end. Definition Equivb cmp m m' := (forall k, In k m <-> In k m') /\ (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true). Lemma equal_1 : forall m (Hm:Sort m) m' (Hm': Sort m') cmp, Equivb cmp m m' -> equal cmp m m' = true. Proof. intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'. functional induction (equal cmp m m'); simpl; subst;auto; unfold Equivb; intuition; subst. match goal with H: compare _ _ = _ |- _ => clear H end. assert (cmp_e_e':cmp e e' = true). apply H1 with x; auto. rewrite cmp_e_e'; simpl. apply IHb; auto. inversion_clear Hm; auto. inversion_clear Hm'; auto. unfold Equivb; intuition. destruct (H0 k). assert (In k ((x,e) ::l)). destruct H as (e'', hyp); exists e''; auto. destruct (In_inv (H2 H4)); auto. inversion_clear Hm. elim (Sort_Inf_NotIn H6 H7). destruct H as (e'', hyp); exists e''; auto. apply MapsTo_eq with k; auto. destruct (H0 k). assert (In k ((x,e') ::l')). destruct H as (e'', hyp); exists e''; auto. destruct (In_inv (H3 H4)); auto. subst. inversion_clear Hm'. now elim (Sort_Inf_NotIn H5 H6). apply H1 with k; destruct (eq_dec x k); auto. destruct (compare x x') as [Hlt|Heq|Hlt]; try contradiction; clear y. destruct (H0 x). assert (In x ((x',e')::l')). apply H; auto. exists e; auto. destruct (In_inv H3). (* order. *) apply lt_not_eq in Hlt; now contradict Hlt. inversion_clear Hm'. assert (Inf (x,e) l'). apply Inf_lt with (x',e'); auto. elim (Sort_Inf_NotIn H5 H7 H4). destruct (H0 x'). assert (In x' ((x,e)::l)). apply H2; auto. exists e'; auto. destruct (In_inv H3). (* order. *) subst; apply lt_not_eq in Hlt; now contradict Hlt. inversion_clear Hm. assert (Inf (x',e') l). apply Inf_lt with (x,e); auto. elim (Sort_Inf_NotIn H5 H7 H4). destruct m; destruct m';try contradiction. clear H1;destruct p as (k,e). destruct (H0 k). destruct H1. exists e; auto. inversion H1. destruct p as (x,e). destruct (H0 x). destruct H. exists e; auto. inversion H. destruct p;destruct p0;contradiction. Qed. Lemma equal_2 : forall m (Hm:Sort m) m' (Hm:Sort m') cmp, equal cmp m m' = true -> Equivb cmp m m'. Proof. intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'. functional induction (equal cmp m m'); simpl; subst;auto; unfold Equivb; intuition; try discriminate; subst; try match goal with H: compare _ _ = _ |- _ => clear H end. inversion H0. inversion_clear Hm;inversion_clear Hm'. destruct (andb_prop _ _ H); clear H. destruct (IHb H1 H3 H6). destruct (In_inv H0). exists e'; constructor; split; trivial; apply eq_trans with x; auto. destruct (H k). destruct (H9 H8) as (e'',hyp). exists e''; auto. inversion_clear Hm;inversion_clear Hm'. destruct (andb_prop _ _ H); clear H. destruct (IHb H1 H3 H6). destruct (In_inv H0). exists e; constructor; split; trivial; apply eq_trans with x'; auto. destruct (H k). destruct (H10 H8) as (e'',hyp). exists e''; auto. inversion_clear Hm;inversion_clear Hm'. destruct (andb_prop _ _ H); clear H. destruct (IHb H2 H4 H7). inversion_clear H0. destruct H9; simpl in *; subst. inversion_clear H1. destruct H0; simpl in *; subst; auto. elim (Sort_Inf_NotIn H4 H5). exists e'0; apply MapsTo_eq with x; auto. (* order. *) inversion_clear H1. destruct H0; simpl in *; subst; auto. elim (Sort_Inf_NotIn H2 H3). exists e0; apply MapsTo_eq with x; auto. (* order. *) apply H8 with k; auto. Qed. (** This lemma isn't part of the spec of [Equivb], but is used in [FMapAVL] *) Lemma equal_cons : forall cmp l1 l2 x y, Sort (x::l1) -> Sort (y::l2) -> eqk x y -> cmp (snd x) (snd y) = true -> (Equivb cmp l1 l2 <-> Equivb cmp (x :: l1) (y :: l2)). Proof. intros. inversion H; subst. inversion H0; subst. destruct x; destruct y; compute in H1, H2. split; intros. apply equal_2; auto. simpl. case (compare k k0); subst; intro HH; try (apply lt_not_eq in HH; now contradict HH). rewrite H2; simpl. apply equal_1; auto. apply equal_2; auto. generalize (equal_1 H H0 H3). simpl. case (compare k k0); subst; intro HH; try (apply lt_not_eq in HH; now contradict HH). rewrite H2; simpl; auto. Qed. End Array. End Raw. Section FArray. Variable key : Type. Variable elt : Type. Variable key_dec : DecType key. Variable key_ord : OrdType key. Variable key_comp : Comparable key. Variable elt_dec : DecType elt. Variable elt_ord : OrdType elt. Variable elt_comp : Comparable elt. Set Implicit Arguments. Record slist := {this :> Raw.farray key elt; sorted : sort (Raw.ltk key_ord) this}. Definition farray := slist. (* Boolean comparison over elements *) Definition cmp (e e':elt) := match compare e e' with EQ _ => true | _ => false end. Definition empty : farray := Build_slist (Raw.empty_sorted elt key_ord). Definition is_empty m : bool := Raw.is_empty m.(this). Definition add x e m : farray := Build_slist (Raw.add_sorted key_dec key_comp m.(sorted) x e). Definition find x m : option elt := Raw.find key_comp x m.(this). Definition remove x m : farray := Build_slist (Raw.remove_sorted key_comp m.(sorted) x). Definition mem x m : bool := Raw.mem key_comp x m.(this). Definition elements m : list (key*elt) := Raw.elements m.(this). Definition cardinal m := length m.(this). Definition fold (A:Type)(f:key->elt->A->A) m (i:A) : A := Raw.fold f m.(this) i. Definition equal m m' : bool := Raw.equal key_comp cmp m.(this) m'.(this). Definition MapsTo x e m : Prop := Raw.MapsTo x e m.(this). Definition In x m : Prop := Raw.In x m.(this). Definition Empty m : Prop := Raw.Empty m.(this). Definition Equal m m' := forall y, find y m = find y m'. Definition Equiv m m' := (forall k, In k m <-> In k m') /\ (forall k e e', MapsTo k e m -> MapsTo k e' m' -> e = e'). Definition Equivb m m' : Prop := Raw.Equivb cmp m.(this) m'.(this). Definition eq_key : (key*elt) -> (key*elt) -> Prop := @Raw.eqk key elt. Definition eq_key_elt : (key*elt) -> (key*elt) -> Prop:= @Raw.eqke key elt. Definition lt_key : (key*elt) -> (key*elt) -> Prop := @Raw.ltk key elt key_ord. Lemma MapsTo_1 : forall m x y e, eq x y -> MapsTo x e m -> MapsTo y e m. Proof. intros m. apply (Raw.MapsTo_eq key_dec elt_dec). Qed. Lemma mem_1 : forall m x, In x m -> mem x m = true. Proof. intros m; apply (Raw.mem_1); auto. apply m.(sorted). Qed. Lemma mem_2 : forall m x, mem x m = true -> In x m. Proof. intros m; apply (Raw.mem_2); auto. apply m.(sorted). Qed. Lemma empty_1 : Empty empty. Proof. apply Raw.empty_1. Qed. Lemma is_empty_1 : forall m, Empty m -> is_empty m = true. Proof. intros m; apply Raw.is_empty_1. Qed. Lemma is_empty_2 : forall m, is_empty m = true -> Empty m. Proof. intros m; apply Raw.is_empty_2. Qed. Lemma add_1 : forall m x y e, eq x y -> MapsTo y e (add x e m). Proof. intros m; apply Raw.add_1; auto. Qed. Lemma add_2 : forall m x y e e', ~ eq x y -> MapsTo y e m -> MapsTo y e (add x e' m). Proof. intros m; apply Raw.add_2; auto. Qed. Lemma add_3 : forall m x y e e', ~ eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m. Proof. intros m; apply Raw.add_3; auto. Qed. Lemma remove_1 : forall m x y, eq x y -> ~ In y (remove x m). Proof. intros m; apply Raw.remove_1; auto. apply m.(sorted). Qed. Lemma remove_2 : forall m x y e, ~ eq x y -> MapsTo y e m -> MapsTo y e (remove x m). Proof. intros m; apply Raw.remove_2; auto. apply m.(sorted). Qed. Lemma remove_3 : forall m x y e, MapsTo y e (remove x m) -> MapsTo y e m. Proof. intros m; apply Raw.remove_3; auto. apply m.(sorted). Qed. Lemma find_1 : forall m x e, MapsTo x e m -> find x m = Some e. Proof. intros m; apply Raw.find_1; auto. apply m.(sorted). Qed. Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. Proof. intros m; apply Raw.find_2; auto. Qed. Lemma elements_1 : forall m x e, MapsTo x e m -> InA eq_key_elt (x,e) (elements m). Proof. intros m; apply Raw.elements_1. Qed. Lemma elements_2 : forall m x e, InA eq_key_elt (x,e) (elements m) -> MapsTo x e m. Proof. intros m; apply Raw.elements_2. Qed. Lemma elements_3 : forall m, sort lt_key (elements m). Proof. intros m; apply Raw.elements_3; auto. apply m.(sorted). Qed. Lemma elements_3w : forall m, NoDupA eq_key (elements m). Proof. intros m; apply (Raw.elements_3w key_dec m.(sorted)). Qed. Lemma cardinal_1 : forall m, cardinal m = length (elements m). Proof. intros; reflexivity. Qed. Lemma fold_1 : forall m (A : Type) (i : A) (f : key -> elt -> A -> A), fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i. Proof. intros m; apply Raw.fold_1. Qed. Lemma equal_1 : forall m m', Equivb m m' -> equal m m' = true. Proof. intros m m'; apply Raw.equal_1; auto. apply m.(sorted). apply m'.(sorted). Qed. Lemma equal_2 : forall m m', equal m m' = true -> Equivb m m'. Proof. intros m m'; apply Raw.equal_2; auto. apply m.(sorted). apply m'.(sorted). Qed. Fixpoint eq_list (m m' : list (key * elt)) : Prop := match m, m' with | nil, nil => True | (x,e)::l, (x',e')::l' => match compare x x' with | EQ _ => eq e e' /\ eq_list l l' | _ => False end | _, _ => False end. Definition eq m m' := eq_list m.(this) m'.(this). Lemma eq_equal : forall m m', eq m m' <-> equal m m' = true. Proof. intros (l,Hl); induction l. intros (l',Hl'); unfold eq; simpl. destruct l'; unfold equal; simpl; intuition. intros (l',Hl'); unfold eq. destruct l'. destruct a; unfold equal; simpl; intuition. destruct a as (x,e). destruct p as (x',e'). unfold equal; simpl. destruct (compare x x') as [Hlt|Heq|Hlt]; simpl; intuition. unfold cmp at 1. case (compare e e'); subst; intro HH; try (apply lt_not_eq in HH; now contradict HH); clear HH; simpl. inversion_clear Hl. inversion_clear Hl'. destruct (IHl H (Build_slist H2)). unfold equal, eq in H5; simpl in H5; auto. destruct (andb_prop _ _ H); clear H. generalize H0; unfold cmp. case (compare e e'); subst; intro HH; try (apply lt_not_eq in HH; now contradict HH); auto; intro; discriminate. destruct (andb_prop _ _ H); clear H. inversion_clear Hl. inversion_clear Hl'. destruct (IHl H (Build_slist H3)). unfold equal, eq in H6; simpl in H6; auto. Qed. Lemma eq_1 : forall m m', Equivb m m' -> eq m m'. Proof. intros. generalize (@equal_1 m m'). generalize (@eq_equal m m'). intuition. Qed. Lemma eq_2 : forall m m', eq m m' -> Equivb m m'. Proof. intros. generalize (@equal_2 m m'). generalize (@eq_equal m m'). intuition. Qed. Lemma eqfarray_refl : forall m : farray, eq m m. Proof. intros (m,Hm); induction m; unfold eq; simpl; auto. destruct a. destruct (compare k k) as [Hlt|Heq|Hlt]; auto. apply lt_not_eq in Hlt. auto. split. apply eq_refl. inversion_clear Hm. apply (IHm H). apply lt_not_eq in Hlt. auto. Qed. Lemma eqfarray_sym : forall m1 m2 : farray, eq m1 m2 -> eq m2 m1. Proof. intros (m,Hm); induction m; intros (m', Hm'); destruct m'; unfold eq; simpl; try destruct a as (x,e); try destruct p as (x',e'); auto. destruct (compare x x') as [Hlt|Heq|Hlt]; try easy. inversion_clear Hm; inversion_clear Hm'. intro. destruct H3. subst. case (compare x' x'); subst; intro HH; try (apply lt_not_eq in HH; now contradict HH). split; auto. apply (IHm H (Build_slist H1)); auto. Qed. Lemma eqfarray_trans : forall m1 m2 m3 : farray, eq m1 m2 -> eq m2 m3 -> eq m1 m3. Proof. intros (m1,Hm1); induction m1; intros (m2, Hm2); destruct m2; intros (m3, Hm3); destruct m3; unfold eq; simpl; try destruct a as (x,e); try destruct p as (x',e'); try destruct p0 as (x'',e''); try contradiction; auto. destruct (compare x x') as [Hlt|Heq|Hlt]; destruct (compare x' x'') as [Hlt'|Heq'|Hlt']; try easy. intros; destruct H, H0; subst. case (compare x'' x''); subst; intro HH; try (apply lt_not_eq in HH; now contradict HH). split; auto. inversion_clear Hm1; inversion_clear Hm2; inversion_clear Hm3. apply (IHm1 H (Build_slist H3) (Build_slist H5)); intuition. Qed. Fixpoint lt_list (m m' : list (key * elt)) : Prop := match m, m' with | nil, nil => False | nil, _ => True | _, nil => False | (x,e)::l, (x',e')::l' => match compare x x' with | LT _ => True | GT _ => False | EQ _ => lt e e' \/ (e = e' /\ lt_list l l') end end. Definition lt_farray m m' := lt_list m.(this) m'.(this). Lemma lt_farray_trans : forall m1 m2 m3 : farray, lt_farray m1 m2 -> lt_farray m2 m3 -> lt_farray m1 m3. Proof. intros (m1,Hm1); induction m1; intros (m2, Hm2); destruct m2; intros (m3, Hm3); destruct m3; unfold lt_farray; simpl; try destruct a as (x,e); try destruct p as (x',e'); try destruct p0 as (x'',e''); try contradiction; auto. destruct (compare x x') as [Hlt|Heq|Hlt]; destruct (compare x' x'') as [Hlt'|Heq'|Hlt']; destruct (compare x x'') as [Hlt''|Heq''|Hlt'']; intros; subst; auto; try easy. apply (lt_trans x') in Hlt; apply lt_not_eq in Hlt. now contradict Hlt. auto. apply (lt_trans x') in Hlt; apply lt_not_eq in Hlt. now contradict Hlt. apply (lt_trans _ x'') ; auto. apply lt_not_eq in Hlt. now contradict Hlt. apply (lt_trans x'') in Hlt; apply lt_not_eq in Hlt. now contradict Hlt. auto. subst. apply lt_not_eq in Hlt'. now contradict Hlt'. apply (lt_trans x'') in Hlt'; apply lt_not_eq in Hlt'. now contradict Hlt'. auto. destruct H, H0. left; apply lt_trans with e'; auto. left. destruct H0. subst; auto. left. destruct H. subst; auto. right. destruct H, H0. subst; split; auto. inversion_clear Hm1; inversion_clear Hm2; inversion_clear Hm3. apply (IHm1 H (Build_slist H3) (Build_slist H5)); intuition. apply lt_not_eq in Hlt''. now contradict Hlt''. Qed. Lemma lt_farray_not_eq : forall m1 m2 : farray, lt_farray m1 m2 -> ~ eq m1 m2. Proof. intros (m1,Hm1); induction m1; intros (m2, Hm2); destruct m2; unfold eq, lt; simpl; try destruct a as (x,e); try destruct p as (x',e'); try contradiction; auto. destruct (compare x x') as [Hlt|Heq|Hlt]; auto. intuition. inversion_clear Hm1; inversion_clear Hm2. subst. apply (IHm1 H0 (Build_slist H4)); intuition. unfold lt_farray in *. simpl in H. case (compare x' x') in *. apply lt_not_eq in l. now contradict l. destruct H. apply lt_not_eq in H. now contradict H. destruct H. auto. apply lt_not_eq in l. now contradict l. Qed. Definition compare_farray : forall m1 m2, Compare lt_farray eq m1 m2. Proof. intros (m1,Hm1); induction m1; intros (m2, Hm2); destruct m2; [ apply EQ | apply LT | apply GT | ]; auto. (* cmp_solve. *) unfold eq. simpl; auto. unfold lt_farray. simpl; auto. unfold lt_farray. simpl; auto. destruct a as (x,e); destruct p as (x',e'). destruct (compare x x'); [ apply LT | | apply GT ]. unfold lt_farray. simpl. destruct (compare x x'); auto. subst. apply lt_not_eq in l; now contradict l. apply (lt_trans x') in l; auto. subst. apply lt_not_eq in l; now contradict l. (* subst. *) destruct (compare e e'); [ apply LT | | apply GT ]. unfold lt_farray. simpl. destruct (compare x x'); auto; try (subst; apply lt_not_eq in l0; now contradict l0). assert (Hm11 : sort (Raw.ltk key_ord) m1). inversion_clear Hm1; auto. assert (Hm22 : sort (Raw.ltk key_ord) m2). inversion_clear Hm2; auto. destruct (IHm1 Hm11 (Build_slist Hm22)); [ apply LT | apply EQ | apply GT ]. unfold lt_farray in *. simpl. destruct (compare x x'); auto; try (subst; apply lt_not_eq in l0; now contradict l0). unfold eq in *. simpl. destruct (compare x x'); auto; try (subst; apply lt_not_eq in l; now contradict l). unfold lt_farray in *. simpl. destruct (compare x' x); auto; try (subst; apply lt_not_eq in l0; now contradict l0). unfold lt_farray in *. simpl. destruct (compare x' x); auto; try (subst; apply lt_not_eq in l0; now contradict l0). unfold lt_farray in *. simpl. destruct (compare x' x); auto; try (subst; apply lt_not_eq in l; now contradict l). apply (lt_trans x) in l; auto. subst. apply lt_not_eq in l; now contradict l. Qed. (* TODO *) Lemma eq_option_alt : forall (elt:Type)(o o':option elt), o=o' <-> (forall e, o=Some e <-> o'=Some e). Proof. split; intros. subst; split; auto. destruct o; destruct o'; try rewrite H; auto. symmetry; rewrite <- H; auto. Qed. Lemma find_mapsto_iff : forall m x e, MapsTo x e m <-> find x m = Some e. Proof. split; [apply find_1|apply find_2]. Qed. Lemma add_neq_mapsto_iff : forall m x y e e', x <> y -> (MapsTo y e' (add x e m) <-> MapsTo y e' m). Proof. split; [apply add_3|apply add_2]; auto. Qed. Lemma add_eq_o : forall m x y e, x = y -> find y (add x e m) = Some e. Proof. intros. apply find_1. apply add_1. auto. Qed. Lemma add_neq_o : forall m x y e, ~ x = y -> find y (add x e m) = find y m. Proof. intros. rewrite eq_option_alt. intro e'. rewrite <- 2 find_mapsto_iff. apply add_neq_mapsto_iff; auto. Qed. Hint Resolve add_neq_o. Lemma MapsTo_fun : forall m x (e e':elt), MapsTo x e m -> MapsTo x e' m -> e=e'. Proof. intros. generalize (find_1 H) (find_1 H0); clear H H0. intros; rewrite H in H0; injection H0; auto. Qed. (** Another characterisation of [Equal] *) Lemma Equal_mapsto_iff : forall m1 m2 : farray, Equal m1 m2 <-> (forall k e, MapsTo k e m1 <-> MapsTo k e m2). Proof. intros m1 m2. split; [intros Heq k e|intros Hiff]. rewrite 2 find_mapsto_iff, Heq. split; auto. intro k. rewrite eq_option_alt. intro e. rewrite <- 2 find_mapsto_iff; auto. Qed. (** * Relations between [Equal], [Equiv] and [Equivb]. *) (** First, [Equal] is [Equiv] with Leibniz on elements. *) Lemma Equal_Equiv : forall (m m' : farray), Equal m m' <-> Equiv m m'. Proof. intros. rewrite Equal_mapsto_iff. split; intros. split. split; intros (e,Hin); exists e; unfold MapsTo in H; [rewrite <- H|rewrite H]; auto. intros; apply MapsTo_fun with m k; auto; rewrite H; auto. split; intros H'. destruct H. assert (Hin : In k m') by (rewrite <- H; exists e; auto). destruct Hin as (e',He'). rewrite (H0 k e e'); auto. destruct H. assert (Hin : In k m) by (rewrite H; exists e; auto). destruct Hin as (e',He'). rewrite <- (H0 k e' e); auto. Qed. Lemma Equiv_Equivb : forall m m', Equiv m m' <-> Equivb m m'. Proof. unfold Equiv, Equivb, Raw.Equivb, cmp; intuition; specialize (H1 k e e' H H2). destruct (compare e e'); auto; apply lt_not_eq in l; auto. destruct (compare e e'); auto; now contradict H1. Qed. (** Composition of the two last results: relation between [Equal] and [Equivb]. *) Lemma Equal_Equivb : forall (m m':farray), Equal m m' <-> Equivb m m'. Proof. intros; rewrite Equal_Equiv. apply Equiv_Equivb; auto. Qed. (** * Functional arrays *) Definition select (a: farray) (i: key) : option elt := find i a. Definition store (a: farray) (i: key) (v: elt) : farray := add i v a. Lemma read_over_same_write : forall a i j v, i = j -> select (store a i v) j = Some v. Proof. intros a i j v Heq. unfold select, store. intros. rewrite add_eq_o; auto. Qed. Lemma read_over_other_write : forall a i j v, i <> j -> select (store a i v) j = select a j. Proof. intros a i j v Hneq. unfold select, store. rewrite add_neq_o; auto. Qed. (* TODO *) Lemma find_ext_dec: (forall m1 m2: farray, Equal m1 m2 -> (equal m1 m2) = true). Proof. intros. apply Equal_Equivb in H. apply equal_1. exact H. Qed. Lemma extensionnality : forall a b, (forall i, select a i = select b i) -> equal a b = true. Proof. intros. unfold select in H. apply find_ext_dec in H. exact H. Qed. Require Import ProofIrrelevance. Lemma equal_eq : forall a b, equal a b = true -> a = b. Proof. intros. apply eq_equal in H. destruct a as (a, asort), b as (b, bsort). unfold eq in H. revert b bsort H. induction a; intros; destruct b. apply f_equal. apply proof_irrelevance. simpl in H. now contradict H. simpl in H. destruct a; now contradict H. simpl in H. destruct a, p. destruct (compare k k0); auto; try (now contradict H). destruct H. subst. inversion_clear asort. inversion_clear bsort. specialize (IHa H b H2 H0). inversion IHa. subst. apply f_equal. apply proof_irrelevance. Qed. (** farray equal in Prop *) Definition equalP (m m' : farray) : Prop := if equal m m' then True else False. Lemma eq_list_refl: forall a, eq_list a a. Proof. intro a. induction a; intros. - now simpl. - simpl. destruct a as (k, e). case_eq (compare k k); intros. + revert H. generalize l. apply lt_not_eq in l. now contradict l. + split; easy. + revert H. generalize l. apply lt_not_eq in l. now contradict l. Qed. Lemma equal_refl: forall a, equal a a = true. Proof. intros; apply eq_equal; apply eq_list_refl. Qed. Lemma equal_eqP : forall a b, equalP a b <-> a = b. Proof. intros. split; intro H. unfold equalP in H. case_eq (equal a b); intros; rewrite H0 in H. now apply equal_eq. now contradict H. rewrite H. unfold equalP. now rewrite equal_refl. Qed. Lemma equal_B2P: forall (m m' : farray), equal m m' = true <-> equalP m m'. Proof. intros. split; intros. apply equal_eq in H. rewrite H. unfold equalP. now rewrite equal_refl. apply equal_eqP in H. now rewrite H, equal_refl. Qed. End FArray. (* Local Variables: coq-load-path: ((rec ".." "SMTCoq")) End: *)