adapt to coq/coq#18729

andres-erbsen · Feb 28, 2024 · 0c074d8 · 0c074d8
1 parent f1bd5f3
commit 0c074d8
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 5 deletions.
diff --git a/src/FCF/HasDups.v b/src/FCF/HasDups.v
@@ -6,6 +6,7 @@ Set Implicit Arguments.
 
 Require Import FCF.FCF.
 Require Import FCF.CompFold.
+Require Import ZifyNat.
 Local Open Scope list_scope.
 
 Fixpoint hasDups (A : Set)(eqd : EqDec A)(ls : list A) :=
@@ -165,7 +166,7 @@ Section DupProb.
         (length ls / 2^eta + (length ls ^ 2) / 2 ^ eta)
           <=
         (S (length ls * 1 + length ls * S (length ls * 1)) / 2 ^ eta)
-              ).
+              ). {
 
     eapply leRat_trans.
     2:{
@@ -183,9 +184,10 @@ Section DupProb.
 
     eapply ratAdd_leRat_compat.
     eapply leRat_terms; lia.
-    eapply leRat_terms; intuition.
-    simpl.
+    eapply leRat_terms; intuition;
+    simpl;
     eapply Nat.mul_le_mono; intuition.
+    }
 
     eapply leRat_trans.
     2:{

diff --git a/src/FCF/RepeatCore.v b/src/FCF/RepeatCore.v
@@ -314,8 +314,9 @@ Section DistSingle_impl_Mult.
     comp_skip.
     comp_simp.
     comp_skip.
+    epose proof hybrid_replace_c2_equiv as HH.
     comp_skip.
-    eapply hybrid_replace_c2_equiv.
+    eapply HH.
     eapply RndNat_support_lt; intuition.
 
   Qed.
@@ -328,8 +329,9 @@ Section DistSingle_impl_Mult.
     comp_skip.
     comp_simp.
     comp_skip.
+    epose proof hybrid_replace_c1_equiv as HH.
     comp_skip.
-    eapply hybrid_replace_c1_equiv.
+    eapply HH.
     eapply RndNat_support_lt; intuition.
 
   Qed.

diff --git a/src/FCF/SemEquiv.v b/src/FCF/SemEquiv.v
@@ -14,6 +14,7 @@ Require Import FCF.StdNat.
 Require Import FCF.Fold.
 Require Import FCF.Limit.
 Require Import Permutation.
+Require Import ZifyNat.
 
 Local Open Scope rat_scope.
 Local Open Scope list_scope.