## Stream: Coq users

### Topic: ✔ how to prove this in Coq

#### TX Xia (Jul 28 2022 at 20:38):

Hi,
I'm new to Coq and I was trying to prove this thing below.

``````Goal forall P (h : reflect P true), P.
Proof.
move=> P.
case.
``````

What I don't understand is why after `case` there are 2 branches of goal. I don't suppose that the second goal `~P -> P` should appear because that would mean `h : reflect P false` while `h : reflect P true`.
Can anybody help me?
Thanks so much!

#### Li-yao (Jul 28 2022 at 20:44):

`case` uses a very primitive form of pattern-matching which doesn't take into account the fact that the second parameter of `reflect` is already `true`.
A common solution here is to generalize `true` (`remember true`) before `case`.

#### TX Xia (Jul 28 2022 at 20:53):

Li-yao said:

`case` uses a very primitive form of pattern-matching which doesn't take into account the fact that the second parameter of `reflect` is already `true`.
A common solution here is to generalize `true` (`remember true`) before `case`.

I saw your response and tried this. I don't know if I did it right but it seems I still couldn't solve it.

``````Goal forall P (h : reflect P true), P.
Proof.
move=> P.
remember true.
case.
by [].
``````

And here is what's left in my panel:

``````P: Prop
b: bool
Heqb: b = true
---
1/1
~ P -> P
``````

#### Pierre Jouvelot (Jul 28 2022 at 20:53):

`reflect` is defined as an `Inductive` with two constructors, yielding the two goals you saw. But you don't need to use `case` here, using instead directly the reflection mechanism:

``````Goal forall P (h : reflect P true), P.
Proof.
move=> P h.
exact/h.
Qed.
``````

#### TX Xia (Jul 28 2022 at 21:00):

Pierre Jouvelot said:

`reflect` is defined as an `Inductive` with two constructors, yielding the two goals you saw. But you don't need to use `case` here, using instead directly the reflection mechanism:

``````Goal forall P (h : reflect P true), P.
Proof.
move=> P h.
exact/h.
Qed.
``````

Ah, thanks. I didn't think of that.
But here the concern is also if in the future I define another `Inductive` like `reflect`, such as

``````Inductive fooo (P : Prop) : bool -> bool -> Set :=
| RT : P -> fooo P true true
| RF : ~ P -> fooo P false false.
``````

And if I get `(h : fooo P true true)` in my context, how can I extract a proof of P out of there?

#### Paolo Giarrusso (Jul 28 2022 at 21:36):

inversion h should do it

#### Pierre Jouvelot (Jul 28 2022 at 22:01):

I'm not sure, but you can look at what `elimT` does, as an example, I guess.

#### Paolo Giarrusso (Jul 28 2022 at 22:17):

confirm that `inversion` works here:

``````Goal forall P, fooo P true true -> P.
Proof. intros P H. inversion H. assumption. Qed.
``````

#### Alexander Gryzlov (Jul 28 2022 at 23:03):

If you really want to stick to ssreflect's `case`, you can use the type family version:

``````move=> P H.
by case E: _ / H.
``````

#### Notification Bot (Jul 29 2022 at 06:15):

TX Xia has marked this topic as resolved.

Last updated: Jun 20 2024 at 11:02 UTC