aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Algebra/Field.v2
-rw-r--r--src/Algebra/IntegralDomain.v11
-rw-r--r--src/Reflection/InlineCast.v2
-rw-r--r--src/Reflection/InlineWf.v1
-rw-r--r--src/Reflection/MultiSizeTest2.v2
-rw-r--r--src/Reflection/Named/Syntax.v2
-rw-r--r--src/Reflection/SmartMap.v2
-rw-r--r--src/Reflection/Syntax.v6
-rw-r--r--src/Reflection/Z/Interpretations128/RelationsCombinations.v4
-rw-r--r--src/Reflection/Z/Interpretations64/RelationsCombinations.v4
-rw-r--r--src/Reflection/Z/Syntax/Util.v2
-rw-r--r--src/Spec/WeierstrassCurve.v2
-rw-r--r--src/Specific/GF25519Bounded.v7
13 files changed, 26 insertions, 21 deletions
diff --git a/src/Algebra/Field.v b/src/Algebra/Field.v
index e901bde2f..76b2a9ed3 100644
--- a/src/Algebra/Field.v
+++ b/src/Algebra/Field.v
@@ -271,7 +271,7 @@ Ltac _inverse_to_equation_by fld d tac :=
lazymatch goal with
| H: eq (mul ?di d) one |- _ => rewrite <-!(left_inv_unique(H:=fld) _ _ H) in *
| H: eq (mul d ?di) one |- _ => rewrite <-!(right_inv_unique(H:=fld) _ _ H) in *
- | _ => _introduce_inverse constr:(fld) constr:(d) d_nz
+ | _ => _introduce_inverse fld d d_nz
end;
clear d_nz.
diff --git a/src/Algebra/IntegralDomain.v b/src/Algebra/IntegralDomain.v
index 72414b46e..f58874710 100644
--- a/src/Algebra/IntegralDomain.v
+++ b/src/Algebra/IntegralDomain.v
@@ -45,13 +45,12 @@ Module IntegralDomain.
| Coef_add c1 c2 => Z.add (CtoZ c1) (CtoZ c2)
| Coef_mul c1 c2 => Z.mul (CtoZ c1) (CtoZ c2)
end.
- Local Notation of_Z := (@Ring.of_Z R zero one opp add).
+ Let of_Z := (@Ring.of_Z R zero one opp add).
Lemma CtoZ_correct c : of_Z (CtoZ c) = denote c.
Proof.
- Set Printing All.
induction c; simpl CtoZ; simpl denote;
- repeat (rewrite_hyp ?* || Ring.push_homomorphism constr:(of_Z)); reflexivity.
+ repeat (rewrite_hyp ?* || Ring.push_homomorphism of_Z); reflexivity.
Qed.
(* TODO: move *)
@@ -77,7 +76,7 @@ Module IntegralDomain.
Proof.
rewrite <-List.Forall_forall in H; induction H; simpl List.fold_right.
{ eapply char_ge_C; assumption. }
- { rewrite Znat.N2Z.inj_mul; Ring.push_homomorphism constr:(of_Z).
+ { rewrite Znat.N2Z.inj_mul; Ring.push_homomorphism of_Z.
eapply Ring.nonzero_product_iff_nonzero_factor; eauto. }
Qed.
@@ -116,8 +115,8 @@ Module IntegralDomain.
| _ => progress (change (denote (Coef_one)) with (of_Z 1) in * )
| _ => progress (change (denote (Coef_opp c)) with (opp (denote c)) in * )
| _ => progress (change (denote (Coef_mul c1 c2)) with (denote c1 * denote c2) in * )
- | |- opp _ <> zero => setoid_rewrite Ring.opp_zero_iff
- | |- _ * _ <> zero => eapply Ring.nonzero_product_iff_nonzero_factor
+ | |- (opp _ <> zero)%type => setoid_rewrite Ring.opp_zero_iff
+ | |- (mul _ _ <> zero)%type => eapply Ring.nonzero_product_iff_nonzero_factor
| _ => solve [eauto using is_constant_nonzero_correct, Pos.le_1_l]
| _ => progress rewrite <-CtoZ_correct
end.
diff --git a/src/Reflection/InlineCast.v b/src/Reflection/InlineCast.v
index 554c42da7..d3e85d02d 100644
--- a/src/Reflection/InlineCast.v
+++ b/src/Reflection/InlineCast.v
@@ -76,7 +76,7 @@ Section language.
| TT
=> None
end.
- Definition push_cast {var t} : @exprf var t -> inline_directive (op:=op) (var:=var) t
+ Definition push_cast {var t} : @exprf var t -> @inline_directive _ op var t
:= match t with
| Tbase _ => fun v => match maybe_push_cast v with
| Some e => inline e
diff --git a/src/Reflection/InlineWf.v b/src/Reflection/InlineWf.v
index 64ecb9247..084f0d46b 100644
--- a/src/Reflection/InlineWf.v
+++ b/src/Reflection/InlineWf.v
@@ -170,6 +170,7 @@ Section language.
| progress invert_expr
| progress inversion_wf
| progress break_innermost_match_step
+ | discriminate
| congruence
| solve [ auto ] ].
Qed.
diff --git a/src/Reflection/MultiSizeTest2.v b/src/Reflection/MultiSizeTest2.v
index 575b8978a..4bac3d14c 100644
--- a/src/Reflection/MultiSizeTest2.v
+++ b/src/Reflection/MultiSizeTest2.v
@@ -158,6 +158,7 @@ Example ex1 : Expr base_type op (Arrow Unit TNat) := fun var =>
LetIn (Op (tR:=TNat) (Plus Nat) (Pair (Var a) (Var b))) (fun c : var Nat =>
Op (Plus Nat) (Pair (Var c) (Var c)))))).
+(*
Example ex1f : Expr base_type op (Arrow (TNat * TNat) TNat) := fun var =>
Abs (fun a0b0 : interp_flat_type _ (TNat * TNat) =>
let a0 := fst a0b0 in let b0 := snd a0b0 in
@@ -179,3 +180,4 @@ Eval compute in ex1fb.
Definition ex1fb' := Boundify ex1f (64, 64)%core.
Eval compute in ex1fb'.
+*) \ No newline at end of file
diff --git a/src/Reflection/Named/Syntax.v b/src/Reflection/Named/Syntax.v
index 996d707a3..1f171e9af 100644
--- a/src/Reflection/Named/Syntax.v
+++ b/src/Reflection/Named/Syntax.v
@@ -187,7 +187,7 @@ Global Arguments wff {_ _ _ _ _} ctx {t} _.
Global Arguments wf {_ _ _ _ _} ctx {t} _.
Global Arguments interp_genf {_ _ _ var _} _ _ _ _ _ _ {ctx t} _ _.
Global Arguments interpf {_ _ _ _ _ interp_op ctx t} _ _.
-Global Arguments interp {_ _ _ _ _ interp_op ctx t} _ _.
+Global Arguments interp {_ _ _ _ _ interp_op ctx t} _ _ _.
Notation "'slet' x := A 'in' b" := (LetIn _ x A%nexpr b%nexpr) : nexpr_scope.
Notation "'λn' x .. y , t" := (Abs x .. (Abs y t%nexpr) .. ) : nexpr_scope.
diff --git a/src/Reflection/SmartMap.v b/src/Reflection/SmartMap.v
index 5cddc0418..2a49196bb 100644
--- a/src/Reflection/SmartMap.v
+++ b/src/Reflection/SmartMap.v
@@ -198,7 +198,7 @@ Global Arguments SmartFlatTypeMap {_ _} _ {_} _.
Global Arguments SmartFlatTypeUnMap {_} _.
Global Arguments SmartFlatTypeMapInterp {_ _ _ _} _ {_} _.
Global Arguments SmartFlatTypeMapUnInterp {_ _ _ _ _} fv {_ _} _.
-Global Arguments SmartVarMap {_ _ _} _ _ {!_} _ / .
+Global Arguments SmartVarMap {_ _ _} _ _ {!_} _ / _.
Section hetero_type.
Fixpoint flatten_flat_type {base_type_code} (t : flat_type (flat_type base_type_code)) : flat_type base_type_code
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v
index d77731633..d8b88e560 100644
--- a/src/Reflection/Syntax.v
+++ b/src/Reflection/Syntax.v
@@ -134,10 +134,10 @@ Global Arguments interp_type_gen_hetero {_} _ _ _.
Global Arguments interp_type_gen {_} _ _.
Global Arguments interp_flat_type {_} _ _.
Global Arguments interp_type {_} _ _.
-Global Arguments Interp {_ _ _} interp_op {t} _.
-Global Arguments interp {_ _ _} interp_op {t} _.
+Global Arguments Interp {_ _ _} interp_op {t} _ _.
+Global Arguments interp {_ _ _} interp_op {t} _ _.
Global Arguments interpf {_ _ _} interp_op {t} _.
-Global Arguments interp _ _ _ _ _ !_ / .
+Global Arguments interp _ _ _ _ _ !_ / _.
Module Export Notations.
Notation "()" := (@Unit _) : ctype_scope.
diff --git a/src/Reflection/Z/Interpretations128/RelationsCombinations.v b/src/Reflection/Z/Interpretations128/RelationsCombinations.v
index 6e7eb2865..b2f7ce4a5 100644
--- a/src/Reflection/Z/Interpretations128/RelationsCombinations.v
+++ b/src/Reflection/Z/Interpretations128/RelationsCombinations.v
@@ -190,7 +190,7 @@ Module Relations.
t proj012.
Qed.
End proj_from_option2.
- Global Arguments uncurry_interp_type_rel_pointwise_proj_from_option2 {_ _ _ _ _} proj {t f0 f g} _ _ _.
+ Global Arguments uncurry_interp_type_rel_pointwise_proj_from_option2 {_ _ _ _ _} proj {t f0 f g} _ _ _ _ _.
Section proj1_from_option2.
Context {interp_base_type0 interp_base_type1 : Type} {interp_base_type2 : base_type -> Type}
@@ -234,7 +234,7 @@ Module Relations.
t proj012.
Qed.
End proj1_from_option2.
- Global Arguments uncurry_interp_type_rel_pointwise_proj1_from_option2 {_ _ _ _ _} R {t f0 f g} _ _ _.
+ Global Arguments uncurry_interp_type_rel_pointwise_proj1_from_option2 {_ _ _ _ _} R {t f0 f g} _ _ _ _ _.
Section combine_related.
Lemma related_flat_transitivity {interp_base_type1 interp_base_type2 interp_base_type3}
diff --git a/src/Reflection/Z/Interpretations64/RelationsCombinations.v b/src/Reflection/Z/Interpretations64/RelationsCombinations.v
index 2e05b18de..adfceb899 100644
--- a/src/Reflection/Z/Interpretations64/RelationsCombinations.v
+++ b/src/Reflection/Z/Interpretations64/RelationsCombinations.v
@@ -190,7 +190,7 @@ Module Relations.
t proj012.
Qed.
End proj_from_option2.
- Global Arguments uncurry_interp_type_rel_pointwise_proj_from_option2 {_ _ _ _ _} proj {t f0 f g} _ _ _.
+ Global Arguments uncurry_interp_type_rel_pointwise_proj_from_option2 {_ _ _ _ _} proj {t f0 f g} _ _ _ _ _.
Section proj1_from_option2.
Context {interp_base_type0 interp_base_type1 : Type} {interp_base_type2 : base_type -> Type}
@@ -234,7 +234,7 @@ Module Relations.
t proj012.
Qed.
End proj1_from_option2.
- Global Arguments uncurry_interp_type_rel_pointwise_proj1_from_option2 {_ _ _ _ _} R {t f0 f g} _ _ _.
+ Global Arguments uncurry_interp_type_rel_pointwise_proj1_from_option2 {_ _ _ _ _} R {t f0 f g} _ _ _ _ _.
Section combine_related.
Lemma related_flat_transitivity {interp_base_type1 interp_base_type2 interp_base_type3}
diff --git a/src/Reflection/Z/Syntax/Util.v b/src/Reflection/Z/Syntax/Util.v
index 1d591658f..92e5b2728 100644
--- a/src/Reflection/Z/Syntax/Util.v
+++ b/src/Reflection/Z/Syntax/Util.v
@@ -25,7 +25,7 @@ Definition base_type_leb (v1 v2 : base_type) : bool
Definition base_type_min := base_type_min base_type_leb.
Global Arguments base_type_min !_ !_ / .
-Global Arguments TypeUtil.base_type_min _ _ _ / .
+Global Arguments TypeUtil.base_type_min _ _ _ / _.
Definition Castb {var} A A' (v : exprf base_type op (var:=var) (Tbase A))
: exprf base_type op (var:=var) (Tbase A')
diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v
index 87b5bcffd..eebc79df4 100644
--- a/src/Spec/WeierstrassCurve.v
+++ b/src/Spec/WeierstrassCurve.v
@@ -62,7 +62,7 @@ Module W.
| ∞, _ => coordinates P2
| _, ∞ => coordinates P1
end) _.
- Next Obligation. exact (Pre.add_onCurve _ _ (proj2_sig _) (proj2_sig _)). Qed.
+ Next Obligation. apply (Pre.add_onCurve _ _ (proj2_sig _) (proj2_sig _)). Qed.
Fixpoint mul (n:nat) (P : point) : point :=
match n with
diff --git a/src/Specific/GF25519Bounded.v b/src/Specific/GF25519Bounded.v
index fafdc412b..81de77008 100644
--- a/src/Specific/GF25519Bounded.v
+++ b/src/Specific/GF25519Bounded.v
@@ -282,9 +282,12 @@ Proof.
eexists.
unfold GF25519.eqb.
simpl @fe25519WToZ in *; cbv beta iota.
- intros.
+ intros A B; specialize_by assumption; clear A B.
cbv [Tuple.map Tuple.on_tuple Tuple.to_list Tuple.to_list' List.map Tuple.from_list Tuple.from_list' fe25519WToZ] in *.
- rewrite <- frf, <- frg by assumption.
+ etransitivity. Focus 2. {
+ apply f_equal2.
+ apply frf.
+ apply frg. } Unfocus.
etransitivity; [ eapply fieldwisebW_correct | ].
cbv [fe25519WToZ].
reflexivity.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 09:32:26 +0000