forked from vafeiadis/hahn
-
Notifications
You must be signed in to change notification settings - Fork 0
/
HahnFun.v
93 lines (67 loc) · 2.27 KB
/
HahnFun.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
(******************************************************************************)
(** * Function update *)
(******************************************************************************)
Require Import HahnBase List.
Set Implicit Arguments.
(** Function update *)
(******************************************************************************)
Section FunctionUpdate.
Variables (A B: Type).
Definition upd (f : A -> B) a b x :=
ifP x = a then b else f x.
Lemma upds f a b : upd f a b a = b.
Proof. unfold upd; desf. Qed.
Lemma updo f a b c (NEQ: c <> a) : upd f a b c = f c.
Proof. unfold upd; desf. Qed.
Lemma updss f l x y : upd (upd f l x) l y = upd f l y.
Proof.
extensionality z; unfold upd; desf.
Qed.
Lemma updC l l' (NEQ: l <> l') f x y :
upd (upd f l x) l' y = upd (upd f l' y) l x.
Proof.
extensionality z; unfold upd; desf.
Qed.
Lemma updI f a : upd f a (f a) = f.
Proof.
extensionality a'; unfold upd; desf.
Qed.
Lemma map_upd_irr a l (NIN: ~ In a l) f b :
map (upd f a b) l = map f l.
Proof.
unfold upd; induction l; ins.
apply not_or_and in NIN; desf; f_equal; eauto.
Qed.
End FunctionUpdate.
Ltac rupd := repeat first [rewrite upds | rewrite updo ; try done].
(** Decidable function update *)
(******************************************************************************)
Section DecidableUpdate.
Variables (A: eqType) (B: Type).
Definition mupd (f: A -> B) y z :=
fun x => if eq_op x y then z else f x.
Lemma mupds f x y : mupd f x y x = y.
Proof. by unfold mupd; desf; desf. Qed.
Lemma mupdo f x y z : x <> z -> mupd f x y z = f z.
Proof. by unfold mupd; desf; desf. Qed.
Lemma mupdss f l x y : mupd (mupd f l x) l y = mupd f l y.
Proof.
extensionality z; unfold mupd; desf; desf.
Qed.
Lemma mupdC l l' (NEQ: l <> l') f x y :
mupd (mupd f l x) l' y = mupd (mupd f l' y) l x.
Proof.
extensionality z; unfold mupd; desf; desf.
Qed.
Lemma mupdI f a : mupd f a (f a) = f.
Proof.
extensionality z; unfold mupd; desf; desf.
Qed.
Lemma map_mupd_irr a l (NIN: ~ In a l) f b :
map (mupd f a b) l = map f l.
Proof.
unfold mupd; induction l; ins.
apply not_or_and in NIN; desf; desf; f_equal; eauto.
Qed.
End DecidableUpdate.
Arguments mupd [A B] f y z x.