proposition: Lemma decode_encode n l : (length l <= n)%nat -> unique l -> l = decode (encode l n).
proof: Proof. revert l; elim n; simpl; clear n. intros l; case l; simpl; auto. now intros p1 k1 HH; inversion HH. intros n Hrec l; case l; simpl; auto; clear l. intros p1 l H H1; apply f_equal2 with (f := @cons _); auto. rewrite <- Hrec. - inversion_clear H1 as [ |xx yy Ha Hb]. generalize Hb; elim Ha; auto; clear l Ha Hb H. intros a1 l Ha Hrec1 Hb Ha1. simpl. generalize (cube_compare_correct p1 a1); case cube_compare; intros H2. + case Ha1; rewrite H2; auto with datatypes. + generalize (cube_compare_correct p1 (cube_pred a1)); case cube_compare; intros H3. * apply f_equal2 with (f := @cons _); auto with datatypes. generalize H2; case a1; auto; intros HH; contradict HH; auto with arith. * apply f_equal2 with (f := @cons _); auto with datatypes. generalize H2; case a1; auto; intros HH; contradict HH; auto with arith. * contradict H3; generalize H2; case a1; auto with arith. + generalize (cube_compare_correct p1 a1); case cube_compare; intros H3; try (contradict H2; try rewrite H3; auto with arith; fail). apply f_equal2 with (f := @cons _); auto with datatypes. - rewrite encode_aux_length; auto with arith. - apply encode_aux_unique; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik