Commit 7541c956 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Redaction de la bonne fondaison de subterm_acc par l'absurde

parent 09bb37e7
......@@ -32,40 +32,57 @@
\end{defi}
\begin{lem}\label{lem-subacc-wf}
$\surterm_{acc}$ is well-founded on $\mbb{U}$.
There is no infinite sequence $(t_i)_{i\in\N}$ such that $t_0\in\mbb{U}$ and for all $i\in\N$, $t_i\surterm_{acc}t_{i+1}$.
\end{lem}
\begin{proof}
Let $f\,\bar u\in\mbb{U}$.
We want to show there is no infinite sequence $(t_i)_{i\in\N}$ such that $t_0=f\,\bar u$ and for all $i\in\N$, $t_i\surterm_{acc}t_{i+1}$.
Let us assume that there is such an infinite sequence.
First note that every $t_i$ is headed by an element of $\CObj$, otherwise there is no $t$ such that $t_i\surterm_{acc}t$.
Hence, among every infinite sequence,
let us choose one such that $t_0=f\,\bar u$
where $\tau(f)=\Pi\overline{(x:T)}.C\,\bar v$
and for all $C'\prec C$, there is no infinite sequence starting by a constructor of $C'$.
We will prove that for every $i$, $t_i=t'_i\,\bar v$
where $t'_0=t_0$, for all $i$, $t'_i\surterm t'_{i+1}$ and $t'_i$ is headed by a constructor of a type equivalent to $C$.
Let $i$ be such that $t_i$ has this property.
Hence $t_i=t'_i\,\bar v$.
Since $t_i$ is headed by a constructor,
$t'_i$ too, $t'_i=c\,\bar u$.
Since $t'_i\,\bar v\surterm_{acc}t_{i+1}$, two options:
\begin{itemize}
\item
If $f\notin\CObj$, then there is no $t$ such that $f\,\bar u\surterm_{acc}t$.
\item
So, let us consider $f\in\CObj$.
Then $\tau(f)=\Pi\overline{(x:T)}.C\,\bar v$.
By induction on $\succ$,
let's assume that for all $C'\prec C$,
for all terms headed by a constructor of $C'$,
there is no infinite sequence with the expected property.
There is a $j\in\Acc(f)$ such that $t_1=u_j\,\bar w$.
$u_j\in\interp{T_j}$, hence:
\begin{itemize}
\item
if $T_j$ is not a product and $u_j$ is headed by a constructor,
the constructor is fully applied, so $\valabs{\bar w}=0$.
\item
if $T_j$ is a product,
then by definition of accessibility, $T_j\in\Froz_{\<C}$.
So all the element of $\bar w$ headed by a constructor
are headed by a constructor of a type constant $C'\prec C$.
So if we choose to access an element of $\bar w$ we can apply the induction hypothesis on $\prec$.
\end{itemize}
We see that $\surterm_{acc}$ is well-founded on $\mbb{U}$
because $\surterm$ is well-founded and we can access finitely many invented terms, by well-foundedness of $\succ$.
\qedhere
\item
if $t_{i+1}=u_j\,\bar x$, then $u_j\subterm t'_{i}$ hence there is a $t'_{i+1}$ (namely $u_j$) such that $t_{i+1}=t'_{i+1}\,\bar x$ such that $t'_i\surterm t'_{i+1}$.
By definition of accessibility, if $\tau(c)=\Pi\overline{(x:T)}.C'\,\bar w$ with $C'\sim C$,
$T_j\in\Froz_{\<C}$.
In particular, $T_j=\Pi\overline{(y:V)}.C''\,\bar u'$,
with $C''\preceq C$.
Hence $u_j$ is headed by a constructor of $C''$.
\begin{itemize}
\item
If $C''\sim C$, we can conclude the induction,
\item
If $C''\prec C$, the minimality hypothesis is violated.
\end{itemize}
\item
if $t_{i+1}=v_j\,\bar x$, then we contradict the minimality hypothesis.
Indeed, $t_{i-1}=c_{i-1}\,\bar w$, with $c_{i-1}\in\CObj$,
$\tau(c_{i-1})=\Pi\overline{(x:T)}.C_{i-1}\,\bar u'$
and $C_{i-1}\sim C$.
Hence, for all $r\in\Acc(c_{i-1})$,
$T_r=\Pi\overline{(x:U)}.V$ where all $U_k$ are product ended by a $D_k\,\bar v'$ with $D_k\in\CTyp$ and $D_k\prec C$.
Hence, there is a $r$ such that $t'_i=w_r$ and $t_i=t'_i\,\bar v$ and for all $k$, $v_k\in\interp{U_k}$.
So, if $v_j$ is headed by a constructor,
this constructor is one of $D_k$ which violates the minimality property.
\end{itemize}
Hence the existence of such an infinite sequence leads to the existence of an infinite sequence of subterms of $t_0$,
contradicting the well-foundedness of $\subterm$.
\end{proof}
\begin{lem}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment