Stream: Coq users

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


view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Guillaume Melquiond (Jun 13 2022 at 06:25):

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

view this post on Zulip 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: ).

view this post on Zulip 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.

view this post on Zulip Julin S (Jun 13 2022 at 06:48):

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

view this post on Zulip Julin S (Jun 13 2022 at 06:49):

Oh is it that Prop is erased away during extraction?

view this post on Zulip Julin S (Jun 13 2022 at 06:49):

Is there any disadvantage in using classical logic, though?

view this post on Zulip 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!

view this post on Zulip Notification Bot (Jun 13 2022 at 07:35):

Jiahong Lee has marked this topic as resolved.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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