strings: inline proof of compare_ok on > 8.20

.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

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.
+#[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.