Update to 8.19 and the new autosubst

.github/workflows/build.yml

@@ -15,7 +15,7 @@ jobs:
     runs-on: ubuntu-latest
 
     env:
-      coq_version: '8.18'
+      coq_version: '8.19'
       fail-fast: true
 
     steps:

README.md

@@ -9,30 +9,28 @@ https://zenodo.org/records/11500966
 ## Building the syntax (optional)
 
 We build the syntax of our type theories using [Autosubst 2 OCaml].
-When we prepared this supplementary material there was no Coq 8.18 version for
-this package so we provide instead the generated file directly in this
-repository.
+We provide the generated files, but if you want to run generation again you can
+simply run `make autosubst` after having installed [Autosubst 2 OCaml] for
+Coq 8.19.
 
-In the event you would like to build the syntax files, you can checkout the
-`coq-8.13` branch of [Autosubst 2 OCaml] and run
-```
-dune build
-dune install
+Just run
+```sh
+opam install coq-autosubst-ocaml
 ```
+after you installed the other dependencies (see below).
 
-Once installed, you can run `make` in the `theories/autosubst` directory. It
-will generate `GAST.v`, `CCAST.v`, `unscoped.v` and `core.v`.
+It will generate `GAST.v`, `CCAST.v`, `unscoped.v` and `core.v`.
 
 ## Building the project
 
-We use Coq 8.18 and Equations 1.3.
+We use Coq 8.19 and Equations 1.3.
 You can get Coq and Equations using [opam] as follows:
 
 ```sh
 opam repo add coq-released https://coq.inria.fr/opam/released
 opam update
