cleaning up attributes + deprecations

case-studies/README.md

@@ -17,7 +17,6 @@ You can issue `make` in this directory to have Coq compile all the files.
 ### `case-studies/kathrin/coq/`
 This directory contains a subset of the case studies by Kathrin Stark from https://www.ps.uni-saarland.de/~kstark/thesis/
 Several metatheorems are proved, mostly about the simply typed lambda calculus and variations of System F.
-The files are adapted to be compatible with Coq 8.13.
 
 We generate the languages for the cases studies using Autosubst OCaml with mostly functional extensionality disabled (see the ./generate.sh script).
 Only Chapter6/variadic_fin.v uses functional extensionality because the language is defined with the codomain functor which needs the axiom.

case-studies/kathrin/coq/ARS.v

@@ -6,6 +6,7 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Require Import Coq.Program.Equality.
 
+Declare Scope prop_scope.
 Delimit Scope prop_scope with PROP.
 Open Scope prop_scope.
 
@@ -29,7 +30,7 @@ Inductive Or {X} (R R': X -> X -> Prop) : X -> X -> Prop :=
 | Inl x y : R x y -> Or R R' x y
 | Inr x y : R' x y -> Or R R' x y.
 
-Hint Constructors Or.
+#[global] Hint Constructors Or : core.
 
 
 (** ** Reflexive, Transitive closure *)
@@ -43,8 +44,8 @@ Inductive star (x : T) : T -> Prop :=
 | starR : star x x
 | starSE y z : e x y -> star y z -> star x z.
 
-Hint Constructors star.
-Hint Resolve starR.
+Hint Constructors star : core.
+#[local] Hint Resolve starR : core.
 
 
 Lemma star1 x y : e x y -> star x y.
@@ -57,7 +58,7 @@ Proof.
 Qed.
 
 End Definitions.
-Hint Constructors star.
+#[global] Hint Constructors star : core.
 
 Arguments star_trans {T e} y {x z} A B.
 
@@ -81,7 +82,7 @@ Arguments star_hom {T1 T2} f e1 {e2} A x y B.
 Inductive plus {X} (R : X -> X -> Prop) : X -> X -> Prop :=
  | plusR s t u : R s t -> star R t u -> plus R s u.
 
-Hint Constructors plus star.
+#[global] Hint Constructors plus star : core.
 
 Lemma star_plus {X} (R: X -> X -> Prop) s t :
   star R s t -> star (plus R) s t.
@@ -95,12 +96,12 @@ Qed.
 Inductive sn T (e: Rel T)  : T -> Prop :=
 | SNI x: (forall y, e x y -> sn e y) -> sn e x.
 
-Hint Immediate SNI.
+#[global] Hint Immediate SNI : core.
 
 Definition morphism {T1 T2} (R1 : Rel T1) (R2 : Rel T2) (h : T1 -> T2) :=
   forall x y, R1 x y -> R2 (h x) (h y).
 
-Hint Unfold morphism.
+#[global] Hint Unfold morphism : core.
 
 (** Morphism lemma, due to Steven Schäfer. *)
 Fact sn_morphism {T1 T2} (R1 : Rel T1) (R2 : Rel T2) (h : T1 -> T2) x :
@@ -163,7 +164,7 @@ Definition confluent {X} (R: X -> X -> Prop) :=
 Definition terminating {X} (R : X -> X -> Prop) :=
   forall x, sn R x.
 
-Hint Unfold terminating.
+#[global] Hint Unfold terminating : core.
 
 Fact newman {X} (R : X -> X -> Prop) :
   terminating R -> locally_confluent R -> confluent R.
@@ -183,4 +184,4 @@ Proof.
   assert (exists w, (star R) y1' w /\ star R v w) as (w&H13&H14).
   { eapply (IH y1); eauto using star_trans. }
   exists w. eauto using star_trans.
-Qed.
+Qed.

case-studies/kathrin/coq/Chapter10/POPLMark1.v

@@ -47,12 +47,12 @@ Inductive sub {n} (Delta : ctx n) : ty n -> ty n -> Prop :=
     SUB Delta |- all A1 A2 <: all B1 B2
 where "'SUB' Delta |- A <: B" := (sub Delta A B).
 
-Hint Constructors sub.
+#[global] Hint Constructors sub : core.
 
 Require Import Setoid Morphisms.
 
 (* a.d. we prove this morphism for asimpl *)
-Instance sub_morphism {n}:
+#[global] Instance sub_morphism {n}:
   Proper (pointwise_relation _ eq ==> eq ==> eq ==> Basics.impl) (@sub n).
 Proof.
   intros Gamma Gamma' HGamma T T' -> t t' ->.
@@ -99,7 +99,7 @@ Definition transitivity_at {n} (B: ty n) := forall m Gamma (A : ty m) C  (xi: fi
   transitivity_at B ->
   SUB Gamma |- A <: B -> SUB Gamma |- B <: C -> SUB Gamma |- A <: C.
 Proof. intros H. specialize (H n Gamma A C id). now asimpl in H. Qed.
-Hint Resolve transitivity_proj.
+#[global] Hint Resolve transitivity_proj : core.
 
 Lemma transitivity_ren m n B (xi: fin m -> fin n) : transitivity_at B -> transitivity_at B⟨xi⟩.
 Proof. unfold transitivity_at. intros. apply H with (xi:=funcomp xi0 xi); asimpl in H0; asimpl in H1; eauto.
@@ -188,10 +188,10 @@ Inductive has_ty {m n} (Delta : ctx m) (Gamma : dctx  n m) : tm m n -> ty m -> P
     TY Delta;Gamma |- s : B
 where "'TY' Delta ; Gamma |- s : A" := (has_ty Delta Gamma s A).
 
-Hint Constructors has_ty.
+#[global] Hint Constructors has_ty : core.
 
 (* a.d. we prove this morphism for asimpl *)
-Instance has_ty_morphism {m n} :
+#[global] Instance has_ty_morphism {m n} :
   Proper (pointwise_relation _ eq ==> pointwise_relation _ eq ==> eq ==> eq ==> Basics.impl) (@has_ty m n).
 Proof.
   intros Delta Delta' HDelta Gamma Gamma' HGamma T T' -> t t' -> H.
@@ -229,7 +229,7 @@ Inductive eval {m n} : tm m n -> tm m n -> Prop :=
 where "'EV' s => t" := (eval s t).
 
 (* a.d. we prove this morphism for asimpl *)
-Instance eval_morphism {m n}:
+#[global] Instance eval_morphism {m n}:
   Proper (eq ==> eq ==> Basics.impl) (@eval m n).
 Proof.
   intros s s' -> t t' ->. unfold Basics.impl. trivial.

case-studies/kathrin/coq/Chapter10/POPLMark21.v

@@ -29,7 +29,7 @@ Inductive unique {X} : list (nat * X) -> Prop :=
 | unil : unique nil
 | ucons l x xs : unique xs -> (forall x, ~ In (l, x) xs) ->  unique (cons (l,x) xs).
 
-Hint Constructors unique.
+#[global] Hint Constructors unique : core.
 
 Lemma unique_map {X Y: Type} {f : X -> Y} (xs : list (nat * X)) :
   unique xs -> unique (map (prod_map (fun x => x) f) xs).
@@ -73,7 +73,7 @@ Proof.
   apply H in H0. destruct H0 as (?&?). exists (f x). rewrite in_map_iff. exists (l, x). eauto.
 Qed.
 
-Hint Resolve unique_map label_equiv_map.
+#[global] Hint Resolve unique_map label_equiv_map : core.
 
 Definition update {X} (ts : list (nat * X)) l x : list (nat * X) :=
   map (fun p => if (Nat.eqb (fst p) l) then (l, x) else p) ts.
@@ -125,7 +125,7 @@ Proof.
     + right. cbn. eauto.
 Qed.
 
-Hint Resolve unique_update natequiv_update.
+#[global] Hint Resolve unique_update natequiv_update : core.
 
 (** POPLMark 1B. *)
 Reserved Notation "'SUB' Delta |- A <: B" (at level 68, A at level 99, no associativity).
@@ -149,7 +149,7 @@ Inductive sub {n} (Delta : ctx n) : ty n -> ty n -> Prop :=
                        unique xs -> unique ys -> SUB Delta |- recty xs <: recty ys
 where "'SUB' Delta |- A <: B" := (sub Delta A B).
 
-Hint Constructors sub.
+#[global] Hint Constructors sub : core.
 
 Lemma sub_rec :  forall P : forall n : nat, ctx n -> ty n -> ty n -> Prop,
        (forall (n : nat) (Delta : ctx n) (A : ty n), P n Delta A top) ->
@@ -229,7 +229,7 @@ Lemma transitivity_proj n (Gamma: ctx n) A B C :
   SUB Gamma |- A <: B -> SUB Gamma |- B <: C -> SUB Gamma |- A <: C.
 Proof. intros H. specialize (H n Gamma A C id).  now asimpl in H. Qed.
 
-Hint Resolve transitivity_proj.
+#[local] Hint Resolve transitivity_proj : core.
 
 Lemma transitivity_ren m n B (xi: fin m -> fin n) : transitivity_at B -> transitivity_at B⟨xi⟩.
 Proof. unfold transitivity_at. intros. eapply H with (xi:=funcomp xi0 xi); asimpl in H0; asimpl in H1; eauto. Qed.
@@ -357,7 +357,7 @@ exists HT1.
 apply (f _ Delta _ _ HT1).
 Defined.
 
-Instance sub_morphism {n}:
+#[global] Instance sub_morphism {n}:
   Proper (pointwise_relation _ eq ==> eq ==> eq ==> Basics.impl) (@sub n).
 Proof.
   intros Gamma Gamma' HGamma T T' -> t t' ->.
@@ -423,7 +423,7 @@ Axiom pat_ty_ext : forall {m p} (pt: pat m) (T: ty m) (sigma sigma': fin p -> ty
 (* a.d. we need the following morphism.
  * To prove it we have to assume pat_ty_ext above
  *)
-Instance pat_ty_morphism {m p} :
+#[global] Instance pat_ty_morphism {m p} :
   Proper (eq ==> eq ==> pointwise_relation _ eq ==> Basics.impl) (@pat_ty m p).
 Proof.
   intros ? pt -> ? T -> sigma sigma' Hsigma Hpat.
@@ -779,4 +779,4 @@ Qed.
 End Pattern.
 
 (* a.d. now the only assumptions are the one for pat_ty and UIP (because of depind) *)
-Print Assumptions preservation.
+Print Assumptions preservation.

case-studies/kathrin/coq/Chapter10/POPLMark22.v

@@ -31,7 +31,7 @@ Inductive unique {X} : list (nat * X) -> Prop :=
 | unil : unique nil
 | ucons l x xs : unique xs -> (forall x, ~ In (l, x) xs) ->  unique (cons (l,x) xs).
 
-Hint Constructors unique.
+#[global] Hint Constructors unique : core.
 
 Lemma unique_map {X Y: Type} {f : X -> Y} (xs : list (nat * X)) :
   unique xs -> unique (map (prod_map (fun x => x) f) xs).
@@ -75,7 +75,7 @@ Proof.
   apply H in H0. destruct H0 as (?&?). exists (f x). rewrite in_map_iff. exists (l, x). eauto.
 Qed.
 
-Hint Resolve unique_map label_equiv_map.
+#[global] Hint Resolve unique_map label_equiv_map : core.
 
 Definition update {X} (ts : list (nat * X)) l x : list (nat * X) :=
   map (fun p => if (Nat.eqb (fst p) l) then (l, x) else p) ts.
@@ -127,7 +127,7 @@ Proof.
     + right. cbn. eauto.
 Qed.
 
-Hint Resolve unique_update natequiv_update.
+#[global] Hint Resolve unique_update natequiv_update : core.
 
 (** POPLMark 1B. *)
 Reserved Notation "'SUB' Delta |- A <: B" (at level 68, A at level 99, no associativity).
@@ -149,7 +149,7 @@ Inductive sub {n} (Delta : ctx n) : ty n -> ty n -> Prop :=
                        unique xs -> unique ys -> SUB Delta |- recty xs <: recty ys
 where "'SUB' Delta |- A <: B" := (sub Delta A B).
 
-Hint Constructors sub.
+#[global] Hint Constructors sub : core.
 
 
 (** Generated with Marcel's induction generation program. 
@@ -230,7 +230,7 @@ exists HT1.
 apply (f _ Delta _ _ HT1).
 Defined.
 
-Instance sub_morphism {n}:
+#[global] Instance sub_morphism {n}:
 Proper (pointwise_relation _ eq ==> eq ==> eq ==> Basics.impl) (@sub n).
 Proof.
 intros Gamma Gamma' HGamma T T' -> t t' ->.
@@ -343,7 +343,7 @@ Lemma transitivity_proj n (Gamma: ctx n) A B C :
   SUB Gamma |- A <: B -> SUB Gamma |- B <: C -> SUB Gamma |- A <: C.
 Proof. intros H. specialize (H n Gamma A C id).  now asimpl in H. Qed.
 
-Hint Resolve transitivity_proj.
+#[local] Hint Resolve transitivity_proj : core.
 
 Lemma transitivity_ren m n B (xi: fin m -> fin n) : transitivity_at B -> transitivity_at B⟨xi⟩.
 Proof. unfold transitivity_at. intros. eapply H with (xi:=funcomp xi0 xi); asimpl in H0; asimpl in H1; eauto. Qed.
@@ -428,7 +428,7 @@ Axiom pat_ty_ext : forall {m p} (pt: pat m) (T: ty m) (sigma sigma': fin p -> ty
 (* a.d. we need the following morphism.
  * To prove it we have to assume pat_ty_ext above
  *)
-Instance pat_ty_morphism {m p} :
+#[global] Instance pat_ty_morphism {m p} :
   Proper (eq ==> eq ==> pointwise_relation _ eq ==> Basics.impl) (@pat_ty m p).
 Proof.
   intros ? pt -> ? T -> sigma sigma' Hsigma Hpat.

case-studies/kathrin/coq/Chapter10/sysf_rest.v

@@ -19,23 +19,23 @@ Arguments abs {n_ty} {n_tm}.
 
 Arguments tabs {n_ty} {n_tm}.
 
-Instance Subst_ty { m_ty : nat } { n_ty : nat } : Subst1 ((fin) (m_ty) -> ty (n_ty)) (ty (m_ty)) (ty (n_ty)) := @subst_ty (m_ty) (n_ty) .
+#[global] Instance Subst_ty { m_ty : nat } { n_ty : nat } : Subst1 ((fin) (m_ty) -> ty (n_ty)) (ty (m_ty)) (ty (n_ty)) := @subst_ty (m_ty) (n_ty) .
 
-Instance Subst_tm { m_ty m_tm : nat } { n_ty n_tm : nat } : Subst2 ((fin) (m_ty) -> ty (n_ty)) ((fin) (m_tm) -> tm (n_ty) (n_tm)) (tm (m_ty) (m_tm)) (tm (n_ty) (n_tm)) := @subst_tm (m_ty) (m_tm) (n_ty) (n_tm) .
+#[global] Instance Subst_tm { m_ty m_tm : nat } { n_ty n_tm : nat } : Subst2 ((fin) (m_ty) -> ty (n_ty)) ((fin) (m_tm) -> tm (n_ty) (n_tm)) (tm (m_ty) (m_tm)) (tm (n_ty) (n_tm)) := @subst_tm (m_ty) (m_tm) (n_ty) (n_tm) .
 
-Instance Ren_ty { m_ty : nat } { n_ty : nat } : Ren1 ((fin) (m_ty) -> (fin) (n_ty)) (ty (m_ty)) (ty (n_ty)) := @ren_ty (m_ty) (n_ty) .
+#[global] Instance Ren_ty { m_ty : nat } { n_ty : nat } : Ren1 ((fin) (m_ty) -> (fin) (n_ty)) (ty (m_ty)) (ty (n_ty)) := @ren_ty (m_ty) (n_ty) .
 
-Instance Ren_tm { m_ty m_tm : nat } { n_ty n_tm : nat } : Ren2 ((fin) (m_ty) -> (fin) (n_ty)) ((fin) (m_tm) -> (fin) (n_tm)) (tm (m_ty) (m_tm)) (tm (n_ty) (n_tm)) := @ren_tm (m_ty) (m_tm) (n_ty) (n_tm) .
+#[global] Instance Ren_tm { m_ty m_tm : nat } { n_ty n_tm : nat } : Ren2 ((fin) (m_ty) -> (fin) (n_ty)) ((fin) (m_tm) -> (fin) (n_tm)) (tm (m_ty) (m_tm)) (tm (n_ty) (n_tm)) := @ren_tm (m_ty) (m_tm) (n_ty) (n_tm) .
 
-Instance VarInstance_ty { m_ty : nat } : Var ((fin) (m_ty)) (ty (m_ty)) := @var_ty (m_ty) .
+#[global] Instance VarInstance_ty { m_ty : nat } : Var ((fin) (m_ty)) (ty (m_ty)) := @var_ty (m_ty) .
 
 Notation "x '__ty'" := (var_ty x) (at level 5, format "x __ty") : subst_scope.
 
 Notation "x '__ty'" := (@ids (_) (_) VarInstance_ty x) (at level 5, only printing, format "x __ty") : subst_scope.
 
 Notation "'var'" := (var_ty) (only printing, at level 1) : subst_scope.
 
-Instance VarInstance_tm { m_ty m_tm : nat } : Var ((fin) (m_tm)) (tm (m_ty) (m_tm)) := @var_tm (m_ty) (m_tm) .
+#[global] Instance VarInstance_tm { m_ty m_tm : nat } : Var ((fin) (m_tm)) (tm (m_ty) (m_tm)) := @var_tm (m_ty) (m_tm) .
 
 Notation "x '__tm'" := (var_tm x) (at level 5, format "x __tm") : subst_scope.
 
@@ -53,19 +53,19 @@ Notation "↑__tm" := (up_tm) (only printing) : subst_scope.
 
 Notation "↑__ty" := (up_ty_ty) (only printing) : subst_scope.
 
-Instance Up_ty_ty { m : nat } { n_ty : nat } : Up_ty (_) (_) := @up_ty_ty (m) (n_ty) .
+#[global] Instance Up_ty_ty { m : nat } { n_ty : nat } : Up_ty (_) (_) := @up_ty_ty (m) (n_ty) .
 
 Notation "↑__ty" := (up_ty_tm) (only printing) : subst_scope.
 
-Instance Up_ty_tm { m : nat } { n_ty n_tm : nat } : Up_tm (_) (_) := @up_ty_tm (m) (n_ty) (n_tm) .
+#[global] Instance Up_ty_tm { m : nat } { n_ty n_tm : nat } : Up_tm (_) (_) := @up_ty_tm (m) (n_ty) (n_tm) .
 
 Notation "↑__tm" := (up_tm_ty) (only printing) : subst_scope.
 
-Instance Up_tm_ty { m : nat } { n_ty : nat } : Up_ty (_) (_) := @up_tm_ty (m) (n_ty) .
+#[global] Instance Up_tm_ty { m : nat } { n_ty : nat } : Up_ty (_) (_) := @up_tm_ty (m) (n_ty) .
 
 Notation "↑__tm" := (up_tm_tm) (only printing) : subst_scope.
 
-Instance Up_tm_tm { m : nat } { n_ty n_tm : nat } : Up_tm (_) (_) := @up_tm_tm (m) (n_ty) (n_tm) .
+#[global] Instance Up_tm_tm { m : nat } { n_ty n_tm : nat } : Up_tm (_) (_) := @up_tm_tm (m) (n_ty) (n_tm) .
 
 Notation "s [ sigmaty ]" := (subst_ty sigmaty s) (at level 7, left associativity, only printing) : subst_scope.
 

case-studies/kathrin/coq/Chapter9/equivalence.v

@@ -26,7 +26,7 @@ Inductive mwhr : tm -> tm -> Prop :=
  | mwhrR s : mwhr s s
  | mwhrS s t u : whr s t -> mwhr t u -> mwhr s u.
 
-Hint Constructors whr mwhr.
+#[global] Hint Constructors whr mwhr : core.
 
 Lemma mwhr_appL s s' t :
   mwhr s s' -> mwhr (app s t) (app s' t).
@@ -36,7 +36,7 @@ Lemma mwhr_trans s t u :
   mwhr s t -> mwhr t u ->  mwhr s u.
 Proof. induction 1; eauto. Qed.
 
- Hint Immediate mwhr_trans.
+#[global] Hint Immediate mwhr_trans : core.
 
 Lemma whr_ren xi M N :
   whr M  N -> whr (M⟨xi⟩) (N⟨xi⟩).

case-studies/kathrin/coq/Chapter9/reduction.v

@@ -7,7 +7,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 
 Ltac inv H := dependent destruction H.
-Hint Constructors star.
+#[global] Hint Constructors star : core.
 Import ScopedNotations.
 
 (** *** Single-step reduction *)
@@ -17,7 +17,7 @@ Inductive step {n} : tm n -> tm n -> Prop :=
 | step_appL s1 s2 t : step s1 s2 -> step (app s1 t) (app s2 t)
 | step_appR s t1 t2 : step t1 t2 -> step (app s t1) (app s t2).
 
-Hint Constructors step.
+#[global] Hint Constructors step : core.
 
 Lemma step_beta' n A b (t t': tm n):
   t' = b[t..] -> step (app (lam A b) t) t'.

case-studies/kathrin/coq/Chapter9/sn_raamsdonk.v

@@ -156,7 +156,7 @@ match goal with
 |[H: ids _ = ids _|- _] => inv H
 end.
 
-Hint Constructors SN SNe SNRed.
+#[global] Hint Constructors SN SNe SNRed : core.
 
 Lemma anti_rename:
   (forall n (M: tm n), SN M -> forall n' M' (R: fin n' -> fin n), M = ren_tm R M' -> SN M')

case-studies/kathrin/coq/Chapter9/variadic_preservation.v

@@ -7,7 +7,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 
 Ltac inv H := dependent destruction H.
-Hint Constructors star.
+#[global] Hint Constructors star : core.
 Import ScopedNotations.
 
 (** *** Single-step reduction *)
@@ -16,7 +16,7 @@ Inductive step {n} : tm n -> tm n -> Prop :=
 | step_abs  p b1 b2 : @step (p + n) b1 b2 -> step (lam p b1) (lam p b2)
 | step_appL p s1 s2 t : step s1 s2 -> step (app p s1 t) (app _ s2 t).
 
-Hint Constructors step.
+#[global] Hint Constructors step : core.
 
 Lemma step_beta' n p b (t: fin p -> tm n) t':
   t' = b[scons_p p t ids] -> step (app _ (lam p b) t) t'.