Stream: Coq devs & plugin devs

Topic: intros quiz


view this post on Zulip Pierre-Marie Pédrot (Apr 13 2023 at 14:08):

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!

view this post on Zulip Pierre-Marie Pédrot (Apr 13 2023 at 14:13):

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

view this post on Zulip Janno (Apr 13 2023 at 15:23):

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.

view this post on Zulip Janno (Apr 13 2023 at 15:25):

The actual results are quite.. interesting!

view this post on Zulip Pierre-Marie Pédrot (Apr 13 2023 at 15:36):

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


Last updated: Dec 05 2023 at 12:01 UTC