Require SyntheticComputability.Shared.Dec.
Require Import Setoid Morphisms.
Require Export Lia List NPeano.
Import ListNotations.
Fact ldec_stable P :
P \/ ~ P -> ~~ P -> P.
Proof.
tauto.
Qed.
Definition DNE := forall P, ~~ P -> P.
Definition LEM := forall P, P \/ ~ P.
Lemma LEM_DNE : LEM <-> DNE.
Proof.
split.
- intros lem P. destruct (lem P); intuition.
- intros dne P. eapply dne. tauto.
Qed.
Lemma DNI (P : Prop) : P -> ~~ P.
Proof.
tauto.
Qed.
Lemma DN (P : Prop) : P -> ~~ P. Proof. tauto. Qed.
Lemma DN_impl (P Q : Prop) : (P -> ~~Q) -> ~~ P -> ~~ Q. Proof. tauto. Qed.
Lemma neg_impl (P Q : Prop) : (P -> ~Q) -> ~~ P -> ~ Q. Proof. tauto. Qed.
Lemma negative_dn (P Q : Prop) :
(~~Q -> Q) -> (P -> Q) -> ~~ P -> Q.
Proof.
tauto.
Qed.
Lemma negative_ca P Q :
(~~Q -> Q) -> (P \/ ~ P -> Q) -> Q.
Proof.
intros H1 H2. eapply (negative_dn (P \/ ~P) Q H1 H2).
tauto.
Qed.
Lemma stable_iff_negative P :
(~~P -> P) <-> (exists Q, P <-> ~ Q).
Proof.
firstorder. exists (~P). firstorder.
Qed.
Definition MP := forall f : nat -> bool, ~~ (exists n, f n = true) -> exists n, f n = true.
Lemma MP_ca (f : nat -> bool) P Q :
MP ->
(Q <-> (exists n, f n = true)) ->
((P \/ ~ P) -> Q) -> Q.
Proof.
intros mp ->. eapply negative_ca, mp.
Qed.
Fact computational_explosion (A : Type) : False -> A.
Proof.
tauto.
Qed.
Fact typecast X (A : X -> Type) (x1 x2 : X) :
x1 = x2 -> A x1 -> A x2.
Proof.
now intros ->.
Qed.
Tactic Notation "cprove" tactic3(tac) := apply DN; tac.
Lemma DN_dec (P : Prop) `{Dec.dec P} : ~~ P -> P.
Proof.
destruct H as [H | H1]; tauto.
Qed.
Tactic Notation "cunwrap" hyp(H) :=
(revert H; (apply DN_impl || apply neg_impl); intros H).
Tactic Notation "cunwrap" "one" := match goal with [H : ~~ ?P |- _ ] => cunwrap H end.
Tactic Notation "cunwrap" := repeat (cunwrap one).
Lemma ccase_neg P Q : ((P \/ ~ P) -> ~ Q) -> ~ Q.
Proof.
intros H. assert (H1 : ~~ (P \/ ~P)) by tauto.
intros q. apply H1. intros [Hp | Hp]; eapply H; eauto.
Qed.
Tactic Notation "ccase" constr(P) "as" intropattern(pat) :=
match goal with
| [ |- ~ ?G ] => eapply (ccase_neg P); intros pat
(* let H := fresh "H" in assert (H : ~~ (P \/ ~P)) by tauto; cunwrap H; revert H; intros pat *)
| [ |- ?G ] => eapply (@DN_dec _ _); eapply (ccase_neg P); intros pat; apply DN
(* let H := fresh "H" in assert (H : ~~ (P \/ ~P)) by tauto; cunwrap H; revert H; intros pat;
apply DN *)
end.
Tactic Notation "cstart" := eapply (@DN_dec _ _).
Inductive IsFilter {X} (p : X -> Prop) : list X -> list X -> Prop :=
IsFilter_nil : IsFilter p [] []
| IsFilter_cons1 l x l' : IsFilter p l l' -> p x -> IsFilter p (x :: l) (x :: l')
| IsFilter_cons2 l x l' : IsFilter p l l' -> ~ p x -> IsFilter p (x :: l) l'.
Lemma IsFilter_spec {X} l l' (p : X -> Prop) :
IsFilter p l l' -> length l' <= length l /\ (forall x0, In x0 l -> ~ p x0 -> length l' < length l) /\ forall x, In x l' <-> In x l /\ p x.
Proof.
induction 1; cbn; firstorder try congruence; lia.
Qed.
Require Import SyntheticComputability.Shared.Dec SyntheticComputability.Shared.ListAutomation.
Lemma IsFilter_filter {X} p (D : forall x : X, {p x} + {~ p x}) l :
IsFilter p l (filter (fun x => if D x then true else false) l).
Proof.
induction l; cbn.
- econstructor.
- destruct (D a) as [Ha | Ha]; econstructor; eauto.
Qed.
Lemma IsFilter_nnex {X} l (p : X -> Prop) :
~~ exists l', IsFilter p l l'.
Proof.
induction l as [ | x l IH].
- cprove exists []. econstructor.
- cunwrap. destruct IH as (l' & IH).
ccase (p x) as [Hx | Hx].
+ cprove exists (x :: l'). now econstructor.
+ cprove exists l'. now econstructor.
Qed.
Lemma IsFilter_ex {X} l (p : X -> Prop) (H : forall x, p x \/ ~ p x) :
exists l', IsFilter p l l'.
Proof.
induction l as [ | x l IH].
- exists []. econstructor.
- destruct IH as (l' & IH).
destruct (H x) as [Hx | Hx].
+ exists (x :: l'). now econstructor.
+ exists l'. now econstructor.
Qed.
#[export] Instance dec_lt {n m} : Dec.dec (n < m).
Proof.
eapply Compare_dec.lt_dec.
Qed.
Lemma remove_Sigma {X} (l : list X) x0 (H : forall x1 x2 : X, dec (x1 <> x2)) :
{ l' | length l' <= length l /\ (~~ In x0 l -> length l' < length l) /\ forall x, In x l' <-> In x l /\ x <> x0}.
Proof.
unshelve epose proof (IsFilter_filter (fun x => x <> x0) _ l) as (H1 & H2 & H3) % IsFilter_spec.
- abstract (firstorder).
- eexists. split. exact H1. firstorder. cstart. ccase (In x0 l) as [Hx | Hx]; firstorder.
Qed.
Lemma remove_ex {X} (l : list X) x0 (H : forall x1 x2 : X, (x1 <> x2) \/ ~ x1 <> x2) :
exists l', length l' <= length l /\ (~~ In x0 l -> length l' < length l) /\ forall x, In x l' <-> In x l /\ x <> x0.
Proof.
destruct (IsFilter_ex l (fun x => x <> x0)) as [l' (H1 & H2 & H3) % IsFilter_spec]; eauto.
exists l'. firstorder. cstart. ccase (In x0 l) as [Hx | Hx]; firstorder.
Qed.
Lemma remove_nnex {X} (l : list X) x0 :
~~ exists l', length l' <= length l /\ (In x0 l -> length l' < length l) /\ forall x, In x l' <-> In x l /\ x <> x0.
Proof.
pose proof (IsFilter_nnex l (fun x => x <> x0)) as H. cunwrap.
destruct H as [l' (H1 & H2 & H3) % IsFilter_spec].
cprove exists l'. eauto 7.
Qed.
Lemma in_ldec {X} (x : X) l (H : forall x1 x2 : X, x1 <> x2 \/ ~ x1 <> x2) :
~~ In x l \/ ~ In x l.
Proof.
induction l as [ | x' l [IH |IH]]; firstorder.
Qed.
Lemma in_dec {X} (x : X) l (H : forall x1 x2 : X, dec (x1 <> x2)) :
dec ( ~ In x l ).
Proof.
induction l as [ | x' l [IH |IH]]; firstorder.
Qed.
Lemma pigeonhole_Sigma {X} (l1 l2 : list X) (H : forall x1 x2 : X, dec (x1 <> x2)) :
NoDup l1 -> length l1 > length l2 -> { x | In x l1 /\ ~ In x l2}.
Proof.
intros Hd. revert l2. induction l1 as [ | x l1 IH]; cbn; intros.
- lia.
- destruct (in_dec x l2 H) as [Hx | Hx].
+ exists x. firstorder.
+ destruct (remove_Sigma l2 x H) as (l2_no_x & H1 & H2 % (fun H2 => H2 Hx) & H3).
edestruct (IH ltac:(now inversion Hd) l2_no_x) as (x0 & H4 & H5).
* lia.
* exists x0. inversion Hd. split. eauto. firstorder congruence.
Qed.
Lemma pigeonhole {X} (l1 l2 : list X) (H : forall x1 x2 : X, x1 <> x2 \/ ~ x1 <> x2) :
NoDup l1 -> length l1 > length l2 -> exists x, In x l1 /\ ~ In x l2.
Proof.
intros Hd. revert l2.
induction Hd; cbn; intros l2 Hle.
- lia.
- destruct (in_ldec x l2 H) as [Hx | Hx].
+ destruct (remove_ex l2 x H) as (l2_no_x & H1 & H2 % (fun H2 => H2 Hx) & H3).
edestruct (IHHd l2_no_x) as (x0 & H4 & H5).
* lia.
* exists x0. split. eauto. firstorder congruence.
+ exists x. firstorder.
Qed.
Lemma pigeonhole_constructive {X} (l1 l2 : list X) :
NoDup l1 -> length l1 > length l2 -> ~~ exists x, In x l1 /\ ~ In x l2.
Proof.
intros Hd. revert l2.
induction Hd; cbn; intros l2 Hle.
- lia.
- ccase (In x l2) as [Hx | Hx].
+ pose proof (remove_nnex l2 x) as H0. cunwrap. destruct H0 as (l2_no_x & H1 & H2 % (fun H2 => H2 Hx) & H3).
unshelve epose proof (IHHd l2_no_x _) as H0. 1:lia. cunwrap. destruct H0 as (x0 & H4 & H5).
cprove exists x0. split. eauto. firstorder congruence.
+ cprove exists x. firstorder.
Qed.
Lemma pigeonhole_length {X} (L1: list X) (Heq : forall x1 x2 : X, x1 <> x2 \/ ~ x1 <> x2) :
NoDup L1 -> forall L2, incl L1 L2 -> length L1 <= length L2.
Proof.
intros H L2 H1.
destruct (Nat.le_gt_cases (length L1) (length L2)) as [H0 | H0].
- assumption.
- eapply pigeonhole in H0.
+ destruct H0 as (x & H2 & H3). firstorder.
+ eassumption.
+ eauto.
Qed.
Require Import Setoid Morphisms.
Require Export Lia List NPeano.
Import ListNotations.
Fact ldec_stable P :
P \/ ~ P -> ~~ P -> P.
Proof.
tauto.
Qed.
Definition DNE := forall P, ~~ P -> P.
Definition LEM := forall P, P \/ ~ P.
Lemma LEM_DNE : LEM <-> DNE.
Proof.
split.
- intros lem P. destruct (lem P); intuition.
- intros dne P. eapply dne. tauto.
Qed.
Lemma DNI (P : Prop) : P -> ~~ P.
Proof.
tauto.
Qed.
Lemma DN (P : Prop) : P -> ~~ P. Proof. tauto. Qed.
Lemma DN_impl (P Q : Prop) : (P -> ~~Q) -> ~~ P -> ~~ Q. Proof. tauto. Qed.
Lemma neg_impl (P Q : Prop) : (P -> ~Q) -> ~~ P -> ~ Q. Proof. tauto. Qed.
Lemma negative_dn (P Q : Prop) :
(~~Q -> Q) -> (P -> Q) -> ~~ P -> Q.
Proof.
tauto.
Qed.
Lemma negative_ca P Q :
(~~Q -> Q) -> (P \/ ~ P -> Q) -> Q.
Proof.
intros H1 H2. eapply (negative_dn (P \/ ~P) Q H1 H2).
tauto.
Qed.
Lemma stable_iff_negative P :
(~~P -> P) <-> (exists Q, P <-> ~ Q).
Proof.
firstorder. exists (~P). firstorder.
Qed.
Definition MP := forall f : nat -> bool, ~~ (exists n, f n = true) -> exists n, f n = true.
Lemma MP_ca (f : nat -> bool) P Q :
MP ->
(Q <-> (exists n, f n = true)) ->
((P \/ ~ P) -> Q) -> Q.
Proof.
intros mp ->. eapply negative_ca, mp.
Qed.
Fact computational_explosion (A : Type) : False -> A.
Proof.
tauto.
Qed.
Fact typecast X (A : X -> Type) (x1 x2 : X) :
x1 = x2 -> A x1 -> A x2.
Proof.
now intros ->.
Qed.
Tactic Notation "cprove" tactic3(tac) := apply DN; tac.
Lemma DN_dec (P : Prop) `{Dec.dec P} : ~~ P -> P.
Proof.
destruct H as [H | H1]; tauto.
Qed.
Tactic Notation "cunwrap" hyp(H) :=
(revert H; (apply DN_impl || apply neg_impl); intros H).
Tactic Notation "cunwrap" "one" := match goal with [H : ~~ ?P |- _ ] => cunwrap H end.
Tactic Notation "cunwrap" := repeat (cunwrap one).
Lemma ccase_neg P Q : ((P \/ ~ P) -> ~ Q) -> ~ Q.
Proof.
intros H. assert (H1 : ~~ (P \/ ~P)) by tauto.
intros q. apply H1. intros [Hp | Hp]; eapply H; eauto.
Qed.
Tactic Notation "ccase" constr(P) "as" intropattern(pat) :=
match goal with
| [ |- ~ ?G ] => eapply (ccase_neg P); intros pat
(* let H := fresh "H" in assert (H : ~~ (P \/ ~P)) by tauto; cunwrap H; revert H; intros pat *)
| [ |- ?G ] => eapply (@DN_dec _ _); eapply (ccase_neg P); intros pat; apply DN
(* let H := fresh "H" in assert (H : ~~ (P \/ ~P)) by tauto; cunwrap H; revert H; intros pat;
apply DN *)
end.
Tactic Notation "cstart" := eapply (@DN_dec _ _).
Inductive IsFilter {X} (p : X -> Prop) : list X -> list X -> Prop :=
IsFilter_nil : IsFilter p [] []
| IsFilter_cons1 l x l' : IsFilter p l l' -> p x -> IsFilter p (x :: l) (x :: l')
| IsFilter_cons2 l x l' : IsFilter p l l' -> ~ p x -> IsFilter p (x :: l) l'.
Lemma IsFilter_spec {X} l l' (p : X -> Prop) :
IsFilter p l l' -> length l' <= length l /\ (forall x0, In x0 l -> ~ p x0 -> length l' < length l) /\ forall x, In x l' <-> In x l /\ p x.
Proof.
induction 1; cbn; firstorder try congruence; lia.
Qed.
Require Import SyntheticComputability.Shared.Dec SyntheticComputability.Shared.ListAutomation.
Lemma IsFilter_filter {X} p (D : forall x : X, {p x} + {~ p x}) l :
IsFilter p l (filter (fun x => if D x then true else false) l).
Proof.
induction l; cbn.
- econstructor.
- destruct (D a) as [Ha | Ha]; econstructor; eauto.
Qed.
Lemma IsFilter_nnex {X} l (p : X -> Prop) :
~~ exists l', IsFilter p l l'.
Proof.
induction l as [ | x l IH].
- cprove exists []. econstructor.
- cunwrap. destruct IH as (l' & IH).
ccase (p x) as [Hx | Hx].
+ cprove exists (x :: l'). now econstructor.
+ cprove exists l'. now econstructor.
Qed.
Lemma IsFilter_ex {X} l (p : X -> Prop) (H : forall x, p x \/ ~ p x) :
exists l', IsFilter p l l'.
Proof.
induction l as [ | x l IH].
- exists []. econstructor.
- destruct IH as (l' & IH).
destruct (H x) as [Hx | Hx].
+ exists (x :: l'). now econstructor.
+ exists l'. now econstructor.
Qed.
#[export] Instance dec_lt {n m} : Dec.dec (n < m).
Proof.
eapply Compare_dec.lt_dec.
Qed.
Lemma remove_Sigma {X} (l : list X) x0 (H : forall x1 x2 : X, dec (x1 <> x2)) :
{ l' | length l' <= length l /\ (~~ In x0 l -> length l' < length l) /\ forall x, In x l' <-> In x l /\ x <> x0}.
Proof.
unshelve epose proof (IsFilter_filter (fun x => x <> x0) _ l) as (H1 & H2 & H3) % IsFilter_spec.
- abstract (firstorder).
- eexists. split. exact H1. firstorder. cstart. ccase (In x0 l) as [Hx | Hx]; firstorder.
Qed.
Lemma remove_ex {X} (l : list X) x0 (H : forall x1 x2 : X, (x1 <> x2) \/ ~ x1 <> x2) :
exists l', length l' <= length l /\ (~~ In x0 l -> length l' < length l) /\ forall x, In x l' <-> In x l /\ x <> x0.
Proof.
destruct (IsFilter_ex l (fun x => x <> x0)) as [l' (H1 & H2 & H3) % IsFilter_spec]; eauto.
exists l'. firstorder. cstart. ccase (In x0 l) as [Hx | Hx]; firstorder.
Qed.
Lemma remove_nnex {X} (l : list X) x0 :
~~ exists l', length l' <= length l /\ (In x0 l -> length l' < length l) /\ forall x, In x l' <-> In x l /\ x <> x0.
Proof.
pose proof (IsFilter_nnex l (fun x => x <> x0)) as H. cunwrap.
destruct H as [l' (H1 & H2 & H3) % IsFilter_spec].
cprove exists l'. eauto 7.
Qed.
Lemma in_ldec {X} (x : X) l (H : forall x1 x2 : X, x1 <> x2 \/ ~ x1 <> x2) :
~~ In x l \/ ~ In x l.
Proof.
induction l as [ | x' l [IH |IH]]; firstorder.
Qed.
Lemma in_dec {X} (x : X) l (H : forall x1 x2 : X, dec (x1 <> x2)) :
dec ( ~ In x l ).
Proof.
induction l as [ | x' l [IH |IH]]; firstorder.
Qed.
Lemma pigeonhole_Sigma {X} (l1 l2 : list X) (H : forall x1 x2 : X, dec (x1 <> x2)) :
NoDup l1 -> length l1 > length l2 -> { x | In x l1 /\ ~ In x l2}.
Proof.
intros Hd. revert l2. induction l1 as [ | x l1 IH]; cbn; intros.
- lia.
- destruct (in_dec x l2 H) as [Hx | Hx].
+ exists x. firstorder.
+ destruct (remove_Sigma l2 x H) as (l2_no_x & H1 & H2 % (fun H2 => H2 Hx) & H3).
edestruct (IH ltac:(now inversion Hd) l2_no_x) as (x0 & H4 & H5).
* lia.
* exists x0. inversion Hd. split. eauto. firstorder congruence.
Qed.
Lemma pigeonhole {X} (l1 l2 : list X) (H : forall x1 x2 : X, x1 <> x2 \/ ~ x1 <> x2) :
NoDup l1 -> length l1 > length l2 -> exists x, In x l1 /\ ~ In x l2.
Proof.
intros Hd. revert l2.
induction Hd; cbn; intros l2 Hle.
- lia.
- destruct (in_ldec x l2 H) as [Hx | Hx].
+ destruct (remove_ex l2 x H) as (l2_no_x & H1 & H2 % (fun H2 => H2 Hx) & H3).
edestruct (IHHd l2_no_x) as (x0 & H4 & H5).
* lia.
* exists x0. split. eauto. firstorder congruence.
+ exists x. firstorder.
Qed.
Lemma pigeonhole_constructive {X} (l1 l2 : list X) :
NoDup l1 -> length l1 > length l2 -> ~~ exists x, In x l1 /\ ~ In x l2.
Proof.
intros Hd. revert l2.
induction Hd; cbn; intros l2 Hle.
- lia.
- ccase (In x l2) as [Hx | Hx].
+ pose proof (remove_nnex l2 x) as H0. cunwrap. destruct H0 as (l2_no_x & H1 & H2 % (fun H2 => H2 Hx) & H3).
unshelve epose proof (IHHd l2_no_x _) as H0. 1:lia. cunwrap. destruct H0 as (x0 & H4 & H5).
cprove exists x0. split. eauto. firstorder congruence.
+ cprove exists x. firstorder.
Qed.
Lemma pigeonhole_length {X} (L1: list X) (Heq : forall x1 x2 : X, x1 <> x2 \/ ~ x1 <> x2) :
NoDup L1 -> forall L2, incl L1 L2 -> length L1 <= length L2.
Proof.
intros H L2 H1.
destruct (Nat.le_gt_cases (length L1) (length L2)) as [H0 | H0].
- assumption.
- eapply pigeonhole in H0.
+ destruct H0 as (x & H2 & H3). firstorder.
+ eassumption.
+ eauto.
Qed.