Removed dependency to coq-topology

README.md

@@ -27,9 +27,8 @@
 ## Building the Project
 
 ### Requirements
-* [Coq 8.15.1](https://coq.inria.fr)
+* [Coq 8.17.0](https://coq.inria.fr)
 * [Hahn library](https://github.com/vafeiadis/hahn) (`coq-hahn`)
-* [Coq formalization of Zorn's lemma included in "topology" package](https://github.com/coq-community/topology) (`coq-topology`)
 * [The Coq supplementary library w/ basic data types](https://github.com/snu-sf/promising-lib) (`coq-promising-lib`)
 
 ### Building Manually

configure

@@ -2,4 +2,4 @@
 opam repo add coq-released https://coq.inria.fr/opam/released
 opam remote add coq-promising-local -k git https://github.com/snu-sf/promising-opam-coq-archive
 opam remote add coq-weakmemory-local -k git https://github.com/weakmemory/local-coq-opam-archive
-opam install coq-hahn coq-promising-lib coq-topology
+opam install coq-hahn coq-promising-lib

opam

@@ -14,10 +14,9 @@ build: [
 install: [make "-f" "Makefile.coq" "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/imm"]
 depends: [
-  "coq" { (>= "8.15.1") | (= "dev") }
+  "coq" { (>= "8.17.0") | (= "dev") }
   "coq-promising-lib" { = "dev" }
   "coq-hahn" { >= "1.1" | (= "dev") }
-  "coq-topology" { >= "10.0.1" }
 ]
 url {
   git: "https://github.com/weakmemory/imm"

src/basic/AuxDef.v

@@ -1,11 +1,41 @@
 From hahn Require Import Hahn.
+Require Import Coq.Logic.ChoiceFacts.
 Require Import Classical.
 Require Import Lia.
 Require Import IndefiniteDescription.
 Require Import PropExtensionality.
-From ZornsLemma Require Classical_Wf. 
 Require Import Events.
 
+Lemma not_wf_inf_decr_enum {A: Type} (r: relation A)
+      (NWF: ~ well_founded r):
+  exists (f: nat -> A), forall i, r (f (i + 1)) (f i).
+Proof using.
+  unfold well_founded in NWF.
+  apply not_all_ex_not in NWF.
+  assert (forall n (NAC : ~ Acc r n),
+           { m | << MN : r m n >> /\
+                 << MAC : ~ Acc r m >>}) as ACD.
+  { ins. apply constructive_indefinite_description.
+    apply NNPP. intros HH. apply NAC.
+    constructor. intros y RY. apply NNPP. intros AR.
+    apply HH; eauto. }
+  remember (functional_choice_imp_functional_dependent_choice functional_choice)
+    as FCI.
+  clear HeqFCI. red in FCI.
+  set (B := { x : A | ~ Acc r x }).
+  set (R := fun x y : B => r (proj1_sig y) (proj1_sig x)).
+  destruct NWF as [a AAC].
+  edestruct (FCI B R) as [f [FF RF]].
+  { ins. destruct x.
+    destruct (ACD x n) as [m [MX AM]]. unnw.
+    subst R; ins. exists (exist _ m AM). ins. }
+  exists (fun n => proj1_sig (f n)).
+  ins. arewrite (i + 1 = 1 + i) by lia.
+  apply RF.
+Unshelve.
+red. econstructor. apply AAC.
+Qed.
+
 Lemma list_max_In (l: list nat) (NNIL: l <> nil):
   In (list_max l) l. 
 Proof using.
@@ -441,16 +471,6 @@ Lemma acyclic_transp {A: Type} (r: relation A)
   acyclic (transp r). 
 Proof using. red. rewrite <- transp_ct. vauto. Qed.   
 
-Lemma not_wf_inf_decr_enum {A: Type} (r: relation A)
-      (NWF: ~ well_founded r):
-  exists (f: nat -> A), forall i, r (f (i + 1)) (f i).
-Proof using.
-  contra DECR. destruct NWF.
-  apply Classical_Wf.DSP_implies_WF. red. apply not_ex_not_all. 
-  intros [f DECR']. destruct DECR. exists f.
-  ins. contra Nri. destruct DECR'. exists i. by rewrite <- PeanoNat.Nat.add_1_r. 
-Qed. 
-
 Lemma In_gt_list_max (l: list nat) (n: nat)
       (GT_MAX: n > list_max l):
   ~ In n l. 

src/hardware/PowerFairness.v

@@ -4,7 +4,6 @@
 (******************************************************************************)
 
 From hahn Require Import Hahn.
-From ZornsLemma Require Classical_Wf. 
 Require Import Events.
 Require Import Execution.
 Require Import Execution_eco.

src/lib/AuxRel.v

@@ -144,14 +144,14 @@ Proof using.
 Qed.
 
 (* TODO : rename *)
-Lemma seq_transp_sym : symmetric r -> ⦗ s ⦘ ⨾ r ⨾ ⦗ s' ⦘ ≡ (⦗ s' ⦘ ⨾ r ⨾ ⦗ s ⦘)⁻¹.
+Lemma seq_transp_sym (SYM : symmetric r) :
+  ⦗ s ⦘ ⨾ r ⨾ ⦗ s' ⦘ ≡ (⦗ s' ⦘ ⨾ r ⨾ ⦗ s ⦘)⁻¹.
 Proof using. 
   ins. 
   rewrite !transp_seq. 
   rewrite !seqA.
-  rewrite !transp_sym_equiv; auto. 
   rewrite !transp_eqv_rel. 
-  done.
+  rewrite !transp_sym_equiv; auto. 
 Qed.
 
 (******************************************************************************)