diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/AddCoordinates.v | 18 | ||||
| -rw-r--r-- | src/Util/Tower.v | 18 |
3 files changed, 20 insertions, 17 deletions
diff --git a/_CoqProject b/_CoqProject index 09f5d5223..11d34e925 100644 --- a/_CoqProject +++ b/_CoqProject @@ -345,6 +345,7 @@ src/Util/Relations.v src/Util/Sigma.v src/Util/Sum.v src/Util/Tactics.v +src/Util/Tower.v src/Util/Tuple.v src/Util/Unit.v src/Util/WordUtil.v diff --git a/src/Specific/GF25519Reflective/Reified/AddCoordinates.v b/src/Specific/GF25519Reflective/Reified/AddCoordinates.v index 99cac74e0..9f6662dcc 100644 --- a/src/Specific/GF25519Reflective/Reified/AddCoordinates.v +++ b/src/Specific/GF25519Reflective/Reified/AddCoordinates.v @@ -23,27 +23,11 @@ Require Import Crypto.Specific.GF25519Reflective.Reified.Mul. Require Import Crypto.Specific.GF25519Reflective.CommonBinOp. Require Import Crypto.Util.LetIn. Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.Tower. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. Require Import Bedrock.Word. -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} - (f : PA A0 -> PA A1 -> PA A2 -> PA A3 -> PA A4 -> PA A5 -> PA A6 -> PA A7 -> PA A8 -> PB B) - : PB (ARR A0 (ARR A1 (ARR A2 (ARR A3 (ARR A4 (ARR A5 (ARR A6 (ARR A7 (ARR A8 B))))))))). -Proof. - repeat (apply F; intro); apply f; assumption. -Defined. - -Definition apply9_nd {BK PA PB ARR} - (F : forall (B : BK), (PA -> PB B) -> PB (ARR B)) - {B : BK} - (f : PA -> PA -> PA -> PA -> PA -> PA -> PA -> PA -> PA -> PB B) - : PB (ARR (ARR (ARR (ARR (ARR (ARR (ARR (ARR (ARR B))))))))) - := @apply9 unit BK (fun _ => PA) PB (fun _ => ARR) (fun _ => F) - tt tt tt tt tt tt tt tt tt B f. - Definition radd_coordinatesZ' var twice_d P1 P2 := @Extended.add_coordinates_gen _ diff --git a/src/Util/Tower.v b/src/Util/Tower.v new file mode 100644 index 000000000..6bcd44bf4 --- /dev/null +++ b/src/Util/Tower.v @@ -0,0 +1,18 @@ +Require Export Crypto.Util.FixCoqMistakes. + +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} + (f : PA A0 -> PA A1 -> PA A2 -> PA A3 -> PA A4 -> PA A5 -> PA A6 -> PA A7 -> PA A8 -> PB B) + : PB (ARR A0 (ARR A1 (ARR A2 (ARR A3 (ARR A4 (ARR A5 (ARR A6 (ARR A7 (ARR A8 B))))))))). +Proof. + repeat (apply F; intro); apply f; assumption. +Defined. + +Definition apply9_nd {BK PA PB ARR} + (F : forall (B : BK), (PA -> PB B) -> PB (ARR B)) + {B : BK} + (f : PA -> PA -> PA -> PA -> PA -> PA -> PA -> PA -> PA -> PB B) + : PB (ARR (ARR (ARR (ARR (ARR (ARR (ARR (ARR (ARR B))))))))) + := @apply9 unit BK (fun _ => PA) PB (fun _ => ARR) (fun _ => F) + tt tt tt tt tt tt tt tt tt B f. |