~amiloradovsky/symbolic-dynamics

symbolic-dynamics/DeMorgan.v -rw-r--r-- 686 bytes View raw
5857f238Andrew Miloradovsky .build.yml: continuous integration for SourceHut 7 months ago
                                                                                
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
(* These laws are true constructively, even without the LEM *)

Section De_Morgan's.

  Lemma de_Morgan_0 (X Y: Prop): ((~ X) /\ (~ Y)) <-> (~ (X \/ Y)).
  Proof. tauto. Qed.
  Lemma de_Morgan_1 (X Y: Prop): ((~ X) \/ (~ Y))  -> (~ (X /\ Y)).
  Proof. tauto. Qed.

  Lemma de_Morgan_0' {X: Type} (P: X -> Prop):
    (forall x, ~ P x) <-> (~ exists x, P x).
  Proof. split.
    intros. contradict H. intro H'. destruct H. exact (H' x H).
    intros. contradict H. exists x. assumption.
  Qed.
  Lemma de_Morgan_1' {X: Type} (P: X -> Prop):
    (exists x, ~ P x)  -> (~ forall x, P x).
  Proof.
    intros. contradict H. intro H'. destruct H'. exact (H0 (H x)).
  Qed.

End De_Morgan's.