blob: 2b46de13660bda0c00dbd8fbccad642fa51079df (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
Require Import Coq.Lists.List.
Require Import Coq.Numbers.BinNums.
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Named.PositiveContext.
Require Import Crypto.Compilers.CountLets.
Require Import Crypto.Compilers.Named.NameUtil.
Require Import Crypto.Compilers.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 using Type.
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 using Type. 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 using Type. 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 using Type. apply name_list_unique_map_pos_of_succ_nat_seq. Qed.
End language.
|
