From 3d46bed76e656d6a0e4d87320e4d0fd67d1211c2 Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Tue, 19 Jan 2021 11:55:49 -0800 Subject: Remove the SearchHead command --- test-suite/output/SearchHead.out | 69 ---------------------------------- test-suite/output/SearchHead.v | 19 ---------- test-suite/output/Search_headconcl.out | 49 ++++++++++++++++++++++++ test-suite/output/Search_headconcl.v | 18 +++++++++ 4 files changed, 67 insertions(+), 88 deletions(-) delete mode 100644 test-suite/output/SearchHead.out delete mode 100644 test-suite/output/SearchHead.v create mode 100644 test-suite/output/Search_headconcl.out create mode 100644 test-suite/output/Search_headconcl.v (limited to 'test-suite') diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out deleted file mode 100644 index 2f0d854ac6..0000000000 --- a/test-suite/output/SearchHead.out +++ /dev/null @@ -1,69 +0,0 @@ -File "stdin", line 3, characters 0-14: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] -le_n: forall n : nat, n <= n -le_0_n: forall n : nat, 0 <= 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_n_S: forall n m : nat, n <= m -> S n <= S m -le_S_n: forall n m : nat, S n <= S m -> n <= m -File "stdin", line 4, characters 0-16: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] -false: bool -true: bool -negb: bool -> bool -xorb: bool -> bool -> bool -andb: bool -> bool -> bool -orb: bool -> bool -> bool -implb: bool -> bool -> bool -Nat.odd: nat -> bool -Nat.even: nat -> bool -Number.uint_beq: Number.uint -> Number.uint -> bool -Nat.testbit: nat -> nat -> bool -Nat.eqb: nat -> nat -> bool -Hexadecimal.hexadecimal_beq: - Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool -Nat.ltb: nat -> nat -> bool -Nat.leb: nat -> nat -> bool -Number.number_beq: Number.number -> Number.number -> bool -Number.int_beq: Number.int -> Number.int -> bool -Hexadecimal.int_beq: Hexadecimal.int -> Hexadecimal.int -> bool -Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool -Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool -Decimal.int_beq: Decimal.int -> Decimal.int -> bool -Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool -File "stdin", line 5, characters 0-21: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] -mult_n_O: forall n : nat, 0 = n * 0 -plus_O_n: forall n : nat, 0 + n = n -plus_n_O: forall n : nat, n = n + 0 -pred_Sn: forall n : nat, n = Nat.pred (S n) -f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y -eq_add_S: forall n m : nat, S n = S m -> n = m -eq_S: forall x y : nat, x = y -> S x = S y -max_r: forall n m : nat, n <= m -> Nat.max n m = m -max_l: forall n m : nat, m <= n -> Nat.max n m = n -min_r: forall n m : nat, m <= n -> Nat.min n m = m -min_l: forall n m : nat, n <= m -> Nat.min n m = 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) -mult_n_Sm: forall n m : nat, n * m + n = n * S m -f_equal2_plus: - forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 -f_equal2_mult: - forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 -File "stdin", line 11, characters 2-20: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] -h: newdef n -File "stdin", line 17, characters 2-15: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] -h: P n diff --git a/test-suite/output/SearchHead.v b/test-suite/output/SearchHead.v deleted file mode 100644 index 2ee8a0d184..0000000000 --- a/test-suite/output/SearchHead.v +++ /dev/null @@ -1,19 +0,0 @@ -(* 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/Search_headconcl.out b/test-suite/output/Search_headconcl.out new file mode 100644 index 0000000000..24e2ee76af --- /dev/null +++ b/test-suite/output/Search_headconcl.out @@ -0,0 +1,49 @@ +le_n: forall n : nat, n <= n +le_0_n: forall n : nat, 0 <= 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_n_S: forall n m : nat, n <= m -> S n <= S m +le_S_n: forall n m : nat, S n <= S m -> n <= m +false: bool +true: bool +negb: bool -> bool +xorb: bool -> bool -> bool +andb: bool -> bool -> bool +orb: bool -> bool -> bool +implb: bool -> bool -> bool +Nat.odd: nat -> bool +Nat.even: nat -> bool +Number.uint_beq: Number.uint -> Number.uint -> bool +Nat.testbit: nat -> nat -> bool +Nat.eqb: nat -> nat -> bool +Hexadecimal.hexadecimal_beq: + Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool +Nat.ltb: nat -> nat -> bool +Nat.leb: nat -> nat -> bool +Number.number_beq: Number.number -> Number.number -> bool +Number.int_beq: Number.int -> Number.int -> bool +Hexadecimal.int_beq: Hexadecimal.int -> Hexadecimal.int -> bool +Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool +Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool +Decimal.int_beq: Decimal.int -> Decimal.int -> bool +Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool +mult_n_O: forall n : nat, 0 = n * 0 +plus_O_n: forall n : nat, 0 + n = n +plus_n_O: forall n : nat, n = n + 0 +pred_Sn: forall n : nat, n = Nat.pred (S n) +f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y +eq_add_S: forall n m : nat, S n = S m -> n = m +eq_S: forall x y : nat, x = y -> S x = S y +max_r: forall n m : nat, n <= m -> Nat.max n m = m +max_l: forall n m : nat, m <= n -> Nat.max n m = n +min_r: forall n m : nat, m <= n -> Nat.min n m = m +min_l: forall n m : nat, n <= m -> Nat.min n m = 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) +mult_n_Sm: forall n m : nat, n * m + n = n * S m +f_equal2_plus: + forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 +f_equal2_mult: + forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 +h: newdef n +h: P n diff --git a/test-suite/output/Search_headconcl.v b/test-suite/output/Search_headconcl.v new file mode 100644 index 0000000000..8b168dcd25 --- /dev/null +++ b/test-suite/output/Search_headconcl.v @@ -0,0 +1,18 @@ +(* Some tests of the Search command *) + +Search headconcl: le. (* app nodes *) +Search headconcl: bool. (* no apps *) +Search headconcl: (@eq nat). (* complex pattern *) + +Definition newdef := fun x:nat => x = x. + +Goal forall n:nat, newdef n -> False. + intros n h. + Search headconcl: newdef. (* search hypothesis *) +Abort. + + +Goal forall n (P:nat -> Prop), P n -> False. + intros n P h. + Search headconcl: P. (* search hypothesis also for patterns *) +Abort. -- cgit v1.2.3