From 5cefabfee05c2a5a9d4d3a5fdcb98250b0a18780 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 14 Mar 2017 21:19:05 -0400 Subject: Add NameUtilProperties --- src/Reflection/Named/NameUtilProperties.v | 40 +++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 src/Reflection/Named/NameUtilProperties.v (limited to 'src/Reflection') 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. -- cgit v1.2.3