Merge pull request #119 from coq-community/withLibHyps

With lib hyps

.github/workflows/docker-action.yml

@@ -16,6 +16,7 @@ jobs:
       matrix:
         image:
           - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.15'
           - 'mathcomp/mathcomp:1.13.0-coq-8.14'
           - 'mathcomp/mathcomp:1.13.0-coq-8.13'
           - 'mathcomp/mathcomp:1.12.0-coq-8.14'

.nix/coq-overlays/hydra-battles-single/default.nix

@@ -1,5 +1,5 @@
 { lib, mkCoqDerivation, coq, version ? null
-, equations, gaia, mathcomp-ssreflect, mathcomp-algebra, mathcomp-zify, paramcoq
+, equations, gaia, LibHyps, mathcomp-ssreflect, mathcomp-algebra, mathcomp-zify, paramcoq
 , python3Packages, serapi, texlive, withMovies ? true, withTex ? true }:
 
 with lib; mkCoqDerivation rec {
@@ -45,6 +45,7 @@ with lib; mkCoqDerivation rec {
   propagatedBuildInputs = [
     equations
     gaia
+    LibHyps
     mathcomp-ssreflect
     mathcomp-algebra
     mathcomp-zify

.nix/coq-overlays/hydra-battles/default.nix

@@ -0,0 +1,35 @@
+{ lib, mkCoqDerivation, coq, equations, LibHyps, version ? null }:
+with lib;
+
+mkCoqDerivation {
+  pname = "hydra-battles";
+  owner = "coq-community";
+
+  release."0.4".sha256 = "1f7pc4w3kir4c9p0fjx5l77401bx12y72nmqxrqs3qqd3iynvqlp";
+  release."0.5".sha256 = "121pcbn6v59l0c165ha9n00whbddpy11npx2y9cn7g879sfk2nqk";
+  releaseRev = (v: "v${v}");
+
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.13" "8.14"; out = "0.5"; }
+    { case = range "8.11" "8.12"; out = "0.4"; }
+  ] null;
+
+  propagatedBuildInputs = [ equations LibHyps ];
+
+  useDune2 = true;
+
+  meta = {
+    description = "Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq";
+    longDescription = ''
+      An exploration of some properties of Kirby and Paris' hydra
+      battles, with the help of the Coq Proof assistant. This
+      development includes the study of several representations of
+      ordinal numbers, and a part of the so-called Ketonen and Solovay
+      machinery (combinatorial properties of epsilon0).
+    '';
+    maintainers = with maintainers; [ siraben Zimmi48 ];
+    license = licenses.mit;
+    platforms = platforms.unix;
+  };
+}

.nix/nixpkgs.nix

@@ -0,0 +1,4 @@
+fetchTarball {
+         url = https://github.com/Zimmi48/nixpkgs/archive/c9c002d30a165fe0ecfec348de66bbe910ac1a57.tar.gz;
+         sha256 = "05mx4mmw0px0sylal287clpj3s6gm2qy0djjaxxm71s06y2j5fv6";
+       }

README.md

@@ -65,6 +65,7 @@ in the proceedings of [JFLA 2022](http://jfla.inria.fr/jfla2022.html).
   - [MathComp Algebra](https://github.com/math-comp/math-comp)
   - [Gaia](https://github.com/coq-community/gaia) 1.12 or later
   - [Mczify](https://github.com/math-comp/mczify)
+  - [LibHyps](https://github.com/Matafou/LibHyps)
 - Coq namespaces: `hydras`, `additions`, `gaia_hydras`
 - Related publication(s):
   - [Hydras & Co.: Formalized mathematics in Coq for inspiration and entertainment](https://hal.archives-ouvertes.fr/hal-03404668) 

_CoqProject

@@ -171,4 +171,10 @@ theories/gaia/T1Bridge.v
 theories/gaia/GaiaToHydra.v
 theories/gaia/nfwfgaia.v
 theories/gaia/GCanon.v
+
+
+theories/ordinals/Prelude/MoreLibHyps.v
+theories/ordinals/Prelude/LibHyps_Experiments.v
+
 theories/gaia/GF_alpha.v
+

coq-addition-chains.opam

@@ -17,9 +17,9 @@ correctness."""
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "2.5"}
-  "coq" {(>= "8.13" & < "8.15~") | (= "dev")}
+  "coq" {(>= "8.13" & < "8.16~") | (= "dev")}
   "coq-paramcoq" {(>= "1.1.3" & < "1.2~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "1.12.0" & < "1.14~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "1.12.0" & < "1.15~") | (= "dev")}
   "coq-mathcomp-algebra"
 ]
 

coq-gaia-hydras.opam

@@ -16,11 +16,11 @@ similar concepts in the two projects."""
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "2.5"}
-  "coq" {(>= "8.13" & < "8.15~") | (= "dev")}
+  "coq" {(>= "8.13" & < "8.16~") | (= "dev")}
   "coq-hydra-battles" {= version}
-  "coq-mathcomp-ssreflect" {(>= "1.12.0" & < "1.14~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "1.12.0" & < "1.15~") | (= "dev")}
   "coq-mathcomp-zify"
-  "coq-gaia" {(>= "1.12" & < "1.14~") | (= "dev")}
+  "coq-gaia" {(>= "1.12" & < "1.15~") | (= "dev")}
 ]
 
 tags: [

coq-hydra-battles.opam

@@ -18,8 +18,9 @@ properties of epsilon0)."""
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "2.5"}
-  "coq" {(>= "8.13" & < "8.15~") | (= "dev")}
+  "coq" {(>= "8.13" & < "8.16~") | (= "dev")}
   "coq-equations" {(>= "1.2" & < "1.4~") | (= "dev")}
+  "coq-libhyps"
 ]
 
 tags: [

meta.yml

@@ -104,11 +104,13 @@ license:
 
 supported_coq_versions:
   text: 8.13 or later
-  opam: '{(>= "8.13" & < "8.15~") | (= "dev")}'
+  opam: '{(>= "8.13" & < "8.16~") | (= "dev")}'
 
 tested_coq_opam_versions:
 - version: 'coq-dev'
   repo: 'mathcomp/mathcomp-dev'
+- version: '1.14.0-coq-8.15'
+  repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.14'
   repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.13'
@@ -131,7 +133,7 @@ dependencies:
     [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "1.12.0" & < "1.14~") | (= "dev")}'
+    version: '{(>= "1.12.0" & < "1.15~") | (= "dev")}'
   description: |-
     [MathComp SSReflect](https://github.com/math-comp/math-comp) 1.12 or later
 - opam:
@@ -140,13 +142,17 @@ dependencies:
     [MathComp Algebra](https://github.com/math-comp/math-comp)
 - opam:
     name: coq-gaia
-    version: '{(>= "1.12" & < "1.14~") | (= "dev")}'
+    version: '{(>= "1.12" & < "1.15~") | (= "dev")}'
   description: |-
     [Gaia](https://github.com/coq-community/gaia) 1.12 or later
 - opam:
     name: coq-mathcomp-zify
   description: |-
     [Mczify](https://github.com/math-comp/mczify)
+- opam:
+    name: coq-libhyps
+  description: |-
+    [LibHyps](https://github.com/Matafou/LibHyps)
 
 namespace: hydras
 

theories/gaia/T1Bridge.v

@@ -115,7 +115,7 @@ Qed.
 Lemma h2g_eq_iff (a b :hT1) :  h2g a = h2g b <-> a = b.
 (* end snippet h2gEqIff *)
 Proof. 
-    split.
+  split.
     -  rewrite  -(g2h_h2gK a) -(g2h_h2gK b) !h2g_g2hK  =>  // -> //.
     - move => -> //. 
 Qed.
@@ -149,7 +149,6 @@ Proof.
   by rewrite Href g2h_h2gK.
 Qed.
 
-
 Lemma refines2_R f f' :
   refines2 f f' ->
   forall y z: T1, f (g2h y) (g2h z) = g2h (f' y z).
@@ -160,6 +159,7 @@ Qed.
 
 (** Refinements of usual constants *)
 (* begin snippet constantRefs:: no-out *)
+
 Lemma zero_ref : refines0 hzero zero.
 Proof. by []. Qed.
 
@@ -456,9 +456,8 @@ Lemma nf_ref (a: hT1)  : hnfb a = T1nf (h2g a).
 (* end snippet nfRef *)
 Proof.
   elim: a => //.
-  - move => a IHa n b IHb; rewrite Epsilon0.T1.nf_b_cons_eq; simpl T1nf. 
-    rewrite IHa IHb;  change (phi0 (h2g a)) with (h2g (Epsilon0.T1.phi0 a)).
-    by rewrite andbA decide_hlt_rw.
+  - move => a IHa n b IHb; rewrite T1.nf_b_cons_eq; simpl T1nf. 
+    by rewrite IHa IHb [phi0 (h2g a)]/(h2g (T1.phi0 a)) andbA decide_hlt_rw.
 Qed.
 
 Lemma LT_ref : refinesRel  hLT  gLT.
@@ -468,39 +467,30 @@ Proof.
     + by rewrite  -nf_ref.
     + by apply lt_ref. 
     + by rewrite -nf_ref. 
-  -  case => H H0 H1; repeat  split. 
-     +  red; by rewrite nf_ref.
-     + by apply lt_ref. 
-     +  red; by rewrite nf_ref.
+  -  case => H H0 H1; repeat  split; red; rewrite ?nf_ref ?lt_ref => // ;
+            by apply lt_ref. 
 Qed. 
 
 
 Lemma LE_ref : refinesRel hLE gLE.
 Proof. 
   split. 
-  - case => a b.
-    split. 
-    rewrite -nf_ref => //.
-    case: b => c _.    
-    destruct c. 
-
-    apply T1ltW. 
-    rewrite - decide_hlt_rw => //.
-    red;  rewrite bool_decide_eq_true => //.
-    apply T1lenn. 
-    case b => _ H.
-    rewrite - nf_ref => //. 
-  - case.
-    rewrite /hLE; split. 
-    rewrite -nf_ref in p p1 => //.
-    split => //.
-    rewrite T1le_eqVlt in p0. move : p0 => /orP.
-    case => /eqP Heq; subst.  rewrite h2g_eq_iff in Heq; subst. 
-    right. 
-    left. 
-    rewrite -decide_hlt_rw in Heq => //.
-    move: Heq => /eqP H. rewrite bool_decide_eq_true in H => //.
-    rewrite -nf_ref in p1 => //.
+  - case => a b; split. 
+    + rewrite -nf_ref => //.
+    + case: b => c _; case :c => [y0 Hy0 |].
+      apply T1ltW. 
+      * rewrite - decide_hlt_rw => //.
+        red;  rewrite bool_decide_eq_true => //.
+      *  apply T1lenn. 
+    +  case b => _ ?; rewrite - nf_ref => //. 
+  - case; rewrite /hLE; repeat split => //.
+   +  rewrite -nf_ref in p p1 => //.
+   +  rewrite T1le_eqVlt in p0; move : p0 => /orP.
+      case => /eqP Heq; subst.
+      * rewrite h2g_eq_iff in Heq; subst; right. 
+      *    left; rewrite -decide_hlt_rw in Heq => //.
+           move: Heq => /eqP H;  rewrite bool_decide_eq_true in H => //.
+   + rewrite -nf_ref in p1 => //.
 Qed.