proposition: Lemma get_next_correct n n1 s s1 s2 : (s1, s2) = fst (iter2s n) -> n1 < n -> nsreachable (S n1) s -> match get_next s s1 s2 with Some m => nsreachable n1 (m2f m s) | None => False end.
proof: Proof. generalize (iter2s_correct n) (fun n1 s => get_number_correct n n1 s s1 s2); case iter2s. intros (s3, s4) ss; simpl; intros (H1, (H2, H3)) Hn HH Hl Hr. injection HH; intros; subst s3 s4; clear HH. case (move_nsreachable _ _ Hr); intros s3 (Hs1, Hs2). case (fun x => (move_Movel _ _ (move_sym _ _ x Hs1))). case Hs2; intros H4 _; apply nreachable_valid with (1 := H4). intros a (Ha, Ha1); subst. unfold get_next. generalize (get_next_aux_correct (pos_down (get_number s s1 s2)) s s1 s2 Movel); case get_next_aux. - intros a1 (Ha2, Ha3). rewrite <- (Hn (S n1) s) in Ha3; auto with arith. assert (F1: nreachable (S (S n1)) (m2f a1 s)). apply nreachS with s; auto. + case Hr; auto. + apply Movel_move; auto. + case (nsreachable_bound _ _ F1); intros k1 (Hk2, Hk3). assert (F2: nreachable (S k1) s). apply nreachS with (m2f a1 s); auto. * case Hk3; auto. * apply move_sym; try apply Movel_move; auto. apply nreachable_valid with (S n1); case Hr; auto. * case (nsreachable_bound _ _ F2); intros k2 (Hk4, Hk5). assert (k2 = (S n1)); subst. apply nsreachable_unique with (2 := Hr); auto. assert (Hv : n1 <= k1) by auto with zarith. apply Nat.le_lteq in Hv; clear Hk4; destruct Hv as [Hk4|Hk4]; subst; auto. apply Nat.le_lteq in Hk2; destruct Hk2 as [Hk2|Hk2]. -- rewrite <- (Hn k1) in Ha3; auto with arith. ++ rewrite porderS, pos_down_up in Ha3; auto. ** assert (Hv : k1 <= S n1) by auto with zarith. apply Nat.le_lteq in Hv; destruct Hv as [HH|HH]. --- contradict HH; auto with arith. --- subst; contradict Ha3. rewrite porderS. case (porder n1); simpl; auto; try (intros; discriminate). intros p; case p; intros; discriminate. ** generalize (porder_inv n1); intros [HH1|[HH1|HH1]]; rewrite HH1; red; auto. ++ apply Nat.le_trans with (S n1); auto with arith. -- subst k1; clear F1 F2. case (Nat.le_gt_cases (S (S n1)) n); intros Hk6. ++ rewrite <- (Hn (S (S n1))) in Ha3; auto with arith. contradict Ha3; repeat rewrite porderS. case (porder n1); simpl; auto; try (intros; discriminate). intros p; case p; intros; discriminate. ++ assert (F1: get_number (m2f a1 s) s1 s2 = 4%positive). ** unfold get_number. generalize (in_states_correct (m2f a1 s) s1); case in_states; intros G1. --- rewrite H1 in G1. contradict Hk6; case G1; intros k (Hk, (Hk1,Hk2)). assert (k = S (S n1)); subst; auto with arith. apply nsreachable_unique with (1 := Hk1); auto. --- generalize (in_states_correct (m2f a1 s) s2); case in_states; intros G2; auto. rewrite H2 in G2. contradict Hk6; case G2; intros k (Hk, (Hk1,Hk2)). assert (k = S (S n1)); subst; auto with arith. apply nsreachable_unique with (1 := Hk1); auto. ** contradict Ha3; rewrite F1. case porder; simpl; try (intros; discriminate); intros p; case p; intros; discriminate. - intros HH; case (HH a); auto. rewrite <- (Hn n1 (m2f a s)); auto with arith. rewrite <- (Hn (S n1)); auto with arith. rewrite porderS, pos_down_up; auto; generalize (porder_inv n1); intros [HH1|[HH1|HH1]]; rewrite HH1; red; auto. Qed.
imports: ZArith List