Finite Partial Functions

  • In this section we implement finite partial functions (FPF) with type set defined at module ListSet.v.
  • A FPF is a set of pairs. Given that both (x,y1) and (x,y2) with y1 != y2 may belong to a set of pairs, not every set of pairs is a FPF. For this reason, the specifier should use function IsPARTFUNC to test whether a given set of pairs is a FPF or not. All the other functions (DOM, RAN and PARTFUNC) assume that this test has been performed, otherwise their results are usless.
  • If f is a FPF and (x,y) belongs to f, then
    • f applied to x yields y,
    • x belongs to the domain of f
    • y belongs to the range of f.

Require PolyList.

Require ListFunctions.

Require ListSet.

Implicit Arguments On.

Section PartialFunctions.

Variables X,Y:Set.

Hypothesis Xeq_dec : (x1,x2:X) {x1=x2}+{~x1=x2}.

Hypothesis Yeq_dec : (x1,x2:Y) {x1=x2}+{~x1=x2}.

Hypothesis XYeq_dec : (x1,x2:X*Y){x1=x2}+{~x1=x2}.

Main definitions

  • Domain of a FPF

Fixpoint DOM [f:(set X*Y)] : (set X) :=
 Cases f of
  |nil => (nil X)
  |(cons (x,y) g) => (set_add Xeq_dec x (DOM g))
 end.

  • Range of a FPF

Fixpoint RAN [f:(set X*Y)] : (set Y) :=
 Cases f of
  |nil => (nil Y)
  |(cons (x,y) g) => (set_add Yeq_dec y (RAN g))
 end.

  • Application of a FPF

Fixpoint PARTFUNC [f:(set X*Y)] : X -> (Exc Y) :=
 [x:X]
 Cases f of
  |nil => (None Y)
  |(cons (x1,y) g) => Cases (Xeq_dec x x1) of
                          |(left _) => (Some Y y)
                          |(right _) => (PARTFUNC g x)
                         end
 end.

  • Test to decide whether a set of pairs is a FPF or not

Fixpoint IsPARTFUNC [f:(set X*Y)] : Prop :=
 Cases f of
  |nil => True
  |(cons a l) => Cases (set_In_dec Xeq_dec (Fst a) (DOM l)) of
                  |(left _) => False
                  |(right _) => (IsPARTFUNC l)
                 end
 end.


A library of lemmas about our implementation of FPF

Lemma AddEq:
 (a,b:X; y:Y; f:(set X*Y))
   ~a=b
   ->(PARTFUNC f a)=
        (PARTFUNC (set_add XYeq_dec (b,y) f) a).
Intros.
Induction f.
Simpl.
Elim (Xeq_dec a b).
Intros.
Cut False.
Intro.
Elim H0.

Unfold not in H; Apply H.
Auto.

Auto.

Simpl.
Elim a0.
Intros.
Elim (Xeq_dec a a1).
Elim (XYeq_dec (b,y) (a1,b0)).
Intros.
Cut False.
Intro F.
Elim F.

Unfold not in H.
Apply H.
Rewrite a3.
Injection a2.
Auto.

Simpl.
Elim (Xeq_dec a a1).
Auto.

Intros.
Cut False.
Intro F.
Elim F.

Auto.

Elim (XYeq_dec (b,y) (a1,b0)).
Simpl.
Elim (Xeq_dec a a1).
Intros.
Cut False.
Intro F.
Elim F.

Auto.

Auto.

Simpl.
Elim (Xeq_dec a a1).
Intros.
Cut False.
Intro F.
Elim F.

Auto.

Intros.
Auto.

Qed.

Lemma AddEq1:
 (x:X; y:Y; f:(set X*Y))
   ~(set_In x (DOM f))
   ->(value Y y)=(PARTFUNC (set_add XYeq_dec (x,y) f) x).
Induction f.
Simpl.
Elim (Xeq_dec x x); Auto.
Intro; Absurd x=x; Auto.

Simpl.
Intros until l.
Elim a.
Intros until b.
Elim (XYeq_dec (x,y) (a0,b)).
Simpl.
Elim (Xeq_dec x a0).
Intros.
Injection a2; Intros.
Rewrite H1; Auto.

Intros.
Injection a1; Intros; Absurd x=a0; Auto.

Simpl.
Elim (Xeq_dec x a0).
Intros.
Rewrite a1 in H0.
Cut False.
Tauto.

