## Stream: Coq users

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

#### Jiahong Lee (Jun 13 2022 at 05:08):

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.

Problems:

1. I can prove `leb_nm__leb_mn` without using `leb_spec`. Still, I couldn't see how these two are related.
2. What does it mean for a theorem A to be a specialisation of another theorem B?
I guess it means theorem B is a more general theorem, and that theorem A can be proven simply by proving a special case. But from my POV, that is not the case with `leb_nm__leb_mn` and `leb_spec`.

#### Guillaume Melquiond (Jun 13 2022 at 05:18):

`leb_nm__leb_mn` is indeed a specialization of `leb_spec`. You can prove `leb_nm__leb_mn` without ever looking at the properties of `leb`. In fact, you could just as well prove the following:

``````Lemma foo : forall p q : bool,
(p = true \/ (p = false /\ q = true)) ->
(p = false -> q = true).
``````

#### Guillaume Melquiond (Jun 13 2022 at 05:29):

Note that you can also prove the converse implication. So you could also say the second lemma is not a specialization / corollary of the first one, but just an equivalent formulation. Both lemmas are just as strong as the other.

#### Jiahong Lee (Jun 13 2022 at 06:05):

Thanks, now it makes sense to me. As for the converse implication, it'll involve proving this:

``````Lemma implies_or : forall p q : Prop,
(p -> q) <-> (~ p \/ q).
``````

Can this be proven in Coq?

#### Guillaume Melquiond (Jun 13 2022 at 06:23):

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

#### Guillaume Melquiond (Jun 13 2022 at 06:25):

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

#### Julin S (Jun 13 2022 at 06:41):

If `forall p q` is really needed, I suppose classical logic could be used, but then you lose the ability to do extraction (heard something like that recently from here :smile: ).

#### Pierre-Marie Pédrot (Jun 13 2022 at 06:43):

Classical logic in Prop is perfectly fine w.r.t. extraction. More generally any consistent set of axioms in Prop are fine, that's the whole point of the Prop-Type separation.

#### Julin S (Jun 13 2022 at 06:48):

Extraction is possible even with `p \/ ~p` added as axiom?

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

Oh is it that Prop is erased away during extraction?

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

Is there any disadvantage in using classical logic, though?

#### 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: Sep 30 2023 at 07:01 UTC