From de0a4ce7d93437aa8229308cd06cd95f27f58809 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 17 Nov 2016 16:54:26 -0500 Subject: Update AddCoordinates Now the _correct_and_bounded lemma goes through --- src/Util/Tower.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'src/Util/Tower.v') diff --git a/src/Util/Tower.v b/src/Util/Tower.v index 6bcd44bf4..e3f57f3ed 100644 --- a/src/Util/Tower.v +++ b/src/Util/Tower.v @@ -1,5 +1,22 @@ Require Export Crypto.Util.FixCoqMistakes. +Definition apply4 {AK BK PA PB ARR} + (F : forall (A : AK) (B : BK), (PA A -> PB B) -> PB (ARR A B)) + {A0 A1 A2 A3 : AK} {B : BK} + (f : PA A0 -> PA A1 -> PA A2 -> PA A3 -> PB B) + : PB (ARR A0 (ARR A1 (ARR A2 (ARR A3 B)))). +Proof. + repeat (apply F; intro); apply f; assumption. +Defined. + +Definition apply4_nd {BK PA PB ARR} + (F : forall (B : BK), (PA -> PB B) -> PB (ARR B)) + {B : BK} + (f : PA -> PA -> PA -> PA -> PB B) + : PB (ARR (ARR (ARR (ARR B)))) + := @apply4 unit BK (fun _ => PA) PB (fun _ => ARR) (fun _ => F) + tt tt tt tt B f. + Definition apply9 {AK BK PA PB ARR} (F : forall (A : AK) (B : BK), (PA A -> PB B) -> PB (ARR A B)) {A0 A1 A2 A3 A4 A5 A6 A7 A8 : AK} {B : BK} -- cgit v1.2.3