(** * A proof of Open Induction on Cantor space assuming delimited control operators (Some lemmas, obviously true, involving the initial segment relation still have to be proved, but the main argument is fully formalized.) Danko Ilik, 18th February, 2013 *) Require Import List. Require Import Max. Require Import Plus. Require Import Le. (** For working with lists we use 'firstn', for initial segments, and 'nth', for n-th element of a list. These operations start counting from the top of the list. *) Definition append1 (p : list bool)(a : bool) := p ++ (a :: nil). Fixpoint overline (n:nat)(alpha : nat->bool) : list bool := match n with | O => nil | S m => append1 (overline m alpha) (alpha m) end. Print firstn. Open Scope type_scope. Definition lessthan (beta alpha : nat->bool) : Set := {n:nat | (overline n beta = overline n alpha) /\ ((beta n = false) /\ (alpha n = true))}. Definition membership (pi:nat->(list bool)) : (nat->bool) -> Set := fun alpha => {l:nat & {m:nat | overline l alpha = pi m}}. Definition membership_list (pi:nat->(list bool)) : list bool -> Set := fun p => {l:nat & {m:nat | firstn l p = pi m}}. Lemma firstn_firstn : forall (A:Set)(l:list A)(n1 n2:nat), firstn n1 (firstn n2 l) = firstn (min n1 n2) l. Proof. induction l. + intros. destruct n1; destruct n2; reflexivity. + intros. destruct n1. * simpl. reflexivity. * destruct n2. simpl. reflexivity. simpl. rewrite IHl. reflexivity. Qed. Lemma app_firstn : forall (A:Set)(l1 l2:list A)(n1 n2:nat), length l1 = n1 -> (l1 ++ firstn n2 l2) = firstn (n1+n2) (l1++l2). Proof. induction l1. + simpl. intros l2 n1 n2 Heq. rewrite <- Heq. simpl. reflexivity. + simpl. intros l2 n1 n2 Heq. rewrite <- Heq. simpl. rewrite IHl1 with (n1:=length l1). reflexivity. reflexivity. Qed. (** The next four lemmas are temporary, with purpose to show firstn_overline *) Lemma overline_S : forall n beta default, overline (S n) beta = hd default (overline (S n) beta) :: tl (overline (S n) beta). Admitted. Lemma firstn_tl : forall (A:Set)(k:nat)(l:list A), firstn k l = l -> firstn k (tl l) = tl l. Admitted. Lemma hd_overline : forall n k beta default, hd default (overline (S n) beta) = hd default (overline (S k) beta). Admitted. Lemma firstn_overline : forall k n beta, (firstn k (overline n beta) = overline n beta) + (firstn k (overline n beta) = overline k beta). Proof. intros. induction k. simpl. right;reflexivity. destruct n. simpl. left;reflexivity. rewrite overline_S with (default:=false)(n:=n). rewrite overline_S with (default:=false)(n:=k). set (l1 := (overline (S n) beta)) in *. set (l2 := (overline (S k) beta)) in *. simpl firstn. destruct IHk as [IH1 | IH2]. left. rewrite firstn_tl. reflexivity. assumption. right. unfold l1 in IH2. unfold l1 at 1. unfold l2 at 1. rewrite (hd_overline n k). assert (firstn k (tl l1) = tl l2). { unfold l2. simpl overline. rewrite <- IH2. fold l1. destruct k. simpl. reflexivity. replace (tl (append1 (firstn (S k) l1) (beta (S k)))) with (append1 (tl (firstn (S k) l1)) (beta (S k))). simpl. unfold l1. simpl. Admitted. Lemma firstn_overline_same : forall k beta, (firstn k (overline k beta) = overline k beta). Proof. induction k. - reflexivity. - intros. simpl overline. rewrite <- IHk at 2. Admitted. Lemma length_overline : forall n alpha, length (overline n alpha) = n. Proof. induction n. simpl. auto. simpl. unfold append1. intros. rewrite app_length. simpl. rewrite IHn. rewrite plus_comm. simpl. reflexivity. Qed. Lemma length_0 : forall (A:Set)(l:list A), length l = 0 -> l = nil. Proof. intros. destruct l. reflexivity. simpl in H. congruence. Qed. Lemma length_S : forall (A:Set)(l:list A)(n:nat)(default:A), length l = S n -> l = (hd default l :: nil) ++ (tl l). Proof. induction l. - simpl. intros. congruence. - simpl. reflexivity. Qed. Lemma length_tl : forall (A:Set)(l:list A)(n:nat), length l = S n -> length (tl l) = n. Proof. destruct l. simpl. intros. congruence. simpl. intros n H. congruence. Qed. Lemma length_first_le : forall (A:Set)(p:list A)(k1 k2:nat), length p = k2 -> k1 <= k2 -> length (firstn k1 p) = k1. Proof. induction p. simpl. destruct k1. reflexivity. simpl. intros k2 eq_1 eq_2. rewrite <- eq_1 in eq_2. apply le_Sn_0 in eq_2. contradict eq_2. simpl. intros k1 k2 eq_1 eq_2. destruct k1. reflexivity. simpl. destruct k2. apply le_Sn_0 in eq_2. contradict eq_2. rewrite IHp with (k2:=k2). reflexivity. congruence. apply le_S_n. assumption. Qed. Lemma length_skipn : forall (A:Set)(l:list A)(n k:nat), length l = (n+k)%nat -> length (skipn n l) = k. Proof. induction l. simpl. intros n k Heq. destruct n; destruct k; auto. simpl. simpl in Heq. congruence. intros n k Heq. simpl in Heq. simpl. destruct n; destruct k; auto. simpl. apply IHl. simpl in Heq. congruence. simpl in Heq. simpl. apply IHl. congruence. Qed. Lemma lemma_1 : forall k n beta, length (firstn k (skipn (S n) (overline (S n + k) beta))) = k. Proof. intro k. destruct k. - simpl. reflexivity. - intros. assert (forall (A:Set)(l:list A)(m:nat), m = length l -> length (firstn m l) = m). intros A l m Heq. apply length_first_le with m. auto. auto. rewrite H. reflexivity. rewrite length_skipn with (k:=S k). reflexivity. apply length_overline. Qed. Open Scope nat_scope. Lemma lemma_2 : forall k n beta, overline (S n) beta ++ firstn k (skipn (S n) (overline (S n + k) beta)) = overline (S n + k) beta. Proof. induction k; intros. - simpl. rewrite plus_comm. simpl. rewrite app_nil_r. reflexivity. - assert ((overline (S n + S k) beta) = ((overline (S n + k) beta) ++ (beta (S n + k) :: nil))). admit. rewrite H at 2. rewrite <- IHk. assert (firstn (S k) (skipn (S n) (overline (S n + S k) beta)) = (firstn k (skipn (S n) (overline (S n + k) beta))) ++ beta (S n + k) :: nil). admit. rewrite H0. rewrite app_assoc. reflexivity. Qed. Section OpenInduction. (** The open set [U] is given by an enumeration [pi] of basic open sets *) Variable pi : nat -> (list bool). Definition U : (nat -> bool) -> Set := fun alpha => membership pi alpha. (** Membership in [U] is equvalently stated for finite sequences using [B] *) Definition B : (list bool) -> Set := fun p => {k:nat & forall q, length q = k -> membership_list pi (p++q)}. (** Axioms to be realized by delimited control in extracted code *) Axiom reset : B nil -> B nil. Axiom decide_by_shift : forall x : list bool, B x + (B x -> B nil). (** The characteristic function [chi] of [B] built using [decide_by_shift] *) Definition chi : (list bool) -> bool := fun x => match decide_by_shift x with inl _ => true | inr _ => false end. Lemma chi_property : forall x, (chi x = true -> B x) * (chi x = false -> B x -> B nil). Proof. intro x. unfold chi. destruct decide_by_shift. split. intro Heq. assumption. intro Heq. congruence. split. intro Heq. congruence. intro Heq. assumption. Defined. (** Using [chi] we build the infinite sequence [alpha] with the help of [alpha_list] *) Fixpoint alpha_list (n:nat) {struct n} : list bool := match n with O => nil | S m => append1 (alpha_list m) (match chi (append1 (alpha_list m) false) with true => match chi (append1 (alpha_list m) true) with true => false | false => true end | false => false end) end. Definition alpha : nat -> bool := fun n => nth n (alpha_list (S n)) false. Lemma nth_append' : forall l1 n b1, length l1 = n -> (nth n (append1 l1 b1) false) = b1. Proof. induction l1. + intros n b1 Hlen. simpl in Hlen. rewrite <- Hlen. simpl. reflexivity. + intros n b1 Hlen. simpl in Hlen. rewrite <- Hlen. simpl. destruct n. congruence. assert (Hlen' : length l1 = n). congruence. rewrite <- IHl1 with (n:=n). unfold append1. rewrite <- Hlen'. reflexivity. assumption. Qed. Lemma length_append1 : forall l n b, length l = n -> length (append1 l b) = S n. Proof. induction l. simpl. congruence. simpl. intros. destruct n. congruence. unfold append1 in IHl. rewrite IHl with (n:=n). reflexivity. congruence. Qed. Lemma length_alpha_list : forall n, length (alpha_list n) = n. Proof. induction n. simpl. reflexivity. simpl. apply length_append1. assumption. Qed. Lemma nth_append : forall n b1, (nth n (append1 (alpha_list n) b1) false) = b1. Proof. intros. apply nth_append'. apply length_alpha_list. Qed. Lemma overline_alpha : forall n, overline n alpha = alpha_list n. Proof. induction n. simpl. reflexivity. simpl. rewrite IHn. unfold alpha. simpl. rewrite nth_append. reflexivity. Qed. (** Key lemmas *) Lemma a_3 : forall n, (B (overline n alpha) -> B nil) -> B (overline (S n) alpha) -> B nil. Proof. intros n Hn HSn. destruct (chi_property (overline (S n) alpha)) as [chi_true chi_false]. remember (chi (overline (S n) alpha)) as chi_case. destruct chi_case. (* case chi_true *) apply Hn. clear - Heqchi_case. assert (alpha_n_false : chi (append1 (overline n alpha) false) = true). simpl in *. rewrite overline_alpha in *. unfold alpha in *. simpl in *. rewrite nth_append in *. remember (chi (append1 (alpha_list n) false)) as b. destruct b. reflexivity. rewrite <- Heqchi_case in Heqb. assumption. assert (alpha_n_true : chi (append1 (overline n alpha) true) = true). simpl in *. rewrite overline_alpha in *. unfold alpha in *. simpl in *. rewrite nth_append in *. remember (chi (append1 (alpha_list n) false)) as b0. remember (chi (append1 (alpha_list n) true)) as b1. destruct b0; destruct b1. reflexivity. rewrite <- Heqchi_case in Heqb1. assumption. reflexivity. assumption. apply chi_property in alpha_n_false. apply chi_property in alpha_n_true. unfold append1 in alpha_n_false, alpha_n_true. destruct alpha_n_false as [k0 H0]. destruct alpha_n_true as [k1 H1]. (* exists (S k). *) exists (S (max k0 k1)). intros q q_length. assert (q_decomposed : q = (hd false q :: nil) ++ (tl q)). apply length_S with (max k0 k1). assumption. rewrite q_decomposed. remember (hd false q) as q_hd. destruct q_hd. rewrite app_assoc. unfold membership_list in H1 |- *. assert (k1_len : length (firstn k1 (tl q)) = k1). apply length_first_le with (k2 := max k0 k1). apply length_tl. assumption. apply le_max_r. destruct (H1 (firstn k1 (tl q)) k1_len) as [l1 [m1 H1']]. exists (min l1 ((n+1)+k1)). exists m1. rewrite app_firstn with (n1:=(n+1)%nat) in H1' . rewrite firstn_firstn in H1'. exact H1'. rewrite app_length. rewrite length_overline. simpl. reflexivity. rewrite app_assoc. unfold membership_list in H0 |- *. assert (k0_len : length (firstn k0 (tl q)) = k0). apply length_first_le with (k2 := max k0 k1). apply length_tl. assumption. apply le_max_l. destruct (H0 (firstn k0 (tl q)) k0_len) as [l0 [m0 H0']]. exists (min l0 ((n+1)+k0)). exists m0. rewrite app_firstn with (n1:=(n+1)%nat) in H0' . rewrite firstn_firstn in H0'. exact H0'. rewrite app_length. rewrite length_overline. simpl. reflexivity. (* case chi_false *) apply chi_false. reflexivity. apply HSn. Defined. Theorem open_induction : (forall alpha : nat->bool, (forall beta : nat->bool, lessthan beta alpha -> U beta) -> U alpha) -> forall alpha' : nat->bool, U alpha'. Proof. intros U_progressive alpha'. assert (H : B nil). apply reset. destruct (U_progressive alpha) as [l c]. intros beta h'. destruct h' as [n h'']. destruct h'' as [h''1 [h''21 h''22]]. assert (a_1 : B (overline (S n) beta)). apply chi_property. simpl. rewrite h''1. rewrite h''21. rewrite overline_alpha. clear -h''22. unfold alpha in h''22. simpl in *. rewrite nth_append in h''22. destruct (chi (append1 (alpha_list n) false)). reflexivity. assumption. destruct a_1 as [k h''']. unfold membership_list in h'''. unfold U. unfold membership. set (q := firstn k (skipn (S n) (overline (S n + k) beta))). assert (q_len : length q = k). apply lemma_1. destruct (h''' q q_len) as [l [m h4]]. assert (h5 : (overline (S n) beta ++ q) = overline (S n + k) beta). unfold q. apply lemma_2. rewrite h5 in h4. assert (h_f_o := firstn_overline l (S n + k) beta). rewrite h4 in h_f_o. destruct h_f_o as [h_f_o | h_f_o]. exists ((S n) + k)%nat. exists m. symmetry. assumption. exists l. exists m. symmetry. assumption. assert (a_I : forall n, B (overline n alpha) -> B nil). intros n Hn. induction n. simpl in Hn. exact Hn. apply (a_3 n). assumption. assumption. apply (a_I l). exists 0. intros q lenq. apply length_0 in lenq. rewrite lenq. rewrite app_nil_r. exists l. rewrite firstn_overline_same. exact c. destruct H as [k' h5]. assert (h5' := h5 (overline k' alpha') (length_overline k' alpha')). rewrite app_nil_l in h5'. destruct h5' as [l h5'']. assert (h_f_o := firstn_overline l k' alpha'). destruct h_f_o as [h_f_o | h_f_o]. rewrite h_f_o in h5''. exists k'. exact h5''. rewrite h_f_o in h5''. exists l. exact h5''. Defined. End OpenInduction. Print open_induction. Recursive Extraction open_induction. Extraction "oi_delcont" open_induction. Extraction Language Scheme. Extraction "oi_delcont" open_induction. Extraction Language Haskell. Extraction "oi_delcont" open_induction.