Library misc.G4

Require Import Arith.
Require Import Omega.
Require Import Relations.

Record item :Set := quad {
                    base: nat ;
                    coeff2 :nat ;                     coeff1 :nat ;                     coeff0 :nat }.

Inductive Rg: item -> item ->Prop :=
 Rg0 : forall b i j k, Rg (quad b i j (S k)) (quad (S b) i j k)
|Rg1 : forall b i j , Rg (quad b i (S j) 0) (quad (S b) i j b)
|Rg2 : forall b i , Rg (quad b (S i) 0 0) (quad (S b) i b b).

Hint Constructors Rg.

Definition Rgstar := clos_refl_trans _ Rg.

Definition reachable (q:item) := Rgstar (quad 3 2 2 2) q.

Hint Unfold reachable.

Hint Constructors clos_refl_trans.

Lemma reachable_Rgstar : forall q q', reachable q ->
                                      Rgstar q q' ->
                                      reachable q'.
Proof.
 intros q q' H H0.
 unfold reachable; constructor 3 with q;auto.
Qed.

Inductive final : item -> Prop :=
 final_intro :forall b , final (quad b 0 0 0).

Hint Constructors final.

Lemma final_no_future : forall q, final q -> forall q', ~ Rg q q'.
Proof.
 red;intros q Hq ; elim Hq.
 inversion 1.
Qed.

Definition next (q:item) : {q' : item | Rg q q'} + {final q}.
 intros q; case q ; intros b x y z.
 case z.
  case y.
   case x;auto.
   intro x';left;exists (quad (S b) x' b b);auto.
   intros y';left;exists (quad (S b) x y' b);auto.
   intros z'; left; exists (quad (S b) x y z');auto.
Defined.

