Merge pull request #35 from SkySkimmer/intuit-auto

Stop using auto with * in intuition

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 ->

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:

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).

Kami/Lib/Word.v

@@ -484,15 +484,15 @@ 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.
 
 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].

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.
 

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 =>

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').

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.
 

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.

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.