tex
	title = "Proof of Dickson lemma"
	author = "Christophe Raffalli\\footnote{email: raffalli@univ-savoie.fr}
\\footnote{address: Laboratoire de Math\\'ematique, Universit\\'e de Savoie, 73376 Le Bourget-du-Lac cedex (FRANCE)}"
        institute = "LAMA, Savoie University"
	documents = math
.
flag auto_lvl 1.
flag tex_lisp_app false.
flag tex_type_sugar true.
flag tex_infix_sugar true.
flag tex_indent 60.

(* flag tex_type_sugar false. *)

Import nat.

Import set.

tex_syntax N Prefix "\\NN" ! "[" ! x ! "]".
tex_syntax $<< Infix[5] A "\\subset" B.
tex_syntax $=> Infix[9] A ! "\\mapsto" ! B.

def Minima Q f x = Q x & /\y:N (Q y -> f x <= f y).
tex_syntax Minima Prefix "\\hbox{Min}" ! "[" ! Q ! "," f ! "," x  ! "]".

goal /\Q << N /\f:(N => N) (\/x:N Q x -> \/x:N (Minima Q f x)).
(*!math
\begin{lemma}\label{lemone}
We define the predicate \[Minima Q f x\] by
$$ 
\[Minima Q f x\] = \[$$Minima Q f x\]
$$ 
which means that \[x\] is a minimum of \[f\] on the subset \[Q\] of \[N\]. Then, we can prove the minimum principle:
$$
\[ $0 \] $$
\end{lemma}

\begin{proof}
The proof uses absurdity reasoning and the well founded induction principle on \[N\]. \qed
\end{proof} 
*)
intros.
lefts H1 $& $\/.
by_absurd.
elim False.
prove /\x:N (Q x -> \/y (N y & Q y & f y < f x)).
intros.
by_absurd.
elim H3.
intros.
intro.
axiom H4.
intros.
intros.
by_absurd.
elim H6.
intros.
intros.
axiom H7.
axiom H8.
elim not.lesseq.imply.less.N;; trivial.
rmh H3.
prove /\y:N /\x:N (y = f x -> Q x -> False).
intro 2.
elim well_founded.N with H3.
select 2.
trivial.
intros.
apply G with H8.
lefts G0 $& $\/.
apply H5 with H11.
trivial.
elim G0 with H10.
intro.
save lem1.

def LeftMinima Q f x = Q x & /\y:N (Q y -> x < y -> f x <= f y).  
def Unbounded Q = /\x:N \/y:N (x <= y & Q y).
tex_syntax LeftMinima Prefix "\\hbox{LMin}" ! "[" ! Q ! "," f ! "," x  ! "]".
tex_syntax Unbounded Prefix "\\hbox{Ub}" ! "[" ! Q ! "]".

goal /\Q << N /\f:(N => N) (Unbounded Q -> Unbounded (\x (LeftMinima Q f x))).
(*!math
\begin{lemma}\label{lemtwo}
Now, we define the following predicates :
$$
\begin{array}{lcl}
\[ Unbounded Q \] & = & \[ $$Unbounded Q \]  \cr
\[ LeftMinima Q f x \] & = & \[ $$LeftMinima Q f x\]
\end{array}
$$
\[ Unbounded Q \] means that $Q$ is unbounded and \[ LeftMinima Q f x \] means that $x$ is a left minimum of $f$ on $Q$.
Then, we prove 
$$
\[ $0 \]
$$
\end{lemma}
*)
intros.
intros.
local R y = x <= y & Q y.
(*!math
\begin{proof}
Immediate from the previous lemma because  \[ LeftMinima Q f x\] means 
 \[ Minima $$R f x\]. \qed
\end{proof}

*)
prove \/y:N R y.
apply H1 with H2.
trivial.
apply lem1 with H0 and G.
trivial.
lefts G0 $& $\/.
rename x0 y.
unfold_hyp H4 Minima.
lefts H4.
lefts H4.
intros $& $\/.
axiom H3.
axiom H4.
intros.
intros.
elim H5.
trivial.
save lem2.

Import list.

tex_syntax List Prefix "\\LL" ! "_{" ! D ! "}[" ! x ! "]".
tex_syntax Forall  Prefix "\\forall" \D\ ! "\\in" ! l D %as $Forall D l.
  
