(* * Infinite Data Types *)
From SyntheticComputability Require Import Shared.prelim Synthetic.ListEnumerabilityFacts Synthetic.EnumerabilityFacts Shared.ListAutomation.
Require Import Lia.
Set Implicit Arguments.
Unset Strict Implicit.
(* ** Definition of infinite and generating types *)
Definition generating X p :=
forall (A : list X), exists x, ~ In x A /\ p x.
Definition injective X Y (f : X -> Y) :=
forall x x', f x = f x' -> x = x'.
Definition infinite {X} (p : X -> Prop) :=
exists (f : nat -> X), injective f /\ forall n, p (f n).
Section Inf.
Variables (X : Type) (f' : nat -> option X).
Variable p : X -> Prop.
Hypothesis Hf' : forall x, p x <-> exists n, f' n = Some x.
Hypothesis HX : eq_dec X.
(* ** Infinite data types are generating *)
Section Gen.
Variable f : nat -> X.
Hypothesis Hf : injective f.
Hypothesis Hfp : forall n, p (f n).
Fixpoint LX n :=
match n with
| 0 => [f 0]
| S n => f (S n) :: LX n
end.
Lemma LX_len n :
length (LX n) = S n.
Proof.
induction n; cbn; eauto.
Qed.
Lemma LX_el n x :
x el LX n -> exists n', n' <= n /\ f n' = x.
Proof.
induction n.
- intros [H|[] ]. exists 0. split; auto.
- intros [H|H]; eauto.
destruct (IHn H) as [n'[H1 H2] ].
exists n'. split; auto.
Qed.
Lemma LX_NoDup n :
NoDup (LX n).
Proof.
induction n; cbn; repeat constructor; auto.
intros (n'&H1&H2) % LX_el.
apply Hf in H2. lia.
Qed.
Lemma sub_dec (A B : list X) :
(List.incl A B) + {x | x el A /\ ~ x el B}.
Proof.
revert B. induction A; intros B; cbn; auto.
- left. intros ? [].
- destruct (IHA B); decide (a el B); eauto.
+ left. intros ? [-> | ]; eauto.
+ destruct s as (x & Hx1 & Hx2). eauto.
Qed.
Lemma LX_p n x :
x el LX n -> p x.
Proof.
intros (n' & _ & H) % LX_el.
subst. eapply Hfp.
Qed.
Lemma X_gen :
generating p.
Proof.
intros A. destruct (sub_dec (LX (length A)) A) as [H|H].
- apply NoDup_incl_length in H; try apply LX_NoDup.
rewrite LX_len in H. lia.
- destruct H as [x [? H] ]. exists x. split. eauto.
eapply LX_p. eauto.
Qed.
End Gen.
(* ** Generating data types are infinite *)
Hypothesis Hg : generating p.
Instance el_dec :
forall (A : list X) x, dec (x el A).
Proof.
intros A x. induction A; cbn; auto.
Qed.
From Coq.Logic Require Import ConstructiveEpsilon.
Definition dummy : {x : X | p x}.
Proof.
pose (q := fun n => exists x, f' n = Some x).
destruct (constructive_indefinite_ground_description_nat q) as [n Hn].
- intros n. destruct (f' n) eqn : H.
+ left. now exists x.
+ right. intros [x H']. congruence.
- destruct (Hg nil) as (x & Hx1 & Hx2). eapply Hf' in Hx2 as [n Hn]. now exists n, x.
- destruct (f' n) eqn : H.
+ exists x. eapply Hf'. eauto.
+ exfalso. destruct Hn as [x Hx]. congruence.
Qed.
Definition f n :=
match (f' n) with Some x => x | None => proj1_sig dummy end.
Lemma f_sur :
forall x, p x -> exists n, f n = x.
Proof.
intros x H. eapply Hf' in H as [n Hn]. exists n.
unfold f. now rewrite Hn.
Qed.
Definition le_f x y :=
exists n, f n = x /\ forall n', f n' = y -> n <= n'.
Lemma gen (A : list X) :
{ x | ~ x el A /\ (forall y, ~ y el A -> le_f x y) /\ p x}.
Proof.
pose (q := fun n => ~ f n el A).
assert (H1 : forall x, dec (q x)).
{ intros n. destruct (el_dec A (f n)) as [H|H].
- right. intros H'. contradiction.
- left. assumption. }
assert (H2 : exists x, q x).
{ destruct (Hg A) as (x & Hx1 & Hx2). destruct (f_sur Hx2) as [n <-]. now exists n. }
exists (f (proj1_sig (mu_nat_p _ H1 H2))). split; try apply proj2_sig. split.
- intros y Hy. exists (proj1_sig (mu_nat_p _ H1 H2)). split; trivial.
intros n <-. eapply mu_nat_p_least. eassumption.
- unfold f. destruct f' eqn:E.
+ eapply Hf'. eauto.
+ eapply proj2_sig.
Defined.
Definition gen' A :=
proj1_sig (gen A).
Lemma gen_spec A :
~ gen' A el A.
Proof.
unfold gen'. destruct (gen A); cbn. apply a.
Qed.
Lemma gen_le_f A :
forall x, ~ x el A -> le_f (gen' A) x.
Proof.
unfold gen'. destruct (gen A); cbn. apply a.
Qed.
Fixpoint LL n :=
match n with 0 => nil | S n => LL n ++ [gen' (LL n)] end.
Definition F n :=
gen' (LL n).
Lemma LL_cum :
cumulative LL.
Proof.
intros n. now exists [(F n)].
Qed.
Lemma F_nel n :
~ F n el LL n.
Proof.
apply gen_spec.
Qed.
Lemma F_el n :
F n el LL (S n).
Proof.
cbn. apply in_app_iff. right. left. reflexivity.
Qed.
Lemma F_lt n m :
n < m -> F n el LL m.
Proof.
intros H. apply (cum_ge' (n:=S n)).
- apply LL_cum.
- apply F_el.
- lia.
Qed.
Lemma F_inj' n m :
F n = F m -> ~ n < m.
Proof.
intros H1 H2 % F_lt. rewrite H1 in H2. apply (F_nel H2).
Qed.
Lemma F_inj :
injective F.
Proof.
intros n m Hnm. destruct (PeanoNat.Nat.lt_total n m) as [H|[H|H] ]; trivial.
- contradiction (F_inj' Hnm H).
- symmetry in Hnm. contradiction (F_inj' Hnm H).
Qed.
Lemma F_p :
forall n, p (F n).
Proof.
unfold F. unfold gen'. intros.
destruct gen as (? & ? & ? & ?); eassumption.
Qed.
(* ** Generating data types are in bijection to nat *)
Lemma lt_acc n :
Acc lt n.
Proof.
eapply Wf_nat.lt_wf.
Qed.
Lemma LL_f n :
f n el LL (S n).
Proof.
induction (lt_acc n) as [n _ IH].
decide _; try eassumption. exfalso.
assert (H : ~ f n el LL n).
{ intros H. apply n0. apply (cum_ge' LL_cum H). auto. }
apply gen_le_f in H as [n'[H1 H2] ].
specialize (H2 n eq_refl).
destruct (PeanoNat.Nat.lt_total n' n) as [H3|[->|H3] ].
- apply (gen_spec (A:=LL n)). rewrite <- H1.
now apply (cum_ge' LL_cum (IH n' H3)).
- apply n0. rewrite H1. apply in_app_iff; fold LL.
right. left. reflexivity.
- lia.
Qed.
Lemma LL_F x n :
x el LL n -> exists m, F m = x.
Proof.
induction n; cbn; auto.
- tauto.
- intros [H|[H|H]] % in_app_iff; auto.
now exists n. inv H.
Qed.
Lemma F_sur :
forall x, p x -> exists n, F n = x.
Proof.
intros x Hx. destruct (f_sur Hx) as [n H].
destruct (LL_F (LL_f n)) as [m H'].
exists m. congruence.
Qed.
(* Definition G x := *)
(* proj1_sig (mu_nat_p _ (F_sur x)). *)
(* Lemma FG n : *)
(* F (G n) = n. *)
(* Proof. *)
(* unfold G. apply proj2_sig. *)
(* Qed. *)
(* Lemma GF n : *)
(* G (F n) = n. *)
(* Proof. *)
(* apply F_inj. now rewrite FG. *)
(* Qed. *)
End Inf.
From SyntheticComputability Require Import Shared.prelim Synthetic.ListEnumerabilityFacts Synthetic.EnumerabilityFacts Shared.ListAutomation.
Require Import Lia.
Set Implicit Arguments.
Unset Strict Implicit.
(* ** Definition of infinite and generating types *)
Definition generating X p :=
forall (A : list X), exists x, ~ In x A /\ p x.
Definition injective X Y (f : X -> Y) :=
forall x x', f x = f x' -> x = x'.
Definition infinite {X} (p : X -> Prop) :=
exists (f : nat -> X), injective f /\ forall n, p (f n).
Section Inf.
Variables (X : Type) (f' : nat -> option X).
Variable p : X -> Prop.
Hypothesis Hf' : forall x, p x <-> exists n, f' n = Some x.
Hypothesis HX : eq_dec X.
(* ** Infinite data types are generating *)
Section Gen.
Variable f : nat -> X.
Hypothesis Hf : injective f.
Hypothesis Hfp : forall n, p (f n).
Fixpoint LX n :=
match n with
| 0 => [f 0]
| S n => f (S n) :: LX n
end.
Lemma LX_len n :
length (LX n) = S n.
Proof.
induction n; cbn; eauto.
Qed.
Lemma LX_el n x :
x el LX n -> exists n', n' <= n /\ f n' = x.
Proof.
induction n.
- intros [H|[] ]. exists 0. split; auto.
- intros [H|H]; eauto.
destruct (IHn H) as [n'[H1 H2] ].
exists n'. split; auto.
Qed.
Lemma LX_NoDup n :
NoDup (LX n).
Proof.
induction n; cbn; repeat constructor; auto.
intros (n'&H1&H2) % LX_el.
apply Hf in H2. lia.
Qed.
Lemma sub_dec (A B : list X) :
(List.incl A B) + {x | x el A /\ ~ x el B}.
Proof.
revert B. induction A; intros B; cbn; auto.
- left. intros ? [].
- destruct (IHA B); decide (a el B); eauto.
+ left. intros ? [-> | ]; eauto.
+ destruct s as (x & Hx1 & Hx2). eauto.
Qed.
Lemma LX_p n x :
x el LX n -> p x.
Proof.
intros (n' & _ & H) % LX_el.
subst. eapply Hfp.
Qed.
Lemma X_gen :
generating p.
Proof.
intros A. destruct (sub_dec (LX (length A)) A) as [H|H].
- apply NoDup_incl_length in H; try apply LX_NoDup.
rewrite LX_len in H. lia.
- destruct H as [x [? H] ]. exists x. split. eauto.
eapply LX_p. eauto.
Qed.
End Gen.
(* ** Generating data types are infinite *)
Hypothesis Hg : generating p.
Instance el_dec :
forall (A : list X) x, dec (x el A).
Proof.
intros A x. induction A; cbn; auto.
Qed.
From Coq.Logic Require Import ConstructiveEpsilon.
Definition dummy : {x : X | p x}.
Proof.
pose (q := fun n => exists x, f' n = Some x).
destruct (constructive_indefinite_ground_description_nat q) as [n Hn].
- intros n. destruct (f' n) eqn : H.
+ left. now exists x.
+ right. intros [x H']. congruence.
- destruct (Hg nil) as (x & Hx1 & Hx2). eapply Hf' in Hx2 as [n Hn]. now exists n, x.
- destruct (f' n) eqn : H.
+ exists x. eapply Hf'. eauto.
+ exfalso. destruct Hn as [x Hx]. congruence.
Qed.
Definition f n :=
match (f' n) with Some x => x | None => proj1_sig dummy end.
Lemma f_sur :
forall x, p x -> exists n, f n = x.
Proof.
intros x H. eapply Hf' in H as [n Hn]. exists n.
unfold f. now rewrite Hn.
Qed.
Definition le_f x y :=
exists n, f n = x /\ forall n', f n' = y -> n <= n'.
Lemma gen (A : list X) :
{ x | ~ x el A /\ (forall y, ~ y el A -> le_f x y) /\ p x}.
Proof.
pose (q := fun n => ~ f n el A).
assert (H1 : forall x, dec (q x)).
{ intros n. destruct (el_dec A (f n)) as [H|H].
- right. intros H'. contradiction.
- left. assumption. }
assert (H2 : exists x, q x).
{ destruct (Hg A) as (x & Hx1 & Hx2). destruct (f_sur Hx2) as [n <-]. now exists n. }
exists (f (proj1_sig (mu_nat_p _ H1 H2))). split; try apply proj2_sig. split.
- intros y Hy. exists (proj1_sig (mu_nat_p _ H1 H2)). split; trivial.
intros n <-. eapply mu_nat_p_least. eassumption.
- unfold f. destruct f' eqn:E.
+ eapply Hf'. eauto.
+ eapply proj2_sig.
Defined.
Definition gen' A :=
proj1_sig (gen A).
Lemma gen_spec A :
~ gen' A el A.
Proof.
unfold gen'. destruct (gen A); cbn. apply a.
Qed.
Lemma gen_le_f A :
forall x, ~ x el A -> le_f (gen' A) x.
Proof.
unfold gen'. destruct (gen A); cbn. apply a.
Qed.
Fixpoint LL n :=
match n with 0 => nil | S n => LL n ++ [gen' (LL n)] end.
Definition F n :=
gen' (LL n).
Lemma LL_cum :
cumulative LL.
Proof.
intros n. now exists [(F n)].
Qed.
Lemma F_nel n :
~ F n el LL n.
Proof.
apply gen_spec.
Qed.
Lemma F_el n :
F n el LL (S n).
Proof.
cbn. apply in_app_iff. right. left. reflexivity.
Qed.
Lemma F_lt n m :
n < m -> F n el LL m.
Proof.
intros H. apply (cum_ge' (n:=S n)).
- apply LL_cum.
- apply F_el.
- lia.
Qed.
Lemma F_inj' n m :
F n = F m -> ~ n < m.
Proof.
intros H1 H2 % F_lt. rewrite H1 in H2. apply (F_nel H2).
Qed.
Lemma F_inj :
injective F.
Proof.
intros n m Hnm. destruct (PeanoNat.Nat.lt_total n m) as [H|[H|H] ]; trivial.
- contradiction (F_inj' Hnm H).
- symmetry in Hnm. contradiction (F_inj' Hnm H).
Qed.
Lemma F_p :
forall n, p (F n).
Proof.
unfold F. unfold gen'. intros.
destruct gen as (? & ? & ? & ?); eassumption.
Qed.
(* ** Generating data types are in bijection to nat *)
Lemma lt_acc n :
Acc lt n.
Proof.
eapply Wf_nat.lt_wf.
Qed.
Lemma LL_f n :
f n el LL (S n).
Proof.
induction (lt_acc n) as [n _ IH].
decide _; try eassumption. exfalso.
assert (H : ~ f n el LL n).
{ intros H. apply n0. apply (cum_ge' LL_cum H). auto. }
apply gen_le_f in H as [n'[H1 H2] ].
specialize (H2 n eq_refl).
destruct (PeanoNat.Nat.lt_total n' n) as [H3|[->|H3] ].
- apply (gen_spec (A:=LL n)). rewrite <- H1.
now apply (cum_ge' LL_cum (IH n' H3)).
- apply n0. rewrite H1. apply in_app_iff; fold LL.
right. left. reflexivity.
- lia.
Qed.
Lemma LL_F x n :
x el LL n -> exists m, F m = x.
Proof.
induction n; cbn; auto.
- tauto.
- intros [H|[H|H]] % in_app_iff; auto.
now exists n. inv H.
Qed.
Lemma F_sur :
forall x, p x -> exists n, F n = x.
Proof.
intros x Hx. destruct (f_sur Hx) as [n H].
destruct (LL_F (LL_f n)) as [m H'].
exists m. congruence.
Qed.
(* Definition G x := *)
(* proj1_sig (mu_nat_p _ (F_sur x)). *)
(* Lemma FG n : *)
(* F (G n) = n. *)
(* Proof. *)
(* unfold G. apply proj2_sig. *)
(* Qed. *)
(* Lemma GF n : *)
(* G (F n) = n. *)
(* Proof. *)
(* apply F_inj. now rewrite FG. *)
(* Qed. *)
End Inf.