Add {m,o,}name_list_unique

1 files changed, 61 insertions, 0 deletions

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.