From aba0e740f25ffa5c338dfa76cab71144802cebc2 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 21 Jun 2020 18:22:00 +0200 Subject: Replace `omega` tactic with `lia` Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`. --- cfrontend/Cstrategy.v | 50 +++++++++++++++++++++++++------------------------- 1 file changed, 25 insertions(+), 25 deletions(-) (limited to 'cfrontend/Cstrategy.v') diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index c235031f..30e5c2ae 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -1553,13 +1553,13 @@ Proof. exploit external_call_trace_length; eauto. destruct t1; simpl; intros. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. econstructor; econstructor. left; eapply step_builtin; eauto. - omegaContradiction. + extlia. (* external calls *) inv H1. exploit external_call_trace_length; eauto. destruct t1; simpl; intros. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. exists (Returnstate vres2 k m2); exists E0; right; econstructor; eauto. - omegaContradiction. + extlia. (* well-behaved traces *) red; intros. inv H; inv H0; simpl; auto. (* valof volatile *) @@ -1582,10 +1582,10 @@ Proof. exploit deref_loc_trace; eauto. destruct t; auto. destruct t; tauto. (* builtins *) exploit external_call_trace_length; eauto. - destruct t; simpl; auto. destruct t; simpl; auto. intros; omegaContradiction. + destruct t; simpl; auto. destruct t; simpl; auto. intros; extlia. (* external calls *) exploit external_call_trace_length; eauto. - destruct t; simpl; auto. destruct t; simpl; auto. intros; omegaContradiction. + destruct t; simpl; auto. destruct t; simpl; auto. intros; extlia. Qed. (** The main simulation result. *) @@ -2734,7 +2734,7 @@ Proof. cofix COEL. intros. inv H. (* cons left *) - eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Ecall a1 (exprlist_app al (Econs x al0)) ty)). eauto. eapply leftcontext_compose; eauto. constructor. auto. apply exprlist_app_leftcontext; auto. traceEq. @@ -2745,7 +2745,7 @@ Proof. eapply leftcontext_compose; eauto. repeat constructor. auto. apply exprlist_app_leftcontext; auto. eapply forever_N_star with (a2 := (esizelist al0)). - eexact R. simpl; omega. + eexact R. simpl; lia. change (Econs a1' al0) with (exprlist_app (Econs a1' Enil) al0). rewrite <- exprlist_app_assoc. eapply COEL. eauto. auto. auto. @@ -2754,42 +2754,42 @@ Proof. intros. inv H. (* field *) - eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Efield x f0 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* valof *) - eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Evalof x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* deref *) - eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Ederef x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* addrof *) - eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Eaddrof x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* unop *) - eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Eunop op x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* binop left *) - eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Ebinop op x a2 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* binop right *) destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Ebinop op x a2 ty)) f k) as [P [Q R]]. eapply leftcontext_compose; eauto. repeat constructor. - eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; omega. + eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; lia. eapply COE with (C := fun x => C(Ebinop op a1' x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. auto. traceEq. (* cast *) - eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Ecast x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* seqand left *) - eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Eseqand x a2 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* seqand 2 *) @@ -2802,7 +2802,7 @@ Proof. eapply COE with (C := fun x => (C (Eparen x type_bool ty))). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* seqor left *) - eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Eseqor x a2 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* seqor 2 *) @@ -2815,7 +2815,7 @@ Proof. eapply COE with (C := fun x => (C (Eparen x type_bool ty))). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* condition top *) - eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Econdition x a2 a3 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* condition *) @@ -2828,33 +2828,33 @@ Proof. eapply COE with (C := fun x => (C (Eparen x ty ty))). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* assign left *) - eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Eassign x a2 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* assign right *) destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Eassign x a2 ty)) f k) as [P [Q R]]. eapply leftcontext_compose; eauto. repeat constructor. - eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; omega. + eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; lia. eapply COE with (C := fun x => C(Eassign a1' x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. auto. traceEq. (* assignop left *) - eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Eassignop op x a2 tyres ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* assignop right *) destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Eassignop op x a2 tyres ty)) f k) as [P [Q R]]. eapply leftcontext_compose; eauto. repeat constructor. - eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; omega. + eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; lia. eapply COE with (C := fun x => C(Eassignop op a1' x tyres ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. auto. traceEq. (* postincr *) - eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Epostincr id x ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* comma left *) - eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Ecomma x a2 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* comma right *) @@ -2865,14 +2865,14 @@ Proof. left; eapply step_comma; eauto. reflexivity. eapply COE with (C := C); eauto. traceEq. (* call left *) - eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia. eapply COE with (C := fun x => C(Ecall x a2 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* call right *) destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Ecall x a2 ty)) f k) as [P [Q R]]. eapply leftcontext_compose; eauto. repeat constructor. - eapply forever_N_star with (a2 := (esizelist a2)). eexact R. simpl; omega. + eapply forever_N_star with (a2 := (esizelist a2)). eexact R. simpl; lia. eapply COEL with (al := Enil). eauto. auto. auto. auto. traceEq. (* call *) destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Ecall x rargs ty)) f k) -- cgit