Avoid relying on intuition being intuition auto with * (#496)

Coq 8.17 warns about this, since at some point in the future `intuition` will become `intuition auto`. This commit rewrites a number of uses of `intuition` to avoid relying on the implicit `intuition auto with *`. Co-authored-by: Gaëtan Gilbert <[email protected]>
AbsInt · Jul 10, 2023 · 974fbd8 · 974fbd8
1 parent 920da14
commit 974fbd8
Show file tree

Hide file tree

Showing 12 changed files with 52 additions and 56 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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.