-opam pin add coq 8.18.0
-opam install coq-equations
+opam pin add coq 8.19.0
+opam install coq-equations coq-autosubst-ocaml
 ```
 
 Running `make` at the root of the project is enough to build everything.

opam

@@ -9,6 +9,7 @@ authors: [
 depends: [
   "coq" { >= "8.18" & < "8.20~" }
   "coq-equations" { >= "1.3" }
+  "coq-autosubst-ocaml"
 ]
 build: [
   [make]

theories/autosubst/AST_preamble

@@ -0,0 +1,5 @@
+From GhostTT.autosubst Require Import core unscoped.
+From GhostTT Require Import BasicAST.
+From Coq Require Import Setoid Morphisms Relation_Definitions.
+
+

theories/autosubst/CCAST.v

@@ -2495,28 +2495,28 @@ Instance Up_cterm_cterm : (Up_cterm _ _) := @up_cterm_cterm.
 Instance VarInstance_cterm : (Var _ _) := @cvar.
 
 Notation "[ sigma_cterm ]" := (subst_cterm sigma_cterm)
-  ( at level 1, left associativity, only printing) : fscope.
+( at level 1, left associativity, only printing)  : fscope.
 
 Notation "s [ sigma_cterm ]" := (subst_cterm sigma_cterm s)
-  ( at level 7, left associativity, only printing) : subst_scope.
+( at level 7, left associativity, only printing)  : subst_scope.
 
-Notation "↑__cterm" := up_cterm (only printing) : subst_scope.
+Notation "↑__cterm" := up_cterm (only printing)  : subst_scope.
 
-Notation "↑__cterm" := up_cterm_cterm (only printing) : subst_scope.
+Notation "↑__cterm" := up_cterm_cterm (only printing)  : subst_scope.
 
 Notation "⟨ xi_cterm ⟩" := (ren_cterm xi_cterm)
-  ( at level 1, left associativity, only printing) : fscope.
+( at level 1, left associativity, only printing)  : fscope.
 
 Notation "s ⟨ xi_cterm ⟩" := (ren_cterm xi_cterm s)
-  ( at level 7, left associativity, only printing) : subst_scope.
+( at level 7, left associativity, only printing)  : subst_scope.
 
-Notation "'var'" := cvar ( at level 1, only printing) : subst_scope.
+Notation "'var'" := cvar ( at level 1, only printing)  : subst_scope.
 
 Notation "x '__cterm'" := (@ids _ _ VarInstance_cterm x)
-  ( at level 5, format "x __cterm", only printing) : subst_scope.
+( at level 5, format "x __cterm", only printing)  : subst_scope.
 
-Notation "x '__cterm'" := (cvar x) ( at level 5, format "x __cterm") :
-  subst_scope.
+Notation "x '__cterm'" := (cvar x) ( at level 5, format "x __cterm")  :
+subst_scope.
 
 #[global]
 Instance subst_cterm_morphism :

theories/autosubst/GAST.v

@@ -1426,28 +1426,28 @@ Class Up_term X Y :=
 Instance VarInstance_term : (Var _ _) := @var.
 
 Notation "[ sigma_term ]" := (subst_term sigma_term)
-  ( at level 1, left associativity, only printing) : fscope.
+( at level 1, left associativity, only printing)  : fscope.
 
 Notation "s [ sigma_term ]" := (subst_term sigma_term s)
-  ( at level 7, left associativity, only printing) : subst_scope.
+( at level 7, left associativity, only printing)  : subst_scope.
 
-Notation "↑__term" := up_term (only printing) : subst_scope.
+Notation "↑__term" := up_term (only printing)  : subst_scope.
 
-Notation "↑__term" := up_term_term (only printing) : subst_scope.
+Notation "↑__term" := up_term_term (only printing)  : subst_scope.
 
 Notation "⟨ xi_term ⟩" := (ren_term xi_term)
-  ( at level 1, left associativity, only printing) : fscope.
+( at level 1, left associativity, only printing)  : fscope.
 
 Notation "s ⟨ xi_term ⟩" := (ren_term xi_term s)
-  ( at level 7, left associativity, only printing) : subst_scope.
+( at level 7, left associativity, only printing)  : subst_scope.
 
-Notation "'var'" := var ( at level 1, only printing) : subst_scope.
+Notation "'var'" := var ( at level 1, only printing)  : subst_scope.
 
 Notation "x '__term'" := (@ids _ _ VarInstance_term x)
-  ( at level 5, format "x __term", only printing) : subst_scope.
+( at level 5, format "x __term", only printing)  : subst_scope.
 
-Notation "x '__term'" := (var x) ( at level 5, format "x __term") :
-  subst_scope.
+Notation "x '__term'" := (var x) ( at level 5, format "x __term")  :
+subst_scope.
 
 #[global]
 Instance subst_term_morphism :

theories/autosubst/Makefile

@@ -1,3 +1,3 @@
 syntax:
-	autosubst -f -s ucoq -v ge813 -allfv GAST.sig -o GAST.v
-	autosubst -f -s ucoq -v ge813 -allfv CCAST.sig -o CCAST.v
+	autosubst -f -s ucoq -v ge813 -allfv GAST.sig -o GAST.v -p AST_preamble
+	autosubst -f -s ucoq -v ge813 -allfv CCAST.sig -o CCAST.v -p AST_preamble

theories/autosubst/core.v

@@ -104,10 +104,7 @@ Proof.
   - reflexivity. 
 Defined.
 
-(* a.d. TODO hints outside of sections without explicit locality are deprecated. Is this even used in the first place?  *)
-(* but with 8.13.1 the attribute is forbidden. So what's the correct way to use this? *)
-(* #[ global ] *)
-Hint Rewrite in_map_iff : FunctorInstances.
+#[export] Hint Rewrite in_map_iff : FunctorInstances.
 
 (* Declaring the scopes that all our notations will live in *)
 Declare Scope fscope.
@@ -140,7 +137,7 @@ Proof.
   trivial.
 Qed.
 
-Instance funcomp_morphism {X Y Z} :
+#[export] Instance funcomp_morphism {X Y Z} :
   Proper (@pointwise_relation Y Z eq ==> @pointwise_relation X Y eq ==> @pointwise_relation X Z eq) funcomp.
 Proof.
   cbv - [funcomp].
@@ -149,7 +146,7 @@ Proof.
   reflexivity.
 Qed.
 
-Instance funcomp_morphism2 {X Y Z} :
+#[export] Instance funcomp_morphism2 {X Y Z} :
   Proper (@pointwise_relation Y Z eq ==> @pointwise_relation X Y eq ==> eq ==> eq) funcomp.
 Proof.
   intros g0 g1 Hg f0 f1 Hf ? x ->.

theories/autosubst/unscoped.v

@@ -7,7 +7,7 @@ Version: December 11, 2019.
  I changed this library a bit to work better with my generated code.
  1. I use nat directly instead of defining fin to be nat and using Some/None as S/O
  2. I removed the "s, sigma" notation for scons because it interacts with dependent function types "forall x, A"*)
-From GhostTT.autosubst Require Import core.
+Require Import core.
 Require Import Setoid Morphisms Relation_Definitions.
 
 Definition ap {X Y} (f : X -> Y) {x y : X} (p : x = y) : f x = f y :=
@@ -97,7 +97,7 @@ End SubstNotations.
 Class Var X Y :=
   ids : X -> Y.
 
-Instance idsRen : Var nat nat := id.
+#[export] Instance idsRen : Var nat nat := id.
 
 (** ** Proofs for the substitution primitives. *)
 
@@ -144,7 +144,7 @@ Lemma scons_comp' (T: Type) {U} (s: T) (sigma: nat -> T) (tau: T -> U) :
 Proof. intros x. destruct x; reflexivity. Qed.
 
 (* Morphism for Setoid Rewriting. The only morphism that can be defined statically. *)
-Instance scons_morphism {X: Type} :
+#[export] Instance scons_morphism {X: Type} :
   Proper (eq ==> pointwise_relation _ eq ==> pointwise_relation _ eq) (@scons X).
 Proof.
   intros ? t -> sigma tau H.
@@ -153,7 +153,7 @@ Proof.
   apply H.
 Qed.
 
-Instance scons_morphism2 {X: Type} :
+#[export] Instance scons_morphism2 {X: Type} :
   Proper (eq ==> pointwise_relation _ eq ==> eq ==> eq) (@scons X).
 Proof.
   intros ? t -> sigma tau H ? x ->.
@@ -170,16 +170,16 @@ Module UnscopedNotations.
   Include RenNotations.
   Include SubstNotations.
   Include CombineNotations.
-
+  
   (* Notation "s , sigma" := (scons s sigma) (at level 60, format "s ,  sigma", right associativity) : subst_scope. *)
 
   Notation "s '..'" := (scons s ids) (at level 1, format "s ..") : subst_scope.
 
   Notation "↑" := (shift) : subst_scope.
 
-  #[ global ]
+  #[global]
   Open Scope fscope.
-  #[ global ]
+  #[global]
   Open Scope subst_scope.
 End UnscopedNotations.
 
@@ -210,4 +210,4 @@ Ltac fsimpl :=
          (* DONE had to put an underscore as the last argument to scons. This might be an argument against unfolding funcomp *)
          | [|- context[funcomp _ (scons _ _)]] => setoid_rewrite scons_comp'; eta_reduce
          | [|- context[scons var_zero shift]] => setoid_rewrite scons_eta_id'; eta_reduce
-                        end.
+                        end.