functions.v 2.59 KB
 Ralf Jung committed Feb 16, 2016 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 ``````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. `````` Ralf Jung committed Feb 22, 2016 32 33 `````` (** "Cons-ing" of functions from nat to T *) `````` Ralf Jung committed Feb 22, 2016 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 ``````(* Coq's standard lists are not universe polymorphic. Hence we have to re-define them. Ouch. TODO: If we decide to end up going with this, we should move this elsewhere. *) Polymorphic Inductive plist {A : Type} : Type := | pnil : plist | pcons: A → plist → plist. Arguments plist : clear implicits. Polymorphic Fixpoint papp {A : Type} (l1 l2 : plist A) : plist A := match l1 with | pnil => l2 | pcons a l => pcons a (papp l l2) end. (* TODO: Notation is totally up for debate. *) Infix "`::`" := pcons (at level 60, right associativity) : C_scope. Infix "`++`" := papp (at level 60, right associativity) : C_scope. `````` Ralf Jung committed Feb 22, 2016 51 52 53 54 55 ``````Polymorphic Definition fn_cons {T : Type} (t : T) (f: nat → T) : nat → T := λ n, match n with | O => t | S n => f n end. `````` Ralf Jung committed Feb 22, 2016 56 `````` `````` Ralf Jung committed Feb 22, 2016 57 58 59 60 61 ``````Polymorphic Fixpoint fn_mcons {T : Type} (ts : plist T) (f : nat → T) : nat → T := match ts with | pnil => f | pcons t ts => fn_cons t (fn_mcons ts f) end. `````` Ralf Jung committed Feb 22, 2016 62 `````` `````` Ralf Jung committed Feb 22, 2016 63 ``````(* TODO: Notation is totally up for debate. *) `````` Ralf Jung committed Feb 22, 2016 64 65 66 ``````Infix ".::" := fn_cons (at level 60, right associativity) : C_scope. Infix ".++" := fn_mcons (at level 60, right associativity) : C_scope. `````` Ralf Jung committed Feb 22, 2016 67 68 ``````Polymorphic Lemma fn_mcons_app {T : Type} (ts1 ts2 : plist T) f : (ts1 `++` ts2) .++ f = ts1 .++ (ts2 .++ f). `````` Ralf Jung committed Feb 22, 2016 69 ``````Proof. `````` Ralf Jung committed Feb 22, 2016 70 `````` induction ts1; simpl; eauto. congruence. `````` Ralf Jung committed Feb 22, 2016 71 ``Qed.``