aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers')
-rw-r--r--theories/Numbers/Cyclic/Int31/Ring31.v20
-rw-r--r--theories/Numbers/Cyclic/ZModulo/ZModulo.v6
-rw-r--r--theories/Numbers/Integer/Abstract/ZDivEucl.v14
-rw-r--r--theories/Numbers/Integer/BigZ/BigZ.v24
-rw-r--r--theories/Numbers/Integer/BigZ/ZMake.v12
-rw-r--r--theories/Numbers/NatInt/NZGcd.v2
-rw-r--r--theories/Numbers/Natural/BigN/BigN.v26
-rw-r--r--theories/Numbers/Natural/BigN/NMake.v2
-rw-r--r--theories/Numbers/Natural/BigN/NMake_gen.ml2
-rw-r--r--theories/Numbers/Rational/BigQ/BigQ.v14
-rw-r--r--theories/Numbers/Rational/BigQ/QMake.v37
-rw-r--r--theories/Numbers/Rational/SpecViaQ/QSig.v10
12 files changed, 88 insertions, 81 deletions
diff --git a/theories/Numbers/Cyclic/Int31/Ring31.v b/theories/Numbers/Cyclic/Int31/Ring31.v
index 215b8bd581..d160f5f1de 100644
--- a/theories/Numbers/Cyclic/Int31/Ring31.v
+++ b/theories/Numbers/Cyclic/Int31/Ring31.v
@@ -19,13 +19,13 @@ Local Open Scope list_scope.
Ltac isInt31cst_lst l :=
match l with
- | nil => constr:true
+ | nil => constr:(true)
| ?t::?l => match t with
| D1 => isInt31cst_lst l
| D0 => isInt31cst_lst l
- | _ => constr:false
+ | _ => constr:(false)
end
- | _ => constr:false
+ | _ => constr:(false)
end.
Ltac isInt31cst t :=
@@ -38,17 +38,17 @@ Ltac isInt31cst t :=
::i11::i12::i13::i14::i15::i16::i17::i18::i19::i20
::i21::i22::i23::i24::i25::i26::i27::i28::i29::i30::nil)
in isInt31cst_lst l
- | Int31.On => constr:true
- | Int31.In => constr:true
- | Int31.Tn => constr:true
- | Int31.Twon => constr:true
- | _ => constr:false
+ | Int31.On => constr:(true)
+ | Int31.In => constr:(true)
+ | Int31.Tn => constr:(true)
+ | Int31.Twon => constr:(true)
+ | _ => constr:(false)
end.
Ltac Int31cst t :=
match isInt31cst t with
- | true => constr:t
- | false => constr:NotConstant
+ | true => constr:(t)
+ | false => constr:(NotConstant)
end.
(** The generic ring structure inferred from the Cyclic structure *)
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index c115a831d9..04fc5a8dfa 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -369,7 +369,7 @@ Section ZModulo.
assert (Z.div_eucl ([|x|]*[|y|]) wB = (([|x|]*[|y|])/wB,([|x|]*[|y|]) mod wB)).
unfold Z.modulo, Z.div; destruct Z.div_eucl; auto.
generalize (Z_div_mod ([|x|]*[|y|]) wB wB_pos); destruct Z.div_eucl as (h,l).
- destruct 1; injection H; clear H; intros.
+ destruct 1; injection H as ? ?.
rewrite H0.
assert ([|l|] = l).
apply Zmod_small; auto.
@@ -411,7 +411,7 @@ Section ZModulo.
unfold Z.modulo, Z.div; destruct Z.div_eucl; auto.
generalize (Z_div_mod [|a|] [|b|] H0).
destruct Z.div_eucl as (q,r); destruct 1; intros.
- injection H1; clear H1; intros.
+ injection H1 as ? ?.
assert ([|r|]=r).
apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|];
auto with zarith.
@@ -522,7 +522,7 @@ Section ZModulo.
unfold Z.modulo, Z.div; destruct Z.div_eucl; auto.
generalize (Z_div_mod a [|b|] H3).
destruct Z.div_eucl as (q,r); destruct 1; intros.
- injection H4; clear H4; intros.
+ injection H4 as ? ?.
assert ([|r|]=r).
apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|];
auto with zarith.
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index 278e1bcffa..c2fa69e535 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -30,18 +30,23 @@ Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv.
We just ignore them here.
*)
-Module Type EuclidSpec (Import A : ZAxiomsSig')(Import B : DivMod' A).
- Axiom mod_always_pos : forall a b, b ~= 0 -> 0 <= a mod b < abs b.
+Module Type EuclidSpec (Import A : ZAxiomsSig')(Import B : DivMod A).
+ Axiom mod_always_pos : forall a b, b ~= 0 -> 0 <= B.modulo a b < abs b.
End EuclidSpec.
Module Type ZEuclid (Z:ZAxiomsSig) := NZDiv.NZDiv Z <+ EuclidSpec Z.
-Module Type ZEuclid' (Z:ZAxiomsSig) := NZDiv.NZDiv' Z <+ EuclidSpec Z.
Module ZEuclidProp
(Import A : ZAxiomsSig')
(Import B : ZMulOrderProp A)
(Import C : ZSgnAbsProp A B)
- (Import D : ZEuclid' A).
+ (Import D : ZEuclid A).
+
+ (** We put notations in a scope, to avoid warnings about
+ redefinitions of notations *)
+ Infix "/" := D.div : euclid.
+ Infix "mod" := D.modulo : euclid.
+ Local Open Scope euclid.
Module Import Private_NZDiv := Nop <+ NZDivProp A D B.
@@ -615,4 +620,3 @@ intros (c,Hc). rewrite Hc. now apply mod_mul.
Qed.
End ZEuclidProp.
-
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index ec495d0947..7c76011f21 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -138,7 +138,7 @@ intros NEQ.
generalize (BigZ.spec_div_eucl a b).
generalize (Z_div_mod_full [a] [b] NEQ).
destruct BigZ.div_eucl as (q,r), Z.div_eucl as (q',r').
-intros (EQ,_). injection 1. intros EQr EQq.
+intros (EQ,_). injection 1 as EQr EQq.
BigZ.zify. rewrite EQr, EQq; auto.
Qed.
@@ -148,26 +148,26 @@ Ltac isBigZcst t :=
match t with
| BigZ.Pos ?t => isBigNcst t
| BigZ.Neg ?t => isBigNcst t
- | BigZ.zero => constr:true
- | BigZ.one => constr:true
- | BigZ.two => constr:true
- | BigZ.minus_one => constr:true
- | _ => constr:false
+ | BigZ.zero => constr:(true)
+ | BigZ.one => constr:(true)
+ | BigZ.two => constr:(true)
+ | BigZ.minus_one => constr:(true)
+ | _ => constr:(false)
end.
Ltac BigZcst t :=
match isBigZcst t with
- | true => constr:t
- | false => constr:NotConstant
+ | true => constr:(t)
+ | false => constr:(NotConstant)
end.
Ltac BigZ_to_N t :=
match t with
| BigZ.Pos ?t => BigN_to_N t
- | BigZ.zero => constr:0%N
- | BigZ.one => constr:1%N
- | BigZ.two => constr:2%N
- | _ => constr:NotConstant
+ | BigZ.zero => constr:(0%N)
+ | BigZ.one => constr:(1%N)
+ | BigZ.two => constr:(2%N)
+ | _ => constr:(NotConstant)
end.
(** Registration for the "ring" tactic *)
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 8673b8a58f..fec6e06837 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -147,7 +147,7 @@ Module Make (NN:NType) <: ZType.
Proof.
apply Bool.eq_iff_eq_true.
rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare.
- destruct Z.compare; split; try easy. now destruct 1.
+ now destruct Z.compare; split.
Qed.
Definition min n m := match compare n m with Gt => m | _ => n end.
@@ -427,13 +427,13 @@ Module Make (NN:NType) <: ZType.
(* Pos Neg *)
generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r).
break_nonneg x px EQx; break_nonneg y py EQy;
- try (injection 1; intros Hr Hq; rewrite NN.spec_eqb, NN.spec_0, Hr;
+ try (injection 1 as Hq Hr; rewrite NN.spec_eqb, NN.spec_0, Hr;
simpl; rewrite Hq, NN.spec_0; auto).
change (- Zpos py) with (Zneg py).
assert (GT : Zpos py > 0) by (compute; auto).
generalize (Z_div_mod (Zpos px) (Zpos py) GT).
unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r').
- intros (EQ,MOD). injection 1. intros Hr' Hq'.
+ intros (EQ,MOD). injection 1 as Hq' Hr'.
rewrite NN.spec_eqb, NN.spec_0, Hr'.
break_nonneg r pr EQr.
subst; simpl. rewrite NN.spec_0; auto.
@@ -442,13 +442,13 @@ Module Make (NN:NType) <: ZType.
(* Neg Pos *)
generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r).
break_nonneg x px EQx; break_nonneg y py EQy;
- try (injection 1; intros Hr Hq; rewrite NN.spec_eqb, NN.spec_0, Hr;
+ try (injection 1 as Hq Hr; rewrite NN.spec_eqb, NN.spec_0, Hr;
simpl; rewrite Hq, NN.spec_0; auto).
change (- Zpos px) with (Zneg px).
assert (GT : Zpos py > 0) by (compute; auto).
generalize (Z_div_mod (Zpos px) (Zpos py) GT).
unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r').
- intros (EQ,MOD). injection 1. intros Hr' Hq'.
+ intros (EQ,MOD). injection 1 as Hq' Hr'.
rewrite NN.spec_eqb, NN.spec_0, Hr'.
break_nonneg r pr EQr.
subst; simpl. rewrite NN.spec_0; auto.
@@ -457,7 +457,7 @@ Module Make (NN:NType) <: ZType.
(* Neg Neg *)
generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r).
break_nonneg x px EQx; break_nonneg y py EQy;
- try (injection 1; intros Hr Hq; rewrite Hr, Hq; auto).
+ try (injection 1 as -> ->; auto).
simpl. intros <-; auto.
Qed.
diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v
index 1d36729435..44088f8c4a 100644
--- a/theories/Numbers/NatInt/NZGcd.v
+++ b/theories/Numbers/NatInt/NZGcd.v
@@ -60,8 +60,6 @@ Proof.
intros n. exists 0. now nzsimpl.
Qed.
-Hint Rewrite divide_1_l divide_0_r : nz.
-
Lemma divide_0_l : forall n, (0 | n) -> n==0.
Proof.
intros n (m,Hm). revert Hm. now nzsimpl.
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 29a1145e0c..e8ff516f35 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -110,7 +110,7 @@ intros NEQ.
generalize (BigN.spec_div_eucl a b).
generalize (Z_div_mod_full [a] [b] NEQ).
destruct BigN.div_eucl as (q,r), Z.div_eucl as (q',r').
-intros (EQ,_). injection 1. intros EQr EQq.
+intros (EQ,_). injection 1 as EQr EQq.
BigN.zify. rewrite EQr, EQq; auto.
Qed.
@@ -119,10 +119,10 @@ Qed.
Ltac isStaticWordCst t :=
match t with
- | W0 => constr:true
+ | W0 => constr:(true)
| WW ?t1 ?t2 =>
match isStaticWordCst t1 with
- | false => constr:false
+ | false => constr:(false)
| true => isStaticWordCst t2
end
| _ => isInt31cst t
@@ -139,30 +139,30 @@ Ltac isBigNcst t :=
| BigN.N6 ?t => isStaticWordCst t
| BigN.Nn ?n ?t => match isnatcst n with
| true => isStaticWordCst t
- | false => constr:false
+ | false => constr:(false)
end
- | BigN.zero => constr:true
- | BigN.one => constr:true
- | BigN.two => constr:true
- | _ => constr:false
+ | BigN.zero => constr:(true)
+ | BigN.one => constr:(true)
+ | BigN.two => constr:(true)
+ | _ => constr:(false)
end.
Ltac BigNcst t :=
match isBigNcst t with
- | true => constr:t
- | false => constr:NotConstant
+ | true => constr:(t)
+ | false => constr:(NotConstant)
end.
Ltac BigN_to_N t :=
match isBigNcst t with
| true => eval vm_compute in (BigN.to_N t)
- | false => constr:NotConstant
+ | false => constr:(NotConstant)
end.
Ltac Ncst t :=
match isNcst t with
- | true => constr:t
- | false => constr:NotConstant
+ | true => constr:(t)
+ | false => constr:(NotConstant)
end.
(** Registration for the "ring" tactic *)
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index 98949736cb..1425041a10 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -338,7 +338,7 @@ Module Make (W0:CyclicType) <: NType.
Proof.
apply eq_iff_eq_true.
rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare.
- destruct Z.compare; split; try easy. now destruct 1.
+ now destruct Z.compare; split.
Qed.
Definition min (n m : t) : t := match compare n m with Gt => m | _ => n end.
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 601fa108f9..5177fae65f 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -147,7 +147,7 @@ pr
pr " Local Notation Size := (SizePlus O).";
pr "";
- pr " Tactic Notation \"do_size\" tactic(t) := do %i t." (size+1);
+ pr " Tactic Notation (at level 3) \"do_size\" tactic3(t) := do %i t." (size+1);
pr "";
pr " Definition dom_t n := match n with";
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index fe38ea4f2d..850afe5345 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -104,18 +104,18 @@ Ltac isBigQcst t :=
| BigQ.Qz ?t => isBigZcst t
| BigQ.Qq ?n ?d => match isBigZcst n with
| true => isBigNcst d
- | false => constr:false
+ | false => constr:(false)
end
- | BigQ.zero => constr:true
- | BigQ.one => constr:true
- | BigQ.minus_one => constr:true
- | _ => constr:false
+ | BigQ.zero => constr:(true)
+ | BigQ.one => constr:(true)
+ | BigQ.minus_one => constr:(true)
+ | _ => constr:(false)
end.
Ltac BigQcst t :=
match isBigQcst t with
- | true => constr:t
- | false => constr:NotConstant
+ | true => constr:(t)
+ | false => constr:(NotConstant)
end.
Add Field BigQfield : BigQfieldth
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index 4ac36425b4..b9fed9d566 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -1050,13 +1050,13 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
Theorem spec_of_Qc: forall q, [[of_Qc q]] = q.
Proof.
intros; apply Qc_decomp; simpl; intros.
- rewrite strong_spec_of_Qc; auto.
+ rewrite strong_spec_of_Qc. apply canon.
Qed.
Theorem spec_oppc: forall q, [[opp q]] = -[[q]].
Proof.
intros q; unfold Qcopp, to_Qc, Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
apply Qred_complete.
rewrite spec_opp, <- Qred_opp, Qred_correct.
apply Qeq_refl.
@@ -1085,10 +1085,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
unfold to_Qc.
transitivity (Q2Qc ([x] + [y])).
unfold Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
apply Qred_complete; apply spec_add; auto.
unfold Qcplus, Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
apply Qred_complete.
apply Qplus_comp; apply Qeq_sym; apply Qred_correct.
Qed.
@@ -1099,10 +1099,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
unfold to_Qc.
transitivity (Q2Qc ([x] + [y])).
unfold Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
apply Qred_complete; apply spec_add_norm; auto.
unfold Qcplus, Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
apply Qred_complete.
apply Qplus_comp; apply Qeq_sym; apply Qred_correct.
Qed.
@@ -1147,10 +1147,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
unfold to_Qc.
transitivity (Q2Qc ([x] * [y])).
unfold Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
apply Qred_complete; apply spec_mul; auto.
unfold Qcmult, Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
apply Qred_complete.
apply Qmult_comp; apply Qeq_sym; apply Qred_correct.
Qed.
@@ -1161,10 +1161,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
unfold to_Qc.
transitivity (Q2Qc ([x] * [y])).
unfold Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
apply Qred_complete; apply spec_mul_norm; auto.
unfold Qcmult, Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
apply Qred_complete.
apply Qmult_comp; apply Qeq_sym; apply Qred_correct.
Qed.
@@ -1185,10 +1185,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
unfold to_Qc.
transitivity (Q2Qc (/[x])).
unfold Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
apply Qred_complete; apply spec_inv; auto.
unfold Qcinv, Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
apply Qred_complete.
apply Qinv_comp; apply Qeq_sym; apply Qred_correct.
Qed.
@@ -1199,10 +1199,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
unfold to_Qc.
transitivity (Q2Qc (/[x])).
unfold Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
apply Qred_complete; apply spec_inv_norm; auto.
unfold Qcinv, Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
apply Qred_complete.
apply Qinv_comp; apply Qeq_sym; apply Qred_correct.
Qed.
@@ -1247,13 +1247,13 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
unfold to_Qc.
transitivity (Q2Qc ([x]^2)).
unfold Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
apply Qred_complete; apply spec_square; auto.
simpl Qcpower.
replace (Q2Qc [x] * 1) with (Q2Qc [x]); try ring.
simpl.
unfold Qcmult, Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
apply Qred_complete.
apply Qmult_comp; apply Qeq_sym; apply Qred_correct.
Qed.
@@ -1264,14 +1264,14 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
unfold to_Qc.
transitivity (Q2Qc ([x]^Zpos p)).
unfold Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
apply Qred_complete; apply spec_power_pos; auto.
induction p using Pos.peano_ind.
simpl; ring.
rewrite Pos2Nat.inj_succ; simpl Qcpower.
rewrite <- IHp; clear IHp.
unfold Qcmult, Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
apply Qred_complete.
setoid_replace ([x] ^ ' Pos.succ p)%Q with ([x] * [x] ^ ' p)%Q.
apply Qmult_comp; apply Qeq_sym; apply Qred_correct.
@@ -1281,4 +1281,3 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
Qed.
End Make.
-
diff --git a/theories/Numbers/Rational/SpecViaQ/QSig.v b/theories/Numbers/Rational/SpecViaQ/QSig.v
index a40d940598..8e20fd0608 100644
--- a/theories/Numbers/Rational/SpecViaQ/QSig.v
+++ b/theories/Numbers/Rational/SpecViaQ/QSig.v
@@ -115,7 +115,10 @@ Ltac solve_wd2 := intros x x' Hx y y' Hy; qify; now rewrite Hx, Hy.
Local Obligation Tactic := solve_wd2 || solve_wd1.
Instance : Measure to_Q.
-Instance eq_equiv : Equivalence eq := {}.
+Instance eq_equiv : Equivalence eq.
+Proof.
+ change eq with (RelCompFun Qeq to_Q); apply _.
+Defined.
Program Instance lt_wd : Proper (eq==>eq==>iff) lt.
Program Instance le_wd : Proper (eq==>eq==>iff) le.
@@ -141,7 +144,10 @@ Proof. intros. qify. destruct (Qcompare_spec [x] [y]); auto. Qed.
(** Let's implement [TotalOrder] *)
Definition lt_compat := lt_wd.
-Instance lt_strorder : StrictOrder lt := {}.
+Instance lt_strorder : StrictOrder lt.
+Proof.
+ change lt with (RelCompFun Qlt to_Q); apply _.
+Qed.
Lemma le_lteq : forall x y, x<=y <-> x<y \/ x==y.
Proof. intros. qify. apply Qle_lteq. Qed.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 19:25:28 +0000