diff options
author | Jason Gross <jgross@mit.edu> | 2017-03-22 17:11:59 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-03-22 17:11:59 -0400 |
commit | 4b68b853d4a8e8b819baa9208d8317182a70da5b (patch) | |
tree | 09b7723a718eadf2d8f4765f4ec7af3f8eb08e95 /src/Reflection | |
parent | 210224d83b3723fdb6e997cf7681d7591a8bf601 (diff) |
Add split_onames_split_names
Diffstat (limited to 'src/Reflection')
-rw-r--r-- | src/Reflection/Named/NameUtilProperties.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/Reflection/Named/NameUtilProperties.v b/src/Reflection/Named/NameUtilProperties.v index 597f6b16f..8dcf32ec5 100644 --- a/src/Reflection/Named/NameUtilProperties.v +++ b/src/Reflection/Named/NameUtilProperties.v @@ -200,4 +200,24 @@ Section language. destruct (le_lt_dec (count_pairs t) (List.length ls)); specialize_by omega; destruct (fst (split_names t ls)); split; try intuition (congruence || omega). Qed. + + Lemma split_onames_split_names (t : flat_type base_type_code) (ls : list Name) + : split_onames t (List.map Some ls) + = (fst (split_names t ls), List.map Some (snd (split_names t ls))). + Proof. + revert ls; induction t; + try solve [ destruct ls; reflexivity ]. + repeat first [ progress simpl in * + | progress intros + | rewrite snd_split_names_skipn + | rewrite snd_split_onames_skipn + | rewrite skipn_map + | match goal with + | [ H : forall ls, split_onames ?t (map Some ls) = _ |- context[split_onames ?t (map Some ?ls')] ] + => specialize (H ls') + end + | break_innermost_match_step + | progress inversion_prod + | congruence ]. + Qed. End language. |