Set Implicit Arguments.
Require Export Omega.

Section recgen. 
Variables (X:Set) (R:X->X->Prop).
Variables (R_wf:(well_founded R)) 
           (Phi:(forall x : X, (forall y : X, R y x -> X) -> X)).
    
Definition genrec:=(well_founded_induction R_wf (fun _:X=>X) Phi).

End recgen.

Section transfer.

Scheme Acc_ind2 := Induction for Acc Sort Prop.

Variables (A : Set) (R : A -> A -> Prop) (R_wf : well_founded R)
  (B : A -> Set) (F : forall x : A, (forall y : A, R y x -> B y) -> B x).


Inductive Trans : A -> A -> Prop :=
  | Tc1 : forall x y : A, R x y -> Trans x y
  | Tc2 : forall x y z : A, R x y -> Trans y z -> Trans x z.

Hint Constructors Trans.

Theorem trans_balance :
 forall x y z : A, R x y -> Trans y z -> exists t : A, Trans x t /\ R t z.
intros x y z H H0; generalize x H; clear H x; elim H0; eauto.
intros x y0 z0 H H1 H2 x0 H3; elim (H2 x); auto.
intros x1 H4; split with x1; elim H4; eauto.
Defined.

Theorem well_founded_ind2 :
 forall P : A -> Prop,
 (forall x : A, (forall y : A, Trans y x -> P y) -> P x) -> forall a : A, P a.

intros P H a; apply H; cut ((forall y : A, Trans y a -> P y) /\ P a).
 intros H0; elim H0; auto.
 elim a using (well_founded_ind R_wf).
   intros x H0; split.
  intros y H1; inversion H1.
   elim (H0 y); auto.
   elim trans_balance with (1 := H2) (2 := H3).
     intros x1 H7; elim H7; intros H8 H9.
     elim (H0 x1); auto.
  apply H; intros y H1; generalize H0; inversion H1.
   intro H5; elim (H5 y); auto.
   elim trans_balance with (1 := H2) (2 := H3).
     intros x1 H6 H7; elim H6; intros H8 H9.
     elim H7 with (y := x1); auto.
Defined.

Theorem is_trans : forall x y z : A, Trans x y -> R y z -> Trans x z.
simple induction 1; eauto.
Defined.

Hint Resolve is_trans.


