精益中用于破坏假设的嵌套模式匹配

Question

让我们看一些引理的例子（其陈述是否正确与本次讨论无关）：

lemma L1 : forall (n m: ℕ) (p : ℕ → Prop), (p n ∧ ∃ (u:ℕ), p u ∧ p m) ∨ (¬p n ∧ p m) → n = m :=
begin
  intros n m p H, cases H with H H,
    {cases H with H1 H2, cases H2 with u H2, cases H2 with H2 H3, sorry},
    {cases H with H1 H2, sorry}
end

我想在这里强调的一点是，当用 cases 策略破坏我的假设时，除了多次使用该策略（可以这么说，每个 'layer' 一次），我不知道任何其他方法。

如果我在 Coq 中查看相同的引理：

Lemma L1 : forall (n m:nat) (p:nat -> Prop), 
    (p n /\ exists (u:nat), p u /\ p m) \/ (~p n /\ p m) -> n = m.
Proof.
    intros n m p [[H1 [u [H2 H3]]]|[H1 H2]].
    - admit.
    -
Show.

我能够用单个嵌套模式匹配来破坏我的假设。

我想我可以在精益中做同样的事情，但我不知道怎么做。如果能告诉我，我将不胜感激，因为我发现嵌套模式匹配在实践中非常方便。

Answer 1

你需要 mathlib 和 import tactic.rcases。您可以使用 rcases 策略。

import tactic.rcases

lemma L1 : forall (n m: ℕ) (p : ℕ → Prop), (p n ∧ ∃ (u:ℕ), p u ∧ p m) ∨ (¬p n ∧ p m) → n = m :=
begin
  intros n m p H, 
  rcases H with ⟨H1, u, H2, H3⟩ | ⟨H1, H2⟩,
  
end

精益中用于破坏假设的嵌套模式匹配

Nested pattern matching in Lean for destructing hypothesis

lean