Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adapt w.r.t. coq/coq#16904. #175

Merged
merged 1 commit into from
Nov 25, 2022
Merged

Adapt w.r.t. coq/coq#16904. #175

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 12 additions & 12 deletions algebra/Bernstein.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ Proof.
destruct (le_lt_eq_dec _ _ H0).
replace (lt_n_Sm_le (S i) n l) with (lt_n_Sm_le _ _ (lt_n_S _ _ H)) by apply le_irrelevent.
reflexivity.
elimtype False; lia.
exfalso; lia.
Qed.

Lemma Bernstein_inv2 : forall n (H:S n <= S n),
Expand All @@ -75,7 +75,7 @@ Proof.
intros n H.
simpl (Bernstein H).
destruct (le_lt_eq_dec _ _ H).
elimtype False; lia.
exfalso; lia.
replace (lt_n_Sm_le n n H) with (le_S_n n n H) by apply le_irrelevent.
reflexivity.
Qed.
Expand All @@ -91,7 +91,7 @@ Proof.
revert n i H.
induction n; intros [|i] H.
apply H0.
elimtype False; auto with *.
exfalso; auto with *.
apply H1.
apply IHn.
simpl.
Expand Down Expand Up @@ -137,7 +137,7 @@ Proof.
unfold part_tot_nat_fun.
destruct (le_lt_dec (S n) (S n)).
reflexivity.
elimtype False; lia.
exfalso; lia.
intros i j Hij. subst.
intros Hi Hj.
unfold A.
Expand All @@ -148,22 +148,22 @@ Proof.
rewrite <- (le_irrelevent _ _ (le_0_n _) _).
ring.
destruct (le_lt_dec (S n) i).
elimtype False; lia.
exfalso; lia.
destruct (le_lt_dec (S n) (S i)); simpl (Bernstein (lt_n_Sm_le (S i) (S n) Hi));
destruct (le_lt_eq_dec (S i) (S n) (lt_n_Sm_le (S i) (S n) Hi)).
elimtype False; lia.
exfalso; lia.
replace (lt_n_Sm_le i n (lt_n_Sm_le (S i) (S n) Hi)) with (lt_n_Sm_le i n l) by apply le_irrelevent.
ring.
replace (le_S_n i n (lt_n_Sm_le (S i) (S n) Hi)) with (lt_n_Sm_le i n l) by apply le_irrelevent.
replace l1 with l0 by apply le_irrelevent.
reflexivity.
elimtype False; lia.
exfalso; lia.
Qed.

Lemma RaiseDegreeA : forall n i (H:i<=n), (nring (S n))[*]_X_[*]Bernstein H[=](nring (S i))[*]Bernstein (le_n_S _ _ H).
Proof.
induction n.
intros [|i] H; [|elimtype False; lia].
intros [|i] H; [|exfalso; lia].
repeat split; ring.
intros i H.
change (nring (S (S n)):cpoly_cring R) with (nring (S n)[+][1]:cpoly_cring R).
Expand Down Expand Up @@ -207,7 +207,7 @@ Qed.
Lemma RaiseDegreeB : forall n i (H:i<=n), (nring (S n))[*]([1][-]_X_)[*]Bernstein H[=](nring (S n - i))[*]Bernstein (le_S _ _ H).
Proof.
induction n.
intros [|i] H; [|elimtype False; lia].
intros [|i] H; [|exfalso; lia].
repeat split; ring.
intros i H.
change (nring (S (S n)):cpoly_cring R) with (nring (S n)[+][1]:cpoly_cring R).
Expand Down Expand Up @@ -340,7 +340,7 @@ Proof.
rewrite (V0_eq v1), (V0_eq v2). ring.
intros l v1 v2.
destruct n as [|n].
elimtype False; auto with *.
exfalso; auto with *.
rewrite (VSn_eq v1), (VSn_eq v2).
simpl.
rewrite IHi.
Expand Down Expand Up @@ -377,7 +377,7 @@ Proof.
clear - i.
unfold part_tot_nat_fun.
destruct (le_lt_dec (S n) i).
elimtype False; auto with *.
exfalso; auto with *.
simpl.
replace (lt_n_Sm_le _ _ l0) with (le_S_n _ _ l) by apply le_irrelevent.
reflexivity.
Expand Down Expand Up @@ -422,7 +422,7 @@ Proof.
rewrite <- c_zero. ring.
intros l l0 v.
destruct n as [|n].
elimtype False; auto with *.
exfalso; auto with *.
rewrite (VSn_eq v).
simpl.
rewrite -> IHi.
Expand Down
2 changes: 1 addition & 1 deletion algebra/CFields.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -809,7 +809,7 @@ Lemma part_function_recip_strext : forall x y Hx Hy,
Proof.
intros x y Hx Hy H.
elim (div_strext _ _ _ _ _ _ _ H); intro H1.
elimtype False; apply ap_irreflexive_unfolded with (x := [1]:X); auto.
exfalso; apply ap_irreflexive_unfolded with (x := [1]:X); auto.
exact (pfstrx _ _ _ _ _ _ H1).
Qed.

