Set Implicit Arguments. Require Export List. Require Import Omega. Require Export ZArith. Require Import Max. Require Export Ltree. Open Scope positive_scope. (* building an infinite tree containing exactly one occurrence of each positive naturel number *) CoFixpoint PosTree (p:positive) : LTree positive := LBin p (PosTree (xO p)) (PosTree (xI p)). (* examples of computation *) Eval compute in (LTree_label (PosTree 1) (d0 :: d1 :: nil)). Eval compute in (LTree_label (PosTree 1) (d0 :: d1 :: d1 :: nil)). Eval compute in (LTree_label (PosTree 1) (d0 :: d1 :: d1 :: d0 :: d0 ::d1 :: nil)). (***********************************************************************) (***** Correctness proof ********) (* unfold lemma *) Lemma PosTree_unfold : forall p:positive, PosTree p = LBin p (PosTree (xO p)) (PosTree (xI p)). Proof. intros p; LTree_unfold (PosTree p). trivial. Qed. (* some technical lemmas *) Lemma short : forall (A:Set)(a:A) l l', (length l < length (l ++ (a::l')))%nat. Proof. induction l;simpl; auto with arith. Qed. (* The following lemmas express some simple properties of positive numbers *) Lemma xO_lt : forall p, p < xO p. Proof. unfold Plt. intro;apply nat_of_P_lt_Lt_compare_complement_morphism. rewrite nat_of_P_xO. generalize (lt_O_nat_of_P p). intros;omega. Qed. Lemma xI_lt : forall p, p < xI p. Proof. unfold Plt. intro;apply nat_of_P_lt_Lt_compare_complement_morphism. rewrite nat_of_P_xI. intros;omega. Qed. Lemma lt_le : forall p q, p< q -> p <= q. Proof. unfold Plt,Ple in *. intros p q;case ((p ?= q) Eq);intros;try discriminate. Qed. Lemma le_refl: forall p, p <= p. Proof. unfold Ple. intro p; rewrite Pcompare_refl. discriminate. Qed. Lemma le_trans : forall n p q, n<=p -> p<= q -> n <= q. (* left as an exercise *) Admitted. Lemma lt_le_trans : forall n p q, n
p<= q -> n < q. (* left as an exercise *) Admitted. Lemma le_lt_trans : forall n p q, n<=p -> p< q -> n < q. (* left as an exercise *) Admitted. Lemma lt_irr : forall p, ~ p
xI p. Proof. induction p. red; intro H;injection H;auto. red; intro H. discriminate. discriminate. Qed. Lemma xO_diff : forall p, p <> xO p. Proof. induction p. red; intro H;discriminate. red;intro H;injection H;auto. discriminate. Qed. (* accessible p w n means that p is reachable from n by a sequence w of multiplications by two and fun i => 2i+1 w is an encoded by the type path *) Inductive accessible (p:positive) : path -> positive -> Prop := | accessible_1 : accessible p nil p | accessible_O : forall pa n , accessible p pa (xO n) -> accessible p (d0::pa) n | accessible_I : forall pa n , accessible p pa (xI n) -> accessible p (d1::pa) n. Lemma accessible_le : forall pa n p, accessible p pa n -> n <= p. Proof. induction 1. apply le_refl. apply le_trans with n~0;auto. apply lt_le. apply xO_lt. apply le_trans with n~1;auto. apply lt_le. apply xI_lt. Qed. Lemma accessible_eq : forall p pa n , accessible p pa n -> pa=nil -> n = p. Proof. induction 1. auto. intro;discriminate. intro;discriminate. Qed. Lemma accessible_inv_d0: forall p pa n, accessible p (d0::pa) n -> n < p. Proof. inversion_clear 1. apply lt_le_trans with n~0. apply xO_lt. eapply accessible_le. eauto. Qed. Lemma accessible_inv_d1: forall p pa n , accessible p (d1::pa) n -> n < p. Proof. inversion_clear 1. apply lt_le_trans with n~1. apply xI_lt. eapply accessible_le. eauto. Qed. Lemma accessible_d_inv : forall a pa n p, accessible p (a::pa) n -> n < p. Proof. destruct a;intros. eapply accessible_inv_d0;eauto. eapply accessible_inv_d1;eauto. Qed. Lemma acc_d0_tail : forall q pa p , accessible q pa p -> accessible (xO q) (pa++(d0::nil)) p . Proof. induction pa. simpl. inversion 1. constructor 2. constructor 1. intros. simpl. inversion H. constructor 2. apply IHpa. auto. constructor 3. apply IHpa. auto. Qed. Lemma acc_d1_tail : forall q pa p , accessible q pa p -> accessible (xI q) (pa++(d1::nil)) p . Proof. induction pa. simpl. inversion 1. constructor 3. constructor 1. intros. simpl. inversion H. constructor 2. apply IHpa. auto. constructor 3. apply IHpa. auto. Qed. (* all positive integers are accessible from 1 *) Lemma all_acc : forall p, exists pa, accessible p pa 1 . Proof. induction p. case IHp;intros pa Ha. exists (pa++(d1::nil)). apply acc_d1_tail;auto. case IHp;intros pa Ha. exists (pa++(d0::nil)). apply acc_d0_tail;auto. exists nil;constructor. Qed. (* every node in the tree rooted in p is accessible from p the witness for accessibility is the path leading to that node *) Lemma node_accessible : forall pa p q, LTree_label (PosTree p) pa = Some(node_label q) -> accessible q pa p. Proof. induction pa. intros p q;rewrite PosTree_unfold. simpl. rewrite LTree_label_rw_root_bin;trivial. injection 1. intro;subst p. constructor. intros p q;rewrite PosTree_unfold. simpl. case a. rewrite LTree_label_rw0 . intro;constructor 2;apply IHpa. auto. rewrite LTree_label_rw1 . intro;constructor 3;apply IHpa. auto. Qed. (* converse of node_accessible *) Lemma complete_enum_0 : forall pa p q, accessible q pa p -> LTree_label (PosTree p) pa = Some(node_label q). Proof. induction 1. rewrite PosTree_unfold. rewrite LTree_label_rw_root_bin;trivial. rewrite (PosTree_unfold n). rewrite LTree_label_rw0 . auto. rewrite (PosTree_unfold n). rewrite LTree_label_rw1 . auto. Qed. (******************************************) Theorem complete_enum : forall p:positive, exists pa, LTree_label (PosTree 1) pa = Some(node_label p). Proof. intro p;case (all_acc p). intros pa Ha;exists pa;apply complete_enum_0. trivial. Qed. (* Waouh ! we've shown that every positive occurs in our tree Now, let's look at unicity *) Lemma acc_path_cases : forall pa p n, accessible p pa n -> p = n /\ pa=nil \/ (exists p', (exists pa', accessible p' pa' n /\ (p=xO p' /\ pa=pa'++(d0::nil) \/ p=xI p' /\ pa=pa'++(d1::nil)))). Proof. induction 1. left;auto. case IHaccessible. right. exists n. exists nil. split. constructor. left. simpl;auto. decompose [and] H0. subst pa;simpl;auto. intros. case H0;intros. case H1;intros. case H2;intros. decompose [or and] H2. right. exists x. exists (d0::x0). rewrite H6. split. constructor 2;auto. left. split. auto. simpl;auto. rewrite H8. auto. right. exists x. exists (d0::x0). split. constructor 2;auto. rewrite H8. right. simpl. split. auto. auto. case IHaccessible. right. exists n. exists nil. split. constructor 1. right. simpl;auto. decompose [and] H0. subst pa;simpl;auto. intros. case H0;intros. case H1;intros. case H2;intros. decompose [or and] H4. right. exists x. exists (d1::x0). split. constructor 3;auto. rewrite H7. left. split. auto. simpl;auto. right. exists x. exists (d1::x0). rewrite H7. split. constructor;auto. right. simpl. split. auto. auto. Qed. Lemma acc_of_xO_inv : forall p pa n, accessible (xO p) pa n -> n=xO p /\ pa=nil \/ exists pa', accessible p pa' n /\ pa = pa'++(d0::nil). Proof. intros. case (acc_path_cases H). firstorder. destruct 1. right. case H0;intros. exists x0. case H1. intros. destruct H3. decompose [and] H3. injection H4. intros. subst x. split. auto. subst pa. auto. case H3;intros;discriminate. Qed. Lemma acc_of_xI_inv : forall p pa n, accessible (xI p) pa n -> n=xI p /\ pa=nil \/ exists pa', accessible p pa' n /\ pa = pa'++(d1::nil)%nat. Proof. intros. case (acc_path_cases H). firstorder. destruct 1. right. case H0;intros. exists x0. case H1. intros. destruct H3. case H3;intros;discriminate. decompose [and] H3. injection H4. intros. subst x. split. auto. subst pa. auto. Qed. Lemma path_inj_xI : forall p pa pb n, accessible (xI p) pa n -> accessible (xI p) pb n -> n=xI p /\ pa=nil /\ pb=nil \/ exists pa', exists pb', accessible p pa' n /\ accessible p pb' n /\ (pa = pa'++(d1::nil) /\ pb = pb'++(d1::nil)). Proof. intros. case (acc_of_xI_inv H); case (acc_of_xI_inv H0). left. firstorder. intros. decompose [and] H2. subst pa. inversion_clear H. case_eq pb. intro. subst pb. case H1;intros;simpl. simpl in H. case H;case x;intros. discriminate H5. simpl in H5; discriminate H5. intros. subst pb. subst n. case (@lt_irr p~1). eapply accessible_d_inv;eauto. intros. decompose [and] H1. subst pb. inversion_clear H0. case_eq pa. intro. left;auto. intros. subst pa. subst n. case (@lt_irr p~1). eapply accessible_d_inv;eauto. right. case H1. intros. case H2;intros. decompose [and] H3. decompose [and] H4. exists x0. exists x. tauto. Qed. Lemma path_inj_xO : forall p pa pb n, accessible (xO p) pa n -> accessible (xO p) pb n -> n=xO p /\ pa=nil /\ pb=nil \/ exists pa', exists pb', accessible p pa' n /\ accessible p pb' n /\ (pa = pa'++(d0::nil) /\ pb = pb'++(d0::nil)). Proof. intros. case (acc_of_xO_inv H); case (acc_of_xO_inv H0). left. firstorder. intros. decompose [and] H2. subst pa. inversion_clear H. case_eq pb. intro. subst pb. case H1;intros;simpl. simpl in H. case H;case x;intros. discriminate H5. simpl in H5; discriminate H5. intros. subst pb. subst n. case (@lt_irr p~0). eapply accessible_d_inv;eauto. intros. decompose [and] H1. subst pb. inversion_clear H0. case_eq pa. intro. left;auto. intros. subst pa. subst n. case (@lt_irr p~0). eapply accessible_d_inv;eauto. right. case H1. intros. case H2;intros. decompose [and] H3. decompose [and] H4. exists x0. exists x. tauto. Qed. Lemma acc_inj_bounded_length : forall l p pa pb n, (length pa <= l)%nat -> (length pb <= l)%nat -> accessible p pa n -> accessible p pb n -> pa=pb. Proof. induction l. intros. assert(pa = nil). generalize H;case pa;simpl. auto. inversion 1. subst pa. generalize H0;case pb. auto. intros. simpl in H3. inversion H3. intros. case_eq p. intros. subst p. case (path_inj_xI H1 H2). firstorder. subst pa;auto. destruct 1;intros. case H3;intros. decompose [and] H4;clear H4. subst pa pb. generalize (IHl p0 x x0 n). intros. rewrite H4;auto. generalize (short d1 x nil). intro. generalize (Lt.lt_le_trans _ _ _ H6 H). auto with arith. generalize (short d1 x0 nil). intro. generalize (Lt.lt_le_trans _ _ _ H6 H0). auto with arith. intros. subst p. case (path_inj_xO H1 H2). firstorder. subst pa;auto. destruct 1;intros. case H3;intros. decompose [and] H4;clear H4. subst pa pb. generalize (IHl p0 x x0 n). intros. rewrite H4;auto. generalize (short d0 x nil). intro. generalize (Lt.lt_le_trans _ _ _ H6 H). auto with arith. generalize (short d0 x0 nil). intro. generalize (Lt.lt_le_trans _ _ _ H6 H0). auto with arith. intro;subst p. case (acc_path_cases H1). destruct 1. subst pa. subst n. case (acc_path_cases H2). firstorder. intros. case H3;intros. case H4;intros. decompose [and] H5. case H7. destruct 1. discriminate. destruct 1. discriminate. destruct 1. case H3;intros. decompose [and or] H4. discriminate. discriminate. Qed. Lemma acc_inj : forall p pa n , accessible p pa n -> forall pa', accessible p pa' n -> pa = pa'. Proof. intros. eapply acc_inj_bounded_length with (l:=max (length pa) (length pa')). auto with arith. auto with arith. eauto. eauto. Qed. Theorem at_most_one_occurrence : forall pa pa' p, LTree_label (PosTree 1) pa = Some(node_label p) -> LTree_label (PosTree 1) pa' = Some(node_label p) -> pa=pa'. intros pa pa' p H H'. apply acc_inj with p 1;apply node_accessible; trivial. Qed.