Skip to content

Commit 2c3ee37

Browse files
adomaniadomani
committed
chore(test/*): add test_sorry axiom in tests to make them less noisy (#6868)
This PR adds `axiom test_sorry` for the `sorry`s in tests, in order to remove the noisy output of `sorry`. In `test/rewrites.lean` and `test/IsCompact.lean` some of the `#guard_msgs` are `#guard_msgs(warning)`, due to further messages. Affected files: ``` test/apply_fun.lean test/cancel_denoms.lean test/Change.lean test/congr.lean test/congrm.lean test/convert.lean test/DefEqTransformations.lean test/FBinop.lean test/GCongr/inequalities.lean test/GeneralizeProofs.lean test/ImplicitUniverses.lean test/InstanceTransparency.lean test/LibrarySearch/IsCompact.lean test/LiftLets.lean test/linarith.lean test/MfldSetTac.lean test/mod_cases.lean test/Monotonicity.lean test/nontriviality.lean test/norm_num.lean test/push_neg.lean test/Real.lean test/rewrites.lean test/ring.lean test/Zify.lean ``` [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/noisy.20tests)
1 parent f1e1b39 commit 2c3ee37

25 files changed

+210
-195
lines changed

‎test/Change.lean‎

Lines changed: 8 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -1,55 +1,44 @@
11
import Mathlib.Tactic.Change
22
import Std.Tactic.GuardExpr
33

4+
private axiom test_sorry : ∀ {α}, α
45
set_option pp.unicode.fun true
56

67
set_option autoImplicit true
78

8-
/-- warning: declaration uses 'sorry' -/
9-
#guard_msgs in
109
example : n + 2 = m := by
1110
change n + 1 + 1 = _
1211
guard_target =ₛ n + 1 + 1 = m
13-
sorry
12+
exact test_sorry
1413

15-
/-- warning: declaration uses 'sorry' -/
16-
#guard_msgs in
1714
example (h : n + 2 = m) : False := by
1815
change _ + 1 = _ at h
1916
guard_hyp h :ₛ n + 1 + 1 = m
20-
sorry
17+
exact test_sorry
2118

22-
/-- warning: declaration uses 'sorry' -/
23-
#guard_msgs in
2419
example : n + 2 = m := by
2520
fail_if_success change true
2621
fail_if_success change _ + 3 = _
2722
fail_if_success change _ * _ = _
2823
change (_ : Nat) + _ = _
29-
sorry
24+
exact test_sorry
3025

3126
-- `change ... at ...` allows placeholders to mean different things at different hypotheses
32-
/-- warning: declaration uses 'sorry' -/
33-
#guard_msgs in
3427
example (h : n + 3 = m) (h' : n + 2 = m) : False := by
3528
change _ + 1 = _ at h h'
3629
guard_hyp h :ₛ n + 2 + 1 = m
3730
guard_hyp h' :ₛ n + 1 + 1 = m
38-
sorry
31+
exact test_sorry
3932

4033
-- `change ... at ...` preserves dependencies
41-
/-- warning: declaration uses 'sorry' -/
42-
#guard_msgs in
4334
example (p : n + 2 = m → Type) (h : n + 2 = m) (x : p h) : false := by
4435
change _ + 1 = _ at h
4536
guard_hyp x :ₛ p h
46-
sorry
37+
exact test_sorry
4738

48-
/-- warning: declaration uses 'sorry' -/
49-
#guard_msgs in
50-
example : Nat := by
39+
noncomputable example : Nat := by
5140
fail_if_success change Type 1
52-
sorry
41+
exact test_sorry
5342

5443
def foo (a b c : Nat) := if a < b then c else 0
5544

‎test/DefEqTransformations.lean‎

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ import Mathlib.Tactic.DefEqTransformations
22
import Mathlib.Init.Logic
33
import Std.Tactic.GuardExpr
44

5+
private axiom test_sorry : ∀ {α}, α
56
namespace Tests
67

78
example : id (1 = 1) := by
@@ -22,7 +23,7 @@ example : (fun x => 1 + x) 2 = (fun y => 2 + y) 3 := by
2223
beta_reduce
2324
guard_target =ₛ 1 + 2
2425
guard_target =ₛ 1 + 2 = (fun y => 2 + y) 3
25-
sorry
26+
exact test_sorry
2627

2728
example : 1 + 2 * 3 = 7 := by
2829
reduce
@@ -77,7 +78,7 @@ example : 1 + 2 = 2 + 1 := by
7778
example (m n : Nat) : (m == n) = true := by
7879
unfold_projs
7980
guard_target =ₛ Nat.beq m n = true
80-
sorry
81+
exact test_sorry
8182

8283
example (f : Nat → Nat) : (fun a => f a) = (fun a => f (f a)) := by
8384
eta_expand
@@ -86,7 +87,7 @@ example (f : Nat → Nat) : (fun a => f a) = (fun a => f (f a)) := by
8687
guard_target =ₛ f = fun a => f (f a)
8788
eta_expand
8889
guard_target =ₛ (fun a => f a) = (fun a => f (f a))
89-
sorry
90+
exact test_sorry
9091

9192
example : (fun (a b : Nat) => a + b) = (· + ·) := by
9293
eta_reduce
@@ -105,7 +106,7 @@ example : (fun (a : Nat) => 1 + a) = (1 + ·) := by
105106
example (f : Nat → Nat → Nat) : (fun x => f 1 x) 2 = 3 := by
106107
eta_expand
107108
guard_target =ₛ f 1 2 = 3
108-
sorry
109+
exact test_sorry
109110

110111
example : (fun (a : Nat) => 1 + a) 2 = (1 + ·) 2 := by
111112
eta_expand
@@ -115,12 +116,12 @@ example : (fun (a : Nat) => 1 + a) 2 = (1 + ·) 2 := by
115116
example (p : Nat × Nat) : (p.1, p.2) = (p.2, p.1) := by
116117
eta_struct
117118
guard_target =ₛ p = (p.2, p.1)
118-
sorry
119+
exact test_sorry
119120

120121
example (p : Nat × Nat) : ((p.1, p.2).1, (p.1, p.2).2) = ((p.1, p.2).2, (p.1, p.2).1) := by
121122
eta_struct
122123
guard_target =ₛ p = (p.2, p.1)
123-
sorry
124+
exact test_sorry
124125

125126
example (n : Fin 5) : n = ⟨n.1, n.2⟩ := by
126127
eta_struct

‎test/FBinop.lean‎

Lines changed: 17 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ import Mathlib.Data.Set.Prod
33
import Mathlib.Data.Finset.Prod
44
import Mathlib.Data.SetLike.Basic
55

6+
private axiom test_sorry : ∀ {α}, α
67
universe u v w
78
set_option autoImplicit true
89

@@ -28,31 +29,31 @@ instance : SProd' (Finset α) (Finset β) (Finset (α × β)) := ⟨Finset.produ
2829
example (s : Set α) (t : Set β) : s ×ˢ' t = s ×ˢ' t := rfl
2930
example {α : Type u} {β : Type v} (s : Finset α) (t : Finset β) : s ×ˢ' t = s ×ˢ' t := rfl
3031

31-
example (f : α × α → β) (s : Set (α × α)) : s.InjOn f := sorry
32-
example (f : α × α → β) (s t : Set α) : (s ×ˢ' t).InjOn f := sorry
33-
example (f : α × α → β) (s t : Finset α) : (s ×ˢ' t : Set (α × α)).InjOn f := sorry
34-
example (f : α × α → β) (s t : Finset α) : (s ×ˢ' t : Set _).InjOn f := sorry
35-
example (f : α × α → β) (s t : Finset α) : (s ×ˢ' t : Set _).InjOn f := sorry
36-
example (f : α × α → β) (s t : Finset α) : ((s : Set _) ×ˢ' (t : Set _)).InjOn f := sorry
37-
example (f : α × α → β) (s t : Finset α) : ((s : Set _) ×ˢ' (t : Set _)).InjOn f := sorry
38-
example (f : α × α → β) (s t : Finset α) : Set.InjOn f (s ×ˢ' t) := sorry
32+
example (f : α × α → β) (s : Set (α × α)) : s.InjOn f := test_sorry
33+
example (f : α × α → β) (s t : Set α) : (s ×ˢ' t).InjOn f := test_sorry
34+
example (f : α × α → β) (s t : Finset α) : (s ×ˢ' t : Set (α × α)).InjOn f := test_sorry
35+
example (f : α × α → β) (s t : Finset α) : (s ×ˢ' t : Set _).InjOn f := test_sorry
36+
example (f : α × α → β) (s t : Finset α) : (s ×ˢ' t : Set _).InjOn f := test_sorry
37+
example (f : α × α → β) (s t : Finset α) : ((s : Set _) ×ˢ' (t : Set _)).InjOn f := test_sorry
38+
example (f : α × α → β) (s t : Finset α) : ((s : Set _) ×ˢ' (t : Set _)).InjOn f := test_sorry
39+
example (f : α × α → β) (s t : Finset α) : Set.InjOn f (s ×ˢ' t) := test_sorry
3940

4041
axiom Nat.card : Sort u → Nat
41-
example (s : Finset α) (t : Finset γ) : Nat.card (s ×ˢ' t) = 0 := sorry
42+
example (s : Finset α) (t : Finset γ) : Nat.card (s ×ˢ' t) = 0 := test_sorry
4243

43-
example (s : Set α) (t : Set (α × ℕ)) : s ×ˢ' {n | 0 < n} = t := sorry
44-
example (s : Set α) (t : Set (α × ℕ)) : s ×ˢ' {1, 2, 3} = t := sorry
45-
example (s : Set α) (t : Set (ℕ × α)) : {1, 2, 3} ×ˢ' s = t := sorry
44+
example (s : Set α) (t : Set (α × ℕ)) : s ×ˢ' {n | 0 < n} = t := test_sorry
45+
example (s : Set α) (t : Set (α × ℕ)) : s ×ˢ' {1, 2, 3} = t := test_sorry
46+
example (s : Set α) (t : Set (ℕ × α)) : {1, 2, 3} ×ˢ' s = t := test_sorry
4647

4748
-- These need `fbinop%`. (Comment out `macro_rules` above to check.)
4849

4950
example {α : Type u} {β : Type v} (s : Finset α) (t : Set β) : s ×ˢ' t = s ×ˢ' t := rfl
50-
example (s : Finset α) (t : Finset (α × ℕ)) : s ×ˢ' {1, 2, 3} = t := sorry
51-
example (s : Finset α) (t : Finset (ℕ × α)) : {1, 2, 3} ×ˢ' s = t := sorry
52-
example (s : Finset α) (t : Finset (ℕ × α)) : ({1, 2, 3} ×ˢ' s).card = 22 := sorry
51+
example (s : Finset α) (t : Finset (α × ℕ)) : s ×ˢ' {1, 2, 3} = t := test_sorry
52+
example (s : Finset α) (t : Finset (ℕ × α)) : {1, 2, 3} ×ˢ' s = t := test_sorry
53+
example (s : Finset α) (_t : Finset (ℕ × α)) : ({1, 2, 3} ×ˢ' s).card = 22 := test_sorry
5354
#check ({1,2,3} ×ˢ' {4,5,6} : Finset _)
5455

55-
example (s : Finset α) (t : Set β) (u : Finset γ) : Nat.card (s ×ˢ' t ×ˢ' u) = 0 := sorry
56+
example (s : Finset α) (t : Set β) (u : Finset γ) : Nat.card (s ×ˢ' t ×ˢ' u) = 0 := test_sorry
5657

5758
example (s : Finset α) (t : Finset β) :
5859
(↑(s ×ˢ' t) : Set _) = (s : Set α) ×ˢ' t := Finset.coe_product s t

‎test/GCongr/inequalities.lean‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ import Mathlib.Tactic.GCongr
99
import Mathlib.Tactic.SuccessIfFailWithMsg
1010
import Mathlib.Tactic.NormNum.OfScientific
1111

12+
private axiom test_sorry : ∀ {α}, α
1213
/-! # Inequality tests for the `gcongr` tactic -/
1314

1415
open Nat Finset BigOperators
@@ -110,10 +111,10 @@ example {a b x c d : ℝ} (h1 : a ≤ b) (h2 : c ≤ d) (h3 : 1 ≤ x + 1) : x *
110111

111112
-- test for a missing `withContext`
112113
example {x y : ℚ} {n : ℕ} (hx : 0 ≤ x) (hn : 0 < n) : y ≤ x := by
113-
have h : x < y := sorry
114-
have : x ^ n < y ^ n
114+
have h : x < y := test_sorry
115+
have _this : x ^ n < y ^ n
115116
· rel [h] -- before bugfix: complained "unknown identifier 'h'"
116-
sorry
117+
exact test_sorry
117118

118119
/-! ## Non-finishing examples -/
119120

‎test/GeneralizeProofs.lean‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,15 +3,16 @@ import Mathlib.Tactic.GeneralizeProofs
33
import Std.Tactic.GuardExpr
44
import Mathlib.Tactic.LibrarySearch
55

6+
private axiom test_sorry : ∀ {α}, α
67
set_option autoImplicit true
7-
def List.nthLe (l : List α) (n) (h : n < l.length) : α := sorry
8+
noncomputable def List.nthLe (l : List α) (n) (_h : n < l.length) : α := test_sorry
89

910
example : List.nthLe [1, 2] 1 (by simp) = 2 := by
1011
-- ⊢ [1 2].nth_le 1 _ = 2
1112
generalize_proofs h
1213
-- h : 1 < [1 2].length
1314
-- ⊢ [1 2].nth_le 1 h = 2
14-
sorry
15+
exact test_sorry
1516

1617
example (x : ℕ) (h : x < 2) : Classical.choose (⟨x, h⟩ : ∃ x, x < 2) < 2 := by
1718
generalize_proofs a
@@ -30,20 +31,20 @@ example (x : ℕ) (h : x < 2) : Classical.choose (⟨x, h⟩ : ∃ x, x < 2) =
3031
generalize_proofs a
3132
guard_hyp a : ∃ x, x < 2
3233
guard_target = Classical.choose a = Classical.choose _
33-
sorry
34+
exact test_sorry
3435

3536
example (x : ℕ) (h : x < 2) : Classical.choose (⟨x, h⟩ : ∃ x, x < 2) =
3637
Classical.choose (⟨x, Nat.lt_succ_of_lt h⟩ : ∃ x, x < 3) := by
3738
generalize_proofs
3839
guard_target = Classical.choose _ = Classical.choose _
39-
sorry
40+
exact test_sorry
4041

4142
example (x : ℕ) (h : x < 2) : Classical.choose (⟨x, h⟩ : ∃ x, x < 2) =
4243
Classical.choose (⟨x, Nat.lt_succ_of_lt h⟩ : ∃ x, x < 3) := by
4344
generalize_proofs _ a
4445
guard_hyp a : ∃ x, x < 3
4546
guard_target = Classical.choose _ = Classical.choose a
46-
sorry
47+
exact test_sorry
4748

4849
example (a : ∃ x, x < 2) : Classical.choose a < 2 := by
4950
generalize_proofs

‎test/ImplicitUniverses.lean‎

Lines changed: 12 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,42 +1,43 @@
11
import Mathlib.Tactic.Basic
22
import Mathlib.Tactic.SuccessIfFailWithMsg
33

4-
example (x y : Type*) : sorry := by
4+
private axiom test_sorry : ∀ {α}, α
5+
noncomputable example (_x _y : Type*) : test_sorry := by
56
success_if_fail_with_msg
67
"type mismatch
7-
y
8+
_y
89
has type
910
Type u_2 : Type (u_2 + 1)
1011
but is expected to have type
11-
Type u_1 : Type (u_1 + 1)" (exact x = y)
12-
sorry
12+
Type u_1 : Type (u_1 + 1)" (exact _x = _y)
13+
exact test_sorry
1314

14-
example (x : Sort*) : sorry := by
15+
noncomputable example (_x : Sort*) : test_sorry := by
1516
success_if_fail_with_msg
1617
"type mismatch
1718
Prop
1819
has type
1920
Type : Type 1
2021
but is expected to have type
21-
Sort u_1 : Type u_1" (exact x = Prop)
22-
sorry
22+
Sort u_1 : Type u_1" (exact _x = Prop)
23+
exact test_sorry
2324

24-
example : sorry := by
25+
noncomputable example : test_sorry := by
2526
success_if_fail_with_msg
2627
"type mismatch
2728
y
2829
has type
2930
Type u_2 : Type (u_2 + 1)
3031
but is expected to have type
3132
Type u_1 : Type (u_1 + 1)" (exact ∀ x y : Type*, x = y)
32-
sorry
33+
exact test_sorry
3334

34-
example : sorry := by
35+
noncomputable example : test_sorry := by
3536
success_if_fail_with_msg
3637
"type mismatch
3738
Prop
3839
has type
3940
Type : Type 1
4041
but is expected to have type
4142
Sort u_1 : Type u_1" (exact ∀ x : Sort*, x = Prop)
42-
sorry
43+
exact test_sorry

‎test/InstanceTransparency.lean‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,18 +13,19 @@ This file checks that this and similar tricks have had the desired effect:
1313
`with_reducible_and_instances apply mul_le_mul` fails although `apply mul_le_mul` succeeds.
1414
-/
1515

16+
private axiom test_sorry : ∀ {α}, α
1617
set_option autoImplicit true
1718

1819
example {a b : α} [LinearOrderedField α] : a / 2 ≤ b / 2 := by
1920
fail_if_success with_reducible_and_instances apply mul_le_mul -- fails, as desired
20-
sorry
21+
exact test_sorry
2122

2223
example {a b : ℚ} : a / 2 ≤ b / 2 := by
2324
fail_if_success with_reducible_and_instances apply mul_le_mul -- fails, as desired
2425
apply mul_le_mul
25-
repeat sorry
26+
repeat exact test_sorry
2627

2728
example {a b : ℝ} : a / 2 ≤ b / 2 := by
2829
fail_if_success with_reducible_and_instances apply mul_le_mul -- fails, as desired
2930
apply mul_le_mul
30-
repeat sorry
31+
repeat exact test_sorry

‎test/LibrarySearch/IsCompact.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,11 @@ import Mathlib.Topology.Instances.Real
22
import Mathlib.Topology.Algebra.Order.Compact
33
import Mathlib.Tactic.LibrarySearch
44

5+
set_option pp.unicode.fun true
6+
7+
-- TODO: uses sorry, but is hidden behind the `apply?`
8+
/-- warning: declaration uses 'sorry' -/
9+
#guard_msgs(warning, drop info) in
510
example (f : ℝ → ℝ) {K : Set ℝ} (_hK : IsCompact K) : ∃ x ∈ K, ∀ y ∈ K, f x ≤ f y := by
611
fail_if_success exact?
712
apply? -- Verify that this includes: `refine IsCompact.exists_forall_le _hK ?_ ?_`

‎test/LiftLets.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
import Mathlib.Tactic.LiftLets
22
import Std.Tactic.GuardExpr
33

4+
private axiom test_sorry : ∀ {α}, α
45
set_option autoImplicit true
56

67
example : (let x := 1; x) = 1 := by
@@ -105,4 +106,4 @@ example (m : Nat) (h : ∃ n, n + 1 = m) (x : Fin m) (y : Fin _) :
105106
intro h'
106107
clear_value h'
107108
guard_hyp h' : m = Exists.choose h + 1
108-
sorry
109+
exact test_sorry

0 commit comments

Comments
 (0)