エルデシュ=シュトラウス・ぼつ

erdos.v

Require Import Arith. (* lt_wf *)
(* Require Import Omega. *)

Hypothesis div2 : forall x, x / 2 < x.
Hypothesis mul2 : forall x y z w, x = y / 2 * z + w -> x * 2 = y * z + w * 2.

Theorem erdos2 :
  forall n,
    (exists c x y, 4 * c * x * y = n * (1 + x) + y).
Proof.
  intros.
  (* induction n. *)
  induction n using (well_founded_ind lt_wf).
    (* all: cycle 1. *)
    remember (H (n / 2)) as H2.
    (* remember (Nat.div_lt n 2) as F.
    remember (div2 n) as E. *)
    remember (H2 (div2 n)) as H3.
    clear HeqH2.
    clear HeqH3.
    destruct H3 as [ c H4 ].
    destruct H4 as [ x H5 ].
    destruct H5 as [ y H6 ].

    exists c.
    exists x.
    exists (2 * y).

    remember (mul2 (4 * c * x * y) n (1 + x) y H6) as H7.
    clear HeqH7.
    ring_simplify in H7.
    ring_simplify.
    trivial.
Qed.

Lemma hoge:
  forall A, A -> A.
Proof.
  intros.
  apply X.
Qed.

erdos2.v

Require Import Arith. (* lt_wf *)
(* Require Import Omega. *)

Hypothesis div2 : forall x, x < S x.
Hypothesis mul2 :
  forall p1 p2 q r t,
    p1 * p2 = q * r + t
      -> p1 * (S q * p2 / q) = (S q) * r + (S q) * t / q.

Theorem erdos2 :
  forall n,
    (exists c x y, 4 * c * x * y = S (S (S n)) * (1 + x) + y).
Proof.
  intros.
  induction n using (well_founded_ind lt_wf).
    destruct n.
      all: cycle 1.
      remember (H (n)) as H2.
      remember (H2 (div2 n)) as H3.

      clear HeqH2.
      clear HeqH3.
      destruct H3 as [ c H4 ]. (* ここは固定 *)
      destruct H4 as [ x H5 ]. (* ここは固定 *)
      destruct H5 as [ y H6 ]. (* ここは固定 *)

      exists c.
      exists x.
      exists ((S (S (S (S n)))) * y / (S (S (S n)))).

      remember (mul2 (4 * c * x) y (S (S (S n))) (1 + x) y H6) as H7.
      clear HeqH7.
      trivial.

      (* ring_simplify in H7.
      ring_simplify.
      trivial. *)
Abort.


Theorem erdos :
  forall n,
    n = 0 \/ Nat.odd n = true \/ (exists c x y, 4 * c * x * y = (S n) * (1 + x) + y).
Proof.
  intros.
  (* right. *)
  (* induction n. *)
  induction n using (well_founded_ind lt_wf).
    (* all: cycle 1. *)
    destruct n.
      auto.
      (* right. *)

      destruct n.
        auto.

      remember (H 0) as H2.
      (* remember (Nat.div_lt n 2) as F.
      remember (div2 n) as E. *)
      remember (H2 (div2 n)) as H3.

      destruct H3 as [ HA | HB ].

      clear HeqH2.
      clear HeqH3.
      destruct H3 as [ c H4 ].
      destruct H4 as [ x H5 ].
      destruct H5 as [ y H6 ].

      exists c.
      exists x.
      exists (y * n).

      remember (mul2 (4 * c * x * y) n (1 + x) y H6) as H7.
      clear HeqH7.
      ring_simplify in H7.
      ring_simplify.
      trivial.
Qed.

erdos3.v

Require Import Arith. (* ring_simplify. *)
Require Import Omega.

Section Erdos.
  Variables n c' y' : nat.

  Lemma l1 :
    (forall d y, d > 1 -> exists c x, 4 * c * x * y = d * (1 + n * x + y)).
  Proof.
    
    induction d.
    all: cycle 1.
    
    intros.
    (* Search (_ / _). *)
    remember (IHd y) as H1.
    case H1 as [ c H2 ].
    case H2 as [ x H3 ].
    exists (c+c/d).
    exists x.
    ring_simplify.
    (* ring_simplify in H3. *)
    rewrite H3.
    ring_simplify.
    remember (d * n * x + d * y + d).
    Search (_ + _).
    rewrite <- (Nat.add_assoc n0 (n*x) y).
    rewrite <- (Nat.add_assoc n0 (n*x+y) 1).
    Check (Nat.add_cancel_l (4 * x * y * (c / d)) (n * x + y + 1) n0).
    apply (Nat.add_cancel_l (4 * x * y * (c / d)) (n * x + y + 1) n0).
    Search (_ / _).

    (* congruence. *)
    (* f_equal (fun n => n + x*d*n). *)
    eauto.
    simpl.
    simpl.
    simpl in H3.
    rewrite <- H3.
    (* rewrite <- H0. *)
    (* apply Nat.mul_cancel_r.
    simpl.
    apply Nat.neq_succ_0.
    apply Nat.eq_sym_iff.
    discriminate.
    apply Nat.neq_succ_diag_r.
    ring_simplify. *)
  Abort.

  Theorem erdos2 :
    (* e は 0 でないのに、↑の証明で e=0 を使うのはおかしい *)
    (exists e, forall d c y, exists x, 4 * c * x * y = (1 + n * x + y) * d * e)
      -> exists x, 4 * (c'*1) * x * (y'*n) = (1 + n * x + y'*n) * n * 1.
      (* -> exists c x y, 4 * c * x * y = 1 + n * x + n * y. *)
  Proof.
    intro.
    case H as [ e H1 ].
    remember (H1 n (c'*e) (y'*n)) as H2.
    case H2 as [ x H3 ].
    simpl in H3.
  Abort.

  Theorem erdos :
    (forall d y, exists c x, 4 * c * x * y = (1 + n * x + y) * d)
      -> exists c x, 4 * c * x * (y'*n) = (1 + n * x + (y'*n)) * n.
      (* -> exists c x y, 4 * c * x * y = 1 + n * x + n * y. *)
  Proof.
    intro.
    remember (H n (y'*n)) as H1.
    (* destruct H as [ n H1 ]. すでにある値を入れられない
    case H.
    intros.
    case H0.
    intros.
    case H1.
    intros.
    case H2.
    intros. *)
  Abort.
End Erdos.