Как бих доказал, че b = c ако (и b b c = orb b c) в coq?

Не се нуждаете от индукция, тъй като 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.

Ще искате да използвате тактиката intro. Това ще премести false = true във вашия контекст на доказателство като предположение, което след това можете да използвате, за да пренапишете.

Това може да не е най-ефективният начин да го направите.

На стъпка 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.

Вторият подход е груба сила и използване на метода "Таблица на истината". Това означава, че можете да разбиете всички променливи до техните истински стойности и да опростите: 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.

Първият подход е по-обезпокоителен, но не включва изброяване на всички редове на таблицата на истината (мисля).