Как бы доказать, что b = c if (andb b c = orb b c) в coq?

Question

Я новичок в Coq, и я пытаюсь доказать это ...

Theorem andb_eq_orb : 
    forall (b c : bool), 
    (andb b c = orb b c) -> (b = c). 

Вот мое доказательство, но я застреваю, когда я добираюсь до цели (ложь = истина -> ложь = истины).

Proof. 
intros b c. 
induction c. 
destruct b. 
reflexivity. 
simpl. 
reflexivity. 

Я не уверен, как бы переписать это выражение, чтобы я мог использовать рефлексивность. Но даже если я это сделаю, я не уверен, что это приведет к доказательству.

Мне удалось решить доказательство, если я начал с гипотезы b = c, хотя. А именно ...

Theorem andb_eq_orb_rev : 
    forall (b c : bool), 
    (b = c) -> (andb b c = orb b c). 
Proof. 
intros. 
simpl. 
rewrite H. 
destruct c. 
reflexivity. 
reflexivity. 
Qed. 

Но я не могу понять, как решить, если я начну с гипотезой, что имеет булевы функции.

Answer 1

Вам не нужна индукция, так как bool не является рекурсивной структурой данных. Просто просмотрите различные случаи для значений b и c. Для этого используйте destruct.В двух случаях гипотеза H будет иметь тип true = false, и вы можете закончить доказательство с помощью inversion H. В двух других случаях цель будет иметь тип true = true и ее можно решить с помощью reflexivity.

Theorem andb_eq_orb : forall b c, andb b c = orb b c -> b = c. 
Proof. destruct b,c; intro H; inversion H; reflexivity. Qed. 

Answer 2

Вы должны будете использовать тактику intro. Это переместит false = true в ваш контекст доказательства как предположение, которое вы затем можете использовать для перезаписи.

Answer 3

Возможно, это не самый эффективный способ сделать это.

На этапе induction c. (где он застрял):

______________________________________(1/2) 
b && true = b || true -> b = true 
______________________________________(2/2) 
b && false = b || false -> b = false 

Вы можете использовать rewrite и основные теоремы в [BOOL] [1], чтобы упростить такие термины, как b && true к b и b || true к true.

Это может свести к двум «тривиальным» целям подразделов:

b : bool 
______________________________________(1/2) 
b = true -> b = true 
______________________________________(2/2) 
false = b -> b = false 

Это почти тривиальное доказательство, используя assumption, за исключением того, что это один symmetry прочь. Вы можете try если symmetry сделаете их соответствие с помощью:

try (symmetry;assumption); try assumption. 

(Кто-то, кто действительно знает Coq может просветить меня, как try это более лаконично)

Собирает вместе:

Require Import Bool. 
Theorem andb_eq_orb : forall b c, andb b c = orb b c -> b = c. 
Proof. 
destruct c; 

try (rewrite andb_true_r); 
try (rewrite orb_true_r); 
try (rewrite andb_false_r); 
try (rewrite orb_false_r); 
intro H; 
try (symmetry;assumption); try assumption. 
Qed. 

A второй подход заключается в том, чтобы перетащить его и использовать метод «Таблица истины». Это означает, что вы можете разбить все переменные на свои значения истинности и упростить: destruct b, c; simpl.. Это снова дает четыре тривиальные последствия, вплоть до одного symmetry к try:

4 subgoal 
______________________________________(1/4) 
true = true -> true = true 
______________________________________(2/4) 
false = true -> true = false 
______________________________________(3/4) 
false = true -> false = true 
______________________________________(4/4) 
false = false -> false = false 

Собирая вместе:

Theorem andb_eq_orb1 : forall b c, andb b c = orb b c -> b = c. 
Proof. 
destruct b, c; simpl; intro; try (symmetry;assumption); try assumption. 
Qed. 

Первый подход является более трудным, но это не связано с перечислением всех строк таблицы истинности (I думать).