From a08754aad4ba2c9a494d7ab391caf6561058913e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 5 Jul 2023 14:00:02 +0200 Subject: [PATCH] Stop using auto with * in intuition --- Kami/InlineFacts.v | 2 ++ Kami/Lib/FMap.v | 5 ++++- Kami/Lib/NatLib.v | 6 +++--- Kami/Lib/Word.v | 8 ++++---- Kami/PartialInlineFacts.v | 3 +++ Kami/RefinementFacts.v | 2 ++ Kami/Renaming.v | 4 +++- Kami/SemFacts.v | 6 ++++-- Kami/Specialize.v | 2 ++ Kami/Wf.v | 2 ++ 10 files changed, 29 insertions(+), 11 deletions(-) diff --git a/Kami/InlineFacts.v b/Kami/InlineFacts.v index c5971c51..d8ad642b 100644 --- a/Kami/InlineFacts.v +++ b/Kami/InlineFacts.v @@ -12,6 +12,8 @@ Require Import (hints) btauto.Algebra. Set Implicit Arguments. Set Asymmetric Patterns. +Local Ltac Tauto.intuition_solver ::= auto with datatypes exfalso. + Lemma inlineDm_SemAction_intact: forall {retK} or a nr calls (retV: type retK), SemAction or a nr calls retV -> diff --git a/Kami/Lib/FMap.v b/Kami/Lib/FMap.v index 153756d5..fca47a81 100644 --- a/Kami/Lib/FMap.v +++ b/Kami/Lib/FMap.v @@ -7,6 +7,9 @@ Require Import Equalities Eqdep_dec FMapInterface. Require Import Lib.CommonTactics Lib.StringAsOT Lib.StringEq Lib.Struct. +Local Ltac Tauto.intuition_solver ::= auto with datatypes. + + Set Implicit Arguments. Set Asymmetric Patterns. @@ -2754,7 +2757,7 @@ Section MakeMap. Proof. induction m; simpl; intros; [apply M.KeysSubset_empty|]. destruct a as [an [atype av]]; simpl. - apply M.KeysSubset_add; intuition. + apply M.KeysSubset_add; intuition auto with MapDefs datatypes. Qed. Lemma makeMap_union: diff --git a/Kami/Lib/NatLib.v b/Kami/Lib/NatLib.v index 4893a34b..8c76c069 100644 --- a/Kami/Lib/NatLib.v +++ b/Kami/Lib/NatLib.v @@ -52,7 +52,7 @@ Section strong. Hypothesis PH : forall n, (forall m, m < n -> P m) -> P n. Lemma strong' : forall n m, m <= n -> P m. - induction n; simpl; intuition; apply PH; intuition. + induction n; simpl; intuition auto with zarith; apply PH; intuition. exfalso; lia. Qed. @@ -92,7 +92,7 @@ Theorem drop_mod2 : forall n k, do 2 (destruct n; simpl in *; repeat rewrite untimes2 in *; intuition). - destruct k; simpl in *; intuition. + destruct k; simpl in *; intuition lia. destruct k; simpl; intuition. rewrite <- plus_n_Sm. @@ -380,7 +380,7 @@ Qed. Theorem Npow2_nat : forall n, nat_of_N (Npow2 n) = pow2 n. induction n as [|n IHn]; simpl; intuition. rewrite <- IHn; clear IHn. - case_eq (Npow2 n); intuition. + case_eq (Npow2 n); intuition lia. Qed. Theorem pow2_N : forall n, Npow2 n = N.of_nat (pow2 n). diff --git a/Kami/Lib/Word.v b/Kami/Lib/Word.v index 8ac9a541..a23c7c2e 100644 --- a/Kami/Lib/Word.v +++ b/Kami/Lib/Word.v @@ -484,7 +484,7 @@ Theorem natToWord_wordToNat : forall sz w, natToWord sz (wordToNat w) = w. Qed. Theorem roundTrip_0 : forall sz, wordToNat (natToWord sz 0) = 0. - induction sz; simpl; intuition. + induction sz; simpl; intuition lia. Qed. #[global] Hint Rewrite roundTrip_0 : wordToNat. @@ -492,7 +492,7 @@ Qed. Lemma wordToNat_natToWord' : forall sz w, exists k, wordToNat (natToWord sz w) + k * pow2 sz = w. induction sz as [|sz IHsz]; simpl; intro w; intuition; repeat rewrite untimes2. - exists w; intuition. + exists w; intuition lia. case_eq (mod2 w); intro Hmw. @@ -526,7 +526,7 @@ Qed. Theorem wordToNat_natToWord: forall sz w, exists k, wordToNat (natToWord sz w) = w - k * pow2 sz /\ (k * pow2 sz <= w)%nat. Proof. - intros sz w; destruct (wordToNat_natToWord' sz w) as [k]; exists k; intuition. + intros sz w; destruct (wordToNat_natToWord' sz w) as [k]; exists k; intuition lia. Qed. Lemma wordToNat_natToWord_2: forall sz w : nat, @@ -5087,7 +5087,7 @@ Qed. Lemma ZToWord_plus: forall sz a b, ZToWord sz (a + b) = ZToWord sz a ^+ ZToWord sz b. Proof. - destruct sz as [|sz]; intros n m; intuition. + destruct sz as [|sz]; intros n m; intuition auto with worder. rewrite wplus_wplusZ. unfold wplusZ, wordBinZ. destruct (wordToZ_ZToWord' (S sz) n) as [k1 D1]. diff --git a/Kami/PartialInlineFacts.v b/Kami/PartialInlineFacts.v index ba336292..d7c72197 100644 --- a/Kami/PartialInlineFacts.v +++ b/Kami/PartialInlineFacts.v @@ -6,6 +6,9 @@ Require Import Program.Equality FunctionalExtensionality. Import ListNotations. +Local Ltac Tauto.intuition_solver ::= auto with datatypes exfalso bool zarith. + + Set Implicit Arguments. Set Asymmetric Patterns. diff --git a/Kami/RefinementFacts.v b/Kami/RefinementFacts.v index 72906dd3..e6353e48 100644 --- a/Kami/RefinementFacts.v +++ b/Kami/RefinementFacts.v @@ -9,6 +9,8 @@ Import ListNotations. Set Implicit Arguments. Set Asymmetric Patterns. +Local Ltac Tauto.intuition_solver ::= auto with exfalso zarith. + Section LabelMapComposition. Definition compLabelMaps (p q: M.key -> sigT SignT -> option (sigT SignT)) := fun s v => diff --git a/Kami/Renaming.v b/Kami/Renaming.v index bfdb1cea..1cf5085f 100644 --- a/Kami/Renaming.v +++ b/Kami/Renaming.v @@ -6,6 +6,8 @@ Require Import Lib.CommonTactics. Set Implicit Arguments. Set Asymmetric Patterns. +Local Ltac Tauto.intuition_solver ::= auto with datatypes. + Lemma prepend1To1: forall c s1 s2: string, (c ++ s1)%string = (c ++ s2)%string -> s1 = s2. Proof. induction c; simpl in *; intros. @@ -218,7 +220,7 @@ Section Rename. rewrite M.find_add_1; intuition. unfold Morphisms.Proper, Morphisms.respectful; intros. rewrite H, H1, H2. - intuition. + intuition auto with MapDefs. unfold M.F.P.transpose_neqkey, M.Map.Equal; intros. f_equal. M.cmp (rename k0) (rename k'). diff --git a/Kami/SemFacts.v b/Kami/SemFacts.v index 43c469d5..6f49aa5c 100644 --- a/Kami/SemFacts.v +++ b/Kami/SemFacts.v @@ -6,6 +6,8 @@ Require Import Kami.Syntax Kami.Semantics Kami.Wf. Set Implicit Arguments. Set Asymmetric Patterns. +Local Ltac Tauto.intuition_solver ::= auto with exfalso datatypes. + Ltac specializeAll k := repeat match goal with @@ -99,11 +101,11 @@ Section LiftToMap. + intuition. + clear; unfold Morphisms.Proper, Morphisms.respectful; intros; subst. apply M.leibniz in H1; subst. - intuition. + intuition auto with MapDefs. + clear; unfold M.F.P.transpose_neqkey; intros. unfold rmModify. destruct (p k e), (p k' e'); - try apply M.transpose_neqkey_Equal_add; intuition. + try apply M.transpose_neqkey_Equal_add; intuition auto with MapDefs. + intuition. Qed. diff --git a/Kami/Specialize.v b/Kami/Specialize.v index b7edf4bb..b09a2b6f 100644 --- a/Kami/Specialize.v +++ b/Kami/Specialize.v @@ -8,6 +8,8 @@ Require Import Compare_dec. Set Implicit Arguments. Set Asymmetric Patterns. +Local Ltac Tauto.intuition_solver ::= auto with exfalso bool zarith. + Section SpecializeModule. Variable m: Modules. Variable i: nat. diff --git a/Kami/Wf.v b/Kami/Wf.v index 8b98ccdf..bd1c50f6 100644 --- a/Kami/Wf.v +++ b/Kami/Wf.v @@ -7,6 +7,8 @@ Require Import FunctionalExtensionality Program.Equality Eqdep Eqdep_dec. Set Implicit Arguments. Set Asymmetric Patterns. +Local Ltac Tauto.intuition_solver ::= auto with datatypes. + (* PHOAS equivalence *) Section Equiv. Variable t1 t2: Kind -> Type.