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!

`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`

.

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
```

`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.
```

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?

inversion h should do it

I'm not sure, but you can look at what `elimT`

does, as an example, I guess.

confirm that `inversion`

works here:

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

If you really want to stick to ssreflect's `case`

, you can use the type family version:

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

TX Xia has marked this topic as resolved.

Last updated: Jun 20 2024 at 11:02 UTC