Download Prouveur interactif - Manuel Utilisateur

148
Prouveur interactif - Manuel Utilisateur
Le but devient :
(nc1-nc2) mod 2 ∈ 1-2. .0 ⇒ nc1-(nc1-nc2)/2-(nc2+(nc1-nc2)/2) ∈ -1. .1
Nous retrouvons le but précédent l’ajout d’hypothèse, sous l’hypothèse voulue. Cette partie de la démonstration a profité à la fois de la règle ajoutée et des fonctionnalités de
preuve automatique, ce qui nous permet de ne pas s’attarder sur les parties démontrables
automatiquement. La zone de ligne de commande contient l’arbre de preuve suivant :
Force(0) &
dd &
dc(nc1-nc2<=0) &
dd &
ah((nc1-nc2) mod 2: 1-2..0) &
ar(IntDiv.4,Once) &
pr &
pr &
pr &
Next
Le mot clef Next indenté directement sous la commande ah indique que le but actuel est
un sous-but produit par cette commande. Rappelons que ah(H) produit deux sous-buts à
partir d’un but B : le sous-but H puis le sous-but H ⇒ B. Nous sommes donc sur ce
deuxième sous-but, en effet Next est le deuxième mot clef indenté sous ah, après ar.
La règle manuelle a servi à fabriquer une nouvelle hypothèse, il s’agit donc d’une sorte
de génération par l’avant. Il aurait été possible de fabriquer une règle forward pour obtenir le même résultat, mais celle-ci serait moins simple. Le procédé utilisant l’ajout d’hypothèse nous permet d’exploiter facilement une règle écrite uniquement en fonction de
considérations mathématiques.
Nous avons introduit l’intervalle de variation du reste, mais le prouveur ne peut pas encore
aboutir sans utiliser la première règle de la théorie IntDiv :
b*(a/b) == a - (a mod b);
Si nous utilisons la commande pr, il est clair que le but courant ne va pas être déchargé. Il
est néanmoins utile que le prouveur simplifie la nouvelle hypothèse et commence la preuve
en simplifiant le but. Pour faire tout ceci sans démarrer des preuves par cas exploratoires,
nous pouvons utiliser pr(Red) :
PRI > pr(Red)
Starting Prover Call
Le but devient :
0 ≤ 1+nc1-nc2-2×((nc1-nc2)/2)