proposition: Theorem pb_unique_prefix1 : forall (t : pbtree) (a1 a2 : A) (lb1 lb2 : list bool), In (a1, lb1) (compute_pbcode t) -> In (a2, lb2) (compute_pbcode t) -> is_prefix lb1 lb2 -> a1 = a2 :>A.
proof: Proof. intros t; elim t; simpl in |- *; auto. intros leaf a1 a2 lb1 lb2 H1 H2. case H1; intros H3; [ injection H3 | case H3 ]. case H2; intros H4; [ injection H4 | case H4 ]. intros H H0 H5 H6 H7; apply trans_equal with (2 := H0); auto. intros p H a1 a2 lb1 lb2 H0 H1 H2. case ((proj1 (in_map_iff _ _ _)) H0). intros (a3, l3) (Hl3, Ha3). case ((proj1 (in_map_iff _ _ _)) H1). intros (a4, l4) (Hl4, Ha4). apply (H a1 a2 l3 l4); auto. injection Hl3; intros HH1 HH2; rewrite <- HH2; auto. injection Hl4; intros HH1 HH2; rewrite <- HH2; auto. cut (is_prefix (false :: l3) (false :: l4)); [ intros HH1; inversion HH1; auto | idtac ]. injection Hl3; injection Hl4; intros HH1 HH2 HH3 HH4; rewrite HH3; rewrite HH1; auto. intros p H a1 a2 lb1 lb2 H0 H1 H2. case ((proj1 (in_map_iff _ _ _)) H0). intros (a3, l3) (Hl3, Ha3). case ((proj1 (in_map_iff _ _ _)) H1). intros (a4, l4) (Hl4, Ha4). apply (H a1 a2 l3 l4); auto. injection Hl3; intros HH1 HH2; rewrite <- HH2; auto. injection Hl4; intros HH1 HH2; rewrite <- HH2; auto. cut (is_prefix (true :: l3) (true :: l4)); [ intros HH1; inversion HH1; auto | idtac ]. injection Hl3; injection Hl4; intros HH1 HH2 HH3 HH4; rewrite HH3; rewrite HH1; auto. intros t1 Rec1 t2 Rec2 a1 a2 lb1 lb2 H1 H2. case (in_app_or _ _ _ H1); case (in_app_or _ _ _ H2); clear H1 H2; intros H2 H1 H3. generalize H1 H2; inversion H3. intros H4; case ((proj1 (in_map_iff _ _ _)) H4). intros x; case x; intros x1 x2 (H6, H5); discriminate. intros H5 H6; apply Rec1 with (lb1 := l1) (lb2 := l2); auto. case ((proj1 (in_map_iff _ _ _)) H5). intros x; case x. intros a l (H8, H7); injection H8. intros R1 R2 R3; rewrite <- R1; rewrite <- R3; auto. case ((proj1 (in_map_iff _ _ _)) H6). intros x; case x. intros a l (H8, H7); injection H8. intros R1 R2 R3; rewrite <- R1; rewrite <- R3; auto. generalize H3. case ((proj1 (in_map_iff _ _ _)) H1). intros x; case x; intros aa1 ll1 (H5, H4). case ((proj1 (in_map_iff _ _ _)) H2). intros x1; case x1; intros aa2 ll2 (H7, H6). inversion H5; inversion H7; intros tH8; inversion tH8. generalize H3. case ((proj1 (in_map_iff _ _ _)) H1). intros x; case x; intros aa1 ll1 (H5, H4). case ((proj1 (in_map_iff _ _ _)) H2). intros x1; case x1; intros aa2 ll2 (H7, H6). inversion H5; inversion H7; intros tH8; inversion tH8. generalize H1 H2; inversion H3. intros H4; case ((proj1 (in_map_iff _ _ _)) H4). intros x; case x; intros x1 x2 (H6, H5); discriminate. intros H5 H6; apply Rec2 with (lb1 := l1) (lb2 := l2); auto. case ((proj1 (in_map_iff _ _ _)) H5). intros x; case x. intros a l (H8, H7); injection H8. intros R1 R2 R3; rewrite <- R1; rewrite <- R3; auto. case ((proj1 (in_map_iff _ _ _)) H6). intros x; case x. intros a l (H8, H7); injection H8. intros R1 R2 R3; rewrite <- R1; rewrite <- R3; auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)