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: Oct 01 2023 at 18:01 UTC