Skip to content

Instantly share code, notes, and snippets.

@youxkei

youxkei/coq_logic_puzzle.v

Created May 10, 2026 10:37
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save youxkei/d7e648a543d1d3351ff4181dae99c6e8 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save youxkei/d7e648a543d1d3351ff4181dae99c6e8 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
coq_logic_puzzle.v
Theorem dne_then_lem : (forall (P: Prop), (~~P -> P)) -> (forall (Q: Prop),(Q \/ ~Q)).
Proof.
unfold not.
intros.
apply H.
intros.
apply H0.
right.
intros.
apply H0.
left.
assumption.
Qed.
Theorem lem_then_dne : (forall (P: Prop), (P \/ ~P)) -> (forall (Q: Prop), (~~Q -> Q)).
Proof.
unfold not.
intros.
specialize (H Q).
destruct H.
- assumption.
- specialize (H0 H).
contradiction.
Qed.
Theorem peirce_then_lem : (forall (P Q : Prop), ((P -> Q) -> P) -> P) -> (forall (R : Prop), R \/ ~R).
Proof.
unfold not.
intros.
specialize (H (R \/ (R -> False)) False).
apply H.
intros.
right.
intros.
apply H0.
left.
assumption.
Qed.
Theorem lem_then_peirce : (forall (P : Prop), P \/ ~P) -> (forall (Q R : Prop), ((Q -> R) -> Q) -> Q).
Proof.
unfold not.
intros.
specialize (H Q).
destruct H.
- assumption.
- apply H0.
intros.
specialize (H H1).
contradiction.
Qed.
Theorem demorgan_not_or : forall (P Q : Prop), ~(P \/ Q) -> ~P /\ ~Q.
Proof.
unfold not.
intros.
split.
- intros.
apply H.
left.
assumption.
- intros.
apply H.
right.
assumption.
Qed.
Theorem demorgan_and_not : forall (P Q : Prop), ~P /\ ~Q -> ~(P \/ Q).
Proof.
unfold not.
intros.
destruct H as [HP HQ].
destruct H0.
- apply HP.
assumption.
- apply HQ.
assumption.
Qed.
Theorem demorgan_not_and : (forall (P : Prop), P \/ ~P) -> (forall (Q R : Prop), ~(Q /\ R) -> ~Q \/ ~R).
Proof.
unfold not.
intros.
pose proof (H Q) as HQ.
pose proof (H R) as HR.
destruct HQ.
- destruct HR.
* pose proof (conj H1 H2).
specialize (H0 H3).
contradiction.
* right.
assumption.
- destruct HR.
* left.
assumption.
* right.
assumption.
Qed.
Theorem impl_to_or : (forall (P : Prop), P \/ ~P) -> (forall (Q R : Prop), (Q -> R) -> ~Q \/ R).
Proof.
unfold not.
intros.
specialize (H Q).
destruct H.
- right.
apply H0.
assumption.
- left.
assumption.
Qed.
Theorem iad : (forall (P : Prop), P \/ ~P) -> (forall (Q R : Prop), (Q -> R) -> ~Q \/ R).
Proof.
unfold not.
intros.
specialize (H Q).
destruct H.
- right.
apply H0 in H.
assumption.
- left.
assumption.
Qed.
Theorem contrapos : (forall (P : Prop), ~~P -> P) -> (forall (Q R : Prop), (~R -> ~Q) -> Q -> R).
Proof.
unfold not.
intros.
specialize (H R).
apply H.
intros.
specialize (H0 H2).
apply H0 in H1.
assumption.
Qed.
Theorem dni : forall (P : Prop), P -> ~~P.
Proof.
unfold not.
intros.
specialize (H0 H).
assumption.
Qed.
Theorem tne : forall (P : Prop), ~~~P -> ~P.
Proof.
unfold not.
intros.
apply H.
intros.
specialize (H1 H0).
assumption.
Qed.
Theorem nn_and : forall (P Q : Prop), ~~(P /\ Q) <-> ~~P /\ ~~Q.
Proof.
unfold not.
split.
- intros.
split.
+ intros.
apply H.
intros.
apply H0.
destruct H1.
assumption.
+ intros.
apply H.
intros.
apply H0.
destruct H1.
assumption.
- intros.
destruct H.
apply H.
intros.
apply H1.
intros.
pose proof (conj H2 H3).
specialize (H0 H4).
assumption.
Qed.
Theorem nn_impl : forall (P Q : Prop), ~~(P -> Q) <-> (~~P -> ~~Q).
Proof.
unfold not.
split.
- intros.
apply H.
intros.
apply H0.
intros.
specialize (H2 H3).
apply H1.
assumption.
- intros.
apply H.
+ intros.
apply H0.
intros.
specialize (H1 H2).
contradiction.
+ intros.
apply H0.
intros.
assumption.
Qed.
Theorem nn_mono : forall (P Q : Prop), (P -> Q) -> (~~P -> ~~Q).
Proof.
unfold not.
intros.
apply H0.
intros.
apply H1.
specialize (H H2).
assumption.
Qed.
Theorem glivenko_lem : forall (P : Prop), ~~(P \/ ~P).
Proof.
unfold not.
intros.
apply H.
right.
intros.
apply H.
left.
assumption.
Qed.
Theorem curry : forall (P Q R : Prop), (P /\ Q -> R) <-> (P -> Q -> R).
Proof.
split.
- intros.
specialize (H (conj H0 H1)).
assumption.
- intros.
destruct H0.
specialize (H H0 H1).
assumption.
Qed.
Theorem and_assoc : forall (P Q R : Prop), (P /\ Q) /\ R <-> P /\ (Q /\ R).
Proof.
split.
- intros.
decompose [and] H.
split.
+ assumption.
+ split; assumption.
- intros.
decompose [and] H.
split.
+ split; assumption.
+ assumption.
Qed.
Theorem or_assoc : forall (P Q R : Prop), (P \/ Q) \/ R <-> P \/ (Q \/ R).
Proof.
split.
- intros.
decompose [or] H.
+ left.
assumption.
+ right. left.
assumption.
+ right. right.
assumption.
- intros.
decompose [or] H.
+ left. left.
assumption.
+ left. right.
assumption.
+ right.
assumption.
Qed.
Theorem wlem : (forall (P : Prop), P \/ ~P) -> (forall (Q : Prop), ~Q \/ ~~Q).
Proof.
unfold not.
intros.
specialize (H (Q -> False)).
assumption.
Qed.
Theorem material_impl : (forall (P : Prop), P \/ ~P) -> (forall (Q R : Prop), (Q -> R) <-> (~Q \/ R)).
Proof.
unfold not.
intros.
split.
- intros.
specialize (H Q).
destruct H.
+ specialize (H0 H).
right.
assumption.
+ left.
assumption.
- intros.
destruct H0.
+ specialize (H0 H1).
contradiction.
+ assumption.
Qed.
Theorem consequentia_mirabilis : (forall (P : Prop), P \/ ~P) -> (forall (Q : Prop), (~Q -> Q) -> Q).
Proof.
unfold not.
intros.
specialize (H Q).
destruct H.
- assumption.
- apply H0.
assumption.
Qed.
Theorem cm_to_lem : (forall (Q : Prop), (~Q -> Q) -> Q) -> (forall (P : Prop), P \/ ~P).
Proof.
unfold not.
intros.
specialize (H (P \/ (P -> False))).
apply H.
intros.
right.
intros.
apply H0.
left.
assumption.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment