Library Logic.logic_compl
This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Faissole, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Logic axioms commonly used for numerical analysis and additional definitions
and results about classical logic.
Provides the following logic axioms:
Provides definitions:
Provides equivalence results to enable the use of the rewrite tactic.
All names use the "_equiv" suffix. These are for:
Provides aliases for convenience:
This module may be used through the import of Numbers.Numbers_wDep,
Subsets.Subsets_wDep, Algebra.Algebra_wDep, Lebesgue.Lebesgue_p_wDep, or
Lebesgue.Bochner.Bochner_wDep, where it is exported.
Brief description
Description
- classical logic (ie excluded middle in Prop),
- functional and propositional extensionality,
- proof irrelevance,
- excluded-middle in Set,
- unique and non-unique choice,
- a constructive form of indefinite description.
- neq is the 'not eq' binary relation on any type;
- all propositional connectives, possibly in various configurations;
- all de Morgan's laws for quantifiers.
- fun_ext is an alias for functional_extensionality;
- fun_ext_rev is an alias for equal_f;
- prop_ext is an alias for propositional_extensionality;
- proof_irrel is an alias for proof_irrelevance;
- classic_dec is an alias for excluded_middle_informative;
- ex_EX is an alias for constructive_indefinite_description, where "ex" and "EX" stand for weak existential and strong existential respectively.
Usage
From Coq Require Export FunctionalExtensionality PropExtensionality.
From Coq Require Export ClassicalDescription ClassicalChoice.
From Coq Require Export IndefiniteDescription.
Section Aliases.
Lemma fun_ext :
∀ {T1 T2 : Type} {f g : T1 → T2}, (∀ x1, f x1 = g x1) → f = g.
Proof. intros T1 T2; exact functional_extensionality. Qed.
Lemma fun_ext_rev :
∀ {T1 T2 : Type} {f g : T1 → T2}, f = g → ∀ x1, f x1 = g x1.
Proof. intros T1 T2 f g; exact equal_f. Qed.
Lemma fun_ext2 :
∀ {T1 T2 T3 : Type} {f g : T1 → T2 → T3},
(∀ x1 x2, f x1 x2 = g x1 x2) → f = g.
Proof. intros; do 2 (apply fun_ext; intro); easy. Qed.
Lemma fun_ext2_rev :
∀ {T1 T2 T3 : Type} {f g : T1 → T2 → T3},
f = g → ∀ x1 x2, f x1 x2 = g x1 x2.
Proof. intros; do 2 apply fun_ext_rev; easy. Qed.
Lemma prop_ext : ∀ (P Q : Prop), P ↔ Q → P = Q.
Proof. exact propositional_extensionality. Qed.
Lemma proof_irrel : ∀ (H : Prop) (P Q : H), P = Q.
Proof. exact proof_irrelevance. Qed.
Lemma classic_dec : ∀ (P : Prop), {P} + {¬ P}.
Proof. exact excluded_middle_informative. Qed.
Lemma unique_choice :
∀ {A B : Type} (R : A → B → Prop),
(∀ x, ∃! y, R x y) → ∃ f, ∀ x, R x (f x).
Proof. exact unique_choice. Qed.
Lemma ex_EX :
∀ {T : Type} (P : T → Prop), (∃ x, P x) → {x | P x}.
Proof. exact constructive_indefinite_description. Qed.
End Aliases.
Section Logic_Def.
Definition eq_dec (T : Type) : Type := ∀ (x y : T), { x = y } + { x ≠ y }.
Definition neq {T : Type} : T → T → Prop := fun x y ⇒ x ≠ y.
End Logic_Def.
Section Logic_Facts.
Lemma ifflr : ∀ {P Q}, P ↔ Q → P → Q.
Proof. tauto. Qed.
Lemma iffrl : ∀ {P Q}, P ↔ Q → Q → P.
Proof. tauto. Qed.
Lemma and_or_equiv : ∀ {P Q}, P ∧ Q ↔ P ∨ Q → P ↔ Q.
Proof. tauto. Qed.
Lemma and_or_inj_l :
∀ {P Q} R, P ∧ R ↔ Q ∧ R → P ∨ R ↔ Q ∨ R → P ↔ Q.
Proof. tauto. Qed.
Lemma and_or_inj_r :
∀ P {Q R}, P ∧ Q ↔ P ∧ R → P ∨ Q ↔ P ∨ R → Q ↔ R.
Proof. tauto. Qed.
Lemma modus_ponens_and :
∀ (P1 Q1 P2 Q2 : Prop),
(P1 → Q1) → (P2 → Q2) → P1 ∧ P2 → Q1 ∧ Q2.
Proof. tauto. Qed.
Lemma modus_ponens_and3 :
∀ (P1 Q1 R1 P2 Q2 R2 : Prop),
(P1 → Q1 → R1) → (P2 → Q2 → R2) → P1 ∧ P2 → Q1 ∧ Q2 → R1 ∧ R2.
Proof. tauto. Qed.
Lemma modus_ponens_or :
∀ (P1 Q1 P2 Q2 : Prop),
(P1 → Q1) → (P2 → Q2) → P1 ∨ P2 → Q1 ∨ Q2.
Proof. tauto. Qed.
Lemma and_iff_compat :
∀ (P1 Q1 P2 Q2 : Prop),
(P1 ↔ Q1) → (P2 ↔ Q2) → P1 ∧ P2 ↔ Q1 ∧ Q2.
Proof. tauto. Qed.
Lemma or_iff_compat :
∀ (P1 Q1 P2 Q2 : Prop),
(P1 ↔ Q1) → (P2 ↔ Q2) → P1 ∨ P2 ↔ Q1 ∨ Q2.
Proof. tauto. Qed.
Context {T : Type}.
Lemma eq_sym_equiv : ∀ x y : T, x = y ↔ y = x.
Proof. easy. Qed.
Lemma neq_sym_equiv : ∀ x y : T, x ≠ y ↔ y ≠ x.
Proof. intros; split; intros H; contradict H; easy. Qed.
End Logic_Facts.
Section Predicate_Facts.
Context {T : Type}.
Lemma equiv_forall :
∀ (P Q : T → Prop),
(∀ x, P x ↔ Q x) → ((∀ x, P x) ↔ (∀ x, Q x)).
Proof. intros P Q H1; split; intros H2 x; apply H1; easy. Qed.
End Predicate_Facts.
Section Classical_propositional_Facts1.
Lemma PNNP : ∀ {P : Prop}, P → ¬ ¬ P.
Proof. tauto. Qed.
Lemma NNPP_equiv : ∀ (P : Prop), ¬ ¬ P ↔ P.
Proof. intros; tauto. Qed.
End Classical_propositional_Facts1.
Section Classical_propositional_Facts2.
Context {P Q : Prop}.
Lemma not_and_equiv : ¬ (P ∧ Q) ↔ ¬ P ∨ ¬ Q.
Proof. tauto. Qed.
Lemma not_or_equiv : ¬ (P ∨ Q) ↔ ¬ P ∧ ¬ Q.
Proof. tauto. Qed.
Lemma imp_and_equiv : (P → Q) ↔ ¬ (P ∧ ¬ Q).
Proof. tauto. Qed.
Lemma imp_not_l_and_equiv : (¬ P → Q) ↔ ¬ (~ P ∧ ¬ Q).
Proof. tauto. Qed.
Lemma imp_not_r_and_equiv : (P → ¬ Q) ↔ ¬ (P ∧ Q).
Proof. tauto. Qed.
Lemma imp_or_equiv : (P → Q) ↔ ¬ P ∨ Q.
Proof. tauto. Qed.
Lemma imp_not_l_or_equiv : (¬ P → Q) ↔ P ∨ Q.
Proof. tauto. Qed.
Lemma imp_not_r_or_equiv : (P → ¬ Q) ↔ ¬ P ∨ ¬ Q.
Proof. tauto. Qed.
Lemma not_imp_and_equiv : ¬ (P → Q) ↔ P ∧ ¬ Q.
Proof. tauto. Qed.
Lemma not_imp_not_l_and_equiv : ¬ (~ P → Q) ↔ ¬ P ∧ ¬ Q.
Proof. tauto. Qed.
Lemma not_imp_not_r_and_equiv : ¬ (P → ¬ Q) ↔ P ∧ Q.
Proof. tauto. Qed.
Lemma not_imp_or_equiv : ¬ (P → Q) ↔ ¬ (~ P ∨ Q).
Proof. tauto. Qed.
Lemma not_imp_not_l_or_equiv : ¬ (~ P → Q) ↔ ¬ (P ∨ Q).
Proof. tauto. Qed.
Lemma not_imp_not_r_or_equiv : ¬ (P → ¬ Q) ↔ ¬ (~ P ∨ ¬ Q).
Proof. tauto. Qed.
Lemma contra_equiv : (P → Q) ↔ (¬ Q → ¬ P).
Proof. tauto. Qed.
Lemma contra_not_l_equiv : (¬ P → Q) ↔ (¬ Q → P).
Proof. tauto. Qed.
Lemma contra_not_r_equiv : (P → ¬ Q) ↔ (Q → ¬ P).
Proof. tauto. Qed.
Lemma iff_sym_equiv : (P ↔ Q) ↔ (Q ↔ P).
Proof. tauto. Qed.
Lemma iff_not_equiv : (P ↔ Q) ↔ (¬ P ↔ ¬ Q).
Proof. tauto. Qed.
Lemma iff_not_l_equiv : (¬ P ↔ Q) ↔ (P ↔ ¬ Q).
Proof. tauto. Qed.
Lemma iff_not_r_equiv : (P ↔ ¬ Q) ↔ (¬ P ↔ Q).
Proof. tauto. Qed.
Lemma not_iff_equiv : ¬ (P ↔ Q) ↔ P ∧ ¬ Q ∨ ¬ P ∧ Q.
Proof. tauto. Qed.
End Classical_propositional_Facts2.
Section Classical_propositional_Facts3.
Variable P Q R : Prop.
Lemma not_and3_equiv : ¬ (P ∧ Q ∧ R) ↔ ¬ P ∨ ¬ Q ∨ ¬ R.
Proof. tauto. Qed.
Lemma not_or3_equiv : ¬ (P ∨ Q ∨ R) ↔ ¬ P ∧ ¬ Q ∧ ¬ R.
Proof. tauto. Qed.
Lemma imp3_or_equiv : (P → Q → R) ↔ ¬ P ∨ ¬ Q ∨ R.
Proof. tauto. Qed.
Lemma imp3_and_equiv : (P → Q → R) ↔ ¬ (P ∧ Q ∧ ¬ R).
Proof. tauto. Qed.
Lemma imp3_imp_equiv : (P → Q → R) ↔ (¬ R → ¬ P ∨ ¬ Q).
Proof. tauto. Qed.
Lemma not_imp3_and_equiv : ¬ (P → Q → R) ↔ P ∧ Q ∧ ¬ R.
Proof. tauto. Qed.
Lemma not_imp3_or_equiv : ¬ (P → Q → R) ↔ ¬ (~ P ∨ ¬ Q ∨ R).
Proof. tauto. Qed.
Lemma contra3_equiv : (P → Q → R) ↔ (¬ R ∧ Q → ¬ P).
Proof. tauto. Qed.
Lemma contra3_not_l_equiv : (¬ P → Q → R) ↔ (¬ R ∧ Q → P).
Proof. tauto. Qed.
Lemma contra3_not_m_equiv : (P → ¬ Q → R) ↔ (¬ R ∧ ¬ Q → ¬ P).
Proof. tauto. Qed.
Lemma contra3_not_r_equiv : (P → Q → ¬ R) ↔ (R ∧ Q → ¬ P).
Proof. tauto. Qed.
End Classical_propositional_Facts3.
Section Classical_propositional_Facts4.
Variable P Q R S : Prop.
Lemma not_and4_equiv : ¬ (P ∧ Q ∧ R ∧ S) ↔ ¬ P ∨ ¬ Q ∨ ¬ R ∨ ¬ S.
Proof. tauto. Qed.
Lemma not_or4_equiv : ¬ (P ∨ Q ∨ R ∨ S) ↔ ¬ P ∧ ¬ Q ∧ ¬ R ∧ ¬ S.
Proof. tauto. Qed.
End Classical_propositional_Facts4.
Section Classical_propositional_Facts5.
Context {T : Type}.
Variable x y : T.
Lemma eq_sym_refl : eq_sym (@eq_refl _ x) = @eq_refl _ x.
Proof. easy. Qed.
Lemma neq_sym_invol : ∀ (H : x ≠ y), not_eq_sym (not_eq_sym H) = H.
Proof. intros; apply proof_irrel. Qed.
End Classical_propositional_Facts5.
Section Classical_predicate_Facts1.
Context {T : Type}.
Variable P Q : T → Prop.
Lemma all_and_equiv :
(∀ x, P x ∧ Q x) ↔ (∀ x, P x) ∧ (∀ x, Q x).
Proof. split; intros H; [split; intros | intros; split]; apply H. Qed.
Lemma not_all_not_ex_equiv : ¬ (∀ x, ¬ P x) ↔ ∃ x, P x.
Proof. split; [apply not_all_not_ex | intros [x Hx] H; apply (H x); easy]. Qed.
Lemma not_all_ex_not_equiv : ¬ (∀ x, P x) ↔ ∃ x, ¬ P x.
Proof. split; [apply not_all_ex_not | apply ex_not_not_all]. Qed.
Lemma not_ex_all_not_equiv : ¬ (∃ x, P x) ↔ ∀ x, ¬ P x.
Proof. split; [apply not_ex_all_not | apply all_not_not_ex]. Qed.
Lemma not_ex_not_all_equiv : ¬ (∃ x, ¬ P x) ↔ ∀ x, P x.
Proof. split; [apply not_ex_not_all | intros H [x Hx]; auto]. Qed.
Lemma ex_equiv :
(∀ x, P x ↔ Q x) → (∃ x, P x) ↔ (∃ x, Q x).
Proof. intros H; split; intros [x Hx]; ∃ x; apply H; easy. Qed.
Lemma all_equiv :
(∀ x, P x ↔ Q x) → (∀ x, P x) ↔ (∀ x, Q x).
Proof. intros H1; split; intros H2 x; apply H1; easy. Qed.
End Classical_predicate_Facts1.
Section Classical_predicate_Facts2.
Context {T1 T2 : Type}.
Variable P Q : T1 → T2 → Prop.
Lemma all2_and_equiv :
(∀ x1 x2, P x1 x2 ∧ Q x1 x2) ↔
(∀ x1 x2, P x1 x2) ∧ (∀ x1 x2, Q x1 x2).
Proof. split; intros H; [split; intros | intros; split]; apply H. Qed.
Lemma not_all2_not_ex2_equiv :
¬ (∀ x1 x2, ¬ P x1 x2) ↔ ∃ x1 x2, P x1 x2.
Proof.
rewrite not_all_ex_not_equiv; apply ex_equiv;
intros; apply not_all_not_ex_equiv.
Qed.
Lemma not_all2_ex2_not_equiv :
¬ (∀ x1 x2, P x1 x2) ↔ ∃ x1 x2, ¬ P x1 x2.
Proof.
rewrite not_all_ex_not_equiv; apply ex_equiv;
intros; apply not_all_ex_not_equiv.
Qed.
Lemma not_ex2_all2_not_equiv :
¬ (∃ x1 x2, P x1 x2) ↔ ∀ x1 x2, ¬ P x1 x2.
Proof.
rewrite not_ex_all_not_equiv; apply all_equiv;
intros; apply not_ex_all_not_equiv.
Qed.
Lemma not_ex2_not_all2_equiv :
¬ (∃ x1 x2, ¬ P x1 x2) ↔ ∀ x1 x2, P x1 x2.
Proof.
rewrite not_ex_all_not_equiv; apply all_equiv;
intros; apply not_ex_not_all_equiv.
Qed.
End Classical_predicate_Facts2.
Section Datatypes_Facts.
Context {T1 T2 : Type}.
Lemma pair_neq_spec :
∀ (a1 b1 : T1) (a2 b2 : T2),
(a1, a2) ≠ (b1, b2) ↔ a1 ≠ b1 ∨ a2 ≠ b2.
Proof.
intros; rewrite <- not_and_equiv, <- iff_not_equiv.
apply pair_equal_spec.
Qed.
End Datatypes_Facts.