Time for a little quiz. What do the following snippets do?

```
Goal forall (f : nat -> bool), True.
Proof.
intros [].
Abort.
Goal forall (f : nat -> bool), f = f.
Proof.
intros [].
Abort.
Goal forall (f : nat -> bool), f = f.
Proof.
intros f; destruct f.
Abort.
Goal forall (f : forall n : nat, 0 = n), True.
Proof.
intros [].
Abort.
Goal forall (f : forall n : nat, 0 = n), f = f.
Proof.
intros f; destruct f.
Abort.
Goal forall (f : forall n : nat, n = 0), True.
Proof.
intros [].
Abort.
Goal forall (f : forall n : nat, n = 0), True.
Proof.
intros f; destruct f.
Abort.
```

No cheating!

I am kind enough to not give you the corresponding examples with case / ecase.

I didn't know you could use `intros []`

on functions (and I haven't tried it so maybe it doesn't work at all) so here are my wild guesses:

```
Goal forall (f : nat -> bool), True.
Proof. intros []. (* edestruct (f _) ?? *) Abort.
Goal forall (f : nat -> bool), f = f.
Proof. intros []. (* edestruct (f _) ?? *) Abort.
Goal forall (f : nat -> bool), f = f.
Proof. intros f; destruct f. (* error because f is not inductive *) Abort.
Goal forall (f : forall n : nat, 0 = n), True.
Proof. intros []. (* edestruct (f _ _) ?? *) Abort.
Goal forall (f : forall n : nat, 0 = n), f = f.
Proof. intros f; destruct f. (* error because f is not inductive *) Abort.
Goal forall (f : forall n : nat, n = 0), True.
Proof. intros []. (* edestruct (f ?n _) but it gives an error because Coq doesn't know how to rewrite ?n *) Abort.
Goal forall (f : forall n : nat, n = 0), True.
Proof. intros f; destruct f. (* error because f is not inductive *) Abort.
```

The actual results are quite.. interesting!

As any feature of Coq it's actually used in the wild, otherwise it wouldn't be interesting.

Last updated: Oct 13 2024 at 01:02 UTC