step.v

Require Import Coq.Program.Program.
Require Import Coq.Arith.PeanoNat.
Require Import Recdef.
Require Import Omega.

Function sup
         (n:  nat)
         {measure id}
  : nat :=
  match n with
  | O => 10
  | m => match m mod 10 with
         | O => 10 * sup (m / 10)
         | n' => m - n' + 10
         end
  end.
intros n m Heq Heq'.
unfold id.
apply Nat.div_lt.
+ apply Nat.neq_0_lt_0.
  apply not_eq_sym.
  apply Nat.neq_0_succ.
+ repeat constructor.
Defined.

Lemma sup_lt
      (n:  nat)
  : n < sup n.
Proof.
  functional induction sup n.
  + repeat constructor.
  + induction n; [ destruct y |].
    clear y;
      clear IHn;
      remember (S n) as m;
      clear Heqm.
    assert (Heq: m = 10 * (m / 10)). {
      apply Nat.div_exact.
      intros H; discriminate H.
      exact e0.
    }
    rewrite Heq at 1.
    apply Mult.mult_lt_compat_l.
    apply IHn0.
    repeat constructor.
  + clear y0 y.
    assert (H: n mod 10 < 10) by (apply Nat.mod_upper_bound; auto).
    omega.
Defined.

Lemma sup_lt_0
      (n:  nat)
  : 0 < sup n.
Proof.
  apply (Nat.le_lt_trans 0 n (sup n)).
  + apply Nat.le_0_l.
  + apply sup_lt.
Defined.

Function sub
         (n:  nat)
         {measure id}
  : nat :=
  match n with
  | O => 0
  | m => match m mod 10 with
         | O => 10 * sub (m / 10)
         | n' => m - n'
         end
  end.
intros n m Heq Heq'.
unfold id.
apply Nat.div_lt.
+ apply Nat.neq_0_lt_0.
  apply not_eq_sym.
  apply Nat.neq_0_succ.
+ repeat constructor.
Defined.

Fact fun_mod
     (m:  nat)
  : m mod 10 = 0 -> 0 < m -> 0 < m / 10.
Proof.
  intros Heq H.
  apply (Nat.mul_lt_mono_pos_l 10 0 (m / 10)).
  + repeat constructor.
  + assert (H': m = 10 * (m / 10)). {
      rewrite Nat.div_exact.
      + exact Heq.
      + auto.
    }
    rewrite <- H'.
    exact H.
Defined.

Lemma sub_lt
      (n:  nat)
      (Hn: 0 < n)
  : sub n < n.
Proof.
  functional induction sub n.
  + inversion Hn.
  + induction m; [ inversion y |].
    clear IHm.
    apply fun_mod in Hn.
    apply IHn0 in Hn.
    assert (S m = 10 * (S m / 10)). {
      apply Nat.div_exact.
      auto.
      exact e0.
    }
    rewrite H at 2.
    omega.
    exact e0.
  + induction (m mod 10); [ inversion y0 |].
    induction m; [ inversion y |].
    omega.
Defined.

Lemma sub_lt_0
      (n:  nat)
  : 0 < sub n -> 0 < n.
Proof.
  intro H.
  functional induction sub n.
  + auto.
  + assert (Hn: 0 < 10 * sub (m / 10)) by omega.
    assert (Hn': 0 < sub (m / 10)) by omega.
    apply IHn0 in Hn'.
    assert (Hn'': m / 10 <= m). {
      apply Nat.div_le_upper_bound.
      + auto.
      + omega.
    }
    omega.
  + omega.
Defined.

Program Fixpoint step_aux
        (x:     nat)
        (y:     nat)
        (l l':  list (nat * nat))
        {measure (y - x)}
  : list (nat * nat) :=
  match sup x <? y with
  | true
    => step_aux (sup x) y (cons (x, sup x) l) l'
  | otherwise
    => match x <? sub y with
       | true
         => step_aux x (sub y) l (cons (sub y, y) l')
       | otherwise
         => List.rev l ++ (if Nat.eqb x y then nil else (cons (x, y) nil)) ++ l'
       end
  end.
Next Obligation.
  symmetry in Heq_anonymous.
  apply Nat.ltb_lt in Heq_anonymous.
  assert (Hn: x < sup x) by apply sup_lt.
  omega.
Defined.
Next Obligation.
  symmetry in Heq_anonymous.
  apply Nat.ltb_lt in Heq_anonymous.
  apply not_eq_sym in H.
  apply Bool.not_true_is_false in H.
  apply Nat.ltb_ge in H.
  assert (Hs: 0 < sub y) by omega.
  assert (Hy: 0 < y) by apply (sub_lt_0 y Hs).
  assert (Hl: sub y < y) by apply (sub_lt y Hy).
  omega.
Defined.

Eval compute in (step_aux 27 399 nil nil).
(*
  = [(27, 30); (30, 100); (100, 300); (300, 390); (390, 399)]%list
  : list (nat * nat)
*)