From 291f50057cfbb7c96e58ff11ca9b9f4778467ec1 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andres-github@andres.systems>
Date: Thu, 29 Feb 2024 09:01:21 -0800
Subject: [PATCH] adapt to coq/coq#18729 (#46)

* adapt to coq/coq#18729

* require coq 8.19
---
 .github/workflows/build.yml | 2 +-
 src/FCF/HasDups.v           | 8 +++++---
 src/FCF/RepeatCore.v        | 6 ++++--
 src/FCF/SemEquiv.v          | 1 +
 4 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index b770621..946b7ee 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -18,7 +18,7 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:dev'
-          - 'coqorg/coq:8.17'
+          - 'coqorg/coq:8.19'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2
diff --git a/src/FCF/HasDups.v b/src/FCF/HasDups.v
index 9d5886a..ae62a45 100644
--- 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
index 08f6c94..09cf026 100644
--- 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
index 78401c0..895a1b3 100644
--- 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.