Apply H0.
Apply set_add_intro2; Auto.

Intros.
Apply H.
Intro; Apply H0; Apply set_add_intro1; Auto.

Qed.

Lemma RemEq:
 (a,b:X; y:Y; f:(set X*Y))
   ~a=b
   ->(PARTFUNC f a)=
        (PARTFUNC (set_remove XYeq_dec (b,y) f) a).
Intros.
Induction f.
Auto.

Simpl.
Elim a0.
Intros.
Elim (Xeq_dec a a1).
Elim (XYeq_dec (b,y) (a1,b0)).
Intros.
Cut False.
Intro F.
Elim F.

Unfold not in H.
Apply H.
Rewrite a3.
Injection a2.
Auto.

Simpl.
Elim (Xeq_dec a a1).
Auto.

Intros.
Cut False.
Intro F.
Elim F.

Auto.

Elim (XYeq_dec (b,y) (a1,b0)).
Simpl.
Elim (Xeq_dec a a1).
Intros.
Cut False.
Intro F.
Elim F.

Auto.

Auto.

Simpl.
Elim (Xeq_dec a a1).
Intros.
Cut False.
Intro F.
Elim F.

Auto.

Intros.
Auto.

Qed.

Lemma AddRemEq:
 (a,b:X; y,z:Y; f:(set X*Y))
   ~a=b
   ->(PARTFUNC f a) =
          (PARTFUNC (set_add XYeq_dec
                             (b,z)
                             (set_remove XYeq_dec (b,y) f)) a).
Intros.
Induction f.
Simpl.
Elim (Xeq_dec a b).
Intros.
Cut False.
Intro F; Elim F.

Auto.

Auto.

Simpl.
Elim a0.
Intros.
Elim (Xeq_dec a a1).
Elim (XYeq_dec (b,y) (a1,b0)).
Intros.
Cut False.
Intro F; Elim F.

Unfold not in H; Apply H.
Rewrite a3.
Injection a2.
Auto.

Simpl.
Elim (XYeq_dec (b,z) (a1,b0)).
Intros.
Cut False.
Intro F; Elim F.

Unfold not in H.
Apply H.
Rewrite a3.
Injection a2.
Auto.

Simpl.
Elim (Xeq_dec a a1).
Auto.

Intros.
Cut False.
Intro F; Elim F.

Auto.

Elim (XYeq_dec (b,y) (a1,b0)).
Auto.

Intros.
Simpl.
Elim (XYeq_dec (b,z) (a1,b0)).
Simpl.
Elim (Xeq_dec a a1).
Intros.
Cut False.
Intro F; Elim F.

Auto.

Intros.
Apply RemEq.
Auto.

Auto.

Simpl.
Elim (Xeq_dec a a1).
Intros.
Cut False.
Intro F; Elim F.

Auto.

Auto.

Qed.

Lemma NotInDOMIsUndef:
 (o:X; f:(set X*Y))~(set_In o (DOM f)) -> (PARTFUNC f o) = (None Y).
Intros.
Induction f.
Simpl.
Auto.

Generalize H.
Simpl.
Elim a.
Intro; Intro.
Elim (Xeq_dec o a0).
Intro.
Rewrite a1.
Intro.
Cut False.
Intro F; Elim F.

Unfold not in H0.
Apply H0.
Apply set_add_intro2.
Auto.

Intros.
Apply Hrecf.
Unfold not in H0; Unfold not.
Intro; Apply H0.
Apply set_add_intro1.
Auto.

Qed.

Hints Resolve NotInDOMIsUndef.

Lemma InDOMIsNotUndef:
 (o:X; f:(set X*Y))(set_In o (DOM f)) -> ~(PARTFUNC f o) = (None Y).
Induction f.
Auto.

Simpl.
Intro.
Elim a.
Intro.
Elim (Xeq_dec o a0).
Intros; Intro H3; Discriminate H3.

Intros; Apply H.

EAuto.

Qed.

Lemma InDOMWhenAdd:
 (x:X; y:Y; f:(set X*Y))
  (set_In x (DOM (set_add XYeq_dec (x,y) f))).
Intros; Induction f.
Simpl.
Left; Auto.

Simpl.
Elim (XYeq_dec (x,y) a).
Simpl.
Elim a.
Intros.
Injection a1; Intros.
Apply set_add_intro2; Auto.

Simpl.
Elim a.
Intros.
Apply set_add_intro1; Auto.

Qed.

