From 95f78be1b2750df00c2b6a83bbe6c6b117118afe Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 28 Feb 2017 15:14:19 -0500 Subject: Add eta_tuple functions These are for getting nicely reduced forms of, e.g., Tuple.map, without knowing exactly what the tuple is --- src/Util/Tuple.v | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) (limited to 'src/Util/Tuple.v') 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. -- cgit v1.2.3