Commit 24a71fb3 by Ralf Jung

### add some basic theory about pointwise updates of total functions

parent 730a39a3
 ... @@ -34,6 +34,7 @@ prelude/sets.v ... @@ -34,6 +34,7 @@ prelude/sets.v prelude/decidable.v prelude/decidable.v prelude/list.v prelude/list.v prelude/error.v prelude/error.v prelude/functions.v algebra/option.v algebra/option.v algebra/cmra.v algebra/cmra.v algebra/cmra_big_op.v algebra/cmra_big_op.v ... ...
 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.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment