(* * Copyright (c) 2009, Andrew Appel, Robert Dockins and Aquinas Hobor. * *) (** This module defines the standard operators on separation algebras, including the operators over pairs, disjoint sums, function spaces, dependent products, dependent sums, sub-separation algebras, the discrete separation algebra, the lifting operator, and the trivial unit and void separation algrbras. *) Require Import base. Require Import sepalg. (** The trivial separation algebra over the unit type. This SA is the identity of the product SA operator, up to isomorphism. *) Definition join_unit (x y z:unit) := True. Lemma unit_eq : forall x y:unit, x = y. intros; case x; case y; trivial. Qed. Lemma saf_unit : sepalgfacts join_unit. Proof. apply SepAlgFacts; firstorder; apply unit_eq. Qed. Definition sa_unit : sepalg unit := SepAlg saf_unit. (** The trivial separation algrbra over the void type. This SA is the identity of the coproduct (disjoint sum) SA operator, up to isomorphism. *) Inductive Void : Type :=. Definition join_void (x y z:Void) := False. Lemma saf_void : sepalgfacts join_void. Proof. apply SepAlgFacts; intuition. Qed. Definition sa_void : sepalg Void := SepAlg saf_void. (** The "equivalance" or discrete SA. In this SA, every element of an arbitrary set is made an idempotent element. *) Section SepAlgEquiv. Variable A:Type. Definition join_equiv (x y z:A) := x=y /\ y=z. Lemma saf_equiv : sepalgfacts join_equiv. Proof. apply SepAlgFacts; unfold join_equiv. (* join_eq *) intuition; congruence. (* join_asssoc *) intuition; exists a; intuition congruence. (* join com *) intuition; congruence. (* join_canc *) intuition congruence. (* join_ex_identities *) intro a; exists a; auto. (* join_self *) intuition. Qed. Definition sa_equiv : sepalg A := SepAlg saf_equiv. End SepAlgEquiv. (** The subSA operator. Given some SA and a property [P] on the elements of that SA, form the SA consisting of just those elements satisfying [P]. The property [P] must be compatible with the original SA, as specified in the hypothesis [HPunit] and [HPjoin]. *) Section SepAlgProp. Variable A:Type. Variable j:sepalg A. Variable P:A -> Prop. Variable HPunit : forall x e, P x -> @unit_for A j e x -> P e. Variable HPjoin : forall x y z, @join A j x y z -> P x -> P y -> P z. Definition join_prop (x y z: { a:A & P a }) := @join _ j (projT1 x) (projT1 y) (projT1 z). Lemma saf_prop : sepalgfacts join_prop. Proof. apply SepAlgFacts. (* join_eq *) intros. red in H. red in H0. destruct x; destruct y; destruct z; destruct z'; simpl in *. revert p2. replace x2 with x1; intros. replace p2 with p1; auto. apply proof_irr. apply join_eq with x x0; auto. (* join_assoc *) intros. red in H. red in H0. destruct a; destruct b; destruct c; destruct d; destruct e. simpl in *. unfold join_prop; simpl. destruct (join_assoc _ _ _ _ _ H H0) as [f [? ?]]. assert (P f). apply HPjoin with x0 x1; auto. exists (existT (fun x => P x) f H3). simpl; auto. (* join_com *) intros; red; apply join_com; auto. (* join_canc *) intros. destruct a1; destruct a2; destruct b; destruct c. red in H; red in H0; simpl in *. revert p0. replace x0 with x; intros. replace p0 with p; auto. apply proof_irr. apply join_canc with x1 x2; auto. (* join_ex_identities *) intros. destruct a as [x Hx]. destruct (join_ex_identities x) as [e He]. assert (P e) by (apply HPunit with x; trivial; apply identity_unit; firstorder). exists (existT (fun x => P x) e H). red; simpl; apply identity_unit; firstorder. (* join_self *) intros. destruct a; destruct b. red in H; simpl in H. revert p0. replace x0 with x; intros. replace p0 with p; auto. apply proof_irr. apply join_self; auto. Qed. Definition sa_prop : sepalg { a:A & P a } := SepAlg saf_prop. End SepAlgProp. Implicit Arguments sa_prop. (** The function space operator from a key type [key] to a separtion algebra on type [t']. *) Section SepAlgFun. Variable key: Type. Variable t' : Type. Variable range: sepalg t'. Definition m_join (a b c : key -> t') : Prop := forall x, @join _ range (a x) (b x) (c x). Lemma saf_fun: sepalgfacts m_join. Proof. apply SepAlgFacts. (* join_eq *) unfold m_join; intros; extensionality a; apply join_eq with (x a) (y a); auto. (* join_assoc *) unfold m_join; intros. set (F := fun x => join_assoc _ _ _ _ _ (H x) (H0 x)). exists (fun x => projT1 (F x)); split; intros; destruct (F x); simpl; intuition. (* join_com *) unfold m_join; intros; apply join_com; auto. (* join_canc *) unfold m_join; intros; extensionality x; intros; apply join_canc with (b x) (c x); auto. (* join_ex_identities *) unfold m_join; intros. set (F := fun x => join_ex_identities (a x)). exists (fun x => projT1 (F x)). intro x; destruct (F x); apply identity_unit; simpl; firstorder. (* join_self *) unfold m_join; intros. unfold join. extensionality x. apply join_self; auto. Qed. Definition sa_fun:sepalg (key -> t') := SepAlg saf_fun. End SepAlgFun. Implicit Arguments sa_fun. (** The dependent product SA operator from an index set [I] into a SA indexed by [Pi_j]. The construction of this operator either requires constructive witnesses for the unit and associativity axioms or some form of the axiom of choice. We have chosen to have explicitly constructive witnesses and avoid the use of choice. *) Section SepAlgPi. Variable I:Type. Variable Pi: I -> Type. Variable Pi_j : forall i:I, sepalg (Pi i). Let P := forall i:I, Pi i. Definition join_pi (x y z: P) : Prop := forall i:I, join (x i) (y i) (z i). Definition saf_pi : sepalgfacts join_pi. constructor. (* join_eq *) intros; apply (dep_extensionality Pi); intro i. apply (join_eq (x i) (y i)); auto. (* join_assoc *) intros. pose (f := fun i => projT1 (join_assoc _ _ _ _ _ (H i) (H0 i))). exists f. split; intro i; unfold f; destruct (join_assoc _ _ _ _ _ (H i) (H0 i)); simpl; intuition. (* join_com *) intros; intro i; apply join_com; auto. (* cancellation *) intros; apply (dep_extensionality Pi); intro i. apply join_canc with (b i) (c i); auto. (* exist_identities *) intros. pose (e := fun i => projT1 (join_ex_units (a i))). exists e. intro i; unfold e. destruct (join_ex_units (a i)); simpl; auto. (* self_join_identity *) intros. apply (dep_extensionality Pi); intro i. apply (join_self _ _ (H i)). Qed. Definition sa_pi : sepalg P := SepAlg saf_pi. End SepAlgPi. Implicit Arguments sa_pi. Implicit Arguments sa_pi. (** The dependent sum operator on SAs. Here we have defined the operator under the hypothesis that dependent pairs are injective. This property can be proved without axioms provided that the index type [I] enjoys decidable equality. The property for all types follows as a corralary of Streicher's K axiom (or one of its equivalants). The K axiom, in turn, follows from the classical axiom. Users who are willing to assume K can then use this construction at any index type. *) Section SepAlgSigma. Variable I:Type. Variable Sigma: I -> Type. Variable Sigma_j : forall i:I, sepalg (Sigma i). Let S := { i:I & Sigma i }. Let injS := existT (fun x => Sigma x). Hypothesis inj_sig_I : forall i x y, injS i x = injS i y -> x = y. Ltac inj_sig := repeat match goal with [ X : (@eq (sigT (fun x => Sigma x)) (existT _ _ ?a) (existT _ _ ?b)) |- _ ] => generalize (inj_sig_I _ _ _ X); intros; clear X end. Inductive join_sigma : S -> S -> S -> Prop := j_sig_def : forall (i:I) (a b c:Sigma i), join a b c -> join_sigma (injS i a) (injS i b) (injS i c). Lemma saf_sigma : sepalgfacts join_sigma. Proof. apply SepAlgFacts. (* join_eq *) intros. inv H; inv H0; inj_sig; subst. replace c with c0; auto. apply join_eq with a b; auto. (* join_assoc *) intros [ai a] [bi b] [ci c] [di d] [ei e]; intros. assert (ai = bi /\ bi = ci /\ ci = di /\ di = ei). inv H; inv H0; simpl; auto. decompose [and] H1; subst; clear H1. rename ei into i. assert (join a b d). inversion H; inj_sig; subst; auto. assert (join d c e). inversion H0; inj_sig; subst; auto. destruct (join_assoc _ _ _ _ _ H1 H2) as [f [? ?]]. exists (existT (fun i => Sigma i) i f). split; constructor; auto. (* join_com *) intros. inv H; inj_sig; subst. constructor. apply join_com; auto. (* join_canc *) intros. inv H; inv H0; inj_sig; subst. replace a with a1; auto. apply join_canc with b0 c0; auto. (* join_ex_identities *) intros [ai a]. destruct (join_ex_identities a) as [e ?]. exists (existT (fun i => Sigma i) ai e). constructor; auto. apply identity_unit; firstorder. (* join_self *) intros; inv H; inj_sig; subst. replace c with a0; auto. apply join_self; auto. Qed. Definition sa_sigma : sepalg S := SepAlg saf_sigma. End SepAlgSigma. Implicit Arguments sa_sigma. (** The sigma SA construction (see above) specialized to types with decidable equality. *) Section SepAlgSigma_dec. Variable I:Type. Variable Sigma: I -> Type. Variable Sigma_j : forall i:I, sepalg (Sigma i). Variable eq_dec : forall x y:I, {x=y}+{x<>y}. Require Import Eqdep_dec. Let inj_sig_I := inj_pair2_eq_dec I eq_dec (fun x => Sigma x). Definition sa_sigma_dec := sa_sigma Sigma Sigma_j inj_sig_I. End SepAlgSigma_dec. Implicit Arguments sa_sigma_dec. (** The SA operator on cartesian products. *) Section SepAlgProd. Variables A B:Type. Variables (ja:sepalg A) (jb:sepalg B). Definition join_prod (x y z:A*B) : Prop := join (fst x) (fst y) (fst z) /\ join (snd x) (snd y) (snd z). Lemma saf_prod : sepalgfacts join_prod. Proof. apply SepAlgFacts. (* join_eq *) intuition; destruct z'; simpl in *. replace a2 with a1. replace b2 with b1. trivial. apply join_eq with b b0; firstorder. apply join_eq with a a0; firstorder. (* join_assoc *) intuition; firstorder; destruct e; simpl in *. destruct (join_assoc _ _ _ _ _ H H0) as [x [? ?]]. destruct (join_assoc _ _ _ _ _ H1 H2) as [y [? ?]]. exists (x,y); firstorder. (* join_com *) intuition; firstorder; destruct c; simpl in *. apply join_com; auto. apply join_com; auto. (* join_canc *) intuition; firstorder; destruct c; simpl in *. replace a0 with a. replace b0 with b. trivial. apply (join_canc _ _ _ _ H1 H2). apply (join_canc _ _ _ _ H H0). (* join_ex_identities *) intuition; firstorder. destruct (join_ex_identities a0) as [x ?]. destruct (join_ex_identities b) as [y ?]. exists (x,y); firstorder; apply identity_unit; firstorder. (* join_self *) intuition; firstorder; destruct b0; simpl in *. rewrite (join_self a0 a); auto. rewrite (join_self b b0); auto. Qed. Definition sa_prod : sepalg (A*B) := SepAlg saf_prod. End SepAlgProd. Implicit Arguments sa_prod. (** The SA operator on disjoint sums. *) Section SepAlgSum. Variables A B:Type. Variables (ja:sepalg A) (jb:sepalg B). Definition join_sum (x y z:A+B) : Prop := match x, y, z with | inl xa, inl ya, inl za => join xa ya za | inr xb, inr yb, inr zb => join xb yb zb | _, _, _ => False end. Lemma saf_sum : sepalgfacts join_sum. Proof. apply SepAlgFacts. (* join_eq *) intuition; destruct z'; simpl in *; try contradiction. replace a2 with a1; [ trivial | apply (join_eq _ _ _ _ H H0) ]. replace b2 with b1; [ trivial | apply (join_eq _ _ _ _ H H0) ]. (* join_assoc *) intuition; destruct e; simpl in *; try contradiction. destruct (join_assoc _ _ _ _ _ H H0) as [a' [? ?]]. exists (inl B a'); simpl; intuition. destruct (join_assoc _ _ _ _ _ H H0) as [b' [? ?]]. exists (inr A b'); simpl; intuition. (* join_com *) intuition; destruct c; simpl in *; try contradiction. apply join_com; auto. apply join_com; auto. (* join_canc *) intuition; destruct c; simpl in *; try contradiction. replace a0 with a; trivial. apply (join_canc _ _ _ _ H H0). replace b0 with b; trivial. apply (join_canc _ _ _ _ H H0). (* join_ex_identities *) intuition. destruct (join_ex_identities a0). exists (inl B x); simpl; apply identity_unit; destruct a; auto. (* firstorder -- bug in Coq *) destruct (join_ex_identities b). exists (inr A x); simpl; apply identity_unit; destruct a; auto. (* firstorder -- bug in Coq *) (* join_self *) intuition; try destruct b; try destruct b0; simpl in *; try contradiction. rewrite (join_self a0 a); auto. rewrite (join_self b b0); auto. Qed. Definition sa_sum : sepalg (A + B) := SepAlg saf_sum. End SepAlgSum. Implicit Arguments sa_sum. (** The SA operator on lists. Lists are joined componentwise. *) Section sa_list. Variable A:Type. Variable A_sa : sepalg A. Inductive list_join : list A -> list A -> list A -> Prop := | lj_nil : list_join nil nil nil | lj_cons : forall x y z xs ys zs, join x y z -> list_join xs ys zs -> list_join (x::xs) (y::ys) (z::zs). Lemma saf_list : sepalgfacts list_join. Proof. constructor. induction x; intros; inv H; inv H0; auto. rewrite (IHx ys zs zs0); auto. replace z0 with z; auto. eapply join_eq; eauto. induction a; intros. exists nil. inv H; inv H0. split; constructor. destruct b; destruct d; try (elimtype False; inv H; fail). destruct c; destruct e; try (elimtype False; inv H0; fail). assert (join a a1 a2) by (inv H; auto). assert (join a2 a3 a4) by (inv H0; auto). assert (list_join a0 b d) by (inv H; auto). assert (list_join d c e) by (inv H0; auto). destruct (join_assoc _ _ _ _ _ H1 H2) as [z [? ?]]. destruct (IHa _ _ _ _ H3 H4) as [zs [? ?]]. exists (z::zs); split; constructor; auto. induction a; intros; inv H; constructor; auto. apply join_com; auto. induction a1; intros. inv H; inv H0; auto. inv H0; inv H. rewrite <- (IHa1 xs ys zs); auto. replace x with a; auto. eapply join_canc; eauto. induction a. exists nil; constructor. destruct IHa as [es ?]. destruct (join_ex_units a) as [e ?]. exists (e::es); constructor; eauto. induction a; intros; inv H; auto. rewrite IHa with zs; auto. replace z with a; auto. eapply join_self; eauto. Qed. Definition list_sa : sepalg (list A) := SepAlg saf_list. End sa_list. Implicit Arguments list_sa. Definition raw_join_hom A B (j1: A -> A -> A -> Prop) (j2: B -> B -> B -> Prop) (f:A ->B) := forall x y z, j1 x y z -> j2 (f x) (f y) (f z). Implicit Arguments raw_join_hom. (** The SA induced by the preimage of a section in a section-retraction pair. This SA construction is used to generate a separation algebra over "knots". *) Section sa_preimage. Variables A B:Type. Variable B_sa : sepalg B. Variable f:A -> B. Variable f':B -> A. Hypothesis Hf'_f : forall x, f' (f x) = x. Hypothesis Hf_f' : join_hom (f oo f'). Lemma f_inj : forall x y, f x = f y -> x = y. Proof. intros. rewrite <- (Hf'_f x). rewrite <- (Hf'_f y). rewrite H; auto. Qed. Definition join_preimage (a b c:A) := join (f a) (f b) (f c). Lemma saf_preimage : sepalgfacts join_preimage. Proof. unfold join_preimage; constructor; intros. apply f_inj; eapply join_eq; eauto. destruct (join_assoc _ _ _ _ _ H H0) as [z [? ?]]. exists (f' z). rewrite <- (Hf'_f b); rewrite <- (Hf'_f c). rewrite <- (Hf'_f a); rewrite <- (Hf'_f e). split; apply Hf_f'; auto. apply join_com; auto. apply f_inj; eapply join_canc; eauto. destruct (join_ex_units (f a)) as [e ?]. exists (f' e). rewrite <- (Hf'_f a). apply Hf_f'; auto. apply f_inj; eapply join_self; eauto. Qed. Definition preimage_sa : sepalg A := SepAlg saf_preimage. End sa_preimage. (** This operator transforms a SA into an isomorphic one by passing through the bijection [bij]. *) Section SepAlgBijection. Variables A B:Type. Record bijection : Type := Bijection { bij_f: A -> B; bij_g: B -> A; bij_fg: forall x, bij_f (bij_g x) = x; bij_gf: forall x, bij_g (bij_f x) = x }. Variable bij : bijection. Variable saa : sepalg A. Definition join_bijection (x y z : B) : Prop := match bij with Bijection _ g _ _ => join (g x) (g y) (g z) end. Lemma saf_bijection : sepalgfacts join_bijection. Proof. unfold join_bijection. destruct bij as [f g fg gf]. apply SepAlgFacts; intros; auto. generalize (f_equal f (join_eq _ _ _ _ H H0)); intro; repeat rewrite fg in H1; auto. destruct (join_assoc _ _ _ _ _ H H0); exists (f x); rewrite gf; auto. apply join_com; auto. generalize (f_equal f (join_canc _ _ _ _ H H0)); repeat rewrite fg; auto. destruct (join_ex_identities (g a)); exists (f x); rewrite gf; apply identity_unit; firstorder. generalize (f_equal f (join_self _ _ H)); repeat rewrite fg; auto. Qed. Definition sa_bijection : sepalg B := SepAlg saf_bijection. End SepAlgBijection. (** This section defines the "strictly positive" ([pjoinable]) elements of a SA as the nonidentity elements. These elements satisfy all the SA axioms except the existance of identities. We then define the "lifting" operator by adding a new, unique identity element to the strictly positive elements. *) Section PJoin. Variable T : Type. Variable j : sepalg T. Definition pjoinable : Type := {t : T & ~ identity t}. Definition pjoin (j1 j2 j3 : pjoinable) : Prop := match (j1, j2, j3) with (existT t1 _, existT t2 _, existT t3 _) => join t1 t2 t3 end. Lemma pjoin_eq: forall x y z z', pjoin x y z -> pjoin x y z' -> z = z'. Proof. intros. destruct x. destruct y. destruct z. destruct z'. unfold pjoin in *. generalize (join_eq _ _ _ _ H H0); intro. subst x2. assert (n1 = n2) by apply proof_irr. subst n2. trivial. Qed. Lemma pjoin_assoc: forall a b c d e, pjoin a b d -> pjoin d c e -> {f : pjoinable & pjoin b c f /\ pjoin a f e}. Proof. intros. destruct a. destruct b. destruct c. destruct d. destruct e. unfold pjoin in *. destruct (join_assoc _ _ _ _ _ H H0) as [? [? ?]]. assert (~ identity x4). intro. clear -H3 H1 n0 n1. contradiction n0. eapply split_identity; eauto. exists (existT (fun t : T => ~ identity t) x4 H3). firstorder. Qed. Lemma pjoin_com: forall a b c, pjoin a b c -> pjoin b a c. Proof. intros. destruct a. destruct b. destruct c. unfold pjoin in *. apply join_com. trivial. Qed. Lemma pcancellation: forall a1 a2 b c, pjoin a1 b c -> pjoin a2 b c -> a1=a2. Proof. intros. destruct a1. destruct a2. destruct b. destruct c. unfold pjoin in *. generalize (join_canc _ _ _ _ H H0); intro. subst x0. assert (n = n0) by apply proof_irr. subst n0. trivial. Qed. Lemma pnidentity: forall p p', pjoin p p' p' -> False. Proof. intros. destruct p. destruct p'. unfold pjoin in H. generalize (unit_identity _ _ H). contradiction. Qed. Lemma pnjoin_self: forall p p', pjoin p p p' -> False. Proof. intros. destruct p. destruct p'. unfold pjoin in H. generalize (join_self _ _ H); intro. subst x0. generalize (identity_unit_equiv x); unfold unit_for; intro. rewrite H0 in n; contradiction. Qed. Inductive lift_join : option pjoinable -> option pjoinable -> option pjoinable -> Prop := | lj_None1 : forall x, lift_join None x x | lj_None2 : forall x, lift_join x None x | lj_Sime : forall x y z:pjoinable, pjoin x y z -> lift_join (Some x) (Some y) (Some z). Lemma saf_lift : sepalgfacts lift_join. Proof. constructor. (* join_eq *) intros; inv H; inv H0; auto. replace z0 with z; auto. eapply pjoin_eq; eauto. (* join_assoc *) intros. destruct b. 2: exists c; split; try constructor; auto. 2: inv H; auto. destruct c. 2: exists (Some p); split; try constructor. 2: inv H0; auto. destruct a. 2: exists e; split; try constructor. 2: inv H; auto. destruct d. 2: elimtype False; inv H. destruct e. 2: elimtype False; inv H0. destruct (pjoin_assoc p1 p p0 p2 p3). inv H; auto. inv H0; auto. exists (Some x); intuition; constructor; auto. (* join_com *) intros; inv H; constructor. apply pjoin_com; auto. (* join_canc *) intros; inv H; inv H0; auto. elim (pnidentity _ _ H3). elim (pnidentity _ _ H1). replace x0 with x; auto. eapply pcancellation; eauto. (* join_ex_identity *) intros. exists (@None pjoinable); constructor. (* self_join *) intros; inv H; auto. replace z with x; auto. elim (pnjoin_self _ _ H2). Qed. Definition sa_lift : sepalg (option pjoinable) := SepAlg saf_lift. End PJoin. Implicit Arguments pjoinable. Implicit Arguments pjoin. Implicit Arguments pjoin_eq. Implicit Arguments pjoin_assoc. Implicit Arguments pjoin_com. Implicit Arguments pcancellation. Implicit Arguments sa_lift. (** This operator is a combination of the function space and lifting operators which provides the SA equivalant of partial maps. We also constrain the domain of the functions to be finite, giving a useful semantic characterization of finite partial maps. *) Section FinitePartialMap. Variable A:Type. Variable A_dec_eq : forall x y:A, {x=y}+{x<>y}. Variable B:Type. Variable B_sa : sepalg B. Let Rng := option (pjoinable B_sa). Let Rng_sa : sepalg Rng := sa_lift B_sa. Definition finMap (f:A -> Rng) : Prop := exists l, forall a:A, ~In a l -> f a = None. Lemma finMap_unit : forall x e, finMap x -> @unit_for _ (sa_fun A Rng_sa) e x -> finMap e. Proof. intros. destruct H as [l Hl]. exists nil. intros a _. red in H0. simpl in H0. spec H0 a. simpl in H0. inv H0; auto. elim (pnidentity _ _ _ _ H3). Qed. Lemma finMap_join : forall x y z, @join _ (sa_fun A Rng_sa) x y z -> finMap x -> finMap y -> finMap z. Proof. intros. destruct H0 as [l0 H0]. destruct H1 as [l1 H1]. exists (l0 ++ l1). intros. spec H a. simpl in H. inv H. apply H1. intro; apply H2. apply in_or_app; auto. apply H0. intro; apply H2. apply in_or_app; auto. destruct (In_dec A_dec_eq a l0). elim H2. apply in_or_app; auto. rewrite H0 in H3; auto. discriminate. Qed. Definition fpm := {f : A -> Rng & finMap f}. Definition fpm_sa : sepalg fpm := (sa_prop (sa_fun A Rng_sa) finMap finMap_unit finMap_join). Definition empty_fpm : fpm. refine (existT (fun x => finMap x) (fun _ => None) _). exists nil; auto. Defined. Definition lookup_fpm (f:fpm) : A -> Rng := projT1 f. Definition insert_fpm (a:A) (b:pjoinable B_sa) (f:fpm) : fpm. intros a b [f Hf]. set (f' := fun x => if A_dec_eq a x then Some b else f x). refine (existT _ f' _). destruct Hf as [l Hl]. exists (a :: l); simpl; intros. unfold f'. destruct (A_dec_eq a a0). subst a0. elim H; auto. apply Hl. intro; apply H; auto. Defined. Definition remove_fpm (a:A) (f:fpm) : fpm. intros a [f Hf]. set (f' := fun x => if A_dec_eq a x then None else f x). refine (existT _ f' _). destruct Hf as [l Hl]. exists l; intros. unfold f'. destruct (A_dec_eq a a0); auto. Defined. End FinitePartialMap.