Proof on booleans, false = true

Question

Je suis actuellement au chapitre 5 de "Fondations logicielles" mais j'ai ressenti le besoin de revenir au chapitre un pour clarifier un certain nombre de choses. En particulier, il y a un exercice que je n'ai pas vraiment digéré, dans lequel on nous demande d'utiliser destruct deux fois pour prouver un résultat sur des booléens. Ici c'est avec les noms et autres détails changés.

Inductive bool: Type := 
|true: bool 
|false: bool. 

Definition fb (b1:bool) (b2:bool) : bool := 
match b1, b2 with 
| false, false => false 
| _, _ => true 
end. 

Theorem th: forall a b: bool, 
    fb a b = false -> b = false. 
Proof. 
intros [] [] H. 
- rewrite <- H. reflexivity. 
- reflexivity. 
- rewrite <- H. reflexivity. 
- reflexivity. 
Qed. 

Quand la première tique, le contexte et l'objectif sont à la fois un non-sens:

H : fb true true = false 
______________________________________(1/1) 
true = false 

deuxième cocher l'hypothèse est fausse. Troisième tick est le même genre de non-sens que le premier. Je ne comprends que par les règles de réécriture, toutes ces choses fonctionnent. Cependant j'ai l'impression que nous quittons l'étroit chemin de la vérité pour le désert de la fausseté. Plus précisément, et AFAIK, une fausse hypothèse peut être faite pour prouver TOUT énoncé, vrai ou faux. Ici, nous l'utilisons pour prouver que false = true, OK pourquoi pas, mais cela me rend un peu mal à l'aise. Je n'aurais pas prévu un assistant de preuve pour permettre cela.

Développant un peu

Dans une preuve typique par la contradiction, je choisirais une hypothèse au hasard, et d'en tirer le but jusqu'à ce que je trouve soit une tautologie ou une contradiction. Je conclurais alors si mon hypothèse était vraie ou fausse.

Qu'est-ce qui se passe ici, dans les cas 1 (même pour le cas 3), Coq commence à partir d'une hypothèse fausse:

H : fb true true = false 

applique à un objectif qui est une contradiction:

true = false 

et les combine pour trouver une tautologie.

Ce n'est pas un raisonnement dont je suis conscient. Cela rappelle les «blagues» des étudiants où, à partir de 0 = 1, tout résultat absurde sur les nombres naturels peut être prouvé.

Followup

Ce matin, pendant mon trajet, je pensais à ce que je venais d'écrire ci-dessus. Je crois maintenant que les cas 1 et 3 sont des preuves appropriées par contradiction. En effet H est faux et nous l'utilisons pour prouver un but qui est faux. Les hypothèses (valeurs de a et b) doivent être rejetées. Ce qui m'a peut-être troublé, c'est qu'en utilisant la réécriture, nous faisons une partie du chemin "en arrière", en partant du but.

Je suis un peu indécis pour le cas 2, qui se lit comme suit:

H : fb true false = false 
______________________________________(1/1) 
false = false 

qui est essentiellement false -> true, une tautologie sous le « principe d'explosion ». Je ne pense pas que cela pourrait être utilisé directement dans une preuve. Oh, je ne suis pas sûr d'avoir bien compris ce qu'il y a sous le capot, mais la confiance en Coq est intacte. Je dois continuer et revenir au chapitre 5. Merci à tous pour vos commentaires.

Answer 1

Tout d'abord, merci de fournir un code autonome.

Je comprends votre inquiétude prouvant un but en utilisant rewrite quand vous savez que ce que vous devriez vraiment faire est de dériver une contradiction des hypothèses. Cela ne rend cependant pas le raisonnement incorrect. Il est vrai que sous de telles hypothèses, vous pouvez prouver ce but.

Cependant, je pense aussi que cela ne rend pas le script de preuve vraiment lisible. Dans votre exemple, vous considérez tous les cas possibles et il arrive que trois sur quatre soient impossibles. Quand nous lisons votre preuve, nous ne pouvons pas voir cela. Pour préciser que vous êtes dans un cas impossible, il y a quelques tactiques qui sont utiles pour dire "regardez, je vais maintenant prouver une contradiction pour exclure cette affaire".

L'un d'entre eux est exfalso. Il remplacera l'objectif actuel par False (puisque tout peut être dérivé de False, comme mentionné par @ejgallego dans un commentaire).

Un deuxième est absurd pour dire "Je vais maintenant prouver une déclaration et sa négation" (ceci est fondamentalement équivalent à prouver Faux). Un troisième qui est suffisant dans votre cas est discriminate. Il essaie de trouver dans les hypothèses une égalité contradictoire, telle que true = false.

Theorem th: forall a b: bool, 
    fb a b = false -> b = false. 
Proof. 
    intros [] [] H. 
    - discriminate. 
    - discriminate. 
    - discriminate. 
    - reflexivity. 
Qed. 

---

Maintenant, si vous le savez, discriminate et reflexivity sont tous deux jugés par la tactique easy. Ainsi, la preuve suivante fonctionne aussi bien (mais il ne montre pas ce qui se passe et tombe donc hors de portée de cette question):

Theorem th: forall a b: bool, 
    fb a b = false -> b = false. 
Proof. 
    intros [] [] H; easy. 
Qed. 

ce qui est du sucre syntaxique pour la même épreuve:

Theorem th: forall a b: bool, 
    fb a b = false -> b = false. 
Proof. 
    now intros [] [] H. 
Qed.