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'< 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.