proposition: Lemma encode_valid s : valid_state s -> valid3 (encode_state s).
proof: Proof. case s. intros i7 i6 i5 i4 i3 i2 i1 o1 o2 o3 o4 o5 o6 o7 H. unfold encode_state. set (l1 := (i7 :: i6 :: i5 :: i4 :: i3 :: i2 :: i1 :: nil)). unfold encode_memo, encode_memo_list. rewrite memo_get_val_correct. assert (F1 : unique l1). case H; intros H1 H2. apply unique_perm with (1 := H1). now apply unique7. assert (F2: lmax l1 = 6%nat). case H; intros H1 _. now unfold l1; rewrite <- (lmax_perm _ _ H1); simpl; auto. assert (F3: (decrease (encode l1 7) 7)). now apply encode_decrease; auto; rewrite F2; red; auto. generalize (decode_encode 7 l1 (le_n _) F1) F3. change l1 with ((i7 :: i6 :: i5 :: i4 :: i3 :: i2 :: nil) ++ (i1 :: nil)). rewrite encode_max; auto. case encode. now intros; discriminate. intros p7 l; case l; clear l. match goal with |- ?X = ?Y -> _ => intros HH; assert (HH1: length X = length Y); try discriminate end. intros p6 l; case l; clear l. now match goal with |- ?X = ?Y -> _ => intros HH; assert (HH1: length X = length Y); try discriminate end. intros p5 l; case l; clear l. now match goal with |- ?X = ?Y -> _ => intros HH; assert (HH1: length X = length Y); try discriminate end. intros p4 l; case l; clear l. now match goal with |- ?X = ?Y -> _ => intros HH; assert (HH1: length X = length Y); try discriminate end. intros p3 l; case l; clear l. now match goal with |- ?X = ?Y -> _ => intros HH; assert (HH1: length X = length Y); try discriminate end. intros p2 l Hp; unfold rev, app, decode_state. match type of Hp with _ = decode ?X => generalize (decode_length X); rewrite <- Hp; simpl length; repeat rewrite app_length; simpl length end. generalize Hp; case l; simpl length; simpl app; clear Hp. intros Hp _ (Hd1, (Hd2, (Hd3, (Hd4, (Hd5, (Hd6, _)))))). repeat split; auto. unfold valid63; generalize Hd5; case o6; case p3; case p7; intros H1 H2; try discriminate; contradict H1; apply Nat.le_ngt; simpl; auto with arith. intros pp ll; rewrite Nat.add_comm. now intros _ HH; inversion HH. simpl app; case H; intros H1 _. rewrite <- (lmax_perm _ _ H1); simpl. unfold Z.max; simpl; auto with zarith. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max