Différences entre versions de « Commande PreuveDétaillée »

De GeoGebra Manual
Aller à : navigation, rechercher
(à traduire)
 
 
(7 versions intermédiaires par 3 utilisateurs non affichées)
Ligne 1 : Ligne 1 :
<noinclude>{{Manual Page|version=5.0}}</noinclude>{{betamanual|version=5.0}}
+
<noinclude>{{Manual Page|version=6.0}}</noinclude>
{{command|logical}}
+
{{command|logical|PreuveDétaillée}}
{{warning|This GeoGebra command is heavily under construction. Expect to encounter various problems when trying it out. The syntax or the output of this command may be subject to change.}}
 
;ProveDetails[ <Boolean Expression> ]: Returns some details of the result of the automated proof.
 
  
Normally, GeoGebra decides whether a [[Boolean_values|boolean expression]] is true or not by using numerical computations. However, the ProveDetails command uses [[w:Symbolic_computation|symbolic methods]] to determine whether a statement is true or false in general. This command works like the [[Prove_Command|Prove]] command, but also returns some details of the result as a [[Lists|list]]:
+
 
* An empty list '''{}''' if GeoGebra cannot determine the answer.
+
 
* A list with one element: '''{false}''', if the statement is not true in general.
+
;PreuveDétaillée(  <Expression booléenne>  ): Retourne quelques détails sur le résultat d'une preuve automatisée du caractère ''vraie'' ou ''fausse'' en général de l'expression booléenne.
* A list with one element: '''{true}''', if the statement is always true.
+
 
