Tests for Searchxxx commands added and modified.

8 files changed, 191 insertions, 3 deletions

diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index dbd72017a4..c17b285bc9 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -1,28 +1,74 @@
 le_n: forall n : nat, n <= n
 le_S: forall n m : nat, n <= m -> n <= S m
+le_ind:
+  forall (n : nat) (P : nat -> Prop),
+  P n ->
+  (forall m : nat, n <= m -> P m -> P (S m)) ->
+  forall n0 : nat, n <= n0 -> P n0
 le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
 le_S_n: forall n m : nat, S n <= S m -> n <= m
 le_0_n: forall n : nat, 0 <= n
 le_n_S: forall n m : nat, n <= m -> S n <= S m
+max_l: forall n m : nat, m <= n -> Nat.max n m = n
+max_r: forall n m : nat, n <= m -> Nat.max n m = m
+min_l: forall n m : nat, n <= m -> Nat.min n m = n
+min_r: forall n m : nat, m <= n -> Nat.min n m = m
 true: bool
 false: bool
+bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
+bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
+bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
 andb: bool -> bool -> bool
 orb: bool -> bool -> bool
 implb: bool -> bool -> bool
 xorb: bool -> bool -> bool
 negb: bool -> bool
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
+andb_true_intro:
+  forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
+eq_true: bool -> Prop
+eq_true_rect:
+  forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b
+eq_true_ind:
+  forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
+eq_true_rec:
+  forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b
+is_true: bool -> Prop
+eq_true_ind_r:
+  forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true
+eq_true_rec_r:
+  forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true
+eq_true_rect_r:
+  forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true
+BoolSpec: Prop -> Prop -> bool -> Prop
+BoolSpec_ind:
+  forall (P Q : Prop) (P0 : bool -> Prop),
+  (P -> P0 true) ->
+  (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b
 Nat.eqb: nat -> nat -> bool
 Nat.leb: nat -> nat -> bool
 Nat.ltb: nat -> nat -> bool
 Nat.even: nat -> bool
 Nat.odd: nat -> bool
 Nat.testbit: nat -> nat -> bool
+Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
+bool_choice:
+  forall (S : Set) (R1 R2 : S -> Prop),
+  (forall x : S, {R1 x} + {R2 x}) ->
+  {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
 eq_S: forall x y : nat, x = y -> S x = S y
+f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y
 f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
 pred_Sn: forall n : nat, n = Nat.pred (S n)
 eq_add_S: forall n m : nat, S n = S m -> n = m
+not_eq_S: forall n m : nat, n <> m -> S n <> S m
+O_S: forall n : nat, 0 <> S n
+n_Sn: forall n : nat, n <> S n
 f_equal2_plus:
   forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
+f_equal2_nat:
+  forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat),
+  x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2
 plus_n_O: forall n : nat, n = n + 0
 plus_O_n: forall n : nat, 0 + n = n
 plus_n_Sm: forall n m : nat, S (n + m) = n + S m
@@ -35,3 +81,28 @@ max_l: forall n m : nat, m <= n -> Nat.max n m = n
 max_r: forall n m : nat, n <= m -> Nat.max n m = m
 min_l: forall n m : nat, n <= m -> Nat.min n m = n
 min_r: forall n m : nat, m <= n -> Nat.min n m = m
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
+andb_true_intro:
+  forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
+bool_choice:
+  forall (S : Set) (R1 R2 : S -> Prop),
+  (forall x : S, {R1 x} + {R2 x}) ->
+  {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
+andb_true_intro:
+  forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
+h': newdef n <> n
+h: n <> newdef n
+h': newdef n <> n
+h: n <> newdef n
+h: n <> newdef n
+h: n <> newdef n
+h': ~ P n
+h: P n
+h': ~ P n
+h: P n
+h': ~ P n
+h: P n
+h: P n
+h: P n
diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v
index 4ef2634733..2a0f0b407c 100644
--- a/test-suite/output/Search.v
+++ b/test-suite/output/Search.v
@@ -1,5 +1,29 @@
 (* Some tests of the Search command *)
 
-SearchHead le.				(* app nodes *)
-SearchHead bool. 				(* no apps *)
-SearchHead (@eq nat).			(* complex pattern *)
+Search le.				(* app nodes *)
+Search bool. 				(* no apps *)
+Search (@eq nat).			(* complex pattern *)
+Search (@eq _ _ true).
+Search (@eq _ _ _) true -false.         (* andb_prop *)
+Search (@eq _ _ _) true -false "prop" -"intro".  (* andb_prop *)
+       
+Definition newdef := fun x:nat => x.
+
+Goal forall n:nat, n <> newdef n -> newdef n <> n -> False.
+  intros n h h'.
+  Search n.                             (* search hypothesis *)
+  Search newdef.                        (* search hypothesis *)
+  Search ( _ <> newdef _).              (* search hypothesis, pattern *)
+  Search ( _ <> newdef _) -"h'".        (* search hypothesis, pattern *)
+Abort.
+
+Goal forall n (P:nat -> Prop), P n -> ~P n -> False.
+  intros n P h h'.
+  Search P.                 (* search hypothesis also for patterns *)
+  Search (P _).             (* search hypothesis also for patterns *)
+  Search (P n).             (* search hypothesis also for patterns *)
+  Search (P _) -"h'".       (* search hypothesis also for patterns *)
+  Search (P _) -not.       (* search hypothesis also for patterns *)
+
+Abort.
+
diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out
new file mode 100644
index 0000000000..0d5924ec61
--- /dev/null
+++ b/test-suite/output/SearchHead.out
@@ -0,0 +1,39 @@
+le_n: forall n : nat, n <= n
+le_S: forall n m : nat, n <= m -> n <= S m
+le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
+le_S_n: forall n m : nat, S n <= S m -> n <= m
+le_0_n: forall n : nat, 0 <= n
+le_n_S: forall n m : nat, n <= m -> S n <= S m
+true: bool
+false: bool
+andb: bool -> bool -> bool
+orb: bool -> bool -> bool
+implb: bool -> bool -> bool
+xorb: bool -> bool -> bool
+negb: bool -> bool
+Nat.eqb: nat -> nat -> bool
+Nat.leb: nat -> nat -> bool
+Nat.ltb: nat -> nat -> bool
+Nat.even: nat -> bool
+Nat.odd: nat -> bool
+Nat.testbit: nat -> nat -> bool
+eq_S: forall x y : nat, x = y -> S x = S y
+f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
+pred_Sn: forall n : nat, n = Nat.pred (S n)
+eq_add_S: forall n m : nat, S n = S m -> n = m
+f_equal2_plus:
+  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
+plus_n_O: forall n : nat, n = n + 0
+plus_O_n: forall n : nat, 0 + n = n
+plus_n_Sm: forall n m : nat, S (n + m) = n + S m
+plus_Sn_m: forall n m : nat, S n + m = S (n + m)
+f_equal2_mult:
+  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
+mult_n_O: forall n : nat, 0 = n * 0
+mult_n_Sm: forall n m : nat, n * m + n = n * S m
+max_l: forall n m : nat, m <= n -> Nat.max n m = n
+max_r: forall n m : nat, n <= m -> Nat.max n m = m
+min_l: forall n m : nat, n <= m -> Nat.min n m = n
+min_r: forall n m : nat, m <= n -> Nat.min n m = m
+h: newdef n
+h: P n
diff --git a/test-suite/output/SearchHead.v b/test-suite/output/SearchHead.v
new file mode 100644
index 0000000000..2ee8a0d184
--- /dev/null
+++ b/test-suite/output/SearchHead.v
@@ -0,0 +1,19 @@
+(* Some tests of the Search command *)
+
+SearchHead le.				(* app nodes *)
+SearchHead bool. 				(* no apps *)
+SearchHead (@eq nat).			(* complex pattern *)
+
+Definition newdef := fun x:nat => x = x.
+
+Goal forall n:nat, newdef n -> False.
+  intros n h.
+  SearchHead newdef.             (* search hypothesis *)
+Abort.
+
+
+Goal forall n (P:nat -> Prop), P n -> False.
+  intros n P h.
+  SearchHead P.                  (* search hypothesis also for patterns *)
+Abort.
+
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index 74bbf6882e..1eb7eca8f1 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -75,3 +75,9 @@ pair: forall A B : Type, A -> B -> A * B
 conj: forall A B : Prop, A -> B -> A /\ B
 Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
 
+h: n <> newdef n
+h: n <> newdef n
+h: P n
+h': ~ P n
+h: P n
+h: P n
diff --git a/test-suite/output/SearchPattern.v b/test-suite/output/SearchPattern.v
index 802d8c9760..bde195a511 100644
--- a/test-suite/output/SearchPattern.v
+++ b/test-suite/output/SearchPattern.v
@@ -17,3 +17,20 @@ SearchPattern (forall (x:?A) (y:?B), _ ?A ?B).
 
 (* No delta-reduction *)
 SearchPattern (Exc _).
+
+Definition newdef := fun x:nat => x.
+
+Goal forall n:nat, n <> newdef n -> False.
+  intros n h.
+  SearchPattern ( _ <> newdef _).          (* search hypothesis *)
+  SearchPattern ( n <> newdef _).          (* search hypothesis *)
+Abort.
+
+Goal forall n (P:nat -> Prop), P n -> ~P n -> False.
+  intros n P h h'.
+  SearchPattern (P _).      (* search hypothesis also for patterns *)
+  Search (~P n).          (* search hypothesis also for patterns *)
+  Search (P _) -"h'".       (* search hypothesis also for patterns *)
+  Search (P _) -not.       (* search hypothesis also for patterns *)
+
+Abort.
\ No newline at end of file
diff --git a/test-suite/output/SearchRewrite.out b/test-suite/output/SearchRewrite.out
index f87aea1c84..5edea5dff6 100644
--- a/test-suite/output/SearchRewrite.out
+++ b/test-suite/output/SearchRewrite.out
@@ -1,2 +1,5 @@
 plus_n_O: forall n : nat, n = n + 0
 plus_O_n: forall n : nat, 0 + n = n
+h: n = newdef n
+h: n = newdef n
+h: n = newdef n
diff --git a/test-suite/output/SearchRewrite.v b/test-suite/output/SearchRewrite.v
index 171a7363fe..53d043c681 100644
--- a/test-suite/output/SearchRewrite.v
+++ b/test-suite/output/SearchRewrite.v
@@ -2,3 +2,12 @@
 
 SearchRewrite (_+0). 			(* left *)
 SearchRewrite (0+_). 			(* right *)
+
+Definition newdef := fun x:nat => x.
+
+Goal forall n:nat, n = newdef n -> False.
+  intros n h.
+  SearchRewrite (newdef _).
+  SearchRewrite n.                (* use hypothesis for patterns *)
+  SearchRewrite (newdef n).       (* use hypothesis for patterns *)
+Abort.