## Stream: Coq users

### Topic: ✔ Theorem A as a Specialisation of Theorem B?

#### Jiahong Lee (Jun 13 2022 at 07:34):

Guillaume Melquiond said:

Not for arbitrary inhabitants of `Prop`. But if you replace your atoms by `p = true` and `q = true`, then it becomes provable.

(Actually, you only need to make `p` a boolean; `q` can stay in `Prop`.)

Make sense, thanks!

#### Notification Bot (Jun 13 2022 at 07:35):

Jiahong Lee has marked this topic as resolved.

#### Jiahong Lee (Jun 13 2022 at 07:37):

Julin S said:

Is there any disadvantage in using classical logic, though?

Ermmm, I think it deserves as a new thread? Thanks!

#### Julin S (Jun 13 2022 at 07:49):

Maybe yeah. Still, I had thought the extraction part was what would get in trouble because if excluded middle is there, we can't say which clause was true to make the whole thing true.

#### Paolo Giarrusso (Jun 13 2022 at 07:55):

You could state excluded middle in Type (forall T : Type, {T} + {~T}), and then you'd definitely have extraction trouble.

#### Jiahong Lee (Jun 22 2022 at 08:00):

Jiahong Lee said:

Hi, I'm self-learning Coq and arrived here. So, given these:

``````Lemma leb_spec : forall (n m : nat),
leb n m = true \/ (leb n m = false /\ leb m n = true).
Lemma leb_nm__leb_mn : forall (n m : nat),
leb n m = false -> leb m n = true.
``````

the author(s) claims that `leb_nm__leb_mn` is a specialisation of `leb_spec`, and that confuses me.

Revisiting the problem, I can complete the prove simply by introducing the theorem into the context.

``````Lemma leb_nm__leb_mn' : forall (n m : nat),
leb n m = false -> leb m n = true.
Proof.
intros n m H. destruct (leb_spec n m) as [H1 | [H2 H3]].
- rewrite H1 in H. discriminate H.
- apply H3.
Qed.
``````

Cheers.

Last updated: Jan 27 2023 at 02:04 UTC