2
$\begingroup$

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?

$\endgroup$

3 Answers 3

4
$\begingroup$

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.

About your original request,

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.
$\endgroup$
2
  • $\begingroup$ What does the notation [-> | Hd] mean? $\endgroup$ Jan 25, 2023 at 15:27
  • 1
    $\begingroup$ 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. $\endgroup$ Jan 25, 2023 at 16:09
1
$\begingroup$

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].
$\endgroup$
1
$\begingroup$

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).
$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$
    – Ana Borges
    Jan 25, 2023 at 13:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.