Expand Down
22 changes: 11 additions & 11 deletions algebra/COrdCauchy.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -266,9 +266,9 @@ Proof.
apply less_leEq_trans with e; eauto with arith.
unfold CS_seq_recip_seq in |- *.
elim lt_le_dec; intro; simpl in |- *.
elimtype False; apply le_not_lt with N n; eauto with arith.
exfalso; apply le_not_lt with N n; eauto with arith.
elim lt_le_dec; intro; simpl in |- *.
elimtype False; apply le_not_lt with N (max K N); eauto with arith.
exfalso; apply le_not_lt with N (max K N); eauto with arith.
rstepr (f (max K N)[-]f n).
apply AbsSmall_leEq_trans with (d[*]e[*]e).
apply mult_resp_leEq_both.
Expand Down Expand Up @@ -477,7 +477,7 @@ Proof.
intros.
elim (ap_imp_less _ _ _ (X (less_imp_ap _ _ _ X0))); intros.
auto.
elimtype False.
exfalso.
apply less_irreflexive_unfolded with (x := f x Hx).
apply leEq_less_trans with (f y Hy); auto.
apply H; apply less_leEq; auto.
Expand Down Expand Up @@ -533,7 +533,7 @@ Lemma local_mon_imp_mon : forall f : nat -> R,
(forall i, f i [<] f (S i)) -> forall i j, i < j -> f i [<] f j.
Proof.
simple induction j.
intros H0; elimtype False; inversion H0.
intros H0; exfalso; inversion H0.
clear j; intro j; intros H0 H1.
elim (le_lt_eq_dec _ _ H1); intro.
apply leEq_less_trans with (f j).
Expand Down Expand Up @@ -579,7 +579,7 @@ Proof.
intros.
cut (~ i <> j); [ lia | intro ].
cut (i < j \/ j < i); [ intro | apply not_eq; auto ].
inversion_clear H1; (elimtype False; cut (f i [#] f j); [ apply eq_imp_not_ap; assumption | idtac ]).
inversion_clear H1; (exfalso; cut (f i [#] f j); [ apply eq_imp_not_ap; assumption | idtac ]).
apply less_imp_ap; apply X; assumption.
apply Greater_imp_ap; apply X; assumption.
Qed.
Expand All @@ -588,7 +588,7 @@ Lemma local_mon_imp_mon_lt : forall n (f : forall i, i < n -> R),
(forall i H H', f i H [<] f (S i) H') -> forall i j Hi Hj, i < j -> f i Hi [<] f j Hj.
Proof.
simple induction j.
intros Hi Hj H0; elimtype False; inversion H0.
intros Hi Hj H0; exfalso; inversion H0.
clear j; intro j; intros.
elim (le_lt_eq_dec _ _ H); intro.
cut (j < n); [ intro | auto with arith ].
Expand Down Expand Up @@ -629,7 +629,7 @@ Lemma local_mon'_imp_mon'2_lt : forall n (f : forall i, i < n -> R),
(forall i H H', f i H [<=] f (S i) H') -> forall i j Hi Hj, i < j -> f i Hi [<=] f j Hj.
Proof.
intros; induction j as [| j Hrecj].
elimtype False; inversion H0.
exfalso; inversion H0.
elim (le_lt_eq_dec _ _ H0); intro.
cut (j < n); [ intro | auto with arith ].
apply leEq_transitive with (f j H1).
Expand All @@ -656,7 +656,7 @@ Proof.
cut (~ i <> j); intro.
clear X H Hj Hi; lia.
cut (i < j \/ j < i); [ intro | apply not_eq; auto ].
inversion_clear H1; (elimtype False; cut (f i Hi [#] f j Hj);
inversion_clear H1; (exfalso; cut (f i Hi [#] f j Hj);
[ apply eq_imp_not_ap; assumption | idtac ]).
apply less_imp_ap; auto.
apply Greater_imp_ap; auto.
Expand All @@ -666,7 +666,7 @@ Lemma local_mon_imp_mon_le : forall n (f : forall i, i <= n -> R),
(forall i H H', f i H [<] f (S i) H') -> forall i j Hi Hj, i < j -> f i Hi [<] f j Hj.
Proof.
simple induction j.
intros Hi Hj H0; elimtype False; inversion H0.
intros Hi Hj H0; exfalso; inversion H0.
clear j; intro j; intros.
elim (le_lt_eq_dec _ _ H); intro.
cut (j <= n); [ intro | auto with arith ].
Expand Down Expand Up @@ -707,7 +707,7 @@ Lemma local_mon'_imp_mon'2_le : forall n (f : forall i, i <= n -> R),
(forall i H H', f i H [<=] f (S i) H') -> forall i j Hi Hj, i < j -> f i Hi [<=] f j Hj.
Proof.
intros; induction j as [| j Hrecj].
elimtype False; inversion H0.
exfalso; inversion H0.
elim (le_lt_eq_dec _ _ H0); intro.
cut (j <= n); [ intro | auto with arith ].
apply leEq_transitive with (f j H1).
Expand All @@ -733,7 +733,7 @@ Proof.
cut (~ i <> j); intro.
clear H X Hj Hi; lia.
cut (i < j \/ j < i); [ intro | apply not_eq; auto ].
inversion_clear H1; (elimtype False; cut (f i Hi [#] f j Hj);
inversion_clear H1; (exfalso; cut (f i Hi [#] f j Hj);
[ apply eq_imp_not_ap; assumption | idtac ]).
apply less_imp_ap; auto.
apply Greater_imp_ap; auto.
Expand Down
16 changes: 8 additions & 8 deletions algebra/COrdFields.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -455,7 +455,7 @@ Proof.
elim (ap_imp_less _ _ _ (ring_non_triv R)).
2: auto.
intro H.
elimtype False.
exfalso.
apply (less_irreflexive_unfolded R [1]).
apply less_transitive_unfolded with ([0]:R).
auto.
Expand Down Expand Up @@ -1074,7 +1074,7 @@ Proof.
cut ([0] [<] ([1][/] y[//]y_) or ([1][/] y[//]y_) [<] [0]).
intros H0. elim H0; clear H0; intros H0.
auto.
elimtype False.
exfalso.
apply (less_irreflexive_unfolded R [0]).
eapply less_transitive_unfolded.
2: apply H0.
Expand Down Expand Up @@ -1159,7 +1159,7 @@ Proof.
split; auto.
elim (ap_imp_less _ _ _ H7); auto.
intro H9.
elimtype False.
exfalso.
apply (less_irreflexive_unfolded R [0]).
apply less_leEq_trans with (a[*]b); auto.
apply less_leEq.
Expand All @@ -1173,7 +1173,7 @@ Proof.
split; auto.
elim (ap_imp_less _ _ _ H7); auto.
intro H9.
elimtype False.
exfalso.
apply (less_irreflexive_unfolded R [0]).
apply less_leEq_trans with (a[*]b); auto.
apply less_leEq.
Expand Down Expand Up @@ -1468,11 +1468,11 @@ Proof.
intro n; induction n as [| n Hrecn].
intros m H.
induction m as [| m Hrecm].
elimtype False; generalize H; apply less_irreflexive_unfolded.
exfalso; generalize H; apply less_irreflexive_unfolded.
auto with arith.
intros m H.
induction m as [| m Hrecm].
elimtype False.
exfalso.
cut (nring (R:=R) 0 [<] nring (S n)).
apply less_antisymmetric_unfolded; assumption.
apply nring_less; auto with arith.
Expand Down Expand Up @@ -1539,7 +1539,7 @@ Lemma Sumx_resp_less : forall n, 0 < n -> forall f g : forall i, i < n -> R,
(forall i H, f i H [<] g i H) -> Sumx f [<] Sumx g.
Proof.
simple induction n.
intros; simpl in |- *; elimtype False; inversion H.
intros; simpl in |- *; exfalso; inversion H.
simple induction n0.
intros.
clear H.
Expand Down Expand Up @@ -1572,7 +1572,7 @@ Lemma positive_Sumx : forall n (f : forall i, i < n -> R),
Proof.
simple induction n.
simpl in |- *.
intros; elimtype False; generalize X; apply less_irreflexive_unfolded.
intros; exfalso; generalize X; apply less_irreflexive_unfolded.
simple induction n0.
simpl in |- *.
intros.
Expand Down
24 changes: 12 additions & 12 deletions algebra/COrdFields2.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -306,7 +306,7 @@ Proof.
assumption.
elim (ap_imp_less _ _ _ H7); intro H9.
assumption.
elimtype False.
exfalso.
elim (less_irreflexive_unfolded R [0]).
apply less_leEq_trans with (a[*]b).
assumption.
Expand All @@ -323,7 +323,7 @@ Proof.
split.
assumption.
elim (ap_imp_less _ _ _ H7); intro H9.
elimtype False.
exfalso.
elim (less_irreflexive_unfolded R [0]).
apply less_leEq_trans with (a[*]b).
assumption.
Expand Down Expand Up @@ -592,7 +592,7 @@ Proof.
auto with arith.
intros.
induction m as [| m Hrecm].
elimtype False.
exfalso.
cut (nring (R:=R) n [<] [0]).
change (Not (nring (R:=R) n[<](nring 0))).
rewrite <- leEq_def.
Expand All @@ -602,7 +602,7 @@ Proof.
apply nring_less.
apply lt_le_trans with (S n).
auto with arith.
elimtype False. revert H; rewrite -> leEq_def. intro H; destruct H.
exfalso. revert H; rewrite -> leEq_def. intro H; destruct H.
apply nring_less; auto with arith.
cut (n <= m).
auto with arith.
Expand Down Expand Up @@ -679,7 +679,7 @@ Lemma nexp_resp_less : forall (x y : R) n, 1 <= n -> [0] [<=] x -> x [<] y -> x[
Proof.
intros.
induction n as [| n Hrecn].
elimtype False.
exfalso.
inversion H.
elim n.
simpl in |- *.
Expand Down Expand Up @@ -797,9 +797,9 @@ Proof.
assumption.
intros.
elim (le_lt_dec m i); intro;
[ simpl in |- * | elimtype False; apply (le_not_lt m i); auto with arith ].
[ simpl in |- * | exfalso; apply (le_not_lt m i); auto with arith ].
elim (le_lt_dec i n); intro;
[ simpl in |- * | elimtype False; apply (le_not_lt i n); auto with arith ].
[ simpl in |- * | exfalso; apply (le_not_lt i n); auto with arith ].
apply H0.
Qed.

Expand Down Expand Up @@ -863,7 +863,7 @@ Lemma power_plus_leEq : forall n (x y:R), (0 < n) -> ([0][<=]x) -> ([0][<=]y) ->
(x[^]n [+] y[^]n)[<=](x[+]y)[^]n.
Proof.
intros [|n] x y Hn Hx Hy.
elimtype False; auto with *.
exfalso; auto with *.
induction n.
simpl.
rstepl ([1][*](x[+]y)).
Expand Down Expand Up @@ -921,7 +921,7 @@ Proof.
assumption.
elim (ap_imp_less _ _ _ H7); intro.
assumption.
elimtype False.
exfalso.
elim (less_irreflexive_unfolded R [0]).
apply less_leEq_trans with (a[*]b).
assumption.
Expand All @@ -938,7 +938,7 @@ Proof.
split.
assumption.
elim (ap_imp_less _ _ _ H7); intro.
elimtype False.
exfalso.
elim (less_irreflexive_unfolded R [0]).
apply less_leEq_trans with (a[*]b).
assumption.
Expand Down Expand Up @@ -1061,7 +1061,7 @@ Lemma square_eq_pos : forall x a : R, [0] [<] a -> [0] [<] x -> x[^]2 [=] a[^]2
Proof.
intros.
elim (square_eq _ x a); intros; auto.
elimtype False.
exfalso.
apply less_irreflexive_unfolded with (x := ZeroR).
apply less_leEq_trans with x.
auto.
Expand All @@ -1075,7 +1075,7 @@ Lemma square_eq_neg : forall x a : R, [0] [<] a -> x [<] [0] -> x[^]2 [=] a[^]2
Proof.
intros.
elim (square_eq _ x a); intros; auto.
elimtype False.
exfalso.
apply less_irreflexive_unfolded with (x := ZeroR).
apply leEq_less_trans with x.
astepr a; apply less_leEq; auto.
Expand Down
2 changes: 1 addition & 1 deletion algebra/CPolynomials.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -748,7 +748,7 @@ Proof.
intro.
rewrite cpoly_zero_plus.
intro H.
elimtype False.
exfalso.
apply (ap_irreflexive _ _ H).
do 4 intro.
pattern q in |- *; apply Ccpoly_ind_cs.
Expand Down
Loading