Change logical project name to "BelGames"

pPomCo · Oct 26, 2023 · 56131df · 56131df
1 parent 77195fd
commit 56131df
Show file tree

Hide file tree

Showing 16 changed files with 28 additions and 32 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -1,4 +1,4 @@
--R theories decision
+-R theories BelGames
 
 # utils
 theories/lib/ssrnum.v

diff --git a/hb_graphs/capacity.v b/hb_graphs/capacity.v
@@ -1,5 +1,5 @@
 From HB Require Import structures.
 
-From decision Require Import capacity.
+From BelGames Require Import capacity.
 
 HB.graph "capacity.dot".
diff --git a/hb_graphs/massfun.v b/hb_graphs/massfun.v
@@ -1,5 +1,5 @@
 From HB Require Import structures.
 
-From decision Require Import massfun.
+From BelGames Require Import massfun.
 
 HB.graph "massfun.dot".
diff --git a/theories/HRtransform.v b/theories/HRtransform.v
@@ -14,8 +14,8 @@ Unset Printing Implicit Defensive.
 Import GRing GRing.Theory.
 Import Num.Theory.
 
-From decision Require Import fintype finset ssrnum.
-From decision Require Import massfun decision games.
+From BelGames Require Import fintype finset ssrnum.
+From BelGames Require Import massfun decision games.
 
 Local Open Scope ring_scope.
 
@@ -481,6 +481,7 @@ Section HowsonRosenthal.
 
 End HowsonRosenthal.
 
+From HB Require Import structures.
 
 Section HRTBMWeakConditioningLocalGames.
 
@@ -491,8 +492,6 @@ Section HRTBMWeakConditioningLocalGames.
 
   Notation Tn := {ffun forall i, T i}.
 
-  From HB Require Import structures.
-
   Notation m_example := [ffun X : {set Tn} => if X == setT then 1 else 0:R].
 
   Lemma HRTBM_Weak_example_massfun0 :

diff --git a/theories/capacity.v b/theories/capacity.v
@@ -28,7 +28,7 @@ Unset Printing Implicit Defensive.
 Import GRing GRing.Theory.
 Import Num.Theory.
 
-From decision Require Import fintype finset minmax setfun massfun.
+From BelGames Require Import fintype finset minmax setfun massfun.
 
 Import Order Order.POrderTheory Order.TotalTheory.
 

diff --git a/theories/conditioning.v b/theories/conditioning.v
@@ -22,8 +22,8 @@ Unset Printing Implicit Defensive.
 Import GRing GRing.Theory.
 Import Num.Theory.
 
-From decision Require Import fintype finset setfun ssrnum order minmax.
-From decision Require Import massfun capacity.
+From BelGames Require Import fintype finset setfun ssrnum order minmax.
+From BelGames Require Import massfun capacity.
 
 
 

diff --git a/theories/decision.v b/theories/decision.v
@@ -19,8 +19,8 @@ Import Num.Theory.
 
 Open Scope ring_scope.
 
-From decision Require Import fintype finset setfun ssrnum order minmax.
-From decision Require Import massfun.
+From BelGames Require Import fintype finset setfun ssrnum order minmax.
+From BelGames Require Import massfun.
 
 Section Capacity.
 

diff --git a/theories/drule.v b/theories/drule.v
@@ -27,8 +27,8 @@ Import GRing GRing.Theory.
 Import Order Order.TotalTheory Order.POrderTheory.
 
 (* Local libraries *)
-From decision Require Import minmax fintype finset ssrnum setfun.
-From decision Require Import massfun capacity.
+From BelGames Require Import minmax fintype finset ssrnum setfun.
+From BelGames Require Import massfun capacity.
 
 
 

diff --git a/theories/games.v b/theories/games.v
@@ -22,8 +22,8 @@ Import GRing GRing.Theory.
 Import Num.Theory.
 
 
-From decision Require Import fintype finset ssrnum.
-From decision Require Import massfun drule decision.
+From BelGames Require Import fintype finset ssrnum.
+From BelGames Require Import massfun drule decision.
 
 Local Open Scope ring_scope.
 

diff --git a/theories/games2.v b/theories/games2.v
@@ -24,8 +24,8 @@ Import GRing GRing.Theory.
 Import Num.Theory.
 
 
