proposition: Lemma addToTreeCorrect3 : 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' (addToTree st p f l Corr Pref) p' = Some seed -> p = p' \/ varySeed' st p' = Some seed.
proof: Proof. intros st p. generalize dependent st. induction p. + intros. destruct p'. - left; auto. - right. exfalso. unfold addToTree in H; simpl in H. destruct st; simpl in H. * inversion H. * clear H. apply corrEmptyLeaf in Corr; inversion Corr; subst; clear Corr. subst. eapply Pref. instantiate (1 := []). left; auto. instantiate (1 := []); instantiate (1 := []); auto. * inversion H. + intros. destruct p'; destruct st; destruct a; simpl in *; try solve [match goal with [ H : None = Some _ |- _ ] => inversion H end]. ++ exfalso. clear H. apply corrEmptyLeaf in Corr; inversion Corr; subst; clear Corr. eapply Pref. subst. instantiate (1 := []) ; left; auto. instantiate (1 := (Left :: p)); instantiate (1 := []); rewrite app_nil_r; auto. ++ exfalso. clear H. apply corrEmptyLeaf in Corr; inversion Corr; subst; clear Corr. eapply Pref. subst. instantiate (1 := []) ; left; auto. instantiate (1 := (Right :: p)); instantiate (1 := []); rewrite app_nil_r; auto. ++ destruct s; simpl in *. - assert (p = p' \/ varySeed' SeedTreeUndef p' = Some seed) by (eapply IHp; eauto). inversion H0. * left; subst; auto. * simpl in H1. inversion H1. - inversion H. ++ destruct s; simpl in *. - inversion H. - assert (p = p' \/ varySeed' SeedTreeUndef p' = Some seed) by (eapply IHp; eauto). inversion H0. * left; subst; auto. * simpl in H1. inversion H1. ++ exfalso. clear H. apply corrEmptyLeaf in Corr; inversion Corr; subst; clear Corr. subst. eapply Pref. instantiate (1 := []). - left; auto. - instantiate (1 := Left :: p); instantiate (1 := []); rewrite app_nil_r; auto. ++ exfalso. clear H. apply corrEmptyLeaf in Corr; inversion Corr; subst; clear Corr. subst. eapply Pref. instantiate (1 := []). - left; auto. - instantiate (1 := Right :: p); instantiate (1 := []); rewrite app_nil_r; auto. ++ destruct s eqn:S; simpl in *. - assert (p = p' \/ varySeed' st1 p' = Some seed) by (eapply IHp; eauto). inversion H0. * left; subst; auto. * right; auto. - right; auto. ++ destruct s eqn:S; simpl in *. - right; auto. - assert (p = p' \/ varySeed' st2 p' = Some seed) by (eapply IHp; eauto). inversion H0. * left; subst; auto. * right; auto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List