proposition: Lemma checker_backtrack_spec_false l : checker_backtrack l = Some false <-> (forall f, List.In f l -> f tt = Some false).
proof: Proof. unfold checker_backtrack. induction l. - split; eauto. intros Heq; intros f Hin; inv Hin. - destruct (a tt) eqn:Hdec. * destruct b. -- split. congruence. intros Hin. assert (Hc : a tt = Some false). { eapply Hin. now left. } congruence. -- split. ++ intros Haux f Hin. inv Hin; eauto. eapply IHl; eauto. ++ intros Hin. eapply IHl. intros. eapply Hin. now right. * split. -- intros H1 f Hin. revert H1. clear. intros H1; induction l. congruence. destruct (a tt). ++ destruct b. congruence. eauto. ++ eauto. -- intros Hall. assert (Hc : a tt = Some false). { eapply Hall. now left. } congruence. Qed.
imports: String List RoseTrees Show State Producer Generators Enumerators Classes DependentClasses Checker Decidability TacticsUtil Ltac2(Ltac2)