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
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
|
Require Import Coq.Classes.Morphisms.
Require Import Coq.Relations.Relation_Definitions.
Require Import Coq.Lists.List.
Require Import Crypto.Util.Decidable.
Require Import Crypto.Util.ListUtil.
Require Import Crypto.Util.IffT.
Require Import Crypto.Util.Tuple.
Require Export Crypto.Util.FixCoqMistakes.
Fixpoint hlist' T n (f : T -> Type) : tuple' T n -> Type :=
match n return tuple' _ n -> Type with
| 0 => fun T => f T
| S n' => fun Ts => (hlist' T n' f (fst Ts) * f (snd Ts))%type
end.
Global Arguments hlist' {T n} f _.
Definition hlist {T n} (f : T -> Type) : forall (Ts : tuple T n), Type :=
match n return tuple _ n -> Type with
| 0 => fun _ => unit
| S n' => @hlist' T n' f
end.
Fixpoint hlistP' T n (f : T -> Prop) : tuple' T n -> Prop :=
match n return tuple' _ n -> Prop with
| 0 => fun T => f T
| S n' => fun Ts => (hlistP' T n' f (fst Ts) /\ f (snd Ts))%type
end.
Global Arguments hlistP' {T n} f _.
Definition hlistP {T n} (f : T -> Prop) : forall (Ts : tuple T n), Prop :=
match n return tuple _ n -> Prop with
| 0 => fun _ => True
| S n' => @hlistP' T n' f
end.
Fixpoint rhlist' T n (f : T -> Type) : rtuple' T n -> Type :=
match n return rtuple' _ n -> Type with
| 0 => fun T => f T
| S n' => fun Ts => (f (fst Ts) * rhlist' T n' f (snd Ts))%type
end.
Global Arguments rhlist' {T n} f _.
Definition rhlist {T n} (f : T -> Type) : forall (Ts : rtuple T n), Type :=
match n return rtuple _ n -> Type with
| 0 => fun _ => unit
| S n' => @rhlist' T n' f
end.
Fixpoint const' {T n F xs} (v : forall x, F x) : @hlist' T n F xs
:= match n return forall xs, @hlist' T n F xs with
| 0 => fun _ => v _
| S n' => fun _ => (@const' T n' F _ v, v _)
end xs.
Definition const {T n F xs} (v : forall x, F x) : @hlist T n F xs
:= match n return forall xs, @hlist T n F xs with
| 0 => fun _ => tt
| S n' => fun xs => @const' T n' F xs v
end xs.
(* tuple map *)
Fixpoint mapt' {n A F B} (f : forall x : A, F x -> B) : forall {ts : tuple' A n}, hlist' F ts -> tuple' B n
:= match n return forall ts : tuple' A n, hlist' F ts -> tuple' B n with
| 0 => fun ts v => f _ v
| S n' => fun ts v => (@mapt' n' A F B f _ (fst v), f _ (snd v))
end.
Definition mapt {n A F B} (f : forall x : A, F x -> B)
: forall {ts : tuple A n}, hlist F ts -> tuple B n
:= match n return forall ts : tuple A n, hlist F ts -> tuple B n with
| 0 => fun ts v => tt
| S n' => @mapt' n' A F B f
end.
Lemma map'_mapt' {n A F B C} (g : B -> C) (f : forall x : A, F x -> B)
{ts : tuple' A n} (ls : hlist' F ts)
: Tuple.map (n:=S n) g (mapt' f ls) = mapt' (fun x v => g (f x v)) ls.
Proof.
induction n as [|n IHn]; [ reflexivity | ].
{ simpl @mapt' in *.
rewrite <- IHn.
rewrite Tuple.map_S; reflexivity. }
Qed.
Lemma map_mapt {n A F B C} (g : B -> C) (f : forall x : A, F x -> B)
{ts : tuple A n} (ls : hlist F ts)
: Tuple.map g (mapt f ls) = mapt (fun x v => g (f x v)) ls.
Proof.
destruct n as [|n]; [ reflexivity | ].
apply map'_mapt'.
Qed.
Lemma map_is_mapt {n A F B} (f : A -> B) {ts : tuple A n} (ls : hlist F ts)
: Tuple.map f ts = mapt (fun x _ => f x) ls.
Proof.
destruct n as [|n]; simpl; [ destruct ts; reflexivity | ].
induction n as [|n IHn]; [ reflexivity | ].
{ simpl in *; rewrite <- IHn; clear IHn.
reflexivity. }
Qed.
Lemma map_is_mapt' {n A F B} (f : A -> B) {ts : tuple A (S n)} (ls : hlist' F ts)
: Tuple.map f ts = mapt' (fun x _ => f x) ls.
Proof. apply (@map_is_mapt (S n)). Qed.
Lemma hlist'_impl {n A F G} (xs:tuple' A n)
: (hlist' (fun x => F x -> G x) xs) -> (hlist' F xs -> hlist' G xs).
Proof.
induction n; simpl in *; intuition.
Defined.
Lemma hlist_impl {n A F G} (xs:tuple A n)
: (hlist (fun x => F x -> G x) xs) -> (hlist F xs -> hlist G xs).
Proof.
destruct n; [ constructor | apply hlist'_impl ].
Defined.
Local Arguments Tuple.map : simpl never.
Lemma hlist_map {n A B F} {f:A -> B} (xs:tuple A n)
: hlist F (Tuple.map f xs) = hlist (fun x => F (f x)) xs.
Proof.
destruct n as [|n]; [ reflexivity | ].
induction n; [ reflexivity | ].
specialize (IHn (fst xs)).
destruct xs; rewrite Tuple.map_S.
simpl @hlist in *; rewrite <- IHn.
reflexivity.
Qed.
Lemma fold_right_and_True_hlist' {n A F} (xs:tuple' A n)
: iffT (List.fold_right and True (List.map F (Tuple.to_list' _ xs))) (hlist' F xs).
Proof.
induction n.
{ simpl; tauto. }
{ specialize (IHn (fst xs)).
destruct xs; simpl in *.
tauto. }
Qed.
Lemma fold_right_and_True_hlist {n A F} (xs:tuple A n)
: iffT (List.fold_right and True (List.map F (Tuple.to_list _ xs))) (hlist F xs).
Proof.
destruct n; [ simpl; tauto | apply fold_right_and_True_hlist' ].
Qed.
Global Instance mapt_Proper
: forall {n A F B},
Proper
((forall_relation (fun x => pointwise_relation _ Logic.eq))
==> forall_relation (fun ts => Logic.eq ==> Logic.eq))
(@mapt n A F B).
Proof.
intro n; unfold forall_relation, pointwise_relation, respectful.
repeat intro; subst; destruct n as [|n]; [ reflexivity | ].
induction n; simpl in *; congruence.
Qed.
Module Tuple.
Lemma map_id_ext {n A} (f : A -> A) (xs:tuple A n)
: hlist (fun x => f x = x) xs -> Tuple.map f xs = xs.
Proof.
destruct n as [|n]; [cbv in *; destruct xs; trivial|].
induction n as [|n IHn]; [cbv in *;trivial|].
simpl in *. destruct xs. simpl in *; intros [??].
rewrite map_S. eauto using f_equal2.
Qed.
End Tuple.
|
