proposition: Theorem nestedRandomFunc_app_spec : forall ls ls1 x1 x2 a, (forall y, arrayLookup _ x1 y = arrayLookup _ x2 y) -> comp_spec (fun y1 y2 => any_dec (fun y => if arrayLookup _ ls (fst y) then true else false) (snd y1) = any_dec (fun y => if arrayLookup _ ls (fst y) then true else false) (snd y2) /\ (any_dec (fun y => if arrayLookup _ ls (fst y) then true else false) (snd y1) = false -> (forall z, arrayLookup _ (snd y1) z = arrayLookup _ (snd y2) z) /\ fst y1 = fst y2)) (nestedRandomFunc (ls ++ ls1) x1 a) (nestedRandomFunc ls1 x2 a).
proof: Proof. intros. unfold nestedRandomFunc. match goal with | [|- context[match ?a with | Some _ => _ | None => _ end] ] => case_eq a; intros end. match goal with | [H: arrayLookup ?eqd (?ls1 ++ ?ls2) ?a = Some _ |- _] => case_eq (arrayLookup eqd ls1 a); intros end. erewrite arrayLookup_app_Some in H0; eauto. inversion H0; clear H0; subst. match goal with | [|- context[match ?a with | Some _ => _ | None => _ end] ] => case_eq a; intros end. eapply comp_spec_ret; intuition idtac. simpl in *. repeat rewrite any_dec_cons. simpl. match goal with | [|- context[if ?a then _ else _] ] => replace a with (Some r) end; simpl; trivial. simpl in *. rewrite any_dec_cons in *. apply orb_false_elim in H2. intuition. simpl in *. match goal with | [H: (if ?a then _ else _) = false |- _] => replace a with (Some r) in H end; trivial. discriminate. simpl in *. rewrite any_dec_cons in *. apply orb_false_elim in H2. intuition idtac. simpl in *. match goal with | [H: (if ?a then _ else _) = false |- _] => replace a with (Some r) in H end; trivial. discriminate. unfold randomFunc. match goal with | [|- context[match ?a with | Some _ => _ | None => _ end] ] => case_eq a; intros end. eapply comp_spec_ret; intuition idtac. simpl in *. rewrite any_dec_cons. simpl. match goal with | [|- context[if ?a then _ else _] ] => replace a with (Some r) end; trivial. simpl. symmetry. eapply ex_any_dec. eapply arrayLookup_Some_impl_In. eauto. simpl. match goal with | [|- context[if ?a then _ else _] ] => replace a with (Some r) end; simpl; trivial. simpl in *. rewrite any_dec_cons in *. apply orb_false_elim in H3. intuition idtac. simpl in *. match goal with | [H: (if ?a then _ else _) = false |- _] => replace a with (Some r) in H end; trivial. discriminate. simpl in *. rewrite any_dec_cons in *. apply orb_false_elim in H3. intuition idtac. simpl in *. match goal with | [H: (if ?a then _ else _) = false |- _] => replace a with (Some r) in H end; trivial. discriminate. fcf_irr_r. eapply comp_spec_ret; intuition idtac. simpl in *. repeat rewrite any_dec_cons. simpl in *. repeat rewrite (any_dec_map fst (fun y =>if (arrayLookup _ ls y) then true else false)). repeat rewrite <- fst_split_map_eq. rewrite any_dec_arrayLookup_swap. symmetry. rewrite any_dec_arrayLookup_swap. symmetry. f_equal. eapply any_dec_f_eq. intuition idtac. rewrite H. reflexivity. simpl in *. rewrite any_dec_cons in *. apply orb_false_elim in H4. intuition idtac. simpl in *. match goal with | [H: (if ?a then _ else _) = false |- _] => replace a with (Some r) in H end; trivial. discriminate. simpl in *. rewrite any_dec_cons in *. apply orb_false_elim in H4. intuition idtac. simpl in *. match goal with | [H: (if ?a then _ else _) = false |- _] => replace a with (Some r) in H end; trivial. discriminate. rewrite arrayLookup_app_None in H0. rewrite H0. eapply comp_spec_ret; intuition idtac. simpl in *. repeat rewrite any_dec_cons. simpl in *. repeat rewrite (any_dec_map fst (fun y =>if (arrayLookup _ ls y) then true else false)). repeat rewrite <- fst_split_map_eq. rewrite any_dec_arrayLookup_swap. symmetry. rewrite any_dec_arrayLookup_swap. symmetry. f_equal. eapply any_dec_f_eq. intuition idtac. rewrite H. reflexivity. simpl in *. rewrite H. reflexivity. trivial. match goal with | [H: arrayLookup ?eqd (?ls1 ++ ?ls2) ?a = None |- _] => case_eq (arrayLookup eqd ls1 a); intros end. erewrite arrayLookup_app_Some in H0; eauto. discriminate. rewrite arrayLookup_app_None in H0. rewrite H0. unfold randomFunc. rewrite H. match goal with | [|- context[match ?a with | Some _ => _ | None => _ end] ] => case_eq a; intros end. eapply comp_spec_ret; intuition idtac. simpl in *. repeat rewrite (any_dec_map fst (fun y =>if (arrayLookup _ ls y) then true else false)). repeat rewrite <- fst_split_map_eq. rewrite any_dec_arrayLookup_swap. symmetry. rewrite any_dec_arrayLookup_swap. symmetry. eapply any_dec_f_eq. intuition idtac. rewrite H. reflexivity. fcf_skip. eapply comp_base_exists; eauto. eapply comp_base_exists; eauto. eapply comp_spec_ret; intuition idtac. simpl in *. repeat rewrite any_dec_cons. repeat rewrite (any_dec_map fst (fun y =>if (arrayLookup _ ls y) then true else false)). repeat rewrite <- fst_split_map_eq. rewrite any_dec_arrayLookup_swap. symmetry. rewrite any_dec_arrayLookup_swap. symmetry. f_equal. eapply any_dec_f_eq. intuition idtac. rewrite H. reflexivity. simpl. rewrite H. reflexivity. trivial. Qed.
imports: FCF.FCF FCF.CompFold FCF.Array FCF.Hybrid