Search code examples
coqcoq-tactic

When destructing fixpoint, add hypothesis without simplifying

Suppose I have to prove the following lemma: 

Require Import Coq.Arith.EqNat.

Lemma myLemma: forall m,
  if beq_nat m 0
  then m = 0
  else m <> 0.

and I proceed this way:

Proof.
  intro.
  destruct (beq_nat m 0).  (* [1] *)
  - (* [2] *)
  - (* ???? Can't do anything *)
Qed.

then, at point [1], the destruct proceeds by case analysis, first beq_nat m 0 is replaced by true in the if which is simplified to the goal m = 0, without additional hypothesis (at point [2]).

My question is: instead of splitting the goal, replacing and simplifying, is there a way to split the goal, and adding the corresponding case as an hypothesis ?

That is, at point [2], instead of having the following:

m : nat
______________________________________(1/1)
m = 0

I'd like to have:

m : nat
true = PeanoNat.Nat.eqb m 0
______________________________________(1/1)
if PeanoNat.Nat.eqb m 0 then m = 0 else m <> 0

and to proceed myself to the following of the proof.

(N.B.: this is a very dummy mwe, I know that there are other ways to finish here, my point is not to finish this particular proof, but to have a method to get an hypothesis from a destruct).

Solution

  • Instead of destruct (beq_nat m 0) you can use

    destruct (beq_nat m 0) eqn:Equation_name.

    or

    case_eq (beq_nat m 0).

    destruct ... eqn:E is like case_eq ...; intros E. You can find out more about the differences between destruct and case having read this entry.

    The first two options simplify things, but we can do something like this to avoid the simplification:

    remember (beq_nat m 0) as b eqn:E; rewrite E; destruct b.

    This third option will give you a proof state like this

    m : nat
E : true = PeanoNat.Nat.eqb m 0
============================
if PeanoNat.Nat.eqb m 0 then m = 0 else m <> 0

    for the first subgoal.