diff options
Diffstat (limited to 'src/Compilers/Named/ContextProperties')
| -rw-r--r-- | src/Compilers/Named/ContextProperties/NameUtil.v | 10 | ||||
| -rw-r--r-- | src/Compilers/Named/ContextProperties/Proper.v | 25 |
2 files changed, 20 insertions, 15 deletions
diff --git a/src/Compilers/Named/ContextProperties/NameUtil.v b/src/Compilers/Named/ContextProperties/NameUtil.v index 0bc970357..320d910f0 100644 --- a/src/Compilers/Named/ContextProperties/NameUtil.v +++ b/src/Compilers/Named/ContextProperties/NameUtil.v @@ -47,7 +47,7 @@ Section with_context. : (exists t, @find_Name n T N = Some t) <-> List.In (Some n) (List.firstn (CountLets.count_pairs T) ls). Proof using Type. - revert dependent ls; intro ls; revert ls ls'; induction T; intros; + revert dependent ls; intro ls; revert ls ls'; induction T; intros ls ls' H; [ | | specialize (IHT1 (fst N) ls (snd (split_onames T1 ls))); specialize (IHT2 (snd N) (snd (split_onames T1 ls)) (snd (split_onames (T1 * T2) ls))) ]; repeat first [ misc_oname_t_step @@ -77,7 +77,11 @@ Section with_context. rewrite fst_split_onames_firstn, snd_split_onames_skipn in H. inversion_prod; subst. split; [ split | intros [? ?] ]; eauto using In_firstn, oname_list_unique_specialize. - eapply In_firstn_skipn_split in H; destruct_head' or; eauto; exfalso; eauto. + match goal with + | [ H : List.In (Some _) ?ls |- _ ] + => is_var ls; + eapply In_firstn_skipn_split in H; destruct_head' or; eauto; exfalso; eauto + end. Qed. Lemma split_onames_find_Name_Some_unique @@ -97,7 +101,7 @@ Section with_context. : @find_Name_and_val var' t n T N V None = Some v <-> List.In (existT (fun t => (Name * var' t)%type) t (n, v)) (Wf.flatten_binding_list N V). Proof using Type. - revert dependent ls; intro ls; revert ls ls'; induction T; intros; + revert dependent ls; intro ls; revert ls ls'; induction T; intros ls ls' Hls H; [ | | specialize (IHT1 (fst N) (fst V) ls (snd (split_onames T1 ls))); specialize (IHT2 (snd N) (snd V) (snd (split_onames T1 ls)) (snd (split_onames (T1 * T2) ls))) ]; repeat first [ find_Name_and_val_default_to_None_step diff --git a/src/Compilers/Named/ContextProperties/Proper.v b/src/Compilers/Named/ContextProperties/Proper.v index 48cecde8f..0c583e446 100644 --- a/src/Compilers/Named/ContextProperties/Proper.v +++ b/src/Compilers/Named/ContextProperties/Proper.v @@ -41,15 +41,15 @@ Section with_context. | rewrite lookupb_removeb_different by assumption | solve [ auto ] ]. - Global Instance extendb_Proper {t} : Proper (context_equiv ==> eq ==> eq ==> context_equiv) (@extendb t) | 10. + Global Instance extendb_Proper : forall {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'. + intros t ??? 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. + Global Instance removeb_Proper : forall {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'. + intros t ??? 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. + Global Instance lookupb_Proper : forall {t}, Proper (context_equiv ==> eq ==> eq) (@lookupb t) | 10. Proof. repeat intro; subst; auto. Qed. Local Ltac proper_t2 t := @@ -68,13 +68,14 @@ Section with_context. first [ eapply IHt2; [ eapply IHt1 | .. ]; auto | idtac ] ]. - Global Instance extend_Proper {t} : Proper (context_equiv ==> eq ==> eq ==> context_equiv) (@extend t) | 10. - Proof. proper_t2 t. Qed. - Global Instance remove_Proper {t} : Proper (context_equiv ==> eq ==> context_equiv) (@remove t) | 10. - Proof. proper_t2 t. Qed. - Global Instance lookup_Proper {t} : Proper (context_equiv ==> eq ==> eq) (@lookup t) | 10. + Global Instance extend_Proper : forall {t}, Proper (context_equiv ==> eq ==> eq ==> context_equiv) (@extend t) | 10. + Proof. intro t; proper_t2 t. Qed. + Global Instance remove_Proper : forall {t}, Proper (context_equiv ==> eq ==> context_equiv) (@remove t) | 10. + Proof. intro t; proper_t2 t. Qed. + + Global Instance lookup_Proper : forall {t}, Proper (context_equiv ==> eq ==> eq) (@lookup t) | 10. Proof. - proper_t2 t. + intro t; proper_t2 t. repeat match goal with | [ |- context G[lookup (?A * ?B) ?ctx (?na, ?nb)] ] => let G' := context G[match lookup A ctx na, lookup B ctx nb with @@ -88,7 +89,7 @@ Section with_context. | _ => progress subst | _ => progress inversion_option | _ => reflexivity - | [ H : lookup _ _ _ = ?x, H' : lookup _ _ _ = ?y |- _ ] + | [ IHt2 : Proper _ (lookup t2), H : lookup _ _ _ = ?x, H' : lookup _ _ _ = ?y |- _ ] => assert (x = y) by (rewrite <- H, <- H'; first [ eapply IHt1 | eapply IHt2 ]; (assumption || reflexivity)); clear H H' |