proposition: Lemma encode_decode_state s : valid_state s -> decode3 (rev3 (encode_state s)) = s.
proof: Proof. assert (Har: forall n m, (m <= n -> m - n = 0)%nat). induction n as [ | n Hrec]; destruct m as [ | m]; simpl; auto with arith. 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. now 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, _)))))). unfold rev3, decode3; simpl rev; unfold decode_state. rewrite cube3_encode_decode; auto with arith. unfold decode_memo, decode_memo_list. rewrite memo_get_val_correct. rewrite <- Hp; simpl. case H; simpl; intros H1 H2. rewrite oinv_eq with (oy := o7); auto. assert (oadd_assoc: forall ox oy oz, oadd ox (oadd oy oz) = oadd (oadd ox oy) oz). now intros ox oy oz; case ox; case oy; case oz; auto. now repeat rewrite oadd_assoc; auto. case o6; auto. intros pp ll; rewrite Nat.add_comm. now intros _ HH; inversion HH. simpl app; case H; intros H1 _. rewrite <- (lmax_perm _ _ H1); simpl; auto with arith. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max