Require Export tactics.

Require Import Wf_nat.
Load param.

(* Definition of a loop *)

Section Loop.
 Variable A : Set.
 Variable body : A -> (bool * A).

 Inductive loop_prop : A -> A -> Prop :=
 | loop_prop_interrupt : forall a a',
   body a = (false, a') -> loop_prop a a'
 | loop_prop_continue : forall a a' a'',
   body a = (true, a') -> loop_prop a' a'' -> loop_prop a a''.

 Lemma loop_functional : forall a a',
 loop_prop a a' -> forall a'', loop_prop a a'' -> a' = a''.

 Proof.
  induction 1 as [| ? ? ? ? loop ]; induction 1 as [| ? ? ? ? loop'].
  congruence.
  discr.
  discr.
  apply IHloop.
  congruence.
 Qed.

 Inductive loop_term : A -> Prop :=
 | loop_term_interrupt : forall a a',
   body a = (false, a') -> loop_term a
 | loop_term_continue : forall a a',
   body a = (true, a') -> loop_term a' -> loop_term a.

 Hint Constructors loop_prop loop_term.

 Definition loop : forall a, loop_term a ->
 {a' | loop_prop a a'}.
 
 Proof.
  refine (fix f a (h : loop_term a) := 
   let k := body a in
   (match k as k0 return k = k0 -> _ with
    | (true, a') => fun h0 =>
      match f a' _ with
      | _ => _
      end
    | (false, a') => fun h0 => exist _ a' _
    end) (refl_equal _)
  ) ; subst.
  destruct (f a') as [ a'' Ha''] .
   induction h as [? ? H|? ? H].
   rewrite h0 in H ; discriminate.
   rewrite h0 in H ; injection H ; intros ; subst ; auto.
   exists a''.
   apply loop_prop_continue with a' ; auto.
  apply loop_prop_interrupt ; auto.
 Defined.

 Lemma loop_terminates : forall a a', loop_prop a a' -> loop_term a.
 
 Proof.
 induction 1 ; eauto.
 Qed.

 Corollary loop_dec : forall a, (exists a', loop_prop a a') -> {a'0 | loop_prop a a'0}.
 Proof.
 intros.
 apply loop.
 inversion H.
 eapply loop_terminates.
 eassumption.
 Defined.

Section Loop_term_weight.
 
 Hypothesis weight_wf_ex : exists weight : A -> nat, forall a a', body a = (true, a') -> weight a' < weight a.

 Theorem loop_terminates_weight : forall a, loop_term a.

 Proof.
 inversion weight_wf_ex as [weight weight_wf].
  apply  (@well_founded_ind _ _ (well_founded_ltof _ (weight))).
  intro x.
  case_eq (body x).
  intros b a Hba Hx.
  destruct b.
  apply loop_term_continue with a ; auto.
  apply Hx.
  unfold ltof.
  apply weight_wf.
  auto.
  apply loop_term_interrupt with a ; auto.
 Qed.

 Definition loop_weight a := loop (loop_terminates_weight a).

End Loop_term_weight.

Section Loop_part.

Inductive loop_part : A -> bool -> A -> Prop :=
| loop_part_step : forall a b c, body a = (b, c) -> loop_part a b c
| loop_part_loop : forall a a' b c, body a = (true, a') -> loop_part a' b c -> loop_part a b c.

Theorem loop_prop_loop_part : forall a c, loop_prop a c -> loop_part a false c.
Proof.
induction 1.
 eapply loop_part_step.
 assumption.
eapply loop_part_loop.
 eassumption.
assumption.
Qed.

Theorem loop_part_loop_prop : forall a b c, loop_part a b c -> b = false -> loop_prop a c.
Proof.
induction 1.
 intros ? ; subst.
 eapply loop_prop_interrupt.
 assumption.
intros ? ; subst.
eapply loop_prop_continue.
 eassumption.
eauto.
Qed.

Corollary loop_part_false_func : forall a c c', loop_part a false c -> loop_part a false c' -> c = c'.
Proof.
intros.
eapply loop_functional;
 eapply loop_part_loop_prop; eauto.
Qed.

Theorem loop_part_chain : forall a b' a', loop_part a b' a' -> b' = true -> forall b c, loop_part a' b c -> loop_part a b c.
Proof.
induction 1.
intro ; subst.
intros; eapply loop_part_loop.
  eassumption.
 assumption.
intro ; subst.
intros.
eapply loop_part_loop.
 eassumption.
eauto.
Qed.


End Loop_part.

End Loop.

Section General_loops.

Variable A : Set.
Variable p : A -> bool -> A -> Prop.

Inductive genloop_prop : A -> A -> Prop :=
| genloop_prop_interrupt : forall a a',
  p a false a' ->genloop_prop a a'
| genloop_prop_continue : forall a a' a'',
  p a true a' -> genloop_prop a' a'' -> genloop_prop a a''.


Inductive genloop_term : A -> Prop :=
| genloop_term_interrupt : forall a a',
  p a false a' ->genloop_term a
| genloop_term_continue : forall a a',
  p a true a' -> genloop_term a' -> genloop_term a.

Hint Constructors genloop_prop genloop_term.

Lemma genloop_terminates : forall a a', genloop_prop a a' -> genloop_term a.
Proof.
induction 1; eauto.
Qed.

Lemma genloop_p : forall a, genloop_term a -> exists b, exists c, p a b c.
Proof.
induction 1; repeat eapply ex_intro; eauto.
Qed.

Lemma genloop_term_prop : forall a, genloop_term a -> exists a', genloop_prop a a'.
Proof.
induction 1; try inversion IHgenloop_term ; eapply ex_intro; eauto.
Qed.

Hypothesis p_functional_bool : forall a b c, p a b c -> forall b' c', p a b' c' -> b = b'.
Hypothesis p_functional_A : forall a b c, p a b c -> forall b' c', p a b' c' -> c = c'.

Lemma genloop_functional : forall a a',
genloop_prop a a' -> forall a'', genloop_prop a a'' -> a' = a''.
Proof.
induction 1.
 inversion 1. 
  subst.
  eapply p_functional_A; eauto.
 subst.
 generalize (p_functional_bool H H1).
 discriminate 1.
inversion 1.
 subst.
 generalize (p_functional_bool H H2).
 discriminate 1.
subst.
generalize (p_functional_A H H2).
intros.
subst.
eapply IHgenloop_prop.
assumption.
Qed.

Hypothesis p_dec : forall a, (exists b, exists c, p a b c) -> {b' : _ & {c' | p a b' c'}}.

Definition genloop : forall a, genloop_term a ->
 {a' | genloop_prop a a'}.
 
 Proof.
  refine (fix f a (h : genloop_term a) := 
    match p_dec (genloop_p h) with
    | existT true (exist a' Ha') => 
      match f a' _ with
      | exist a'' Ha'' => _
      end
    | existT false (exist a' Ha') => exist _ a' _
    end) ; subst.
 destruct s.
 destruct s0.
 destruct h.
 generalize (p_functional_bool Ha' H).
 discriminate 1.
 generalize (p_functional_A Ha' H).
 intro.
 rewrite H0.
 assumption. (* OK ! *)
 exists a''.
 eapply genloop_prop_continue.
  eassumption.
 assumption.
 eapply genloop_prop_interrupt.
 assumption.
Defined.

Corollary genloop_dec : forall a, (exists a', genloop_prop a a') -> {a' | genloop_prop a a'}.
intros.
apply genloop.
inversion H.
eapply genloop_terminates; eauto.
Defined.

End General_loops.

Hint Constructors loop_prop loop_term genloop_prop genloop_term.

Lemma genloop_implies :
forall (A : Set) (P P' : A -> bool -> A -> Prop),
(forall a b a', P a b a' -> P' a b a') ->
forall a a', genloop_prop P a a' -> genloop_prop P' a a'.
Proof.
intros A P P' H.
induction 1; eauto.
Qed.