# In Coq, is there a simpler tactic for introducing a disjunction and immediately destructing it?

Very often, I find myself writing some tactics like these:

assert (delta = 1 \/ delta <> 1) as Hd by lia.
destruct Hd.
...(proceed to work with two cases)...


Is there a shorter way or a more idiomatic tactic that does this?

You can destruct things in many ways at the time you introduce them with "intro patterns".

https://coq.inria.fr/refman/proof-engine/tactics.html#intro-patterns

Here are small examples:

Lemma exple1 (A B : Prop) : A \/ B -> B \/ A.
Proof.
(* disjunctive pattern *)
intros [H | H'].
- right; exact H.
- left; exact H'.
Qed.

Lemma exple2 (A B : Prop) : A /\ B -> B /\ A.
Proof.
(* conjunctive pattern *)
intros [H H'].
split.
- exact H'.
- exact H.
Qed.

Lemma exple3 (A B : Prop) : A /\ B -> A.
Proof.
(* useless parts can be thrown away *)
intros [H _].
exact H.
Qed.

Lemma exple4 (A B C : Prop) : A /\ (B \/ C) -> (A /\ B) \/ (A /\ C).
Proof.
(* intro patterns can be nested *)
intros [HA [HB | HC]].
- left. split.
+ exact HA.
+ exact HB.
- right. split.
+ exact HA.
+ exact HC.
Qed.

Lemma exple5 (x : nat) : x = 0 -> x + x = x.
Proof.
(* the -> intro pattern acts like "rewrite name; clear name" *)
intros ->. reflexivity.
Qed.

Lemma exple6 (x : nat) : x = 0 -> x = x + x.
Proof.
(* the hyp%term intro pattern acts like "intros hyp; apply term in hyp" *)
intros Hx%exple5. symmetry. exact Hx.
Qed.

Lemma exple6' (x : nat) : x = 0 -> x = x + x.
Proof.
(* % intro patterns can be composed *)
intros Hx%exple5%eq_sym. exact Hx.
Qed.

Lemma exple7 (A B : Prop) : A -> B -> A /\ B.
Proof.
intros H1 H2.
(* intro patterns can occur (almost) every time you name a term.
assert ([H H']: A /\ B) fails but this works: *)
assert (A /\ B) as [H H'].
(* this was an artificial example *)
easy. easy.
Qed.


assert (delta = 1 \/ delta <> 1) as [Hd | Hd] by lia.


does the trick, and you may want to consider :

assert (delta = 1 \/ delta <> 1) as [-> | Hd] by lia.

• What does the notation [-> | Hd] mean? Jan 25, 2023 at 15:27
• This means : "in that case, instead of naming and introducing the equality delta = 1, use it to replace delta with 1 in the goal". Use the other arrow <- to rewrite in the other direction. Jan 25, 2023 at 16:09

There is a theorem to do that Nat.eq_dec. I usually import it by

Require Import Arith.


Then I do

destruct (Nat.eq_dec delta 1) as [Hd1|Hnd1].


Since you're dealing with natural numbers, you can also use booleans instead of properties. Using ssreflect, you could then do:

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma foo (delta : nat) : false.
Proof.
have [hd1|hd2] := boolP(delta == 1).

• If delta == 1 occurs in the context, you can use the shorter case: eqP => [eq|neq].. You can also do case: @eqP _ delta 1 => [eq|neq]. even if it doesn't appear in the context, but then it's less obvious that it's better than Pierre's suggestion. Jan 25, 2023 at 13:12