Unfolding not

~ P in Coq stands for not P, and is defined as P -> False, so to prove ~ P, it sometimes helps to do unfold not. intro.

Theorem P_and_not_P : forall P : Prop, P -> ~ P -> False.
forall P : Prop, P -> ~ P -> False
Proof.
forall P : Prop, P -> ~ P -> False
  intros P HP HnP.
P: Prop
HP: P
HnP: ~ P
False
  unfold "~" in HnP.
P: Prop
HP: P
HnP: P -> False
False

As HnP is of type P -> False, we can apply it to the hypothesis HP: P to get a hypothesis of type False.

  apply HnP in HP as HFalse.
P: Prop
HP: P
HnP: P -> False
HFalse: False
False

We can then solve the goal using HFalse.

  apply HFalse.
Qed.

Behavior of simpl on fixpoints

Some students have been running into a situation where simpl doesn't behave as they expect. This hint explores the behavior of simpl on Fixpoint definitions.

Here's a simple Fixpoint definition always_true : nat -> bool that deserves its name:

Fixpoint always_true (x : nat) {struct x} : bool := true.
Not a truly recursive fixpoint.
[non-recursive,fixpoints,default]

Note that the syntax {struct x} is a hint to Coq that our definition structurally recurses on the x argument (the only argument). Of course, there isn't any recursion at all here! So indeed, every recursive call (of which there are none) passes a structurally smaller x argument to always_true.

Now, suppose we try to prove the following theorem:

Theorem always_true_ok : forall x : nat,
    always_true x = true.
forall x : nat, always_true x = true
Proof.
forall x : nat, always_true x = true
  intro x.
x: nat
always_true x = true
  simpl. (* Does not perform simplification! *)
x: nat
always_true x = true
  Fail reflexivity. (* Fails! *)
The command has indeed failed with message:
In environment
x : nat
Unable to unify "true" with "always_true x".
x: nat
always_true x = true

That's surprising, isn't it?

Here's a key fact to understanding how simpl works on Fixpoint definitions: simpl only reduces the application of Fixpoint definitions when the argument on which it structurally recurses (according to Coq) is in the form of a constructor application.

That's a mouthful. A trivial way to remedy this is to use destruct on the argument for which the fixpoint is known to be structurally recursive:

  destruct x; reflexivity.
Qed.

Another possible solution for our example here is to just define always_true as a Definition, rather than a Fixpoint; then reflexivity will work as expected.

In the exercise set, you may run into a Fixpoint that can be viewed as structurally recursive on two different arguments, and by using the "{struct}" syntax seen above, you can choose which - one may be more convenient with respect to simpl's behavior as noted in the bolded statement above.

Finally, since Coq usually infers which argument a fixpoint is structurally decreasing on, you can run Print f. for any fixpoint f to see which argument Coq chose.