FinMatrix.CoqExt.LogicExt

Require Export Coq.Logic.Classical.
Require Export Coq.Logic.FunctionalExtensionality.
Require Export Coq.Logic.PropExtensionality.
Require Import Coq.Sets.Ensembles.

Existing properties in Coq standard library

Properties from Coq.Logic.FunctionalExtensionality

Properties from Coq.Logic.PropExtensionality

Properties Coq.Logic.Classical_Prop

Properties from Coq.Logic.EqdepFacts

Other properties

Properties for logic operations

Lemma or_same : forall (P : Prop), P \/ P -> P.
Proof. intros. destruct H; auto. Qed.

Lemma impl_or_distr : forall A B C : Prop, (A -> B \/ C ) <-> (A -> B ) \/ (A -> C ).
Proof.
  intros; split; intros.
  - apply imply_to_or in H. destruct H.
    + left. intros. easy.
    + destruct H; auto.
  - destruct H; auto.
Qed.

Lemma impl_or_distr_eq : forall A B C : Prop, (A -> B \/ C ) = ((A -> B ) \/ (A -> C )).
Proof. intros. apply propositional_extensionality. apply impl_or_distr. Qed.

Lemma extensionality_ensembles : forall (U : Type) (A B : U -> Prop),
    (forall x : U, A x -> B x ) /\ (forall x : U, B x -> A x ) -> A = B.
Proof. intros.
apply Extensionality_Ensembles. auto. Qed.

Exercises for logic

Section exercise_forall_exist_not.

Existing lemmas ex_not_not_all: forall (U : Type) (P : U -> Prop), (exists n : U, ~ P n) -> ~ (forall n : U, P n) not_all_ex_not: forall (U : Type) (P : U -> Prop), ~ (forall n : U, P n) -> exists n : U, ~ P n not_all_not_ex: forall (U : Type) (P : U -> Prop), ~ (forall n : U, ~ P n) -> exists n : U, P n

These lemmas needn't axiom

  Lemma my_all_not_not_ex : forall (U : Type) (P : U -> Prop),
      (forall n : U, ~ P n ) -> ~ (exists n : U , P n ).
  Proof. intros. intro. destruct H0. specialize (H x). easy. Qed.

  Lemma my_ex_not_not_all : forall (U : Type) (P : U -> Prop),
      (exists n : U , ~ P n ) -> ~ (forall n : U, P n ).
  Proof. intros. intro. destruct H. specialize (H0 x). easy. Qed.

These lemmas need axiom in Classic Logic

  Lemma my_reverse_proof : forall P Q : Prop, (~Q -> ~P ) -> (P -> Q ).
  Proof. Abort.

  Lemma my_not_ex_not_all:
    forall (U : Type) (P : U -> Prop), ~ (exists n : U , ~ P n ) -> forall n : U, P n.
  Proof. Abort.

  Lemma my_not_ex_all_not:
    forall (U : Type) (P : U -> Prop), ~ (exists n : U , P n ) -> forall n : U, ~ P n.
  Proof. Abort.

  Lemma my_not_all_ex_not: forall (U : Type) (P : U -> Prop),
      ~ (forall n : U, P n ) -> exists n : U , ~ P n.
  Proof. Abort.

  Lemma my_not_all_not_ex: forall (U : Type) (P : U -> Prop),
      ~ (forall n : U, ~ P n ) -> exists n : U , P n.
  Proof. Abort.

End exercise_forall_exist_not.

Properties for function

The application result is equal

Lemma fun_app : forall {A B} (f : A -> B) (a b : A), a = b -> f a = f b .
Proof. intros. subst; auto. Qed.

Two functions are equal, iff extensional equal

Lemma feq_iff : forall {A} (f g : A -> A), f = g <-> (forall x, f x = g x ).
Proof. intros. split; intros; subst; auto. extensionality x; auto. Qed.

A short name of "functional_extensionality"

eta expansion

Bidirection form of functional extensionality (unary function)

Lemma fun_eq_iff_forall_eq : forall A B (f g : A -> B),
    (fun i => f i ) = (fun i => g i ) <-> forall i, f i = g i.
Proof.
  intros. split; intros.
  -

    remember (fun (f:A->B) (i:A) => f i) as F eqn:EqF.
    replace (fun i => f i) with (F f) in H by (rewrite EqF; auto).
    replace (fun i => g i) with (F g) in H by (rewrite EqF; auto).
    replace (f i) with (F f i) by (rewrite EqF; auto).
    replace (g i) with (F g i) by (rewrite EqF; auto).
    rewrite H. auto.
  - extensionality i. auto.
Qed.

Another form of functional extensionality (binary function)

Lemma fun_eq_iff_forall_eq2 : forall A B C (f g : A -> B -> C),
    (fun i j => f i j ) = (fun i j => g i j ) <-> forall i j, f i j = g i j.
Proof.
  intros. split; intros.
  - rewrite (fun_eq_iff_forall_eq) in H. rewrite H. auto.
  - extensionality i. extensionality j. auto.
Qed.