From e2956617c26998eaee2d6228eac600f84136c285 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 16 May 2017 23:00:34 -0400 Subject: Add context_equiv and prove some Proper lemmas --- src/Compilers/Named/ContextDefinitions.v | 3 ++ src/Compilers/Named/ContextProperties/Proper.v | 46 ++++++++++++++++++++++++++ 2 files changed, 49 insertions(+) create mode 100644 src/Compilers/Named/ContextProperties/Proper.v (limited to 'src') diff --git a/src/Compilers/Named/ContextDefinitions.v b/src/Compilers/Named/ContextDefinitions.v index 79a3f2f1c..010cf1fca 100644 --- a/src/Compilers/Named/ContextDefinitions.v +++ b/src/Compilers/Named/ContextDefinitions.v @@ -58,4 +58,7 @@ Section with_context. : forall (ctx : Context) n t t', lookupb t' (removeb t ctx n) n = None; lookupb_empty : forall n t, lookupb t (@empty _ _ _ Context) n = None }. + + Definition context_equiv (a b : Context) + := forall n t, lookupb t a n = lookupb t b n. End with_context. diff --git a/src/Compilers/Named/ContextProperties/Proper.v b/src/Compilers/Named/ContextProperties/Proper.v new file mode 100644 index 000000000..0827ae233 --- /dev/null +++ b/src/Compilers/Named/ContextProperties/Proper.v @@ -0,0 +1,46 @@ +Require Import Coq.Classes.Morphisms. +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Named.Context. +Require Import Crypto.Compilers.Named.ContextDefinitions. +Require Import Crypto.Util.Decidable. + +Section with_context. + Context {base_type_code} + {base_type_code_dec : DecidableRel (@eq base_type_code)} + {Name} + {Name_dec : DecidableRel (@eq Name)} + {var} {Context : @Context base_type_code Name var} + {ContextOk : ContextOk Context}. + + Local Notation context_equiv := (@context_equiv base_type_code Name var Context). + Local Notation extendb := (@extendb base_type_code Name var Context). + Local Notation removeb := (@removeb base_type_code Name var Context). + Local Notation lookupb := (@lookupb base_type_code Name var Context). + + Global Instance context_equiv_Equivalence : Equivalence context_equiv | 10. + Proof. split; repeat intro; congruence. Qed. + Global Instance context_equiv_Reflexive : Reflexive context_equiv | 10 := _. + Global Instance context_equiv_Symmetric : Symmetric context_equiv | 10 := _. + Global Instance context_equiv_Transitive : Transitive context_equiv | 10 := _. + + Local Ltac proper_t n n' t t' := + destruct (dec (n = n')), (dec (t = t')); subst; + repeat first [ reflexivity + | rewrite lookupb_extendb_same by assumption + | rewrite lookupb_extendb_different by assumption + | rewrite lookupb_extendb_wrong_type by assumption + | rewrite lookupb_removeb_same by assumption + | rewrite lookupb_removeb_different by assumption + | solve [ auto ] ]. + + Global Instance extendb_Proper {t} : Proper (context_equiv ==> eq ==> eq ==> context_equiv) (@extendb t) | 10. + Proof. + intros ??? n n0 ???? n' t'; subst n0; subst; proper_t n n' t t'. + Qed. + Global Instance removeb_Proper {t} : Proper (context_equiv ==> eq ==> context_equiv) (@removeb t) | 10. + Proof. + intros ??? n n0 ? n' t'; subst n0; subst; proper_t n n' t t'. + Qed. + Global Instance lookupb_Proper {t} : Proper (context_equiv ==> eq ==> eq) (@lookupb t) | 10. + Proof. repeat intro; subst; auto. Qed. +End with_context. -- cgit v1.2.3