goal /\l:(List (N => N)) /\Q << N (Unbounded Q -> \/Q'<<Q (Unbounded Q' & /\x,y:Q' (x < y -> Forall (\f (f x <= f y)) l))).
(*!math
\begin{proof}[of Dickson's lemma]
We can now formalize Dickson's lemma as
$$
\[[ $0 \]]
$$
which is proved by induction on the length of the list $l$ using the previous lemma: we get an unbounded set $Q$ such that any point of $Q$ is a left minimum on $Q$ for all functions in the list which is what we wanted. \qed
\end{proof}
*)
intro 2.
elim H.
trivial.
rename a f.
intros.
apply H2 with H3 and H4.
lefts G $& $\/.
apply lem2 with f and H6.
trivial.
intros.
intros.
select 2.
axiom G.
trivial.
intros.
intro.
elim H8.
trivial.
trivial.
elim H7.
trivial.
trivial.
save lem3.

Import list_nat.

Inductive Good l R = 
  zero : Good nil R
| un   : /\i:N (Good (i::nil) R)
| succ : /\i,j:N /\l:(List N) (Good (j::l) R -> R i j -> Good (i::j::l) R).
  
tex_syntax Good Prefix "\\hbox{Decreasing}" ! "[" ! R ! "," l ! "]" %as $Good l R.
 
def Rl i j l_f = i > j & Forall \f (f i >= f j) l_f.
tex_syntax Rl Prefix "\\hbox{R}" ! "_{" ! l_f ! "}[" ! i ! "," j ! "]" %as $Rl i j l_f.

def Spec l_f l li = length li = l & Good li (\i \j (Rl i j l_f)).
tex_syntax Spec Prefix "\\hbox{S}" ! "[" ! l_f ! "," l ! "," li ! "]".

goal /\l_f:(List (N => N)) /\p:N \/l:(List N) (Spec l_f p l).
(*!math 

\begin{proof}[of weak Dickson's lemma]
To prove Dickson's lemma we need to manipulate finite sets of naturals. We formalize finite sets as ordered lists. Then, the specification uses the following definitions:
$$
\begin{array}{lcl}
\[ Good l R \]  && \hbox{ means that $l$ is ordered for $R$ (defined by induction)} \cr
\[ Rl i j l_f \] & = & \[ $$Rl i j l_f\] \hbox{ (the relation used to sort list)} \cr
\[ Spec l_f p l \] & = & \[ $$Spec l_f p l \].
\end{array}
$$
The weak Dickson's lemma is stated as 
$$\[ $0 \]$$
and it is an immediate consequence of the previous lemma (by induction on the integer $p$) and
*)
intros.
elim lem3 with H and N.
trivial.
intros.
intros.
instance ?1 x.
trivial.
use \/l:(List Q') Spec l_f p l.
trivial =G.
elim H0.
trivial =.
lefts H3 $& $\/.
rename y l.
lefts H1 $& $\/.
elim H3 with [case].
apply H5 with N N0.
trivial =.
lefts G $& $\/.
intros.
instance ?2 y::nil.
trivial =H10 H9 H8 H7 H4.
lefts H7 $& $\/.
apply H5 with N (S d).
trivial = H1 H7.
lefts G $& $\/.
intros.
instance ?3 (y::l).
trivial.
save dickson.


goal /\x,y:N (x <= y or ~ x <= y).
intro 2.
elim H.
trivial.
intros.
elim H2.
trivial.
apply H1 with H3.
left G.
intro r.
trivial.
intro l.
trivial.
save lesseq_dec.

goal /\x,y:N (x < y or ~ x < y).
intro 2.
elim H.
intros.
elim H0 with [case].
trivial.
trivial.
intros.
elim H2.
trivial.
apply H1 with H3.
left G.
intro r.
trivial.
intro l.
trivial.
save less_dec.

goal /\x,y:N (x = y or ~ x = y).
intro 2.
elim H.
intros.
elim H0 with [case].
trivial.
trivial.
intros.
elim H2.
trivial.
apply H1 with H3.
left G.
intro r.
trivial.
intro l.
trivial.
save eq_dec.

goal /\X /\Q (/\x:X (Q x or ~ Q x) -> /\l:(List X) (Forall Q l or ~ Forall Q l)). 
intros.
elim H0.
trivial.
left H3.
trivial.
apply H with H1.
left G.
trivial.
trivial.
save forall_dec.


goal /\l_f:(List (N => N)) /\l:N /\li:(List N) (Spec l_f l li or ~ Spec l_f l li).
(*!math
\end{proof}

\begin{proof}[decidability of the specification] It is stated as follows and it is easy (but long and tedious) to prove in intuitionistic logic.
$$
\[ $0 \] \
$$\qed
\end{proof}
*)
intros.
elim /\l:N (Spec l_f l li or ~ Spec l_f l li).
elim H1.
intros.
elim H2 with [case].
intro l.
trivial.
intro r.
trivial.
intros.
elim H5 with [case].
intro r.
trivial.
apply H4 with H6.
left G.
intro r.
intro.
elim H8.
lefts H9.
intros.
trivial.
elim H10 with [case] ;; trivial.
elim H3 with [case].
intro l. trivial.
lefts H9 $& $\/.
elim less_dec with N d then N a.
local Q f = f d <= f a.
elim forall_dec with N => N then Q.
intros.
elim lesseq_dec.
trivial.
trivial.
axiom H.
intro l.
trivial.
intro r.
intro.
lefts H14.
elim H15 with [case] ;; trivial.
intro r.
intro.
lefts H13.
elim H14 with [case] ;; trivial.
save Spec_dec.

depend lesseq_dec.

depend Spec_dec.