aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/Named
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-03-19 16:54:34 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-03-19 16:54:34 -0400
commit6a3c0d90e968c60fd655ef00d0a382987cbbea39 (patch)
treeb06385a779aa234044c34f4348a8f783fb38de6c /src/Reflection/Named
parent2849fff1a54905c344f42a5ce1cda726cdbc0516 (diff)
Add Named/PositiveContext/DefaultsProperties.v
Diffstat (limited to 'src/Reflection/Named')
-rw-r--r--src/Reflection/Named/PositiveContext/DefaultsProperties.v38
1 files changed, 38 insertions, 0 deletions
diff --git a/src/Reflection/Named/PositiveContext/DefaultsProperties.v b/src/Reflection/Named/PositiveContext/DefaultsProperties.v
new file mode 100644
index 000000000..0fb1254ce
--- /dev/null
+++ b/src/Reflection/Named/PositiveContext/DefaultsProperties.v
@@ -0,0 +1,38 @@
+Require Import Coq.Lists.List.
+Require Import Coq.Numbers.BinNums.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Named.PositiveContext.
+Require Import Crypto.Reflection.CountLets.
+Require Import Crypto.Reflection.Named.NameUtil.
+Require Import Crypto.Reflection.Named.PositiveContext.Defaults.
+Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Util.NatUtil.
+Require Import Crypto.Util.Tactics.DestructHead.
+
+Section language.
+ Context {base_type_code : Type}
+ {op : flat_type base_type_code -> flat_type base_type_code -> Type}.
+
+ Lemma name_list_unique_map_pos_of_succ_nat_seq a b
+ : name_list_unique (map BinPos.Pos.of_succ_nat (seq a b)).
+ Proof.
+ unfold name_list_unique, oname_list_unique, mname_list_unique.
+ intros k n.
+ rewrite !map_map, firstn_map, skipn_map, firstn_seq, skipn_seq.
+ rewrite !in_map_iff; intros; destruct_head' ex; destruct_head' and; inversion_option; subst.
+ match goal with H : _ |- _ => apply Pnat.SuccNat2Pos.inj in H end; subst.
+ rewrite in_seq in *.
+ omega *.
+ Qed.
+
+ Lemma name_list_unique_default_names_forf {var dummy t e}
+ : name_list_unique (@default_names_forf base_type_code op var dummy t e).
+ Proof. apply name_list_unique_map_pos_of_succ_nat_seq. Qed.
+ Lemma name_list_unique_default_names_for {var dummy t e}
+ : name_list_unique (@default_names_for base_type_code op var dummy t e).
+ Proof. apply name_list_unique_map_pos_of_succ_nat_seq. Qed.
+ Lemma name_list_unique_DefaultNamesFor {t e}
+ : name_list_unique (@DefaultNamesFor base_type_code op t e).
+ Proof. apply name_list_unique_map_pos_of_succ_nat_seq. Qed.
+End language.