Comment pourrais-je prouver que b = c si (andb b c = orb b c) dans coq?

Question

Je suis nouveau et je COQ essaie de le prouver ...

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

Voici ma preuve, mais je reçois coincé quand je suis à l'objectif (faux = true -> false = true). Je ne suis pas sûr comment je réécrirais cette expression afin que je puisse utiliser la réflexivité. Mais même si je fais cela, je ne suis pas sûr que cela conduira à la preuve.

J'ai été capable de résoudre le prouver si j'ai commencé avec l'hypothèse b = c si. A savoir ...

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. 

Mais je ne peux pas comprendre comment résoudre si je commence avec l'hypothèse qui a des fonctions booléennes.

Answer 1

Vous n'avez pas besoin d'induction, car bool n'est pas une structure de données récursive. Il suffit de passer par les différents cas pour les valeurs de b et c. Utilisez destruct pour ce faire.Dans deux cas l'hypothèse H sera du type true = false, et vous pouvez terminer la preuve avec inversion H. Dans les deux autres cas, l'objectif sera de type true = true et peut être résolu avec 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

Vous devez utiliser la tactique intro. Cela va déplacer false = true dans votre contexte de preuve comme une hypothèse que vous pouvez ensuite utiliser pour réécrire.

Answer 3

Ce n'est peut-être pas le moyen le plus efficace de le faire.

A l'étape induction c. (où il est coincé):

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

Vous pouvez utiliser rewrite et théorèmes de base dans [bool] [1] pour simplifier des termes tels que b && true à b et b || true à true.

Cela peut réduire à deux objectifs sous « triviales »:

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

Ceci est une preuve presque triviale en utilisant assumption, sauf qu'il est un symmetry loin. Vous pouvez try si symmetry leur fera correspondre à l'aide:

try (symmetry;assumption); try assumption. 

(Quelqu'un qui sait vraiment Coq peut me éclairer comment try cette plus succinctement)

Constituer:

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 la seconde approche consiste à le forcer et à utiliser la méthode "table de vérité". Cela signifie que vous pouvez décomposer toutes les variables à leurs valeurs de vérité, et simplifier: destruct b, c; simpl.. Cela donne à nouveau quatre conséquences triviales, jusqu'à un 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 

Putting ensemble:

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. 

La première approche est plus difficile, mais il ne comporte pas énumérer toutes les lignes de table de vérité (I pense).