From b806a8d4fedca9cac03bbbe60efe4c673aa27723 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 5 Jul 2023 14:52:54 +0200 Subject: [PATCH 1/2] Stop using auto with * in intuition --- backend/Locations.v | 2 +- backend/ValueAnalysis.v | 4 +++- cfrontend/Cminorgenproof.v | 2 ++ cfrontend/Cstrategy.v | 2 ++ common/Events.v | 2 ++ common/Memory.v | 2 ++ common/Smallstep.v | 2 ++ lib/Floats.v | 2 ++ lib/Integers.v | 2 ++ lib/Intv.v | 2 ++ lib/IntvSets.v | 2 ++ lib/Zbits.v | 2 ++ 12 files changed, 24 insertions(+), 2 deletions(-) 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..5eb82b7e40 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -17,6 +17,8 @@ Require Import Values Memory Globalenvs Builtins Events. Require Import Registers Op RTL. Require Import ValueDomain ValueAOp Liveness. +Local Ltac Tauto.intuition_solver ::= auto with exfalso bool va. + (** * The dataflow analysis *) Definition areg (ae: aenv) (r: reg) : aval := AE.get r ae. @@ -527,7 +529,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 info_auto with *. - (* mmatch *) constructor; simpl; intros. + (* stack *) diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index ed45ac237d..a37ca0d734 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -22,6 +22,8 @@ Require Import Csharpminor Switch Cminor Cminorgen. Local Open Scope error_monad_scope. +Local Ltac Tauto.intuition_solver ::= auto with exfalso. + Definition match_prog (p: Csharpminor.program) (tp: Cminor.program) := match_program (fun cu f tf => transl_fundef f = OK tf) eq p tp. diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index 3c45e93b64..850231fe20 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -34,6 +34,8 @@ Require Import Cop. Require Import Csyntax. Require Import Csem. +Local Ltac Tauto.intuition_solver ::= auto with bool. + Section STRATEGY. Variable ge: genv. diff --git a/common/Events.v b/common/Events.v index 1b70ecd6aa..171a08c834 100644 --- a/common/Events.v +++ b/common/Events.v @@ -27,6 +27,8 @@ Require Import Memory. Require Import Globalenvs. Require Import Builtins. +Local Ltac Tauto.intuition_solver ::= auto with mem. + (** Backwards compatibility for Hint Rewrite locality attributes. *) Set Warnings "-unsupported-attributes". diff --git a/common/Memory.v b/common/Memory.v index 2c9151edf1..2ca3d2fdbf 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -46,6 +46,8 @@ Local Unset Case Analysis Schemes. Local Notation "a # b" := (PMap.get b a) (at level 1). +Local Ltac Tauto.intuition_solver ::= auto with zarith bool exfalso. + Module Mem <: MEM. Definition perm_order' (po: option permission) (p: permission) := diff --git a/common/Smallstep.v b/common/Smallstep.v index 3cbd893423..80c2e3702e 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -29,6 +29,8 @@ Require Import Integers. Set Implicit Arguments. +Local Ltac Tauto.intuition_solver ::= auto with sets. + (** * Closures of transitions relations *) Section CLOSURES. diff --git a/lib/Floats.v b/lib/Floats.v index 33e485248b..f629064837 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -25,6 +25,8 @@ Require Import Program. Require Archi. Import ListNotations. +Local Ltac Tauto.intuition_solver ::= auto with exfalso bool. + Close Scope R_scope. Open Scope Z_scope. Set Asymmetric Patterns. diff --git a/lib/Integers.v b/lib/Integers.v index b69e98425a..dfb4242b17 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -20,6 +20,8 @@ Require Import Eqdep_dec Zquot Zwf. Require Import Coqlib Zbits. Require Archi. +Local Ltac Tauto.intuition_solver ::= auto with zarith bool. + (** Backwards compatibility for Hint Rewrite locality attributes. *) Set Warnings "-unsupported-attributes". diff --git a/lib/Intv.v b/lib/Intv.v index 3a49181987..baa42112c5 100644 --- a/lib/Intv.v +++ b/lib/Intv.v @@ -21,6 +21,8 @@ Require Import Zwf. Require Coq.Program.Wf. Require Import Recdef. +Local Ltac Tauto.intuition_solver ::= auto with zarith bool. + Definition interv : Type := (Z * Z)%type. (** * Membership *) diff --git a/lib/IntvSets.v b/lib/IntvSets.v index c3fda5f71d..452ceeb193 100644 --- a/lib/IntvSets.v +++ b/lib/IntvSets.v @@ -18,6 +18,8 @@ Require Import Coqlib. +Local Ltac Tauto.intuition_solver ::= auto with zarith bool. + Module ISet. (** "Raw", non-dependent implementation. A set of intervals is a diff --git a/lib/Zbits.v b/lib/Zbits.v index f6dc0c9d4f..6bddee55b5 100644 --- a/lib/Zbits.v +++ b/lib/Zbits.v @@ -20,6 +20,8 @@ Require Import Psatz Zquot. Require Import Coqlib. +Local Ltac Tauto.intuition_solver ::= auto with crelations zarith bool. + (** ** Modulo arithmetic *) (** We define and state properties of equality and arithmetic modulo a From a146716693ab3869ae705fe3afd8278ed6b18684 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 10 Jul 2023 09:31:02 +0200 Subject: [PATCH 2/2] Remove one more intuition auto with * --- backend/ValueAnalysis.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 5eb82b7e40..9890400440 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -529,7 +529,7 @@ Proof. - (* romatch *) apply romatch_exten with bc. eapply romatch_alloc; eauto. eapply mmatch_below; eauto. - simpl; intros. destruct (eq_block b sp); intuition info_auto with *. + simpl; intros. destruct (eq_block b sp); intuition. - (* mmatch *) constructor; simpl; intros. + (* stack *)