Lemma DOMFuncRel:
 (a:X*Y; f:(set X*Y))
  ~(set_In (Fst a) (DOM f))->f=(set_remove XYeq_dec a f).
Induction f.
Simpl; Auto.

Simpl.
Intro; Elim a0.
Intros until b; Elim (XYeq_dec a (a1,b)).
Elim a.
Intros.
Injection a3; Intros.
Simpl in H0; Rewrite H2 in H0.
Cut False.
Tauto.

Apply H0; Apply set_add_intro2; Auto.

Elim a.
Simpl.
Intros.
Cut l=(set_remove XYeq_dec (a2,b0) l).
Intro.
Rewrite <- H1; Auto.

Apply H.
Intro; Apply H0; Apply set_add_intro; Auto.

Qed.

Hints Resolve DOMFuncRel.

Lemma DOMFuncRel2:
 (z:X*Y; f:(set X*Y))
  (set_In z f)->(set_In (Fst z) (DOM f)).
Induction f.
Simpl; Auto.

Simpl.
Intro; Elim a.
Elim z.
Simpl.
Intros.
Elim H0; Intro.
Injection H1; Intros.
Apply set_add_intro; Auto.

Cut (set_In a0 (DOM l)).
Intro; Apply set_add_intro1; Auto.

Auto.

Qed.

Hints Resolve DOMFuncRel2.

Lemma DOMFuncRel3:
(x:X; y:Y; f:(set X*Y))
 (IsPARTFUNC f)
 ->(set_In (x,y) f)
 ->~(set_In x (DOM (set_remove XYeq_dec (x,y) f))).
Induction f.
Simpl; Auto.

Simpl.
Intros until l; Elim (set_In_dec Xeq_dec (Fst a) (DOM l));
  Elim (XYeq_dec (x,y) a).
Tauto.

Tauto.

Intros; Cut l=(set_remove XYeq_dec (x,y) l).
Intro H2; Rewrite <- H2; Replace x with (Fst a); Auto.
Rewrite <- a0; Auto.

Rewrite a0; Auto.

Simpl.
Elim a.
Simpl.
Intros.
Elim H1; Intro.
Absurd (a0,b)=(x,y); Auto.

Elim (Xeq_dec x a0); Intro.
Rewrite <- a1 in b1.
Intro; Apply b1; Replace x with (Fst (x,y)); Auto.

Cut ~(set_In x (DOM (set_remove XYeq_dec (x,y) l))).
Auto.

Auto.

Qed.

Lemma DOMFuncRel4:
 (x:X; f:(set X*Y))
  Cases (PARTFUNC f x) of
   |(Some a) => (set_In (x,a) f)
   |None => ~(set_In x (DOM f))
  end.
Induction f.
Simpl; Auto.

Simpl.
Intros until l; Elim a.
Intros until b; Elim (Xeq_dec x a0).
Elim (PARTFUNC l x).
Intros y2 H; Left; Rewrite H; Auto.

Intros H H1; Left; Rewrite H; Auto.

Elim (PARTFUNC l x).
Auto.

Auto.

Qed.

Lemma UndefWhenRem:
 (x:X; y:Y; f:(set X*Y))
  (IsPARTFUNC f)
  ->(set_In (x,y) f)
  ->(PARTFUNC (set_remove XYeq_dec (x,y) f) x)=(None Y).
Induction f.
Simpl; Auto.

Simpl.
Intros until l.
Elim (set_In_dec Xeq_dec (Fst a) (DOM l)); Elim (XYeq_dec (x,y) a).
Tauto.

Tauto.

Intros.
Replace (set_remove XYeq_dec (x,y) l) with l.
Rewrite <- a0 in b.
Simpl in b.
Auto.

Rewrite <- a0 in b.
Auto.

Simpl.
Elim a.
Intros.
Elim H1; Intro.
Cut False.
Tauto.

Apply b0; Symmetry; Auto.

Elim (Xeq_dec x a0).
Intro.
Simpl in b1.
Rewrite <- a1 in b1.
Absurd (set_In x (DOM l)).
Auto.

Replace x with (Fst (x,y)); Auto.

Auto.

Qed.

End PartialFunctions.

Hints Resolve AddEq RemEq AddRemEq NotInDOMIsUndef InDOMIsNotUndef
              InDOMWhenAdd UndefWhenRem AddEq1 DOMFuncRel3.

Index
This page has been generated by coqdoc