* A list with more elements, containing the boolean value ''true'' and another list for the so-called ''non-degeneracy conditions'', if the statement is true under certain conditions, e.g. {true, {"DegeneratePolygon[A,B,C,D]"}}. This means that if none of the conditions are true, then the statement will be true.
+
Normalement, GeoGebra détermine si une [[Valeurs_booléennes|expression booléenne]] est ''vraie'' ou non numériquement. <br/>La commande <code>PreuveDétaillée</code>, comme le fait la commande <code>Prouver</code> utilise, quant à elle, des méthodes de calcul formel pour déterminer si une affirmation est ''vraie'' ou ''fausse'' en général, mais, en plus du résultat, à la différence de cette dernière, elle retourne quelques détails, sous forme de liste :
{{example| 1=<div>Let us define a triangle with vertices ''A'', ''B'' and ''C'', and define <code><nowiki>D=MidPoint[B,C]</nowiki></code>, <code><nowiki>E=MidPoint[A,C]</nowiki></code>, <code><nowiki>p=Line[A,B]</nowiki></code>, <code><nowiki>q=Line[D,E]</nowiki></code>. Now <code><nowiki>ProveDetails[p∥q]</nowiki></code> returns <nowiki>{true,{"AreEqual[A,B]"}}</nowiki>.This means that if the points ''A'' and ''B'' differ, then the midline ''DE'' of the triangle is parallel to the side ''AB''.</div>}}
+
* Une liste vide '''{}''' si GeoGebra ne peut se prononcer sur la réponse ;
It is possible that the list of the non-degeneracy conditions is not the simplest possible set.
+
* Une liste avec ce seul élément : '''{false}''', si l'assertion n'est pas ''vraie'' dans tous les cas ;
{{Note| See also [[Prove Command|Prove]] command, [[Boolean values|Boolean values]] and [http://dev.geogebra.org/trac/wiki/TheoremProving technical details of the algorithms].}}
+
* Une liste avec ce seul élément : '''{true}''', si l'assertion est  ''vraie'' dans tous les cas (dans tous les cas où le diagramme peut être construit) ;
 +
* Une liste '''{true,{"..."}}'', contenant la valeur booléenne ''true'' et une autre liste pour  les ''conditions non-dégénérées'', si l'assertion est  ''vraie'' sous certaines conditions,<br/>par ex. <nowiki>{true, {"PolygoneDégénéré(A,B,C,D)","SontEgaux(A,B)"}}</nowiki> .<br/> Cela signifie que si aucune de ces conditions n'est vérifiée, alors l'assertion est  ''vraie'' .
 +
 
 +
{{note|La liste apparaît dans la fenêtre Algèbre, non affichée dans Graphique, un clic sur la pastille d'affichage, la fait apparaitre, sous forme de liste déroulante, dans Graphique.}}
 +
 
 +
{{exemples| 1=<div>
 +
Nous définissons un triangle de sommets ''A'', ''B'' et ''C'', et définissons <code><nowiki>D=MilieuCentre(B,C)</nowiki></code>, <code><nowiki>E=MilieuCentre(A,C)</nowiki></code>, <code><nowiki>p=Droite(A,B)</nowiki></code>, <code><nowiki>q=Droite(D,E)</nowiki></code>.
 +
La commande <code><nowiki>PreuveDétaillée(p∥q)</nowiki></code> retourne <nowiki>{true}</nowiki>. Cela signifie que si le diagramme peut être construit, alors la ''droite des milieux'' (DE) du triangle est parallèle au côté <nowiki>[AB]</nowiki>.
 +
 
 +
Soit le segment [AB] appelé ''a'', et son milieu <code><nowiki>C=MilieuCentre(A,B)</nowiki></code>, et sa médiatrice  <code><nowiki>b=Médiatrice(A,B)</nowiki></code>, <code><nowiki>D=Intersection(a,b)</nowiki></code>. <code><nowiki>PreuveDétaillée(C==D)</nowiki></code> retourne <nowiki>{true,{"SontÉgaux(A,B)"}}</nowiki> : ce qui précise que si les points ''A'' et ''B'' sont différents, alors les points ''C'' et ''D'' sont confondus.
 +
 
 +
Soit le segment [AB]  appelé ''f'', un point ''C'' quelconque de la droite (AB), et soit <code><nowiki>g=Segment(B, C)</nowiki></code> et <code><nowiki>h=Segment(A, C)</nowiki></code>, <code><nowiki>PreuveDétaillée(f==g+h)</nowiki></code> retourne <nowiki> {true, {"f+h=g", "h=g+f"}} </nowiki> : ce qui précise que si  ni <math>f+h=g</math>, ni <math>h=g+f</math>, alors <math>f=g+h</math>
 +
 
 +
Nous définissons un quadrilatère de sommets ''A'', ''B'', ''C''et ''D'', et définissons les milieux ''E'', ''F'', ''G'' et ''H'' de ses côtés, puis <code><nowiki>f=Segment(E, F)</nowiki></code> et <code><nowiki>g=Segment(G, H)</nowiki></code> <br/>
 +
La commande <code><nowiki>PreuveDétaillée(SontÉgaux(f,g))</nowiki></code> retourne la liste <nowiki>{true} </nowiki>.
 +
</div>}}
 +
 
 +
 
 +
 
 +
 
 +
{{note|1=<div>--[[Utilisateur:Noel Lambert|Noel Lambert]]
 +
Je rappelle que cette commande en est à ses balbutiements !
 +
La propriété devrait aussi être annoncée comme ''vraie'' pour un quadrilatère dégénéré en triangle, si A et B sont confondus, alors leur milieu E existe et est confondu avec eux, le segment [EH] = [AH]  est de même longueur que [FG] (propriété métrique du "segment des milieux") !
 +
Surtout que, si au lieu de l'égalité de longueur, on demande s'il y a parallélisme, la commande <code><nowiki>PreuveDétaillée(SontParallèles(Droite(F,G),Droite(E,H)))</nowiki></code>, elle, retourne {true}, sans cas particulier ? Or, en cas de polygone dégénéré par une superposition des points B et D, les droites citées ne sont pas définies !</div>}}
 +
 
 +
 
 +
 
 +
{{Note| Voir aussi la commande [[commande Prouver|Prouver]], la page [[Valeurs booléennes]] et pour les curieux, la page (en anglais) sur les  [http://dev.geogebra.org/trac/wiki/TheoremProving détails techniques des algorithmes].}}

Version actuelle datée du 8 octobre 2017 à 22:05



PreuveDétaillée( <Expression booléenne> )
Retourne quelques détails sur le résultat d'une preuve automatisée du caractère vraie ou fausse en général de l'expression booléenne.

Normalement, GeoGebra détermine si une expression booléenne est vraie ou non numériquement.
La commande PreuveDétaillée, comme le fait la commande Prouver utilise, quant à elle, des méthodes de calcul formel pour déterminer si une affirmation est vraie ou fausse en général, mais, en plus du résultat, à la différence de cette dernière, elle retourne quelques détails, sous forme de liste :

  • Une liste vide {} si GeoGebra ne peut se prononcer sur la réponse ;
  • Une liste avec ce seul élément : {false}, si l'assertion n'est pas vraie dans tous les cas ;
  • Une liste avec ce seul élément : {true}, si l'assertion est vraie dans tous les cas (dans tous les cas où le diagramme peut être construit) ;
  • Une liste '{true,{"..."}}, contenant la valeur booléenne true et une autre liste pour les conditions non-dégénérées, si l'assertion est vraie sous certaines conditions,
    par ex. {true, {"PolygoneDégénéré(A,B,C,D)","SontEgaux(A,B)"}} .
    Cela signifie que si aucune de ces conditions n'est vérifiée, alors l'assertion est vraie .
Note : La liste apparaît dans la fenêtre Algèbre, non affichée dans Graphique, un clic sur la pastille d'affichage, la fait apparaitre, sous forme de liste déroulante, dans Graphique.
Exemples :

Nous définissons un triangle de sommets A, B et C, et définissons D=MilieuCentre(B,C), E=MilieuCentre(A,C), p=Droite(A,B), q=Droite(D,E). La commande PreuveDétaillée(p∥q) retourne {true}. Cela signifie que si le diagramme peut être construit, alors la droite des milieux (DE) du triangle est parallèle au côté [AB].

Soit le segment [AB] appelé a, et son milieu C=MilieuCentre(A,B), et sa médiatrice b=Médiatrice(A,B), D=Intersection(a,b). PreuveDétaillée(C==D) retourne {true,{"SontÉgaux(A,B)"}} : ce qui précise que si les points A et B sont différents, alors les points C et D sont confondus.

Soit le segment [AB] appelé f, un point C quelconque de la droite (AB), et soit g=Segment(B, C) et h=Segment(A, C), PreuveDétaillée(f==g+h) retourne {true, {"f+h=g", "h=g+f"}} : ce qui précise que si ni f+h=g, ni h=g+f, alors f=g+h

Nous définissons un quadrilatère de sommets A, B, Cet D, et définissons les milieux E, F, G et H de ses côtés, puis f=Segment(E, F) et g=Segment(G, H)
La commande PreuveDétaillée(SontÉgaux(f,g)) retourne la liste {true} .



Note :
--Noel Lambert

Je rappelle que cette commande en est à ses balbutiements ! La propriété devrait aussi être annoncée comme vraie pour un quadrilatère dégénéré en triangle, si A et B sont confondus, alors leur milieu E existe et est confondu avec eux, le segment [EH] = [AH] est de même longueur que [FG] (propriété métrique du "segment des milieux") !

Surtout que, si au lieu de l'égalité de longueur, on demande s'il y a parallélisme, la commande PreuveDétaillée(SontParallèles(Droite(F,G),Droite(E,H))), elle, retourne {true}, sans cas particulier ? Or, en cas de polygone dégénéré par une superposition des points B et D, les droites citées ne sont pas définies !


Note : Voir aussi la commande Prouver, la page Valeurs booléennes et pour les curieux, la page (en anglais) sur les détails techniques des algorithmes.
© 2024 International GeoGebra Institute