From 90bb71575cd52840d5cd2606b4f335e4b564d016 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 26 Feb 2025 13:57:13 +0100
Subject: [PATCH] strings: inline proof of compare_ok on > 8.20

---
 .github/workflows/ci.yml            |  2 --
 theories/core/PrimStringAxioms.v.in | 35 +++++++++++++++++++++++++++--
 2 files changed, 33 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 190fcb66e..7fc88232f 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -28,8 +28,6 @@ jobs:
           opam_file: 'rocq-elpi.opam'
           custom_image: ${{ matrix.image }}
           after_script: |
-            ls -l
-            id
             sudo chmod -R a+w .
             make all-examples
             make all-tests
diff --git a/theories/core/PrimStringAxioms.v.in b/theories/core/PrimStringAxioms.v.in
index a7f6ab8a4..5e67feddd 100644
--- a/theories/core/PrimStringAxioms.v.in
+++ b/theories/core/PrimStringAxioms.v.in
@@ -1,3 +1,34 @@
 #[only="8.20"] From Coq Require Export PrimStringAxioms PString.
-#[skip="8.20"] From Corelib Require Export PrimStringAxioms PString.
-Definition compare_ok := compare_eq.
\ No newline at end of file
+#[only="8.20"] Definition compare_ok := compare_eq.
+
+#[skip="8.20] From Corelib Require Import ssreflect ssrbool Uint63Axioms PrimStringAxioms.
+#[skip="8.20] Lemma compare_refl (s : string) : compare s s = Eq.
+#[skip="8.20] Proof.
+#[skip="8.20]   rewrite PrimStringAxioms.compare_spec.
+#[skip="8.20]   elim: (to_list s) => //= x xs ->.
+#[skip="8.20]   rewrite Uint63Axioms.compare_def_spec /compare_def eqb_refl.
+#[skip="8.20]   suff: ltb x x = false by move->.
+#[skip="8.20]   have [+ _] := ltb_spec x x.
+#[skip="8.20]   by case: ltb => // /(_ isT); case: (to_Z x) => //=; elim.
+#[skip="8.20] Qed.
+#[skip="8.20] Lemma to_list_inj (s1 s2 : string) :
+#[skip="8.20]   to_list s1 = to_list s2 -> s1 = s2.
+#[skip="8.20] Proof.
+#[skip="8.20]   intros H. rewrite -(of_to_list s1) -(of_to_list s2) H.
+#[skip="8.20]   reflexivity.
+#[skip="8.20] Qed.
+#[skip="8.20] Lemma compare_eq_correct (s1 s2 : string) :
+#[skip="8.20]   compare s1 s2 = Eq -> s1 = s2.
+#[skip="8.20] Proof.
+#[skip="8.20]   move=> E; rewrite -[s1]of_to_list -[s2]of_to_list; congr (of_list _).
+#[skip="8.20]   move: E; rewrite compare_spec.
+#[skip="8.20]   elim: (to_list s1) (to_list s2) => [[]//|x xs IH [|y ys] //=].
+#[skip="8.20]   rewrite Uint63Axioms.compare_def_spec /compare_def.
+#[skip="8.20]   move: (eqb_correct x y); case: eqb => [/(_ isT)->|_].
+#[skip="8.20]     suff: ltb y y = false by move=> -> /IH ->.
+#[skip="8.20]     have [+ _] := ltb_spec y y.
+#[skip="8.20]     by case: ltb => // /(_ isT); case: (to_Z y) => //=; elim.
+#[skip="8.20]   by case: ltb.
+#[skip="8.20] Qed.
+#[skip="8.20] Lemma compare_ok (s1 s2 : string) : compare s1 s2 = Eq <-> s1 = s2.
+#[skip="8.20] Proof. split; [apply compare_eq_correct|intros []; apply compare_refl]. Qed.