proposition: Lemma addToTreeCorrect2 : forall (st : SeedTree) (p : SplitPath) (f : SplitPath -> RandomSeed) (l : list SplitPath) (Corr : correspondingSeedTree l f st) (Pref : forall p', In p' l -> (forall p1 p2, p ++ p1 = p' ++ p2 -> False)), forall p' seed, varySeed' st p' = Some seed -> varySeed' (addToTree st p f l Corr Pref) p' = Some seed.
proof: Proof. intros st p. generalize dependent st. induction p as [ | d ds]. + intros. exfalso. eapply Pref. - inversion Corr as [Vary_In In_Vary Pref']; clear Corr. eapply Vary_In; eassumption. - instantiate (1 := []); instantiate (1 := p'); rewrite app_nil_r; auto. + intros st f l Corr Pref p' seed VarySome. destruct st; destruct d; simpl; auto. * exfalso. apply corrUndefEmpty in Corr. subst. inversion VarySome. * exfalso. apply corrUndefEmpty in Corr. subst. inversion VarySome. * exfalso. apply corrEmptyLeaf in Corr; inversion Corr; subst; clear Corr. eapply Pref. instantiate (1 := []); left; auto. instantiate (1:= Left :: ds). instantiate (1 := []). rewrite app_nil_r; simpl; auto. * exfalso. apply corrEmptyLeaf in Corr; inversion Corr; subst; clear Corr. eapply Pref. instantiate (1 := []); left; auto. instantiate (1:= Right :: ds). instantiate (1 := []). rewrite app_nil_r; simpl; auto. * destruct p'. - simpl in VarySome. inversion VarySome. - destruct s. ++ apply IHds; auto. ++ auto. * destruct p'. - simpl in VarySome; inversion VarySome. - destruct s. ++ auto. ++ apply IHds; auto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List