diff options
author | Jason Gross <jgross@mit.edu> | 2017-03-14 21:19:05 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-03-14 21:19:05 -0400 |
commit | 5cefabfee05c2a5a9d4d3a5fdcb98250b0a18780 (patch) | |
tree | 325e4a55dffc074e43b92ef7bf08cae61e810389 | |
parent | b2e1bc62fc9d572c0a5cb57953b12c7a0ceace4b (diff) |
Add NameUtilProperties
-rw-r--r-- | _CoqProject | 1 | ||||
-rw-r--r-- | src/Reflection/Named/NameUtilProperties.v | 40 |
2 files changed, 41 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index d6d27dd56..2e48ee0b5 100644 --- a/_CoqProject +++ b/_CoqProject @@ -162,6 +162,7 @@ src/Reflection/Named/InterpretToPHOAS.v src/Reflection/Named/InterpretToPHOASInterp.v src/Reflection/Named/InterpretToPHOASWf.v src/Reflection/Named/NameUtil.v +src/Reflection/Named/NameUtilProperties.v src/Reflection/Named/PositiveContext.v src/Reflection/Named/RegisterAssign.v src/Reflection/Named/SmartMap.v diff --git a/src/Reflection/Named/NameUtilProperties.v b/src/Reflection/Named/NameUtilProperties.v new file mode 100644 index 000000000..499b6f80a --- /dev/null +++ b/src/Reflection/Named/NameUtilProperties.v @@ -0,0 +1,40 @@ +Require Import Coq.Lists.List. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.CountLets. +Require Import Crypto.Reflection.Named.NameUtil. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.RewriteHyp. +Require Import Crypto.Util.ListUtil. + +Local Open Scope core_scope. +Section language. + Context {base_type_code : Type} + {Name : Type}. + + Section monad. + Context (MName : Type) (force : MName -> option Name). + + Lemma snd_split_mnames_skipn + (t : flat_type base_type_code) (ls : list MName) + : snd (split_mnames force t ls) = skipn (count_pairs t) ls. + Proof. + revert ls; induction t; + repeat first [ progress simpl in * + | progress intros + | rewrite <- skipn_skipn + | reflexivity + | progress break_innermost_match_step + | rewrite_hyp !* ]. + Qed. + End monad. + + Lemma snd_split_onames_skipn + (t : flat_type base_type_code) (ls : list (option Name)) + : snd (split_onames t ls) = skipn (count_pairs t) ls. + Proof. apply snd_split_mnames_skipn. Qed. + + Lemma snd_split_names_skipn + (t : flat_type base_type_code) (ls : list Name) + : snd (split_names t ls) = skipn (count_pairs t) ls. + Proof. apply snd_split_mnames_skipn. Qed. +End language. |