diff options
| -rw-r--r-- | src/Util/Tuple.v | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index b8a5c2738..bf0288ae4 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -633,6 +633,43 @@ Proof. apply IHn; auto. Qed. +Fixpoint eta_tuple'_dep {T n} : forall (P : tuple' T n -> Type), + (forall ts : tuple' T n, P ts) -> forall ts : tuple' T n, P ts + := match n with + | 0 => fun P f => f + | S n' => fun P f (ts : tuple' T n' * T) + => let '(ts', x) := ts in + @eta_tuple'_dep T n' (fun ts' => P (ts', x)) (fun ts'' => f (ts'', x)) ts' + end. +Definition eta_tuple' {T n B} : (tuple' T n -> B) -> (tuple' T n -> B) + := @eta_tuple'_dep T n (fun _ => B). +Definition eta_tuple_dep {T n} : forall (P : tuple T n -> Type), + (forall ts : tuple T n, P ts) -> forall ts : tuple T n, P ts + := match n with + | 0 => fun P f => f + | S n' => @eta_tuple'_dep T n' + end. +Definition eta_tuple {T n B} : (tuple T n -> B) -> (tuple T n -> B) + := @eta_tuple_dep T n (fun _ => B). + +Fixpoint eta_rtuple'_dep {T n} : forall (P : rtuple' T n -> Type), + (forall ts : rtuple' T n, P ts) -> forall ts : rtuple' T n, P ts + := match n with + | 0 => fun P f => f + | S n' => fun P f (ts : T * rtuple' T n') + => let '(x, ts') := ts in + @eta_rtuple'_dep T n' (fun ts' => P (x, ts')) (fun ts'' => f (x, ts'')) ts' + end. +Definition eta_rtuple' {T n B} : (rtuple' T n -> B) -> (rtuple' T n -> B) + := @eta_rtuple'_dep T n (fun _ => B). +Definition eta_rtuple_dep {T n} : forall (P : rtuple T n -> Type), + (forall ts : rtuple T n, P ts) -> forall ts : rtuple T n, P ts + := match n with + | 0 => fun P f => f + | S n' => @eta_rtuple'_dep T n' + end. +Definition eta_rtuple {T n B} : (rtuple T n -> B) -> (rtuple T n -> B) + := @eta_rtuple_dep T n (fun _ => B). Require Import Crypto.Util.ListUtil. (* To initialize [distr_length] database *) Hint Rewrite length_to_list' @length_to_list : distr_length. |