proposition: Lemma backtrack_correct_size_opt {A} (lst : list (nat * G (option A))) s : semProdSizeOpt (backtrack lst) s <--> \bigcup_(x in lst :&: (fun x => x.1 <> 0)) (fun g => semProdSizeOpt (snd g) s) x.
proof: Proof. unfold backtrack. assert (Hret := @semReturnSize G _ _ (option A)). assert (Hbind := @semBindSize G _ _). simpl in *. assert (sum_fst lst = sum_fst lst)%coq_nat by reflexivity. revert H. assert (Datatypes.length lst = Datatypes.length lst)%coq_nat by reflexivity. revert H. generalize (sum_fst lst) at 1 3. generalize (Datatypes.length lst) at 1 3. intros n1. generalize lst. induction n1; intros l n2 Heq1 Heq2. - simpl. intros x; split; intros Hin. + eapply semReturnSizeOpt_None in Hin; eauto with typeclass_instances. inv Hin. + inv Hin. inv H. destruct l; try (simpl in *; congruence). inv H0. inv H2. - intros x; split; intros Hin. + with_strategy opaque [pickDrop] (simpl in Hin). eapply Hbind in Hin. inv Hin. inv H. eapply semChooseSize in H0; eauto. simpl in *. Admitted. Lemma backtrack_correct_opt {A} (lst : list (nat * G (option A))) : semProdOpt (backtrack lst) <--> \bigcup_(x in lst :&: fun x => x.1 <> 0) (semProdOpt x.2). Proof. split; intros H. - inv H. inv H0. assert (Hin : semProdSizeOpt (backtrack lst) x a). { eassumption. } eapply (@backtrack_correct_size_opt A) in Hin. inv Hin. inv H3. eexists. split; eauto. eexists. split; eauto. - destruct H. destruct H. destruct H0. destruct H0. destruct x. simpl in *. inv H. simpl in *. assert (Hin : (\bigcup_(x in lst :&: fun x => x.1 <> 0) (semProdSizeOpt x.2 x0)) a). { eexists. split; eauto. } eapply (@backtrack_correct_size_opt A) in Hin. eexists. split; eauto. Qed.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)