Fixpoint nexts (n:nat)(q:item){struct n} : option item :=
  match n with 0 => Some q
             | S p => (match (next q)
                       with | inleft (exist q' _) => nexts p q'
                             | inright _ => None
                          
                                         end)
  end.


Lemma next_unicity : forall q q' q'',
      Rg q q' -> Rg q q'' -> q' = q''.
Proof.
 destruct 1; inversion_clear 1;auto.
Qed.

Lemma nexts_plus : forall n p q , nexts (n+p) q = match (nexts n q)
                                                 with Some q' => nexts p q' |
                                                      None => None end.
 induction n;simpl.
 auto.
 intros; case (next q).
 intro s; case s;auto.
 auto.
Qed.

Lemma nexts_ok : forall n q q', nexts n q = Some q' ->
                                Rgstar q q'.
Proof.
 induction n; simpl; auto.
 injection 1; destruct 1;constructor 2.
 intros q q'; case (next q).
 destruct s.
 intro.
 constructor 3 with x;auto.
 apply IHn;auto.
 discriminate 2.
Qed.

Lemma nexts_ok_R : forall q q', Rgstar q q' ->
                              exists n, nexts n q = Some q'.
Proof.
 intros.
 elim H.
 exists 1.
 simpl.
 case (next x).
 intro s.
 case s.
 intros x0 H1. rewrite (next_unicity _ _ _ H1 H0).
 trivial.
 intros.
 case (final_no_future _ f _ H0).
 exists 0.
 simpl;trivial.
 intros.
 case H1;case H3;intros.
 exists (x1 + x0).
 rewrite nexts_plus;auto.

 rewrite H5.
 auto.
Qed.

Definition nth_item n := nexts n (quad 3 2 2 2).

Eval compute in nth_item 0.
Eval compute in nth_item 2.

Eval compute in nth_item 3.

Eval compute in nth_item 8.
Eval compute in nth_item 20.
Eval compute in nth_item 21.

Eval compute in nth_item 44.
Eval compute in nth_item 92.

Eval compute in nth_item 188.

Fixpoint power (b:nat)(n:nat){struct n}:nat :=
 match n with 0 => 1
            | S p => b * b ^ p
 end
where "n ^ p" := (power n p):nat_scope.

Definition f n := pred (3 * 2^n).

Lemma f_Sn : forall n, f (S n) = S (2*(f n)).
 induction n;simpl.
 compute.
 auto.
 unfold f;simpl.
 unfold f at 1 in IHn.
 simpl in IHn.

 omega.
Qed.


Lemma L1 : forall k i j b,
      Rgstar (quad b i j (S k)) (quad (S k + b) i j 0).
Proof.
 induction k.
 simpl.
 constructor 1;auto.
 simpl.
 econstructor 3.
 econstructor 1; eauto.
 simpl in IHk.
 replace (S (S (k+b))) with (S (k + (S b))).
 apply IHk.
 auto with arith.
Qed.

Lemma L2 : forall k i j b,
      Rgstar (quad b i j k) (quad (k + b) i j 0).
 intro k; case k;intros.
 simpl;constructor 2.
 apply L1.
Qed.

Lemma L3 : forall b i j,
    Rgstar (quad b i (S j) 0) (quad (S (2 * b)) i j 0).
Proof.
 intros.
 case b.
 simpl.
 econstructor 1.
 constructor.
 econstructor 3.
 econstructor 1; econstructor.
 replace (S (2* S n)) with ( S n + S (S n)).
 apply L1.
 omega.
Qed.

Lemma L4 : forall b i j,
                   reachable (quad (f b) i (S j) 0) ->
                   reachable (quad (f (S b)) i j 0).
Proof.
 intros.
 econstructor 3.
 unfold reachable in H.
 eexact H.
 rewrite f_Sn.
 apply L3.
Qed.

Lemma L5 : forall k b i j,
          reachable (quad (f b) i (k+j) 0) ->
          reachable (quad (f (k+b)) i j 0).
Proof.
 induction k.
 simpl.
 auto.
 intros; econstructor 3.
 unfold reachable in IHk; eapply IHk.
 replace (S k + j) with (k + (S j)) in H.
 unfold reachable in H;eauto.
 omega.
 simpl;rewrite f_Sn.
 apply L3.
Qed.

Lemma F1 : reachable (quad (f 1) 2 2 0).
Proof.
 compute.
 replace 5 with (2+3).
 apply L1.
 simpl;trivial.
Qed.

Lemma F2 : reachable (quad (f 2) 2 1 0).
Proof.
 apply L4.
 apply F1.
Qed.

Lemma F3 : reachable (quad (f 3) 2 0 0).
Proof.
 compute.
 apply nexts_ok with 20.
 trivial.
Qed.

Lemma SF3 : reachable (quad (S (f 3)) 1 (f 3) (f 3)).
Proof.
 eapply reachable_Rgstar.
 eexact F3.
 constructor 1.
 constructor.
Qed.

Lemma F4 : reachable (quad (f 4) 1 (f 3) 0).
Proof.
 rewrite (f_Sn 3).
 eapply reachable_Rgstar.
 eexact SF3.
 replace (S (2 * (f 3))) with (f 3 + (S ( f 3))).
 apply L2.
 compute.
 trivial.
Qed.

Lemma F27 : reachable (quad (f 27) 1 0 0).
Proof.
 replace 27 with (f 3 + 4).
 apply L5.
 rewrite <- plus_n_O ; apply F4.
 trivial.
Qed.

Lemma SF27 : reachable (quad (S (f 27)) 0 (f 27) (f 27)).
Proof.
 eapply reachable_Rgstar.
 eexact F27.
 constructor 1.
 constructor.
Qed.

Lemma F28 : reachable (quad (f 28) 0 (f 27) 0).
Proof.
 rewrite f_Sn.
 replace (S (2 * f 27)) with (f 27 + (S (f 27))).
 2:omega.
 eapply reachable_Rgstar.
 eexact SF27.
 apply L2.
Qed.

Lemma Final : reachable (quad (f (f 27 + 28)) 0 0 0).
Proof.
 apply L5.
 rewrite <- plus_n_O.
 apply F28.
Qed.

Lemma big_number_eq : f (f 27 + 28) =
          3 * 2 ^ (3 * 2 ^ (3 ^3) + 3 ^3) - 1.
Proof.
 unfold f.
 rewrite <- pred_of_minus.
 replace 27 with (3^3).
 generalize (3^3).
 intro n; assert (0 < 2 ^ n).
 induction n.
 simpl;auto with arith.
 simpl.
 auto with arith.
 generalize H ; generalize (2 ^n).
 intros.
 replace (pred (3*n0) + S n) with (3*n0 + n).
 auto.
 omega.
 simpl;trivial.
Qed.

Theorem G4_length : reachable
                    (quad
                      (3 * 2 ^ (3 * 2 ^ (3 ^3) + 3 ^3) - 1)
                      0
                      0
                      0).
Proof.
 generalize big_number_eq.
 generalize (3 * 2 ^ (3 * 2 ^ 3 ^ 3 + 3 ^ 3) - 1).
 generalize Final.
 generalize (f (f 27 + 28)).
 induction 2.
 auto.
Qed.

Require Import ZArith.

Open Scope Z_scope.
Definition f_Z n := 3*(Zpower 2 n)-1.

Eval compute in (f_Z 27 + 28).