diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-22 17:04:27 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-22 17:04:27 -0400 |
| commit | 210224d83b3723fdb6e997cf7681d7591a8bf601 (patch) | |
| tree | 1530466de4bd8a843174ed9d73d6f2ef6764b5e0 /src/Reflection/Named | |
| parent | 055d75c242af8cbf49f767ca0e3636ae3c257ae0 (diff) | |
Add length_fst_split_names_None_iff
Diffstat (limited to 'src/Reflection/Named')
| -rw-r--r-- | src/Reflection/Named/NameUtilProperties.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/Reflection/Named/NameUtilProperties.v b/src/Reflection/Named/NameUtilProperties.v index f54b315f8..597f6b16f 100644 --- a/src/Reflection/Named/NameUtilProperties.v +++ b/src/Reflection/Named/NameUtilProperties.v @@ -1,4 +1,5 @@ Require Import Coq.omega.Omega. +Require Import Coq.Arith.Arith. Require Import Coq.Lists.List. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.CountLets. @@ -190,4 +191,13 @@ Section language. | [ |- iff _ _ ] => split end ]. Qed. + + Lemma length_fst_split_names_None_iff + (t : flat_type base_type_code) (ls : list Name) + : fst (split_names t ls) = None <-> List.length ls < count_pairs t. + Proof. + destruct (length_fst_split_names_Some_iff t ls). + 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. End language. |