Commit 2f8fd311 authored by Ralf Jung's avatar Ralf Jung
Browse files

add some basic theory about pointwise updates of total functions

parent a2af977f
From stdpp 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