(* Well_founded *)

(** %\section{Well--Founded Relations}
Let $\prec$ be a binary relation on a set $A$. The type $Fin({A},\prec)$ 
 is the set of elements $a \in A$ such that
there
is no infinite descending sequence $\{a_n\}_{n\in N}$ verifying 
 \begin{equation}
 \dots a_{n+1} \prec a_n \prec \dots a_2 \prec a_1 \prec a.  \label{chain}
 \end{equation}
 The relation $\prec \subseteq A \times A$ is called noetherian if  
$A=Fin({A},\prec).$


 Furthermore, given $A:Set$ and $\prec \subseteq A \times A,$ the concept of {\em accessibility} can 
 be defined as an inductive
predicate: an element $x \in A$ is accessible if every $y \in A$ such that $y \; \prec
\; x$ is accessible:
\begin{equation}
\boldsymbol{\forall} x:A \bullet \bigl(\boldsymbol{\forall} y:A \bullet x \prec y \Rightarrow (Acc \; \prec \; y)\bigr) \Rightarrow (Acc \; \prec \; x)  \label{acc}
\end{equation}
and the relation $\prec \subseteq A \times A$ is {\em well--founded} if $A=Acc({A},\prec).$ 
% *)

Section generalidades.

Require Arith.

Variables (A:Set) (R:A->A->Prop).

(*Definition Rl:=fun (x:A)=>{y:A | (R y x)}.*)

Print Acc.
Check Acc_intro.
Check Acc_inv. 

 

(**% The well-founded character of a relation can be expressed in different ways:% *)


Definition wfis:=forall (B: A->Set),(forall(x:A),(forall (y:A),(R y x)->(B y))->(B x))->
forall(a:A),(B a).

Definition wfip:=forall (P:A->Prop),(forall (x:A),(forall (y:A),(R y x)->(P y))->(P x))->
forall(a:A),(P a).

(**% that are all equivalent as we will show.
 %*)



Theorem wf_wfis : (well_founded R) ->wfis.
Proof.
unfold wfis.
intros wf family wfp element.
elim (wf element).
intros; auto.
Qed.


Theorem wf_wfip:(well_founded R) -> wfip.
Proof.
intro H.
red in H.
red.
intros.
elim (H a).
intros; auto.
Qed.

Theorem wfip_wf:wfip -> (well_founded R).
Proof.
intro H.
red in H.
red; split; auto.
intros.
apply (H (fun (u:A)=>(Acc R u))).
intros x cla.
split; intros y0 H00.
apply cla.
auto.
Qed.

(**% Now, to prove that $wfis \Rightarrow well\_founded \; R $ we use the well known
projections from the type \verb"sig":% *)

Section proj.

Variable B:A->Prop.
Definition pr1:=fun (H:{z:A|B z})=>let (a,_):= H in a.

Definition pr2:=fun (H:{z:A|B z})=>let (a,p) return (B (pr1 H)) := H in p.


Check pr1.
End proj.

Definition p1:=fun y:A=>(pr1 (fun _:A => (Acc R y))).

Check pr2.
Definition p2:=fun y:A=>(pr2 (fun _:A => (Acc R y))).
Check p2.

(**% Este lema es necesario para poder utilizar la hipotesis \verb"wfis"% *)

Lemma nec : forall(x:A),(forall(y:A),(R y x)
->{a:A|(Acc  R y)})->{a:A|(Acc  R x)}.
Proof.
intros.
split with x.
split.
intros.
apply (p2 y (H y H0)).
Qed.

Theorem wfis_wf :wfis -> (well_founded  R).
Proof.
intro H.
red in H.
red.
intros.
apply (p2 a (H (fun(a:A)=>{z:A | (Acc  R a)}) nec a)).
Qed.


(**%As a curiosity, let us prove
that well--founded relations are not reflexive: %*)
 

Lemma norefl_acc:forall(x:A),(Acc R x)->~(R x x).
Proof.
red.
intros x H.
elim H.
intros x0 H0 H1 H2.
apply (H1 x0); auto.
Qed.

Theorem norefl_Wf:(well_founded R)->forall(a:A),~(R a a).
Proof.
intros wf a.
red in wf.
exact (norefl_acc a (wf a)).
Qed.

(**% Now, let us finally prove that a well--founded relation 
can not have infinite descendent sequences.

First we define what is a chain of elements of \verb"A" (every function from \verb"nat"
to \verb"A")and then what is a descendent chain:%*)



Definition shift:=fun(s:nat->A)=>fun(n:nat)=>(s (S n)).

Lemma shift_triv:forall(s:nat->A),(shift s O)=(s (1)).
Proof.
unfold shift.
auto.
Qed.

(* una cadena descendente es una sucesion tal que forall(i:nat),(R (s i+1) (s (i)))
*)

Definition Desc_chain := fun(s:nat->A)=>forall (i:nat),(R (s (S i)) (s i)).

Definition no_Desc_chain:=fun(a:A)=>forall (s:nat->A),(s O)=a->~(Desc_chain s).

(**% A well--founded relation does not have descendent chains %*)

Lemma wfip_no_Desc_chain:wfip->forall(a:A),(no_Desc_chain a).
Proof.
unfold wfip.
intros H x.
apply (H no_Desc_chain).
intros.
red.
red in H0.
intros.
red; intros.
red in H2.
rewrite <- H1 in H0.
red in H0.
apply (H0 (s (1)) (H2 O) (shift s) ).
simpl.
unfold shift.
auto.

red.
unfold shift.
intro i.
apply H2.
Qed.

(**%\noindent and the existence of a descendent chain implies no well--foundness %*) 

Lemma  Desc_chain_nowf:(exists s:nat->A,(Desc_chain s))->~wfip.
intros.
case H;intros s p.
clear H. 
intro.
assert (forall(a:A),(no_Desc_chain a)).
apply wfip_no_Desc_chain;auto.
Check (H0 (s 0)).
unfold no_Desc_chain in H0.
Print eq.
case (H0 (s 0) s (refl_equal (s 0))).
auto.
Qed.