proposition: Lemma encode_max n l a : (length l <= n)%nat -> unique (l ++ (a :: nil)) -> (lmax (l ++ (a :: nil)) <= length l)%nat -> encode (l ++ (a :: nil)) (S n) = encode l n ++ (C1 :: nil).
proof: Proof. revert l a; elim n; clear n. intros l; case l; simpl; auto. intros a _ _; rewrite Nat.max_l; auto with zarith. intros; apply f_equal2 with (f := @cons _); auto. now generalize H; case a; simpl; auto with arith; intros HH; contradict HH; auto with arith. now intros p l1 a H; contradict H; auto with arith. intros n Hrec l; case l; auto; clear l. intros a _ _; simpl; rewrite Nat.max_l; auto with zarith. now case a; simpl; auto with arith; intros HH; contradict HH; auto with arith. intros p l a H1 H2 H3. change (encode ((p :: l) ++ a :: nil) (S (S n))) with (p :: encode (encode_aux (l ++ a :: nil) p) (S n)). change (encode (p :: l) (S n) ++ C1 :: nil) with (p :: (encode (encode_aux l p) n ++ C1 :: nil)). apply f_equal2 with (f := @cons _); auto. assert (F1: (length (l ++ a :: nil) <= S n)%nat). now rewrite app_length; rewrite Nat.add_comm; auto. generalize F1; rewrite <- (encode_aux_length p). assert (F2: unique (encode_aux (l ++ a :: nil) p)). now apply encode_aux_unique; auto. generalize F2. rewrite encode_aux_app. intros G1 G2. set (u := encode_aux l p); simpl encode_aux. apply Hrec; unfold u. - rewrite encode_aux_length. apply le_S_n; generalize F1; rewrite app_length; auto. - assert (F3: unique (encode_aux (l ++ a :: nil) p)). now apply encode_aux_unique; auto. generalize F3; rewrite encode_aux_app; auto. - change (match cube_compare p a with | Eq => a | Lt => cube_pred a | Gt => a end :: nil) with (encode_aux (a :: nil) p). rewrite <- encode_aux_app. assert (F4: (lmax (encode_aux (l ++ a :: nil) p) < length (p :: l))%nat). case (Nat.le_gt_cases (c2N p) (lmax (l ++ a :: nil))); intros H4. assert (F3 : (lmax (encode_aux (l ++ a :: nil) p) < lmax (l ++ a :: nil))%nat). apply encode_aux_lmax_lt; auto. now case l; intros; discriminate. change (lmax ((p :: l) ++ a :: nil)) with (Nat.max (c2N p) (lmax (l ++ a :: nil))) in H3. rewrite Nat.max_r in H3; auto. now apply Nat.lt_le_trans with (1 := F3); auto. rewrite encode_aux_id; auto. apply Nat.lt_le_trans with (2 := H3); auto. change (lmax ((p :: l) ++ a :: nil)) with (Nat.max (c2N p) (lmax (l ++ a :: nil))). now rewrite Nat.max_l; auto with zarith. rewrite encode_aux_length. generalize F4; unfold length; repeat rewrite inj_S; auto with zarith. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max