diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Compilers/Named/ContextDefinitions.v | 3 | ||||
| -rw-r--r-- | src/Compilers/Named/ContextProperties/Proper.v | 46 |
3 files changed, 50 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 0a151d30d..294d527fc 100644 --- a/_CoqProject +++ b/_CoqProject @@ -106,6 +106,7 @@ src/Compilers/Named/Wf.v src/Compilers/Named/WfFromUnit.v src/Compilers/Named/WfInterp.v src/Compilers/Named/ContextProperties/NameUtil.v +src/Compilers/Named/ContextProperties/Proper.v src/Compilers/Named/ContextProperties/SmartMap.v src/Compilers/Named/ContextProperties/Tactics.v src/Compilers/Named/PositiveContext/Defaults.v 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. |