functions.v 1.39 KB
Newer Older
1
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
2
(* This file is distributed under the terms of the BSD license. *)
3
From stdpp Require Export base tactics.
4
Set Default Proof Using "Type".
5 6

Section definitions.
7
  Context {A T : Type} `{EqDecision A}.
8 9 10 11
  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.
12 13
End definitions.

Ralf Jung's avatar
Ralf Jung committed
14
(* TODO: For now, we only have the properties here that do not need a notion
15 16 17
   of equality of functions. *)

Section functions.
18
  Context {A T : Type} `{!EqDecision A}.
19

20 21
  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.
22
  Lemma fn_lookup_insert_rev  (f : A  T) a t1 t2 :
23
    <[a:=t1]>f a = t2  t1 = t2.
24
  Proof. rewrite fn_lookup_insert. congruence. Qed.
25 26
  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.
27

28 29
  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.
30
  Lemma fn_lookup_alter_ne (g : T  T) (f : A  T) a b :
31 32
    a  b  alter g a f b = f b.
  Proof. unfold alter, fn_alter. by destruct (decide (a = b)). Qed.
33
End functions.