Require Import Arith. Require Import Lia. Fixpoint exp (a : nat) (n : nat) : nat := match n with | O => 1 | S k => (exp a k) * a end. Lemma expsum : forall a x y : nat, exp a (x + y) = exp a x * exp a y. Proof. intros. induction y. simpl. replace (x+0) with x. auto with arith. auto with arith. simpl. replace (x+S y) with (S(x + y)). simpl. rewrite IHy. auto with arith. auto with arith. Qed. Fixpoint sum (a : nat -> nat) (n : nat) : nat := match n with | O => 0 | S k => (sum a k) + (a k) end. Definition div (a b : nat) := exists q, a = b*q. Definition numc (c m : nat) := sum (fun i => c*(exp 10 i)) m. Lemma numc_shift : forall c m : nat, (numc c m)*10 + c = numc c m + c * exp 10 m. Proof. intros. induction m. unfold numc. simpl. auto with arith. unfold numc. simpl. ring_simplify. unfold numc in IHm. simpl in IHm. lia. Qed. Lemma l3k : forall c m : nat, numc c (3*m) = (numc c m) * (1 + exp 10 m + exp 10 (2*m)). Proof. intros. induction m. simpl. auto with arith. unfold numc. unfold numc in IHm. replace (sum (fun i : nat => c * exp 10 i) (3 * S m)) with (sum (fun i : nat => c * exp 10 i) (3 * m) + c * (exp 10 (3*m)) + c * (exp 10 (3*m+1)) + c*(exp 10 (3*m+2))). rewrite IHm. replace (sum (fun i : nat => c * exp 10 i) (S m)) with (sum (fun i : nat => c * exp 10 i) m + c * exp 10 m). ring_simplify. replace (exp 10 (1 + m)) with (10 * (exp 10 m)). replace (exp 10 (2 * (1 + m))) with (100 * (exp 10 (2 * m))). replace (exp 10 m * c * exp 10 (2 * (1 + m))) with (c * exp 10 (3*m + 2)). replace (exp 10 m * c * exp 10 (1 + m)) with (c * exp 10 (2*m + 1)). replace (sum (fun i : nat => c * exp 10 i) m) with (numc c m). replace (exp 10 m * c * (10 * exp 10 m)) with (10 * c * exp 10 (2 * m)). replace (numc c m * (10 * exp 10 m) + numc c m * (100 * exp 10 (2 * m)) + numc c m + 10 * c * exp 10 (2 * m) + exp 10 m * c * (100 * exp 10 (2 * m)) + exp 10 m * c) with ((numc c m * 10 + c) * exp 10 m + numc c m * (100 * exp 10 (2 * m)) + numc c m + 10 * c * exp 10 (2 * m) + exp 10 m * c * (100 * exp 10 (2 * m))). rewrite (numc_shift c m). ring_simplify. replace (numc c m * exp 10 m + 100 * numc c m * exp 10 (2 * m) + numc c m + exp 10 m * exp 10 m * c + 100 * exp 10 m * exp 10 (2 * m) * c + 10 * exp 10 (2 * m) * c) with (numc c m * exp 10 m + (numc c m * 10 + c) * 10 * exp 10 (2 * m) + numc c m + exp 10 m * exp 10 m * c + 100 * exp 10 m * exp 10 (2 * m) * c). rewrite (numc_shift c m). ring_simplify. replace (exp 10 m * exp 10 m * c) with (exp 10 (2 * m) * c). replace (numc c m * exp 10 m + 10 * numc c m * exp 10 (2 * m) + numc c m + exp 10 (2 * m) * c + 110 * exp 10 m * exp 10 (2 * m) * c) with (numc c m * exp 10 m + (numc c m * 10 + c) * exp 10 (2 * m) + numc c m + 110 * exp 10 m * exp 10 (2 * m) * c). rewrite (numc_shift c m). ring_simplify. replace (exp 10 (3 * m + 1)) with (10 * exp 10 (3*m)). replace (exp 10 (3 * m + 2)) with (100 * exp 10 (3*m)). replace (111*exp 10 m * exp 10 (2*m)) with (111*exp 10 (3*m)). ring. replace (3*m) with (m + 2*m). rewrite expsum. ring. ring. replace (3*m + 2) with (S (S (3*m))). simpl. ring. lia. replace (3*m + 1) with (S (3*m)). simpl. ring. lia. ring. replace (2*m) with (m+m). rewrite expsum. ring. ring. ring. ring. replace (2*m) with (m+m). rewrite expsum. ring. ring. auto. replace (2*m+1) with (m+(1+m)). rewrite expsum. ring. ring. replace (3*m+2) with (m+(2*(1+m))). rewrite expsum. ring. ring. replace (2*(1+m)) with (S(S(2*m))). simpl. ring. ring. replace (1+m) with (S m). simpl. ring. ring. simpl. reflexivity. replace (3 * S m) with (S (S (S (3*m)))). replace (3 * m + 1) with (S (3*m)). replace (3 * m + 2) with (S (S (3*m))). simpl. ring. ring. ring. ring. Qed. Theorem t3k : forall c n : nat, div (numc c (exp 3 n)) (exp 3 n). Proof. intros. induction n. unfold numc. simpl. exists c. auto with arith. elim IHn. intros. replace (exp 3 (S n)) with (3 * exp 3 n). rewrite l3k. assert (forall k , div (1 + exp 10 k + exp 10 (2 * k)) 3). intro k. assert (forall k', exists q, exp 10 k' = 3*q + 1). intro k'. induction k'. exists 0. simpl. reflexivity. simpl (exp 10 (S k')). elim IHk'. intros. rewrite H0. exists (x0*10 + 3). ring. elim (H0 k). intros. elim (H0 (2*k)). intros. rewrite H1. rewrite H2. exists (x0+x1+1). ring. elim (H0 (exp 3 n)). intros. rewrite H1. rewrite H. exists (x0*x). ring. simpl. ring. Qed.