Comme je sais qu'il y a au moins une personne qui fait du Coq ici, je pose ma question à tout hasard.
Je (re-)débute avec le tutorial de Mike Nahas et j'en suis à essayer de montrer que (forall a b, Is_true (a || b) <-> Is_true a \/ Is_true b) : https://coq.inria.fr/tutorial-nahas#orb_is_or
Pour prouver ce théorème fondamental digne d'une médaille Fields, je commence comme dans le corrigé par montrer la première implication Is_true (a || b) -> Is_true a \/ Is_true b par analyse de cas sur a et sur b.
Mais contrairement au corrigé, je fais d'abord le case sur a et ensuite sur b au lieu de faire les deux à la fois. Le tuto mentionne explicitement cette alternative donc ça ne devrait pas être débile, mais je me retrouve coincé sur le cas a=false, b=false.
Code:
Theorem orb_is_or : (forall a b, Is_true (orb a b) <-> Is_true a \/ Is_true b).
Proof.
intros a b.
unfold iff.
refine (conj _ _).
(* Montrons Is_true (a || b) -> Is_true a \/ Is_true b *)
intros H. (* H : Is_true (a || b) *)
case a.
(* Cas a = true *)
refine (or_introl _).
exact I. (* Terme de gauche vrai *)
(* Cas a = false *)
case b.
(* Cas b = true *)
exact (or_intror I). (* Terme de droite vrai *)
(* Cas b = false : contradiction avec H : Is_true(a || b) *)
simpl in H. (* Je calcule H ?? *)
À ce stade, je me retrouve dans l'état :
Code:
2 subgoals
a, b : bool
H : Is_true (a || b)
______________________________________(1/2)
Is_true false \/ Is_true false
______________________________________(2/2)
Is_true a \/ Is_true b -> Is_true (a || b)
J'ai perdu l'hypothèse que a et b valent false, et du coup je ne peux pas calculer H pour faire apparaître la contradiction, et sans contradiction dans les hypothèses je vais avoir du mal à montrer Is_true false... C'est normal ? Il y a une explication de pourquoi a et b sont remplacés par leur valeur respective dans H quand on les décompose ensemble, mais pas quand on le fait séparément ?