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