Theorem
  wf_transfer :
    (forall (x : A) (f' : forall y : A, B y) (g : forall y : A, R y x -> B y),
     (forall (y : A) (h : R y x), g y h = f' y) ->
     F  (fun (y : A) (h : R y x) => g y h) =
     F  (fun (y : A) (_ : R y x) => f' y)) ->
    forall x : A, (well_founded_induction R_wf B F x) = 
    F  (fun (y : A) (h : R y x) => (well_founded_induction R_wf B F y)).

intros H x; elim x using well_founded_ind2;intros x'.
replace (well_founded_induction R_wf B F x') with
(Acc_rec B (fun (x0:A) (_:forall  y:A, R y x0 -> Acc R y) 
(H1: forall y:A, R y x0->B y)=> F H1)  (R_wf x')).
2:auto.
elim (R_wf x') using Acc_ind2;simpl.
intros x'' accesible H_rec_acc H_rec_well_founded.
apply H with
  (g:= fun (y:A) (h: R y x'') => (Acc_rec B
     (fun (x0 : A) (_ : forall y1 : A, R y1 x0 -> Acc R y1)
        (g' : forall y1 : A, R y1 x0 -> B y1) => F  g') (accesible y h))).

intros y h; rewrite H_rec_well_founded;eauto.
Defined.

End transfer.



Section While.

Variable X:Set.
Variable R:X->X->Prop.
Variable P:X->Prop.
Variable r:forall x, {P x}+{~ (P x)}.
Variable f:X->X.
Variable term:forall x:X,(P x)->(R (f x) x).

(* Iteration *)

Fixpoint itern (n:nat):X->X:=
match n with
 0%nat => fun x:X => x
|S m => fun x:X => f (itern m x)
end. 

Lemma iter_iter:forall (n:nat) (x:X), itern (S n) x = f (itern n x).
intuition.
Defined.

Lemma Iter: forall (n:nat) (x:X),itern n (f x) = f (itern n x).
induction n;try auto.
intro x.
rewrite iter_iter.
rewrite (IHn x).
rewrite iter_iter.
auto.
Defined.

 Definition PhiW:forall x:X,(forall y:X,(R y x)->X)->X:=
fun (x : X) (H : forall y : X, R y x -> X) =>
match r x with
| left p => H (f x) (term  p)
| right _ => x
end.

Variable wfR:well_founded R. 

Theorem transfer_hyp: (forall (x : X) (f' : X->X) (g : forall y : X, R y x -> X),
     (forall (y : X) (h : R y x), g y h = f' y) ->
     PhiW  (fun (y : X) (h : R y x) => g y h) =
     PhiW  (fun (y : X) (_ : R y x) => f' y)).
intros;unfold PhiW;case (r x);intros;auto.
Defined.

Theorem balaa: forall (x:X),
genrec  wfR PhiW x = PhiW (fun y:X => fun _:(R y x)=>(genrec  wfR PhiW y)).
unfold genrec.
apply (wf_transfer   wfR (fun _:X=>X) PhiW transfer_hyp).
Defined.

Definition while_do:=fun x:X=>(genrec wfR PhiW x).

Lemma while1:forall (x:X), P x -> while_do x = while_do (f x).
unfold while_do.
intros x p.
rewrite balaa.
unfold PhiW.
case (r x);auto.
intro nop;case (nop p).
Defined.
 
Lemma while2:forall (x:X), ~(P x) -> while_do x = x.
unfold while_do.
intros x nop.
rewrite balaa.
unfold PhiW.
case (r x);auto.
intro p;case (nop p). 
Defined.

Section unicity.
Variable F:X->X.
Variable While1:forall (x:X), P x -> F x = F (f x).
Variable While2:forall (x:X), ~(P x) -> F x = x.

Definition PP:= (fun (a:X)=> while_do a = F a).

Theorem wf_prop:forall (P:X->Prop),
(forall (x:X),(forall (y:X),(R y x)->(P y))->(P x))->forall (a:X),(P a).
Proof.
intros family wfp element.
elim (wfR element).
intros; auto.
Defined.

Theorem unic:forall x:X, (PP x).
Proof.
apply (wf_prop PP).
unfold PP in |- *.
intros.
case (r x).
 intro.
   rewrite while1.
  rewrite While1; auto.
  auto.
 intro; rewrite while2; intros.
  rewrite While2; auto.
  auto.
Qed.

End unicity.

Theorem wf_set:forall (P:X->Set),
(forall (x:X),(forall (y:X),(R y x)->(P y))->(P x))->forall (a:X),(P a).
Proof.
intros family wfp element.
elim (wfR element).
intros; auto.
Defined. 

Theorem while_iter:forall x:X, {n:nat|while_do x=itern n x}.
Proof.
apply (wf_set (fun x:X =>  {n:nat|while_do x=itern n x})). 
intro x.
case (r x);intuition.
rewrite while1;auto.
case (H (f x));intros.
apply term;auto.
rewrite e.
exists (S x0);rewrite iter_iter;intuition.
rewrite Iter.
auto.
rewrite while2;auto.
exists O;intuition;auto.
Defined.

Definition num_iter:X -> nat:= fun (x:X)=>
let (n,_):=(while_iter x) in n.

Theorem comp_num_iter:forall x:X, while_do x = itern (num_iter x) x.
Proof.
intros x.
unfold num_iter.
case (while_iter x).
auto.
Defined.

Lemma appl_fun:forall x:X, forall n m,n=m->itern n x=itern m x.
intros.
rewrite H;trivial.
Defined.

Theorem while_iter_P:forall x:X, forall m,
(forall n,lt n m->P(itern n x))->while_do x=while_do (itern m x).
intros.
induction m.
simpl;trivial.
rewrite IHm.
rewrite while1.
rewrite <- iter_iter.
trivial.
apply H;omega.
intros;apply H.
omega.
Defined.

End While.

Implicit Arguments while_do [X R P].

Require Export ZArith.
Open Scope Z_scope.
Require Export Wf.

Section Define_asn.
Variable Var:Set.

Variable d:forall x y:Var,{x=y}+{~(x=y)}.

Let States:= Var->Z.

Definition update (x:Var) (n:Z) (s:Var->Z) := (fun (y:Var)=> 
                                       if (d x y) then n else (s y)).

Inductive aexp:Set:=
V:Var -> aexp|Num:Z->aexp
|Sum :aexp->aexp->aexp.

Require Export Omega.

Fixpoint sem (s:States) (a:aexp){struct a}:Z:= 
match a with
 V t => (s t)
|Num n => n
|Sum a1 a2 => (sem s a1)+(sem s a2)
end.  

Definition asn (x:Var) (a:aexp) (s:States):= update x (sem s a) s.

Lemma asn1:forall (x:Var) (a:aexp) (s:States), (asn x a s) x = (sem s a).
induction a;unfold asn;unfold update;simpl;case d;auto;intro absurd;case absurd;auto.
Defined.

Lemma asn2:forall (x y:Var) (a:aexp) (s:States), ~(x=y) -> (asn x a s) y = (s y).
induction a;
unfold asn;simpl;
unfold update;
case d;auto;
intros e s H;
case (H e).
Defined.
End Define_asn.

Section Define_comp.

Variables A B C:Set.

Definition comp (f:A->B)  (g:B->C) := fun (a:A)=> g ( f a).
Implicit Arguments comp.
End Define_comp.

Infix ";" := comp (right associativity, at level 60).

Inductive Var:Set:=
v1:Var|v2:Var.

Lemma d:forall x y:Var,{x=y}+{~(x=y)}.
destruct x;destruct y;auto;
right;unfold not;intro H;inversion H.
Defined.

Definition s0 (t:Var):= 
match t with
 v1 => 0
|v2 => 0
end.

Definition States:=Var->Z.
 
Definition f:= (asn d v1 (Sum (V v1) (Num Var 1)));  (asn d v2 (Sum (V v2) (V v1))).

Definition P (n:Z) (s:States):Prop := (s v1) < n.

Definition R (n:Z) (s1 s2:(States)): Prop:=
(0<= n-s2 v1)/\(n-s1 v1)<(n-s2 v1).

Require Import ZArith_dec.
Require Import Zorder.

Lemma one:(forall (n:Z) (x : (States)), {P n x} + {~ P n x}).
intros.
unfold P.
apply Z_lt_dec.
Defined.

Lemma two:forall (n:Z) (x:(States)),(P n x)->(R n (f x) x).
Proof.
intros.
unfold R.
unfold f.
unfold comp.
unfold asn.
simpl.
unfold update.
case d.
 intros.
   inversion e.
 intros.
   simpl.
   split.
  red in H.
    auto with zarith.
  auto with zarith.
Defined.


Require Import Wellfounded.
Require Import Zwf.

Definition g (n:Z) (s:States):Z := n-(s v1).

Lemma three: forall n:Z,well_founded (R n).
intro n.
unfold R.
unfold well_founded.
intro st.
apply (Acc_inverse_image States Z (Zwf 0) (g n)).
apply Zwf_well_founded.
Defined.

Definition prog:= fun z:Z =>  (while_do  (one z) f (@two z) (three z)).


Definition realprog:= fun z:Z => prog z s0 v2.

Lemma k1: (P 0 s0)->False.
unfold P;simpl;intuition.
Qed.

Hint Resolve k1.

Lemma k2:forall n, n<=0 -> ((P n s0)->False).
unfold P;simpl.
intuition.
Defined.

Hint Resolve k2.


Theorem specification_0:forall z:Z, z<=0 -> realprog z=0.
unfold realprog;unfold prog.
intros.
rewrite while2.
simpl;intuition;eauto.
unfold not;intro;eauto.
Defined.


Definition nat2z:nat->Z.
induction 1.
exact 0.
exact (IHnat+1).
Defined.

Lemma nat2z_ge_0:forall n:nat, 0<=nat2z n.
induction n;simpl;omega.
Defined.

Hint Resolve nat2z_ge_0.


Lemma nat2z_pos:forall n:nat,lt 0 n->0<nat2z n.
Proof.
induction n.
intro H;inversion H.
simpl.
intro.
cut (0 <= nat2z n);try omega.
intuition.
Defined.

Lemma nat2z_inj: forall n m : nat, nat2z n = nat2z m -> n = m.
Proof.
induction n; induction m; simpl in |- *;  intuition; auto.
 cut (0 <= nat2z m); try  omega.
    apply nat2z_ge_0.
    cut (0 <= nat2z n); try  omega; apply nat2z_ge_0.
Qed.    

Lemma Nat2Z:forall n,nat2z(n+1)=(nat2z n)+1.
induction n.
simpl.
trivial.
simpl.
rewrite IHn;auto.
Defined.

Lemma nat2z_monotone:forall n m:nat, lt n m->nat2z n<nat2z m.
induction n;induction m.
intros;inversion H.
intros.
simpl.
replace (nat2z m+1) with (nat2z (S m)).
apply nat2z_pos.
trivial.
simpl;trivial.
intros.
inversion H.
intros.
simpl.
intuition.
Defined.

(* Some properties fo f *)

Lemma f2:forall s:States, (f s v1) = (s v1)+1.
intros.
intuition.
Defined.

Lemma f21:forall s:States, (f s v2) = (s v2)+(f s v1).
intros;intuition.
Defined. 

Lemma f1:forall n, f (itern f n s0) v1=(nat2z n)+1.
induction n.
intuition.
simpl.
rewrite f2.
rewrite IHn.
intuition.
Qed.

Lemma f_value:forall n : nat, itern f n s0 v1 = nat2z n.
induction n;  intuition.
rewrite iter_iter.
rewrite f1.
simpl in |- *.
auto.
Qed.

Lemma sfirst:forall n : nat, (n > 0)%nat -> itern f n s0 <> s0.
red in |- *; intros.
cut (itern f n s0 v1 = s0 v1).
intros.
rewrite f_value in H1.
simpl in H1.
cut (nat2z n > 0).
rewrite H1.
omega.
cut (0 < nat2z n).
intuition.
apply nat2z_pos.
omega.
rewrite H0; auto.
Qed.
              
Lemma sL:forall n m : nat, itern f n s0 = itern f m s0 -> n = m.
Proof.
intros.
cut (itern f n s0 v1 = itern f m s0 v1).
   rewrite f_value.
      rewrite f_value.
         intros.
            apply nat2z_inj; auto.
            rewrite H; auto.
Qed.


Lemma f_iter_value_v2:forall n, f (itern f n s0) v2= (itern f n s0 v2)+(nat2z (n+1)).
induction n.
intuition.
simpl.
rewrite f21.
rewrite IHn.
rewrite f2;rewrite f1;rewrite Nat2Z;trivial.
Defined.

Lemma PRED1: forall n m,lt m n->(P (nat2z n) (itern f m s0)).
intros n m H.
red.
rewrite f_value.
apply nat2z_monotone.
auto.
Qed.

Lemma PRED2:forall n:nat,  ~(P (nat2z n) (itern f n s0)).
unfold not.
unfold P.
intro n.
rewrite f_value.
omega.
Qed.


Theorem sPRIN: forall n,(forall n',lt n' n->P (nat2z n) (itern f n' s0))->~P (nat2z n) 
(itern f n s0)
->n=num_iter (P (nat2z n)) (one (nat2z n)) f 
          (two (n:=nat2z n)) (three (nat2z n)) s0.
intros.
 cut ((while_do  (one (nat2z n)) f (@two (nat2z n)) (three (nat2z n)) s0) =
(while_do  (one (nat2z n)) f (@two (nat2z n)) (three (nat2z n)) (itern f n s0))).

intros.
symmetry in H1.
rewrite while2 in H1.
rewrite comp_num_iter in H1.
apply sL.
Focus 2.
apply PRED2;auto.
Focus 2.
eapply while_iter_P.
apply PRED1;auto.
auto.
Defined.

Hint Resolve sPRIN.


Lemma num_iter_value: forall n, 
         n=num_iter (P (nat2z n)) (one (nat2z n)) f 
          (two (n:=nat2z n)) (three (nat2z n)) s0.
Proof.
intros.
apply sPRIN.
apply PRED1.
apply PRED2.
Qed.


Theorem realprog_itern:forall n:nat, realprog (nat2z n)=itern f n s0 v2.
intro n0.
unfold realprog, prog.
rewrite comp_num_iter.
cut (itern f
  (num_iter (P (nat2z n0)) (one (nat2z n0)) f (two (n:=nat2z n0))
     (three (nat2z n0)) s0) s0 = itern f n0 s0 ).
intros.
Focus 2.
apply appl_fun.
symmetry.
apply num_iter_value.
rewrite <- H.
auto.
Qed.

Theorem specification_1:forall n:nat,(realprog (nat2z (S n)))=(realprog (nat2z n))+(nat2z (S n)).
intro n.

rewrite realprog_itern.
rewrite realprog_itern.
rewrite iter_iter.
rewrite f_iter_value_v2.
replace (S n) with (n+1)%nat.
auto.
omega.
Qed.