diff --git a/backend/Locations.v b/backend/Locations.v index 2a3ae1d766..6c87c17545 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -488,7 +488,7 @@ Module OrderedLoc <: OrderedType. destruct H0. auto. destruct H. right. split. auto. - intuition. + intuition try lia. right; split. congruence. eapply OrderedTyp.lt_trans; eauto. Qed. Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 61a3718017..755fe3db74 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -527,7 +527,7 @@ Proof. - (* romatch *) apply romatch_exten with bc. eapply romatch_alloc; eauto. eapply mmatch_below; eauto. - simpl; intros. destruct (eq_block b sp); intuition. + simpl; intros. destruct (eq_block b sp); intuition auto with va. - (* mmatch *) constructor; simpl; intros. + (* stack *) @@ -621,7 +621,7 @@ Proof. simpl; intros. destruct (eq_block b sp); auto. - (* romatch *) apply romatch_exten with bc; auto. - simpl; intros. destruct (eq_block b sp); intuition. + simpl; intros. destruct (eq_block b sp); intuition auto with va. - (* mmatch top *) constructor; simpl; intros. + destruct (eq_block b sp). congruence. elim n. eapply bc_stack; eauto. @@ -708,7 +708,7 @@ Proof. simpl; intros. destruct (eq_block b sp); congruence. - (* romatch *) apply romatch_exten with bc; auto. - simpl; intros. destruct (eq_block b sp); intuition. + simpl; intros. destruct (eq_block b sp); intuition auto with va. - (* mmatch top *) constructor; simpl; intros. + destruct (eq_block b sp). congruence. elim n. eapply bc_stack; eauto. @@ -791,7 +791,7 @@ Proof. eapply ematch_incr; eauto. - (* romem *) apply romatch_exten with callee; auto. - intros; simpl. destruct (eq_block b sp); intuition. + intros; simpl. destruct (eq_block b sp); intuition auto with va. - (* mmatch *) constructor; simpl; intros. + (* stack *) @@ -902,7 +902,7 @@ Proof. eapply ematch_incr; eauto. - (* romem *) apply romatch_exten with callee; auto. - intros; simpl. destruct (eq_block b sp); intuition. + intros; simpl. destruct (eq_block b sp); intuition auto with va. - (* mmatch *) constructor; simpl; intros. + (* stack *) diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index ed45ac237d..3ff6250b8a 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -765,7 +765,7 @@ Proof. induction vars; simpl; intros. contradiction. rewrite PTree.grspec. destruct (PTree.elt_eq id (fst a)). auto. - destruct H. intuition. eauto. + destruct H; intuition auto with exfalso. Qed. Definition cenv_compat (cenv: compilenv) (vars: list (ident * Z)) (tsz: Z) : Prop := diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index 3c45e93b64..d0eec6db85 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -2256,7 +2256,7 @@ Proof. eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. exploit (H2 (fun x => C(Ebinop op a1' x ty))). eapply leftcontext_compose; eauto. repeat constructor. auto. intros [E [F G]]. - simpl; intuition. eapply star_trans; eauto. + simpl; intuition auto with bool. eapply star_trans; eauto. (* cast *) exploit (H0 (fun x => C(Ecast x ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. @@ -2365,7 +2365,7 @@ Proof. rewrite exprlist_app_simple. simpl. rewrite H5; rewrite A; auto. repeat rewrite exprlist_app_assoc. simpl. intros [E F]. - simpl; intuition. + simpl; intuition auto with bool. eapply star_trans; eauto. (* skip *) diff --git a/common/Events.v b/common/Events.v index 1b70ecd6aa..aef57fcce1 100644 --- a/common/Events.v +++ b/common/Events.v @@ -796,11 +796,11 @@ Proof. (* mem extends *) - inv H. inv H1. inv H6. inv H4. exploit volatile_load_extends; eauto. intros [v' [A B]]. - exists v'; exists m1'; intuition. constructor; auto. + exists v'; exists m1'; intuition auto with mem. constructor; auto. (* mem injects *) - inv H0. inv H2. inv H7. inversion H5; subst. exploit volatile_load_inject; eauto. intros [v' [A B]]. - exists f; exists v'; exists m1'; intuition. constructor; auto. + exists f; exists v'; exists m1'; intuition auto with mem. constructor; auto. red; intros. congruence. (* trace length *) - inv H; inv H0; simpl; lia. @@ -882,7 +882,7 @@ Proof. eapply eventval_match_lessdef; eauto. apply Val.load_result_lessdef; auto. auto with mem. - exploit Mem.store_within_extends; eauto. intros [m2' [A B]]. - exists m2'; intuition. + exists m2'; intuition auto with mem. + econstructor; eauto. + eapply Mem.store_unchanged_on; eauto. unfold loc_out_of_bounds; intros. @@ -959,11 +959,11 @@ Proof. (* mem extends*) - inv H. inv H1. inv H6. inv H7. inv H4. exploit volatile_store_extends; eauto. intros [m2' [A [B C]]]. - exists Vundef; exists m2'; intuition. constructor; auto. + exists Vundef; exists m2'; intuition auto with mem. constructor; auto. (* mem inject *) - inv H0. inv H2. inv H7. inv H8. inversion H5; subst. exploit volatile_store_inject; eauto. intros [m2' [A [B [C D]]]]. - exists f; exists Vundef; exists m2'; intuition. constructor; auto. red; intros; congruence. + exists f; exists Vundef; exists m2'; intuition auto with mem. constructor; auto. red; intros; congruence. (* trace length *) - inv H; inv H0; simpl; lia. (* receptive *) @@ -1025,7 +1025,7 @@ Proof. intros [m3' [A B]]. exploit Mem.store_within_extends. eexact B. eauto. eauto. intros [m2' [C D]]. - exists (Vptr b Ptrofs.zero); exists m2'; intuition. + exists (Vptr b Ptrofs.zero); exists m2'; intuition auto with mem. econstructor; eauto. eapply UNCHANGED; eauto. (* mem injects *) @@ -1313,12 +1313,12 @@ Proof. - inv H; auto. (* mem extends *) - inv H. - exists Vundef; exists m1'; intuition. + exists Vundef; exists m1'; intuition auto with mem. econstructor; eauto. eapply eventval_list_match_lessdef; eauto. (* mem injects *) - inv H0. - exists f; exists Vundef; exists m1'; intuition. + exists f; exists Vundef; exists m1'; intuition auto with mem. econstructor; eauto. eapply eventval_list_match_inject; eauto. red; intros; congruence. @@ -1358,12 +1358,12 @@ Proof. - inv H; auto. (* mem extends *) - inv H. inv H1. inv H6. - exists v2; exists m1'; intuition. + exists v2; exists m1'; intuition auto with mem. econstructor; eauto. eapply eventval_match_lessdef; eauto. (* mem inject *) - inv H0. inv H2. inv H7. - exists f; exists v'; exists m1'; intuition. + exists f; exists v'; exists m1'; intuition auto with mem. econstructor; eauto. eapply eventval_match_inject; eauto. red; intros; congruence. @@ -1401,11 +1401,11 @@ Proof. - inv H; auto. (* mem extends *) - inv H. - exists Vundef; exists m1'; intuition. + exists Vundef; exists m1'; intuition auto with mem. econstructor; eauto. (* mem injects *) - inv H0. - exists f; exists Vundef; exists m1'; intuition. + exists f; exists Vundef; exists m1'; intuition auto with mem. econstructor; eauto. red; intros; congruence. (* trace length *) diff --git a/common/Memory.v b/common/Memory.v index 2c9151edf1..691622a31c 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -1940,7 +1940,7 @@ Proof. rewrite PMap.gsspec. destruct (peq b bf). subst b. destruct (zle lo ofs); simpl. destruct (zlt ofs hi); simpl. - exfalso; intuition. + exfalso; intuition auto with zarith. auto. auto. auto. Qed. @@ -1983,7 +1983,7 @@ Theorem valid_access_free_1: Proof. intros. inv H. constructor; auto with mem. red; intros. eapply perm_free_1; eauto. - destruct (zlt lo hi). intuition. right. lia. + destruct (zlt lo hi). intuition auto with zarith. right. lia. Qed. Theorem valid_access_free_2: @@ -2178,7 +2178,7 @@ Proof. destruct (zlt ofs0 lo). eapply perm_drop_3; eauto. destruct (zle hi ofs0). eapply perm_drop_3; eauto. apply perm_implies with p. eapply perm_drop_1; eauto. lia. - generalize (size_chunk_pos chunk); intros. intuition. + generalize (size_chunk_pos chunk); intros. intuition auto with zarith exfalso. eapply perm_drop_3; eauto. Qed. @@ -2219,7 +2219,7 @@ Proof. destruct (eq_block b' b). subst b'. destruct (zlt ofs0 lo). eapply perm_drop_3; eauto. destruct (zle hi ofs0). eapply perm_drop_3; eauto. - apply perm_implies with p. eapply perm_drop_1; eauto. lia. intuition. + apply perm_implies with p. eapply perm_drop_1; eauto. lia. intuition auto with zarith exfalso. eapply perm_drop_3; eauto. rewrite pred_dec_false; eauto. red; intros; elim n0; red; intros. @@ -2793,7 +2793,7 @@ Proof. eapply range_perm_drop_1; eauto. lia. auto with mem. eapply perm_drop_4; eauto. eapply perm_max. apply perm_implies with p0. eauto. eauto with mem. - intuition. + intuition auto with zarith. (* align *) intros. eapply mi_align0 with (ofs := ofs) (p := p0); eauto. red; intros; eapply perm_drop_4; eauto. @@ -3405,7 +3405,7 @@ Proof. exploit mi_no_overlap; eauto. instantiate (1 := x - delta1). apply H2. lia. instantiate (1 := x - delta2). apply H3. lia. - intuition. + intuition auto with zarith. Qed. Theorem aligned_area_inject: diff --git a/common/Smallstep.v b/common/Smallstep.v index 3cbd893423..c7efcc903a 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -961,7 +961,7 @@ Proof. (* base case *) exploit fsim_simulation'; eauto. intros [A | [i' A]]. left; auto. - right; exists i'; intuition. + right; exists i'; intuition auto with sets. (* inductive case *) exploit fsim_simulation'; eauto. intros [[i' [s2' [A B]]] | [i' [A [B C]]]]. exploit simulation_star. apply plus_star; eauto. eauto. @@ -1440,7 +1440,7 @@ Proof. - (* base case *) exploit bsim_simulation'; eauto. intros [[i' [s1' [A B]]] | [i' [A [B C]]]]. + left; exists i'; exists s1'; auto. -+ right; exists i'; intuition. ++ right; exists i'; intuition auto with sets. - (* inductive case *) exploit Eapp_E0_inv; eauto. intros [EQ1 EQ2]; subst. exploit bsim_simulation'; eauto. intros [[i' [s1' [A B]]] | [i' [A [B C]]]]. diff --git a/lib/Floats.v b/lib/Floats.v index 33e485248b..ff2584871b 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -472,7 +472,7 @@ Theorem of_intu_of_int_1: Proof. unfold of_intu, of_int, Int.signed, Int.ltu; intro. change (Int.unsigned ox8000_0000) with Int.half_modulus. - destruct (zlt (Int.unsigned x) Int.half_modulus); now intuition. + destruct (zlt (Int.unsigned x) Int.half_modulus); now intuition auto. Qed. Theorem of_intu_of_int_2: @@ -860,7 +860,7 @@ Theorem of_longu_of_long_1: Proof. unfold of_longu, of_long, Int64.signed, Int64.ltu; intro. change (Int64.unsigned (Int64.repr Int64.half_modulus)) with Int64.half_modulus. - destruct (zlt (Int64.unsigned x) Int64.half_modulus); now intuition. + destruct (zlt (Int64.unsigned x) Int64.half_modulus); now intuition auto. Qed. Theorem of_longu_of_long_2: diff --git a/lib/Integers.v b/lib/Integers.v index b69e98425a..a29d35be2d 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -121,7 +121,7 @@ Proof (Z_mod_two_p_range wordsize). Lemma Z_mod_modulus_range': forall x, -1 < Z_mod_modulus x < modulus. Proof. - intros. generalize (Z_mod_modulus_range x); intuition. + intros. generalize (Z_mod_modulus_range x); intuition auto with zarith. Qed. Lemma Z_mod_modulus_eq: @@ -3335,7 +3335,7 @@ Proof. rewrite andb_false_iff. generalize (bits_size_2 a i). generalize (bits_size_2 b i). - zify; intuition. + zify; intuition auto with zarith. Qed. Corollary and_interval: diff --git a/lib/Intv.v b/lib/Intv.v index 3a49181987..d5d024aa69 100644 --- a/lib/Intv.v +++ b/lib/Intv.v @@ -195,7 +195,7 @@ Proof. simpl; split; intros. destruct H. clear IHl. lia. rewrite IHl in H. clear IHl. lia. destruct (zeq (hi - 1) x); auto. right. rewrite IHl. clear IHl. lia. - simpl; intuition. + simpl; intuition auto with zarith. Qed. End ELEMENTS. diff --git a/lib/IntvSets.v b/lib/IntvSets.v index c3fda5f71d..39af622d26 100644 --- a/lib/IntvSets.v +++ b/lib/IntvSets.v @@ -61,7 +61,7 @@ Proof. * tauto. * split; intros. congruence. exfalso. destruct H0. lia. exploit BELOW; eauto. lia. -+ rewrite IHok. intuition. ++ rewrite IHok. intuition auto. Qed. Fixpoint contains (L H: Z) (s: t) : bool := @@ -75,11 +75,11 @@ Lemma contains_In: (contains l0 h0 s = true <-> (forall x, l0 <= x < h0 -> In x s)). Proof. induction 2; simpl. -- intuition. elim (H0 l0); lia. +- intuition auto with zarith bool. elim (H0 l0); lia. - destruct (zle h0 h); simpl. destruct (zle l l0); simpl. - intuition. - rewrite IHok. intuition. destruct (H3 x); auto. exfalso. + intuition auto with zarith. + rewrite IHok. intuition auto with zarith. destruct (H3 x); auto. exfalso. destruct (H3 l0). lia. lia. exploit BELOW; eauto. lia. rewrite IHok. intuition. destruct (H3 x); auto. exfalso. destruct (H3 h). lia. lia. exploit BELOW; eauto. lia. @@ -144,7 +144,7 @@ Proof. destruct (zlt h l0). simpl. rewrite IHok. intuition lia. destruct (zlt h0 l). - simpl. intuition. exploit BELOW; eauto. lia. + simpl. intuition auto with zarith. exploit BELOW; eauto. lia. destruct (zlt l l0). destruct (zlt h0 h); simpl. clear IHok. split. intros [A | [A | A]]. @@ -156,7 +156,7 @@ Proof. auto. intuition lia. destruct (zlt h0 h); simpl. - intuition. exploit BELOW; eauto. lia. + intuition auto with zarith. exploit BELOW; eauto. lia. rewrite IHok. intuition. extlia. Qed. @@ -205,18 +205,18 @@ Proof. tauto. assert (ok (Cons l0 h0 s0)) by (constructor; auto). destruct (zle h l0). - rewrite IHok; auto. simpl. intuition. extlia. + rewrite IHok; auto. simpl. intuition auto with zarith. extlia. exploit BELOW0; eauto. intros. extlia. destruct (zle h0 l). - simpl in IHok0; rewrite IHok0. intuition. extlia. + simpl in IHok0; rewrite IHok0. intuition auto with zarith. extlia. exploit BELOW; eauto. intros; extlia. destruct (zle l l0). destruct (zle h0 h). - simpl. simpl in IHok0; rewrite IHok0. intuition. - simpl. rewrite IHok; auto. simpl. intuition. exploit BELOW0; eauto. intros; extlia. + simpl. simpl in IHok0; rewrite IHok0. intuition auto with zarith. + simpl. rewrite IHok; auto. simpl. intuition auto with zarith. exploit BELOW0; eauto. intros; extlia. destruct (zle h h0). - simpl. rewrite IHok; auto. simpl. intuition. - simpl. simpl in IHok0; rewrite IHok0. intuition. + simpl. rewrite IHok; auto. simpl. intuition auto with zarith. + simpl. simpl in IHok0; rewrite IHok0. intuition auto with zarith. exploit BELOW; eauto. intros; extlia. Qed. @@ -325,9 +325,7 @@ Qed. Theorem In_interval: forall x l h, In x (interval l h) <-> l <= x < h. Proof. - intros. unfold In, interval; destruct (zlt l h); simpl. - intuition. - intuition. + intros. unfold In, interval; destruct (zlt l h); simpl; intuition auto with zarith. Qed. Program Definition add (l h: Z) (s: t) : t := @@ -355,7 +353,7 @@ Proof. unfold remove, In; intros. destruct (zlt l h). simpl. apply R.In_remove. apply proj2_sig. - intuition. + intuition auto with zarith. Qed. Program Definition inter (s1 s2: t) : t := R.inter s1 s2. diff --git a/lib/Zbits.v b/lib/Zbits.v index f6dc0c9d4f..a69a1f8651 100644 --- a/lib/Zbits.v +++ b/lib/Zbits.v @@ -170,12 +170,12 @@ Lemma Z_mod_two_p_range: Proof. intros; unfold Z_mod_two_p. generalize (two_power_nat_pos n); intros. destruct x. - - intuition. + - lia. - apply P_mod_two_p_range. - set (r := P_mod_two_p p n). assert (0 <= r < two_power_nat n) by apply P_mod_two_p_range. destruct (zeq r 0). - + intuition. + + intuition auto with crelations zarith bool. + Psatz.lia. Qed. @@ -192,10 +192,8 @@ Proof. set (r := P_mod_two_p p n) in *. rewrite <- B in C. change (Z.neg p) with (- (Z.pos p)). destruct (zeq r 0). - + symmetry. apply Zmod_unique with (-q). rewrite C; rewrite e. Psatz.lia. - intuition. - + symmetry. apply Zmod_unique with (-q - 1). rewrite C. Psatz.lia. - intuition. + + symmetry. apply Zmod_unique with (-q). rewrite C; rewrite e. lia. lia. + + symmetry. apply Zmod_unique with (-q - 1). rewrite C. lia. lia. Qed. (** ** Bit-level operations and properties *)