From 755de48ff318dcf370037c969374148dc56d458e Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Thu, 29 Feb 2024 15:12:52 +1100 Subject: [PATCH] chore: upstream orphaned tests from Std (#3539) --- tests/lean/run/decidability_timeout.lean | 6 + tests/lean/run/ext.lean | 106 +++++++++ tests/lean/run/guard_expr.lean | 58 +++++ tests/lean/run/int_complement_shiftRight.lean | 15 ++ tests/lean/run/json.lean | 22 ++ tests/lean/run/left_right.lean | 66 ++++++ tests/lean/run/omega_examples.lean | 57 +++++ tests/lean/run/rcases.lean | 211 ++++++++++++++++++ tests/lean/run/repeat.lean | 13 ++ tests/lean/run/solve_by_elim.lean | 152 +++++++++++++ tests/lean/run/symm.lean | 27 +++ 11 files changed, 733 insertions(+) create mode 100644 tests/lean/run/decidability_timeout.lean create mode 100644 tests/lean/run/ext.lean create mode 100644 tests/lean/run/guard_expr.lean create mode 100644 tests/lean/run/int_complement_shiftRight.lean create mode 100644 tests/lean/run/json.lean create mode 100644 tests/lean/run/left_right.lean create mode 100644 tests/lean/run/omega_examples.lean create mode 100644 tests/lean/run/rcases.lean create mode 100644 tests/lean/run/repeat.lean create mode 100644 tests/lean/run/solve_by_elim.lean create mode 100644 tests/lean/run/symm.lean diff --git a/tests/lean/run/decidability_timeout.lean b/tests/lean/run/decidability_timeout.lean new file mode 100644 index 0000000000..eefc382d3c --- /dev/null +++ b/tests/lean/run/decidability_timeout.lean @@ -0,0 +1,6 @@ + +-- Prior to leanprover/lean4#2552 there was a performance trap +-- depending on the implementation details in `decidableBallLT`. +-- We keep this example (which would have gone over maxHeartbeats) +-- as a regression test for the instance. +example : ∀ m, m < 25 → ∀ n, n < 25 → ∀ c, c < 25 → m ^ 2 + n ^ 2 + c ^ 2 ≠ 7 := by decide diff --git a/tests/lean/run/ext.lean b/tests/lean/run/ext.lean new file mode 100644 index 0000000000..e628caf53d --- /dev/null +++ b/tests/lean/run/ext.lean @@ -0,0 +1,106 @@ + +set_option linter.missingDocs false +axiom mySorry {α : Sort _} : α + +structure A (n : Nat) where + a : Nat + +example (a b : A n) : a = b ∨ True := by + fail_if_success + apply Or.inl; ext + exact Or.inr trivial + +structure B (n) extends A n where + b : Nat + h : b > 0 + i : Fin b + +@[ext] structure C (n) extends B n where + c : Nat + +example (a b : C n) : a = b := by + ext + guard_target = a.a = b.a; exact mySorry + guard_target = a.b = b.b; exact mySorry + guard_target = HEq a.i b.i; exact mySorry + guard_target = a.c = b.c; exact mySorry + +@[ext (flat := false)] structure C' (n) extends B n where + c : Nat + +example (a b : C' n) : a = b := by + ext + guard_target = a.toB = b.toB; exact mySorry + guard_target = a.c = b.c; exact mySorry + +example (f g : Nat × Nat → Nat) : f = g := by + ext ⟨x, y⟩ + guard_target = f (x, y) = g (x, y); exact mySorry + +-- Check that we generate a warning if there are too many patterns. +/-- warning: `ext` did not consume the patterns: [j] [linter.unusedRCasesPattern] -/ +#guard_msgs in +example (f g : Nat → Nat) (h : f = g) : f = g := by + ext i j + exact h ▸ rfl + +-- allow more specific ext theorems +@[ext high] theorem Fin.zero_ext (a b : Fin 0) : True → a = b := by cases a.isLt +example (a b : Fin 0) : a = b := by ext; exact True.intro + +def Set (α : Type u) := α → Prop +@[ext] structure LocalEquiv (α : Type u) (β : Type v) where + source : Set α +@[ext] structure Pretrivialization {F : Type u} (proj : Z → β) extends LocalEquiv Z (β × F) where + baseSet : Set β + source_eq : source = baseSet ∘ proj + +structure MyUnit + +@[ext high] theorem MyUnit.ext1 (x y : MyUnit) (_h : 0 = 1) : x = y := rfl +@[ext high] theorem MyUnit.ext2 (x y : MyUnit) (_h : 1 = 1) : x = y := rfl +@[ext] theorem MyUnit.ext3 (x y : MyUnit) (_h : 2 = 1) : x = y := rfl + +example (x y : MyUnit) : x = y := by ext; rfl + +-- Check that we don't generate a warning when `x` only uses a pattern in one branch: +example (f : ℕ × (ℕ → ℕ)) : f = f := by + ext x + · rfl + · guard_target = (f.2) x = (f.2) x + rfl + +example (f : Empty → Empty) : f = f := by + ext ⟨⟩ + +@[ext] theorem ext_intros {n m : Nat} (w : ∀ n m : Nat, n = m) : n = m := by apply w + +#guard_msgs (drop warning) in +example : 3 = 7 := by + ext : 1 + rename_i n m + guard_target = n = m + admit + +#guard_msgs (drop warning) in +example : 3 = 7 := by + ext n m : 1 + guard_target = n = m + admit + +section erasing_ext_attribute + +def f (p : Int × Int) : Int × Int := (p.2, p.1) + +example : f ∘ f = id := by + ext ⟨a, b⟩ + · simp [f] + · simp [f] + +attribute [-ext] Prod.ext + +example : f ∘ f = id := by + ext ⟨a, b⟩ + simp [f] + +end erasing_ext_attribute diff --git a/tests/lean/run/guard_expr.lean b/tests/lean/run/guard_expr.lean new file mode 100644 index 0000000000..e03e679c17 --- /dev/null +++ b/tests/lean/run/guard_expr.lean @@ -0,0 +1,58 @@ + +example (n : Nat) : Nat := by + guard_hyp n :ₛ Nat + let m : Nat := 1 + guard_expr 1 =ₛ (by exact 1) + fail_if_success guard_expr 1 = (by exact 2) + guard_hyp m := 1 + guard_hyp m : (fun x => x) Nat :=~ id 1 + guard_target = Nat + have : 1 = 1 := by conv => + guard_hyp m := 1 + guard_expr ‹Nat› = m + fail_if_success guard_target = 1 + lhs + guard_target = 1 + exact 0 + +-- Now with a generic type to test that default instances work correctly +example [∀ n, OfNat α n] (n : α) : α := by + guard_hyp n + fail_if_success guard_hyp m + guard_hyp n :ₛ α + let q : α := 1 + guard_expr (1 : α) =ₛ 1 + fail_if_success guard_expr 1 =ₛ (2 : α) + fail_if_success guard_expr 1 =ₛ (by exact (2 : α)) + guard_hyp q := 1 + guard_hyp q : α := 1 + guard_hyp q : (fun x => x) α :=~ id 1 + guard_target = α + have : (1 : α) = 1 := by conv => + guard_hyp q := 1 + guard_expr ‹α› = q + fail_if_success guard_target = 1 + lhs + guard_target = 1 + exact 0 + +#guard_expr 1 = 1 +#guard_expr 1 =ₛ 1 +#guard_expr 2 = 1 + 1 + +section +variable {α : Type} [∀ n, OfNat α n] +#guard_expr (1 : α) = 1 +end + +#guard true +#guard 2 == 1 + 1 +#guard 2 = 1 + 1 + +instance (p : Bool → Prop) [DecidablePred p] : Decidable (∀ b, p b) := + if h : p false ∧ p true then + isTrue (by { intro b; cases h; cases b <;> assumption }) + else + isFalse (by { intro h'; simp [h'] at h }) + +#guard ∀ (b : Bool), b = !!b diff --git a/tests/lean/run/int_complement_shiftRight.lean b/tests/lean/run/int_complement_shiftRight.lean new file mode 100644 index 0000000000..65397bfaca --- /dev/null +++ b/tests/lean/run/int_complement_shiftRight.lean @@ -0,0 +1,15 @@ + +-- complement +#guard ~~~(-1:Int) = 0 +#guard ~~~(0:Int) = -1 +#guard ~~~(1:Int) = -2 +#guard ~~~(-2:Int) = 1 + +-- shiftRight +#guard (2:Int) >>> 1 = 1 +#guard (0:Int) >>> 1 = 0 +#guard ~~~(1:Int) >>> 1 = ~~~0 +#guard ~~~(0:Int) >>> 1 = ~~~0 +#guard ~~~(2:Int) >>> 1 = ~~~1 +#guard ~~~(4:Int) >>> 1 = ~~~2 +#guard ~~~(4:Int) >>> 2 = ~~~1 diff --git a/tests/lean/run/json.lean b/tests/lean/run/json.lean new file mode 100644 index 0000000000..8755ab9126 --- /dev/null +++ b/tests/lean/run/json.lean @@ -0,0 +1,22 @@ +import Lean.Data.Json.Elab + +/-- info: {"lookACalc": 131, + "lemonCount": 100000000000000000000000000000000, + "isCool": true, + "isBug": null, + "hello": "world", + "cheese": ["edam", "cheddar", {"rank": 100.2, "kind": "spicy"}]}-/ +#guard_msgs in +#eval json% { + hello : "world", + cheese : ["edam", "cheddar", {kind : "spicy", rank : 100.2}], + lemonCount : 100e30, + isCool : true, + isBug : null, + lookACalc: $(23 + 54 * 2) +} + +-- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/json.20elaborator +example : Lean.Json := Id.run do + let _x := true + return json% {"x" : 1} diff --git a/tests/lean/run/left_right.lean b/tests/lean/run/left_right.lean new file mode 100644 index 0000000000..cf65bee79c --- /dev/null +++ b/tests/lean/run/left_right.lean @@ -0,0 +1,66 @@ + +/-- Construct a natural number using `left`. -/ +def zero : Nat := by + left + +example : zero = 0 := rfl + +/-- Construct a natural number using `right`. -/ +def two : Nat := by + right + exact 1 + +example : two = 2 := rfl + +set_option linter.missingDocs false + +/-- +error: tactic 'left' failed, +left tactic works for inductive types with exactly 2 constructors +⊢ Unit +-/ +#guard_msgs in +example : Unit := by + left + +inductive F +| a | b | c + +/-- +error: tactic 'left' failed, +left tactic works for inductive types with exactly 2 constructors +⊢ F +-/ +#guard_msgs in +example : F := by + left + +def G := Nat + +/-- Look through definitions. -/ +example : G := by + left + +/-- +error: tactic 'left' failed, target is not an inductive datatype +⊢ Type +-/ +#guard_msgs in +example : Type := by + left + +example : Sum Nat (List Nat) := by + left + exact zero + +example : Sum Nat (List Nat) := by + right + exact [0] + +example : (1 = 1) ∨ (2 = 3) := by + left + rfl + +example : (1 = 2) ∨ (3 = 3) := by + right + rfl diff --git a/tests/lean/run/omega_examples.lean b/tests/lean/run/omega_examples.lean new file mode 100644 index 0000000000..8e6603435e --- /dev/null +++ b/tests/lean/run/omega_examples.lean @@ -0,0 +1,57 @@ + +-- Turn on `trace.omega` to get detailed information about the processing of hypotheses, +-- and the justification of the contradiction found. +-- set_option trace.omega true + +-- Inequalities +example {x y : Nat} (_ : x + y > 10) (_ : x < 5) (_ : y < 5) : False := by omega + +-- Tightening inequalities over `Int` or `Nat` +example {x y : Nat} (_ : x + y > 10) (_ : 2 * x < 11) (_ : y < 5) : False := by omega + +-- GCDs not dividing constant terms +example {x y : Nat} (_ : 2 * x + 4 * y = 5) : False := by omega + +-- Eliminating variables even when no coefficient is ±1 +example {x y : Nat} (_ : 6 * x + 7 * y = 5) : False := by omega + +-- Case bashing on `Nat.sub` +example {x y z : Nat} (_ : x - y - z = 0) (_ : x > y + z) : False := by omega + +-- Division with constant denominators +example {x y : Nat} (_ : x / 2 - y / 3 < 1) (_ : 3 * x ≥ 2 * y + 4) : False := by omega + +-- Annoying casts +example {x : Nat} : 1 < (1 + ((x + 1 : Nat) : Int) + 2) / 2 := by omega + +-- Divisibility +example {x : Nat} (_ : 10000 ∣ x) (_ : ¬ 100 ∣ x) : False := by omega + +-- Mod +example (x : Nat) : x % 1024 - x % 2048 = 0 := by omega + +-- Systems of equations +example (a b c d e : Int) + (ha : 2 * a + b + c + d + e = 4) + (hb : a + 2 * b + c + d + e = 5) + (hc : a + b + 2 * c + d + e = 6) + (hd : a + b + c + 2 * d + e = 7) + (he : a + b + c + d + 2 * e = 8) : e = 3 := by omega + +-- Case bashing on disjunctions +example (a b c d e : Int) + (ha : 2 * a + b + c + d + e = 4) + (hb : a + 2 * b + c + d + e = 5) + (hc : a + b + 2 * c + d + e = 6) + (hd : a + b + c + 2 * d + e = 7) + (he : a + b + c + d + 2 * e = 8 ∨ e = 3) : e = 3 := by omega + +-- Case bashing conjunctions in the goal +example (ε : Int) (_ : ε > 0) : (ε - 2 ≤ ε / 3 + ε / 2 + ε / 2) ∧ (ε / 3 + ε / 4 + ε / 5 ≤ ε) := by + omega + +-- Fast results with duplicated hypotheses +example {x : Int} (h₁ : 0 ≤ 2 * x + 1) (h₂ : 2 * x + 1 ≤ 0) : False := by + iterate 64 have := h₁ + iterate 64 have := h₂ + omega diff --git a/tests/lean/run/rcases.lean b/tests/lean/run/rcases.lean new file mode 100644 index 0000000000..466d5508ba --- /dev/null +++ b/tests/lean/run/rcases.lean @@ -0,0 +1,211 @@ +import Lean.Elab.Tactic.Basic + +set_option linter.missingDocs false + +example (x : α × β × γ) : True := by + rcases x with ⟨a, b, c⟩ + guard_hyp a : α + guard_hyp b : β + guard_hyp c : γ + trivial + +example (x : α × β × γ) : True := by + rcases x with ⟨(a : α) : id α, -, c : id γ⟩ + guard_hyp a : α + fail_if_success have : β := by assumption + guard_hyp c : id γ + trivial + +example (x : (α × β) × γ) : True := by + fail_if_success rcases x with ⟨_a, b, c⟩ + fail_if_success rcases x with ⟨⟨a:β, b⟩, c⟩ + rcases x with ⟨⟨a:α, b⟩, c⟩ + guard_hyp a : α + guard_hyp b : β + guard_hyp c : γ + trivial + +example : @Inhabited.{1} α × Option β ⊕ γ → True := by + rintro (⟨⟨a⟩, _ | b⟩ | c) + · guard_hyp a : α; trivial + · guard_hyp a : α; guard_hyp b : β; trivial + · guard_hyp c : γ; trivial + +example : cond false Nat Int → cond true Int Nat → Nat ⊕ Unit → True := by + rintro (x y : Int) (z | u) + · guard_hyp x : Int; guard_hyp y : Int; guard_hyp z : Nat; trivial + · guard_hyp x : Int; guard_hyp y : Int; guard_hyp u : Unit; trivial + +example (x y : Nat) (h : x = y) : True := by + rcases x with _|⟨⟩|z + · guard_hyp h : Nat.zero = y; trivial + · guard_hyp h : Nat.succ Nat.zero = y; trivial + · guard_hyp z : Nat + guard_hyp h : Nat.succ (Nat.succ z) = y; trivial + +example (h : x = 3) (h₂ : x < 4) : x < 4 := by + rcases h with ⟨⟩ + guard_hyp h₂ : 3 < 4; guard_target = 3 < 4; exact h₂ + +example (h : x = 3) (h₂ : x < 4) : x < 4 := by + rcases h with rfl + guard_hyp h₂ : 3 < 4; guard_target = 3 < 4; exact h₂ + +example (h : 3 = x) (h₂ : x < 4) : x < 4 := by + rcases h with ⟨⟩ + guard_hyp h₂ : 3 < 4; guard_target = 3 < 4; exact h₂ + +example (h : 3 = x) (h₂ : x < 4) : x < 4 := by + rcases h with rfl + guard_hyp h₂ : 3 < 4; guard_target = 3 < 4; exact h₂ + +example (s : α ⊕ Empty) : True := by + rcases s with s|⟨⟨⟩⟩ + guard_hyp s : α; trivial + +example : True := by + obtain ⟨n : Nat, _h : n = n, -⟩ : ∃ n : Nat, n = n ∧ True + · exact ⟨0, rfl, trivial⟩ + trivial + +example : True := by + obtain (h : True) | ⟨⟨⟩⟩ : True ∨ False + · exact Or.inl trivial + guard_hyp h : True; trivial + +example : True := by + obtain h | ⟨⟨⟩⟩ : True ∨ False := Or.inl trivial + guard_hyp h : True; trivial + +example : True := by + obtain ⟨h, h2⟩ := And.intro trivial trivial + guard_hyp h : True; guard_hyp h2 : True; trivial + +example : True := by + fail_if_success obtain ⟨h, h2⟩ + trivial + +example (x y : α × β) : True := by + rcases x, y with ⟨⟨a, b⟩, c, d⟩ + guard_hyp a : α; guard_hyp b : β + guard_hyp c : α; guard_hyp d : β + trivial + +example (x y : α ⊕ β) : True := by + rcases x, y with ⟨a|b, c|d⟩ + · guard_hyp a : α; guard_hyp c : α; trivial + · guard_hyp a : α; guard_hyp d : β; trivial + · guard_hyp b : β; guard_hyp c : α; trivial + · guard_hyp b : β; guard_hyp d : β; trivial + +example (i j : Nat) : (Σ' x, i ≤ x ∧ x ≤ j) → i ≤ j := by + intro h + rcases h' : h with ⟨x, h₀, h₁⟩ + guard_hyp h' : h = ⟨x, h₀, h₁⟩ + apply Nat.le_trans h₀ h₁ + +example (x : Quot fun _ _ : α => True) (h : x = x): x = x := by + rcases x with ⟨z⟩ + guard_hyp z : α + guard_hyp h : Quot.mk (fun _ _ => True) z = Quot.mk (fun _ _ => True) z + guard_target = Quot.mk (fun _ _ => True) z = Quot.mk (fun _ _ => True) z + exact h + +example (n : Nat) : True := by + obtain _one_lt_n | _n_le_one : 1 < n + 1 ∨ n + 1 ≤ 1 := Nat.lt_or_ge 1 (n + 1) + {trivial}; trivial + +example (n : Nat) : True := by + obtain _one_lt_n | (_n_le_one : n + 1 ≤ 1) := Nat.lt_or_ge 1 (n + 1) + {trivial}; trivial + +open Lean Elab Tactic in +/-- Asserts that the goal has `n` hypotheses. Used for testing. -/ +elab "check_num_hyps " n:num : tactic => liftMetaMAtMain fun _ => do + -- +1 because the _example recursion decl is in the list + guard $ (← getLCtx).foldl (fun i _ => i+1) 0 = n.1.toNat + 1 + +example (h : ∃ x : Nat, x = x ∧ 1 = 1) : True := by + rcases h with ⟨-, _⟩ + check_num_hyps 0 + trivial + +example (h : ∃ x : Nat, x = x ∧ 1 = 1) : True := by + rcases h with ⟨-, _, h⟩ + check_num_hyps 1 + guard_hyp h : 1 = 1 + trivial + +example (h : True ∨ True ∨ True) : True := by + rcases h with - | - | - + iterate 3 · check_num_hyps 0; trivial + +example (h : True ∨ True ∨ True) : True := by + rcases h with -|-|- + iterate 3 · check_num_hyps 0; trivial + +example : Bool → False → True +| false => by rintro ⟨⟩ +| true => by rintro ⟨⟩ + +example : (b : Bool) → cond b False False → True := by + rintro ⟨⟩ ⟨⟩ + +structure Baz {α : Type _} (f : α → α) : Prop where + [inst : Nonempty α] + h : f ∘ f = id + +example {α} (f : α → α) (h : Baz f) : True := by rcases h with ⟨_⟩; trivial + +example {α} (f : α → α) (h : Baz f) : True := by rcases h with @⟨_, _⟩; trivial + +inductive Test : Nat → Prop + | a (n) : Test (2 + n) + | b {n} : n > 5 → Test (n * n) + +example {n} (h : Test n) : n = n := by + have : True := by + rcases h with (a | b) + · guard_hyp a : Nat + trivial + · guard_hyp b : ‹Nat› > 5 + trivial + · rcases h with (a | @⟨n, b⟩) + · guard_hyp a : Nat + trivial + · guard_hyp b : n > 5 + trivial + +example (h : a ≤ 2 ∨ 2 < a) : True := by + obtain ha1 | ha2 : a ≤ 2 ∨ 3 ≤ a := h + · guard_hyp ha1 : a ≤ 2; trivial + · guard_hyp ha2 : 3 ≤ a; trivial + +example (h : a ≤ 2 ∨ 2 < a) : True := by + obtain ha1 | ha2 : a ≤ 2 ∨ 3 ≤ a := id h + · guard_hyp ha1 : a ≤ 2; trivial + · guard_hyp ha2 : 3 ≤ a; trivial + +example (a : Nat) : True := by + rcases h : a with _ | n + · guard_hyp h : a = 0; trivial + · guard_hyp h : a = n + 1; trivial + +inductive BaseType : Type where + | one + +inductive BaseTypeHom : BaseType → BaseType → Type where + | loop : BaseTypeHom one one + | id (X : BaseType) : BaseTypeHom X X + +example : BaseTypeHom one one → Unit := by rintro ⟨_⟩ <;> constructor + +axiom test_sorry {α} : α +example (b c : Nat) : True := by + obtain rfl : b = c ^ 2 := test_sorry + trivial + +example (b c : Nat) : True := by + obtain h : b = c ^ 2 := test_sorry + subst h + trivial diff --git a/tests/lean/run/repeat.lean b/tests/lean/run/repeat.lean new file mode 100644 index 0000000000..3ef3987f81 --- /dev/null +++ b/tests/lean/run/repeat.lean @@ -0,0 +1,13 @@ +import Lean.Elab.Tactic.Basic +import Lean.Meta.Tactic.Util + +open Lean Elab Tactic Meta + +elab "foo" : tactic => liftMetaTactic fun g => do + g.assign (← mkFreshExprMVar (← g.getType)) + throwError "" + +#guard_msgs in +example : True := by + repeat' foo + trivial diff --git a/tests/lean/run/solve_by_elim.lean b/tests/lean/run/solve_by_elim.lean new file mode 100644 index 0000000000..08d5500d89 --- /dev/null +++ b/tests/lean/run/solve_by_elim.lean @@ -0,0 +1,152 @@ +/- +Copyright (c) 2021 Scott Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ + +import Lean.Meta.Tactic.Constructor +import Lean.Elab.SyntheticMVars +import Lean.Elab.Tactic.SolveByElim -- FIXME we need to make SolveByElimConfig builtin + +set_option autoImplicit true + +example (h : Nat) : Nat := by solve_by_elim +example {α β : Type} (f : α → β) (a : α) : β := by solve_by_elim +example {α β : Type} (f : α → α → β) (a : α) : β := by solve_by_elim +example {α β γ : Type} (f : α → β) (g : β → γ) (a : α) : γ := by solve_by_elim +example {α β γ : Type} (_f : α → β) (g : β → γ) (b : β) : γ := by solve_by_elim +example {α : Nat → Type} (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by solve_by_elim + +example (h : Nat) : Nat := by solve_by_elim [] +example {α β : Type} (f : α → β) (a : α) : β := by solve_by_elim [] +example {α β : Type} (f : α → α → β) (a : α) : β := by solve_by_elim [] +example {α β γ : Type} (f : α → β) (g : β → γ) (a : α) : γ := by solve_by_elim [] +example {α β γ : Type} (_f : α → β) (g : β → γ) (b : β) : γ := by solve_by_elim [] +example {α : Nat → Type} (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by solve_by_elim [] + +example {α β : Type} (f : α → β) (a : α) : β := by + fail_if_success solve_by_elim [-f] + fail_if_success solve_by_elim [-a] + fail_if_success solve_by_elim only [f] + solve_by_elim + +example {α β γ : Type} (f : α → β) (g : β → γ) (b : β) : γ := by + fail_if_success solve_by_elim [-g] + solve_by_elim [-f] + +example (h : Nat) : Nat := by solve_by_elim only [h] +example {α β : Type} (f : α → β) (a : α) : β := by solve_by_elim only [f, a] +example {α β : Type} (f : α → α → β) (a : α) : β := by solve_by_elim only [f, a] +example {α β γ : Type} (f : α → β) (g : β → γ) (a : α) : γ := by solve_by_elim only [f, g, a] +example {α β γ : Type} (_f : α → β) (g : β → γ) (b : β) : γ := by solve_by_elim only [g, b] +example {α : Nat → Type} (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by + solve_by_elim only [f, a] + +set_option linter.unusedVariables false in +example (h₁ h₂ : False) : True := by + -- 'It doesn't make sense to remove local hypotheses when using `only` without `*`.' + fail_if_success solve_by_elim only [-h₁] + -- 'It does make sense to use `*` without `only`.' + fail_if_success solve_by_elim [*, -h₁] + solve_by_elim only [*, -h₁] + +-- Verify that already assigned metavariables are skipped. +example (P₁ P₂ : α → Prop) (f : ∀ (a : α), P₁ a → P₂ a → β) + (a : α) (ha₁ : P₁ a) (ha₂ : P₂ a) : β := by + solve_by_elim + +example {X : Type} (x : X) : x = x := by + fail_if_success solve_by_elim (config := {constructor := false}) only -- needs the `rfl` lemma + solve_by_elim + +-- Needs to apply `rfl` twice, with different implicit arguments each time. +-- A naive implementation of solve_by_elim would get stuck. +example {X : Type} (x y : X) (p : Prop) (h : x = x → y = y → p) : p := by solve_by_elim + +example : True := by + fail_if_success solve_by_elim (config := {constructor := false}) only -- needs the `trivial` lemma + solve_by_elim + +-- Requires backtracking. +example (P₁ P₂ : α → Prop) (f : ∀ (a: α), P₁ a → P₂ a → β) + (a : α) (_ha₁ : P₁ a) + (a' : α) (ha'₁ : P₁ a') (ha'₂ : P₂ a') : β := by + fail_if_success solve_by_elim (config := .noBackTracking) + solve_by_elim + +attribute [symm] Eq.symm in +example {α : Type} {a b : α → Prop} (h₀ : b = a) (y : α) : a y = b y := by + fail_if_success solve_by_elim (config := {symm := false}) + solve_by_elim + +example (P : True → False) : 3 = 7 := by + fail_if_success solve_by_elim (config := {exfalso := false}) + solve_by_elim + +-- Verifying that `solve_by_elim` acts only on the main goal. +example (n : Nat) : Nat × Nat := by + constructor + solve_by_elim + solve_by_elim + +-- Verifying that `solve_by_elim*` acts on all remaining goals. +example (n : Nat) : Nat × Nat := by + constructor + solve_by_elim* + +open Lean Elab Tactic in +/-- +`fconstructor` is like `constructor` +(it calls `apply` using the first matching constructor of an inductive datatype) +except that it does not reorder goals. +-/ +elab "fconstructor" : tactic => withMainContext do + let mvarIds' ← (← getMainGoal).constructor {newGoals := .all} + Term.synthesizeSyntheticMVarsNoPostponing + replaceMainGoal mvarIds' + +-- Verifying that `solve_by_elim*` backtracks when given multiple goals. +example (n m : Nat) (f : Nat → Nat → Prop) (h : f n m) : ∃ p : Nat × Nat, f p.1 p.2 := by + fconstructor + fconstructor + solve_by_elim* + +-- test that metavariables created for implicit arguments don't get stuck +example (P : Nat → Type) (f : {n : Nat} → P n) : P 2 × P 3 := by + fconstructor + solve_by_elim* only [f] + +example : 6 = 6 ∧ [7] = [7] := by + fconstructor + solve_by_elim* only [@rfl _] + +-- Test that `Config.intros` causes `solve_by_elim` to call `intro` on intermediate goals. +example (P : Prop) : P → P := by + fail_if_success solve_by_elim (config := {intros := false}) + solve_by_elim + +-- This worked in mathlib3 without the `@`, but now goes into a loop. +-- If someone wants to diagnose this, please do! +example (P Q : Prop) : P ∧ Q → P ∧ Q := by + solve_by_elim [And.imp, @id] + +section apply_assumption + +example {a b : Type} (h₀ : a → b) (h₁ : a) : b := by + apply_assumption + apply_assumption + +example {α : Type} {p : α → Prop} (h₀ : ∀ x, p x) (y : α) : p y := by + apply_assumption + +-- Check that `apply_assumption` uses `exfalso`. +example {P Q : Prop} (p : P) (q : Q) (h : P → ¬ Q) : Nat := by + fail_if_success apply_assumption (config := {exfalso := false}) + apply_assumption <;> assumption + +end apply_assumption + +example (x : (α × (β × γ))) : (α × β) × γ := by + rcases x with ⟨a, b, c⟩ + fail_if_success solve_by_elim (config := {constructor := false}) + solve_by_elim diff --git a/tests/lean/run/symm.lean b/tests/lean/run/symm.lean new file mode 100644 index 0000000000..33f2146617 --- /dev/null +++ b/tests/lean/run/symm.lean @@ -0,0 +1,27 @@ +import Init.Tactics + +set_option autoImplicit true +set_option linter.missingDocs false + +-- testing that the attribute is recognized +@[symm] def eq_symm {α : Type} (a b : α) : a = b → b = a := Eq.symm + +example (a b : Nat) : a = b → b = a := by intros; symm; assumption +example (a b : Nat) : a = b → True → b = a := by intro h _; symm at h; assumption + +def sameParity : Nat → Nat → Prop + | n, m => n % 2 = m % 2 + +@[symm] def sameParity_symm (n m : Nat) : sameParity n m → sameParity m n := Eq.symm + +example (a b : Nat) : sameParity a b → sameParity b a := by intros; symm; assumption + +def MyEq (n m : Nat) := ∃ k, n + k = m ∧ m + k = n + +@[symm] theorem MyEq.symm {n m : Nat} (h : MyEq n m) : MyEq m n := by + rcases h with ⟨k, h1, h2⟩ + exact ⟨k, h2, h1⟩ + +example {n m : Nat} (h : MyEq n m) : MyEq m n := by + symm + assumption