-From decision Require Import fintype finset ssrnum.
-From decision Require Import setfun massfun capacity conditioning drule.
+From BelGames Require Import fintype finset ssrnum.
+From BelGames Require Import setfun massfun capacity drule.
 
 Local Open Scope order_scope.
 

diff --git a/theories/lib/finset.v b/theories/lib/finset.v
@@ -40,10 +40,6 @@ Unset Printing Implicit Defensive.
 Import GRing GRing.Theory.
 Import Num.Theory.
 
-From decision Require Import fintype.
-
-(* Local Open Scope ring_scope. *)
-
 
 
 (** Pick lemmas **)

diff --git a/theories/lib/minmax.v b/theories/lib/minmax.v
@@ -21,8 +21,7 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 
-From decision Require Import finset order.
-
+From BelGames Require Import finset order.
 
 
 

diff --git a/theories/lib/order.v b/theories/lib/order.v
@@ -12,7 +12,7 @@ From mathcomp Require Import finset order.
 Open Scope order_scope.
 Import Order Order.POrderTheory Order.TotalTheory.
 
-From decision Require Import fintype finset.
+From BelGames Require Import finset.
 
 
 

diff --git a/theories/lib/ssrnum.v b/theories/lib/ssrnum.v
@@ -55,7 +55,7 @@ Section NumLemmas.
   move=>H ; apply big_ind=>// ; exact: addr_ge0.
   Qed.
 
-  #[deprecated(since="decision.2.0", note="Use Num.Theory.sumr_ge0")]
+  #[deprecated(since="belgames.2.0", note="Use Num.Theory.sumr_ge0")]
   Notation sum_ge0 := deprecated_sum_ge0.
 
   Lemma sumr_le [I : Type] (r : seq I) (P : pred I) (F G : I -> R) :
@@ -83,7 +83,9 @@ Section NumLemmas.
     rewrite (bigD1 t) //= in Hsum.
     have Hge0' t' : P t' && (t' != t) -> 0 <= f t' by move=>/andP [Ht' _] ; exact: Hge0.
     have Hgt0 : f t > 0 by rewrite lt0r Hge0 // Hcontra.
-    have := addr_gte0 Hgt0 (sum_ge0 _ _ Hge0').
+    have Hsum_ge0 : 0 <= \sum_(t0 | P t0 && (t0 != t)) f t0
+      by apply:sumr_ge0.
+    have := addr_gte0 Hgt0 Hsum_ge0.
     by rewrite Hsum lt0r eqxx andFb.
   - by rewrite (eq_bigr (fun=>0)) // big1.
   Qed.
@@ -93,7 +95,7 @@ Section NumLemmas.
     (forall t, P t -> f t >= 0) -> \sum_(t | P t) f t != 0 -> exists t : T, P t && (f t > 0).
   Proof.
   move=>Hge0 Hsum.
-  have Hsum2 : \sum_(t | P t) f t > 0. by rewrite lt0r Hsum sum_ge0 //.
+  have Hsum2 : \sum_(t | P t) f t > 0. by rewrite lt0r Hsum sumr_ge0 //.
   have Hex : exists t : T, ~~ ~~ (P t && (f t != 0)).
   apply/forallPn/negP=>/forallP Hcontra.
   have Hcontra2 : \sum_(t | P t) f t = 0. apply sum_ge0_eq0E=>// t Ht.

diff --git a/theories/massfun.v b/theories/massfun.v
@@ -29,7 +29,7 @@ Unset Printing Implicit Defensive.
 Import GRing GRing.Theory.
 Import Num.Theory.
 
-From decision Require Import fintype finset order minmax setfun.
+From BelGames Require Import fintype finset order minmax setfun.
 
 Import Order Order.POrderTheory Order.TotalTheory.
 

diff --git a/theories/setfun.v b/theories/setfun.v
@@ -20,9 +20,9 @@ Unset Printing Implicit Defensive.
 Import GRing GRing.Theory.
 Import Num.Theory.
 
-From decision Require Import fintype.
-From decision Require Import finset.
-From decision Require Import minmax.
+From BelGames Require Import fintype.
+From BelGames Require Import finset.
+From BelGames Require Import minmax.
 
 Import Order Order.POrderTheory.
Original file line number	Diff line number	Diff line change
Expand Up		@@ -21,8 +21,7 @@ Unset Strict Implicit.
		Unset Printing Implicit Defensive.


		From decision Require Import finset order.

		From BelGames Require Import finset order.



Expand Down