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
|
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.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 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]; [ reflexivity | ].
induction n as [|n IHn]; [ reflexivity | ].
{ unfold mapt in *; simpl @mapt' in *.
rewrite <- IHn; clear IHn.
rewrite <- (@Tuple.map_S n _ _ f); destruct ts; 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.
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.
Admitted.
End Tuple.
|
