diff --git a/CaseStudies/Convergence/Impossibility_2G_1B.v b/CaseStudies/Convergence/Impossibility_2G_1B.v
index 5b6ce9852d59d84a6a32a25abdb7c8f0ef9795d9..5ee361a8755045a88670a54b83a97833a47a64e8 100644
--- a/CaseStudies/Convergence/Impossibility_2G_1B.v
+++ b/CaseStudies/Convergence/Impossibility_2G_1B.v
@@ -297,7 +297,7 @@ intros pt1 pt2 Hdiff pt k. induction k as [| k]; intros l Hnodup Hlen.
cbn [map]. rewrite map_app. cbn [map].
destruct (in_dec Geq_dec a (a :: half1 l)) as [_ | Habs].
destruct (in_dec Geq_dec z (a :: half1 l)) as [Habs | _].
- + inversion_clear Habs; try (now elim Haz); [].
+ + inversion_clear Habs; try (now contradiction Haz); [].
exfalso. now apply Hzl, half1_incl.
+ rewrite (map_ext_in _ (fun x => if in_dec Geq_dec x (half1 l) then pt1 else pt2)).
- cbn [countA_occ]. rewrite countA_occ_app. rewrite IHk; trivial.
@@ -309,9 +309,9 @@ intros pt1 pt2 Hdiff pt k. induction k as [| k]; intros l Hnodup Hlen.
- intros x Hin.
destruct (in_dec Geq_dec x (half1 l)) as [Hx | Hx],
(in_dec Geq_dec x (a :: half1 l)) as [Hx' | Hx']; trivial.
- -- elim Hx'. intuition.
+ -- contradiction Hx'. intuition.
-- inversion_clear Hx'; subst; contradiction.
- + elim Habs. intuition.
+ + contradiction Habs. intuition.
Qed.
Theorem obs_config1 : !! config1 == observation1.
diff --git a/CaseStudies/Exploration/ImpossibilityKDividesN.v b/CaseStudies/Exploration/ImpossibilityKDividesN.v
index 6eab56689e61b511490ba6f995f4b15f9d95c7a3..905f3a5e30fdb4f0b4083a9ce2db85229eab420e 100644
--- a/CaseStudies/Exploration/ImpossibilityKDividesN.v
+++ b/CaseStudies/Exploration/ImpossibilityKDividesN.v
@@ -17,11 +17,11 @@ Typeclasses eauto := (bfs).
Section Exploration.
(** Given an abitrary ring *)
-Context {gt2 : greater_than 2}.
+Context {_n : greater_than 2}.
(** There are k good robots and no byzantine ones. *)
-Context {gt0 : greater_than 0}.
-Notation n := (@ub 2 gt2).
-Notation k := (@ub 0 gt0).
+Context {_k : greater_than 0}.
+Notation n := (@ub 2 _n).
+Notation k := (@ub 0 _k).
Instance Robots : Names := Robots k 0.
(** Assumptions on the number of robots: it strictly divides the ring size. *)
@@ -33,7 +33,7 @@ Proof using kdn. apply Nat.div_exact. apply neq_ub_lb. apply kdn. Qed.
Lemma local_subproof2 : n / k ≠0.
Proof using kdn.
- intros Habs. eapply (@neq_ub_0 2 gt2). rewrite local_subproof1, Habs.
+ intros Habs. eapply (@neq_ub_0 2 _n). rewrite local_subproof1, Habs.
apply Nat.mul_0_r.
Qed.
@@ -186,7 +186,7 @@ Proof using Hmove kdn k_inf_n.
apply (f_equal (@fin2nat n)) in Hvisited. revert Hvisited.
cbn-[Nat.modulo Nat.div]. rewrite local_subproof1 at 2.
rewrite Nat.mul_mod_distr_r, (Nat.mod_small 1), Nat.mul_eq_1.
- intros [_ Habs]. elim (lt_not_le _ _ k_inf_n). rewrite local_subproof1,
+ intros [_ Habs]. contradiction (lt_not_le _ _ k_inf_n). rewrite local_subproof1,
Habs, Nat.mul_1_r. reflexivity. 3: apply local_subproof2.
2: apply neq_ub_lb. erewrite <- smaller_bound_ub. apply lt_lb_ub.
Unshelve. auto.
@@ -248,7 +248,7 @@ Lemma f_config_injective_N : ∀ config m1 m2,
-> m1 mod n == m2 mod n.
Proof using kdn k_inf_n.
unfold f_config. intros * Heq. specialize (Heq (Good fin0)).
- unshelve eapply (@addm_bounded_diff_inj 2 gt2). 5: rewrite 2 addm_mod.
+ unshelve eapply (@addm_bounded_diff_inj 2 _n). 5: rewrite 2 addm_mod.
5: apply Heq. 2,3: split. 2,4: apply Nat.le_0_l. all: apply mod2fin_lt.
Qed.
@@ -271,7 +271,7 @@ Definition equiv_config config1 config2 : Prop
Lemma equiv_config_m_sym : ∀ m config1 config2,
equiv_config_m m config1 config2
- -> equiv_config_m (@oppm 2 gt2 m) config2 config1.
+ -> equiv_config_m (@oppm 2 _n m) config2 config1.
Proof using k_inf_n kdn.
unfold equiv_config_m. intros * Hequiv. unshelve erewrite Hequiv,
f_config_merge, <- f_config_modulo, (proj2 (Nat.mod_divide _ _ _)).
@@ -289,7 +289,7 @@ Qed.
Instance equiv_config_equiv : Equivalence equiv_config.
Proof using k_inf_n kdn. split.
+ intro config. exists 0. unfold equiv_config_m. now rewrite f_config_0.
- + intros config1 config2 [m Hm]. exists (@oppm 2 gt2 m).
+ + intros config1 config2 [m Hm]. exists (@oppm 2 _n m).
apply (equiv_config_m_sym Hm).
+ intros ? ? ? [m1 Hm1] [m2 Hm2]. exists (m1 + m2).
revert Hm1 Hm2. apply equiv_config_m_trans.
@@ -354,7 +354,7 @@ Proof using .
Qed.
Lemma AlwaysEquiv_sym : ∀ m (e1 e2 : execution),
- AlwaysEquiv m e1 e2 -> AlwaysEquiv (@oppm 2 gt2 m) e2 e1.
+ AlwaysEquiv m e1 e2 -> AlwaysEquiv (@oppm 2 _n m) e2 e1.
Proof using k_inf_n kdn.
cofix Hcoind. intros m1 e1 e2 [Hnow Hlater]. constructor.
+ now apply equiv_config_m_sym.
@@ -481,7 +481,7 @@ Proof using Hmove k_inf_n kdn.
generalize (AlwaysEquiv_refl (execute r bad_demon ref_config)).
generalize 0 at 1. generalize (execute r bad_demon ref_config) at 1 3.
cofix Hcoind. intros e m Hequiv. constructor.
- + clear Hcoind. rewrite Hequiv. intros [Hstop _]. elim Hmove.
+ + clear Hcoind. rewrite Hequiv. intros [Hstop _]. contradiction Hmove.
unfold Stall in Hstop. rewrite execute_tail, round_simplify in Hstop.
simpl hd in Hstop. apply (move_along_I fin0). rewrite move_along_0.
apply fin2nat_inj. setoid_rewrite <- Nat.mod_small. 2,3: apply fin_lt.
diff --git a/CaseStudies/Exploration/Tower.v b/CaseStudies/Exploration/Tower.v
index e1c1639f3600d98c62e23a200005f131bb5bf693..316d99995e38a08b82c203f56d1df3433840de28 100644
--- a/CaseStudies/Exploration/Tower.v
+++ b/CaseStudies/Exploration/Tower.v
@@ -16,7 +16,6 @@
*)
(**************************************************************************)
-
Require Import Utf8 SetoidList Arith_base Lia.
From Pactole Require Import Util.Stream Util.Enum Util.Fin Models.NoByzantine
Models.RingSSync CaseStudies.Exploration.ExplorationDefs.
@@ -28,14 +27,16 @@ Typeclasses eauto := (bfs).
Section Tower.
(** Given an abitrary ring *)
-Context {RR : RingSpec}.
-(** There are S k good robots and no byzantine ones. *)
-Variable k : nat.
-Instance Robots : Names := Robots (S k) 0.
+Context {_n : greater_than 2}.
+(** There are k good robots and no byzantine ones. *)
+Context {_k : greater_than 0}.
+Notation n := (@ub 2 _n).
+Notation k := (@ub 0 _k).
+Instance Robots : Names := Robots k 0.
(** Assumptions on the number of robots: it is non zero and strictly divides the ring size. *)
-Hypothesis kdn : (S (S (S n)) mod (S k) = 0).
-Hypothesis k_inf_n : (S k < S (S (S n))).
+Hypothesis kdn : (n mod k = 0).
+Hypothesis k_inf_n : (k < n).
(** There is no byzantine robot. *)
Instance NoByz : NoByzantine.
@@ -46,26 +47,26 @@ Notation "!! config" :=
Notation execute := (execute (UpdFun := UpdFun)).
(** In order to prove that at least one position is occupied, we define the list of positions. *)
-Definition Vlist := enum (S (S (S n))).
+Definition Vlist := enum (n).
Lemma Vlist_NoDup : NoDupA equiv Vlist.
Proof using . rewrite NoDupA_Leibniz. apply enum_NoDup. Qed.
-Lemma Vlist_length : length Vlist = S (S (S n)).
+Lemma Vlist_length : length Vlist = n.
Proof using . apply enum_length. Qed.
(** As there is strictly less robots than location, there is an empty location. *)
Lemma ConfigExistsEmpty : ∀ config, ¬ (∀ pt, In pt (!! config)).
Proof using k_inf_n kdn.
generalize k_inf_n; intros Hkin config Hall.
- assert (Hsize : size (!! config) < S (S (S n))).
+ assert (Hsize : size (!! config) < n).
{ apply le_lt_trans with (cardinal (!! config)). apply size_cardinal.
- cut (cardinal (!! config) = S k). intros H. rewrite H. apply k_inf_n.
+ cut (cardinal (!! config) = k). intros H. rewrite H. apply k_inf_n.
change (cardinal (make_multiset (List.map get_location
- (config_list config))) = S k). rewrite cardinal_make_multiset,
+ (config_list config))) = k). rewrite cardinal_make_multiset,
config_list_spec, map_map, map_length, names_length. simpl.
rewrite Nat.add_0_r. reflexivity. }
- assert (Hle : S (S (S n)) <= size (!! config)).
+ assert (Hle : n <= size (!! config)).
{ rewrite size_spec. assert (Hobs : ∀ pt, InA equiv pt (support (!! config))).
{ intro pt. specialize (Hall pt). now rewrite support_spec. }
rewrite <- Vlist_length at 1. apply (Preliminary.inclA_length setoid_equiv).
@@ -166,7 +167,7 @@ Proof using .
Qed.
Lemma no_exploration_k_inf_2 : ∀ r d config,
- Fair d -> Explore_and_Stop r -> Valid_starting_config config -> S k > 1.
+ Fair d -> Explore_and_Stop r -> Valid_starting_config config -> k > 1.
Proof using k_inf_n kdn.
intros r d config Hfair Hsol Hvalid. assert (Hexr := exec_stopped r).
assert (Htower := tower_on_final_config).
diff --git a/CaseStudies/Gathering/Impossibility.v b/CaseStudies/Gathering/Impossibility.v
index d66724aa711b42ed72b92655d202cac7bb5d784f..803500306197b1e1603aa2bbb94d06af42de093d 100644
--- a/CaseStudies/Gathering/Impossibility.v
+++ b/CaseStudies/Gathering/Impossibility.v
@@ -307,8 +307,8 @@ assert (Hperm : PermutationA equiv (pt1 :: pt2 :: nil) (pt3 :: pt4 :: nil)).
revert Hobs. rewrite 2 support_add; auto; [].
destruct (In_dec pt3 (singleton pt4 (Nat.div2 nG))) as [Habs |];
[| destruct (In_dec pt1 (singleton pt2 (Nat.div2 nG))) as [Habs |]].
- - rewrite In_singleton in Habs. now elim Hdiff'.
- - rewrite In_singleton in Habs. now elim Hdiff.
+ - rewrite In_singleton in Habs. now contradiction Hdiff'.
+ - rewrite In_singleton in Habs. now contradiction Hdiff.
- rewrite 2 support_singleton; auto; []. now symmetry. }
repeat destruct_match; simpl; rewrite Hgh in *; intro.
+ assert (Heq1 : pt1 == pt3) by now transitivity (get_location (config2 (Good h))).
@@ -359,7 +359,7 @@ assert (Heven : Nat.Even nG).
repeat split; trivial; [|].
+ rewrite <- Nat.even_spec in Heven.
assert (HnG := nG_non_0). simpl nG in *.
- destruct n as [| [| ?]]; simpl; discriminate || lia || now elim HnG.
+ destruct n as [| [| ?]]; simpl; discriminate || lia || now contradiction HnG.
+ exists (sim origin), (sim one).
repeat split.
- intro Heq. apply Similarity.injective in Heq. symmetry in Heq. revert Heq. apply non_trivial.
@@ -460,20 +460,20 @@ destruct (invalid_dec config) as [Hvalid | Hvalid].
rewrite In_singleton in Hin, Hin';
try solve [ simpl in *; tauto ]; [|].
- destruct Hin' as [Hin' _]. apply Similarity.injective in Hin'.
- symmetry in Hin'. elim (non_trivial Hin').
+ symmetry in Hin'. contradiction (non_trivial Hin').
- rewrite 2 support_singleton; auto. }
rewrite PermutationA_2 in Hperm; autoclass; [].
destruct_match.
+ assert (Hpt1 : sim origin == pt1) by (etransitivity; eauto).
assert (Hpt2 : sim one == pt2).
- { decompose [and or] Hperm; auto; []. rewrite Hpt1 in *. now elim Hdiff. }
+ { decompose [and or] Hperm; auto; []. rewrite Hpt1 in *. now contradiction Hdiff. }
now rewrite <- Hpt2.
+ assert (Hpt2 : sim origin == pt2).
{ destruct (Hcase (Good g)); try contradiction; []. etransitivity; eauto. }
assert (Hpt1 : sim one == pt1).
- { decompose [and or] Hperm; auto; []. rewrite Hpt2 in *. now elim Hdiff. }
+ { decompose [and or] Hperm; auto; []. rewrite Hpt2 in *. now contradiction Hdiff. }
now rewrite <- Hpt1.
-* elim Hvalid.
+* contradiction Hvalid.
apply (invalid_reverse (build_similarity non_trivial Hdiff)).
rewrite Hobs. unfold observation0.
rewrite map_add, map_singleton, build_similarity_eq1, build_similarity_eq2; autoclass; [].
@@ -499,7 +499,7 @@ assert (Hconfig : round r da1 config == map_config (lift (existT precondition si
destruct (Hcase (Good g)) as [Hg' | Hg']; rewrite Hg' in *;
solve [ symmetry; apply build_similarity_eq1
| symmetry; apply build_similarity_eq2
- | auto; now elim Hg ]. }
+ | auto; now contradiction Hg ]. }
(* Let us pick an arbitrary robot (here [g0]) and consider a similarity [sim1]
that maps [!! config] to [observation0] and such that [sim1 g0 = origin]. *)
destruct (invalid_obs Hvalid g0) as [sim1 Hsim1 ?].
@@ -649,13 +649,13 @@ destruct (invalid_dec config) as [Hvalid | Hvalid].
assert (Hin := pos_in_config config origin id).
rewrite Hobs', add_In,In_singleton in Hin0, Hin.
destruct Hin as [[] | []], Hin0 as [[] | []];
- tauto || elim Hdiff; etransitivity; eauto. }
+ tauto || contradiction Hdiff; etransitivity; eauto. }
exists (symmetry Hdiff).
repeat destruct_match; simpl in *; destruct Hcase as [[] | []];
unfold Datatypes.id in *;
try solve [ congruence
| now apply Hb2; auto
- | elim Hdiff'; transitivity (config (Good g0)); auto ].
+ | contradiction Hdiff'; transitivity (config (Good g0)); auto ].
+ contradiction.
Qed.
@@ -831,9 +831,9 @@ assert (Hin1 : In (simâ»Â¹ one) (!! config)).
intro pt. rewrite Hobs, 2 add_spec, 2 singleton_spec.
repeat destruct_match;
solve [ lia
- | elim Hdiff; transitivity pt; eauto
- | elim Hdiff_sim; transitivity pt; eauto
- | elim Hdiff_sim;
+ | contradiction Hdiff; transitivity pt; eauto
+ | contradiction Hdiff_sim; transitivity pt; eauto
+ | contradiction Hdiff_sim;
apply (WithMultiplicity.invalid_same_location (reflexivity _) Hinvalid (pt3 := pt)); auto; try (now symmetry); [];
rewrite Hobs, add_In, In_singleton; auto
| rewrite Hobs, add_In, In_singleton in Hin0, Hin1;
@@ -907,7 +907,7 @@ destruct_match_eq Hcase.
* (* The robot is on the second tower so it does not move. *)
rewrite activate2_spec2 in Hcase; trivial; [].
fold sim.
- destruct_match; reflexivity || now elim Hcase; etransitivity; eauto.
+ destruct_match; reflexivity || now contradiction Hcase; etransitivity; eauto.
Qed.
Lemma invalid_da2_left_next : forall config,
@@ -971,7 +971,7 @@ do 2 destruct_match.
rewrite map_add, map_singleton, add_In, In_singleton in Hin; autoclass; [].
now destruct Hin as [[] | []]. }
rewrite Heq2, Heq1. fold sim.
- split; intro Heq; apply Similarity.injective in Heq; contradiction || now elim non_trivial.
+ split; intro Heq; apply Similarity.injective in Heq; contradiction || now contradiction non_trivial.
+ revert_one equiv. intro Heq2. rewrite Heq2.
change ((sim â»Â¹) 0%VS) with (Similarity.center sim) in Heq2.
unfold sim in Heq2. rewrite center_change_frame2, change_frame2_eq in Heq2; trivial; [].
@@ -981,7 +981,7 @@ do 2 destruct_match.
rewrite map_add, map_singleton, add_In, In_singleton in Hin; autoclass; [].
now destruct Hin as [[] | []]. }
rewrite Heq2, Heq1. fold sim.
- split; intro Heq; apply Similarity.injective in Heq; (now symmetry in Heq) || now elim non_trivial.
+ split; intro Heq; apply Similarity.injective in Heq; (now symmetry in Heq) || now contradiction non_trivial.
+ split; intro; solve [ etransitivity; eauto ].
Qed.
@@ -1008,7 +1008,7 @@ destruct_match_eq Hcase.
rewrite map_add, map_singleton, add_In, In_singleton in Hin; autoclass; [].
destruct Hin as [[] | []]; trivial; [].
rewrite activate2_spec2 in Hcase; trivial; [].
- elim Hcase. etransitivity; eauto; []. now apply center_change_frame2. }
+ contradiction Hcase. etransitivity; eauto; []. now apply center_change_frame2. }
rewrite (obs_from_config_ignore_snd origin).
assert (Hobs' : observation0 == map (change_frame2 config g) (!! config)).
{ rewrite <- map_id. Time change id with (Bijection.section Similarity.id).
@@ -1016,7 +1016,7 @@ destruct_match_eq Hcase.
rewrite (change_frame2_obs g Hinvalid), map_merge; autoclass. }
rewrite obs_from_config_ignore_snd, <- obs_from_config_map, <- Hobs'; autoclass; [].
destruct_match; try reflexivity; [].
- fold move. rewrite Hsim0 in *. elim non_trivial. eapply Similarity.injective; eauto.
+ fold move. rewrite Hsim0 in *. contradiction non_trivial. eapply Similarity.injective; eauto.
* (* The robot is on the first tower so it does not move. *)
destruct_match; try reflexivity; [].
exfalso. revert_one equiv. intro Heq.
@@ -1114,7 +1114,7 @@ do 2 destruct_match.
{ rewrite Hobs0. unfold observation0. rewrite map_add, map_singleton, add_In, In_singleton; autoclass. }
rewrite (change_frame2_obs g3 Hinvalid) in Hin. fold sim1 in Hin.
unfold observation0 in Hin. rewrite map_add, map_singleton, add_In, In_singleton in Hin; autoclass.
- decompose [and or] Hin; trivial; elim Hdiff; []. now rewrite <- 2 center_change_frame2. }
+ decompose [and or] Hin; trivial; contradiction Hdiff; []. now rewrite <- 2 center_change_frame2. }
rewrite Hcase in Heq. fold sim0 sim1 in Heq. rewrite Heq in Habs.
apply Similarity.injective in Habs. contradiction.
- symmetry in Heq. contradiction.
@@ -1127,7 +1127,7 @@ do 2 destruct_match.
rewrite map_add, map_singleton, add_In, In_singleton in Hin; autoclass; [].
now destruct Hin as [[] | []]. }
rewrite Heq1.
- split; intro Heq; try (apply Similarity.injective in Heq; now elim non_trivial); [].
+ split; intro Heq; try (apply Similarity.injective in Heq; now contradiction non_trivial); [].
destruct (change_frame2_case g3 Hinvalid (symmetry Hdiff) g1) as [Hcase | Hcase].
* rewrite <- Hcase, <- Heq1. symmetry. now apply center_change_frame2.
* change ((change_frame2 config g0 â»Â¹) 0%VS) with (Similarity.center (change_frame2 config g0)).
@@ -1137,7 +1137,7 @@ do 2 destruct_match.
{ rewrite Hobs0. unfold observation0. rewrite map_add, map_singleton, add_In, In_singleton; autoclass. }
rewrite (change_frame2_obs g3 Hinvalid) in Hin. unfold observation0 in Hin.
rewrite map_add, map_singleton, add_In, In_singleton in Hin; autoclass; [].
- decompose [and or] Hin; trivial; elim Hdiff; []. now rewrite <- 2 center_change_frame2. }
+ decompose [and or] Hin; trivial; contradiction Hdiff; []. now rewrite <- 2 center_change_frame2. }
rewrite Hcase in Heq. fold sim0 sim1 in Heq. rewrite <- Heq in Habs.
apply Similarity.injective in Habs. contradiction.
+ assert (Heq1 : get_location (config (Good g1)) == (sim0 â»Â¹) one).
diff --git a/CaseStudies/Gathering/InR/Algorithm.v b/CaseStudies/Gathering/InR/Algorithm.v
index 96b5f0f185f2f323af87b9ef79ae90c2e548693f..3f344479d6aed089d051840030b0a003425d7be4 100644
--- a/CaseStudies/Gathering/InR/Algorithm.v
+++ b/CaseStudies/Gathering/InR/Algorithm.v
@@ -202,10 +202,10 @@ rewrite <- (@cardinal_total_sub_eq _ _ _ _ _ (add pt2 (Nat.div2 nG) (singleton p
* rewrite size_add; try (now apply half_size_config); [].
destruct (In_dec pt2 (singleton pt1 (Nat.div2 nG))) as [Hin | Hin].
+ exfalso. rewrite In_singleton in Hin.
- destruct Hin. now elim Hdiff.
+ destruct Hin. now contradiction Hdiff.
+ rewrite size_singleton; trivial. apply half_size_config.
* intro pt. destruct (Rdec pt pt2), (Rdec pt pt1); subst.
- + now elim Hdiff.
+ + now contradiction Hdiff.
+ rewrite add_spec, singleton_spec.
setoid_rewrite Hpt2.
repeat destruct_match; simpl in *; contradiction || (try lia).
@@ -236,7 +236,7 @@ assert (Hsup : Permutation (support (!! config)) (pt1 :: pt2 :: nil)).
assert (Hin2 : InA equiv pt2 (support (!! config))).
{ rewrite support_spec. unfold In. setoid_rewrite Hpt2. apply half_size_config. }
apply (PermutationA_split _) in Hin1. destruct Hin1 as [l Hl]. rewrite Hl in Hin2.
- inversion_clear Hin2; try now subst; elim Hdiff.
+ inversion_clear Hin2; try now subst; contradiction Hdiff.
rewrite size_spec, Hl in Hsuplen. destruct l as [| x [| ? ?]]; simpl in Hsuplen; try lia.
inversion_clear H; (now inversion H0) || (cbn in H0; subst). now rewrite <- PermutationA_Leibniz. }
assert (Hpt : pt = pt1 \/ pt = pt2).
@@ -289,7 +289,7 @@ Proof using size_G.
intro abs.
subst.
inversion hnodup;subst.
- elim H1.
+ contradiction H1.
constructor.
reflexivity.
* assert (h : inclA equiv (support (max (!! config))) (support (!! config))).
@@ -314,7 +314,7 @@ Proof using size_G.
rewrite Hsupp in hnodup.
inversion hnodup;subst.
match goal with
- | H: ~ InA equiv pt2 (pt2 :: nil) |- _ => elim H
+ | H: ~ InA equiv pt2 (pt2 :: nil) |- _ => contradiction H
end.
constructor 1.
reflexivity. }
@@ -481,10 +481,10 @@ destruct Hfmon as [Hfinc | Hfdec].
- rewrite map_last in Heq. apply Hfinj in Heq. contradiction.
- intro Habs. apply map_eq_nil in Habs. now apply (sort_non_nil config).
+ rewrite (hd_indep _ (f 0)) in Hneq.
- - elim Hneq. rewrite map_hd. now f_equal.
+ - contradiction Hneq. rewrite map_hd. now f_equal.
- intro Habs. apply map_eq_nil in Habs. now apply (sort_non_nil config).
+ rewrite (last_indep _ (f 0)) in Hneq0.
- - elim Hneq0. rewrite map_last. now f_equal.
+ - contradiction Hneq0. rewrite map_last. now f_equal.
- intro Habs. apply map_eq_nil in Habs. now apply (sort_non_nil config).
* repeat Rdec_full; trivial;
rewrite map_injective_support, (sort_map_decreasing Hfdec) in Heq
@@ -499,10 +499,10 @@ destruct Hfmon as [Hfinc | Hfdec].
- rewrite last_rev_hd, map_hd in Heq. apply Hfinj in Heq. contradiction.
- intro Habs. rewrite rev_nil in Habs. apply map_eq_nil in Habs. now apply (sort_non_nil config).
+ rewrite (last_indep _ (f 0)) in Hneq0.
- - elim Hneq0. rewrite last_rev_hd, map_hd. now f_equal.
+ - contradiction Hneq0. rewrite last_rev_hd, map_hd. now f_equal.
- intro Habs. rewrite rev_nil in Habs. apply map_eq_nil in Habs. now apply (sort_non_nil config).
+ rewrite (hd_indep _ (f 0)) in Hneq.
- - elim Hneq. rewrite hd_rev_last, map_last. now f_equal.
+ - contradiction Hneq. rewrite hd_rev_last, map_last. now f_equal.
- intro Habs. rewrite rev_nil in Habs. apply map_eq_nil in Habs. now apply (sort_non_nil config).
Qed.
@@ -531,10 +531,10 @@ destruct (similarity_monotonic sim) as [Hinc | Hdec].
* rewrite map_injective_support, (sort_map_increasing Hinc); trivial; [].
assert (Hperm := Permuted_sort (support s)).
changeR. destruct (sort (support s)) as [| x l'].
- + symmetry in Hperm. apply Permutation_nil in Hperm. elim Hs. now rewrite <- support_nil.
+ + symmetry in Hperm. apply Permutation_nil in Hperm. contradiction Hs. now rewrite <- support_nil.
+ clear s Hs Hperm. simpl hd. cut (x :: l' <> nil). generalize (x :: l'). intro l.
generalize 0. induction l; intros r Hl.
- - now elim Hl.
+ - now contradiction Hl.
- simpl. destruct l.
simpl. symmetry. now apply similarity_middle.
rewrite <- IHl. reflexivity. discriminate.
@@ -543,10 +543,10 @@ destruct (similarity_monotonic sim) as [Hinc | Hdec].
rewrite last_rev_hd, hd_rev_last.
assert (Hperm := Permuted_sort (support s)).
changeR. destruct (sort (support s)) as [| x l'].
- + symmetry in Hperm. apply Permutation_nil in Hperm. elim Hs. now rewrite <- support_nil.
+ + symmetry in Hperm. apply Permutation_nil in Hperm. contradiction Hs. now rewrite <- support_nil.
+ clear s Hs Hperm. simpl hd. cut (x :: l' <> nil). generalize (x :: l'). intro l.
generalize 0. induction l; intros r Hl.
- - now elim Hl.
+ - now contradiction Hl.
- simpl. destruct l.
-- simpl. rewrite similarity_middle. now rewrite Rplus_comm.
-- rewrite <- IHl. reflexivity. discriminate.
@@ -855,7 +855,7 @@ assert (Heq : config id == round gatherR da config id).
{ rewrite (round_simplify_Generic Hmaj Hlen id); trivial; [].
destruct (da.(activate) id); try reflexivity; [].
unfold is_extremal. Rdec_full; try reflexivity; [].
- elim Hneq. rewrite Hid. apply hd_indep. apply sort_non_nil. }
+ contradiction Hneq. }
(** Main proof *)
apply Rle_antisym.
* apply sort_min.
@@ -898,7 +898,7 @@ assert (Heq : config id == round gatherR da config id).
{ rewrite (round_simplify_Generic Hmaj Hlen id).
destruct (da.(activate) id); try reflexivity; [].
unfold is_extremal. repeat Rdec_full; try reflexivity; [].
- elim Hneq0. rewrite Hid. apply last_indep. apply sort_non_nil. }
+ contradiction Hneq0. }
(** Main proof *)
apply Rle_antisym.
* apply sort_max.
@@ -948,10 +948,10 @@ induction names as [| id l]; simpl in *; unfold Datatypes.id in *.
+ destruct_match_eq Hext; repeat destruct_match.
- f_equal. apply IHl.
- apply IHl.
- - elim (Rlt_irrefl (mini (!! config))).
+ - contradiction (Rlt_irrefl (mini (!! config))).
match goal with H : extreme_center _ == _ |- _ => rewrite <- H at 2 end.
now apply Generic_min_mid_lt.
- - elim (Rlt_irrefl (mini (!! config))).
+ - contradiction (Rlt_irrefl (mini (!! config))).
match goal with H : extreme_center _ == _ |- _ => rewrite <- H at 2 end.
now apply Generic_min_mid_lt.
- exfalso. revert Hext. unfold is_extremal. repeat destruct_match; tauto || discriminate.
@@ -976,10 +976,10 @@ induction names as [| id l]; simpl.
+ destruct_match_eq Hext; repeat destruct_match.
- f_equal. apply IHl.
- apply IHl.
- - elim (Rlt_irrefl (maxi (!! config))).
+ - contradiction (Rlt_irrefl (maxi (!! config))).
match goal with H : extreme_center _ == _ |- _ => rewrite <- H at 1 end.
now apply Generic_mid_max_lt.
- - elim (Rlt_irrefl (maxi (!! config))).
+ - contradiction (Rlt_irrefl (maxi (!! config))).
match goal with H : extreme_center _ == _ |- _ => rewrite <- H at 1 end.
now apply Generic_mid_max_lt.
- exfalso. revert Hext. unfold is_extremal. repeat destruct_match; tauto || discriminate.
@@ -1018,7 +1018,7 @@ destruct (da.(activate) id1) eqn:Hmove1; [destruct (da.(activate) id2) eqn:Hmove
cbv zeta.
destruct (support (max (!! config))) as [| pt [| ? ?]] eqn:Hmaj.
+ (* no robots *)
- rewrite support_nil, max_is_empty in Hmaj. elim (obs_non_nil _ Hmaj).
+ rewrite support_nil, max_is_empty in Hmaj. contradiction (obs_non_nil _ Hmaj).
+ (* a majority tower *)
reflexivity.
+ destruct (size (!! config) =? 3) eqn:Hlen.
@@ -1053,7 +1053,7 @@ Proof using size_G.
intros config pt1 pt2 Hlen Hpt1 Hpt2 Hdiff12.
rewrite <- support_spec in Hpt1, Hpt2. rewrite size_spec in Hlen.
apply (PermutationA_split _) in Hpt1. destruct Hpt1 as [supp1 Hperm].
-rewrite Hperm in Hpt2. inversion_clear Hpt2; try (now elim Hdiff12); []. rename H into Hpt2.
+rewrite Hperm in Hpt2. inversion_clear Hpt2; try (now contradiction Hdiff12); []. rename H into Hpt2.
apply (PermutationA_split _) in Hpt2. destruct Hpt2 as [supp2 Hperm2].
rewrite Hperm2 in Hperm. rewrite Hperm in Hlen.
destruct supp2 as [| pt3 supp]; try (now simpl in Hlen; lia); [].
@@ -1108,7 +1108,7 @@ intros config pt. split.
{ intros id' Hid'. destruct (get_location (round gatherR da config id') =?= pt) as [Heq | Heq]; trivial; [].
assert (Habs := Heq). rewrite <- Hid' in Habs.
assert (Habs' : round gatherR da config id' =/= config id').
- { intro Habs'. rewrite Habs' in Habs. now elim Habs. }
+ { intro Habs'. rewrite Habs' in Habs. now contradiction Habs. }
rewrite <- (moving_spec gatherR) in Habs'. apply Hdest in Habs'. contradiction. }
do 2 rewrite obs_from_config_spec, config_list_spec.
assert (Hin : List.In id names) by apply In_names.
@@ -1116,13 +1116,13 @@ intros config pt. split.
inversion_clear Hin.
+ subst id'. clear IHl. simpl. hnf in Hroundid. unfold Datatypes.id.
destruct_match. revert_one @equiv. intro Heq.
- - rewrite <- Hid in Heq. elim Hroundid. now apply WithMultiplicity.no_info.
+ - rewrite <- Hid in Heq. contradiction Hroundid. now apply WithMultiplicity.no_info.
- destruct_match; try contradiction; []. apply le_n_S. induction l; simpl.
-- reflexivity.
-- repeat destruct_match; try now idtac + apply le_n_S + apply le_S; apply IHl.
- revert_one @complement. intro Hneq. elim Hneq. now apply Hstay.
+ revert_one @complement. intro Hneq. contradiction Hneq. now apply Hstay.
+ apply IHl in H. simpl in *. repeat destruct_match; try lia; [].
- revert_one @complement. intro Hneq. elim Hneq.
+ revert_one @complement. intro Hneq. contradiction Hneq.
apply Hdest. rewrite moving_spec. intro Habs. apply Hneq. now rewrite Habs.
Qed.
@@ -1161,7 +1161,7 @@ destruct (support (max (!! config))) as [| pt [| pt' l']] eqn:Hmaj.
{ assert (Hperm : Permutation (support (!! (round gatherR da config))) (pt1 :: pt2 :: nil)).
{ symmetry. apply NoDup_Permutation_bis.
+ repeat constructor.
- - intro Habs. inversion Habs. now elim Hdiff. now inversion H.
+ - intro Habs. inversion Habs. now contradiction Hdiff. now inversion H.
- intro Habs. now inversion Habs.
(* NoDupA_Leibniz had a useless hyp in coq stdlib until april 2020. *)
(* + rewrite <- NoDupA_Leibniz. change eq with (@equiv location _). apply support_NoDupA. *)
@@ -1338,7 +1338,7 @@ assert (Hstep : da.(activate) gmove = true).
rewrite moving_spec in Hmove.
destruct (support (max (!! config))) as [| pt [| ? ?]] eqn:Hmaj.
* (* No robots *)
- elim (support_max_non_nil _ Hmaj).
+ contradiction (support_max_non_nil _ Hmaj).
* (* A majority tower *)
rewrite <- MajTower_at_equiv in Hmaj.
assert (Hmaj' : MajTower_at pt (round gatherR da config)) by now apply MajTower_at_forever.
@@ -1349,7 +1349,7 @@ destruct (support (max (!! config))) as [| pt [| ? ?]] eqn:Hmaj.
cut ((!! config)[pt] < (!! (round gatherR da config))[pt]). lia.
assert (Hdestg : get_location (round gatherR da config gmove) = pt).
{ rewrite (round_simplify_Majority Hmaj gmove).
- destruct (da.(activate) gmove); trivial; now elim Hstep. }
+ destruct (da.(activate) gmove); reflexivity || contradiction diff_false_true. }
rewrite increase_move_iff. eauto.
* rename Hmaj into Hmaj'.
assert (Hmaj : no_Majority config).
@@ -1385,7 +1385,7 @@ destruct (support (max (!! config))) as [| pt [| ? ?]] eqn:Hmaj.
unfold gt. rewrite increase_move_iff.
exists gmove. split; trivial; [].
rewrite (round_simplify_Three Hmaj Hlen gmove).
- destruct (da.(activate) gmove); reflexivity || now elim Hstep.
+ destruct (da.(activate) gmove); reflexivity || contradiction diff_false_true.
+ (* Generic case *)
red. rewrite (config_to_NxN_Generic_spec Hmaj Hlen).
destruct (support (max (!! (round gatherR da config)))) as [| pt' [| ? ?]] eqn:Hmaj'.
@@ -1414,9 +1414,9 @@ destruct (support (max (!! config))) as [| pt [| ? ?]] eqn:Hmaj.
lia.
rewrite increase_move_iff. exists gmove. split; trivial.
rewrite (round_simplify_Generic Hmaj Hlen gmove) in Hmove |- *; trivial; [].
- destruct (da.(activate) gmove); try (now elim Hstep); [].
+ destruct (da.(activate) gmove); [| contradiction diff_false_true].
destruct (is_extremal (config gmove) (!! config)).
- -- now elim Hmove.
+ -- now contradiction Hmove.
-- reflexivity.
Qed.
@@ -1453,7 +1453,7 @@ Lemma not_gathered_exists : forall config pt,
Proof using .
intros config pt Hgather.
destruct (forallb (fun x => if get_location (config x) =?= pt then true else false) names) eqn:Hall.
-- elim Hgather. rewrite forallb_forall in Hall.
+- contradiction Hgather. rewrite forallb_forall in Hall.
intro id'. setoid_rewrite Rdec_bool_true_iff in Hall. hnf. repeat rewrite Hall; trivial; apply In_names.
- rewrite <- negb_true_iff, existsb_forallb, existsb_exists in Hall.
destruct Hall as [id' [_ Hid']]. revert Hid'. destruct_match; discriminate || intro. now exists id'.
@@ -1476,7 +1476,7 @@ Theorem OneMustMove : forall config id, ~ WithMultiplicity.invalid config -> ~ga
Proof using size_G.
intros config id Hinvalid Hgather.
destruct (support (max (!! config))) as [| pt [| pt' l]] eqn:Hmaj.
-* elim (support_max_non_nil _ Hmaj).
+* contradiction (support_max_non_nil _ Hmaj).
* rewrite <- MajTower_at_equiv in Hmaj.
apply not_gathered_generalize with _ _ pt in Hgather.
apply not_gathered_exists in Hgather. destruct Hgather as [gmove Hmove].
@@ -1558,7 +1558,7 @@ intros da Hda config pt Hgather. rewrite (round_simplify_Majority).
induction names as [| id l].
+ reflexivity.
+ simpl. destruct_match.
- - elim Hdiff. simpl in *. subst. apply (no_byz id), Hgather.
+ - contradiction Hdiff. simpl in *. subst. apply (no_byz id), Hgather.
- apply IHl. }
rewrite H0. specialize (Hgather g1). rewrite <- Hgather. apply pos_in_config.
Qed.
diff --git a/CaseStudies/Gathering/InR/Impossibility.v b/CaseStudies/Gathering/InR/Impossibility.v
index 87188c3e1a6e82843bd865613cdab0c8aa5fa027..baec20937357c06dd3ba71c6251e723413844c54 100644
--- a/CaseStudies/Gathering/InR/Impossibility.v
+++ b/CaseStudies/Gathering/InR/Impossibility.v
@@ -308,7 +308,7 @@ assert (Heven : Nat.Even nG).
repeat split; trivial; [|].
+ rewrite <- Nat.even_spec in Heven.
assert (HnG := nG_non_0). simpl nG in *.
- destruct n as [| [| ?]]; simpl; discriminate || lia || now elim HnG.
+ destruct n as [| [| ?]]; simpl; discriminate || lia || now apply HnG.
+ exists (sim origin), (sim one).
repeat split.
- intro Heq. apply Similarity.injective in Heq. symmetry in Heq. revert Heq. apply non_trivial.
@@ -429,7 +429,7 @@ destruct (invalid_dec config) as [Hvalid | Hvalid].
{ decompose [and or] Hperm; unfold origin in *; simpl in *; congruence. }
simpl get_location. unfold id.
rewrite <- Hpt1. f_equiv. apply Hmove.
-* elim Hvalid.
+* contradiction Hvalid.
apply (invalid_reverse (build_similarity neq_0_1 Hdiff)).
rewrite Hobs. unfold observation0.
rewrite map_add, map_singleton, build_similarity_eq1, build_similarity_eq2; autoclass.
@@ -577,7 +577,7 @@ destruct (invalid_dec config) as [Hvalid | Hvalid].
repeat destruct_match; try contradiction; [|].
- simpl in *. destruct Hperm as [[] | []]; subst; auto.
- simpl in *. destruct Hperm as [[] | []]; subst; auto; congruence.
-+ elim Hvalid.
++ contradiction Hvalid.
apply (invalid_reverse (build_similarity neq_0_1 Hdiff)).
rewrite Hobs. unfold observation0.
rewrite map_add, map_singleton; autoclass; [].
@@ -719,7 +719,7 @@ destruct (get_location (config (Good g)) =?= get_location (config (Good g0))) as
- now rewrite build_similarity_eq1, Hsim0.
- rewrite build_similarity_eq2. rewrite Hobs in Hpt'. unfold observation0 in Hpt'.
rewrite map_add, map_singleton, add_In, In_singleton in Hpt'; autoclass; [].
- decompose [and or] Hpt'; auto; []. elim Hdiff'. etransitivity; eauto. }
+ decompose [and or] Hpt'; auto; []. contradiction Hdiff'. etransitivity; eauto. }
rewrite obs_from_config_ignore_snd, <- obs_from_config_map; autoclass; [].
rewrite Hobs, map_merge; autoclass; [].
rewrite <- (map_extensionality_compat Similarity.id), map_id; autoclass; [|].
@@ -735,11 +735,11 @@ destruct (get_location (config (Good g)) =?= get_location (config (Good g0))) as
{ assert (Hin := pos_in_config config origin (Good g)).
rewrite Hobs in Hin. unfold observation0 in Hin.
rewrite map_add, map_singleton, add_In, In_singleton in Hin; autoclass; [].
- destruct Hin as [[] | []]; trivial. elim Hcase. etransitivity; eauto. }
+ destruct Hin as [[] | []]; trivial. contradiction Hcase. etransitivity; eauto. }
destruct (select_tower_case_2 (fun pt1 pt2 (_ : pt1 =/= pt2) => true)
(fun pt1 pt2 (_ : pt1 =/= pt2) => false) true (Good g) Hvalid Hcase) as [Hdiff Hactivate].
rewrite Hactivate.
- destruct_match; trivial; []. elim Hcase. etransitivity; eauto.
+ destruct_match; trivial; []. contradiction Hcase. etransitivity; eauto.
Qed.
Lemma invalid_da2_left_next : forall config,
@@ -816,7 +816,7 @@ destruct (get_location (config (Good g)) =?= get_location (config (Good g0))) as
{ assert (Hin := pos_in_config config origin (Good g)).
rewrite Hobs in Hin. unfold observation0 in Hin.
rewrite map_add, map_singleton, add_In, In_singleton in Hin; autoclass; [].
- destruct Hin as [[] | []]; trivial; []. elim Hcase. etransitivity; eauto. }
+ destruct Hin as [[] | []]; trivial; []. contradiction Hcase. etransitivity; eauto. }
destruct (select_tower_case_2 (fun pt1 pt2 (_ : pt1 =/= pt2) => false)
(fun pt1 pt2 (_ : pt1 =/= pt2) => true) true (Good g) Hvalid Hcase) as [Hdiff Hactivate].
destruct (select_tower_case_2 (fun pt1 pt2 (Hdiff0 : pt1 =/= pt2) => build_similarity Hdiff0 neq_0_1)
@@ -831,7 +831,7 @@ destruct (get_location (config (Good g)) =?= get_location (config (Good g0))) as
rewrite Hobs, map_merge; autoclass; [].
rewrite <- (map_extensionality_compat Similarity.id), map_id; autoclass; [|].
+ destruct_match.
- - elim neq_0_1. apply (Similarity.injective sim).
+ - contradiction neq_0_1. apply (Similarity.injective sim).
now transitivity (get_location (config (Good g))).
- transitivity ((build_similarity (symmetry Hcase) neq_1_0)â»Â¹ move); try reflexivity; [].
rewrite Hsim, build_similarity_inverse.
@@ -870,7 +870,7 @@ assert (Hcase' : forall id, get_location (config id) = sim 0 \/ get_location (co
{ intro id. assert (Hin := pos_in_config config origin id). unfold observation0 in *.
rewrite Hobs', map_add, map_singleton, add_In, In_singleton in Hin; autoclass; simpl in *; tauto. }
assert (Hsim1 : get_location (config (Good g0)) == sim 1).
-{ destruct (Hcase' (Good g0)); trivial; []. elim Hg3. now rewrite <- Hsim0. }
+{ destruct (Hcase' (Good g0)); trivial; []. contradiction Hg3. now rewrite <- Hsim0. }
clear pt1 pt2 g1 g2 Hg1 Hg2 Hdiff Hobs Hcase.
assert (Hdiff_move : sim move =/= sim 1).
{ intro Heq. now apply Similarity.injective in Heq. }
@@ -928,7 +928,7 @@ assert (Hcase' : forall id, get_location (config id) = sim 0 \/ get_location (co
{ intro id. assert (Hin := pos_in_config config origin id). unfold observation0 in *.
rewrite Hobs', map_add, map_singleton, add_In, In_singleton in Hin; autoclass; simpl in *; tauto. }
assert (Hsim1 : get_location (config (Good g0)) == sim 1).
-{ destruct (Hcase' (Good g0)); trivial; []. elim Hg3. now rewrite <- Hsim0. }
+{ destruct (Hcase' (Good g0)); trivial; []. contradiction Hg3. now rewrite <- Hsim0. }
clear pt1 pt2 g1' g2' Hg1 Hg2 Hdiff Hobs Hcase.
erewrite 2 round_simplify2_right; auto; [].
rewrite 2 mk_info_get_location.
diff --git a/CaseStudies/Gathering/InR2/Algorithm.v b/CaseStudies/Gathering/InR2/Algorithm.v
index 84607b8de3847654e39425572092eca906e7ad36..8d4584667778b4e934821b62f7148f2b5becc5e5 100644
--- a/CaseStudies/Gathering/InR2/Algorithm.v
+++ b/CaseStudies/Gathering/InR2/Algorithm.v
@@ -244,9 +244,9 @@ intros ? ? Heq. unfold is_clean.
destruct (inclA_bool _ equiv_dec (support x) (SECT x)) eqn:Hx,
(inclA_bool _ equiv_dec (support y) (SECT y)) eqn:Hy;
trivial; rewrite ?inclA_bool_true_iff, ?inclA_bool_false_iff in *; [|].
-+ elim Hy. intros e Hin. rewrite <- Heq in Hin.
++ contradiction Hy. intros e Hin. rewrite <- Heq in Hin.
apply SECT_compat in Heq. rewrite <- Heq. now apply Hx.
-+ elim Hx. intros e Hin. rewrite Heq in Hin.
++ contradiction Hx. intros e Hin. rewrite Heq in Hin.
apply SECT_compat in Heq. rewrite Heq. now apply Hy.
Qed.
@@ -362,7 +362,7 @@ intros config pt. split; intro Hmaj.
-- rewrite e. reflexivity.
-- apply lt_le_weak. now apply (Hmaj x).
- destruct (equiv_dec y pt) as [? | Hy]; trivial.
- exfalso. apply (Hmaj y) in Hy. elim (lt_irrefl (!! config)[pt]).
+ exfalso. apply (Hmaj y) in Hy. contradiction (lt_irrefl (!! config)[pt]).
eapply le_lt_trans; try eassumption; [].
apply Hpt.
* intros x Hx. apply max_spec_lub.
@@ -453,7 +453,7 @@ assert (Hsup : Permutation (support (!! config)) (pt1 :: pt2 :: nil)).
assert (Hin2 : InA equiv pt2 (support (!! config))).
{ rewrite support_spec. unfold In. changeR2. setoid_rewrite Hpt2. now apply Exp_prop.div2_not_R0. }
apply (PermutationA_split _) in Hin1. destruct Hin1 as [l Hl]. rewrite Hl in Hin2.
- inversion_clear Hin2; try now subst; elim Hdiff.
+ inversion_clear Hin2; try now subst; contradiction Hdiff.
rewrite size_spec, Hl in Hsuplen. destruct l as [| x [| ? ?]]; simpl in Hsuplen; try lia.
inversion_clear H.
- inversion H0; simpl in H1; subst.
@@ -514,7 +514,7 @@ intro config. unfold no_Majority. split.
intro abs.
subst.
inversion hnodup; subst.
- elim H1.
+ contradiction H1.
constructor.
reflexivity.
* assert (h : inclA equiv (support (max (!! config))) (support (!! config))).
@@ -537,7 +537,7 @@ intro config. unfold no_Majority. split.
assert (hnodup := support_NoDupA (!! config)).
rewrite Hsupp in hnodup.
inversion hnodup; subst.
- match goal with H : ~ InA equiv pt2 (pt2 :: nil) |- _ => elim H end.
+ match goal with H : ~ InA equiv pt2 (pt2 :: nil) |- _ => contradiction H end.
constructor 1.
reflexivity. }
assert (heq_config: !! config == Madd pt1 ((!! config)[pt1]) (Madd pt2 ((!! config)[pt2]) empty)).
@@ -824,10 +824,10 @@ intros sim s s_nonempty. unfold is_clean. changeR2.
destruct (inclA_bool _ equiv_dec (support (map sim s)) (SECT (map sim s))) eqn:Hx,
(inclA_bool _ equiv_dec (support s) (SECT s)) eqn:Hy;
trivial; rewrite ?inclA_bool_true_iff, ?inclA_bool_false_iff, ?inclA_Leibniz in *; [|].
-- elim Hy. intros x Hin. apply (in_map sim) in Hin. rewrite <- map_sim_support in Hin.
+- contradiction Hy. intros x Hin. apply (in_map sim) in Hin. rewrite <- map_sim_support in Hin.
apply Hx in Hin. rewrite SECT_morph, in_map_iff in Hin;auto.
destruct Hin as [x' [Heq ?]]. apply (Similarity.injective sim) in Heq. now rewrite <- Heq.
-- elim Hx. intros x Hin. rewrite SECT_morph; auto. rewrite map_sim_support in Hin.
+- contradiction Hx. intros x Hin. rewrite SECT_morph; auto. rewrite map_sim_support in Hin.
rewrite in_map_iff in *. destruct Hin as [x' [? Hin]]. subst. exists x'. repeat split. now apply Hy.
Qed.
@@ -1109,7 +1109,7 @@ destruct (support (max (!! config))) as [| pt1 [| pt2 l]] eqn:Hmax,
(support (max (!! (map_config sim config)))) as [| pt1' [| pt2' l']];
simpl in Hlen; discriminate || clear Hlen; [| |].
* (* No maximal tower *)
- rewrite support_nil, max_is_empty in Hmax. elim (obs_non_nil _ Hmax).
+ rewrite support_nil, max_is_empty in Hmax. contradiction (obs_non_nil _ Hmax).
* (* One maximal tower *)
simpl in Hperm. rewrite <- PermutationA_Leibniz, (PermutationA_1 _) in Hperm.
subst pt1'. apply Bijection.retraction_section.
@@ -1202,7 +1202,7 @@ destruct (da.(activate) id) eqn:Hactive.
destruct (is_clean (!! config)) eqn:Hclean.
+ reflexivity.
+ destruct (mem equiv_dec (get_location (config id)) (SECT (!! config))) eqn:Hmem.
- - now elim Hmove.
+ - now contradiction Hmove.
- reflexivity.
* apply moving_active in Hmove; trivial; []. rewrite active_spec in Hmove. congruence.
Qed.
@@ -1217,10 +1217,10 @@ destruct (le_lt_dec 2 (length (support (max (!! config))))) as [Hle |Hlt].
now repeat rewrite destination_is_target.
+ rewrite moving_spec in Hmove1, Hmove2.
rewrite (round_simplify _ id1) in Hmove1 |- *. rewrite (round_simplify _ id2) in Hmove2 |- *.
- destruct (da.(activate) id1), (da.(activate) id2); try (now elim Hmove1 + elim Hmove2); [].
+ destruct (da.(activate) id1), (da.(activate) id2); try (now contradiction Hmove1 + contradiction Hmove2); [].
cbn zeta in *.
destruct (support (max (!! config))) as [| ? [| ? ?]] eqn:Hsupp.
- - now elim Hmove1.
+ - now contradiction Hmove1.
- reflexivity.
- simpl in Hlt. lia.
Qed.
@@ -1281,14 +1281,14 @@ intros config pt. split.
induction names as [| id' l]; try (now inversion Hin); [].
inversion_clear Hin.
+ subst id'. clear IHl. simpl. R2dec_full.
- - rewrite <- Hid in Heq. now elim Hroundid.
+ - rewrite <- Hid in Heq. now contradiction Hroundid.
- R2dec_full; try contradiction; [].
apply le_n_S. induction l as [| id' ?]; simpl.
-- reflexivity.
-- repeat R2dec_full; try now idtac + apply le_n_S + apply le_S; apply IHl.
exfalso. now generalize (Hstay id' ltac:(assumption)).
+ apply IHl in H. simpl. repeat R2dec_full; try (simpl in *; lia); [].
- elim Hneq. apply Hdest. rewrite moving_spec. intro Habs. rewrite Habs in Hneq. contradiction.
+ contradiction Hneq. apply Hdest. rewrite moving_spec. intro Habs. rewrite Habs in Hneq. contradiction.
Qed.
(** *** Generic results about the [SEC] after one round **)
@@ -1314,7 +1314,7 @@ destruct (@increase_move gatherR2 config x) as [r_moving [Hdest_rmoving Hrmoving
* simpl in *. lia.
* destruct (le_lt_dec 2 (length (support (max (!! config))))) as [Hle | Hlt].
+ rewrite destination_is_target in Hdest_rmoving.
- - now elim Heq.
+ - now contradiction Heq.
- unfold no_Majority. now rewrite size_spec.
- rewrite moving_spec. intro Habs. apply Hrmoving. now rewrite Habs.
+ assert ((support (max (!! config))) = x :: nil).
@@ -1386,7 +1386,7 @@ intros config id Hmaj Hclean Hcircle.
rewrite (round_simplify_dirty Hmaj Hclean id).
destruct (da.(activate) id); try reflexivity; [].
destruct (mem equiv_dec (get_location (config id)) (SECT (!! config))) eqn:Hmem; try reflexivity; [].
-rewrite mem_false_iff in Hmem. elim Hmem.
+rewrite mem_false_iff in Hmem. contradiction Hmem.
unfold SECT. right. unfold on_SEC. rewrite filter_InA; autoclass; [].
split; trivial; [].
rewrite support_spec. apply pos_in_config.
@@ -1541,8 +1541,8 @@ assert (Hext : forall x, f (!! (round gatherR2 da config)) x = f (!! config) x).
{ intro pt. unfold f.
destruct (InA_dec equiv_dec pt (SECT (!! config))) as [Htest1 | Htest1],
(InA_dec equiv_dec pt (SECT (!! (round gatherR2 da config)))) as [Htest2 | Htest2]; trivial.
- - elim Htest2. now rewrite HsameSECT.
- - elim Htest1. now rewrite <- HsameSECT. }
+ - contradiction Htest2. now rewrite HsameSECT.
+ - contradiction Htest1. now rewrite <- HsameSECT. }
unfold f in Hext.
rewrite (filter_extensionality_compat _ _ Hext). clear Hext.
pose (f_target := fun x => if equiv_dec x (target (!! config)) then true else false).
@@ -1589,7 +1589,7 @@ assert (Heq : @equiv observation observation_Setoid (filter f_out_target (!! (ro
unfold f_target in Htest.
revert Htest. destruct_match; try discriminate; auto.
-- apply IHl.
- - destruct_match; (now elim Hneq) || apply IHl. }
+ - destruct_match; (now contradiction Hneq) || apply IHl. }
rewrite Heq.
lia.
Qed.
@@ -1605,7 +1605,7 @@ Proof using size_G.
intros config pt1 pt2 Hlen Hpt1 Hpt2 Hdiff12.
rewrite <- support_spec in Hpt1, Hpt2. rewrite size_spec in Hlen.
apply (PermutationA_split _) in Hpt1. destruct Hpt1 as [supp1 Hperm].
-rewrite Hperm in Hpt2. inversion_clear Hpt2; try (now elim Hdiff12); []. rename H into Hpt2.
+rewrite Hperm in Hpt2. inversion_clear Hpt2; try (now contradiction Hdiff12); []. rename H into Hpt2.
apply (PermutationA_split _) in Hpt2. destruct Hpt2 as [supp2 Hperm2].
rewrite Hperm2 in Hperm. rewrite Hperm in Hlen.
destruct supp2 as [| pt3 supp]; try (now simpl in Hlen; lia); [].
@@ -1671,7 +1671,7 @@ destruct (support (max (!! config))) as [| pt [| pt' l']] eqn:Hmaj.
{ assert (Hperm : Permutation (support (!! (round gatherR2 da config))) (pt1 :: pt2 :: nil)).
{ symmetry. apply NoDup_Permutation_bis.
+ repeat constructor.
- - intro Habs. inversion Habs. now elim Hdiff. now inversion H.
+ - intro Habs. inversion Habs. now contradiction Hdiff. now inversion H.
- intro Habs. now inversion Habs.
(* NoDupA_Leibniz had a useless hyp in coq stdlib until april 2020. *)
(* + rewrite <- NoDupA_Leibniz. change eq with (@equiv location _). apply support_NoDupA. *)
@@ -1847,7 +1847,7 @@ intros config ptx pty Hinvalid Hmaj Hclean Hsec.
assert (Hperm := diameter_clean_support Hinvalid Hmaj Hclean Hsec).
destruct (support (max (!! (round gatherR2 da config)))) as [| pt [| ? ?]] eqn:Hmax'.
- rewrite support_nil, max_is_empty, <- support_nil in Hmax'.
- now elim (support_non_nil _ Hmax').
+ now contradiction (support_non_nil _ Hmax').
- left. exists pt.
rewrite MajTower_at_equiv. now rewrite Hmax'.
- right.
@@ -2047,7 +2047,7 @@ Lemma triangle_next_maj_or_diameter_or_triangle : forall config,
Proof using Hssync da n size_G.
intros config Hinvalid [Hmaj [ptx [pty [ptz Hsec]]]].
destruct (support (max (!! (round gatherR2 da config)))) as [| pt1 [| pt2 l]] eqn:Hmax'.
-- rewrite support_nil, max_is_empty in Hmax'. elim (obs_non_nil _ Hmax').
+- rewrite support_nil, max_is_empty in Hmax'. contradiction (obs_non_nil _ Hmax').
- now left.
- right.
get_case (round gatherR2 da config). rename Hmaj0 into Hmaj'.
@@ -2978,7 +2978,7 @@ assert (Hex : forall id id',
{ intros id id' Hid Hid' Hneq Hactive. simpl in *.
destruct (da.(activate) id') eqn:Hactive'; trivial; exfalso.
decompose [or] Hid; decompose [or] Hid'; try subst id; try subst id';
- (now elim Hneq) || rewrite Hactive in *; changeR2; rewrite Hactive' in *;
+ (now contradiction Hneq) || rewrite Hactive in *; changeR2; rewrite Hactive' in *;
rewrite ?Hid1, ?Hid2, ?Hid3, ?Hid4 in *; R2dec. }
(* Therefore, at least three were not activated and not on the target *)
assert (Hperm_id : exists id1' id2' id3' id4',
@@ -3108,7 +3108,7 @@ Proof using Hssync.
unfold measure at 2.
destruct (support (max (!! config))) as [| pt [| pt' smax]] eqn:Hmax.
- (* No robots *)
- rewrite support_nil, max_is_empty in Hmax. elim (obs_non_nil _ Hmax).
+ rewrite support_nil, max_is_empty in Hmax. contradiction (obs_non_nil _ Hmax).
- (* A majority tower *)
get_case config.
apply MajTower_at_forever in Hcase.
@@ -3127,7 +3127,7 @@ Proof using Hssync.
simpl.
get_case config.
rewrite (round_simplify_Majority Hcase0 gmove).
- destruct (da.(activate) gmove); try reflexivity; []. now elim Hactive.
+ destruct (da.(activate) gmove); try reflexivity; []. contradiction diff_false_true.
- (* Computing the SEC *)
get_case config. clear Hmax pt pt' smax.
destruct (is_clean (!! config)) eqn:Hclean.
@@ -3219,7 +3219,7 @@ Proof using Hssync.
unfold measure.
destruct (support (max (!! (round gatherR2 da config)))) as [| ? [| ? ?]] eqn:Hmax'.
* (* Absurd: no robot after one round *)
- rewrite support_nil, max_is_empty in Hmax'. elim (obs_non_nil _ Hmax').
+ rewrite support_nil, max_is_empty in Hmax'. contradiction (obs_non_nil _ Hmax').
* (* A majority tower after one round *)
destruct (on_SEC (support (!! config))) as [| ? [| ? [| ? [| ? ?]]]];
cbn in Hle; lia || left; lia.
@@ -3239,7 +3239,7 @@ End SSYNC_Results.
(* destination is independent from the demonic_action. This replace
the same_destination inside previous section. *)
Corollary same_destination_strong : forall da da' (config : configuration) id1 id2,
- SSYNC_da da -> SSYNC_da da' ->
+ SSYNC_da da -> SSYNC_da da' ->
List.In id1 (moving gatherR2 da config) ->
List.In id2 (moving gatherR2 da' config) ->
round gatherR2 da config id1 == round gatherR2 da' config id2.
@@ -3253,10 +3253,10 @@ Proof using Type.
rewrite (round_simplify da hss _ id1) in Hmove1 |- *.
rewrite (round_simplify da' hss' _ id2) in Hmove2 |- *.
destruct (da.(activate) id1), (da'.(activate) id2);
- try (now elim Hmove1 + elim Hmove2); [].
+ try (now contradiction Hmove1 + contradiction Hmove2); [].
cbn zeta in *.
destruct (support (max (!! config))) as [| ? [| ? ?]] eqn:Hsupp.
- - now elim Hmove1.
+ - now contradiction Hmove1.
- reflexivity.
- simpl in Hlt. lia.
Qed.
@@ -3281,7 +3281,7 @@ Lemma not_gathered_exists : forall config pt,
Proof using .
intros config pt Hgather.
destruct (forallb (fun x => if get_location (config x) =?= pt then true else false) names) eqn:Hall.
-- elim Hgather. rewrite forallb_forall in Hall.
+- contradiction Hgather. rewrite forallb_forall in Hall.
intro id'. setoid_rewrite R2dec_bool_true_iff in Hall. repeat rewrite Hall; reflexivity || apply In_names.
- rewrite <- negb_true_iff, existsb_forallb, existsb_exists in Hall.
destruct Hall as [id' [_ Hid']]. revert Hid'. destruct_match; discriminate || now exists id'.
@@ -3293,7 +3293,7 @@ Theorem OneMustMove : forall config id, ~ WithMultiplicity.invalid config -> ~ga
Proof using .
intros config id Hvalid Hgather.
destruct (support (max (!! config))) as [| pt [| pt' lmax]] eqn:Hmax.
-* elim (support_max_non_nil _ Hmax).
+* contradiction (support_max_non_nil _ Hmax).
* rewrite <- MajTower_at_equiv in Hmax.
apply not_gathered_generalize with _ _ pt in Hgather.
apply not_gathered_exists in Hgather. destruct Hgather as [gmove Hmove].
@@ -3301,7 +3301,7 @@ destruct (support (max (!! config))) as [| pt [| pt' lmax]] eqn:Hmax.
rewrite (round_simplify_Majority _ Hda Hmax gmove).
destruct_match.
+ intro Habs. apply Hmove. now rewrite <- Habs.
- + now elim Hactive.
+ + contradiction diff_false_true.
* (* No majority tower *)
get_case config.
destruct (is_clean (!! config)) eqn:Hclean.
@@ -3320,7 +3320,7 @@ destruct (support (max (!! config))) as [| pt [| pt' lmax]] eqn:Hmax.
destruct Hin as [gmove Hmove].
exists gmove. intros da Hda Hactive. rewrite active_spec in Hactive. rewrite moving_spec.
rewrite (round_simplify_dirty da Hda Hmaj Hclean gmove).
- destruct (da.(activate) gmove); try (now elim Hactive); [].
+ destruct (da.(activate) gmove); [|contradiction diff_false_true].
destruct (mem equiv_dec (get_location (config gmove)) (SECT (!! config))) eqn:Htest.
- rewrite mem_true_iff, Hmove in Htest.
contradiction.
@@ -3371,7 +3371,7 @@ intros da config pt Hssync Hgather. rewrite (round_simplify_Majority).
induction names as [| id l].
+ reflexivity.
+ cbn -[equiv_dec]. destruct_match.
- - elim Hdiff. hnf in *. subst pt'. pattern id. apply no_byz. intro g. apply Hgather.
+ - contradiction Hdiff. hnf in *. subst pt'. pattern id. apply no_byz. intro g. apply Hgather.
- apply IHl. }
rewrite H0. specialize (Hgather g1). rewrite <- Hgather. apply pos_in_config.
Qed.
diff --git a/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v b/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v
index 1d8c189bbec500f6ae8ccf3c9dd0bcb1ac3c594e..285174c16c6038ea4c734291618ff70c32c2640c 100644
--- a/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v
+++ b/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v
@@ -218,7 +218,7 @@ Lemma measure_nonneg : forall config, 0 <= measure config.
Proof using .
intros config. unfold measure.
destruct (elements (!! config)) as [| pt l] eqn:Heq.
-+ elim (elements_non_nil _ Heq).
++ contradiction (elements_non_nil _ Heq).
+ rewrite <- (R2_dist_defined_2 pt). apply max_dist_obs_le; rewrite Heq; now left.
Qed.
@@ -264,7 +264,7 @@ intros config. split; intro H.
cut (length (pt' :: l) = length (x :: nil)); try (simpl; lia).
f_equiv; eauto. }
subst. rewrite PermutationA_1 in Hperm; autoclass; [].
- elim H2. left.
+ contradiction H2. left.
cbn in H. do 2 rewrite R2_dist_defined_2 in H.
cbn in H. setoid_rewrite (Rmax_comm 0)%R in H. rewrite (Rmax_left 0 0)%R in H; try reflexivity; [].
rewrite dist_sym in H. repeat (rewrite (Rmax_left (dist pt' pt) 0) in H; try apply dist_nonneg).
@@ -663,7 +663,7 @@ Lemma not_gathered_exists : forall config pt,
Proof.
intros config pt Hgather.
destruct (forallb (fun x => R2dec_bool (config x) pt) names) eqn:Hall.
-- elim Hgather. rewrite forallb_forall in Hall.
+- contradiction Hgather. rewrite forallb_forall in Hall.
intro id'. setoid_rewrite R2dec_bool_true_iff in Hall.
hnf. repeat rewrite Hall; trivial; apply In_names.
- rewrite <- negb_true_iff, existsb_forallb, existsb_exists in Hall.
diff --git a/CaseStudies/Gathering/InR2/Peleg.v b/CaseStudies/Gathering/InR2/Peleg.v
index ded4db6aaf253366c81aba55ede5dde35e833600..c9853b2d24929d47744096663223009aa05d5553 100644
--- a/CaseStudies/Gathering/InR2/Peleg.v
+++ b/CaseStudies/Gathering/InR2/Peleg.v
@@ -214,7 +214,7 @@ Lemma measure_nonneg : forall config, 0 <= measure config.
Proof using size_G.
intros config. unfold measure.
destruct (support (!! config)) as [| pt l] eqn:Heq.
-+ rewrite support_nil in Heq. elim (obs_non_nil _ Heq).
++ rewrite support_nil in Heq. contradiction (obs_non_nil _ Heq).
+ rewrite <- (R2_dist_defined_2 pt). apply max_dist_obs_le; rewrite Heq; now left.
Qed.
@@ -258,7 +258,7 @@ intros config. split; intro H.
cut (length (pt' :: l) = length (x :: nil)); try (simpl; lia).
f_equiv; eauto. }
subst. rewrite PermutationA_1 in Hperm; autoclass; [].
- elim H2. left.
+ contradiction H2. left.
cbn in H. do 2 rewrite R2_dist_defined_2 in H.
rewrite (Rmax_left 0 0) in H; try reflexivity; [].
rewrite dist_sym in H. rewrite (Rmax_comm 0) in H.
@@ -707,7 +707,7 @@ Lemma not_gathered_exists : forall config pt,
Proof.
intros config pt Hgather.
destruct (forallb (fun x => R2dec_bool (config x) pt) names) eqn:Hall.
-- elim Hgather. rewrite forallb_forall in Hall.
+- contradiction Hgather. rewrite forallb_forall in Hall.
intro id'. setoid_rewrite R2dec_bool_true_iff in Hall.
hnf. repeat rewrite Hall; trivial; apply In_names.
- rewrite <- negb_true_iff, existsb_forallb, existsb_exists in Hall.
diff --git a/CaseStudies/Gathering/InR2/Viglietta.v b/CaseStudies/Gathering/InR2/Viglietta.v
index 2edb11fc430b66e2adf389a01a77ec66a5776325..45b0f3bfb005bd0b49255094980872991fab465b 100644
--- a/CaseStudies/Gathering/InR2/Viglietta.v
+++ b/CaseStudies/Gathering/InR2/Viglietta.v
@@ -275,7 +275,7 @@ destruct (gathered_at_dec config (get_location (config (Good r0)))) as [| Hgathe
* right. rewrite round_simplify; trivial; [].
assert (Hone_active : activate da (Good r0) = true \/ activate da (Good r1) = true).
{ destruct (activate da (Good r0)) eqn:Hr0, (activate da (Good r1)) eqn:Hr1; auto; [].
- elim Hmove. apply incl_nil. cut (active da = nil).
+ contradiction Hmove. apply incl_nil. cut (active da = nil).
- intro Hactive. rewrite <- Hactive. apply moving_active.
intros id Hid config'. reflexivity.
- unfold active, names. simpl.
@@ -457,7 +457,7 @@ destruct (gathered_at_dec config (get_location (config (Good r0)))) as [Hgather
apply (Hind (measure (round rendezvous (Stream.hd d) config))).
++ subst n. destruct (round_measure (Stream.hd d) config) as [[pt Hpt] | ?]; trivial; [|].
-- apply Hsim.
- -- elim Hgather'. now rewrite (Hpt r0).
+ -- contradiction Hgather'. now rewrite (Hpt r0).
++ apply Hfair.
++ apply Hsim.
++ reflexivity.
diff --git a/CaseStudies/Gathering/WithMultiplicity.v b/CaseStudies/Gathering/WithMultiplicity.v
index a9903825a3fc4c8b636f2e7e2d44c5de09abb485..4bf58d6f8f3e50d4ad38bd31043706d590a168d0 100644
--- a/CaseStudies/Gathering/WithMultiplicity.v
+++ b/CaseStudies/Gathering/WithMultiplicity.v
@@ -102,12 +102,12 @@ rewrite <- (@cardinal_total_sub_eq _ _ _ _ _ (add pt2 (Nat.div2 nG) (singleton p
+ rewrite size_add.
destruct (In_dec pt2 (singleton pt1 (Nat.div2 nG))) as [Hin | Hin].
- exfalso. rewrite In_singleton in Hin.
- destruct Hin. now elim Hdiff.
+ destruct Hin. now contradiction Hdiff.
- rewrite size_singleton; trivial; [].
apply Exp_prop.div2_not_R0. apply HsizeG.
- apply Exp_prop.div2_not_R0. apply HsizeG.
+ intro pt. destruct (pt =?= pt2) as [Heq2 | Heq2], (pt =?= pt1) as [Heq1 | Heq1].
- - rewrite Heq1, Heq2 in *. now elim Hdiff.
+ - rewrite Heq1, Heq2 in *. now contradiction Hdiff.
- rewrite add_spec, singleton_spec.
do 2 destruct_match; try contradiction; [].
simpl.
@@ -148,7 +148,7 @@ assert (Hcase : pt1' == pt1 /\ pt2' == pt2 \/ pt1' == pt2 /\ pt2' == pt1).
{ rewrite <- Hsupp, support_spec. unfold In. rewrite Hpt2'.
destruct nG as [| [| nG]]; simpl; lia. }
rewrite 2 InA_cons, InA_nil in Hin1, Hin2. clear -Hin1 Hin2 Hdiff.
- decompose [or] Hin1; decompose [or] Hin2; tauto || elim Hdiff; etransitivity; eauto. }
+ decompose [or] Hin1; decompose [or] Hin2; tauto || contradiction Hdiff; etransitivity; eauto. }
split.
+ intro. apply Hdiff.
decompose [and or] Hcase; repeat (etransitivity; eauto; symmetry).
@@ -158,7 +158,7 @@ split.
destruct Hcase as [[Heq1 Heq2] | [Heq1 Heq2]];
rewrite Heq1 in *; rewrite Heq2 in *;
try match goal with H : pt == _ |- _ => rewrite H in *; clear H end;
- rewrite ?Hpt1', ?Hpt2'; lia || now elim Hdiff.
+ rewrite ?Hpt1', ?Hpt2'; lia || now contradiction Hdiff.
- rewrite cardinal_add, cardinal_singleton, cardinal_obs_from_config, even_div2; auto; lia.
Qed.
@@ -171,8 +171,8 @@ destruct (invalid_strengthen HnB Hinvalid) as [pta [ptb Hdiff Hobs]].
rewrite Hobs, add_In, In_singleton in Hin1, Hin2, Hin3.
destruct Hin1 as [[] | []], Hin2 as [[] | []], Hin3 as [[] | []];
solve [ etransitivity; eauto
- | elim Hdiff13; etransitivity; eauto
- | elim Hdiff23; etransitivity; eauto ].
+ | contradiction Hdiff13; etransitivity; eauto
+ | contradiction Hdiff23; etransitivity; eauto ].
Qed.
Arguments invalid_same_location _ config {pt1} {pt2} pt3 _ _ _ _ _.
@@ -210,7 +210,7 @@ destruct (n1 =?= n2) as [Hn | Hn].
eapply proj1. rewrite <- elements_spec.
rewrite Helem. now right; left.
* right.
- intro Hvalid. elim Hn.
+ intro Hvalid. contradiction Hn.
assert (Hhalf : 0 < Nat.div2 nG).
{ destruct Hvalid as [_ [Hle _]]. destruct nG as [| [| ?]]; simpl; lia. }
destruct (invalid_strengthen HnB Hvalid) as [pt1' [pt2' Hdiff Hobs]].
@@ -221,7 +221,7 @@ destruct (n1 =?= n2) as [Hn | Hn].
constructor.
+ split; simpl; reflexivity || lia.
+ destruct_match.
- - elim Hdiff. hnf in * |-; simpl in *. auto.
+ - contradiction Hdiff. hnf in * |-; simpl in *. auto.
- reflexivity. }
rewrite PermutationA_2 in Hperm; autoclass; [].
clear -Hperm. destruct Hperm as [[[] []] | [[] []]]; compute in *; congruence.
diff --git a/CaseStudies/LifeLine/Algorithm.v b/CaseStudies/LifeLine/Algorithm.v
index 0a17fa16938db6e600011bb52b5c10bf5e18ceec..eeb4bce139872c6d043cf440ebeaf1f0501cad72 100644
--- a/CaseStudies/LifeLine/Algorithm.v
+++ b/CaseStudies/LifeLine/Algorithm.v
@@ -36,7 +36,7 @@ Variable n: nat.
(** All robots are non byzantine, except the scout
(considered as a Byzantine as it does not follow the protocol) *)
Instance Identifiers : Names := Robots n 1.
-Definition scout_B : B := fin0.
+Definition scout_B : B := Fin Nat.lt_0_1.
Definition scout : ident := Byz scout_B.
(** The only Byzantine robot is the scout. *)
@@ -382,7 +382,7 @@ Proof using .
intros obs pt. rewrite <- not_false_iff_true, move_to_false. split; intro Hspec.
+ intros tgt Hin. destruct (Rlt_le_dec (2*D) (dist (tgt_loc tgt) pt)) as [Hlt | Hle].
- assumption.
- - elim Hspec. now exists tgt.
+ - contradiction Hspec. now exists tgt.
+ intros [tgt [Hin Habs]]. apply Hspec in Hin.
apply (Rlt_irrefl (2*D)). eapply Rlt_le_trans; eauto.
Qed.
@@ -432,8 +432,8 @@ intros obs pt. rewrite <- not_true_iff_false, should_die_true. split; intro Hspe
+ split; try (now exists elt; apply choose_1); [].
intros tgt Hin. destruct (Rlt_le_dec D (dist (tgt_loc tgt) pt)) as [Hlt | Hle].
- assumption.
- - elim Hspec. right. now exists tgt.
- + elim Hspec. left. intro x. apply choose_2 in Hchoose. specialize (Hchoose x).
+ - contradiction Hspec. right. now exists tgt.
+ + contradiction Hspec. left. intro x. apply choose_2 in Hchoose. specialize (Hchoose x).
split; intro Habs.
- contradiction.
- now apply empty_spec in Habs.
@@ -538,7 +538,7 @@ split.
- unfold obs in Hin. rewrite obs_from_config_spec in Hin.
destruct Hin as [r [Heq [Halive' [Hdist Hid]]]].
exists r. now repeat split.
- - elim Halive. intro x. rewrite empty_spec. split; tauto || apply Hempty.
+ - contradiction Halive. intro x. rewrite empty_spec. split; tauto || apply Hempty.
Qed.
Lemma connected_path_iso_compat :
@@ -646,7 +646,7 @@ Lemma update_simplify : forall da, da_assumption da ->
Proof using .
intros da Hda config Hpath g Hg new_frame local_config local_state obs.
destruct (Rle_dec (dist (choose_new_pos obs (tgt_loc (choose_target obs))) 0) D); eauto; [].
-revert_one not. intro Habs. elim Habs.
+revert_one not. intro Habs. contradiction Habs.
assert (Hobs : obs =/= {}%set).
{ rewrite connected_path_iff_obs_non_empty in Hpath. apply Hpath in Hg. unfold complement in *.
cbn -[equiv] in Hg.
@@ -1006,10 +1006,10 @@ intros [g | b] Halive Hmoving.
* unfold config' in *. simplify_round.
destruct (rbg obs).
+ cbn in Halive. discriminate.
- + cbn -[equiv] in Hmoving. elim Hmoving. apply retraction_section.
+ + cbn -[equiv] in Hmoving. contradiction Hmoving. apply retraction_section.
+ cbn -[equiv] in Hmoving |- *. destruct_match.
- reflexivity.
- - elim Hmoving. cbn. now rewrite simpl_inverse_l.
+ - contradiction Hmoving. cbn. now rewrite simpl_inverse_l.
* rewrite (byz_is_scout b). apply scout_invariant in scout_has_inv.
destruct scout_has_inv as [pt Hpt]. now rewrite Hpt.
Qed.
diff --git a/Core/Configuration.v b/Core/Configuration.v
index 7a83e1a5011be3eec8ec021aa643f4b171e6f516..c58ab2d0ffa3236a9911829d3ae631927f1a0f22 100644
--- a/Core/Configuration.v
+++ b/Core/Configuration.v
@@ -131,7 +131,7 @@ intros configâ‚ configâ‚‚. split; intro Hneq.
- inversion Hin.
- inversion_clear Habs. inversion_clear Hin; solve [now subst | now apply IHl]. }
induction names as [| id l].
- - now elim Hlist.
+ - now contradiction Hlist.
- cbn in Hlist. destruct (equiv_dec (configâ‚ id) (configâ‚‚ id)) as [Hid | Hid].
-- apply IHl. intro Heq. apply Hlist. now constructor.
-- eauto.
@@ -233,5 +233,3 @@ Lemma map_config_merge `{Location} {T U V : Type} `{@State _ T} `{@State _ U} `{
forall (f : T -> U) (g : U -> V), Proper (equiv ==> equiv) g ->
forall config : configuration, map_config g (map_config f config) == map_config (fun x => g (f x)) config.
Proof using . now repeat intro. Qed.
-
-
diff --git a/Core/Formalism.v b/Core/Formalism.v
index 1575dcb9855dfeea76c51c0170583f3adbe308f8..cf10b45596bf3b7acc8d01ee9fce7b10ef2db211 100644
--- a/Core/Formalism.v
+++ b/Core/Formalism.v
@@ -311,10 +311,10 @@ induction names as [| id l]; simpl.
* destruct (round r1 da1 c1 id =?= c1 id) as [Heq1 | Heq1],
(round r2 da2 c2 id =?= c2 id) as [Heq2 | Heq2].
+ apply IHl.
- + elim Heq2. transitivity (round r1 da1 c1 id).
+ + contradiction Heq2. transitivity (round r1 da1 c1 id).
- symmetry. now apply round_compat.
- rewrite Heq1. apply Hc.
- + elim Heq1. transitivity (round r2 da2 c2 id).
+ + contradiction Heq1. transitivity (round r2 da2 c2 id).
- now apply round_compat.
- rewrite Heq2. symmetry. apply Hc.
+ f_equal. apply IHl.
diff --git a/Models/GraphEquivalence.v b/Models/GraphEquivalence.v
index ed7bed142770ae8be14f9ff107f0741d9c12d553..36e5d6e21841716e83379cd502423707bd4bfe39 100644
--- a/Models/GraphEquivalence.v
+++ b/Models/GraphEquivalence.v
@@ -43,17 +43,17 @@ Ltac Rdec := repeat
match goal with
| |- context[Rdec ?x ?x] =>
let Heq := fresh "Heq" in destruct (Rdec x x) as [Heq | Heq];
- [clear Heq | exfalso; elim Heq; reflexivity]
+ [clear Heq | exfalso; contradiction Heq; reflexivity]
| |- context[Rdec 1 0] =>
let Heq := fresh "Heq" in destruct (Rdec 1 0) as [Heq | Heq];
- [now elim R1_neq_R0 | clear Heq]
+ [now contradiction R1_neq_R0 | clear Heq]
| |- context[Rdec 0 1] =>
let Heq := fresh "Heq" in destruct (Rdec 0 1) as [Heq | Heq];
- [now symmetry in Heq; elim R1_neq_R0 | clear Heq]
+ [now symmetry in Heq; contradiction R1_neq_R0 | clear Heq]
| H : context[Rdec ?x ?x] |- _ =>
let Heq := fresh "Heq" in destruct (Rdec x x) as [Heq | Heq];
- [clear Heq | exfalso; elim Heq; reflexivity]
- | H : ?x <> ?x |- _ => elim H; reflexivity
+ [clear Heq | exfalso; contradiction Heq; reflexivity]
+ | H : ?x <> ?x |- _ => contradiction H; reflexivity
end.
Existing Instance InfoV.
@@ -219,7 +219,7 @@ intros ? ? Hconfig ? ? ? ? ? Hframe ? ? Htarget ? ? Hchoice.
simpl in Hchoice. subst. cbn zeta.
repeat destruct_match;
solve [ simpl; repeat split; apply Htarget
- | match goal with | H : complement _ _ _ |- _ => elim H end;
+ | match goal with | H : complement _ _ _ |- _ => contradiction H end;
simpl in Htarget; now (rewrite <- Hconfig, <- (proj1 (proj1 Htarget)))
|| (rewrite Hconfig, (proj1 (proj1 Htarget)))
| apply Hconfig ].
@@ -264,9 +264,9 @@ intros [v1 e1 proof1 | e1 p1] [v2 e2 proof2 | e2 p2] Heq Ï1 Ï2 HÏ; simpl in H
+ unfold move. destruct Heq as [Hv [[Hsrc Htgt] Hthd]].
do 2 destruct_match.
- now f_equiv.
- - match goal with H : complement _ _ _ |- _ => elim H end.
+ - match goal with H : complement _ _ _ |- _ => contradiction H end.
now rewrite <- Hv, <- Hsrc.
- - match goal with H : complement _ _ _ |- _ => elim H end.
+ - match goal with H : complement _ _ _ |- _ => contradiction H end.
now rewrite Hv, Hsrc.
- simpl. tauto.
+ unfold move. f_equiv; auto; []. now destruct p1, p2.
@@ -296,9 +296,9 @@ try destruct (v1 =?= src target1) as [Hsrc1 | Hsrc1],
(v2 =?= src target2) as [Hsrc2 | Hsrc2].
+ f_equiv; trivial; []. simpl.
rewrite Hsrc1, Hsrc2. repeat split; auto; apply Htarget.
-+ match goal with H : complement _ _ _ |- _ => elim H end.
++ match goal with H : complement _ _ _ |- _ => contradiction H end.
now rewrite <- Hsrc, <- (proj1 Hconfig).
-+ match goal with H : complement _ _ _ |- _ => elim H end.
++ match goal with H : complement _ _ _ |- _ => contradiction H end.
now rewrite Hsrc, (proj1 Hconfig).
+ assumption.
+ tauto.
@@ -412,13 +412,13 @@ simpl activate. destruct_match.
- (* the demon does not let the robot move *)
unfold add_edge. simpl equiv_dec.
destruct ((0 + 0)%R =?= 0%R);
- try (match goal with H : complement _ _ _ |- _ => elim H; simpl in *; lra end); [].
+ try (match goal with H : complement _ _ _ |- _ => contradiction H; simpl in *; lra end); [].
simpl. repeat split; reflexivity.
+ (* absurd case: the robot does not make the same choice *)
- match goal with | H : complement _ _ _ |- _ => elim H end.
+ match goal with | H : complement _ _ _ |- _ => contradiction H end.
rewrite <- Heqv, Hv'. apply Hlocal_robot_decision.
+ (* absurd case: the robot does not make the same choice *)
- match goal with | H : complement _ _ _ |- _ => elim H end.
+ match goal with | H : complement _ _ _ |- _ => contradiction H end.
rewrite Heqv, Hv. symmetry. apply Hlocal_robot_decision.
+ (* invalid case: the robot does not choose an adjacent edge *)
simpl. repeat split; apply Heqv || apply Heqe. }
@@ -479,7 +479,7 @@ simpl activate. destruct_match.
- (* the demon chooses not to let the robot move *)
unfold add_edge. simpl.
destruct ((0 + 0)%R =?= 0%R);
- try (match goal with H : complement _ _ _ |- _ => elim H; simpl in *; lra end); [].
+ try (match goal with H : complement _ _ _ |- _ => contradiction H; simpl in *; lra end); [].
repeat split; assumption || reflexivity.
+ unfold valid_stateV in *. simpl in Hvalid.
destruct Hvalid as [ | Hvalid]; try contradiction; [].
@@ -711,10 +711,10 @@ simpl activate. destruct_match_eq Hactive.
- (* the ending point is before the edge threshold *)
symmetry. repeat split; simpl; apply Hlocal_robot_decision.
* (* absurd case: the robot does not make the same choice *)
- match goal with | H : complement _ _ _ |- _ => elim H end.
+ match goal with | H : complement _ _ _ |- _ => contradiction H end.
rewrite Hlocal_g. etransitivity; eauto. symmetry. apply Hlocal_robot_decision.
* (* absurd case: the robot does not make the same choice *)
- match goal with | H : complement _ _ _ |- _ => elim H end.
+ match goal with | H : complement _ _ _ |- _ => contradiction H end.
rewrite <- Hlocal_g. etransitivity; eauto. apply Hlocal_robot_decision.
* (* invalid case: the robot does not choose an adjacent edge *)
rewrite Hlocal_config, <- Hg. reflexivity. }
@@ -834,7 +834,7 @@ simpl activate. destruct_match_eq Hactive.
destruct (Rle_bool (threshold e) (p + choose_inactive da config id)) eqn:Hcase;
rewrite Rle_bool_true_iff in Hcase || rewrite Rle_bool_false_iff in Hcase;
repeat destruct_match; try solve [split; reflexivity | simpl in *; contradiction]; [].
- elim Hcase. transitivity 1; trivial; []. apply Rlt_le. apply threshold_pos.
+ contradiction Hcase. transitivity 1; trivial; []. apply Rlt_le. apply threshold_pos.
Qed.
End GraphEquivalence.
diff --git a/Models/NoByzantine.v b/Models/NoByzantine.v
index a40ce25cfe945cf2ef9a87edba81f89e90fe7000..5e99c0b73ca084ce49970cac62683a55bc49cd08 100644
--- a/Models/NoByzantine.v
+++ b/Models/NoByzantine.v
@@ -22,8 +22,8 @@ Qed.
Lemma no_byz : ∀ (id : ident) (P : ident -> Type), (∀ g, P (Good g)) -> P id.
Proof using NoByz.
- intros [g | b] P HP. { apply HP. }
- elim (@List.in_nil _ b). rewrite <- Bnames_nil. apply In_Bnames.
+ intros [g | b] P HP. { apply HP. } exfalso. apply (@List.in_nil _ b).
+ rewrite <- Bnames_nil. apply In_Bnames.
Qed.
Lemma no_byz_inv : ∀ (P : ident -> Type),
@@ -38,7 +38,7 @@ Qed.
Lemma no_byz_fun {T : Type} : B -> T.
Proof using NoByz.
- intros b. exfalso. elim (@List.in_nil B b). rewrite <- Bnames_nil.
+ intros b. exfalso. apply (@List.in_nil B b). rewrite <- Bnames_nil.
apply In_Bnames.
Qed.
@@ -46,8 +46,8 @@ Lemma no_byz_ex : ∀ (P : ident → Prop),
(∃ id : ident, P id) <-> (∃ g : G, P (Good g)).
Proof using NoByz.
intros. split.
- - intros [[g | b] H]. { exists g. apply H. } exfalso. elim (@List.in_nil B b).
- rewrite <- Bnames_nil. apply In_Bnames.
+ - intros [[g | b] H]. { exists g. apply H. } exfalso.
+ apply (@List.in_nil B b). rewrite <- Bnames_nil. apply In_Bnames.
- intros [g H]. exists (Good g). apply H.
Qed.
diff --git a/Observations/MultisetObservation.v b/Observations/MultisetObservation.v
index 3dee8784bccd2b0e24dcd8d660900d41862250cb..7eb2692b8cc187b7dfb1e9da96d30042fdde2bcf 100644
--- a/Observations/MultisetObservation.v
+++ b/Observations/MultisetObservation.v
@@ -93,7 +93,7 @@ intros x n. induction n.
+ simpl alls. rewrite make_multiset_cons. rewrite IHn. intro y. rewrite singleton_spec.
destruct (equiv_dec y x) as [Heq | Heq].
- rewrite Heq, add_spec, singleton_spec.
- destruct (equiv_dec x x) as [_ | Helim]. lia. now elim Helim.
+ destruct (equiv_dec x x) as [_ | Helim]. lia. now contradiction Helim.
- rewrite add_other; auto. rewrite singleton_spec.
destruct (equiv_dec y x); trivial; []. contradiction.
Qed.
diff --git a/Observations/SetObservation.v b/Observations/SetObservation.v
index 3fd983c4c7e68dbb5f221ca9b13f239211eb94c2..dc3bcf01b91d31adde53e30415861f1ccce0290f 100644
--- a/Observations/SetObservation.v
+++ b/Observations/SetObservation.v
@@ -101,7 +101,7 @@ intros x l. induction l as [| e l].
* destruct IHl as [l' [n [Hin Hperm]]]. destruct (e =?= x) as [Heq | Heq].
+ exists l', (S n). split; trivial. simpl. apply PermutationA_cons; assumption.
+ exists (e :: l'), n. split.
- - intro Habs. inversion_clear Habs. elim Heq. now symmetry. contradiction.
+ - intro Habs. inversion_clear Habs. apply Heq. now symmetry. contradiction.
- rewrite Hperm. apply (PermutationA_middle _).
Qed.
diff --git a/Spaces/R.v b/Spaces/R.v
index f1e51f79c1e98b217b457c75b08a720f4190a40a..b00489a820959371c598530f49a3d5ff6efa0a14 100644
--- a/Spaces/R.v
+++ b/Spaces/R.v
@@ -77,29 +77,29 @@ Ltac Rdec := repeat
match goal with
| |- context[@equiv_dec _ _ R_EqDec ?x ?x] =>
let Heq := fresh "Heq" in destruct (@equiv_dec _ _ R_EqDec x x) as [Heq | Heq];
- [clear Heq | exfalso; elim Heq; reflexivity]
+ [clear Heq | exfalso; contradiction Heq; reflexivity]
| |- context[@equiv_dec _ _ R_EqDec 1 0] =>
let Heq := fresh "Heq" in destruct (@equiv_dec _ _ R_EqDec 1 0) as [Heq | Heq];
- [now elim R1_neq_R0 | clear Heq]
+ [now contradiction R1_neq_R0 | clear Heq]
| |- context[@equiv_dec _ _ R_EqDec 0 1] =>
let Heq := fresh "Heq" in destruct (@equiv_dec _ _ R_EqDec 0 1) as [Heq | Heq];
- [now symmetry in Heq; elim R1_neq_R0 | clear Heq]
+ [now symmetry in Heq; contradiction R1_neq_R0 | clear Heq]
| H : context[@equiv_dec _ _ R_EqDec ?x ?x] |- _ =>
let Heq := fresh "Heq" in destruct (@equiv_dec _ _ R_EqDec x x) as [Heq | Heq];
- [clear Heq | exfalso; elim Heq; reflexivity]
+ [clear Heq | exfalso; contradiction Heq; reflexivity]
| |- context[Rdec ?x ?x] =>
let Heq := fresh "Heq" in destruct (Rdec x x) as [Heq | Heq];
- [clear Heq | exfalso; elim Heq; reflexivity]
+ [clear Heq | exfalso; contradiction Heq; reflexivity]
| |- context[Rdec 1 0] =>
let Heq := fresh "Heq" in destruct (Rdec 1 0) as [Heq | Heq];
- [now elim R1_neq_R0 | clear Heq]
+ [now contradiction R1_neq_R0 | clear Heq]
| |- context[Rdec 0 1] =>
let Heq := fresh "Heq" in destruct (Rdec 0 1) as [Heq | Heq];
- [now symmetry in Heq; elim R1_neq_R0 | clear Heq]
+ [now symmetry in Heq; contradiction R1_neq_R0 | clear Heq]
| H : context[Rdec ?x ?x] |- _ =>
let Heq := fresh "Heq" in destruct (Rdec x x) as [Heq | Heq];
- [clear Heq | exfalso; elim Heq; reflexivity]
- | H : ?x <> ?x |- _ => elim H; reflexivity
+ [clear Heq | exfalso; contradiction Heq; reflexivity]
+ | H : ?x <> ?x |- _ => contradiction H; reflexivity
end.
Ltac Rdec_full :=
@@ -115,7 +115,7 @@ Ltac Rdec_full :=
Ltac Rabs :=
match goal with
- | Hx : ?x <> ?x |- _ => now elim Hx
+ | Hx : ?x <> ?x |- _ => now contradiction Hx
| Heq : ?x == ?y, Hneq : ?y =/= ?x |- _ => symmetry in Heq; contradiction
| Heq : ?x == ?y, Hneq : ?y <> ?x |- _ => symmetry in Heq; contradiction
| Heq : ?x = ?y, Hneq : ?y =/= ?x |- _ => symmetry in Heq; contradiction
@@ -165,14 +165,14 @@ Definition Rleb (x y : R) := if Rle_lt_dec x y then true else false.
Lemma Rleb_spec : forall x y, Rleb x y = true <-> Rle x y.
Proof.
intros x y; unfold Rleb; destruct (Rle_lt_dec x y); split; intro H; trivial.
-inversion H. elim (Rlt_not_le _ _ r H).
+inversion H. contradiction (Rlt_not_le _ _ r H).
Qed.
Corollary Rleb_total : forall x y, Rleb x y = true \/ Rleb y x = true.
Proof.
intros x y. unfold Rleb. destruct (Rle_lt_dec x y).
now left.
- right. destruct (Rle_lt_dec y x). reflexivity. elim (Rlt_irrefl x). now apply Rlt_trans with y.
+ right. destruct (Rle_lt_dec y x). reflexivity. contradiction (Rlt_irrefl x). now apply Rlt_trans with y.
Qed.
Corollary Rleb_trans : Transitive Rleb.
diff --git a/Spaces/R2.v b/Spaces/R2.v
index d423c58c5eca626861574eee2e6e8c9137f95a77..ef78fcc987a5832ceefe6445b33589a7f62f13b4 100644
--- a/Spaces/R2.v
+++ b/Spaces/R2.v
@@ -125,12 +125,12 @@ Ltac R2dec := repeat
match goal with
| |- context[@equiv_dec _ _ R2_EqDec ?x ?x] =>
let Heq := fresh "Heq" in destruct (@equiv_dec _ _ R2_EqDec x x) as [Heq | Heq];
- [clear Heq | exfalso; elim Heq; reflexivity]
+ [clear Heq | exfalso; contradiction Heq; reflexivity]
| H : context[Rdec ?x ?x] |- _ =>
let Heq := fresh "Heq" in destruct (Rdec x x) as [Heq | Heq];
- [clear Heq | exfalso; elim Heq; reflexivity]
- | H : ?x <> ?x |- _ => elim H; reflexivity
- | H : ?x =/= ?x |- _ => elim H; reflexivity
+ [clear Heq | exfalso; contradiction Heq; reflexivity]
+ | H : ?x <> ?x |- _ => contradiction H; reflexivity
+ | H : ?x =/= ?x |- _ => contradiction H; reflexivity
| Heq : ?x == ?y, Hneq : ~?y == ?x |- _ => symmetry in Heq; contradiction
| Heq : ?x == ?y, Hneq : ~?x == ?y |- _ => contradiction
| Heq : ?x == ?y |- context[@equiv_dec _ _ R2_EqDec ?x ?y] =>
@@ -182,7 +182,7 @@ Lemma R2dec_bool_false_iff (x y : R2) : R2dec_bool x y = false <-> x =/= y.
Proof using .
unfold R2dec_bool.
destruct (equiv_dec x y); split; discriminate || auto.
-intros abs. rewrite e in abs. now elim abs.
+intros abs. rewrite e in abs. now contradiction abs.
Qed.
@@ -524,7 +524,7 @@ intros t u v w Heq. null (u - t)%VS; [| null (v - t)%VS].
+ split; apply colinear_origin_l || apply colinear_origin_r.
+ split; try apply colinear_origin_r.
rewrite R2sub_origin in Hnull0. rewrite <- Hnull0 in *.
- elim Hnull.
+ contradiction Hnull.
rewrite R2sub_origin, <- dist_defined. apply Rmult_eq_reg_l with 2; try lra; [].
ring_simplify. apply Rplus_eq_reg_r with (dist v w).
rewrite Rplus_0_l. rewrite Heq at 2. setoid_rewrite dist_sym at 3. ring.
@@ -1298,7 +1298,7 @@ change ((translation t) (/ k * fold_left add l origin)%VS)
rewrite <- (mul_1 t) at 2. rewrite <- (Rinv_l k); trivial; [].
rewrite <- mul_morph, <- mul_distr_add. f_equiv. change eq with equiv.
subst k. clear Hk. induction l as [| e l].
-* now elim Hl.
+* now contradiction Hl.
* destruct l as [| e' l'].
+ destruct e, t. simpl. f_equal; ring.
+ specialize (IHl ltac:(discriminate)).
@@ -1366,7 +1366,7 @@ Proof using .
(List.map (fun xn => (Bijection.section (Similarity.sim_f sim) (fst xn), snd xn)) m) init
= fold_left (fun acc pt' => acc + snd pt' * (sim.(Similarity.zoom))² * (dist pt (fst pt'))²) m init).
{ intro pt. induction m as [| p1 m]; intro init.
- + now elim Hm.
+ + now contradiction Hm.
+ clear Hm. destruct m as [| p2 m].
* cbn -[dist]. now rewrite sim.(Similarity.dist_prop), R_sqr.Rsqr_mult, Rmult_assoc.
* remember (p2 :: m) as mm.
@@ -1464,12 +1464,12 @@ Proof using .
repeat rewrite ?Rle_bool_true_iff, ?Rle_bool_false_iff in *
; repeat progress normalize_R2dist pt1' pt2' pt3' ;try contradiction;
repeat match goal with
- | H1: ?A < ?A |- _ => elim (Rlt_irrefl _ h_ltxx)
+ | H1: ?A < ?A |- _ => contradiction (Rlt_irrefl _ h_ltxx)
| H1: ?A < ?B, H2: ?B < ?A |- _ =>
- assert (h_ltxx:A<A) by (eapply Rlt_trans;eauto);elim (Rlt_irrefl _ h_ltxx)
+ assert (h_ltxx:A<A) by (eapply Rlt_trans;eauto);contradiction (Rlt_irrefl _ h_ltxx)
| H1: ?A < ?B, H2: ?B < ?C, H3: ?C < ?A |- _ =>
assert (h_ltxx:A<C) by (eapply Rlt_trans;eauto);
- assert (h_ltxx':A<A) by (eapply Rlt_trans;eauto);elim (Rlt_irrefl _ h_ltxx')
+ assert (h_ltxx':A<A) by (eapply Rlt_trans;eauto);contradiction (Rlt_irrefl _ h_ltxx')
| H1:?A <> ?B, H2: ?A <= ?B |- _ => assert (A<B) by (apply Rle_neq_lt;auto);clear H2
| H1:?A <> ?B, H2: ?B <= ?A |- _ => assert (B<A) by (apply Rle_neq_lt;auto;apply not_eq_sym;auto);clear H2
end; reflexivity.
@@ -1507,7 +1507,7 @@ subst; trivial; try contradiction.
+ do 2 right. subst. repeat split; trivial. intro Heq. rewrite Heq in *. intuition.
+ repeat match goal with
| H : dist _ _ = _ |- _ => rewrite H in *; clear H
- | H : ?x <> ?x |- _ => now elim H
+ | H : ?x <> ?x |- _ => now contradiction H
end.
+ left. now repeat split.
Qed.
@@ -2196,7 +2196,7 @@ Proof using . intros ? ? Heq. rewrite PermutationA_Leibniz in Heq. now rewrite H
(* The last axiom is useful because of the following degeneracy fact. *)
Lemma enclosing_circle_nil : forall pt r, enclosing_circle {| center := pt; radius := r |} nil.
-Proof using . intros. unfold enclosing_circle. intros x Hin. elim Hin. Qed.
+Proof using . intros. unfold enclosing_circle. intros x Hin. contradiction Hin. Qed.
Definition center_eq c1 c2 := c1.(center) = c2.(center).
Definition radius_eq c1 c2 := c1.(radius) = c2.(radius).
@@ -2264,7 +2264,7 @@ Lemma max_dist_le : forall pt x l, In x l -> dist x pt <= max_dist pt l.
Proof using .
intros pt x l Hin.
unfold max_dist. generalize 0. induction l as [| e l]; intro acc; simpl.
-* elim Hin.
+* contradiction Hin.
* destruct Hin as [? | Hin]; subst.
+ apply Rle_trans with (Rmax acc (dist x pt)).
- apply Rmax_r.
@@ -2275,7 +2275,7 @@ Qed.
Lemma max_dist_exists : forall pt l, l <> nil -> exists x, In x l /\ dist x pt = max_dist pt l.
Proof using .
intros pt l Hl. induction l as [| e1 l].
-* now elim Hl.
+* now contradiction Hl.
* destruct l as [| e2 l].
+ exists e1. split; try now left. unfold max_dist. simpl. symmetry. apply Rmax_right.
change (0 <= dist e1 pt). apply dist_nonneg.
@@ -2429,12 +2429,12 @@ Lemma farthest_from_in_except_In : forall exc c l, (exists pt, pt <> exc /\ In p
In (farthest_from_in_except exc c c l) l.
Proof using .
intros exc c l Hl. induction l as [| e l].
-* now elim Hl.
+* destruct Hl as [? H]. apply H.
* cbn. destruct (equiv_dec e exc) as [Heq | Heq].
+ rewrite Heq in *. destruct l.
- - destruct Hl as [pt' [Habs Hin]]. elim Habs. now inversion Hin.
+ - destruct Hl as [pt' [Habs Hin]]. contradiction Habs. now inversion Hin.
- right. apply IHl. destruct Hl as [pt' [Hneq Hin]]. exists pt'. split; trivial.
- inversion Hin; subst; trivial; now elim Hneq.
+ inversion Hin; subst; trivial; now contradiction Hneq.
+ destruct (Rle_dec (dist e c) (dist c c)) as [H | H].
- assert (He : equiv e c).
{ rewrite <- dist_defined. transitivity (dist c c).
@@ -2627,7 +2627,7 @@ Qed.
Lemma on_SEC_singleton : forall pt, on_SEC (pt :: nil) = pt :: nil.
Proof using .
intro. cbn. rewrite SEC_singleton. unfold on_circle. cbn. rewrite R2_dist_defined_2.
-destruct (Rdec_bool 0 0) eqn:Htest; trivial. rewrite Rdec_bool_false_iff in Htest. now elim Htest.
+destruct (Rdec_bool 0 0) eqn:Htest; trivial. rewrite Rdec_bool_false_iff in Htest. now contradiction Htest.
Qed.
Lemma on_SEC_singleton_is_singleton : forall pt l, NoDup l -> on_SEC l = pt :: nil -> l = pt :: nil.
@@ -2688,7 +2688,7 @@ destruct (equiv_dec pt1 pt2) as [Heq | Heq].
+ assert (Hperm : exists l, Permutation l' (pt2 :: l)).
{ rewrite <- InA_Leibniz in Hpt2. setoid_rewrite <- PermutationA_Leibniz.
apply PermutationA_split; autoclass.
- inversion_clear Hpt2; trivial. subst. now elim Heq. }
+ inversion_clear Hpt2; trivial. subst. now contradiction Heq. }
destruct Hperm as [l Hperm]. rewrite Hperm in *. clear Hpt2 Hperm l'.
change (/2 * dist pt1 pt2) with (radius {| center := middle pt1 pt2; radius := /2 * dist pt1 pt2 |}).
rewrite <- SEC_dueton. apply SEC_incl_compat. intro. cbn. intuition.
@@ -2755,7 +2755,7 @@ destruct Hl as [Hl | [[pt1 [Hl Hnil]] | [pt1 [pt2 [Hneq [Hpt1 Hpt2]]]]]].
{ assert (Hlen : (length l <> 0)%nat) by auto using length_0.
rewrite Hl. clear Hl Hnil.
induction (length l) as [| [| n]].
- + now elim Hlen.
+ + now contradiction Hlen.
+ simpl. apply SEC_dueton.
+ assert (Hperm : Permutation (pt :: alls pt1 (S (S n))) (pt1 :: pt :: alls pt1 (S n)))
by (simpl; constructor).
@@ -3108,8 +3108,8 @@ destruct (equiv_dec pt1 pt2) as [Heq12 | Heq12];
assert (Hpt2' := Hincl pt2' ltac:(intuition)).
simpl in Hpt1', Hpt2'. decompose [or] Hpt1'; decompose [or] Hpt2'; clear Hpt1' Hpt2'; repeat subst;
try match goal with
- | H : False |- _ => elim H
- | H : ~equiv ?x ?x |- _ => elim H; reflexivity
+ | H : False |- _ => contradiction H
+ | H : ~equiv ?x ?x |- _ => contradiction H; reflexivity
end.
- exists pt3. do 4 constructor.
- exists pt2. do 4 constructor.
@@ -3253,7 +3253,7 @@ repeat match goal with
| H : equiv _ _ |- _ => rewrite H in *
| H : InA _ _ _ |- _ => inversion_clear H
end.
-- now elim Hdiff.
+- now contradiction Hdiff.
- rewrite R2_dist_defined_2 in *. symmetry in Heq2. rewrite dist_defined in Heq2. now symmetry in Heq2.
- rewrite R2_dist_defined_2 in *. now rewrite dist_defined in Heq1.
Qed.
diff --git a/Spaces/RealNormedSpace.v b/Spaces/RealNormedSpace.v
index c49a937ff02f5e72604248ce3e3384c86afb70cc..e078fb67ea756b55b9c4de5efb8f34cd678ce15d 100644
--- a/Spaces/RealNormedSpace.v
+++ b/Spaces/RealNormedSpace.v
@@ -379,7 +379,7 @@ Section BarycenterResults.
Proof using .
intros E dm Hnotempty Hdm p Hp.
assert (Hlength_pos: 0 < INR (List.length E)).
- { apply lt_0_INR. destruct E; try (now elim Hnotempty); []. simpl. lia. }
+ { apply lt_0_INR. destruct E; try (now contradiction Hnotempty); []. simpl. lia. }
rewrite norm_dist. subst. unfold isobarycenter.
setoid_replace p%VS with (- / INR (length E) * (- INR (length E) * p))%VS
by (rewrite mul_morph, Ropp_inv_permute, <- Rinv_l_sym, mul_1; lra || reflexivity).
@@ -388,7 +388,7 @@ Section BarycenterResults.
apply Rmult_le_reg_l with (r := INR (length E)); trivial; [].
rewrite <- Rmult_assoc, Rinv_r, Rmult_1_l; try lra; [].
induction E as [| a [| b E]].
- + now elim Hnotempty.
+ + now contradiction Hnotempty.
+ specialize (Hp a ltac:(now left)). cbn -[mul add norm].
setoid_replace ((-(1) * p) + (0 + a))%VS with (a - p)%VS
by now rewrite add_origin_l, add_comm, minus_morph, mul_1.
diff --git a/Spaces/RealVectorSpace.v b/Spaces/RealVectorSpace.v
index 565bf57b4d2abf11b29b470f49413cd36eb0303f..b65e359ead76f3e94d19553e6872d6554a12928f 100644
--- a/Spaces/RealVectorSpace.v
+++ b/Spaces/RealVectorSpace.v
@@ -146,7 +146,7 @@ Proof using .
intros k k' u Hu Heq. destruct (Rdec k k') as [| Hneq]; trivial.
assert (Heq0 : (k - k') * u == 0).
{ unfold Rminus. rewrite <- add_morph, minus_morph, Heq. apply add_opp. }
-elim Hu. rewrite <- (mul_1 u). rewrite <- (Rinv_l (k - k')).
+contradiction Hu. rewrite <- (mul_1 u). rewrite <- (Rinv_l (k - k')).
- rewrite <- mul_morph. rewrite Heq0. apply mul_origin.
- intro Habs. apply Hneq. now apply Rminus_diag_uniq.
Qed.
@@ -265,7 +265,7 @@ Section Barycenter.
0 < snd (barycenter_aux E init).
Proof using .
intros E init Hinit Hnil HE.
- destruct E as [| e E]; try (now elim Hnil); [].
+ destruct E as [| e E]; try (now contradiction Hnil); [].
simpl. apply Rlt_le_trans with (snd e + snd init)%R.
+ inv HE. lra.
+ change (snd e + snd init)%R with (snd ((snd e * fst e + fst init)%VS, snd e + snd init))%R.
diff --git a/Spaces/Ring.v b/Spaces/Ring.v
index 40c0222f986ab884830228bdd22104cf2ca37f3a..228e5ad4de3c0f55d82e39fdf26fd561ff57fe50 100644
--- a/Spaces/Ring.v
+++ b/Spaces/Ring.v
@@ -16,7 +16,8 @@ From Pactole Require Import Util.Coqlib Util.Bijection Spaces.Graph
Section Ring.
-Context {gt2 : greater_than 2}.
+Context {_n : greater_than 2}.
+Notation n := (@ub 2 _n).
Definition ring_node := finite_node ub.
Inductive direction := Forward | Backward | SelfLoop.
@@ -78,7 +79,7 @@ Definition nat2Odir (m : nat) : option direction :=
match m with
| 0 => Some SelfLoop
| 1 => Some Forward
- | _ => if m =? Nat.pred ub then Some Backward else None
+ | _ => if m =? Nat.pred n then Some Backward else None
end.
Definition nat2Odir_compat : Proper (equiv ==> equiv) nat2Odir := _.
@@ -101,8 +102,8 @@ Proof using .
intros. split; intros H.
- intros d Habs. apply nat2Odir_Some in Habs. rewrite H in Habs.
inversion Habs.
- - destruct (nat2Odir m) eqn:Hd. 2: reflexivity. exfalso. elim (H d).
- apply nat2Odir_Some, Hd.
+ - destruct (nat2Odir m) eqn:Hd. 2: reflexivity. exfalso.
+ apply (H d), nat2Odir_Some, Hd.
Qed.
Lemma nat2Odir_pick : ∀ m : nat,
@@ -112,28 +113,28 @@ Proof using .
destruct m as [|m]. apply Pick, dir21.
destruct (S (S m) =? Nat.pred ub) eqn:Hd.
- apply Nat.eqb_eq in Hd. rewrite Hd. apply Pick, dir2SSn.
- - apply Nat.eqb_neq in Hd. apply Nopick. intros d H. elim Hd.
+ - apply Nat.eqb_neq in Hd. apply Nopick. intros d H. apply Hd.
destruct d. all: inversion H. subst. reflexivity.
Qed.
Definition nat2dir (m : nat) (H : ∃ d, dir2nat d = m) : direction.
Proof using .
destruct (nat2Odir_pick m) as [d Hd | Hd]. exact d.
- abstract (exfalso; destruct H as [d H]; elim (Hd d); exact H).
+ abstract (exfalso; destruct H as [d H]; apply (Hd d), H).
Defined.
Lemma dir2natK : ∀ (d1 : direction) (H : ∃ d2, dir2nat d2 = dir2nat d1),
nat2dir (dir2nat d1) H = d1.
Proof using .
intros. unfold nat2dir. destruct (nat2Odir_pick (dir2nat d1)) as [m Hd | Hd].
- eapply dir2nat_inj, Hd. exfalso. elim (Hd d1). reflexivity.
+ eapply dir2nat_inj, Hd. contradiction (Hd d1). reflexivity.
Qed.
Lemma nat2dirK :
∀ (m : nat) (H : ∃ d, dir2nat d = m), dir2nat (nat2dir m H) = m.
Proof using .
intros. unfold nat2dir. destruct (nat2Odir_pick m) as [g Hd | Hd].
- exact Hd. exfalso. destruct H as [d H]. elim (Hd d). exact H.
+ exact Hd. exfalso. destruct H as [d H]. apply (Hd d). exact H.
Qed.
(** From a node, if we move in one direction, get get to another node. *)
@@ -289,8 +290,8 @@ Proof using .
- intros H d Heq. apply move_along_dir2nat_diff in Heq.
rewrite <- Heq, (proj2 (nat2Odir_Some _ _)) in H by reflexivity.
inversion H.
- - intros H. apply nat2Odir_None. intros d Heq. elim (H d).
- apply move_along_dir2nat_diff, Heq.
+ - intros H. apply nat2Odir_None. intros d Heq.
+ apply (H d), move_along_dir2nat_diff, Heq.
Qed.
Definition find_edge_subterm (v1 v2 : ring_node) : option ring_edge
@@ -304,10 +305,10 @@ Lemma find_edge_None_subproof :
<-> ∀ e : ring_edge, ~(fst e == v1 /\ move_along (fst e) (snd e) == v2).
Proof using .
intros. unfold find_edge_subterm. destruct (nat2Odir (diff v2 v1)) eqn:Hd.
- - split; intros H. { inversion H. } elim (H (v1, d)). clear H. split.
+ - split; intros H. { inversion H. } apply (H (v1, d)). clear H. split.
{ reflexivity. } apply move_along_dir2nat_diff, nat2Odir_Some, Hd.
- split; intros H. 2: reflexivity. clear H. intros e [H1 H2]. cbn in H1, H2.
- subst v1. unshelve eelim (proj1 (nat2Odir_diff_None (fst e) v2) _ (snd e)).
+ subst v1. unshelve eapply (proj1 (nat2Odir_diff_None (fst e) v2) _ (snd e)).
2: exact H2. rewrite <- Hd. reflexivity.
Qed.
@@ -321,14 +322,14 @@ Proof using .
all: apply move_along_dir2nat_diff in Hd. symmetry; exact Hd.
apply move_along_I in Hd. exact Hd.
- split. { intros H. inversion H. } cbn. intros [H1 H2]. subst v1.
- unshelve eelim (proj1 (nat2Odir_diff_None (fst e) v2) _ (snd e)).
+ unshelve eapply (proj1 (nat2Odir_diff_None (fst e) v2) _ (snd e)).
2: symmetry; exact H2. rewrite Hd. reflexivity.
Qed.
Definition Ring (thd : ring_edge -> R)
(thd_pos : ∀ e, (0 < thd e < 1)%R)
(thd_compat : Proper (equiv ==> eq) thd)
- : FiniteGraph ub ring_edge.
+ : FiniteGraph n ring_edge.
Proof using .
refine {|
V_EqDec := @finite_node_EqDec ub;
@@ -345,7 +346,7 @@ Proof using .
Defined.
(** If we do not care about threshold values, we just take 1/2 everywhere. *)
-Global Instance nothresholdRing : FiniteGraph ub ring_edge :=
+Global Instance nothresholdRing : FiniteGraph n ring_edge :=
Ring (fun _ => 1/2)%R
ltac:(abstract (intro; lra))
(fun _ _ _ => eq_refl).
@@ -386,7 +387,7 @@ Defined.
Definition trans_compat : Proper (equiv ==> equiv) trans := _.
Lemma trans2nat : ∀ (m : nat) (v : ring_node), fin2nat (trans m v)
- = (v + (ub - m mod ub)) mod ub.
+ = (v + (n - m mod ub)) mod ub.
Proof using . apply asbmV2nat. Qed.
Lemma transV2nat : ∀ (m : nat) (v : ring_node),
@@ -420,30 +421,30 @@ Lemma transI_fin_max : (trans 1)â»Â¹ fin_max = fin0.
Proof using . apply asbm_fin_max. Qed.
Lemma transI_fin0_divide : ∀ (v : ring_node) (m : nat),
- Nat.divide ub (v + m) ↔ (trans m)â»Â¹ v = fin0.
+ Nat.divide n (v + m) ↔ (trans m)â»Â¹ v = fin0.
Proof using . apply asbm_fin0_divide. Qed.
Lemma trans_locally_inj : ∀ (m1 m2 : nat),
- m1 ≤ m2 → m2 - m1 < ub → trans m1 == trans m2 → m1 = m2.
+ m1 ≤ m2 → m2 - m1 < n → trans m1 == trans m2 → m1 = m2.
Proof using .
intros * ?? H. eapply asbmV_locally_inj. 3: apply H. all: eassumption.
Qed.
Lemma transV_locally_inj : ∀ (m1 m2 : nat),
- m1 ≤ m2 → m2 - m1 < ub → (trans m1)â»Â¹ == (trans m2)â»Â¹ → m1 = m2.
+ m1 ≤ m2 → m2 - m1 < n → (trans m1)â»Â¹ == (trans m2)â»Â¹ → m1 = m2.
Proof using .
intros * ?? H. eapply asbm_locally_inj. 3: apply H. all: eassumption.
Qed.
Lemma trans_bounded_diff_inj : ∀ (p : nat) (m1 m2 : nat),
- bounded_diff ub p m1 → bounded_diff ub p m2
+ bounded_diff n p m1 → bounded_diff n p m2
→ trans m1 == trans m2 → m1 = m2.
Proof using .
intros * ?? H. eapply asbmV_bounded_diff_inj. 3: apply H. all: eassumption.
Qed.
Lemma transV_bounded_diff_inj : ∀ (p : nat) (m1 m2 : nat),
- bounded_diff ub p m1 → bounded_diff ub p m2
+ bounded_diff n p m1 → bounded_diff n p m2
→ (trans m1)â»Â¹ == (trans m2)â»Â¹ → m1 = m2.
Proof using .
intros * ?? H. eapply asbm_bounded_diff_inj. 3: apply H. all: eassumption.
diff --git a/Util/FMaps/FMapFacts.v b/Util/FMaps/FMapFacts.v
index 98db9062583feeb4917802253d3c0e0f9a5d8487..224216a70a4ff616abdf43551a280cc15f522485 100644
--- a/Util/FMaps/FMapFacts.v
+++ b/Util/FMaps/FMapFacts.v
@@ -2,7 +2,7 @@ Require Import Bool.
Require Import Structures.DecidableType.
Require Import SetoidDec.
Require Import Pactole.Util.FMaps.FMapInterface.
-
+Require Import Pactole.Util.SetoidDefs.
Set Implicit Arguments.
Unset Strict Implicit.
@@ -95,7 +95,7 @@ Section WeakFacts.
Proof using HF.
split; intros.
rewrite eq_option_alt. intro e. rewrite <- find_mapsto_iff.
- split; intro H'; try discriminate. elim H; exists e; auto.
+ split; intro H'; try discriminate. contradiction H; exists e; auto.
intros (e,He); rewrite find_mapsto_iff,H in He; discriminate.
Qed.
@@ -374,7 +374,7 @@ Section WeakFacts.
Hint Resolve add_neq_o : map.
Lemma add_o : forall m x y e,
- find y (add x e m) = if x == y then Some e else find y m.
+ find y (add x e m) = if x =?= y then Some e else find y m.
Proof using HF.
intros; destruct (equiv_dec x y); auto with map.
Qed.
@@ -395,7 +395,7 @@ Section WeakFacts.
mem y (add x e m) = (equiv x y) || mem y m.
Proof.
intros; do 2 rewrite mem_find_b; rewrite add_o; unfold eqb.
- destruct (equiv_dec x y); simpl; auto.
+ destruct (equiv_dec x y); cbn; auto.
Qed. *)
Lemma remove_eq_o : forall m x y,
@@ -419,7 +419,7 @@ Section WeakFacts.
Hint Resolve remove_neq_o : map.
Lemma remove_o : forall m x y,
- find y (remove x m) = if x == y then None else find y m.
+ find y (remove x m) = if x =?= y then None else find y m.
Proof using HF.
intros; destruct (equiv_dec x y); auto with map.
Qed.
@@ -455,7 +455,7 @@ Section WeakFacts.
intros.
generalize (find_mapsto_iff (map f m) x) (find_mapsto_iff m x)
(fun b => map_mapsto_iff m x b f).
- destruct (find x (map f m)); destruct (find x m); simpl; auto; intros.
+ destruct (find x (map f m)); destruct (find x m); cbn; auto; intros.
rewrite <- H; rewrite H1; exists e0; rewrite H0; auto.
destruct (H e) as [_ H2].
rewrite H1 in H2.
@@ -468,7 +468,7 @@ Section WeakFacts.
mem x (map f m) = mem x m.
Proof using HF.
intros; do 2 rewrite mem_find_b; rewrite map_o.
- destruct (find x m); simpl; auto.
+ destruct (find x m); cbn; auto.
Qed.
Lemma mapi_b : forall m x (f:key->elt->elt'),
@@ -476,7 +476,7 @@ Section WeakFacts.
Proof using HF.
intros.
generalize (mem_in_iff (mapi f m) x) (mem_in_iff m x) (mapi_in_iff m x f).
- destruct (mem x (mapi f m)); destruct (mem x m); simpl; auto; intros.
+ destruct (mem x (mapi f m)); destruct (mem x m); cbn; auto; intros.
symmetry; rewrite <- H0; rewrite <- H1; rewrite H; auto.
rewrite <- H; rewrite H1; rewrite H0; auto.
Qed.
@@ -488,7 +488,7 @@ Section WeakFacts.
intros.
generalize (find_mapsto_iff (mapi f m) x) (find_mapsto_iff m x)
(fun b => mapi_mapsto_iff m x b H).
- destruct (find x (mapi f m)); destruct (find x m); simpl; auto; intros.
+ destruct (find x (mapi f m)); destruct (find x m); cbn; auto; intros.
rewrite <- H0; rewrite H2; exists e0; rewrite H1; auto.
destruct (H0 e) as [_ H3].
rewrite H2 in H3.
@@ -526,7 +526,7 @@ Section WeakFacts.
findA (eqb x) l =
findA (fun y => if eqb_dec x y then true else false) l.
Proof.
- intros; induction l; simpl.
+ intros; induction l; cbn.
reflexivity.
unfold eqb; destruct a; destruct (equiv_dec x k);
destruct (eqb_dec x k); auto; contradiction.
@@ -555,12 +555,12 @@ Section WeakFacts.
rewrite InA_alt in He.
destruct He as ((y,e'),(Ha1,Ha2)).
compute in Ha1; destruct Ha1; subst e'.
- exists (y,e); split; simpl; auto.
+ exists (y,e); split; cbn; auto.
unfold eqb; destruct (equiv_dec x y); intuition.
rewrite <- H; rewrite H0.
destruct H1 as (H1,_).
destruct H1 as ((y,e),(Ha1,Ha2)); [intuition|].
- simpl in Ha2.
+ cbn in Ha2.
unfold eqb in *; destruct (equiv_dec x y); auto; try discriminate.
exists e; rewrite InA_alt.
exists (y,e); intuition.
@@ -793,9 +793,9 @@ Section MoreWeakFacts.
k1 == k2 -> InA eq_key_elt (k1,e1) l -> InA eq_key (k2,e2) l.
Proof using .
intros k1 k2 e1 e2 l Hk. rewrite 2 InA_alt.
- intros ((k',e') & (Hk',He') & H); simpl in *.
+ intros ((k',e') & (Hk',He') & H); cbn in *.
exists (k',e'); split; auto.
- red; red; simpl; eauto.
+ red; red; cbn; eauto.
transitivity k1; auto; symmetry; auto.
Qed.
@@ -841,9 +841,11 @@ Section MoreWeakFacts.
+ assert (forall a, ~ List.In a (elements m)).
{ red; intros a H0. apply (H (fst a) (snd a)).
rewrite elements_mapsto_iff.
- rewrite InA_alt; exists a; auto. }
+ rewrite InA_alt. exists a.
+ split; [|assumption].
+ destruct a. reflexivity. }
destruct (elements m); auto.
- elim (H0 p); simpl; auto.
+ contradiction (H0 p); cbn; auto.
+ red; intros.
rewrite elements_mapsto_iff in H0.
rewrite InA_alt in H0; destruct H0.
@@ -866,18 +868,18 @@ Section MoreWeakFacts.
NoDupA eq_key l ->
(MapsTo k e (of_list l) <-> InA eq_key_elt (k,e) l).
Proof using HF.
- induction l as [|(k',e') l IH]; simpl; intros k e Hnodup.
+ induction l as [|(k',e') l IH]; cbn-[equiv]; intros k e Hnodup.
+ rewrite empty_mapsto_iff, InA_nil; intuition.
+ inversion_clear Hnodup as [| ? ? Hnotin Hnodup'].
specialize (IH k e Hnodup'); clear Hnodup'.
rewrite add_mapsto_iff, InA_cons, <- IH.
unfold eq_key_elt in *.
split; destruct 1 as [H|H]; try (intuition; fail).
- - destruct (equiv_dec k k'); [left|right]; split; try (now (idtac + symmetry); auto); [|].
- * now destruct H.
- * elim c. now destruct H.
+ - left. destruct H. split.
+ * cbn[fst] in H. now symmetry.
+ * cbn in H0. now symmetry.
- destruct (equiv_dec k k').
- * left. elim Hnotin. apply InA_eq_key_elt_eq_key with k e; intuition.
+ * left. contradiction Hnotin. apply InA_eq_key_elt_eq_key with k e; intuition.
* right. now split; try symmetry.
Qed.
@@ -885,7 +887,7 @@ Section MoreWeakFacts.
NoDupA eq_key l ->
find k (of_list l) = findA (eqb k) l.
Proof.
- induction l as [|(k',e') l IH]; simpl; intros k Hnodup.
+ induction l as [|(k',e') l IH]; cbn; intros k Hnodup.
apply empty_o.
inversion_clear Hnodup as [| ? ? Hnotin Hnodup'].
specialize (IH k Hnodup'); clear Hnodup'.
@@ -942,11 +944,11 @@ Section MoreWeakFacts.
{ intros k e; unfold l. now rewrite <- find_mapsto_iff, InA_rev, elements_mapsto_iff. }
clearbody l. clearbody ff. clear Hstep f. revert m Hsame. induction l.
(* empty *)
- intros m Hsame; simpl.
+ intros m Hsame; cbn.
apply Hempty. intros k e.
rewrite find_mapsto_iff, Hsame; intro Habs; inversion Habs.
(* step *)
- intros m Hsame; destruct a as (k,e); simpl.
+ intros m Hsame; destruct a as (k,e); cbn.
apply Hstep' with (of_list l); auto.
- inversion_clear Hdup. contradict H. destruct H as (e',He').
apply InA_eq_key_elt_eq_key with k e'; auto. now rewrite <- of_list_1.
@@ -958,7 +960,7 @@ Section MoreWeakFacts.
* destruct (find k' m) eqn:Habs; trivial.
exfalso. rewrite Hsame in Habs.
inversion_clear Habs.
- -- elim c. now destruct H1.
+ -- contradiction c. now destruct H1.
-- rewrite <- of_list_1, find_mapsto_iff in H1; trivial.
rewrite H1 in Hin. discriminate.
- apply IHl.
@@ -983,7 +985,7 @@ Section MoreWeakFacts.
apply fold_rec; intros.
apply Pmorphism with (empty _); auto. intro k. rewrite empty_o.
case_eq (find k m0); auto; intros e'; rewrite <- find_mapsto_iff.
- intro H'; elim (H k e'); auto.
+ intro H'; contradiction (H k e'); auto.
apply Pmorphism with (add k e m'); try intro; auto.
Qed.
@@ -1026,7 +1028,12 @@ Section MoreWeakFacts.
intros; apply Rstep; auto;
rewrite elements_mapsto_iff, <- InA_rev; auto.
clearbody l; clear Rstep m.
- induction l; simpl; auto.
+ induction l. { cbn. exact Rempty. }
+ cbn. apply Rstep'.
+ { left. now destruct a. }
+ apply IHl. intros k e a' b Hin HR.
+ apply Rstep'; [|assumption].
+ right. assumption.
Qed.
(** From the induction principle on [fold], we can deduce some general
@@ -1062,7 +1069,7 @@ Section MoreWeakFacts.
intros m' Heq k'.
rewrite empty_o.
case_eq (find k' m'); auto; intros e'; rewrite <- find_mapsto_iff.
- intro; elim (Heq k' e'); auto.
+ intro; contradiction (Heq k' e'); auto.
intros k e a m' m'' _ _ Hadd Heq k'.
rewrite Hadd, 2 add_o, Heq; auto.
Qed.
@@ -1093,7 +1100,7 @@ Section MoreWeakFacts.
Proof using HF st.
intros. apply fold_rec_nodep with (P:=fun a => eqA a i).
reflexivity.
- intros. elim (H k e); auto.
+ intros. contradiction (H k e); auto.
Qed.
(** As noticed by P. Casteran, asking for the general [SetoidList.transpose]
@@ -1142,10 +1149,10 @@ Section MoreWeakFacts.
(apply NoDupA_rev; [typeclasses eauto | apply elements_3]).
apply fold_right_equivlistA_restr with (R:=complement eq_key)(eqA:=eq_key_elt);
auto with map; try typeclasses eauto.
- intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; simpl in *; apply Comp; auto.
+ intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; cbn in *; apply Comp; auto.
unfold complement, eq_key, eq_key_elt; repeat red.
intros ? ? Heq ? ? Heq'. rewrite Heq, Heq'. tauto.
- intros (k,e) (k',e'); unfold eq_key; simpl; auto with *.
+ intros (k,e) (k',e'); unfold eq_key; cbn; auto with *.
rewrite <- NoDupA_altdef; auto.
intros (k,e).
rewrite 2 InA_rev; try apply eq_key_elt_Equiv.
@@ -1159,27 +1166,23 @@ Section MoreWeakFacts.
eqA (fold f m2 i) (f k e (fold f m1 i)).
Proof using Comp HF Tra st.
assert (eq_key_elt_refl : forall p, eq_key_elt p p).
- red; auto.
+ { red. auto. }
assert (eq_key_elt_sym : forall p p', eq_key_elt p p' -> eq_key_elt p' p).
- intros (x1,x2) (y1,y2); unfold eq_key_elt; simpl; intuition.
+ { intros (x1,x2) (y1,y2); unfold eq_key_elt; cbn; intuition. }
assert (eq_key_elt_trans : forall p p' p'',
eq_key_elt p p' -> eq_key_elt p' p'' -> eq_key_elt p p'').
- intros (x1,x2) (y1,y2) (z1,z2); unfold eq_key_elt; simpl.
- intuition; subst; auto; transitivity y1; auto.
+ { intros (x1,x2) (y1,y2) (z1,z2); unfold eq_key_elt. etransitivity; eauto. }
intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right.
set (f':=fun y x0 => f (fst y) (snd y) x0) in *.
change (f k e (fold_right f' i (rev (elements m1))))
with (f' (k,e) (fold_right f' i (rev (elements m1)))).
apply fold_right_add_restr with
- (R:=complement eq_key)(eqA:=eq_key_elt)(eqB:=eqA); auto.
- typeclasses eauto.
+ (R:=complement eq_key)(eqA:=eq_key_elt)(eqB:=eqA); eauto with typeclass_instances.
intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; unfold f';
- simpl in *. apply Comp; auto.
- unfold complement, eq_key, eq_key_elt; repeat red.
- intros ? ? Habs Heq. apply Habs. now symmetry.
+ cbn in *. apply Comp; auto.
unfold complement, eq_key, eq_key_elt; repeat red.
intros ? ? Heq ? ? Heq'. rewrite Heq, Heq'. tauto.
- unfold f'; intros (k1,e1) (k2,e2); unfold eq_key; simpl; auto.
+ unfold f'; intros (k1,e1) (k2,e2); unfold eq_key; cbn; auto.
apply NoDupA_rev; auto using eq_key_elt_Equivalence;
apply NoDupA_eq_key_eq_key_elt; apply elements_3.
apply NoDupA_rev; auto using eq_key_elt_Equivalence;
@@ -1194,12 +1197,23 @@ Section MoreWeakFacts.
rewrite InA_cons; do 2 (rewrite InA_rev by apply eq_key_elt_Equivalence);
destruct a as (a,b); fold eq_key_elt;
do 2 rewrite <- elements_mapsto_iff.
- do 2 rewrite find_mapsto_iff; unfold eq_key_elt; simpl.
+ do 2 rewrite find_mapsto_iff; unfold eq_key_elt; cbn.
rewrite H0.
rewrite add_o.
- destruct (equiv_dec k a); intuition try (easy || congruence).
- elim H. exists b; apply MapsTo_1 with a; now auto with map.
- symmetry in H1. contradiction.
+ destruct (equiv_dec k a).
+ - split; intros Hs.
+ + left. split; cbn.
+ { symmetry. apply e0. }
+ symmetry. now inversion Hs.
+ + destruct Hs.
+ * destruct H1. subst. reflexivity.
+ * contradiction H. exists b. apply MapsTo_1 with a.
+ { symmetry. assumption. }
+ apply find_2. assumption.
+ - split; intros Hs.
+ + right. assumption.
+ + destruct Hs as [[? ?]|]. 2:{ assumption. }
+ contradiction c. symmetry. apply H1.
Qed.
Lemma fold_add : forall m k e i, ~In k m ->
@@ -1262,7 +1276,7 @@ Section MoreWeakFacts.
generalize (elements_mapsto_iff m).
destruct (elements m); try discriminate.
exists p; auto.
- rewrite H0; destruct p; simpl; auto.
+ rewrite H0; destruct p; cbn; auto.
Qed.
Lemma cardinal_inv_2b :
@@ -1270,7 +1284,7 @@ Section MoreWeakFacts.
Proof using HF.
intros.
generalize (@cardinal_inv_2 m); destruct @cardinal.
- elim H;auto.
+ contradiction H;auto.
eauto.
Qed.
@@ -1325,16 +1339,16 @@ Section MoreWeakFacts.
intro m. pattern m, (fold f' m (empty _)). apply fold_rec.
intros m' Hm' k e. rewrite empty_mapsto_iff. intuition.
- elim (Hm' k e); auto.
+ contradiction (Hm' k e); auto.
intros k e acc m1 m2 Hke Hn Hadd IH k' e'.
change (Equal m2 (add k e m1)) in Hadd; rewrite Hadd.
- unfold f'; simpl.
- case_eq (f k e); intros Hfke; simpl;
+ unfold f'; cbn.
+ case_eq (f k e); intros Hfke; cbn;
rewrite !add_mapsto_iff, IH; clear IH; intuition.
rewrite <- Hfke; apply Hf; auto.
destruct (equiv_dec k k') as [Hk|Hk]; [left|right]; auto.
- elim Hn; exists e'; rewrite Hk; auto.
+ contradiction Hn; exists e'; rewrite Hk; auto.
assert (f k e = f k' e') by (apply Hf; auto). congruence.
Qed.
@@ -1345,11 +1359,11 @@ Section MoreWeakFacts.
set (f':=fun k e b => if f k e then b else false).
intro m. pattern m, (fold f' m true). apply fold_rec.
- intros m' Hm'. split; auto. intros _ k e Hke. elim (Hm' k e); auto.
+ intros m' Hm'. split; auto. intros _ k e Hke. contradiction (Hm' k e); auto.
intros k e b m1 m2 _ Hn Hadd IH. clear m.
change (Equal m2 (add k e m1)) in Hadd.
- unfold f'; simpl. case_eq (f k e); intros Hfke.
+ unfold f'; cbn. case_eq (f k e); intros Hfke.
(* f k e = true *)
rewrite IH. clear IH. split; intros Hmapsto k' e' Hke'.
rewrite Hadd, add_mapsto_iff in Hke'.
@@ -1372,18 +1386,18 @@ Section MoreWeakFacts.
intro m. pattern m, (fold f' m false). apply fold_rec.
intros m' Hm'. split; try (intros; discriminate).
- intros ((k,e),(Hke,_)); simpl in *. elim (Hm' k e); auto.
+ intros ((k,e),(Hke,_)); cbn in *. contradiction (Hm' k e); auto.
intros k e b m1 m2 _ Hn Hadd IH. clear m.
change (Equal m2 (add k e m1)) in Hadd.
- unfold f'; simpl. case_eq (f k e); intros Hfke.
+ unfold f'; cbn. case_eq (f k e); intros Hfke.
(* f k e = true *)
split; [intros _|auto].
- exists (k,e); simpl; split; auto.
+ exists (k,e); cbn; split; auto.
rewrite Hadd, add_mapsto_iff; auto.
(* f k e = false *)
- rewrite IH. clear IH. split; intros ((k',e'),(Hke1,Hke2)); simpl in *.
- exists (k',e'); simpl; split; auto.
+ rewrite IH. clear IH. split; intros ((k',e'),(Hke1,Hke2)); cbn in *.
+ exists (k',e'); cbn; split; auto.
rewrite Hadd, add_mapsto_iff; right; split; auto.
intro abs; contradict Hn; exists e'; rewrite abs; auto.
rewrite Hadd, add_mapsto_iff in Hke1. destruct Hke1 as [(?,?)|(?,?)].
@@ -1414,7 +1428,7 @@ Section MoreWeakFacts.
m1 = fst (partition f m) ->
(MapsTo k e m1 <-> MapsTo k e m /\ f k e = true).
Proof using HF Hf.
- unfold partition; simpl; intros. subst m1.
+ unfold partition; cbn; intros. subst m1.
apply filter_iff; auto.
Qed.
@@ -1422,10 +1436,10 @@ Section MoreWeakFacts.
m2 = snd (partition f m) ->
(MapsTo k e m2 <-> MapsTo k e m /\ f k e = false).
Proof using HF Hf.
- unfold partition; simpl; intros. subst m2.
+ unfold partition; cbn; intros. subst m2.
rewrite filter_iff.
split; intros (H,H'); split; auto.
- destruct (f k e); simpl in *; auto.
+ destruct (f k e); cbn in *; auto.
rewrite H'; auto.
repeat red; intros. f_equal. apply Hf; auto.
Qed.
@@ -1453,13 +1467,13 @@ Section MoreWeakFacts.
destruct (In_dec m1 k) as [H|H]; [left|right]; auto.
destruct Hm as (Hm,Hm').
destruct Hk as (e,He); rewrite Hm' in He; destruct He.
- elim H; exists e; auto.
+ contradiction H; exists e; auto.
exists e; auto.
Defined.
Lemma Disjoint_sym : forall m1 m2, Disjoint m1 m2 -> Disjoint m2 m1.
Proof using .
- intros m1 m2 H k (H1,H2). elim (H k); auto.
+ intros m1 m2 H k (H1,H2). contradiction (H k); auto.
Qed.
Lemma Partition_sym : forall m m1 m2,
@@ -1475,10 +1489,10 @@ Section MoreWeakFacts.
Proof using .
intros m m1 m2 (Hdisj,Heq). split.
intro He.
- split; intros k e Hke; elim (He k e); rewrite Heq; auto.
+ split; intros k e Hke; contradiction (He k e); rewrite Heq; auto.
intros (He1,He2) k e Hke. rewrite Heq in Hke. destruct Hke.
- elim (He1 k e); auto.
- elim (He2 k e); auto.
+ contradiction (He1 k e); auto.
+ contradiction (He2 k e); auto.
Qed.
Lemma Partition_Add :
@@ -1507,13 +1521,13 @@ Section MoreWeakFacts.
destruct (equiv_dec x k) as [He|Hne]; auto.
rewrite <- He; apply find_1; auto.
(* disjoint *)
- intros k (H1,H2). elim (Hdisj k). split; auto.
+ intros k (H1,H2). contradiction (Hdisj k). split; auto.
rewrite remove_in_iff in H1; destruct H1; auto.
(* mapsto *)
intros k' e'.
rewrite Heq, 2 remove_mapsto_iff, Hor.
intuition.
- intro abs; elim (Hdisj x); split; [exists e|exists e']; auto.
+ intro abs; contradiction (Hdisj x); split; [exists e|exists e']; auto.
apply MapsTo_1 with k'; auto.
(* second case : x in m2 *)
@@ -1525,13 +1539,13 @@ Section MoreWeakFacts.
destruct (equiv_dec x k) as [He|Hne]; auto.
rewrite <- He; apply find_1; auto.
(* disjoint *)
- intros k (H1,H2). elim (Hdisj k). split; auto.
+ intros k (H1,H2). contradiction (Hdisj k). split; auto.
rewrite remove_in_iff in H2; destruct H2; auto.
(* mapsto *)
intros k' e'.
rewrite Heq, 2 remove_mapsto_iff, Hor.
intuition.
- intro abs; elim (Hdisj x); split; [exists e'|exists e]; auto.
+ intro abs; contradiction (Hdisj x); split; [exists e'|exists e]; auto.
apply MapsTo_1 with k'; auto.
Qed.
@@ -1591,7 +1605,7 @@ Section MoreWeakFacts.
replace (fold f m 0) with (fold f m1 (fold f m2 0)).
rewrite <- cardinal_fold.
intros.
- apply fold_rel with (R:=fun u v => u = v + cardinal m2); simpl; auto.
+ apply fold_rel with (R:=fun u v => u = v + cardinal m2); cbn; auto.
symmetry; apply Partition_fold with (eqA:=@Logic.eq _); try red; auto.
compute; auto.
Qed.
@@ -1613,15 +1627,15 @@ Section MoreWeakFacts.
rewrite Hm'.
intuition.
exists e; auto.
- elim (Hm k); split; auto; exists e; auto.
+ contradiction (Hm k); split; auto; exists e; auto.
rewrite (@partition_iff_2 f Hf m m2') by auto.
unfold f.
rewrite <- not_mem_in_iff.
destruct Hm as (Hm,Hm').
rewrite Hm'.
intuition.
- elim (Hm k); split; auto; exists e; auto.
- elim H1; exists e; auto.
+ contradiction (Hm k); split; auto; exists e; auto.
+ contradiction H1; exists e; auto.
Qed.
Lemma update_mapsto_iff : forall m m' k e,
@@ -1635,7 +1649,7 @@ Section MoreWeakFacts.
intros m0 Hm0 k e.
assert (~In k m0) by (intros (e0,He0); apply (Hm0 k e0); auto).
intuition.
- elim (Hm0 k e); auto.
+ contradiction (Hm0 k e); auto.
intros k e m0 m1 m2 _ Hn Hadd IH k' e'.
change (Equal m2 (add k e m1)) in Hadd.
@@ -1647,7 +1661,7 @@ Section MoreWeakFacts.
Proof.
intros m m' k e H. rewrite update_mapsto_iff in H.
destruct (In_dec m' k) as [H'|H']; [left|right]; intuition.
- elim H'; exists e; auto.
+ contradiction H'; exists e; auto.
Defined.
Lemma update_in_iff : forall m m' k,
@@ -1659,7 +1673,7 @@ Section MoreWeakFacts.
destruct (In_dec m' k) as [H|H].
destruct H as (e,H). intros _; exists e.
rewrite update_mapsto_iff; left; auto.
- destruct 1 as [H'|H']; [|elim H; auto].
+ destruct 1 as [H'|H']; [|contradiction H; auto].
destruct H' as (e,H'). exists e.
rewrite update_mapsto_iff; right; auto.
Qed.
@@ -1751,7 +1765,7 @@ Section MoreWeakFacts.
intros k k' e e' i Hneq x.
rewrite !add_o.
destruct (equiv_dec k x); destruct (equiv_dec k' x); auto.
- elim Hneq. etransitivity; eauto.
+ contradiction Hneq. etransitivity; eauto.
apply fold_init with (eqA:=Equal); auto.
intros k k' Hk e e' He m m' Hm; rewrite Hk,He,Hm; red; auto.
Qed.
@@ -1766,14 +1780,14 @@ Section MoreWeakFacts.
pattern (mem k m2); rewrite Hm2. (* UGLY, see with Matthieu *)
destruct (mem k m2'); rewrite Hii'; auto.
apply fold_Equal with (eqA:=Equal); auto.
- intros k k' Hk e e' He m m' Hm; simpl in *.
+ intros k k' Hk e e' He m m' Hm; cbn in *.
pattern (mem k m2'); rewrite Hk. (* idem *)
destruct (mem k' m2'); rewrite ?Hk,?He,Hm; red; auto.
intros k k' e e' i Hneq x.
case_eq (mem k m2'); case_eq (mem k' m2'); intros; auto.
rewrite !add_o.
destruct (equiv_dec k x); destruct (equiv_dec k' x); auto.
- elim Hneq. etransitivity; eauto.
+ contradiction Hneq. etransitivity; eauto.
Qed.
Global Instance diff_m elt :
@@ -1784,16 +1798,16 @@ Section MoreWeakFacts.
apply fold_rel with (R:=Equal); try red; auto.
intros k e i i' H Hii' x.
pattern (mem k m2); rewrite Hm2. (* idem *)
- destruct (mem k m2'); simpl; rewrite Hii'; auto.
+ destruct (mem k m2'); cbn; rewrite Hii'; auto.
apply fold_Equal with (eqA:=Equal); auto.
- intros k k' Hk e e' He m m' Hm; simpl in *.
+ intros k k' Hk e e' He m m' Hm; cbn in *.
pattern (mem k m2'); rewrite Hk. (* idem *)
- destruct (mem k' m2'); simpl; rewrite ?Hk,?He,Hm; red; auto.
+ destruct (mem k' m2'); cbn; rewrite ?Hk,?He,Hm; red; auto.
intros k k' e e' i Hneq x.
- case_eq (mem k m2'); case_eq (mem k' m2'); intros; simpl; auto.
+ case_eq (mem k m2'); case_eq (mem k' m2'); intros; cbn; auto.
rewrite !add_o.
destruct (equiv_dec k x); destruct (equiv_dec k' x); auto.
- elim Hneq. etransitivity; eauto.
+ contradiction Hneq. etransitivity; eauto.
Qed.
End MoreWeakFacts.
@@ -1836,7 +1850,7 @@ Section OrdProperties.
apply SortA_equivlistA_eqlistA; auto.
Qed.
- Ltac clean_eauto := unfold K.eq_key_elt, K.ltk; simpl;
+ Ltac clean_eauto := unfold K.eq_key_elt, K.ltk; cbn;
intuition; try solve [order].
Definition gtb (p p':key*elt) :=
@@ -1848,26 +1862,26 @@ Section OrdProperties.
Lemma gtb_1 : forall p p', gtb p p' = true <-> ltk p' p.
Proof.
- intros (x,e) (y,e'); unfold gtb, K.ltk; simpl.
+ intros (x,e) (y,e'); unfold gtb, K.ltk; cbn.
destruct (compare_dec x y); intuition; try discriminate; order.
Qed.
Lemma leb_1 : forall p p', leb p p' = true <-> ~ltk p' p.
Proof.
- intros (x,e) (y,e'); unfold leb, gtb, K.ltk; simpl.
+ intros (x,e) (y,e'); unfold leb, gtb, K.ltk; cbn.
destruct (compare_dec x y); intuition; try discriminate; order.
Qed.
Lemma gtb_compat : forall p, Proper (eq_key_elt==>eq) (gtb p).
Proof.
- red; intros (x,e) (a,e') (b,e'') H; red in H; simpl in *; destruct H.
+ red; intros (x,e) (a,e') (b,e'') H; red in H; cbn in *; destruct H.
generalize (gtb_1 (x,e) (a,e'))(gtb_1 (x,e) (b,e''));
destruct (gtb (x,e) (a,e')); destruct (gtb (x,e) (b,e'')); auto.
- unfold KeyOrderedType.ltk in *; simpl in *; intros.
+ unfold KeyOrderedType.ltk in *; cbn in *; intros.
symmetry; rewrite H2.
apply eq_lt with a; auto.
rewrite <- H1; auto.
- unfold KeyOrderedType.ltk in *; simpl in *; intros.
+ unfold KeyOrderedType.ltk in *; cbn in *; intros.
rewrite H1.
apply eq_lt with b; auto.
rewrite <- H2; auto.
@@ -1887,8 +1901,8 @@ Section OrdProperties.
unfold elements_lt, elements_ge, leb; intros.
apply filter_split with (eqA:=eq_key) (ltA:=ltk); eauto with map.
intros; destruct x; destruct y; destruct p.
- rewrite gtb_1 in H; unfold K.ltk in H; simpl in *.
- unfold gtb, K.ltk in *; simpl in *.
+ rewrite gtb_1 in H; unfold K.ltk in H; cbn in *.
+ unfold gtb, K.ltk in *; cbn in *.
destruct (compare_dec k1 k0); intuition; try discriminate; order.
Qed.
@@ -1910,7 +1924,7 @@ Section OrdProperties.
intros.
rewrite filter_InA in H1; auto with *; destruct H1.
rewrite leb_1 in H2.
- destruct y; unfold KeyOrderedType.ltk in *; simpl in *.
+ destruct y; unfold KeyOrderedType.ltk in *; cbn in *.
rr; rewrite <- elements_mapsto_iff in H1.
assert (~ x == k).
contradict H.
@@ -1920,24 +1934,24 @@ Section OrdProperties.
intros.
rewrite filter_InA in H1; auto with *; destruct H1.
rewrite gtb_1 in H3.
- destruct y; destruct x0; unfold KeyOrderedType.ltk in *; simpl in *.
+ destruct y; destruct x0; unfold KeyOrderedType.ltk in *; cbn in *.
inversion_clear H2.
- red in H4; simpl in *; destruct H4.
+ red in H4; cbn in *; destruct H4.
order.
rewrite filter_InA in H4; auto with *; destruct H4.
rewrite leb_1 in H4.
- unfold KeyOrderedType.ltk in *; simpl in *; order.
+ unfold KeyOrderedType.ltk in *; cbn in *; order.
rr; red; intros a; destruct a.
rewrite InA_app_iff, InA_cons, 2 filter_InA,
<-2 elements_mapsto_iff, leb_1, gtb_1,
find_mapsto_iff, (H0 k), <- find_mapsto_iff,
add_mapsto_iff; try apply eq_key_elt_Equiv; auto with *.
- unfold eq_key_elt, KeyOrderedType.eq_key_elt, KeyOrderedType.ltk; simpl.
+ unfold eq_key_elt, KeyOrderedType.eq_key_elt, KeyOrderedType.ltk; cbn.
destruct (compare_dec k x);
replace (x =/= k) with (~ x == k) in *; intuition.
right; split; auto; order.
order.
- elim H.
+ contradiction H.
exists e0; apply MapsTo_1 with k; auto.
right; right; split; auto; order.
order.
@@ -1956,15 +1970,15 @@ Section OrdProperties.
destruct x0; destruct y.
rr; rewrite <- elements_mapsto_iff in H1.
unfold KeyOrderedType.eq_key_elt, KeyOrderedType.ltk in *;
- simpl in *; destruct H3.
+ cbn in *; destruct H3.
apply lt_eq with x; auto.
- apply H; simpl in *; subst; exists e0; assumption.
+ apply H; cbn in *; subst; exists e0; assumption.
inversion H3.
red; intros a; destruct a.
rr; rewrite InA_app_iff, InA_cons, InA_nil, <- 2 elements_mapsto_iff,
find_mapsto_iff, (H0 k), <- find_mapsto_iff,
add_mapsto_iff by (apply eq_key_elt_Equiv).
- unfold eq_key_elt, KeyOrderedType.eq_key_elt, complement; simpl; intuition.
+ unfold eq_key_elt, KeyOrderedType.eq_key_elt, complement; cbn; intuition.
destruct (equiv_dec x k); intuition auto.
exfalso.
assert (In k m).
@@ -1986,7 +2000,7 @@ Section OrdProperties.
destruct y; destruct x0.
rr; rewrite <- elements_mapsto_iff in H2.
unfold KeyOrderedType.eq_key_elt, KeyOrderedType.ltk in *;
- simpl in *; destruct H3.
+ cbn in *; destruct H3.
apply eq_lt with x; auto.
apply H; exists e0; assumption.
inversion H3.
@@ -1994,7 +2008,7 @@ Section OrdProperties.
rewrite InA_cons, <- 2 elements_mapsto_iff,
find_mapsto_iff, (H0 k), <- find_mapsto_iff,
add_mapsto_iff by (apply eq_key_elt_Equiv).
- unfold eq_key_elt, KeyOrderedType.eq_key_elt; simpl. intuition.
+ unfold eq_key_elt, KeyOrderedType.eq_key_elt; cbn. intuition.
destruct (equiv_dec x k); auto.
exfalso.
assert (In k m).
@@ -2038,30 +2052,30 @@ Section OrdProperties.
generalize (elements_3 m).
revert x e H y x0 H0 H1.
induction (elements m).
- simpl; intros; try discriminate.
+ cbn; intros; try discriminate.
intros.
- destruct a; destruct l; simpl in *.
+ destruct a; destruct l; cbn in *.
injection H; clear H; intros; subst.
inversion_clear H1.
- repeat red in H; simpl in *. destruct H; order.
- elim H0; eauto.
- inversion H; simpl in *.
+ repeat red in H; cbn in *. destruct H; order.
+ contradiction H0; eauto.
+ inversion H; cbn in *.
change (max_elt_aux (p::l) = Some (x,e)) in H.
generalize (IHl x e H); clear IHl; intros IHl.
inversion_clear H1; [ | inversion_clear H2; eauto ].
- red in H3; simpl in H3; destruct H3.
+ red in H3; cbn in H3; destruct H3.
destruct p as (p1,p2).
destruct (equiv_dec p1 x).
apply lt_eq with p1; auto.
inversion_clear H2.
inversion_clear H5.
- simpl in *; subst; rewrite H1.
+ cbn in *; subst; rewrite H1.
inversion H6; exact H5.
- simpl in *; subst.
+ cbn in *; subst.
transitivity p1; auto.
inversion_clear H2.
inversion_clear H5.
- red in H2; simpl in H2; order.
+ red in H2; cbn in H2; order.
inversion_clear H2.
eapply IHl; eauto.
intro Z; apply H4; order.
@@ -2074,8 +2088,8 @@ Section OrdProperties.
unfold max_elt in *.
rewrite elements_mapsto_iff.
induction (elements m).
- simpl; try discriminate.
- destruct a; destruct l; simpl in *.
+ cbn; try discriminate.
+ destruct a; destruct l; cbn in *.
injection H; intros; subst; constructor; red; auto.
constructor 2; auto.
Qed.
@@ -2087,7 +2101,7 @@ Section OrdProperties.
unfold max_elt in *.
rewrite elements_Empty.
induction (elements m); auto.
- destruct a; destruct l; simpl in *; try discriminate.
+ destruct a; destruct l; cbn in *; try discriminate.
assert (H':=IHl H); discriminate.
Qed.
@@ -2109,16 +2123,16 @@ Section OrdProperties.
try discriminate.
destruct p; injection H; intros; subst.
inversion_clear H1.
- red in H2; destruct H2; simpl in *; order.
+ red in H2; destruct H2; cbn in *; order.
inversion_clear H4.
rewrite (@InfA_alt _ eq_key_elt) in H3; eauto with *.
apply (H3 (y,x0)); auto.
constructor; repeat intro.
- destruct x1; repeat red in H4; simpl in H4; order.
+ destruct x1; repeat red in H4; cbn in H4; order.
destruct x1; destruct y0; destruct z.
- unfold lt_key, KeyOrderedType.ltk in *; simpl in *; order.
+ unfold lt_key, KeyOrderedType.ltk in *; cbn in *; order.
unfold KeyOrderedType.eq_key_elt, lt_key, KeyOrderedType.ltk;
- repeat intro; simpl in *; intuition order.
+ repeat intro; cbn in *; intuition order.
Qed.
Lemma min_elt_MapsTo :
@@ -2128,8 +2142,8 @@ Section OrdProperties.
unfold min_elt in *.
rewrite elements_mapsto_iff.
destruct (elements m).
- simpl; try discriminate.
- destruct p; simpl in *.
+ cbn; try discriminate.
+ destruct p; cbn in *.
injection H; intros; subst; constructor; red; auto.
Qed.
@@ -2140,7 +2154,7 @@ Section OrdProperties.
unfold min_elt in *.
rewrite elements_Empty.
destruct (elements m); auto.
- destruct p; simpl in *; discriminate.
+ destruct p; cbn in *; discriminate.
Qed.
End Min_Max_Elt.
@@ -2219,7 +2233,7 @@ Section OrdProperties.
do 2 rewrite fold_1.
do 2 rewrite <- fold_left_rev_right.
apply fold_right_eqlistA with (eqA:=eq_key_elt) (eqB:=eqA); auto.
- intros (k,e) (k',e') (Hk,He) a a' Ha; simpl in *; apply Hf; auto.
+ intros (k,e) (k',e') (Hk,He) a a' Ha; cbn in *; apply Hf; auto.
apply eqlistA_rev. apply elements_Equal_eqlistA. auto.
Qed.
@@ -2235,10 +2249,10 @@ Section OrdProperties.
transitivity (fold_right f' i (rev (elements m1 ++ (x,e)::nil))).
apply fold_right_eqlistA with (eqA:=eq_key_elt) (eqB:=eqA); auto.
intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha;
- unfold f'; simpl in *; apply H; auto.
+ unfold f'; cbn in *; apply H; auto.
apply eqlistA_rev.
apply elements_Add_Above; auto.
- rewrite distr_rev; simpl.
+ rewrite distr_rev; cbn.
reflexivity.
Qed.
@@ -2254,10 +2268,10 @@ Section OrdProperties.
transitivity (fold_right f' i (rev (((x,e)::nil)++elements m1))).
apply fold_right_eqlistA with (eqA:=eq_key_elt) (eqB:=eqA); auto.
intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha;
- unfold f'; simpl in *; apply H; auto.
+ unfold f'; cbn in *; apply H; auto.
apply eqlistA_rev.
- simpl; apply elements_Add_Below; auto.
- rewrite distr_rev; simpl.
+ cbn; apply elements_Add_Below; auto.
+ rewrite distr_rev; cbn.
rewrite fold_right_app.
reflexivity.
Qed.
diff --git a/Util/FMaps/FMapList.v b/Util/FMaps/FMapList.v
index 4786e36fcbe12834a303321ef6f70c2cd70ab7ec..57ee9ef414807718d5444d9856de2e00c9c3685b 100644
--- a/Util/FMaps/FMapList.v
+++ b/Util/FMaps/FMapList.v
@@ -87,9 +87,9 @@ Lemma list_add_3 : forall (m : t elt) x y e e',
x =/= y -> InA (equiv@@1) (y, e) (list_add x e' m) -> InA (equiv@@1) (y, e) m.
Proof using .
intros m x y e e' Hxy Hy. simpl. induction m as [| [z p] l].
-+ inversion_clear Hy; try inversion H0. now elim Hxy.
++ inversion_clear Hy; try inversion H0. now contradiction Hxy.
+ simpl in *. destruct (equiv_dec x z).
- - right. inversion_clear Hy; trivial. now elim Hxy.
+ - right. inversion_clear Hy; trivial. now contradiction Hxy.
- inversion_clear Hy; now left + (right; apply IHl).
Qed.
@@ -202,7 +202,7 @@ Qed.
Instance MapListFacts_mem key `{EqDec key} : FMapSpecs_mem MapList.
Proof using . split.
* intros elt [m Hm] x [e Hin]. simpl in *. induction m as [| [y n] l]; inversion_clear Hin.
- + simpl. destruct (equiv_dec x y) as [Hxy | Hxy]; trivial. elim Hxy. now destruct H0.
+ + simpl. destruct (equiv_dec x y) as [Hxy | Hxy]; trivial. contradiction Hxy. now destruct H0.
+ simpl. destruct (equiv_dec x y) as [Hxy | Hxy]; trivial. inversion_clear Hm. auto.
* intros elt [m Hm] x Hmem. unfold In. simpl in *. induction m as [| [y n] l]; simpl in Hmem.
+ discriminate.
@@ -218,7 +218,7 @@ Proof using . split. intros elt x e Hin. inversion Hin. Qed.
Instance MapListFacts_is_empty key `{EqDec key} : FMapSpecs_is_empty MapList.
Proof using . split.
* intros elt [m Hm] Hm'. destruct m as [| [x n] l]; trivial.
- elim Hm' with x n. now left.
+ contradiction Hm' with x n. now left.
* intros elt [m Hm] Hm'. destruct m as [| [x n] l]; try discriminate.
intros x n Hin. inversion Hin.
Qed.
@@ -232,12 +232,12 @@ Proof using . split.
+ inversion Hy.
+ simpl. destruct (equiv_dec x z).
- right. inversion_clear Hy; trivial.
- elim Hxy. destruct H0. now transitivity z.
+ contradiction Hxy. destruct H0. now transitivity z.
- inversion_clear Hm. inversion_clear Hy; now left + (right; apply IHl).
* intros elt [m Hm] x y e e' Hxy Hy. simpl in *. induction m as [| [z p] l].
- + inversion_clear Hy; inversion H0. now elim Hxy.
+ + inversion_clear Hy; inversion H0. now contradiction Hxy.
+ simpl in *. destruct (equiv_dec x z).
- - right. inversion_clear Hy; trivial. now elim Hxy.
+ - right. inversion_clear Hy; trivial. now contradiction Hxy.
- inversion_clear Hm. inversion_clear Hy; now left + (right; apply IHl).
Qed.
@@ -247,13 +247,13 @@ Proof using . split.
+ simpl. intros [? Habs]. inversion Habs.
+ simpl. inversion_clear Hm. destruct (equiv_dec x z) as [Hxz | Hxz]; auto; [].
intros [n Habs]. inversion_clear Habs.
- - elim Hxz. destruct H2. now transitivity y.
+ - contradiction Hxz. destruct H2. now transitivity y.
- apply IHl; eauto.
* intros elt [m Hm] x y e Hxy Hy. simpl in *. induction m as [| [z p] l].
+ inversion Hy.
+ inversion_clear Hm. simpl. destruct (equiv_dec x z).
- inversion_clear Hy; simpl in *; auto; [].
- elim Hxy. destruct H2. now transitivity z.
+ contradiction Hxy. destruct H2. now transitivity z.
- inversion_clear Hy; now left + (right; apply IHl).
* intros elt [m Hm] x y e Hy. simpl in *. induction m as [| [z p] l].
+ inversion_clear Hy.
@@ -268,7 +268,7 @@ Proof using . split.
+ inversion_clear Hm. simpl. destruct (equiv_dec x y).
- inversion_clear Hin; try (now f_equal); [].
assert (Heq : equiv@@1 (x, e) (y, p)) by assumption.
- elim H0. eapply InA_eqA; eauto with typeclass_instances; [].
+ contradiction H0. eapply InA_eqA; eauto with typeclass_instances; [].
revert H2. apply InA_impl_compat; trivial; [].
now repeat intro.
- inversion_clear Hin; now auto.
@@ -382,7 +382,7 @@ Proof using . split.
- left. simpl. split; trivial. inversion_clear Hin.
-- simpl in *. destruct H2. now subst.
-- assert (Heq : equiv@@1 (x, e) (y, p)) by assumption.
- elim H0. eapply InA_eqA; eauto with typeclass_instances; [].
+ contradiction H0. eapply InA_eqA; eauto with typeclass_instances; [].
revert H2. apply InA_impl_compat; trivial; [].
now repeat intro.
- inversion_clear Hin; try easy; [].
@@ -405,7 +405,7 @@ Proof using . split.
simpl. split; trivial. inversion_clear Hin.
-- simpl in *. destruct H2. now subst.
-- assert (Heq : equiv@@1 (x, e) (y, p)) by assumption.
- elim H0. eapply InA_eqA; eauto with typeclass_instances; [].
+ contradiction H0. eapply InA_eqA; eauto with typeclass_instances; [].
revert H2. apply InA_impl_compat; trivial; [].
now repeat intro.
- inversion_clear Hin; try easy; [].
diff --git a/Util/FSets/FSetList.v b/Util/FSets/FSetList.v
index 4405d949414dc3bd406adb1567d07f7911f4c48d..5ea91988fa7e49928eeb029a03b068d250525329 100644
--- a/Util/FSets/FSetList.v
+++ b/Util/FSets/FSetList.v
@@ -257,9 +257,9 @@ Lemma list_add_3 : forall (m : t elt) x y e e',
x =/= y -> InA (equiv@@1) (y, e) (list_add x e' m) -> InA (equiv@@1) (y, e) m.
Proof.
intros m x y e e' Hxy Hy. simpl. induction m as [| [z p] l].
-+ inversion_clear Hy; try inversion H0. now elim Hxy.
++ inversion_clear Hy; try inversion H0. now contradiction Hxy.
+ simpl in *. destruct (equiv_dec x z).
- - right. inversion_clear Hy; trivial. now elim Hxy.
+ - right. inversion_clear Hy; trivial. now contradiction Hxy.
- inversion_clear Hy; now left + (right; apply IHl).
Qed.*)
@@ -361,7 +361,7 @@ Qed.
Instance MapListFacts_mem key `{EqDec key} : FMapSpecs_mem (MapList _).
Proof. split.
* intros elt [m Hm] x [e Hin]. simpl in *. induction m as [| [y n] l]; inversion_clear Hin.
- + simpl. destruct (equiv_dec x y) as [Hxy | Hxy]; trivial. elim Hxy. now destruct H0.
+ + simpl. destruct (equiv_dec x y) as [Hxy | Hxy]; trivial. contradiction Hxy. now destruct H0.
+ simpl. destruct (equiv_dec x y) as [Hxy | Hxy]; trivial. inversion_clear Hm. auto.
* intros elt [m Hm] x Hmem. unfold In. simpl in *. induction m as [| [y n] l]; simpl in Hmem.
+ discriminate.
@@ -376,7 +376,7 @@ Proof. split. intros elt x e Hin. inversion Hin. Qed.
Instance MapListFacts_is_empty key `{EqDec key} : FMapSpecs_is_empty (MapList _).
Proof. split.
* intros elt [m Hm] Hm'. destruct m as [| [x n] l]; trivial.
- elim Hm' with x n. now left.
+ contradiction Hm' with x n. now left.
* intros elt [m Hm] Hm'. destruct m as [| [x n] l]; try discriminate.
intros x n Hin. inversion Hin.
Qed.
@@ -588,7 +588,7 @@ Proof using . split.
apply is_empty_2 in Hle. intros x Hin. specialize (Hle x).
destruct (mem x s2) eqn:Hmem.
+ now apply mem_2.
- + elim Hle. apply diff_3; trivial; [].
+ + contradiction Hle. apply diff_3; trivial; [].
intro Habs. apply mem_1 in Habs. congruence.
Qed.
diff --git a/Util/FSets/OrderedType.v b/Util/FSets/OrderedType.v
index 2dfbc12a7ed272a2b89d8d0ffd3347bc0cc849ad..fc271f16a98c06ad5d344ab4542a94a3c072757f 100644
--- a/Util/FSets/OrderedType.v
+++ b/Util/FSets/OrderedType.v
@@ -310,9 +310,9 @@ Ltac normalize_notations :=
end.
Ltac abstraction := match goal with
- | H : False |- _ => elim H
- | H : ?x <<< ?x |- _ => elim (lt_antirefl H)
- | H : ?x =/= ?x |- _ => elim (H (reflexivity x))
+ | H : False |- _ => contradiction H
+ | H : ?x <<< ?x |- _ => contradiction (lt_antirefl H)
+ | H : ?x =/= ?x |- _ => contradiction (H (reflexivity x))
| H : ?x === ?x |- _ => clear H; abstraction
| H : ~?x <<< ?x |- _ => clear H; abstraction
| |- ?x === ?x => reflexivity
@@ -703,7 +703,7 @@ Section KeyOrderedType.
Proof using .
intros; red; intros.
destruct H1 as [e' H2].
- elim (@ltk_not_eqk (k,e) (k,e')).
+ contradiction (@ltk_not_eqk (k,e) (k,e')).
eapply Sort_Inf_In; eauto.
red; simpl; auto.
Qed.
diff --git a/Util/Fin.v b/Util/Fin.v
index 42c9ab8f2342a79fe4a1bbab7faeafef1742f4f1..079cac6ae9152eae863ad89ff6580940b91a90b3 100644
--- a/Util/Fin.v
+++ b/Util/Fin.v
@@ -89,6 +89,23 @@ Proof using . reflexivity. Qed.
End greater_than.
+Section prod_bound.
+
+Context {lb1 lb2 : nat} (gtlb1 : greater_than lb1) (gtlb2 : greater_than lb2).
+
+Definition prod_bound : greater_than (Nat.pred ((S lb1) * (S lb2))).
+Proof using gtlb1 gtlb2.
+ constructor 1 with (@ub lb1 gtlb1 * @ub lb2 gtlb2).
+ abstract (erewrite <- Nat.le_succ_l, Nat.lt_succ_pred;
+ [ apply Nat.mul_le_mono; apply Nat.le_succ_l, lt_lb_ub
+ | apply Nat.mul_pos_pos; apply Nat.lt_0_succ]).
+Defined.
+
+Lemma prod_bound_ub : @ub _ prod_bound = @ub lb1 gtlb1 * @ub lb2 gtlb2.
+Proof using . reflexivity. Qed.
+
+End prod_bound.
+
Section mod2fin.
Context {lb : nat} {gtlb : greater_than lb}.
@@ -126,7 +143,7 @@ Proof using .
intros. apply fin2nat_inj. cbn-[Nat.modulo]. apply Nat.mod_mod, neq_ub_0.
Qed.
-Lemma mod2fin2nat : ∀ m : nat, fin2nat (mod2fin m) = m mod ub.
+Lemma mod2fin2nat : ∀ m : nat, mod2fin m = m mod ub :>nat.
Proof using . intros. reflexivity. Qed.
Lemma mod2finK : ∀ f : fin ub, mod2fin f = f.
@@ -149,7 +166,7 @@ Qed.
Definition fin0 : fin ub := Fin lt_0_ub.
-Lemma fin02nat : fin2nat fin0 = 0.
+Lemma fin02nat : fin0 = 0 :>nat.
Proof using . reflexivity. Qed.
Lemma mod2fin0 : mod2fin 0 = fin0.
@@ -163,7 +180,7 @@ Definition addm (f : fin ub) (m : nat) : fin ub := mod2fin (f + m).
Definition addm_compat : Proper (equiv ==> equiv ==> equiv) addm := _.
Lemma addm2nat : ∀ (f : fin ub) (m : nat),
- fin2nat (addm f m) = (f + m) mod ub.
+ addm f m = (f + m) mod ub :>nat.
Proof using . unfold addm. intros. apply mod2fin2nat. Qed.
Lemma addm_mod : ∀ (f : fin ub) (m : nat), addm f (m mod ub) = addm f m.
@@ -176,9 +193,11 @@ Lemma addIm : ∀ m : nat,
Preliminary.injective equiv equiv (λ f : fin ub, addm f m).
Proof using .
intros * f1 f2 H. eapply fin2nat_inj, (Nat.add_cancel_r _ _ m).
- eapply (@mod2fin_bounded_diff_inj m). 3: apply H. all: split.
- 1,3: apply le_plus_r. all: rewrite Nat.add_comm. all: apply Nat.add_lt_mono_l,
- fin_lt.
+ refine (@mod2fin_bounded_diff_inj m _ _ _ _ H).
+ all: rewrite plus_comm; split.
+ 1,3: rewrite (plus_n_O m) at 1.
+ 1,2: rewrite <-Nat.add_le_mono_l; apply Nat.le_0_l.
+ all: rewrite <-Nat.add_lt_mono_l; apply fin_lt.
Qed.
Lemma addm_locally_inj :
@@ -266,7 +285,7 @@ Definition addf (f1 f2 : fin ub) : fin ub := addm f1 f2.
Definition addf_compat : Proper (equiv ==> equiv ==> equiv) addf := _.
Lemma addf2nat : ∀ f1 f2 : fin ub,
- fin2nat (addf f1 f2) = (f1 + f2) mod ub.
+ addf f1 f2 = (f1 + f2) mod ub :>nat.
Proof using . intros. apply addm2nat. Qed.
Lemma addf_fin0_divide : ∀ f1 f2 : fin ub,
@@ -332,7 +351,7 @@ Definition rev_fin (f : fin ub) : fin ub := Fin (rev_fin_subproof f).
Definition rev_fin_compat : Proper (equiv ==> equiv) rev_fin := _.
-Lemma rev_fin2nat : ∀ f : fin ub, fin2nat (rev_fin f) = Nat.pred ub - f.
+Lemma rev_fin2nat : ∀ f : fin ub, rev_fin f = Nat.pred ub - f :>nat.
Proof using . reflexivity. Qed.
Lemma rev_finK : ∀ f : fin ub, rev_fin (rev_fin f) = f.
@@ -350,7 +369,7 @@ Definition oppf (f : fin ub) : fin ub := addm (rev_fin f) 1.
Definition oppf_compat : Proper (equiv ==> equiv) oppf := _.
-Lemma oppf2nat : ∀ f : fin ub, fin2nat (oppf f) = (ub - f) mod ub.
+Lemma oppf2nat : ∀ f : fin ub, oppf f = (ub - f) mod ub :>nat.
Proof using .
intros. unfold oppf. rewrite addm2nat. f_equal. erewrite rev_fin2nat,
<- Nat.add_sub_swap, Nat.add_1_r, S_pred_ub. reflexivity. apply fin_le.
@@ -360,8 +379,7 @@ Definition oppm (m : nat) : fin ub := oppf (mod2fin m).
Definition oppm_compat : Proper (equiv ==> equiv) oppm := _.
-Lemma oppm2nat : ∀ m : nat,
- fin2nat (oppm m) = (ub - (m mod ub)) mod ub.
+Lemma oppm2nat : ∀ m : nat, oppm m = (ub - (m mod ub)) mod ub :>nat.
Proof using .
intros. unfold oppm. rewrite oppf2nat, mod2fin2nat. reflexivity.
Qed.
@@ -453,14 +471,14 @@ Proof using .
Qed.
Lemma subm2nat : ∀ (f : fin ub) (m : nat),
- fin2nat (subm f m) = (f + (ub - (m mod ub))) mod ub.
+ subm f m = (f + (ub - (m mod ub))) mod ub :>nat.
Proof using .
intros. unfold subm. rewrite addm2nat, oppm2nat, Nat.add_mod_idemp_r.
reflexivity. apply neq_ub_0.
Qed.
Lemma subf2nat : ∀ f1 f2 : fin ub,
- fin2nat (subf f1 f2) = (f1 + (ub - f2)) mod ub.
+ subf f1 f2 = (f1 + (ub - f2)) mod ub :>nat.
Proof using .
intros. rewrite subf_subm, subm2nat, (Nat.mod_small f2). reflexivity.
apply fin_lt.
@@ -597,7 +615,7 @@ Lemma oppf_add : ∀ f : fin ub, f ≠fin0 -> f + oppf f = ub.
Proof using .
intros f H. rewrite oppf2nat, Nat.mod_small. symmetry. apply le_plus_minus.
2: apply Nat.sub_lt. 1,2: apply Nat.lt_le_incl, fin_lt. apply neq_0_lt.
- intros Habs. elim H. apply fin2nat_inj. rewrite fin02nat, Habs. reflexivity.
+ intros Habs. apply H. apply fin2nat_inj. rewrite fin02nat, Habs. reflexivity.
Qed.
Lemma addfE : ∀ f1 f2 : fin ub, addf f1 f2 = subf f1 (oppf f2).
@@ -670,20 +688,19 @@ Proof using . intros f1 f2. apply addf_addm. Qed.
Lemma asbfVE : ∀ f : fin ub, asbf fâ»Â¹ == asbm fâ»Â¹.
Proof using . intros f1 f2. apply subf_subm. Qed.
-Lemma asbm2nat : ∀ (m : nat) (f : fin ub),
- fin2nat (asbm m f) = (f + m) mod ub.
+Lemma asbm2nat : ∀ (m : nat) (f : fin ub), asbm m f = (f + m) mod ub :>nat.
Proof using . intros. apply addm2nat. Qed.
Lemma asbf2nat : ∀ (f1 f2 : fin ub),
- fin2nat (asbf f1 f2) = (f2 + f1) mod ub.
+ asbf f1 f2 = (f2 + f1) mod ub :>nat.
Proof using . intros. apply addf2nat. Qed.
Lemma asbmV2nat : ∀ (m : nat) (f : fin ub),
- fin2nat ((asbm m)â»Â¹ f) = (f + (ub - (m mod ub))) mod ub.
+ (asbm m)â»Â¹ f = (f + (ub - (m mod ub))) mod ub :>nat.
Proof using . intros. apply subm2nat. Qed.
Lemma asbfV2nat : ∀ (f1 f2 : fin ub),
- fin2nat ((asbf f1)â»Â¹ f2) = (f2 + (ub - f1)) mod ub.
+ (asbf f1)â»Â¹ f2 = (f2 + (ub - f1)) mod ub :>nat.
Proof using . intros. apply subf2nat. Qed.
Lemma asbm_mod : ∀ m : nat, asbm (m mod ub) == asbm m.
@@ -853,8 +870,7 @@ Definition symf_compat : Proper (equiv ==> equiv ==> equiv) symf := _.
Lemma symfE : ∀ c f : fin ub, symf c f = addf c (subf c f).
Proof using . reflexivity. Qed.
-Lemma symf2nat : ∀ c f : fin ub,
- fin2nat (symf c f) = (ub - f + c + c) mod ub.
+Lemma symf2nat : ∀ c f : fin ub, symf c f = (ub - f + c + c) mod ub :>nat.
Proof using .
intros. rewrite symfE, addf2nat, subf2nat, Nat.add_mod_idemp_r, Nat.add_assoc,
(Nat.add_comm _ (_ - _)), Nat.add_assoc. reflexivity. apply neq_ub_0.
@@ -917,7 +933,7 @@ Proof using . intros. rewrite diffE, subf0. reflexivity. Qed.
Lemma diff_neq : ∀ f1 f2 : fin ub, f1 ≠f2 -> 0 < diff f1 f2.
Proof using .
- intros * H. apply neq_0_lt. intros Habs. elim H. eapply diffI.
+ intros * H. apply neq_0_lt. intros Habs. apply H. eapply diffI.
rewrite (difff f1). apply Habs.
Qed.
diff --git a/Util/ListComplements.v b/Util/ListComplements.v
index 742d86e22ea5e85604caf909351180f7f7a41ae2..236ef41264f9d23942a68eb97aae0f4d492bf36c 100644
--- a/Util/ListComplements.v
+++ b/Util/ListComplements.v
@@ -64,14 +64,14 @@ Proof using . intros [| x l]; auto. right. exists x. now left. Qed.
Lemma not_nil_In : forall l : list A, l <> nil -> exists x, In x l.
Proof using .
intros [| x l] Hl.
-- now elim Hl.
+- now contradiction Hl.
- exists x. now left.
Qed.
Lemma not_nil_last : forall l, l <> nil -> exists (a : A) l', l = l' ++ a :: nil.
Proof using .
intros l Hl. induction l.
-+ now elim Hl.
++ now contradiction Hl.
+ destruct l.
- exists a, nil. reflexivity.
- destruct (IHl ltac:(discriminate)) as [b [l'' Hl'']].
@@ -108,7 +108,7 @@ Qed. *)
exists l1, exists l2, ~List.In x l1 /\ l = l1 ++ x :: l2.
Proof.
intros x l. induction l as [| a l]; intro Hin.
- now elim (List.in_nil Hin).
+ now contradiction (List.in_nil Hin).
destruct Hin.
subst. exists nil. exists l. intuition.
destruct (IHl H) as [l1 [l2 [Hnin Heq]]].
@@ -127,28 +127,28 @@ Qed.
Lemma hd_indep : forall l (d d' : A), l <> nil -> hd d l = hd d' l.
Proof using .
intros [| x l] d d' Hl.
-- now elim Hl.
+- now contradiction Hl.
- reflexivity.
Qed.
Lemma last_indep : forall l (d d' : A), l <> nil -> last l d = last l d'.
Proof using .
induction l as [| x l]; intros d d' Hl.
-- now elim Hl.
+- now contradiction Hl.
- destruct l; trivial. apply IHl. discriminate.
Qed.
Lemma hd_In : forall (d : A) l, l <> nil -> In (hd d l) l.
Proof using .
intros d [| x l] Hl.
-- now elim Hl.
+- now contradiction Hl.
- now left.
Qed.
Lemma last_In : forall l (d : A), l <> List.nil -> List.In (List.last l d) l.
Proof using .
induction l as [| x l]; intros d Hl.
-- now elim Hl.
+- now contradiction Hl.
- destruct l; try now left. right. apply IHl. discriminate.
Qed.
@@ -167,7 +167,7 @@ Proof using .
intros d l1 l2 Hl2. induction l1; simpl.
reflexivity.
assert (l1 ++ l2 <> nil). { intro Habs. apply Hl2. now destruct (app_eq_nil _ _ Habs). }
- destruct (l1 ++ l2). now elim H. assumption.
+ destruct (l1 ++ l2). now contradiction H. assumption.
Qed.
Lemma rev_nil : forall l : list A, rev l = nil <-> l = nil.
@@ -317,9 +317,9 @@ induction l.
+ inversion_clear Hfl.
rewrite InA_cons in *. destruct Hx as [Hx | Hx], Hy as [Hy | Hy].
- now rewrite Hx, Hy.
- - match goal with H : ~ InA _ _ _ |- _ => elim H end.
+ - match goal with H : ~ InA _ _ _ |- _ => contradiction H end.
rewrite <- Hx, Hxy, InA_map_iff; firstorder.
- - match goal with H : ~ InA _ _ _ |- _ => elim H end.
+ - match goal with H : ~ InA _ _ _ |- _ => contradiction H end.
rewrite <- Hy, <- Hxy, InA_map_iff; firstorder.
- auto.
Qed.
@@ -829,7 +829,7 @@ Lemma NoDupA_2 : forall x y, ~eqA x y -> NoDupA eqA (x :: y :: nil).
Proof using .
intros x y Hdiff. constructor.
intro Habs. inversion_clear Habs.
- now elim Hdiff.
+ now contradiction Hdiff.
inversion H.
apply NoDupA_singleton.
Qed.
@@ -899,7 +899,7 @@ Lemma not_NoDupA : (forall x y, {eqA x y} + {~eqA x y} ) ->
Proof using HeqA.
intros eq_dec l. split; intro Hl.
* induction l.
- + elim Hl. now constructor.
+ + contradiction Hl. now constructor.
+ destruct (InA_dec eq_dec a l) as [Hin | Hnin].
- exists a. apply (PermutationA_split _) in Hin.
destruct Hin as [l' Hperm]. exists l'. now rewrite Hperm.
@@ -1058,7 +1058,7 @@ Qed.
Lemma inclA_dec : forall l1 l2, {inclA eqA l1 l2} + {~inclA eqA l1 l2}.
Proof.
induction l1 as [| x1 l1 Hrec]; intro l2.
-* left. abstract (intros x Habs; rewrite InA_nil in Habs; elim Habs).
+* left. abstract (intros x Habs; rewrite InA_nil in Habs; contradiction Habs).
* refine (match InA_dec eq_dec x1 l2 with
| left in_x => match Hrec l2 with
| left in_l => left _
@@ -1093,7 +1093,7 @@ Lemma not_inclA : forall l1 l2, ~inclA eqA l1 l2 <-> exists x, InA eqA x l1 /\ ~
Proof using HeqA eq_dec.
intros l1 l2. split; intro H.
* induction l1 as [| e l1].
- + elim H. intro. now rewrite InA_nil.
+ + contradiction H. intro. now rewrite InA_nil.
+ destruct (InA_dec eq_dec e l2).
- assert (Hincl : ~ inclA eqA l1 l2).
{ intro Hincl. apply H. intros x Hin. inversion_clear Hin.
@@ -1181,14 +1181,14 @@ intros a b Hab l. induction l as [| x l]; intros [| x' l'] Hl.
apply (PermutationA_cons_inv _), IHl in Hl. simpl.
rewrite Hl. repeat rewrite countA_occ_app. simpl.
destruct (eq_dec x a) as [Hx | Hx], (eq_dec y b) as [Hy | Hy]; try lia.
- - elim Hy. now rewrite <- Hxy, <- Hab.
- - elim Hx. now rewrite Hxy, Hab.
+ - contradiction Hy. now rewrite <- Hxy, <- Hab.
+ - contradiction Hx. now rewrite Hxy, Hab.
Qed.
Lemma countA_occ_alls_in : forall x n, countA_occ x (alls x n) = n.
Proof using HeqA.
intros x n. induction n; simpl; trivial.
-destruct (eq_dec x x) as [| Hneq]. now rewrite IHn. now elim Hneq.
+destruct (eq_dec x x) as [| Hneq]. now rewrite IHn. now contradiction Hneq.
Qed.
Lemma countA_occ_alls_out : forall x y n, ~eqA x y -> countA_occ y (alls x n) = 0%nat.
@@ -1199,11 +1199,11 @@ Proof using HeqA.
intros x l. induction l as [| a l]; simpl.
+ split; intro Habs.
- lia.
- - rewrite InA_nil in Habs. elim Habs.
+ - rewrite InA_nil in Habs. contradiction Habs.
+ destruct (eq_dec a x) as [Heq | Heq].
- split; intro; lia || now left.
- rewrite IHl. split; intro Hin; try now right; [].
- inversion_clear Hin; trivial. now elim Heq.
+ inversion_clear Hin; trivial. now contradiction Heq.
Qed.
Lemma countA_occ_length_le : forall l (x : A), countA_occ x l <= length l.
@@ -1259,7 +1259,7 @@ intros x l. induction l as [| a l]; intro n; simpl.
destruct n as [| n]; try lia; [].
f_equal. rewrite IHl. simpl in Hn. rewrite <- Heq in Hn at 1.
apply PermutationA_cons_inv in Hn; autoclass.
- + rewrite IHl. destruct (eq_dec x a); try (now elim Heq); [].
+ + rewrite IHl. destruct (eq_dec x a); try (now contradiction Heq); [].
rewrite <- PermutationA_middle; autoclass; [].
split; intro Hperm.
- now constructor.
@@ -1299,8 +1299,8 @@ Qed.
Lemma firstn_In : forall (l : list A) n, incl (firstn n l) l.
Proof using .
induction l; intros n x Hin.
-+ destruct n; elim Hin.
-+ destruct n; try now elim Hin. simpl in Hin. destruct Hin.
++ destruct n; contradiction Hin.
++ destruct n; try now contradiction Hin. simpl in Hin. destruct Hin.
- subst. now left.
- right. now apply IHl in H.
Qed.
@@ -1313,7 +1313,7 @@ Lemma firstn_add_tl_In : forall n l (x a : A),
Proof using .
induction n; intros l x a Hin; simpl in *.
- assumption.
-- destruct l as [| b l]; simpl in *; solve [elim Hin | intuition].
+- destruct l as [| b l]; simpl in *; solve [contradiction Hin | intuition].
Qed.
Lemma firstn_add_tl : forall l n (a : A), n <= length l -> firstn n (l ++ a :: nil) = firstn n l.
@@ -1338,8 +1338,8 @@ Qed.
Lemma skipn_In : forall (l : list A) n, incl (skipn n l) l.
Proof using .
induction l; intros n x Hin.
-+ destruct n; elim Hin.
-+ destruct n; try now elim Hin. simpl in Hin. apply IHl in Hin. now right.
++ destruct n; contradiction Hin.
++ destruct n; [apply Hin|]. simpl in Hin. apply IHl in Hin. now right.
Qed.
Lemma In_skipn : forall l l' (pt : A) n, n <= length l -> In pt (skipn n (l ++ pt :: l')).
@@ -1360,7 +1360,7 @@ Lemma skipn_add_tl_In : forall n l (x a : A), In x (skipn n l) -> In x (skipn n
Proof using .
induction n; intros l x a Hin; simpl in *.
- rewrite in_app_iff. now left.
-- destruct l as [| b l]; simpl in *; solve [elim Hin | auto].
+- destruct l as [| b l]; simpl in *; solve [contradiction Hin | auto].
Qed.
Lemma In_skipn_add : forall l (pt : A), In pt (skipn (Nat.div2 (length l)) (l ++ pt :: nil)).
@@ -1644,7 +1644,7 @@ Lemma max_list_ex : forall f l, l <> nil ->
exists pt, InA equiv pt l /\ max_list f l = Rmax (f pt) 0.
Proof using .
intros f l Hl. induction l as [| pt l].
-* now elim Hl.
+* now contradiction Hl.
* destruct (nil_or_In_dec l) as [? | Hin].
+ subst l. exists pt. split; eauto; now left.
+ assert (Hnil : l <> nil). { intro. subst. destruct Hin as [? []]. }
diff --git a/Util/MMultiset/MMultisetExtraOps.v b/Util/MMultiset/MMultisetExtraOps.v
index 30677495aaa4e099bc815798eab0ca89ae3ed86a..d9bb7d3322b4c1071a630fabf33628d43fd72fc2 100644
--- a/Util/MMultiset/MMultisetExtraOps.v
+++ b/Util/MMultiset/MMultisetExtraOps.v
@@ -191,7 +191,7 @@ Section MMultisetExtra.
+ destruct_match.
- rewrite <- IHl. clear IHl.
split; [intros [Hxy Hin] | intro Hin]; intuition.
- inv Hin; try tauto; []. elim Hxy. hnf in *. simpl in *. now transitivity (fst e).
+ inv Hin; try tauto; []. contradiction Hxy. hnf in *. simpl in *. now transitivity (fst e).
- split; [intros [Hxy Hin] | intro Hin].
-- inv Hin; try (now left); []. right. intuition.
-- inv Hin; intuition.
@@ -386,7 +386,7 @@ Section MMultisetExtra.
+ intros m x n Hm Hn Hrec. rewrite map_add, size_add, size_add; trivial.
destruct (In_dec x m) as [Hin | Hin], (In_dec (f x) (map f m)) as [Hinf | Hinf].
- apply Hrec.
- - elim Hinf. rewrite map_In. now exists x.
+ - contradiction Hinf. rewrite map_In. now exists x.
- lia.
- lia.
+ now rewrite map_empty.
@@ -754,7 +754,7 @@ Section MMultisetExtra.
Proof using M.
intro m. split; intro Heq.
+ destruct (empty_or_In_dec m) as [? | [x Hin]]; trivial.
- elim (Nat.lt_irrefl 0). apply Nat.lt_le_trans with m[x].
+ contradiction (Nat.lt_irrefl 0). apply Nat.lt_le_trans with m[x].
- exact Hin.
- rewrite <- Heq. apply max_mult_spec_weak.
+ rewrite Heq. apply max_mult_empty.
@@ -1049,7 +1049,7 @@ Section MMultisetExtra.
- exists x. split.
-- msetdec.
-- rewrite Nat.eqb_eq, Max.max_l; try lia. msetdec.
- * intros x Hin. elim (In_empty Hin).
+ * intros x Hin. contradiction (In_empty Hin).
Qed.
Lemma max_is_empty : forall m, max m == empty <-> m == empty.
@@ -1150,7 +1150,7 @@ Section MMultisetExtra.
destruct (Max.max_spec n (max_mult m)) as [[Hmax1 Hmax2] | [Hmax1 Hmax2]].
- exists max_m. msetdec.
- exists x. msetdec.
- * intro Habs. Fail now msetdec. (* BUG? *) now elim Habs.
+ * intro Habs. Fail now msetdec. (* BUG? *) now contradiction Habs.
Qed.
Lemma max_In_mult3 : forall m x, In x m -> (In x (max m) <-> m[x] = max_mult m).
diff --git a/Util/MMultiset/MMultisetFacts.v b/Util/MMultiset/MMultisetFacts.v
index b887ba7066b7545ddcb291b7d36a2dfff6e5d00a..720d3e127089678c1b069bfbfac84a6c3cfc511a 100644
--- a/Util/MMultiset/MMultisetFacts.v
+++ b/Util/MMultiset/MMultisetFacts.v
@@ -13,8 +13,7 @@ Require Import Bool Lia PeanoNat.
Require Import PArith RelationPairs.
(* Require Import Equalities. *)
Require Import SetoidList SetoidDec.
-From Pactole Require Import Util.SetoidDefs
- Util.MMultiset.Preliminary Util.MMultiset.MMultisetInterface.
+From Pactole.Util Require Import SetoidDefs MMultiset.Preliminary MMultiset.MMultisetInterface.
Set Implicit Arguments.
@@ -75,7 +74,7 @@ Section MMultisetFacts.
| H : ?x = ?x |- _ => clear H
| H : ?x == ?x |- _ => clear H
| H : ?x = ?y |- _ => subst x || rewrite H in *
- | Hneq : ?x =/= ?x |- _ => now elim Hneq
+ | Hneq : ?x =/= ?x |- _ => now contradiction Hneq
| Heq : @equiv elt _ ?x ?y |- _ => clear x Heq || rewrite Heq in *
| Heq : @equiv (multiset _) _ ?x ?y, Hin : context[?x] |- _ => rewrite Heq in Hin
| Heq : @equiv (multiset _) _ ?x ?y |- context[?x] => rewrite Heq
@@ -117,7 +116,7 @@ Section MMultisetFacts.
Lemma InA_pair_elt : forall x n p l, InA eq_pair (x, n) l -> InA eq_elt (x, p) l.
Proof using .
intros x n p l Hin. induction l as [| [y q] l].
- + rewrite InA_nil in Hin. elim Hin.
+ + rewrite InA_nil in Hin. contradiction Hin.
+ inversion_clear Hin.
- destruct H as [Heq ?]. now left.
- right. now apply IHl.
@@ -126,7 +125,7 @@ Section MMultisetFacts.
Lemma InA_elt_pair : forall x n l, InA eq_elt (x, n) l -> exists n', InA eq_pair (x, n') l.
Proof using .
intros x n l Hin. induction l as [| [y p] l].
- + rewrite InA_nil in Hin. elim Hin.
+ + rewrite InA_nil in Hin. contradiction Hin.
+ inversion_clear Hin.
- compute in H. exists p. left. now rewrite H.
- apply IHl in H. destruct H as [k Hin]. exists k. now right.
@@ -533,7 +532,7 @@ Section MMultisetFacts.
Proof using FMultisetsSpec. repeat intro. msetdec. Qed.
Lemma remove_singleton_other : forall x y n p, ~y == x -> remove y n (singleton x p) == singleton x p.
- Proof using FMultisetsSpec. repeat intro. msetdec. (* BUG?: saturate_Einequalities should work! *) now elim H. Qed.
+ Proof using FMultisetsSpec. repeat intro. msetdec. (* BUG?: saturate_Einequalities should work! *) now contradiction H. Qed.
Theorem elements_singleton : forall x n, n > 0 -> eqlistA eq_pair (elements (singleton x n)) ((x, n) :: nil).
Proof using FMultisetsSpec.
@@ -984,7 +983,7 @@ Section MMultisetFacts.
intros m1 m2. split; intro Hin.
+ intro x. destruct (In_dec x m1) as [Hin1 | Hin1], (In_dec x m2) as [Hin2 | Hin2]; auto.
assert (Habs : In x (inter m1 m2)). { rewrite inter_In. auto. }
- rewrite Hin in Habs. apply In_empty in Habs. elim Habs.
+ rewrite Hin in Habs. apply In_empty in Habs. contradiction Habs.
+ intro x. rewrite empty_spec, inter_spec. destruct (Hin x) as [[Hin1 Hin2] | [[Hin1 Hin2] | [Hin1 Hin2]]];
rewrite not_In in *; try rewrite Hin1; try rewrite Hin2; auto with arith.
Qed.
@@ -1272,7 +1271,7 @@ Section MMultisetFacts.
{ intros n Habs. rewrite elements_spec in Habs. destruct Habs. simpl in *. lia. }
destruct (mâ‚[x]) eqn:Hmâ‚. reflexivity.
specialize (Hin (S n)). rewrite <- Heq in Hin. rewrite elements_spec in Hin.
- elim Hin. split; simpl. assumption. lia.
+ contradiction Hin. split; simpl. assumption. lia.
- assert (Hin : InA eq_pair (x, S n) (elements mâ‚‚)). { rewrite elements_spec. split; simpl. assumption. lia. }
rewrite <- Heq in Hin. rewrite elements_spec in Hin. now destruct Hin.
+ intros [x n]. now rewrite Heq.
@@ -1395,7 +1394,7 @@ Section MMultisetFacts.
+ apply removeA_NoDupA; refine _. apply (NoDupA_strengthen _ (elements_NoDupA _)).
+ intros [y p]. rewrite removeA_InA_iff; refine _. rewrite elements_remove, elements_spec. simpl. intuition.
- destruct H1. contradiction.
- - destruct (equiv_dec y x) as [Heq | Heq]; auto. elim H1. split; msetdec.
+ - destruct (equiv_dec y x) as [Heq | Heq]; auto. contradiction H1. split; msetdec.
Qed.
Lemma elements_remove2 : forall x n m, n < m[x] ->
@@ -1406,7 +1405,7 @@ Section MMultisetFacts.
+ apply (NoDupA_strengthen _ (elements_NoDupA _)).
+ constructor.
- intro Habs. eapply InA_pair_elt in Habs. rewrite removeA_InA_iff in Habs; refine _.
- destruct Habs as [_ Habs]. now elim Habs.
+ destruct Habs as [_ Habs]. now contradiction Habs.
- eapply (NoDupA_strengthen subrelation_pair_elt). apply removeA_NoDupA, elements_NoDupA; refine _.
+ intros [y p]. rewrite elements_remove, elements_spec. simpl. intuition.
- rewrite H. left. split. compute. reflexivity. assumption.
@@ -1416,9 +1415,9 @@ Section MMultisetFacts.
+ inversion_clear H.
- left. destruct H0. repeat split; auto. hnf in *. simpl in *. lia.
- apply (InA_pair_elt (m[x])) in H0. rewrite Heq, removeA_InA in H0; refine _.
- destruct H0 as [_ Habs]. elim Habs. reflexivity.
+ destruct H0 as [_ Habs]. contradiction Habs. reflexivity.
+ right. split; trivial. inversion_clear H.
- - elim Heq. destruct H0. auto.
+ - contradiction Heq. destruct H0. auto.
- apply removeA_InA_weak in H0. rewrite elements_spec in H0. assumption. }
Qed.
@@ -1556,7 +1555,7 @@ Section MMultisetFacts.
+ apply add_is_singleton in Hin. specialize (Hin z). msetdec. destruct Hl as [_ Hl].
inversion_clear Hl. inversion_clear H0. simpl in *. lia. }
destruct Heq as [Heq1 Heq2]. destruct Hl as [Hl _]. inversion_clear Hl.
- elim H. left. compute. now transitivity x.
+ contradiction H. left. compute. now transitivity x.
- inversion_clear Hin. inversion_clear H0.
Qed.
@@ -1572,7 +1571,7 @@ Section MMultisetFacts.
Lemma from_elements_in : forall x n l, NoDupA eq_elt l -> InA eq_pair (x, n) l -> (from_elements l)[x] = n.
Proof using FMultisetsSpec.
intros x n l Hl Hin. induction l as [| [y p] l].
- + rewrite InA_nil in Hin. elim Hin.
+ + rewrite InA_nil in Hin. contradiction Hin.
+ simpl. inversion_clear Hin.
- destruct H as [Hx Hn]. compute in Hx, Hn. inversion Hl. now rewrite Hx, add_same, (@from_elements_out y p).
- inversion_clear Hl. rewrite add_other. now apply IHl.
@@ -1614,8 +1613,8 @@ Section MMultisetFacts.
Proof using FMultisetsSpec.
intros l x. induction l as [| [y p] l].
* simpl. split; intro Hin.
- + elim (In_empty Hin).
- + destruct Hin as [? [Hin _]]. rewrite InA_nil in Hin. elim Hin.
+ + contradiction (In_empty Hin).
+ + destruct Hin as [? [Hin _]]. rewrite InA_nil in Hin. contradiction Hin.
* simpl. rewrite add_In, IHl; trivial. split; intros Hin.
+ destruct Hin as [[? Heq] | [n [Hin Hn]]].
- exists p. split; try (left; split); auto; lia.
@@ -1650,10 +1649,10 @@ Section MMultisetFacts.
- subst. now repeat left.
- inversion_clear Hp.
-- destruct H; auto.
- -- inversion_clear Hnodup. elim H0. revert H. apply InA_pair_elt.
+ -- inversion_clear Hnodup. contradiction H0. revert H. apply InA_pair_elt.
+ rewrite add_other; trivial. destruct l as [| z l].
- simpl. rewrite empty_spec. intuition; try lia.
- inversion_clear H. destruct H0; try contradiction. rewrite InA_nil in H0. elim H0.
+ inversion_clear H. destruct H0; try contradiction. rewrite InA_nil in H0. contradiction H0.
- inversion_clear Hnodup. rewrite IHl; discriminate || trivial. intuition.
inversion_clear H1; trivial. destruct H2. contradiction.
Qed.
@@ -1683,7 +1682,7 @@ Section MMultisetFacts.
rewrite from_elements_cons, add_merge. rewrite elements_add_out.
- constructor; try reflexivity. apply is_elements_cons_inv in Hl'.
rewrite Hin, elements_from_elements; trivial. simpl.
- destruct pair_dec as [? | Habs]; try now elim Habs.
+ destruct pair_dec as [? | Habs]; try now contradiction Habs.
rewrite removeA_out; try reflexivity. intro Habs. apply Hout. revert Habs. apply InA_pair_elt.
- apply proj2 in Hl'. inversion_clear Hl'. simpl in *. lia.
- apply is_elements_cons_inv in Hl'. rewrite <- elements_In, elements_from_elements; eauto.
@@ -1920,7 +1919,7 @@ Section MMultisetFacts.
+ pattern m. apply ind; clear m.
- intros m1 m2 Hm. setoid_rewrite Hm. reflexivity.
- intros m x n Hm Hn Hrec _. exists x. apply add_In. left. split; lia || reflexivity.
- - intro Habs. now elim Habs.
+ - intro Habs. now contradiction Habs.
+ intros [x Hin]. intro Habs. revert Hin. rewrite Habs. apply In_empty.
Qed.
@@ -1986,7 +1985,7 @@ Section MMultisetFacts.
destruct (equiv_dec z x).
exfalso. revert Hin. msetdec.
split; msetdec.
- destruct Hin. msetdec. (* BUG?: saturate_Einequalities shou work! *) now elim H0.
+ destruct Hin. msetdec. (* BUG?: saturate_Einequalities shou work! *) now contradiction H0.
- do 2 rewrite support_spec. unfold In in *. msetdec.
Qed.
@@ -2065,7 +2064,7 @@ Section MMultisetFacts.
intro m. split; intro Hm.
+ intro y. rewrite empty_spec, <- empty_spec with y. revert y. change (m == empty). rewrite <- elements_nil.
destruct (elements m) as [| [x n] l] eqn:Helt. reflexivity.
- simpl in Hm. elim (Nat.lt_irrefl 0). apply Nat.lt_le_trans with n.
+ simpl in Hm. contradiction (Nat.lt_irrefl 0). apply Nat.lt_le_trans with n.
- apply elements_pos with x m. rewrite Helt. now left.
- assert (Hn : m[x] = n). { eapply proj1. rewrite <- (elements_spec (x, n)), Helt. now left. }
rewrite <- Hn, <- Hm. apply cardinal_lower.
@@ -2217,7 +2216,7 @@ Section MMultisetFacts.
- inversion Hin.
- exists x. rewrite <- support_spec, Heq. now left.
+ destruct Hin as [x Hin]. destruct (size m) eqn:Hsize.
- - rewrite size_0 in Hsize. rewrite Hsize in Hin. elim (In_empty Hin).
+ - rewrite size_0 in Hsize. rewrite Hsize in Hin. contradiction (In_empty Hin).
- auto with arith.
Qed.
@@ -2235,7 +2234,7 @@ Section MMultisetFacts.
assert (Hnodup : NoDupA equiv (x :: l)). { rewrite <- Hin. apply support_NoDupA. }
(* XXX: why does [rewrite Hin] fails here? *)
rewrite removeA_Perm_compat; eauto; try reflexivity || apply setoid_equiv; []. rewrite Hin.
- simpl. destruct (equiv_dec x x) as [_ | Hneq]; try now elim Hneq.
+ simpl. destruct (equiv_dec x x) as [_ | Hneq]; try now contradiction Hneq.
inversion_clear Hnodup. now rewrite removeA_out.
Qed.
@@ -3485,7 +3484,7 @@ Section MMultisetFacts.
- right. exists y. now split.
+ symmetry. rewrite orb_false_iff. rewrite exists_false in *; trivial.
assert (Hxm : m[x] = 0) by (unfold In in Hin; lia). split.
- - destruct (f x n) eqn:Hfxn; trivial. elim Hm. exists x. split; msetdec.
+ - destruct (f x n) eqn:Hfxn; trivial. contradiction Hm. exists x. split; msetdec.
- intros [y [Hy Hfy]]. apply Hm. exists y. unfold In in *. split; msetdec.
Qed.
@@ -3499,7 +3498,7 @@ Section MMultisetFacts.
rewrite <- (@add_remove_cancel x), exists_add; trivial.
- apply (Hf2 _ _ (reflexivity x)) in Hle. simpl in Hle. rewrite Hall in Hle. simpl in Hle. now rewrite Hle.
- lia.
- - rewrite remove_In. intros [[_ Habs] | [Habs _]]; lia || now elim Habs.
+ - rewrite remove_In. intros [[_ Habs] | [Habs _]]; lia || now contradiction Habs.
+ setoid_rewrite Hall in Hrec. simpl in Hrec. apply Hrec. etransitivity; try eassumption. apply add_subset.
* intros. rewrite exists_empty; trivial. intuition.
Qed.
@@ -3566,7 +3565,7 @@ Section MMultisetFacts.
- exists x. split.
++ rewrite add_In. left. split; lia || reflexivity.
++ rewrite not_In in Hm. rewrite add_same, Hm. simpl. now rewrite Hfxn.
- + intro Habs. elim Habs. intros x Hin. elim (In_empty Hin).
+ + intro Habs. contradiction Habs. intros x Hin. contradiction (In_empty Hin).
* intro Habs. destruct Hm as [x [Hin Hx]]. apply Habs in Hin. rewrite Hin in Hx. discriminate.
Qed.
@@ -3609,7 +3608,7 @@ Section MMultisetFacts.
+ destruct (for_all (fun (x : elt) (n : nat) => negb (f x n)) m) eqn:Hforall; trivial.
rewrite for_all_false_exists, exists_spec in Hforall; trivial.
destruct Hforall as [x [Hin Hfx]]. rewrite negb_involutive in Hfx.
- elim (@In_empty x). rewrite <- Hall, nfilter_In; auto.
+ contradiction (@In_empty x). rewrite <- Hall, nfilter_In; auto.
+ rewrite for_all_spec in Hall; trivial.
destruct (empty_or_In_dec (nfilter f m)) as [? | [x Hin]]; trivial.
rewrite nfilter_In in Hin; trivial. destruct Hin as [Hin Hfx]. apply Hall in Hin.
@@ -3701,7 +3700,7 @@ Ltac msetdec_step :=
| H : ?x = ?x |- _ => clear H
| H : ?x == ?x |- _ => clear H
| H : ?x = ?y |- _ => subst x || rewrite H in *
- | Hneq : ?x =/= ?x |- _ => now elim Hneq
+ | Hneq : ?x =/= ?x |- _ => now contradiction Hneq
| Heq : equiv ?x ?y |- _ => clear x Heq || rewrite Heq in *
| Heq : @equiv (multiset _) _ ?x ?y, Hin : context[?x] |- _ => rewrite Heq in Hin
| Heq : @equiv (multiset _) _ ?x ?y |- context[?x] => rewrite Heq
diff --git a/Util/MMultiset/MMultisetWMap.v b/Util/MMultiset/MMultisetWMap.v
index 4b0bf92ec8a13e3ef5e1e4a307a445f3bc05d5e9..7083449efa6d3f36cba751f79f88c95258f23e1a 100644
--- a/Util/MMultiset/MMultisetWMap.v
+++ b/Util/MMultiset/MMultisetWMap.v
@@ -149,9 +149,9 @@ Proof using .
intros x y n m l Hl Hinx Hiny Heq. induction Hl as [| [z p] l]. inversion_clear Hiny.
inversion_clear Hinx; inversion_clear Hiny.
- compute in H0, H1. destruct H0 as [H0 ?], H1 as [H1 ?]. now subst p m.
-- compute in H0. destruct H0 as [H0 ?]. subst p. elim H.
+- compute in H0. destruct H0 as [H0 ?]. subst p. contradiction H.
apply eq_pair_elt_weak_In with y m. now transitivity x. assumption.
-- compute in H1. destruct H1 as [H1 ?]. subst p. elim H.
+- compute in H1. destruct H1 as [H1 ?]. subst p. contradiction H.
apply eq_pair_elt_weak_In with x n. now transitivity y; auto. assumption.
- now apply IHHl.
Qed.
@@ -255,7 +255,7 @@ Lemma multiplicity_out : forall x m, m[x] = 0 <-> find x m = None.
Proof using .
simpl. unfold m_multiplicity. intros x m. split; intro Hm.
+ destruct (find x m) eqn:Hfind.
- - elim (lt_irrefl 0). rewrite <- Hm at 2. now apply Pos2Nat.is_pos.
+ - contradiction (lt_irrefl 0). rewrite <- Hm at 2. now apply Pos2Nat.is_pos.
- reflexivity.
+ now rewrite Hm.
Qed.
@@ -368,7 +368,7 @@ Proof using MapSpec. split.
specialize (Hs x). cbn in Hs. unfold m_multiplicity in Hs.
destruct (find x s1), (find x s2);
solve [ apply Pos2Nat.inj in Hs; subst; reflexivity
- | elim (lt_irrefl 0); rewrite Hs at 2 || rewrite <- Hs at 2; apply Pos2Nat.is_pos
+ | contradiction (lt_irrefl 0); rewrite Hs at 2 || rewrite <- Hs at 2; apply Pos2Nat.is_pos
| split; intro; discriminate ].
+ assumption.
Qed.
@@ -396,8 +396,8 @@ split; trivial.
unfold m_multiplicity in Habs. specialize (Habs x). simpl in Habs.
destruct (find x s) eqn:Hin1, (find x s') eqn:Hin2.
- f_equal. now apply Pos2Nat.inj.
- - elim (lt_irrefl 0). rewrite <- Habs at 2. now apply Pos2Nat.is_pos.
- - elim (lt_irrefl 0). rewrite Habs at 2. now apply Pos2Nat.is_pos.
+ - contradiction (lt_irrefl 0). rewrite <- Habs at 2. now apply Pos2Nat.is_pos.
+ - contradiction (lt_irrefl 0). rewrite Habs at 2. now apply Pos2Nat.is_pos.
- reflexivity.
* intros s s'. unfold subset. simpl.
cbn in His_empty_spec. rewrite His_empty_spec. clear His_empty_spec.
@@ -532,7 +532,7 @@ assert (Hs' : forall n, ~InA eq_key_elt (x, n) (FMapInterface.elements s)).
revert o. induction (FMapInterface.elements s); simpl; intros o Hin.
+ assumption.
+ apply IHl in Hin.
- - elim (Hs' (snd a)). left. split; simpl. now inversion Hin. reflexivity.
+ - contradiction (Hs' (snd a)). left. split; simpl. now inversion Hin. reflexivity.
- intros n Habs. apply (Hs' n). now right.
Qed.
@@ -590,7 +590,7 @@ induction (FMapInterface.elements s); simpl; intro s'; simpl in Hs.
-- clear. intros [] [] Hxy. now compute in *.
- inversion_clear Hdup. rewrite NoDupA_inj_map in H0; solve [ eassumption | autoclass | now intros [] [] ].
+ inversion_clear Hs.
- - elim Hneq. destruct H as [H1 H2]. split; trivial; [].
+ - contradiction Hneq. destruct H as [H1 H2]. split; trivial; [].
simpl in *. hnf in H2. cbn in H2. now rewrite H2, Pos2Nat.id.
- inversion_clear Hdup.
assert (Hxy : x =/= y) by (intro; eauto using eq_pair_elt_weak_In).
@@ -779,7 +779,7 @@ induction (FMapInterface.elements s); simpl; intros [s1 s2]; simpl in Hs.
- inversion_clear Hdup. rewrite NoDupA_inj_map in H0;
solve [ eassumption | autoclass | now intros [] [] ].
+ inversion_clear Hs.
- - elim Hneq. destruct H as [H1 H2]. split. assumption. hnf in *. simpl in *. now rewrite H2, Pos2Nat.id.
+ - contradiction Hneq. destruct H as [H1 H2]. split. assumption. hnf in *. simpl in *. now rewrite H2, Pos2Nat.id.
- inversion_clear Hdup.
assert (Hxy : x =/= y) by (intro; eauto using eq_pair_elt_weak_In).
rewrite IHl; try assumption. simpl. unfold npartition_fun.
@@ -853,7 +853,7 @@ induction (FMapInterface.elements s); simpl; intros [s1 s2]; simpl in Hs.
- inversion_clear Hdup. rewrite NoDupA_inj_map in H0;
solve [eassumption | autoclass | now intros [] [] ].
+ inversion_clear Hs.
- - elim Hneq. destruct H as [H1 H2]. split. assumption. hnf in *. simpl in *. now rewrite H2, Pos2Nat.id.
+ - contradiction Hneq. destruct H as [H1 H2]. split. assumption. hnf in *. simpl in *. now rewrite H2, Pos2Nat.id.
- inversion_clear Hdup.
assert (Hxy : x =/= y) by (intro; eauto using eq_pair_elt_weak_In).
rewrite IHl; try assumption. simpl.
diff --git a/Util/MMultiset/Preliminary.v b/Util/MMultiset/Preliminary.v
index 06b3973b8a77cf8f872be5526d48b47b166a9a06..c3bcee46b81abc03e50aadd081330fceece47f70 100644
--- a/Util/MMultiset/Preliminary.v
+++ b/Util/MMultiset/Preliminary.v
@@ -101,7 +101,7 @@ Lemma NoDupA_2 : forall x y, ~eqA x y -> NoDupA eqA (x :: y :: nil).
Proof using .
intros x y Hdiff. constructor.
intro Habs. inversion_clear Habs.
- now elim Hdiff.
+ now contradiction Hdiff.
inversion H.
apply NoDupA_singleton.
Qed.
@@ -152,7 +152,7 @@ Proof using .
intros x l Hin. induction l; simpl.
+ reflexivity.
+ destruct (eq_dec x a).
- - elim Hin. now left.
+ - contradiction Hin. now left.
- f_equal. apply IHl. intro Habs. apply Hin. now right.
Qed.
@@ -162,7 +162,7 @@ Proof using HeqA.
intros x y l Hxy. induction l. reflexivity.
simpl. destruct (eq_dec y a).
subst. rewrite IHl. split; intro H. now right. inversion_clear H.
- elim Hxy. now transitivity a.
+ contradiction Hxy. now transitivity a.
assumption.
split; intro H; inversion_clear H; (now left) || right; now rewrite IHl in *.
Qed.
@@ -174,7 +174,7 @@ Proof using HeqA.
intros Hsub x y l. induction l as [| a l].
* split; intro Habs. inversion Habs. destruct Habs as [Habs _]. inversion Habs.
* simpl. destruct (eq_dec y a) as [Heq | Hneq].
- + rewrite IHl. intuition. inversion_clear H2. apply Hsub in H0. now elim H3; transitivity a. assumption.
+ + rewrite IHl. intuition. inversion_clear H2. apply Hsub in H0. now contradiction H3; transitivity a. assumption.
+ split; intro Hin.
- inversion_clear Hin.
split. now left. rewrite H. intro. now apply Hneq.
@@ -190,7 +190,7 @@ Proof using HeqA. apply (removeA_InA_iff_strong eq_dec). reflexivity. Qed.
Lemma removeA_InA_weak eq_dec : forall x y l, InA eqA' x (@removeA A eqA eq_dec y l) -> InA eqA' x l.
Proof using .
intros x y l Hin. induction l; simpl in *.
-+ rewrite InA_nil in Hin. elim Hin.
++ rewrite InA_nil in Hin. contradiction Hin.
+ destruct (eq_dec y a) as [Heq | Heq].
- auto.
- inversion_clear Hin; auto.
@@ -205,8 +205,8 @@ intros x y Hxy l l' ?. subst l'. induction l; simpl.
+ reflexivity.
+ destruct (eq_dec x a) as [Heqx | Hneqx], (eq_dec y a) as [Heqy | Hneqy].
- apply IHl.
- - elim Hneqy. now rewrite <- Hxy.
- - elim Hneqx. now rewrite Hxy.
+ - contradiction Hneqy. now rewrite <- Hxy.
+ - contradiction Hneqx. now rewrite Hxy.
- f_equal. apply IHl.
Qed.
@@ -217,17 +217,17 @@ intros x y ? l1 l2 Hl. subst. induction Hl.
+ constructor.
+ simpl. destruct (eq_dec x xâ‚) as [Heqâ‚ | Hneqâ‚], (eq_dec y xâ‚‚) as [Heqâ‚‚ | Hneqâ‚‚].
- assumption.
- - elim Hneqâ‚‚. now rewrite <- H, Heqâ‚.
- - elim Hneqâ‚. now rewrite H, Heqâ‚‚.
+ - contradiction Hneqâ‚‚. now rewrite <- H, Heqâ‚.
+ - contradiction Hneqâ‚. now rewrite H, Heqâ‚‚.
- now apply PermutationA_cons.
+ simpl. destruct (eq_dec x x0), (eq_dec y y0), (eq_dec y x0), (eq_dec x y0);
- try (now elim n; rewrite H) || (now elim n; rewrite <- H).
+ try (now contradiction n; rewrite H) || (now contradiction n; rewrite <- H).
- now erewrite removeA_eq_compat.
- constructor. reflexivity. now erewrite removeA_eq_compat.
- - elim n0. now rewrite <- H.
+ - contradiction n0. now rewrite <- H.
- constructor. reflexivity. now erewrite removeA_eq_compat.
- - elim n1. now rewrite H.
- - elim n0. now rewrite <- H.
+ - contradiction n1. now rewrite H.
+ - contradiction n0. now rewrite <- H.
- etransitivity. constructor 3. repeat constructor; reflexivity || now erewrite removeA_eq_compat.
+ constructor 4 with (removeA eq_dec y lâ‚‚).
- assumption.
@@ -243,7 +243,7 @@ Qed.
Corollary removeA_inside_in eq_dec :
forall (x : A) l1 l2, @removeA A eqA eq_dec x (l1 ++ x :: l2) = removeA eq_dec x l1 ++ removeA eq_dec x l2.
-Proof using HeqA. intros x ? ?. rewrite removeA_app. simpl. destruct (eq_dec x x) as [| Hneq]; trivial. now elim Hneq. Qed.
+Proof using HeqA. intros x ? ?. rewrite removeA_app. simpl. destruct (eq_dec x x) as [| Hneq]; trivial. now contradiction Hneq. Qed.
Corollary removeA_inside_out eq_dec : forall (x y : A) l1 l2,
~eqA x y -> @removeA A eqA eq_dec x (l1 ++ y :: l2) = removeA eq_dec x l1 ++ y :: removeA eq_dec x l2.
@@ -538,7 +538,7 @@ Lemma inclA_cons_inv : forall x y l1 l2,
Proof using HeqA.
intros x y l1 l2 Hx Heq Hincl z Hin.
assert (Hin' : InA eqA z (x :: l1)) by now right. apply Hincl in Hin'.
-inversion_clear Hin'; trivial. elim Hx. now rewrite Heq, <- H.
+inversion_clear Hin'; trivial. contradiction Hx. now rewrite Heq, <- H.
Qed.
Lemma inclA_length : forall l1 l2, NoDupA eqA l1 -> inclA eqA l1 l2 -> length l1 <= length l2.
@@ -556,7 +556,7 @@ Lemma not_NoDupA : (forall x y, {eqA x y} + {~eqA x y} ) ->
Proof using HeqA.
intros eq_dec l. split; intro Hl.
+ induction l.
- elim Hl. now constructor.
+ contradiction Hl. now constructor.
destruct (InA_dec eq_dec a l) as [Hin | Hnin].
exists a. apply PermutationA_split in Hin. destruct Hin as [l' Hperm]. exists l'. now rewrite Hperm.
destruct IHl as [x [l' Hperm]].
@@ -740,7 +740,7 @@ Lemma le_neq_lt : forall m n : nat, n <= m -> n <> m -> n < m.
Proof using . intros n m Hle Hneq. now destruct (le_lt_or_eq _ _ Hle). Qed.
Lemma min_is_0 : forall n m, min n m = 0 <-> n = 0 \/ m = 0.
-Proof using . intros [| n] [| m]; intuition;discriminate. Qed.
+Proof using . intros [| n] [| m]; intuition. Qed.
Lemma max_is_0 : forall n m, max n m = 0 <-> n = 0 /\ m = 0.
Proof using . intros [| n] [| m]; intuition; discriminate. Qed.
diff --git a/Util/NumberComplements.v b/Util/NumberComplements.v
index f3dcdac6385853501d1fb9fd929acf1a3406b846..d9666fcdcf132aefe4a979b5df55fdc19d679566 100644
--- a/Util/NumberComplements.v
+++ b/Util/NumberComplements.v
@@ -105,7 +105,7 @@ Proof.
intros k r r'.
destruct (Rdec_bool (k + r) (k + r')) eqn:Heq1, (Rdec_bool r r') eqn:Heq2; trivial;
rewrite ?Rdec_bool_true_iff, ?Rdec_bool_false_iff in *.
-- elim Heq2. eapply Rplus_eq_reg_l; eassumption.
+- contradiction Heq2. eapply Rplus_eq_reg_l; eassumption.
- subst. auto.
Qed.
@@ -115,7 +115,7 @@ intros k r r' Hk.
destruct (Rdec_bool r r') eqn:Heq1, (Rdec_bool (k * r) (k * r')) eqn:Heq2; trivial;
rewrite ?Rdec_bool_true_iff, ?Rdec_bool_false_iff in *.
- subst. auto.
-- elim Heq1. eapply Rmult_eq_reg_l; eassumption.
+- contradiction Heq1. eapply Rmult_eq_reg_l; eassumption.
Qed.
Corollary Rdec_bool_plus_r : forall k r r', Rdec_bool (r + k) (r' + k) = Rdec_bool r r'.
@@ -319,6 +319,11 @@ Proof using .
apply lt_O_minus_lt. rewrite <- H. apply lt_minus_O_lt. all: exact Hlt.
Qed.
+Lemma add_mul_lt : ∀ a b c d : nat, a < d -> b < c -> a + b * d < c * d.
+Proof using .
+ intros * a_lt_d b_lt_c. apply (Mult.mult_le_compat_r _ _ d) in b_lt_c. lia.
+Qed.
+
Open Scope Z.
Instance Z_EqDec : @EqDec Z _ := Z.eq_dec.