From 24a71fb350cc1e7ca3696d51c609074356b77ee3 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 16 Feb 2016 21:22:30 +0100 Subject: [PATCH] add some basic theory about pointwise updates of total functions --- _CoqProject | 1 + prelude/functions.v | 31 +++++++++++++++++++++++++++++++ 2 files changed, 32 insertions(+) create mode 100644 prelude/functions.v diff --git a/_CoqProject b/_CoqProject index 942d2976..f28fdc1d 100644 --- a/_CoqProject +++ b/_CoqProject @@ -34,6 +34,7 @@ prelude/sets.v prelude/decidable.v prelude/list.v prelude/error.v +prelude/functions.v algebra/option.v algebra/cmra.v algebra/cmra_big_op.v diff --git a/prelude/functions.v b/prelude/functions.v new file mode 100644 index 00000000..2e4c93ca --- /dev/null +++ b/prelude/functions.v @@ -0,0 +1,31 @@ +From prelude Require Export base tactics. + +Section definitions. + Context {A T : Type} `{∀ a b : A, Decision (a = b)}. + Global Instance fn_insert : Insert A T (A → T) := + λ a t f b, if decide (a = b) then t else f b. + Global Instance fn_alter : Alter A T (A → T) := + λ (g : T → T) a f b, if decide (a = b) then g (f a) else f b. +End definitions. + +(* For now, we only have the properties here that do not need a notion + of equality of functions. *) + +Section functions. + Context {A T : Type} `{∀ a b : A, Decision (a = b)}. + + Lemma fn_lookup_insert (f : A → T) a t : <[a:=t]>f a = t. + Proof. unfold insert, fn_insert. by destruct (decide (a = a)). Qed. + Lemma fn_lookup_insert_rev (f : A → T) a t1 t2 : + <[a:=t1]>f a = t2 → t1 = t2. + Proof. rewrite fn_lookup_insert. congruence. Qed. + Lemma fn_lookup_insert_ne (f : A → T) a b t : a ≠ b → <[a:=t]>f b = f b. + Proof. unfold insert, fn_insert. by destruct (decide (a = b)). Qed. + + Lemma fn_lookup_alter (g : T → T) (f : A → T) a : alter g a f a = g (f a). + Proof. unfold alter, fn_alter. by destruct (decide (a = a)). Qed. + Lemma fn_lookup_alter_ne (g : T → T) (f : A → T) a b : + a ≠ b → alter g a f b = f b. + Proof. unfold alter, fn_alter. by destruct (decide (a = b)). Qed. + +End functions. -- GitLab