diff options
author | 2017-03-19 12:40:33 -0400 | |
---|---|---|
committer | 2017-03-19 12:40:33 -0400 | |
commit | d635e2e1b8d392644e92f44c5bac3fd2fc24ff36 (patch) | |
tree | 7520d63b4a229cee910a705de4d9e40a18febe58 /src | |
parent | 7dcfc8c1955aa1a75d08bf6f6e45dd274355b743 (diff) |
Add {m,o,}name_list_unique
Diffstat (limited to 'src')
-rw-r--r-- | src/Reflection/Named/NameUtil.v | 14 | ||||
-rw-r--r-- | src/Reflection/Named/NameUtilProperties.v | 61 |
2 files changed, 75 insertions, 0 deletions
diff --git a/src/Reflection/Named/NameUtil.v b/src/Reflection/Named/NameUtil.v index 9d910aaef..078449375 100644 --- a/src/Reflection/Named/NameUtil.v +++ b/src/Reflection/Named/NameUtil.v @@ -1,3 +1,4 @@ +Require Import Coq.Lists.List. Require Import Crypto.Reflection.Syntax. Local Open Scope core_scope. @@ -32,11 +33,24 @@ Section language. end, ls) end. + Definition mname_list_unique (ls : list MName) : Prop + := forall k n, + List.In (Some n) (firstn k (List.map force ls)) + -> List.In (Some n) (skipn k (List.map force ls)) + -> False. End monad. Definition split_onames := @split_mnames (option Name) (fun x => x). Definition split_names := @split_mnames Name (@Some _). + + Definition oname_list_unique (ls : list (option Name)) : Prop + := mname_list_unique (option Name) (fun x => x) ls. + Definition name_list_unique (ls : list Name) : Prop + := mname_list_unique Name (@Some _) ls. End language. Global Arguments split_mnames {_ _ MName} force _ _, {_ _} MName force _ _. Global Arguments split_onames {_ _} _ _. Global Arguments split_names {_ _} _ _. +Global Arguments mname_list_unique {_ MName} force ls, {_} MName force ls. +Global Arguments oname_list_unique {_} ls. +Global Arguments name_list_unique {_} ls. diff --git a/src/Reflection/Named/NameUtilProperties.v b/src/Reflection/Named/NameUtilProperties.v index d0ef26b1d..29529a34a 100644 --- a/src/Reflection/Named/NameUtilProperties.v +++ b/src/Reflection/Named/NameUtilProperties.v @@ -7,7 +7,10 @@ Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.RewriteHyp. Require Import Crypto.Util.Tactics.SplitInContext. Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.NatUtil. Require Import Crypto.Util.Prod. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.SplitInContext. Local Open Scope core_scope. Section language. @@ -56,6 +59,28 @@ Section language. (t : flat_type base_type_code) (ls : list MName) : fst (split_mnames force t ls) = fst (split_mnames force t (firstn (count_pairs t) ls)). Proof. rewrite split_mnames_firstn_skipn at 1; reflexivity. Qed. + + Lemma mname_list_unique_firstn_skipn n ls + : mname_list_unique force ls + -> (mname_list_unique force (firstn n ls) + /\ mname_list_unique force (skipn n ls)). + Proof. + unfold mname_list_unique; intro H; split; intros k N; + rewrite <- ?firstn_map, <- ?skipn_map, ?skipn_skipn, ?firstn_firstn_min, ?firstn_skipn_add; + intros; eapply H; try eassumption. + { apply Min.min_case_strong. + { match goal with H : _ |- _ => rewrite skipn_firstn in H end; + eauto using In_firstn. } + { intro; match goal with H : _ |- _ => rewrite skipn_all in H by (rewrite firstn_length; omega * ) end. + simpl in *; tauto. } } + { eauto using In_skipn. } + Qed. + Definition mname_list_unique_firstn n ls + : mname_list_unique force ls -> mname_list_unique force (firstn n ls) + := fun H => proj1 (@mname_list_unique_firstn_skipn n ls H). + Definition mname_list_unique_skipn n ls + : mname_list_unique force ls -> mname_list_unique force (skipn n ls) + := fun H => proj2 (@mname_list_unique_firstn_skipn n ls H). End monad. Lemma split_onames_firstn_skipn @@ -73,6 +98,24 @@ Section language. : fst (split_onames t ls) = fst (split_onames t (firstn (count_pairs t) ls)). Proof. apply fst_split_mnames_firstn. Qed. + Lemma oname_list_unique_firstn n (ls : list (option Name)) + : oname_list_unique ls -> oname_list_unique (firstn n ls). + Proof. apply mname_list_unique_firstn. Qed. + Lemma oname_list_unique_skipn n (ls : list (option Name)) + : oname_list_unique ls -> oname_list_unique (skipn n ls). + Proof. apply mname_list_unique_skipn. Qed. + Lemma oname_list_unique_specialize (ls : list (option Name)) + : oname_list_unique ls + -> forall k n, + List.In (Some n) (firstn k ls) + -> List.In (Some n) (skipn k ls) + -> False. + Proof. + intros H k n; specialize (H k n). + rewrite map_id in H; assumption. + Qed. + + Lemma split_names_firstn_skipn (t : flat_type base_type_code) (ls : list Name) : split_names t ls @@ -87,4 +130,22 @@ Section language. (t : flat_type base_type_code) (ls : list Name) : fst (split_names t ls) = fst (split_names t (firstn (count_pairs t) ls)). Proof. apply fst_split_mnames_firstn. Qed. + + Lemma name_list_unique_firstn n (ls : list Name) + : name_list_unique ls -> name_list_unique (firstn n ls). + Proof. apply mname_list_unique_firstn. Qed. + Lemma name_list_unique_skipn n (ls : list Name) + : name_list_unique ls -> name_list_unique (skipn n ls). + Proof. apply mname_list_unique_skipn. Qed. + Lemma name_list_unique_specialize (ls : list Name) + : name_list_unique ls + -> forall k n, + List.In n (firstn k ls) + -> List.In n (skipn k ls) + -> False. + Proof. + intros H k n; specialize (H k n). + rewrite firstn_map, skipn_map in H. + eauto using in_map. + Qed. End language. |