The Coq mailing list

[Frederic Chyzak <frederic.chyzak AT inria.fr>]

Hi,

Following:

On Tue, 2015-02-10 at 16:33 +0000, Matej Kosik wrote:
> Why is the third occurrence of the free variable "a" in the original
> goal treated in a different way than its first and the second
> occurrences?

I tried using destruct (which was described to me as the “smart case”)
and e- variants instead of case, leading to further related questions:

(* Why will destruct fail on error here, while it does not in foo3
below? *)
Lemma foo1 (a : nat) : (fun c : nat => c + a + a = 42) a.
Proof.
Fail destruct a.
Abort.

(* This yields the same result as with case.  What more does the 'e' do
here? *)
Lemma foo2 (a : nat) : (fun c : nat => c + a + a = 42) a.
Proof.
edestruct a.
Abort.

(* Both following variants replace all occurrences of a.  Why is it now
possible? *)
Lemma foo3 (a : nat) : (fun c : nat => c + a + a = 42) a -> False.
Proof.
destruct a.
Abort.

Lemma foo4 (a : nat) : (fun c : nat => c + a + a = 42) a -> False.
Proof.
edestruct a.
Abort.

(* Just for reference: ssreflect does it with the three replacements. *)
Require Import ssreflect.
Lemma foo5 (a : nat) : (fun c : nat => c + a + a = 42) a.
Proof.
case: a.
Abort.

Frédéric