Как доказать (forall x, P x/\Q x)-> (forall x, P x)
Это по замыслу. По умолчанию TaskScheduler используется .NET ThreadPool , который может быть насыщенным, и вы имеете ограниченный контроль над ним.
Если вы хотите, вы можете создать свой собственный TaskScheduler, чтобы изменить это поведение. Например, при желании вы можете создать тот, который запускает отдельный поток.
Такое поведение стало бы еще более явным, если бы ваш код выполнял еще больше задач, чем он уже делает:
private void DoParallel()
{
//This will over-saturate the ThreadPool unless you use your own TaskScheduler
for (int i = 0; i < 100; i++)
{
Task.Factory.StartNew(() =>
{
Console.WriteLine(DateTime.Now.ToString());
DoSomeWork();
});
}
}
}
4 ответа
Вы можете сделать это быстрее, просто применив H, но этот сценарий должно быть более понятным.
Lemma foo : forall (A:Type) (P Q: A-> Prop), (forall x, P x /\ Q x) -> (forall x, P x).
intros.
destruct (H x).
exact H0.
Qed.
На самом деле, я понял это, когда обнаружил это:
Математика для компьютерных ученых 2
В уроке 5 он решает ту же задачу и использует команду «вырезать (P x / \ Q x)», которая переписывает цель с «P x» на «P x / \ Q x -> P x ". Оттуда вы можете выполнить некоторые манипуляции, а когда цель - просто «P x / \ Q x», вы можете применить «forall x: P x / \ Q x», а остальное просто.
Assume ForAll x: P(x) /\ Q(x)
var x;
P(x) //because you assumed it earlier
ForAll x: P(x)
(ForAll x: P(x) /\ Q(x)) => (ForAll x: P(x))
Интуитивно понятно, что если для всех x, P(x) И Q(x) выполняются, то для всех x, P(x) выполняется.