proposition: Proposition is_path_from_characterization P n l : is_path_from P n l <-> exists l', length l' = n /\ forall n', n'<=n -> ~ P (rev (firstn n' l') ++ l).
proof: Proof. intros. split. - induction 1 as [|* HP _ (l'&Hl'&HPl')|* HP _ (l'&Hl'&HPl')]. + exists []. split. * reflexivity. * intros n ->%Nat.le_0_r. assumption. + exists (true :: l'). split. * apply eq_S, Hl'. * intros [|] H. -- assumption. -- simpl. rewrite <- app_assoc. apply HPl', le_S_n, H. + exists (false :: l'). split. * apply eq_S, Hl'. * intros [|] H. -- assumption. -- simpl. rewrite <- app_assoc. apply HPl', le_S_n, H. - intros (l'& <- &HPl'). induction l' as [|[|]] in l, HPl' |- *. + constructor. apply (HPl' 0). apply Nat.le_0_l. + eapply next_left. * apply (HPl' 0), Nat.le_0_l. * fold (length l'). apply IHl'. intros n' H%le_n_S. apply HPl' in H. simpl in H. rewrite <- app_assoc in H. assumption. + apply next_right. * apply (HPl' 0), Nat.le_0_l. * fold (length l'). apply IHl'. intros n' H%le_n_S. apply HPl' in H. simpl in H. rewrite <- app_assoc in H. assumption. Qed.
imports: WeakFan List Arith