proposition: Lemma fold_next_equiv ss1 ss2 ss ll1 ll2 ll : valid_pair (ss1, ss2) -> (forall s, In s ss -> valid_state s) -> incl ss ss1 -> pstates_equiv (ss1, ss2) (ll1, ll2) -> states_equiv ss ll -> pstates_equiv (fold_left nexts ss2 (ss1,ss)) (tc2it _ next (ll1,ll) ll2).
proof: Proof. intros (He1, He2) He3 H1 (H2, H3) H4. simpl in He1, He2, H2, H3. rewrite make_listtc2fold. unfold pstates_equiv; unfold states_equiv in H3. generalize ss1 ss2 ss ll1 ll He1 He2 He3 H1 H2 H3 H4. elim (tc2it _ make_list nil ll2); clear ss1 ss2 ss ll1 ll2 ll He1 He2 He3 H1 H2 H3 H4. intros ss1 ss2 ss ll1 ll He1 He2 He3 H1 H2; case ss2; auto. simpl; auto. intros s l HH; case (HH (rev3 (encode_state s))); intros _ HH1. now case HH1; simpl; auto with datatypes. intros. assert (F1: lequiv (map decode3 (a :: l)) ss2). intros s. split; intros H5. rewrite in_map_iff in H5; case H5; clear H5. intros l1 (Hl1, Hl2); subst. rewrite H3, in_map_iff in Hl2. case Hl2; intros s (Hs1, Hs2); subst. now rewrite encode_decode_state; auto. rewrite <- (encode_decode_state s); auto. apply (in_map decode3). rewrite H3. now apply (in_map (fun x => (rev3 (encode_state x)))); auto. rewrite fold_left_cons. case_eq (snextp (ll1, ll) a); intros ll2 ll3 Hll2. case_eq (nexts (ss1, ss) (decode3 a)); intros ss3 ss4 Hss3. assert (Fga: valid_state (decode3 a)). assert (F3: In a (a :: l)); auto with datatypes. rewrite H3, in_map_iff in F3; case F3; intros s (Hs1, Hs2); subst a. now rewrite encode_decode_state; auto. generalize (snext_equiv (ss1, ss) (decode3 a) (ll1, ll) a); auto. rewrite Hss3; rewrite Hll2; intros HH; case HH; auto; clear HH; try (split; auto; fail). unfold state_equiv. assert (F3: In a (a :: l)); auto with datatypes. rewrite H3, in_map_iff in F3; case F3; intros s (Hs1, Hs2); subst a. now rewrite encode_decode_state; auto. simpl; intros Heq1 Heq2. case (H ss3 (map decode3 l) ss4 ll2 ll3); auto. - generalize (nexts_valid (ss1, ss) (decode3 a)); auto. rewrite Hss3; intros HH; case HH; auto; clear HH. split; auto. - intros s Hs. rewrite in_map_iff in Hs; case Hs; intros l1 (Hl1, Hl2); subst. assert (F3: In l1 (a :: l)); auto with datatypes. rewrite H3, in_map_iff in F3. case F3; intros s (Hs1, Hs2); subst. rewrite encode_decode_state; auto. - generalize (nexts_valid (ss1, ss) (decode3 a)); auto. rewrite Hss3; intros HH; case HH; auto; clear HH. split; auto. - generalize (nexts_incl (ss1,ss) (decode3 a)); rewrite Hss3; auto. - intros s; rewrite in_map_iff; split. intros Hs. assert (F2: In s (a :: l)); auto with datatypes. rewrite H3, in_map_iff in F2. case F2; intros s1 (Hs1, Hs2); subst. exists s1; split; auto. rewrite in_map_iff. exists (rev3 (encode_state s1)); split; auto. now rewrite <- encode_decode_state; auto. intros (s1, (Hs1, Hs2)); subst. rewrite in_map_iff in Hs2. case Hs2; intros l1 (Hl1, Hl2); subst. assert (F2: In l1 (a :: l)); auto with datatypes. rewrite H3, in_map_iff in F2. case F2; intros s1 (Hs3, Hs4); subst. rewrite (encode_decode_state s1); auto. - intros F2 F3. case (fold_nexts_equiv (ss1, (map decode3 (a :: l))) (ss1, ss2) ss ss); simpl; auto. + split; simpl; auto. intros s; split; auto. + intros s; split; auto. + rewrite Hss3. intros Hf1 Hf2. split. rewrite <- Hll2 in F2. now apply states_equiv_equiv with (1 := F2); auto. rewrite <- Hll2 in F3. apply states_equiv_equiv with (1 := F3); auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max