aboutsummaryrefslogtreecommitdiff
path: root/src/Specific
diff options
context:
space:
mode:
Diffstat (limited to 'src/Specific')
-rw-r--r--src/Specific/ArithmeticSynthesisTest.v14
-rw-r--r--src/Specific/ArithmeticSynthesisTest130.v10
-rw-r--r--src/Specific/IntegrationTestFreeze.v2
-rw-r--r--src/Specific/IntegrationTestLadderstep.v2
-rw-r--r--src/Specific/IntegrationTestLadderstep130.v2
-rw-r--r--src/Specific/IntegrationTestMul.v2
-rw-r--r--src/Specific/IntegrationTestSquare.v2
-rw-r--r--src/Specific/IntegrationTestSub.v2
8 files changed, 18 insertions, 18 deletions
diff --git a/src/Specific/ArithmeticSynthesisTest.v b/src/Specific/ArithmeticSynthesisTest.v
index d9e801a0c..fa520f16c 100644
--- a/src/Specific/ArithmeticSynthesisTest.v
+++ b/src/Specific/ArithmeticSynthesisTest.v
@@ -115,7 +115,7 @@ Section Ops51.
let eval := Positional.Fdecode (m:=m) wt in
eval (add a b) = (eval a + eval b)%F }.
Proof.
- eexists; cbv beta zeta; intros.
+ eexists; cbv beta zeta; intros a b.
pose proof wt_nonzero.
let x := constr:(
Positional.add_cps (n := sz) wt a b id) in
@@ -128,7 +128,7 @@ Section Ops51.
let eval := Positional.Fdecode (m:=m) wt in
eval (sub a b) = (eval a - eval b)%F}.
Proof.
- eexists; cbv beta zeta; intros.
+ eexists; cbv beta zeta; intros a b.
pose proof wt_nonzero.
let x := constr:(
Positional.sub_cps (n:=sz) (coef := coef) wt a b id) in
@@ -141,7 +141,7 @@ Section Ops51.
let eval := Positional.Fdecode (m := m) wt in
eval (opp a) = F.opp (eval a)}.
Proof.
- eexists; cbv beta zeta; intros.
+ eexists; cbv beta zeta; intros a.
pose proof wt_nonzero.
let x := constr:(
Positional.opp_cps (n:=sz) (coef := coef) wt a id) in
@@ -154,7 +154,7 @@ Section Ops51.
let eval := Positional.Fdecode (m := m) wt in
eval (mul a b) = (eval a * eval b)%F}.
Proof.
- eexists; cbv beta zeta; intros.
+ eexists; cbv beta zeta; intros a b.
pose proof wt_nonzero.
let x := constr:(
Positional.mul_cps (n:=sz) (m:=sz2) wt a b
@@ -190,7 +190,7 @@ Section Ops51.
let eval := Positional.Fdecode (m := m) wt in
eval (square a) = (eval a * eval a)%F}.
Proof.
- eexists; cbv beta zeta; intros.
+ eexists; cbv beta zeta; intros a.
pose proof wt_nonzero.
let x := constr:(
Positional.mul_cps (n:=sz) (m:=sz2) wt a a
@@ -221,7 +221,7 @@ Section Ops51.
let eval := Positional.Fdecode (m := m) wt in
eval (carry a) = eval a}.
Proof.
- eexists; cbv beta zeta; intros.
+ eexists; cbv beta zeta; intros a.
pose proof wt_nonzero. pose proof wt_divides_chain1.
pose proof div_mod. pose proof wt_divides_chain2.
let x := constr:(
@@ -262,7 +262,7 @@ Section Ops51.
let eval := Positional.Fdecode (m := m) wt in
eval (freeze a) = eval a}.
Proof.
- eexists; cbv beta zeta; intros.
+ eexists; cbv beta zeta; intros a ?.
pose proof wt_nonzero. pose proof wt_pos.
pose proof div_mod. pose proof wt_divides_full_pos.
pose proof wt_multiples.
diff --git a/src/Specific/ArithmeticSynthesisTest130.v b/src/Specific/ArithmeticSynthesisTest130.v
index 6454bfbf1..15485499b 100644
--- a/src/Specific/ArithmeticSynthesisTest130.v
+++ b/src/Specific/ArithmeticSynthesisTest130.v
@@ -115,7 +115,7 @@ Section Ops51.
let eval := Positional.Fdecode (m:=m) wt in
eval (add a b) = (eval a + eval b)%F }.
Proof.
- eexists; cbv beta zeta; intros.
+ eexists; cbv beta zeta; intros a b.
pose proof wt_nonzero.
let x := constr:(
Positional.add_cps (n := sz) wt a b id) in
@@ -128,7 +128,7 @@ Section Ops51.
let eval := Positional.Fdecode (m:=m) wt in
eval (sub a b) = (eval a - eval b)%F}.
Proof.
- eexists; cbv beta zeta; intros.
+ eexists; cbv beta zeta; intros a b.
pose proof wt_nonzero.
let x := constr:(
Positional.sub_cps (n:=sz) (coef := coef) wt a b id) in
@@ -141,7 +141,7 @@ Section Ops51.
let eval := Positional.Fdecode (m := m) wt in
eval (opp a) = F.opp (eval a)}.
Proof.
- eexists; cbv beta zeta; intros.
+ eexists; cbv beta zeta; intros a.
pose proof wt_nonzero.
let x := constr:(
Positional.opp_cps (n:=sz) (coef := coef) wt a id) in
@@ -154,7 +154,7 @@ Section Ops51.
let eval := Positional.Fdecode (m := m) wt in
eval (mul a b) = (eval a * eval b)%F}.
Proof.
- eexists; cbv beta zeta; intros.
+ eexists; cbv beta zeta; intros a b.
pose proof wt_nonzero.
let x := constr:(
Positional.mul_cps (n:=sz) (m:=sz2) wt a b
@@ -176,7 +176,7 @@ Section Ops51.
let eval := Positional.Fdecode (m := m) wt in
eval (carry a) = eval a}.
Proof.
- eexists; cbv beta zeta; intros.
+ eexists; cbv beta zeta; intros a.
pose proof wt_nonzero. pose proof wt_divides_chain1.
pose proof div_mod. pose proof wt_divides_chain2.
let x := constr:(
diff --git a/src/Specific/IntegrationTestFreeze.v b/src/Specific/IntegrationTestFreeze.v
index 63cc76fc2..b9fad0e12 100644
--- a/src/Specific/IntegrationTestFreeze.v
+++ b/src/Specific/IntegrationTestFreeze.v
@@ -51,7 +51,7 @@ Section BoundedField25p5.
| [ |- { f | forall a, ?phi (f a) = @?rhs a } ]
=> apply lift1_sig with (P:=fun a f => phi f = rhs a)
end.
- intros.
+ intros a.
eexists_sig_etransitivity. all:cbv [phi].
rewrite <- (proj2_sig freeze_sig).
{ set (freezeZ := proj1_sig freeze_sig).
diff --git a/src/Specific/IntegrationTestLadderstep.v b/src/Specific/IntegrationTestLadderstep.v
index 06cd4f808..b88370a48 100644
--- a/src/Specific/IntegrationTestLadderstep.v
+++ b/src/Specific/IntegrationTestLadderstep.v
@@ -92,7 +92,7 @@ Section BoundedField25p5.
| forall a24 x1 Q Q', let eval := B.Positional.Fdecode wt in Tuple.map (n:=2) (Tuple.map (n:=2) eval) (xzladderstep a24 x1 Q Q') = FMxzladderstep (eval a24) (eval x1) (Tuple.map (n:=2) eval Q) (Tuple.map (n:=2) eval Q') }.
Proof.
exists Mxzladderstep.
- intros.
+ intros a24 x1 Q Q' eval.
cbv [Mxzladderstep FMxzladderstep M.donnaladderstep].
destruct Q, Q'; cbv [map map' fst snd Let_In eval].
repeat rewrite ?(proj2_sig add_sig), ?(proj2_sig mul_sig), ?(proj2_sig square_sig), ?(proj2_sig sub_sig), ?(proj2_sig carry_sig).
diff --git a/src/Specific/IntegrationTestLadderstep130.v b/src/Specific/IntegrationTestLadderstep130.v
index c8e3ba2b8..541dcaee8 100644
--- a/src/Specific/IntegrationTestLadderstep130.v
+++ b/src/Specific/IntegrationTestLadderstep130.v
@@ -57,7 +57,7 @@ Section BoundedField25p5.
| forall a24 x1 Q Q', let eval := B.Positional.Fdecode wt in Tuple.map (n:=2) (Tuple.map (n:=2) eval) (xzladderstep a24 x1 Q Q') = FMxzladderstep (eval a24) (eval x1) (Tuple.map (n:=2) eval Q) (Tuple.map (n:=2) eval Q') }.
Proof.
exists (@M.xzladderstep _ (proj1_sig add_sig) (proj1_sig sub_sig) (fun x y => proj1_sig carry_sig (proj1_sig mul_sig x y))).
- intros.
+ intros a24 x1 Q Q' eval.
cbv [FMxzladderstep M.xzladderstep].
destruct Q, Q'; cbv [map map' fst snd Let_In eval].
repeat rewrite ?(proj2_sig add_sig), ?(proj2_sig mul_sig), ?(proj2_sig sub_sig), ?(proj2_sig carry_sig).
diff --git a/src/Specific/IntegrationTestMul.v b/src/Specific/IntegrationTestMul.v
index 0cbc3966e..01d629bfb 100644
--- a/src/Specific/IntegrationTestMul.v
+++ b/src/Specific/IntegrationTestMul.v
@@ -50,7 +50,7 @@ Section BoundedField25p5.
| [ |- { f | forall a b, ?phi (f a b) = @?rhs a b } ]
=> apply lift2_sig with (P:=fun a b f => phi f = rhs a b)
end.
- intros.
+ intros a b.
eexists_sig_etransitivity. all:cbv [phi].
rewrite <- (proj2_sig mul_sig).
symmetry; rewrite <- (proj2_sig carry_sig); symmetry.
diff --git a/src/Specific/IntegrationTestSquare.v b/src/Specific/IntegrationTestSquare.v
index eb91a13ff..d7d717c61 100644
--- a/src/Specific/IntegrationTestSquare.v
+++ b/src/Specific/IntegrationTestSquare.v
@@ -50,7 +50,7 @@ Section BoundedField25p5.
| [ |- { f | forall a, ?phi (f a) = @?rhs a } ]
=> apply lift1_sig with (P:=fun a f => phi f = rhs a)
end.
- intros.
+ intros a.
eexists_sig_etransitivity. all:cbv [phi].
rewrite <- (proj2_sig square_sig).
symmetry; rewrite <- (proj2_sig carry_sig); symmetry.
diff --git a/src/Specific/IntegrationTestSub.v b/src/Specific/IntegrationTestSub.v
index 3eadc371d..7599c99e1 100644
--- a/src/Specific/IntegrationTestSub.v
+++ b/src/Specific/IntegrationTestSub.v
@@ -50,7 +50,7 @@ Section BoundedField25p5.
| [ |- { f | forall a b, ?phi (f a b) = @?rhs a b } ]
=> apply lift2_sig with (P:=fun a b f => phi f = rhs a b)
end.
- intros.
+ intros a b.
eexists_sig_etransitivity. all:cbv [phi].
rewrite <- (proj2_sig sub_sig).
symmetry; rewrite <- (proj2_sig carry_sig); symmetry.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 09:02:14 +0000