Вопросы Теги

Доказательство f (f bool) = bool

Если Вы хотите кодировать в Python и получить большую поддержку поточной обработки, Вы могли бы хотеть проверить IronPython или Jython. Так как код Python в IronPython и Jython работает на CLR.NET и Java VM соответственно, они пользуются большой поддержкой поточной обработки, встроенной в те библиотеки. В дополнение к этому IronPython не имеет GIL, проблемы, которая препятствует тому, чтобы потоки CPython в полной мере пользовались многоядерной архитектурой.

11
задан Gilles 'SO- stop being evil' 16 September 2012 в 21:37
поделиться

3 ответа

Goal forall (f:bool -> bool) (b:bool), f (f (f b)) = f b.
Proof.
intros.
remember (f true) as ft.
remember (f false) as ff.
destruct ff ; destruct ft ; destruct b ; 
    try rewrite <- Heqft ; try rewrite <- Heqff ; 
    try rewrite <- Heqft ; try rewrite <- Heqff ; auto.
Qed.
10
ответ дан 3 December 2019 в 05:58
поделиться

Немного более короткое доказательство:

Require Import Sumbool.

Goal forall (f : bool -> bool) (b:bool), f (f (f b)) = f b.
Proof.
  destruct b;                             (* case analysis on [b] *)
    destruct (sumbool_of_bool (f true));  (* case analysis on [f true] *)
    destruct (sumbool_of_bool (f false)); (* case analysis on [f false] *)
    congruence.                           (* equational reasoning *)
Qed.
4
ответ дан 3 December 2019 в 05:58
поделиться

В SSReflect : 

Require Import ssreflect.

Goal forall (f:bool -> bool) (b:bool), f (f (f b)) = f b.
Proof.
move=> f.
by case et:(f true); case ef:(f false); case; rewrite ?et ?ef // !et ?ef.
Qed.
4
ответ дан 3 December 2019 в 05:58
поделиться