Quand peut-on utiliser l’hypothèse de coinduction ?

Question

Nous pouvons utiliser l’hypothèse d’induction lorsque nous prouvons une propriété d’une structure bien ordonnée.Je suis conscient qu'il existe une preuve pour cela.

En ce qui concerne la coinduction, je suis confus.

Une des réponses à une autre question "Qu’est-ce que la coinduction ?" mentionne qu'il existe une notion de définition corécursive pour être bien formée.

Beaucoup de choses que j'essaie de lire concernant la coinduction parlent principalement de bisimulation et d'équivalence.Mais à ma connaissance, ceux-ci tentent de prouver une relation entre deux structures de données coinductives.Par exemple, ils prouvent que deux flux sont équivalents.Et l'hypothèse coinductive est en quelque sorte dérivée de l'une des hypothèses de bisimulation.Malgré tout, je pense que je suis encore perdu quant aux exigences de ce qui constitue la bonne formation dans le monde coinductif.

Je peux d'une manière ou d'une autre voir que l'hypothèse de coinduction fonctionne pour prouver ce genre de propositions, mais je ne sais toujours pas quand elles peuvent être utilisées pour prouver des propositions plus générales telles que celle mentionnée dans Qu’est-ce que la coinduction ?.Dans ce lien, la proposition déclare que « quelque chose est infini ».Cela semble être une forme de déclaration plus générique que l’on souhaiterait prouver.

Une question éventuellement connexe est de savoir si une proposition peut être convertie et reformulée en tant que proposition d'équivalence ou non.

Existe-t-il un raisonnement informel simple expliquant pourquoi la co-induction fonctionne pour certaines exigences de bonne formation ?

J'espère une explication comme si possible : https://math.stackexchange.com/questions/432293/well-ordering-and-mathematical-induction/432302#432302.

Answer 1

Tout d’abord, permettez-moi de rappeler les points fixes les plus petits et les plus grands pour $\subseteq$.Nous travaillons par rapport à un ensemble $U$, l'univers.Dans le cas des définitions (co)inductives, $U$ est l'ensemble de tous les termes.Une fonction $f:2^U\à2^U$ (à partir de sous-ensembles de $U$ à des sous-ensembles de $U$) est monotone, si $A\subseteq B$ implique toujours $f(A)\subseteq f(B)$.UN un point fixe de $f$ est un ensemble $A$ tel que $f(A)=A$.

Pour monotone $f$ il y a toujours un point le moins fixe $\mu f$, à savoir l'intersection de tous $A\subseteq U$ tel que $f(A)\subseteq A$. Moins signifie que pour des points fixes arbitraires $F$ nous avons toujours $\mu f\subseteq F$.

Pour un exemple, laissez $f_{ t nat}$ être défini par $f_{ t nat}(A)=\{0\}\cup\{n+1\mid n\in A\}$.La fonction $f_{ t nat}$ est la fonction de fermeture en une étape sous les constructeurs $0$ et $+1$.La condition $f_{ t nat}(A)\subseteq A$ signifie que $A$ est fermé sous les constructeurs $0$ et $+1$.L'intersection signifie que le $\mu f_{ t nat}$ contient uniquement les éléments qui sont dans chaque ensemble fermé sous les constructeurs.Ce sont les nombres naturels.L'exemple montre comment la définition inductive des nombres naturels est le point de clôture le moins fixe sous les constructeurs des nombres naturels.Généralement, les ensembles définis inductivement sont les points de fermeture les moins fixes sous les constructeurs.

Dually, pour monotone $f$ il y a aussi un plus grand point fixe $ u f$, à savoir l'union de tous $A\subseteq U$, tel que $f(A)\supseteq A$. Le plus grand signifie que pour des points fixes arbitraires $F$ nous avons toujours $ u f\supseteq F$.Pour compléter la dualité, notons que l'intersection est la $\subseteq$-infimum et union le $\subseteq$-supremum et donc le $\supseteq$-infime.Donc, en fait, les plus grands points fixes pour $\subseteq$ ne sont que des points les moins fixes pour $\supseteq$ et vice versa.(Remarquez également que l’exigence de monotonie est la même pour $\subseteq$ pour ce qui est de $\supseteq$.)

Passons maintenant aux techniques de preuve.Commençons par l’exemple de l’induction sur les nombres naturels.Pour montrer qu'une propriété $P$ est valable pour tous les nombres naturels, nous montrons que $P(0)$ et cela $P(n)$ implique $P(n+1)$.Affichage $P$ comme un sous-ensemble de $U$ (l'ensemble de tous les éléments où réside la propriété), l'obligation de preuve pour l'induction naturelle est que $P$ est fermé sous $f_{ t nat}$.L’exactitude de la technique de preuve de l’induction naturelle découle alors de la définition du moindre point fixe :Si $f_{ t nat}(P)\subseteq P$, alors $P$ fait partie de l'intersection qui forme $\mu f_{ t nat}$, donc la propriété est conservée partout $\mu f_{ t nat}$, c'est $\mu f_{ t nat}\subseteq P$.

L'induction n'est que la généralisation du paragraphe précédent à un ton arbitraire et monotone $f$ au lieu de $f_{ t nat}$.La coinduction est le dual de l'induction :L'obligation de preuve est $f(P)\supseteq P$.Cela signifie que si $P$ tient sur un élément $x$, alors $x$ est construit en utilisant uniquement des éléments de base sur lesquels $P$ tient également.Ainsi, au lieu de montrer que la propriété survit à l’application des constructeurs, il faut montrer qu’elle survit à la déconstruction.Une fois l’obligation de preuve satisfaite, on obtient $ u f\supseteq P$.

A quoi sert la conclusion $ u f\supseteq P$?Reconsidérons $P$ non pas comme une propriété mais comme un sous-ensemble de $U$.La conclusion de la coinduction établit que tous les éléments de $P$ sont des membres bien formés de l'ensemble défini de manière coinductive $ u f$.C'est ce qui se passe dans l'exemple de Qu’est-ce que la coinduction ? montrant forall n, Infinite (from n).Ici, $f$ est la fermeture sous les constructeurs de Infinite (pas de colist!) et $P$ est l'ensemble de tous les termes de la forme from n pour certains n.