diff --git a/.gitignore b/.gitignore index 673e7a7..a72dbf5 100644 --- a/.gitignore +++ b/.gitignore @@ -40,4 +40,5 @@ Makefile.conf *.blg *.vok *.vos -_build/ \ No newline at end of file +_build/ +agda \ No newline at end of file diff --git a/code/Decidability/DecidablePredicates.v b/code/Decidability/DecidablePredicates.v index b16cb50..ab08996 100644 --- a/code/Decidability/DecidablePredicates.v +++ b/code/Decidability/DecidablePredicates.v @@ -1,4 +1,5 @@ Require Import init.imports. +Require Import Inductive.Predicates. Section Definitions. @@ -103,12 +104,12 @@ Section Properties. + exact (isapropdecider p). + exact (isapropdeptypeddecider p). Qed. - + End Properties. Section ClosureProperties. - Lemma decidabledisj {X : UU} (p q : X → hProp) : (deptypeddecider p) → (deptypeddecider q) → (deptypeddecider (λ (x : X), (p x) ∨ (q x))). + Lemma decidabledisj {X : UU} (p q : X → hProp) : (deptypeddecider p) → (deptypeddecider q) → (deptypeddecider (preddisj p q)). Proof. intros decp decq x. induction (decp x). @@ -125,7 +126,7 @@ Section ClosureProperties. * exact (sumofmaps b b0). Qed. - Lemma decidableconj {X : UU} (p q : X → hProp) : (deptypeddecider p) → (deptypeddecider q) → (deptypeddecider (λ (x : X), (p x) ∧ (q x))). + Lemma decidableconj {X : UU} (p q : X → hProp) : (deptypeddecider p) → (deptypeddecider q) → (deptypeddecider (predconj p q)). Proof. intros decp decq x. induction (decp x), (decq x). @@ -135,7 +136,7 @@ Section ClosureProperties. - right. intros [pp qq]. exact (b pp). Qed. - Lemma decidableneg {X : UU} (p q : X → hProp) : (deptypeddecider p) → (deptypeddecider (λ (x : X), hneg (p x))). + Lemma decidableneg {X : UU} (p : X → hProp) : (deptypeddecider p) → (deptypeddecider (predneg p)). Proof. intros decp x. induction (decp x). @@ -144,105 +145,3 @@ Section ClosureProperties. Qed. End ClosureProperties. - -Section EqualityDeciders. - - Definition iseqdecider (X : UU) (f : X → X → bool) : UU := ∏ (x1 x2 : X), x1 = x2 <-> f x1 x2 = true. - - Definition eqdecider (X : UU) := ∑ (f : X → X → bool), (iseqdecider X f). - - Definition make_eqdecider {X : UU} {f : X → X → bool} : (iseqdecider X f) → eqdecider (X) := (λ is : (iseqdecider X f), (f,, is)). - - Lemma eqdecidertodeptypedeqdecider (X : UU) : (eqdecider X) → (isdeceq X). - Proof. - intros [f is] x y. - destruct (is x y) as [impl1 impl2]. - induction (f x y). - - left; apply impl2; apply idpath. - - right. intros eq. apply nopathsfalsetotrue. exact (impl1 eq). - Qed. - - Lemma deptypedeqdecidertoeqdecider (X : UU) : (isdeceq X) → (eqdecider X). - Proof. - intros is. - use tpair. - - intros x y. - induction (is x y). - + exact true. - + exact false. - - intros x y. - induction (is x y); simpl; split. - + exact (λ a : (x = y), (idpath true)). - + exact (λ b : (true = true), a). - + intros; apply fromempty; exact (b X0). - + intros; apply fromempty; exact (nopathsfalsetotrue X0). - Qed. - - Lemma eqdecidertoisapropeq (X : UU) (f : eqdecider X) : ∏ (x y : X) ,(isaprop (x = y)). - Proof. - intros x. - apply isaproppathsfromisolated. - intros y. - set (dec := eqdecidertodeptypedeqdecider X f). - apply (dec x). - Qed. - - Lemma isapropiseqdecider (X : UU) (f : X → X → bool) : (isaprop (iseqdecider X f)). - Proof. - apply isofhlevelsn. - intros is. - repeat (apply impred_isaprop + intros). - apply isapropdirprod; apply isapropimpl. - - induction (f t). - + apply isapropifcontr. - use iscontrloopsifisaset. - exact isasetbool. - + apply isapropifnegtrue. - exact nopathsfalsetotrue. - - apply eqdecidertoisapropeq. - use make_eqdecider. - + exact f. - + exact is. - Qed. - - Lemma pathseqdeciders (X : UU) (f g : X → X → bool) (isf : iseqdecider X f) (isg : iseqdecider X g) : f = g. - Proof. - apply funextsec; intros x. - apply funextsec; intros y. - destruct (isf x y) as [implf1 implf2]. - destruct (isg x y) as [implg1 implg2]. - induction (g x y). - - apply implf1; apply implg2. - apply idpath. - - induction (f x y). - + apply fromempty, nopathsfalsetotrue, implg1, implf2. - exact (idpath true). - + exact (idpath false). - Qed. - - Lemma isapropeqdecider (X : UU) : (isaprop (eqdecider X)). - Proof. - apply invproofirrelevance. - intros [f isf] [g isg]. - induction (pathseqdeciders X f g isf isg). - assert (eq : isf = isg). - - apply proofirrelevance. - apply isapropiseqdecider. - - induction eq. - apply idpath. - Qed. - - Lemma weqisdeceqiseqdecider (X : UU) : (isdeceq X) ≃ (eqdecider X). - Proof. - use make_weq. - - exact (deptypedeqdecidertoeqdecider X). - - apply isweqimplimpl. - + exact (eqdecidertodeptypedeqdecider X). - + exact (isapropisdeceq X). - + exact (isapropeqdecider X). - Qed. -End EqualityDeciders. - -Section ChoiceFunction. - -End ChoiceFunction. diff --git a/code/Enumerability/EnumerablePredicates.v b/code/Enumerability/EnumerablePredicates.v new file mode 100644 index 0000000..24f33c5 --- /dev/null +++ b/code/Enumerability/EnumerablePredicates.v @@ -0,0 +1,230 @@ +Require Import init.imports. +Require Import Inductive.Option. +Require Import Decidability.DecidablePredicates. +Require Import Inductive.Predicates. +Require Import util.NaturalEmbedding. + +Definition rangeequiv {X : UU} {Y : UU} (f g : X → Y) := ∏ (y : Y), ∥hfiber f y∥ <-> ∥hfiber g y∥. + +Notation "f ≡ᵣ g" := (rangeequiv f g) (at level 50). + +Section EnumerablePredicates. + + Definition ispredenum {X : UU} (p : X → hProp) (f : nat → option) := ∏ (x : X), (p x) <-> ∥(hfiber f (some x))∥. + + Definition predenum {X : UU} (p : X → hProp) := ∑ (f : nat → option), (ispredenum p f). + + Definition isenumerablepred {X : UU} (p : X → hProp) := ∥predenum p∥. + + Lemma isapropispredenum {X : UU} (p : X → hProp) (f : nat → option) : (isaprop (ispredenum p f)). + Proof. + apply impred_isaprop. + intros t. + apply isapropdirprod; apply isapropimpl, propproperty. + Qed. + + Lemma rangeequivtohomot {X : UU} (p q : X → hProp) (e1 : (predenum p)) (e2 : (predenum q)) : ((pr1 e1) ≡ᵣ (pr1 e2)) → p ~ q. + Proof. + intros req x. + destruct e1 as [f ispf]. + destruct e2 as [g ispg]. + destruct (req (some x)) as [impl1 impl2]. + destruct (ispf x) as [if1 if2]. + destruct (ispg x) as [ig1 ig2]. + use hPropUnivalence. + - intros px. + apply ig2, impl1, if1. + exact px. + - intros qx. + apply if2, impl2, ig1. + exact qx. + Qed. + + (* Closure properties *) + Lemma enumconj {X : UU} (p q : X → hProp) (deceq : isdeceq X) : (predenum p) → (predenum q) → (predenum (λ x : X, p x ∧ q x)). + Proof. + intros [f enumf] [g enumg]. + use tpair. + - intros n. + destruct (unembed n) as [m1 m2]. + induction (f m1), (g m2). + + induction (deceq a x). + * exact (some x). + * exact none. + + exact none. + + exact none. + + exact none. + - simpl. intros x. + split. intros [px qx]. + destruct (enumf x) as [enumfx1 enumfx2]. + destruct (enumg x) as [enumgx1 enumgx2]. + use squash_to_prop. + + exact (hfiber f (some x)). + + exact (enumfx1 px). + + apply propproperty. + + intros [m1 m1eq]. + use squash_to_prop. + * exact (hfiber g (some x)). + * exact (enumgx1 qx). + * apply propproperty. + * intros [m2 m2eq]. + apply hinhpr. + use make_hfiber. + -- exact (embed (m1,, m2)). + -- simpl. + induction (pathsinv0 (unembedinv (m1,, m2))). + induction (pathsinv0 (m1eq)), (pathsinv0 (m2eq)). + simpl. + induction (deceq x x). + ++ induction a. + apply idpath. + ++ apply fromempty, b. exact (idpath x). + + intros; split; use squash_to_prop. + * exact (hfiber + (λ n : nat, + coprod_rect (λ _ : X ⨿ unit, option) + (λ a : X, + match g (pr2 (unembed n)) with + | inl x => + coprod_rect (λ _ : (a = x) ⨿ (a != x), option) (λ _ : a = x, some x) + (λ _ : a != x, none) (deceq a x) + | inr _ => none + end) (λ _ : unit, match g (pr2 (unembed n)) with + | inl _ | _ => none + end) (f (pr1 (unembed n)))) (some x)). + * exact X0. + * apply propproperty. + * intros [mm enumff]. + destruct (enumg x), (enumf x). + apply pr3, hinhpr. + destruct (unembed mm) as [m1 m2]. + use make_hfiber. + -- exact m1. + -- assert (eq : m1 = Preamble.pr1 (m1,, m2)). + ++ apply idpath. + ++ induction eq. + assert (eq : m2 = Preamble.pr2 (m1,, m2)). + apply idpath. induction eq. + revert enumff. + induction (g m2). + induction (f m1). simpl. + induction (deceq a0 a). simpl. + induction a1. + apply idfun. + simpl; intros. apply fromempty. + exact (nopathsnonesome x enumff). + simpl; intros. apply fromempty. + exact (nopathsnonesome x enumff). + induction (f m1). simpl. intros. apply fromempty. exact (nopathsnonesome x enumff). + simpl. intros. apply fromempty. exact (nopathsnonesome x enumff). + * exact (hfiber + (λ n : nat, + coprod_rect (λ _ : X ⨿ unit, option) + (λ a : X, + match g (pr2 (unembed n)) with + | inl x => + coprod_rect (λ _ : (a = x) ⨿ (a != x), option) (λ _ : a = x, some x) + (λ _ : a != x, none) (deceq a x) + | inr _ => none + end) (λ _ : unit, match g (pr2 (unembed n)) with + | inl _ | _ => none + end) (f (pr1 (unembed n)))) (some x)). + * exact X0. + * apply propproperty. + * intros [mm enumgg]. + destruct (enumg x), (enumf x). + apply pr2, hinhpr. + destruct (unembed mm) as [m1 m2]. + use make_hfiber. + -- exact m2. + -- assert (eq : m1 = Preamble.pr1 (m1,, m2)). + ++ apply idpath. + ++ induction eq. + assert (eq : m2 = Preamble.pr2 (m1,, m2)). + apply idpath. induction eq. + revert enumgg. + induction (g m2). + induction (f m1). simpl. + induction (deceq a0 a). simpl. + induction a1. + apply idfun. + simpl; intros. apply fromempty. + exact (nopathsnonesome x enumgg). + simpl; intros. apply fromempty. + exact (nopathsnonesome x enumgg). + induction (f m1). simpl. intros. apply fromempty. exact (nopathsnonesome x enumgg). + simpl. intros. apply fromempty. exact (nopathsnonesome x enumgg). + Defined. + + Lemma enumdisj {X : UU} (p q : X → hProp) : (predenum p) → (predenum q) → (predenum (λ x : X, p x ∨ q x)). + Proof. + intros [f enumff] [g enumgg]. + use tpair. + - intros n. + destruct (unembed n) as [m1 m2]. + induction m1. + exact (f m2). + exact (g m2). + - simpl. + intros x; split; intros. + destruct (enumff x), (enumgg x); clear enumff enumgg. + use squash_to_prop. exact (p x ⨿ q x). exact X0. apply propproperty. intros [px | qx]; clear X0. + + use squash_to_prop. exact (hfiber f (some x)). exact (pr1 px). apply propproperty. intros [m2 feq]. + apply hinhpr. use make_hfiber. + exact (embed (0,, m2)). simpl. + rewrite -> (unembedinv (0,, m2)). simpl. exact feq. + + use squash_to_prop. exact (hfiber g (some x)). exact (pr0 qx). apply propproperty. intros [m2 geq]. + apply hinhpr. use make_hfiber. + exact (embed (1,, m2)). simpl. + rewrite -> (unembedinv (1,, m2)). simpl. exact geq. + + use squash_to_prop. + * exact (hfiber + (λ n : nat, + nat_rect (λ _ : nat, option) (f (pr2 (unembed n))) + (λ (_ : nat) (_ : option), g (pr2 (unembed n))) (pr1 (unembed n))) + (some x)). + * exact X0. + * apply propproperty. + * clear X0. intros [n feq]. revert feq. + destruct (unembed n) as [m1 m2]. + assert (eq1 : m1 = pr1 (m1,, m2)) by apply idpath. + assert (eq2 : m2 = pr2 (m1,, m2)) by apply idpath. + induction eq1, eq2. + induction m1; intros; apply hinhpr. + -- left. + destruct (enumff x). + apply pr2, hinhpr. exact (m2,, feq). + -- right. + destruct (enumgg x). + apply pr2, hinhpr. exact (m2,, feq). + Defined. + + Lemma isenumerableconj {X : UU} (p q : X → hProp) : (isdeceq X) → (isenumerablepred p) → (isenumerablepred q) → (isenumerablepred (predconj p q)). + Proof. + intros. + use squash_to_prop. + exact (predenum p). exact X1. apply propproperty. intros. + use squash_to_prop. + exact (predenum q). exact X2. apply propproperty. intros. + apply hinhpr. exact (enumconj p q X0 X3 X4). + Qed. + + Lemma isenumerabledisj {X : UU} (p q : X → hProp) : (isenumerablepred p) → (isenumerablepred q) → (isenumerablepred (preddisj p q)). + Proof. + intros. + use squash_to_prop. + - exact (predenum p). + - exact X0. + - apply propproperty. + - intros. + use squash_to_prop. + + exact (predenum q). + + exact X1. + + apply propproperty. + + intros. apply hinhpr. + exact (enumdisj p q X2 X3). + Qed. + +End EnumerablePredicates. + + diff --git a/code/Enumerability/EnumerableTypes.v b/code/Enumerability/EnumerableTypes.v new file mode 100644 index 0000000..de4255b --- /dev/null +++ b/code/Enumerability/EnumerableTypes.v @@ -0,0 +1,463 @@ +Require Import init.imports. +Require Import Enumerability.EnumerablePredicates. +Require Import Decidability.DecidablePredicates. +Require Import util.NaturalEmbedding. +Require Import Inductive.Option. +Require Import Inductive.Predicates. +Require Import util.NaturalEmbedding. +Require Import Inductive.ListProperties. + +Section Definitions. + + Definition isenumerator (X : UU) (f : nat → @option X) := ∏ (x : X), ∃ (n : nat), (f n) = some x. + Definition enumerator (X : UU) := ∑ (f : nat → @option X), (isenumerator X f). + Definition isenumerable (X : UU) := ∥enumerator X∥. + + Lemma isapropisenumerator (X : UU) (f : nat → @option X) : isaprop (isenumerator X f). + Proof. + apply impred_isaprop. + intros t; apply propproperty. + Qed. + + Lemma isapropisenumerable (X : UU) (f : nat → @option X) : isaprop (isenumerable X). + Proof. + apply propproperty. + Qed. + +End Definitions. + +Section TypePredicateEnumerabilityEquivalence. + Lemma typeenumtopredenum (X : UU) (f : nat → @option X) : (isenumerator X f) → (ispredenum (truepred X) f). + Proof. + intros isenumf x. + split; intros. + - exact (isenumf x). + - exact tt. + Defined. + + Lemma predenumtotypeenum (X : UU) (f : nat → @option X) : (ispredenum (truepred X) f) → (isenumerator X f). + Proof. + intros isenumpred x. + destruct (isenumpred x); clear isenumpred. + exact (pr1 tt). + Defined. + + Lemma isenumerabletypetoisenumerablepred (X : UU) : (isenumerable X) ≃ (isenumerablepred (truepred X)). + use weqiff. + - split. + + intros isenumx; use (squash_to_prop isenumx (propproperty _)); intros [f isenum]; apply hinhpr. + exact (f,, (typeenumtopredenum X f isenum)). + + intros isenumpred; use (squash_to_prop isenumpred (propproperty _)); intros [f predenum]; apply hinhpr. + exact (f,, (predenumtotypeenum X f predenum)). + - apply propproperty. + - apply propproperty. + Qed. + + Lemma isdecenumerabletypetoenumerablepred (X : UU) (p : X → hProp) (d : decider p) (e : enumerator X) : (predenum p). + Proof. + destruct d as [f decf]. + destruct e as [g enumg]. + use tpair. + - intros n. + induction (g n). + + induction (f a). + * exact (some a). + * exact none. + + exact none. + - intros x. + destruct (decf x) as [dec1 dec2]. + split; intros. + + set (q := (enumg x)). + use squash_to_prop. + * exact (∑ (n : nat), (g n) = (some x)). + * exact q. + * apply propproperty. + * intros [n neqx]. apply hinhpr. + simpl. + use make_hfiber. + -- exact n. + -- simpl. induction (pathsinv0 neqx). + simpl. induction (pathsinv0 (dec1 X0)). + apply idpath. + + use squash_to_prop. + * exact (hfiber + (λ n : nat, + let o := g n in + coprod_rect (λ _ : X ⨿ unit, option) + (λ a : X, let b := f a in bool_rect (λ _ : bool, option) (some a) none b) + (λ _ : unit, none) o) (some x)). + * exact X0. + * apply propproperty. + * intros [a aa]. + revert aa. simpl. + induction (g a); simpl. + -- assert (q : (f a0) = true → x = a0 → (f x) = true). + ++ intros. induction X2. + exact X1. + ++ induction (f a0). + ** simpl. + intros. + set (bb := (some_injectivity a0 x aa)). + apply dec2, (q (idpath true) (pathsinv0 bb)). + ** simpl; intros. + apply fromempty. exact (nopathsnonesome x aa). + -- intros i. apply fromempty. exact (nopathsnonesome x i). + Defined. + + Lemma isdecidablepredenumerabletypetoenumneg (X : UU) (p : X → hProp) : (enumerator X) → (decider p) → (predenum (predneg p)). + Proof. + intros f g. + use isdecenumerabletypetoenumerablepred. + - apply deptypeddecidertodecider. + use decidableneg. + apply decidertodeptypeddecider. + exact g. + - exact f. + Qed. + +End TypePredicateEnumerabilityEquivalence. + +Section StrongEnumerability. + + Definition isstrongenumerator (X : UU) (f : nat → X) := (issurjective f). + + Definition strongenumerator (X : UU) := ∑ (f : nat → X), isstrongenumerator X f. + + Definition isstrongenumerable (X : UU) := ishinh (strongenumerator X). + + Lemma strongenumeratortoenumerator {X : UU} : strongenumerator X → enumerator X. + Proof. + intros [f isstrenum]. + use tpair; cbn beta. + - intros n. exact (some (f n)). + - intros x. use (squash_to_prop (isstrenum x) (propproperty _)); intros [n eq]; clear isstrenum; apply hinhpr. + use tpair; cbn beta. exact n. rewrite -> eq. apply idpath. + Defined. + + Lemma isstrongenumerabletoisenumerable {X : UU} : isstrongenumerable X → isenumerable X. + Proof. + intros enum. use (squash_to_prop enum (propproperty _)); clear enum; intros enum; apply hinhpr. + apply strongenumeratortoenumerator. exact enum. + Qed. + + Lemma inhabittedenumeratortostrongenumerator {X : UU} : X → enumerator X → strongenumerator X. + Proof. + intros x [f isenum]. + use tpair. + - intros n. induction (f n). + + exact a. + + exact x. + - intros y. use (squash_to_prop (isenum y) (propproperty _)); intros [n eq]; apply hinhpr. + use tpair. + exact n. cbn beta. rewrite -> eq. apply idpath. + Defined. + + Lemma inhabittedenumerabletostrongenumerable {X : UU} : (ishinh X) → isenumerable X → isstrongenumerable X. + Proof. + intros x isenum. + use (squash_to_prop x (propproperty _)); clear x; intros x. + use (squash_to_prop (isenum) (propproperty _)); clear isenum; intros enum. apply hinhpr. + apply inhabittedenumeratortostrongenumerator. exact x. exact enum. + Qed. + + Lemma strongenumerableinhabitted {X : UU} : isstrongenumerable X → (ishinh X). + Proof. + intros isenum. + use (squash_to_prop (isenum) (propproperty _)); clear isenum; intros [f isenum]; apply hinhpr. + exact (f 0). + Qed. + +End StrongEnumerability. + +Section ClosureProperties. + + Lemma enumeratornat : (isenumerator nat (λ (n : nat), (some n))). + Proof. + intros n. + apply hinhpr. + exact (n,, (idpath _)). + Qed. + + Lemma enumeratorbool : (isenumerator bool (λ (n : nat), (nat_rect _ (some true) (λ (n : nat) _ , (some false)) n))). + Proof. + intros b; apply hinhpr. + induction b. + - exact (0,, (idpath _)). + - exact (1,, (idpath _)). + Qed. + + Lemma enumeratorunit : (isenumerator unit (λ (n : nat), (some tt))). + Proof. + intros x; apply hinhpr. + induction x. + exact (0,, (idpath _)). + Qed. + + Lemma enumeratoroption (X : UU) (f : nat → @option X) : (isenumerator X f) → (isenumerator (@option X) (nat_rect (λ _, @option (@option X)) (some none) (λ (n : nat) _, some (f n)))). + Proof. + intros enumff x. + induction x. + - use squash_to_prop. + + exact (hfiber f (some a)). + + exact (enumff a). + + apply propproperty. + + clear enumff; intros [n hfib]. + apply hinhpr. + use tpair. + * exact (S n). + * simpl. apply maponpaths. exact hfib. + - apply hinhpr. + use tpair. + * exact 0. + * simpl; induction b; apply idpath. + Qed. + + Definition enumeratorfunctiondirprod (X Y : UU) (f : nat → @option X) (g : nat → @option Y) : nat → @option (X × Y). + Proof. + intros n. + destruct (unembed n) as [m1 m2]. + clear n. + induction (f m1), (g m2). + - exact (some (a,, y)). + - exact none. + - exact none. + - exact none. + Defined. + + Lemma enumeratordirprod (X Y : UU) (f : nat → @option X) (g : nat → @option Y) :(isenumerator X f) → (isenumerator Y g) → isenumerator (X × Y) (enumeratorfunctiondirprod X Y f g). + Proof. + intros enumff enumgg [a b]. + use (squash_to_prop (enumff a)). apply propproperty. + - intros [n hfibf]. clear enumff. + use (squash_to_prop (enumgg b)). apply propproperty. + + intros [m hfibg]. clear enumgg. + apply hinhpr; use make_hfiber. + * exact (embed (n,, m)). + * unfold enumeratorfunctiondirprod. + rewrite -> (unembedinv (n,, m)), hfibf, hfibg. + simpl; apply idpath. + Qed. + + Definition enumeratorfunctioncoprod (X Y : UU) (f : nat → @option X) (g : nat → @option Y) : nat → (@option (X ⨿ Y)). + Proof. + intros n; destruct (unembed n) as [m1 m2]; clear n. + induction m1. + - induction (f m2). + + exact (some (ii1 a)). + + exact (none). + - induction (g m2). + + exact (some (ii2 a)). + + exact none. + Defined. + + Definition enumeratorcoprod (X Y : UU) (f : nat → @option X) (g : nat → @option Y) : (isenumerator X f) → (isenumerator Y g) → (isenumerator (X ⨿ Y) (enumeratorfunctioncoprod X Y f g)). + Proof. + intros enumff enumgg [x | y]. + - use (squash_to_prop (enumff x) (propproperty _)). + intros [n hfibf]. apply hinhpr. + use make_hfiber. + + exact (embed (0,, n)). + + unfold enumeratorfunctioncoprod. + rewrite -> (unembedinv), hfibf. + simpl. apply idpath. + - use (squash_to_prop (enumgg y) (propproperty _)). + intros [n hfibg]. apply hinhpr. + use make_hfiber. + + exact (embed (1,, n)). + + unfold enumeratorfunctioncoprod. + rewrite -> (unembedinv), hfibg. + simpl. apply idpath. + Qed. + + Lemma isenumerablenat : (isenumerable nat). + Proof. + apply hinhpr. + exact ((λ (n : nat), (some n)),, enumeratornat). + Qed. + + Lemma isenumerablebool : (isenumerable bool). + Proof. + apply hinhpr. + use tpair. + exact (λ (n : nat), (nat_rect _ (some true) (λ (n : nat) _ , (some false))) n). + exact (enumeratorbool). + Qed. + + Lemma isenumerabledirprod (X Y : UU) : (isenumerable X) → (isenumerable Y) → (isenumerable (X × Y)). + Proof. + intros isenumf isenumg. + use (squash_to_prop (isenumf) (propproperty _)). + intros [f enumf]; clear isenumf. + use (squash_to_prop (isenumg) (propproperty _)). + intros [g enumg]; clear isenumg. + apply hinhpr. + use tpair. + - exact (enumeratorfunctiondirprod X Y f g). + - exact (enumeratordirprod X Y f g enumf enumg). + Qed. + + Lemma isenumerablecoprod (X Y : UU) : (isenumerable X) → (isenumerable Y) → (isenumerable (X ⨿ Y)). + Proof. + intros isenumf isenumg. + use (squash_to_prop (isenumf) (propproperty _)). + intros [f enumf]; clear isenumf. + use (squash_to_prop (isenumg) (propproperty _)). + intros [g enumg]; clear isenumg. + apply hinhpr. + use tpair. + - exact (enumeratorfunctioncoprod X Y f g). + - exact (enumeratorcoprod X Y f g enumf enumg). + Qed. + + Lemma isenumerableoption (X : UU) : (isenumerable X) → (isenumerable (@option X)). + Proof. + intros isenumx. + use (squash_to_prop (isenumx) (propproperty _)); intros [f enumx]; apply hinhpr. + use tpair. + - exact (nat_rect (λ _, @option (@option X)) (some none) (λ (n : nat) _, some (f n))). + - exact (enumeratoroption X f enumx). + Qed. + + Lemma kfinstructenumerator {X : UU} (kfin : kfinstruct X) : (enumerator X). + Proof. + destruct kfin as [n [f issurj]]. + use tpair. + - intros m. + induction (natlthorgeh m n). + + exact (some (f (m,, a))). + + exact none. + - intros ?. + use (squash_to_prop (issurj x) (propproperty _)); clear issurj; intros [[m nltm] eq]. apply hinhpr. + use tpair. exact m. cbn beta. induction (natlthorgeh m n); simpl. + assert (a = nltm) by apply propproperty. rewrite -> X0. rewrite <- eq. apply idpath. + apply fromempty. apply (natgehtonegnatlth _ _ b). exact nltm. + Defined. + + Lemma iskfiniteisenumerable {X : UU} : (iskfinite X) → (isenumerable X). + Proof. + intros isk. use (squash_to_prop isk (propproperty _)); intros enum; apply hinhpr. + apply kfinstructenumerator. exact enum. + Qed. + + Lemma finstructenumerator {X : UU} : (finstruct X) → (enumerator X). + Proof. + intros finstr. apply kfinstructenumerator. apply kfinstruct_finstruct. + exact finstr. + Defined. + + Lemma isfiniteisenumerable {X : UU} : (isfinite X) → (isenumerable X). + Proof. + intros isf. use (squash_to_prop isf (propproperty _)); intros finstr; apply hinhpr. + exact (finstructenumerator finstr). + Qed. +End ClosureProperties. + +Section ListEnumerability. + Definition islistenumerator (X : UU) (L : nat → list X) := ∏ (x : X), ∃ (n : nat), (is_in x (L n)). + + Definition listenumerator (X : UU) := ∑ (L : nat → list X), (islistenumerator X L). + + Definition islistenumerable (X : UU) := ishinh (listenumerator X). + + Lemma enumeratortolistenumerator (X : UU) (E : enumerator X) : (listenumerator X). + Proof. + destruct E as [E isenum]. + use tpair. (**TODO: to replace with make_enumerator? **) + - intros n. + induction (E n). + + exact (cons a nil). + + exact nil. + - intros x. + use squash_to_prop. + + exact (hfiber E (some x)). + + exact (isenum x). + + apply propproperty. + + intros [n nfib]; clear isenum; apply hinhpr. + use tpair. + * exact n. + * cbn beta. rewrite -> nfib. right; apply idpath. + Defined. + + Lemma listenumeratortoenumerator (X : UU) (L : listenumerator X) : (enumerator X). + Proof. + destruct L as [L islstenum]. + use tpair. + - intros n. + destruct (unembed n) as [m1 m2]; clear n. + exact (pos (L m1) m2). + - intros x. + use squash_to_prop. + + exact (∑ (n : nat), (is_in x (L n))). + + exact (islstenum x). + + apply propproperty. + + intros [n inn]; apply hinhpr. + use tpair. + * exact (embed (n,, (elem_pos x (L n) inn))). + * cbn beta; rewrite -> unembedinv; simpl. + apply poselem_posinv. + Defined. + + Lemma weqisenumerableislistenumerable (X : UU) : (isenumerable X) ≃ (islistenumerable X). + Proof. + use weqiff. + - split; intros x; use (squash_to_prop x (propproperty _)); intros enum; apply hinhpr. + + exact (enumeratortolistenumerator X enum). + + exact (listenumeratortoenumerator X enum). + - apply propproperty. + - apply propproperty. + Qed. + + Local Infix "++" := concatenate. + + Definition listfun (X : UU) (L : nat → list X) : (nat → (list (list X))). + Proof. + intros n; induction n. + - exact (cons nil nil). + - exact (IHn ++ (map (λ (x : (X×(list X))), (cons (pr1 x) (pr2 x))) (list_prod (cumul L n) IHn))). + Defined. + + Lemma iscumulativelistfun (X : UU) (L : nat → list X) : (iscumulative (listfun X L)). + Proof. + intros ?; simpl. + use (tpair _ (map (λ x : X × list X, cons (pr1 x) (pr2 x)) (list_prod (cumul L n) (listfun X L n)))); apply idpath. + Defined. + + Lemma listlistenumerator (X : UU) (L : nat → list X) : (islistenumerator X L) → (islistenumerator (list X) (listfun X L)). + Proof. + intros lstenm. + use list_ind; cbn beta. + - apply hinhpr. use (tpair _ 0). right; apply idpath. + - intros. + use (squash_to_prop X0 (propproperty _)); intros [n inn1]; clear X0. + use (squash_to_prop (lstenm x) (propproperty _)); intros [m inn2]; clear lstenm. + apply hinhpr; use tpair; cbn beta. + + induction (natlthorgeh n m). exact (S m). exact (S n). + + induction (natlthorgeh n m); simpl. + * induction m. apply fromempty. apply (negnatlthn0 n a). + set (q := (isincumulleh _ _ (iscumulativelistfun _ _) n (S m) (natlthtoleh _ _ a) inn1)). + simpl. apply isin_concatenate2. apply (is_inmap (λ (x : X × (list X)), (cons (pr1 x) (pr2 x))) _ (x,, xs)), inn_list_prod1. apply isin_concatenate2. exact inn2. + exact q. + * induction n. set (q := (nat0gehtois0 m b)). induction (pathsinv0 q). clear q. + apply isin_concatenate2. apply (is_inmap (λ (x : X × (list X)), (cons (pr1 x) (pr2 x))) _ (x,, xs)). apply inn_list_prod1. exact inn2. exact inn1. + apply isin_concatenate2. apply (is_inmap (λ (x : X × (list X)), (cons (pr1 x) (pr2 x))) _ (x,, xs)). apply inn_list_prod1. + assert (inn3 : is_in x (cumul L m)) by apply (isinlisincumull _ _ _ inn2). + apply (isincumulleh _ _ (iscumulativecumul _) m (S n) b inn3). + apply inn1. + Defined. + + Lemma islistenumerablelist {X : UU} (isenum : islistenumerable X) : (islistenumerable (list X)). + Proof. + use squash_to_prop. + - exact (listenumerator X). + - exact isenum. + - apply propproperty. + - clear isenum; intros [L isenum]. apply hinhpr. + exact ((listfun X L),, (listlistenumerator X L isenum)). + Qed. + + Lemma isenumerablelist {X : UU} (isenum : isenumerable X) : (isenumerable (list X)). + Proof. + apply weqisenumerableislistenumerable, islistenumerablelist, weqisenumerableislistenumerable. exact isenum. + Qed. + +End ListEnumerability. \ No newline at end of file diff --git a/code/Inductive/ListProperties.v b/code/Inductive/ListProperties.v index ab70f51..bff03c9 100644 --- a/code/Inductive/ListProperties.v +++ b/code/Inductive/ListProperties.v @@ -1,5 +1,5 @@ Require Import init.imports. -Require Import UniMath.Combinatorics.Lists. +Require Import Inductive.Option. Section Definitions. @@ -203,7 +203,210 @@ Section Filter. End Filter. +Section Position. + Definition pos {X : UU} : (list X) → nat → @option X. + Proof. + use list_ind; cbn beta. + - exact (λ _, none). + - intros xs l f n. + induction n. + + exact (some xs). + + exact (f n). + Defined. + + Definition elem_pos {X : UU} (x : X) (l : list X) (inn : is_in x l) : nat. + Proof. + revert l inn. + use list_ind. + - intros inn. apply fromempty; exact inn. + - intros x0 xs f inn. + destruct inn as [l | r]. + + exact (S (f l)). + + exact 0. + Defined. + + Lemma bla {X : UU} (x : X) (l : list X) (inn : is_in x l) (n : nat) : (elem_pos x l inn) = n → (pos l n) = (some x). + Proof. + revert l n inn. + use list_ind. + - intros n inn. exact (fromempty inn). + - cbn beta. intros x0 xs IHn n inn eq. + destruct inn as [l | r]. + + induction n. + * apply fromempty. exact (negpathssx0 _ eq). + * assert (elem_pos x xs l = n) by exact (invmaponpathsS _ _ eq). + assert (pos (cons x0 xs) (S n) = pos xs n) by apply idpath. + rewrite X1. exact (IHn n l X0). + + induction n. + * assert (pos (cons x0 xs) 0 = some x0) by apply idpath; rewrite -> X0; apply maponpaths. + exact (pathsinv0 r). + * apply fromempty. exact (negpaths0sx _ eq). + Defined. + + Lemma poselem_posinv {X : UU} (x : X) (l : list X) (inn : is_in x l) : pos l (elem_pos x l inn) = some x. + Proof. + apply (bla x l inn). + apply idpath. + Defined. + +End Position. + +Section Append. + + Definition append {X : UU} : (list X) → (list X) → (list X). + Proof. + use list_ind; cbn beta. + - exact (idfun _). + - intros. exact (cons x (X0 X1)). + Defined. + + Section AppendTests. + Definition l0 : list nat := (cons 0 (cons 1 (cons 2 nil))). + Definition l1 : list nat := (cons 1 (cons 2 (cons 3 nil))). + Definition l2 : list nat := (cons 0 (cons 1 (cons 2 (cons 1 (cons 2 (cons 3 nil)))))). + + Example testappend : (append l0 l1) = l2. Proof. apply idpath. Qed. + + Example testappendnilleft : (append nil l1) = l1. Proof. apply idpath. Qed. + + Example testappendnilright: (append l2 nil) = l2. Proof. apply idpath. Qed. + + End AppendTests. + + Local Infix "++" := concatenate. + + Lemma isin_concatenate1 {X : UU} (l1 l2 : list X) (x : X) : (is_in x l1) → (is_in x (l1 ++ l2)). + Proof. + revert l1. + use list_ind; cbn beta; intros. + - apply fromempty; exact X0. + - rewrite -> (concatenateStep x0 xs l2). + destruct X1 as [l | r]. + + left; apply X0; exact l. + + right; exact r. + Defined. + + Lemma isin_concatenate2 {X : UU} (l1 l2 : list X) (x : X) : (is_in x l2) → (is_in x (l1 ++ l2)). + Proof. + revert l1. + use list_ind; cbn beta; intros. + - rewrite -> (nil_concatenate l2); exact X0. + - rewrite -> (concatenateStep x0 xs l2). left. exact (X0 X1). + Defined. + + Lemma isin_concatenate_choice {X : UU} (l1 l2 : list X) (x : X) : (is_in x (l1 ++ l2)) → (is_in x l1) ⨿ (is_in x l2). + Proof. + revert l1. + use list_ind; cbn beta. + - rewrite -> nil_concatenate. intros inn; right; exact inn. + - intros x0 xs IHl. rewrite -> (concatenateStep x0 xs l2). intros [l | r]. + + induction (IHl l) as [a | a]. left; left; exact a. right; exact a. + + left; right; exact r. + Defined. +End Append. + +Section ListProduct. +Local Infix "++" := concatenate. + Definition list_prod {X Y : UU} (l1 : list X) (l2 : list Y) : (list (X × Y)). + Proof. + revert l1. + use list_ind; cbn beta. + - exact nil. + - intros; exact ((map (λ (y : Y), (x,, y)) l2) ++ X0). + Defined. + + Lemma inn_list_prod1 {X Y : UU} (l1 : list X) (l2 : list Y) (x : X) (y : Y) : (is_in x l1) → (is_in y l2) → (is_in (x,, y) (list_prod l1 l2)). + Proof. + revert l1. + use list_ind; cbn beta. + - exact fromempty. + - intros x0 xs IHl inn1 inn2. + destruct inn1 as [l | r]. + + apply isin_concatenate2. exact (IHl l inn2). + + apply isin_concatenate1. rewrite <- r. clear IHl r x0. + revert l2 inn2. use list_ind; cbn beta. + * exact (fromempty). + * intros y0 ys IHl [l | r]; rewrite -> (mapStep). + -- left. exact (IHl l). + -- right. rewrite -> r. apply idpath. + Defined. +End ListProduct. + +Section Map. + + Lemma is_inmap {X Y : UU} (f : X → Y) (l : list X) (x : X) : (is_in x l) → (is_in (f x) (map f l)). + Proof. + revert l. use list_ind; cbn beta. + - exact fromempty. + - intros x0 xs IHl [l | r]. + + left. exact (IHl l). + + right. apply maponpaths. exact r. + Defined. +End Map. + +Section CumulativeFunctions. + + Local Infix "++" := concatenate. + Definition iscumulative {X : UU} (L : nat → list X) := ∏ (n : nat), ∑ (l : list X), (L (S n) = ((L n) ++ l)). + + Lemma cumulativenleqm {X : UU} (L : nat → list X) (iscum : (iscumulative L)) (m n : nat) : n ≤ m → ∑ (l : list X), L m = (L n) ++ l. + Proof. + intros nleqm. + assert (eq : ∑ (k : nat), n + k = m). + - use tpair. + + exact (m - n). + + cbn beta. rewrite -> (natpluscomm n (m - n)). apply (minusplusnmm _ _ nleqm). + - destruct eq as [k eq]. + induction eq; induction k. + + rewrite (natpluscomm n 0). use (tpair _ nil). simpl. rewrite -> (concatenate_nil (L n)). apply idpath. + + rewrite (natplusnsm n k); destruct (iscum (n + k)) as [l eq]; clear iscum. + destruct (IHk (natlehnplusnm _ _)) as [l0 neq]; clear IHk. + use (tpair _ (l0 ++ l)). simpl. rewrite -> eq, neq. apply assoc_concatenate. + Qed. + + Definition cumul {X : UU} : (nat → list X) → (nat → list X). + Proof. + intros L n. + induction n. + - exact (L 0). + - exact (IHn ++ (L (S n))). + Defined. + + Lemma iscumulativecumul {X : UU} (L : nat → list X) : (iscumulative (cumul L)). + Proof. + intros n; induction n. + - use (tpair _ (L 1) (idpath _)). + - use (tpair _ (L (S (S n))) (idpath _)). + Defined. + + Lemma isinlisincumull {X : UU} (L : nat → list X) (x : X) (n : nat) : (is_in x (L n)) → (is_in x (cumul L n)). + Proof. + intros inn. + induction n. + - exact inn. + - simpl. apply isin_concatenate2. exact inn. + Defined. + + Lemma isincumulleh {X : UU} (L : nat → list X) (x : X) (iscum : iscumulative L) (n m: nat) : (n ≤ m) → (is_in x (L n)) → (is_in x (L m)). + Proof. + intros leq inn. + set (q := cumulativenleqm L iscum m n leq); destruct q as [l eq]; rewrite -> eq. + apply isin_concatenate1. exact inn. + Defined. + + Lemma iscumulex {X : UU} (L : nat → list X) (x : X) : (∃ (n : nat), (is_in x (L n))) <-> (∃ (n : nat), (is_in x (cumul L n))). + Proof. + split; intros ex; use (squash_to_prop ex (propproperty _)); clear ex; intros [n inn]; apply hinhpr. + - use (tpair _ n); cbn beta. + apply isinlisincumull. exact inn. + - induction n. + + use (tpair _ 0). exact inn. + + induction (isin_concatenate_choice (cumul L n) (L (S n)) x inn). + * exact (IHn a). + * exact ((S n),, b). + Defined. +End CumulativeFunctions. Section Properties. diff --git a/code/Inductive/Predicates.v b/code/Inductive/Predicates.v new file mode 100644 index 0000000..9888f77 --- /dev/null +++ b/code/Inductive/Predicates.v @@ -0,0 +1,35 @@ +Require Import init.imports. + +(* + +This file contains definitions of the used operations on predicates and a number of useful +properties. + +*) + + +Section Operations. + + Definition predconj {X : UU} (p q : X → hProp) : X → hProp := (λ x : X, (p x) ∧ (q x)). + + Definition preddisj {X : UU} (p q : X → hProp) : X → hProp := (λ x : X, (p x) ∨ (q x)). + + Definition predneg {X : UU} (p : X → hProp) : X → hProp := (λ x : X, hneg (p x)). + + Definition preddirprod {X Y : UU} (p : X → hProp) (q : Y → hProp) : (X × Y) → hProp := (λ x : X × Y, (p (pr1 x)) ∧ (q (pr2 x))). + + Infix "p × q" := (preddirprod p q) (at level 25). + + Definition predcoprod {X Y : UU} (p : X → hProp) (q : Y → hProp) : (X ⨿ Y) → hProp. + Proof. + intros x. + induction x. + - exact (p a). + - exact (q b). + Defined. + + Definition truepred (X : UU) : X → hProp := (λ _ , htrue). + + Definition falsepred (X : UU) : X → hProp := (λ _, hfalse). + +End Operations. diff --git a/code/_CoqProject b/code/_CoqProject index 7b30385..9f7f55c 100644 --- a/code/_CoqProject +++ b/code/_CoqProject @@ -2,17 +2,22 @@ COQC = coqc COQDEP = coqdep -R . "sem" - --arg "-w -notation-overridden -type-in-type -noinit" +-arg "-w -notation-overridden -type-in-type" init/imports.v init/all.v +util/range_equiv.v +util/NaturalEmbedding.v +Inductive/Predicates.v Inductive/ListProperties.v Inductive/Option.v Decidability/DecidablePredicates.v Decidability/DiscreteTypes.v +Enumerability/EnumerablePredicates.v +Enumerability/EnumerableTypes.v + Reducibility/ManyOneReductions.v diff --git a/code/init/imports.v b/code/init/imports.v index 4e28d4e..294dad3 100644 --- a/code/init/imports.v +++ b/code/init/imports.v @@ -1 +1,4 @@ Require Export UniMath.Foundations.All. +Require Export UniMath.Combinatorics.Lists. +Require Export UniMath.Combinatorics.KFiniteTypes. +Require Export UniMath.Combinatorics.FiniteSets. \ No newline at end of file diff --git a/code/util/NaturalEmbedding.v b/code/util/NaturalEmbedding.v new file mode 100644 index 0000000..593c65b --- /dev/null +++ b/code/util/NaturalEmbedding.v @@ -0,0 +1,94 @@ +Require Import init.imports. + +(* + +This file contains the definition of embedding functions, which form a bijective mapping from nat × nat to nat, together with its inverse unembed. + +Together with the two definitions, there also are proofs that the functions are inverses of each other. + +The embedding is done using diagonalization. + +0/0 0/1 0/2 0/3 0/4 0/5 +1/0 1/1 1/2 1/3 1/4 1/5 +2/0 2/1 2/2 2/3 2/4 2/5 +3/0 3/1 3/2 3/3 3/4 3/5 +4/0 4/1 4/2 4/3 4/4 4/5 +5/0 5/1 5/2 5/3 5/4 5/5 +6/0 6/1 6/2 6/3 6/4 6/5 +*) + +Section EmbedNaturals. + + (* Bijective maps from pairs of natural numbers to natural numbers.*) + + Definition gauss_sum (n : nat) : nat := (nat_rec _ 0 (λ (m s : nat), (S m) + s) (n)). + + Definition embed (p : nat×nat) : nat := (pr2 p) + (gauss_sum ((pr2 p) + (pr1 p))). + + Definition unembed (n : nat) : nat × nat := + nat_rec _ (0,, 0) (λ _ a, match (pr1 a) with S x => (x,, S (pr2 a)) | _ => (S (pr2 a),, 0) end) n. + + Section Tests. + Fact embed00 : (embed (0,, 0)) = 0. apply idpath. Defined. + Fact embed01 : (embed (0,, 1)) = 2. apply idpath. Defined. + Fact embed33 : (embed (3,, 3)) = 24. apply idpath. Defined. + + Fact unembed0 : (unembed 0) = (0,, 0). apply idpath. Defined. + Fact unembed2 : (unembed 2) = (0,, 1). apply idpath. Defined. + Fact unembed24 : (unembed 24) = (3,, 3). apply idpath. Defined. + End Tests. + + (*Proofs that embed and unembed are inverses of each other. *) + + Lemma embedinv (n : nat) : (embed (unembed n)) = n. + Proof. + induction n as [|n IH]. reflexivity. + simpl. revert IH. destruct (unembed n) as [x y]. + case x as [|x]; intro Hx; rewrite <- Hx; unfold embed; simpl. + - rewrite natplusr0. apply idpath. + - rewrite natpluscomm, (natpluscomm y (S x)). + simpl. rewrite (natpluscomm y (S (x + y + gauss_sum (x + y)))). apply maponpaths. simpl. apply maponpaths. rewrite (natpluscomm x y). apply idpath. + Qed. + + Lemma embed0x (x y : nat) : (embed (S x,, 0) = S (embed (0,, x))). + Proof. + unfold embed; simpl; rewrite natplusr0. apply idpath. + Qed. + + Lemma embedsxy (x y : nat) : (embed (x,, S y) = S (embed (S x,, y))). + Proof. + unfold embed; simpl. + rewrite natplusnsm, (natplusnsm y x); simpl. + rewrite natplusnsm. apply idpath. + Qed. + + Lemma unembedinv (mn : nat × nat) : (unembed (embed mn)) = mn. + Proof. + assert (∏ (n : nat), embed mn = n → unembed n = mn). + - intro n. revert mn. induction n as [|n IH]. + + intros [[|?][|?]]; intro H; inversion H; apply idpath. + + intros [x [|y]]; simpl. + * case x as [| x]; simpl; intro H. + inversion H. + rewrite (IH (0,, x)); [reflexivity |]. + revert H. rewrite embed0x. intros H; apply invmaponpathsS. apply H. exact x. + * intro H. rewrite (IH (S x,, y)); [reflexivity| ]. + apply invmaponpathsS. rewrite <- embedsxy. exact H. + - apply X. apply idpath. + Qed. + +End EmbedNaturals. + +Lemma nat_ind_geq_n (n : nat) (P : nat → UU) : (P n) → (∏ (k : nat), (P (n + k) → (P (S (n + k))))) → (∏ (m : nat), (n ≤ m) → (P (m))). +Proof. + intros. + assert (∑ (k : nat), n + k = m). + - use tpair. + + exact (m - n). + + cbn beta. rewrite -> (natpluscomm n (m - n)). exact (minusplusnmm m n X1). + - destruct X2 as [k eq]. + induction eq. + induction k. + + rewrite -> (natpluscomm n 0); simpl. exact X. + + rewrite -> (natplusnsm n k); simpl. apply (X0 k), (IHk (natlehnplusnm _ _)). + Defined. \ No newline at end of file diff --git a/code/util/range_equiv.v b/code/util/range_equiv.v new file mode 100644 index 0000000..d835a89 --- /dev/null +++ b/code/util/range_equiv.v @@ -0,0 +1,5 @@ +Require Import init.imports. + +Definition rangeequiv {X : UU} {Y : UU} (f g : X → Y) := ∏ (y : Y), ∥hfiber f y∥ <-> ∥hfiber g y∥. + +Notation "f ≡ᵣ g" := (rangeequiv f g) (at level 50).