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

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除了多次使用该策略（可以说每个“层”一次）之外，我不知道任何其他方法。

如果我在 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

为此，您需要mathlibimport 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