proposition: Lemma snext_equiv ps s ll l : valid_state s -> valid_pair ps -> incl (snd ps) (fst ps) -> pstates_equiv ps ll -> state_equiv s l -> pstates_equiv (nexts ps s) (snextp ll l).
proof: Proof. unfold nexts, snextp, next. destruct ps as (ss1, ss2). destruct ll as (ll1, ll2). destruct l as ((l1,l2),p). intros Hg Hg1 Hi H1 Hs. simpl in Hg1, Hi, H1. match goal with |- context[fold_left ?X _ _] => change X with (fun ps f => filters ps (f s)) end. match goal with |- context[fold_left ?X ?Y (ll1,?Z)] => replace (fold_left X Y (ll1,Z)) with (fold_left (fun ps f => filter ps (f (decode_state l1 l2 p))) Y (ll1,Z)) end. generalize ss1 ss2 s ll1 ll2 l1 l2 p Hg Hg1 Hi H1 Hs (movel_valid). clear ss1 ss2 s ll1 ll2 l1 l2 p Hg Hg1 Hi H1 Hs. elim movel. now unfold pstates_equiv; simpl; auto. intros f lf Hrec ss1 ss2 s ll1 ll2 l1 l2 p Hg Hg1 Hi H1 Hs Hf. assert (F0: valid_state (f s)); auto with datatypes. repeat rewrite fold_left_cons. case_eq (filters (ss1, ss2) (f s)); intros ss3 ss4 Hss3. case_eq (filter (ll1, ll2) (f (decode_state l1 l2 p))); intros ll3 ll4 Hll3. generalize (filter_equiv _ _ _ F0 Hg1 Hi H1). rewrite Hss3. change (decode_state l1 l2 p) with (decode3 (l1, l2, p)) in Hll3. unfold state_equiv in Hs; rewrite Hs in Hll3; auto; rewrite encode_decode_state in Hll3; auto. rewrite Hll3; intros HH; case HH; auto; intros Hf1 Hf2. apply Hrec; auto with datatypes. now generalize (filters_valid (ss1, ss2) (f s)); rewrite Hss3; intros HH1; case HH1; auto. now generalize (filters_incl (ss1, ss2) (f s)); rewrite Hss3; auto. generalize (ll1, ll2); elim movel; simpl; auto. intros a l Hrec q; rewrite Hrec; auto. unfold filter; case encode_state; auto. intros (xx,yy); auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max