proposition: Lemma addToTreeCorrect1 : 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)), varySeed' (addToTree st p f l Corr Pref) p = Some (f p).
proof: Proof. intros st p. generalize dependent st. induction p. + intros st f l Corr Pref. unfold addToTree. destruct st. - auto. - exfalso. apply corrEmptyLeaf in Corr. inversion Corr; clear Corr. subst. pose proof Pref [] as Contra; clear Pref. eapply Contra; clear Contra. * left; auto. * instantiate (1 := []). instantiate (1 := []). auto. - simpl. auto. + intros. destruct st; destruct a; simpl. - rewrite refineFunCorrect. apply IHp. - rewrite refineFunCorrect; apply IHp. - exfalso. eapply corrEmptyLeaf in Corr; inversion Corr; subst; clear Corr. pose proof (Pref []). eapply H. -- subst; left; auto. -- simpl. instantiate (2:= []); rewrite app_nil_r. instantiate (1 := Left ::p); auto. - exfalso. eapply corrEmptyLeaf in Corr; inversion Corr; subst; clear Corr. pose proof (Pref []). eapply H. -- subst; left; auto. -- simpl. instantiate (2:= []); rewrite app_nil_r. instantiate (1 := Right ::p); auto. - rewrite refineFunCorrect; apply IHp. - rewrite refineFunCorrect; apply IHp. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List