Stop using auto with * in intuition (partial) (#44)

src/FCF/Asymptotic.v

@@ -8,6 +8,8 @@ Set Implicit Arguments.
 
 Require Import FCF.StdNat.
 
+Local Ltac Tauto.intuition_solver ::= auto with arith crelations.
+
 Definition polynomial (f : nat -> nat) :=
     exists x c1 c2, forall n,
       (f n <= c1 * expnat n x + c2)%nat.

src/FCF/Blist.v

@@ -14,6 +14,8 @@ Require Import FCF.Fold.
 Require Import ZArith.
 Local Open Scope list_scope.
 
+Local Ltac Tauto.intuition_solver ::= auto with arith bool zarith.
+
 Definition Blist := list bool.
 
 Definition Blist_eq_dec := (list_eq_dec bool_dec).

src/FCF/Comp.v

@@ -12,6 +12,7 @@ Require Export FCF.Blist.
 Require Export FCF.EqDec.
 Require Import FCF.Fold.
 
+Local Ltac Tauto.intuition_solver ::= auto with comp bool zarith.
 
 Inductive Comp : Set -> Type :=
 | Ret : forall (A : Set), eq_dec A -> A -> Comp A
@@ -67,7 +68,7 @@ Lemma comp_EqDec : forall (A : Set),
   Comp A ->
   EqDec A.
 
-  induction 1; intuition.
+  induction 1; intuition auto with typeclass_instances.
   exists (fun a1 a2 => if e a1 a2 then true else false).
   intuition.
   destruct (e x y); simpl in *; trivial. discriminate.

src/FCF/Fold.v

@@ -15,6 +15,8 @@ Require Import Bool.
 
 Local Open Scope rat_scope.
 
+Local Ltac Tauto.intuition_solver ::= auto with crelations datatypes arith.
+
 (* The traditional functional zip and unzip. *)
 (* TODO: get rid of these and replace with combine and split *)
 Definition unzip(A B : Set)(ls : list (A * B)) :=

src/FCF/Limit.v

@@ -13,6 +13,8 @@ Require Import List.
 Require Import FCF.StdNat.
 Require Import FCF.Rat.
 
+Local Ltac Tauto.intuition_solver ::= auto with crelations bool.
+
 Section Limit.
 
   Variable A : Set.

src/FCF/Lognat.v

@@ -11,6 +11,7 @@ Set Implicit Arguments.
 Require Import ZArith.
 Require Import micromega.Lia.
 
+Local Ltac Tauto.intuition_solver ::= auto with zarith.
 
 (* log2 is like log_inf except it returns nat, so I don't have to reason about an unnecessary conversion. This function is only used to implement lognat below.*)
 Fixpoint log2(n : positive) : nat :=

src/FCF/Rat.v

@@ -10,6 +10,8 @@ Require Import FCF.StdNat.
 Require Import Arith.
 Require Import Lia.
 
+Local Ltac Tauto.intuition_solver ::= auto with bool crelations arith.
+
 Inductive Rat :=
     RatIntro : nat -> posnat -> Rat.
 

src/FCF/StdNat.v

@@ -11,6 +11,8 @@ Require Export Arith.Div2.
 Require Export Coq.Numbers.Natural.Peano.NPeano. 
 Require Import Coq.NArith.BinNat.
 
+Local Ltac Tauto.intuition_solver ::= auto with crelations arith.
+
 Lemma mult_same_r : forall n1 n2 n3,
   n3 > 0 ->
   n1 * n3 = n2 * n3 ->