From c41b7dca92a3a3d2c4a7e9eb62f00675d099217c Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Fri, 12 Jul 2024 20:49:40 +0200 Subject: [PATCH] fix most deprecations in 8.19 and later --- examples/plain/Context.v | 13 +++++++------ examples/plain/POPLmark.v | 15 ++++++++------- examples/plain/Size.v | 2 +- examples/ssr/ARS.v | 17 +++++++++-------- examples/ssr/CR.v | 2 +- examples/ssr/POPLmark.v | 14 +++++++------- examples/ssr/SystemF_CBV.v | 8 ++++---- examples/ssr/SystemF_SN.v | 8 ++++---- examples/ssr/pred_CC_omega.v | 12 ++++++------ 9 files changed, 47 insertions(+), 44 deletions(-) diff --git a/examples/plain/Context.v b/examples/plain/Context.v index ec3be45..e8f77d0 100644 --- a/examples/plain/Context.v +++ b/examples/plain/Context.v @@ -67,12 +67,13 @@ Proof. - split. + autosubst. + autosubst. - - simpl. cutrewrite (A.[ren (+S (length Delta))] = - A.[ren(+length Delta)].[ren(+1)]); [idtac|autosubst]. + - simpl. + replace (A.[ren (+S (length Delta))]) with + (A.[ren(+length Delta)].[ren(+1)]); [idtac|autosubst]. split. - + econstructor. eapply IHDelta; eassumption. reflexivity. - + intros H. inv H. rewrite IHDelta. apply lift_inj in H5. - subst. eassumption. + + econstructor. eapply IHDelta; eassumption. reflexivity. + + intros H. inv H. rewrite IHDelta. apply lift_inj in H5. + subst. eassumption. Qed. Lemma atnd_steps' x Gamma Delta A : @@ -83,7 +84,7 @@ Proof. induction Delta; intros. - exists A. simpl in H. - rewrite plus_0_r in H. intuition autosubst. + rewrite Nat.add_0_r in H. intuition autosubst. - asimpl. simpl in *. rewrite plusnS in *. inv H. diff --git a/examples/plain/POPLmark.v b/examples/plain/POPLmark.v index 635ed4c..f35113b 100644 --- a/examples/plain/POPLmark.v +++ b/examples/plain/POPLmark.v @@ -192,7 +192,7 @@ Proof. * now rewrite ren_size_inv. * intros. change (B' :: Delta) with ((B' :: nil) ++ Delta). rewrite app_assoc. - cutrewrite (S (length Delta') = length (Delta' ++ B' :: nil)). + replace (S (length Delta')) with (length (Delta' ++ B' :: nil)). now apply atnd_steps. rewrite app_length. simpl. lia. * asimpl in IHsub. @@ -298,7 +298,8 @@ Lemma ty_weak_ty xi Delta1 Delta2 Gamma1 Gamma2 s s' A A': s' = s.|[ren xi] -> TY Delta2;Gamma2 |- s' : A'. Proof. - intros. subst. cutrewrite(s.|[ren xi] = s.|[ren xi].[ren id]). + intros. subst. + replace (s.|[ren xi]) with (s.|[ren xi].[ren id]). eapply ty_weak; eauto. now autosubst. Qed. @@ -319,8 +320,8 @@ Lemma ty_weak_ter xi Delta Gamma1 Gamma2 s A : TY Delta;Gamma2 |- s.[ren xi] : A. Proof. intros. - cutrewrite (s = s.|[ren id]). - cutrewrite (A = A.[ren id]). + replace s with (s.|[ren id]). + replace A with (A.[ren id]). eapply ty_weak; eauto; intros; asimpl; now eauto. autosubst. autosubst. Qed. @@ -415,8 +416,8 @@ Corollary ty_subst_term Delta Gamma1 Gamma2 s A sigma: TY Delta;Gamma2 |- s.[sigma] : A. Proof. intros. - cutrewrite(s = s.|[ids]);[idtac|autosubst]. - cutrewrite (A = A.[ids]);[idtac|autosubst]. + replace s with (s.|[ids]);[idtac|autosubst]. + replace A with (A.[ids]);[idtac|autosubst]. eapply ty_subst; eauto; intros. - asimpl; eauto using sub, sub_refl. - asimpl; eauto using sub, sub_refl. @@ -488,7 +489,7 @@ Proof. + pose proof (ty_inv_abs H0 H1) as [? [B' [? ?]]]. eapply ty_subst_term; eauto using ty. intros [|] ? ?; simpl in *; subst; eauto using ty. - - cutrewrite (s.|[B/] = s.|[B/].[ids]);[idtac|autosubst]. + - replace (s.|[B/]) with (s.|[B/].[ids]);[idtac|autosubst]. inv H_ty; [idtac | pose proof (ty_inv_tabs H1 H2) as [? [B' [? ?]]]]; (eapply ty_subst; eauto using ty; [ now intros ? ? H_atnd; inv H_atnd; asimpl; eauto using sub, sub_refl diff --git a/examples/plain/Size.v b/examples/plain/Size.v index f4e76ce..0a8669b 100644 --- a/examples/plain/Size.v +++ b/examples/plain/Size.v @@ -92,7 +92,7 @@ Arguments size_fact {A} x {P _}. Lemma size_app (A : Type) (size_A : Size A) l1 l2 : size (app l1 l2) = size l1 + size l2. -Proof. induction l1; simpl; intuition. Qed. +Proof. induction l1; simpl; intuition (auto with zarith). Qed. Global Hint Rewrite @size_app : size. Global Instance size_fact_app (A : Type) (size_A : Size A) l1 l2 : diff --git a/examples/ssr/ARS.v b/examples/ssr/ARS.v index 1c46a35..78efa14 100644 --- a/examples/ssr/ARS.v +++ b/examples/ssr/ARS.v @@ -7,6 +7,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Declare Scope prop_scope. Delimit Scope prop_scope with PROP. Open Scope prop_scope. @@ -41,7 +42,7 @@ Definition diamond := forall x y z, e x y -> e x z -> exists2 u, e y u & e z u. Definition confluent := forall x y z, star x y -> star x z -> joinable star y z. Definition CR := forall x y, conv x y -> joinable star x y. -Local Hint Resolve starR convR. +Local Hint Resolve starR convR : core. Lemma star1 x y : e x y -> star x y. Proof. exact: starSE. Qed. @@ -53,7 +54,7 @@ Lemma starES x y z : e x y -> star y z -> star x z. Proof. move/star1. exact: star_trans. Qed. Lemma star_conv x y : star x y -> conv x y. -Proof. elim=> //={y} y z _. exact: convSE. Qed. +Proof. elim=> //={} y z _. exact: convSE. Qed. Lemma conv1 x y : e x y -> conv x y. Proof. exact: convSE. Qed. @@ -71,7 +72,7 @@ Lemma convESi x y z : e y x -> conv y z -> conv x z. Proof. move/conv1i. exact: conv_trans. Qed. Lemma conv_sym x y : conv x y -> conv y x. -Proof. elim=> //={y} y z _ ih h; [exact: convESi ih|exact: convES ih]. Qed. +Proof. elim=> //={} y z _ ih h; [exact: convESi ih|exact: convES ih]. Qed. Lemma join_conv x y z : star x y -> star z y -> conv x z. Proof. @@ -82,9 +83,9 @@ Lemma confluent_cr : confluent <-> CR. Proof. split=> [h x y|h x y z /star_conv A /star_conv B]. - - elim=> [|{y} y z _ [u h1 h2] /star1 h3|{y} y z _ [u h1 h2] h3]. + - elim=> [|{} y z _ [u h1 h2] /star1 h3|{} y z _ [u h1 h2] h3]. + by exists x. - + case: (h y u z h2 h3) => v {h2 h3} h2 h3. + + case: (h y u z h2 h3) => v {h3} h2 h3. exists v => //. exact: star_trans h2. + exists u => //. exact: starES h2. - apply: h. apply: conv_trans B. exact: conv_sym. @@ -92,7 +93,7 @@ Qed. End Definitions. -Global Hint Resolve starR convR. +Global Hint Resolve starR convR : core. Arguments star_trans {T e} y {x z} A B. Arguments conv_trans {T e} y {x z} A B. @@ -193,7 +194,7 @@ Inductive sn x : Prop := Lemma sn_preimage (h : T -> T) x : (forall x y, e x y -> e (h x) (h y)) -> sn (h x) -> sn x. Proof. - move eqn:(h x) => v A B. elim: B h x A eqn => {v} v _ ih h x A eqn. + move eqn:(h x) => v A B. elim: B h x A eqn => {} v _ ih h x A eqn. apply: SNI => y /A. rewrite eqn => /ih; eauto. Qed. @@ -281,7 +282,7 @@ Qed. Lemma sn_wn x : sn e x -> wn e x. Proof. - elim=> {x} x _ ih. case (classical x) => [[y exy]|A]. + elim=> {} x _ ih. case (classical x) => [[y exy]|A]. - case: (ih _ exy) => z [A B]. exists z. split=> //. exact: starES A. - exists x. by split. Qed. diff --git a/examples/ssr/CR.v b/examples/ssr/CR.v index 7ac58f7..d6cbd27 100644 --- a/examples/ssr/CR.v +++ b/examples/ssr/CR.v @@ -88,7 +88,7 @@ Proof. move<-. exact: pstep_beta. Qed. Lemma pstep_refl s : pstep s s. Proof. elim: s; eauto using pstep. Qed. -Global Hint Resolve pstep_refl. +Global Hint Resolve pstep_refl : core. Lemma step_pstep s t : step s t -> pstep s t. Proof. elim; eauto using pstep. Qed. diff --git a/examples/ssr/POPLmark.v b/examples/ssr/POPLmark.v index f894cea..e716fca 100644 --- a/examples/ssr/POPLmark.v +++ b/examples/ssr/POPLmark.v @@ -66,14 +66,14 @@ where "'SUB' Gamma |- A <: B" := (sub Gamma A B). Lemma sub_refl Gamma A : SUB Gamma |- A <: A. Proof. elim: A Gamma; eauto using sub. Qed. -Global Hint Resolve sub_refl. +Global Hint Resolve sub_refl : core. Lemma sub_ren Gamma Delta xi A B : (forall x, x < size Gamma -> xi x < size Delta) -> (forall x, x < size Gamma -> Delta`_(xi x) = (Gamma`_x).[ren xi]) -> SUB Gamma |- A <: B -> SUB Delta |- A.[ren xi] <: B.[ren xi]. Proof. - move=> sub eqn ty. elim: ty Delta xi sub eqn => {Gamma A B} Gamma //=; + move=> sub eqn ty. elim: ty Delta xi sub eqn => {A B} Gamma //=; eauto using sub. - move=> x A lt _ ih Delta xi sub eqn. apply: sub_var_trans. exact: sub. rewrite eqn //. exact: ih. @@ -94,7 +94,7 @@ Lemma transitivity_proj Gamma A B C : transitivity_at B -> SUB Gamma |- A <: B -> SUB Gamma |- B <: C -> SUB Gamma |- A <: C. Proof. move=> /(_ Gamma A C id). autosubst. Qed. -Global Hint Resolve transitivity_proj. +Global Hint Resolve transitivity_proj : core. Lemma transitivity_ren B xi : transitivity_at B -> transitivity_at B.[ren xi]. Proof. move=> h Gamma A C zeta. asimpl. exact: h. Qed. @@ -153,7 +153,7 @@ Lemma sub_subst Gamma Delta A B sigma : (forall x, x < size Gamma -> SUB Delta |- sigma x <: (Gamma`_x).[sigma]) -> SUB Gamma |- A <: B -> SUB Delta |- A.[sigma] <: B.[sigma]. Proof with eauto using sub. - move=> h ty. elim: ty Delta sigma h => {Gamma A B} Gamma... + move=> h ty. elim: ty Delta sigma h => {A B} Gamma... - move=> x A lt _ ih Delta sigma h /=. apply: sub_trans (h _ lt) _. exact: ih. - move=> A1 A2 B1 B2 _ ih1 _ ih2 Delta sigma h /=. apply: sub_all... apply: ih2 => -[_|x /h/sub_weak]. apply: sub_var_trans => //. autosubst. @@ -247,7 +247,7 @@ Proof with eauto using ty. apply. move=> [_|x/h/sub_weak] /=. apply: sub_var_trans => //. autosubst. autosubst. - move=> Delta1 Gamma A B C s _ ih sub Delta2 sigma h. asimpl. - eapply ty_etapp. Focus 2. by eapply ih. autosubst. exact: sub_subst sub. + eapply ty_etapp. 2: { by eapply ih. } autosubst. exact: sub_subst sub. - move=> Delta1 Gamma A B s _ ih sub Delta2 sigma h. eapply ty_sub. by eapply ih. exact: sub_subst sub. Qed. @@ -354,7 +354,7 @@ Definition is_tabs s := if s is TAbs _ _ then true else false. Lemma canonical_arr' Delta Gamma s T A B : TY Delta;Gamma |- s : T -> SUB Delta |- T <: Arr A B -> value s -> is_abs s. Proof. - move=> ty. elim: ty A B => //={Delta Gamma s T} Delta Gamma A B s. + move=> ty. elim: ty A B => //= {Gamma s T} Delta Gamma A B s. - move=> ty _ A' B' sub. by inv sub. - move=> _ ih /sub_trans h A' B' /h. exact: ih. Qed. @@ -368,7 +368,7 @@ Qed. Lemma canonical_all' Delta Gamma s T A B : TY Delta;Gamma |- s : T -> SUB Delta |- T <: All A B -> value s -> is_tabs s. Proof. - move=> ty. elim: ty A B => //={Delta Gamma s T} Delta Gamma A B s. + move=> ty. elim: ty A B => //= {Gamma s T} Delta Gamma A B s. - move=> _ _ A' B' sub. by inv sub. - move=> _ ih /sub_trans h A' B' /h. exact: ih. Qed. diff --git a/examples/ssr/SystemF_CBV.v b/examples/ssr/SystemF_CBV.v index adf2ba2..c3dbea7 100644 --- a/examples/ssr/SystemF_CBV.v +++ b/examples/ssr/SystemF_CBV.v @@ -51,7 +51,7 @@ Inductive eval : term -> term -> Prop := eval (Abs A s) (Abs A s) | eval_tabs (A : term) : eval (TAbs A) (TAbs A). -Global Hint Resolve eval_abs eval_tabs. +Global Hint Resolve eval_abs eval_tabs : core. (** **** Syntactic typing *) @@ -92,11 +92,11 @@ Notation E A rho := (L (V A rho)). Lemma V_value A rho v : V A rho v -> eval v v. Proof. by elim: A => [x[]|A _ B _/=[A'[s->]]|A _/=[s->]]. Qed. -Global Hint Resolve V_value. +Global Hint Resolve V_value : core. Lemma V_to_E A rho v : V A rho v -> E A rho v. Proof. exists v; eauto. Qed. -Global Hint Resolve V_to_E. +Global Hint Resolve V_to_E : core. Lemma eq_V A rho1 rho2 v : (forall X v, eval v v -> (rho1 X v <-> rho2 X v)) -> V A rho1 v -> V A rho2 v. @@ -119,7 +119,7 @@ Proof. (do 2 eexists) => // t /ih1/h[u ev]/ih2 ih; by exists u. - move=> A ih rho s xi; asimpl. split=> -[s' -> h]; eexists => //; asimpl=> P B; move: {h} (h P B) => [v ev]. - + move=> /ih {ih} ih. exists v => //. by asimpl in ih. + + move=> /ih {} ih. exists v => //. by asimpl in ih. + move=> h. exists v => //. apply/ih. autosubst. Qed. diff --git a/examples/ssr/SystemF_SN.v b/examples/ssr/SystemF_SN.v index be4b34b..5c55abf 100644 --- a/examples/ssr/SystemF_SN.v +++ b/examples/ssr/SystemF_SN.v @@ -198,7 +198,7 @@ Definition admissible (rho : nat -> cand) := Lemma reducible_sn : reducible sn. Proof. constructor; eauto using ARS.sn. by move=> s t [f] /f. Qed. -Global Hint Resolve reducible_sn. +Global Hint Resolve reducible_sn : core. Lemma reducible_var P x : reducible P -> P (TeVar x). Proof. move/p_nc. apply=> // t st. inv st. Qed. @@ -216,7 +216,7 @@ Proof with eauto using step. eapply h. eapply reducible_var; eauto. + move=> s t h st u la. apply: (p_cl _ (s := App s u))... + move=> s ns h t la. have snt := p_sn (ih1 _ safe) la. - elim: snt la => {t} t _ ih3 la. apply: p_nc... move=> v st. inv st=> //... + elim: snt la => {} t _ ih3 la. apply: p_nc... move=> v st. inv st=> //... apply: ih3 => //. exact: (p_cl (ih1 _ safe)) la _. - constructor. + move=> s /(_ sn (TyVar 0) reducible_sn)/p_sn/sn_tclosed; apply. @@ -251,7 +251,7 @@ Lemma beta_expansion A B rho s t : L A rho (App (Abs B s) t). Proof with eauto. move=> ad snt h. have sns := sn_subst (L_sn ad h). - elim: sns t snt h => {s} s sns ih1 t. elim=> {t} t snt ih2 h. + elim: sns t snt h => {} s sns ih1 t. elim=> {} t snt ih2 h. apply: L_nc => // u st. inv st => //. - inv H2. apply: ih1 => //. apply: L_cl ad h _. exact: step_subst. - apply: ih2 => //. apply: L_cl_star ad h _. exact: red_beta. @@ -261,7 +261,7 @@ Lemma inst_expansion A B rho s : admissible rho -> L A rho s.|[B/] -> L A rho (TApp (TAbs s) B). Proof. move=> ad h. have sns := sn_hsubst (L_sn ad h). elim: sns h. - move=> {s} s _ ih h. apply: L_nc => // t st. inv st => //. + move=> {} s _ ih h. apply: L_nc => // t st. inv st => //. inv H2 => //. apply: ih => //. apply: L_cl ad h _. exact: step_hsubst. Qed. diff --git a/examples/ssr/pred_CC_omega.v b/examples/ssr/pred_CC_omega.v index f1c7d5d..fae03f0 100644 --- a/examples/ssr/pred_CC_omega.v +++ b/examples/ssr/pred_CC_omega.v @@ -152,7 +152,7 @@ Fixpoint rho (s : term) : term := Lemma pstep_refl s : pstep s s. Proof. elim: s; eauto using pstep. Qed. -Global Hint Resolve pstep_refl. +Global Hint Resolve pstep_refl : core. Lemma step_pstep s t : step s t -> pstep s t. Proof. elim; eauto using pstep. Qed. @@ -206,13 +206,13 @@ Proof. apply: (cr_method (e2 := pstep) (rho := rho)). exact: step_pstep. exact: pstep_red. exact: rho_triangle. Qed. -Global Hint Resolve church_rosser. +Global Hint Resolve church_rosser : core. (** **** Reduction behaviour *) Lemma normal_step_sort n : normal step (Sort n). Proof. move=> [s st]. inv st. Qed. -Global Hint Resolve normal_step_sort. +Global Hint Resolve normal_step_sort : core. CoInductive RedProdSpec A1 B1 : term -> Prop := | RedProdSpecI A2 B2 : red A1 A2 -> red B1 B2 -> RedProdSpec A1 B1 (Prod A2 B2). @@ -264,7 +264,7 @@ Proof. move/conv_sub1. apply. exact: sub1_refl. Qed. Lemma sub_refl A : A <: A. Proof. apply: sub1_sub. exact: sub1_refl. Qed. -Global Hint Resolve sub_refl. +Global Hint Resolve sub_refl : core. Lemma sub_sort n m : n <= m -> Sort n <: Sort m. Proof. move=> leq. exact/sub1_sub/sub1_sort. Qed. @@ -368,7 +368,7 @@ Notation "[ Gamma |- s ]" := (exists n, [ Gamma |- s :- Sort n ]). Lemma ty_sort_wf Gamma n : [ Gamma |- Sort n ]. Proof. exists n.+1. exact: ty_sort. Qed. -Global Hint Resolve ty_sort_wf ty_sort. +Global Hint Resolve ty_sort_wf ty_sort : core. Lemma ty_prod_wf Gamma A B : [ Gamma |- A ] -> [ A :: Gamma |- B ] -> [ Gamma |- Prod A B ]. @@ -419,7 +419,7 @@ Proof. move=>->->. exact: weakening. Qed. Lemma ty_ok Gamma : [ Gamma |- ] -> forall x, x < size Gamma -> [ Gamma |- Gamma`_x ]. Proof. - elim=> // {Gamma} Gamma A n tp _ ih [_|x /ih [{n tp} n tp]]; + elim=> // {} Gamma A n tp _ ih [_|x /ih [{tp} n tp]]; exists n; exact: weakening tp. Qed.