proposition: Theorem decode_aux_correct : forall c : code, unique_prefix c -> not_null c -> forall (m1 m2 head : list bool) (a : A), find_val (head ++ m1) c = Some a -> decode_aux c head (m1 ++ m2) = a :: decode_aux c [] m2.
proof: Proof. intros c Hc1 Hc2 m1; elim m1; simpl in |- *; auto. intros m2; case m2; simpl in |- *; auto. intros head a; rewrite app_nil_r. intros H1; rewrite H1; auto. rewrite not_null_find_val; auto. intros b l head a; rewrite app_nil_r. intros H1; rewrite H1; auto. rewrite not_null_find_val; auto. intros a l Rec m2 head a1 H2. rewrite <- Rec with (head := head ++ a :: []). generalize (fun a => find_val_correct1 c a head). case (find_val head c); auto. intros a0 H; (cut (In (a0, head) c); [ intros Hin1 | auto ]). cut (In (a1, head ++ a :: l) c); [ intros Hin2 | apply find_val_correct1; auto ]. cut (a1 = a0); [ intros Heq | idtac ]. absurd (head ++ a :: l = head); auto. elim head; simpl in |- *; auto. red in |- *; intros; discriminate. intros a2 l0 H0; red in |- *; intros H1; case H0; auto. injection H1; auto. apply unique_key_in_inv with (l := c) (a := a1); auto. apply unique_prefix2; auto. rewrite Heq; auto. apply sym_equal; apply (unique_prefix1 c a0 a1 head (head ++ a :: l)); auto. elim head; simpl in |- *; auto. rewrite <- app_assoc; auto. Qed.
imports: Coq(Sorting.Permutation)