Require Import ZArith List Psatz Arith Omega. Open Scope Z_scope. Check 10000. Fixpoint fib (n : nat) : nat := match n with | 0%nat => 1%nat | 1%nat => 1%nat | S (S p as q) => (fib p + fib q)%nat end. Check Z.abs_nat. Fixpoint fibr (n : nat) : Z := match n with | 0%nat => 1 | 1%nat => 1 | S (S p as q) => (fibr p + fibr q) end. Fixpoint fibt (n : nat) (v1 v2 : Z) : Z := match n with | 0%nat => v1 | S p => fibt p v2 (v1 + v2) end. Compute fibt 10 1 1 - fibr 10. Time Compute fibt 30 1 1. Section arbitrary_type. Variable T : Type. Variable mult : T -> T -> T. Fixpoint power_positive (x : T) (n : positive) := match n with xH => x | xI p => let v := power_positive x p in mult (mult v v) x | xO p => let v := power_positive x p in mult v v end. End arbitrary_type. Fixpoint my_succ (x : positive) := match x with xH => xO xH | xI p => xO (my_succ p) | xO p => xI p end. Compute my_succ 13. Lemma proof_ring x y z: x * (x + y) + (z + 2) ^ 2 = x ^ 2 + z ^ 2 + 4 * z + x * y + 4. Proof. ring. Qed. Lemma proof_lia x y: x * x > 0 -> 2 * y < x * x -> 3 * y < ((2 * x) * x + 1). Proof. intros x0 c1. lia. Qed. Lemma my_succ_prop : forall p, Pos.to_nat (my_succ p) = S (Pos.to_nat p). Proof. induction p. simpl. rewrite Pos2Nat.inj_xO. rewrite Pos2Nat.inj_xI. rewrite IHp. ring. simpl. rewrite Pos2Nat.inj_xO. rewrite Pos2Nat.inj_xI. reflexivity. reflexivity. Qed. Close Scope Z_scope. Fixpoint mod2 n := match n with S (S n) => mod2 n | _ => n end. Lemma mod2_lt : forall n, mod2 n < 2. Proof. assert (main : forall n, mod2 n < 2 /\ mod2 (S n) < 2). induction n. simpl. lia. split. (* could be done by tauto *) destruct IHn as [_ it]; exact it. simpl. destruct IHn as [it _]; exact it. intros n. destruct (main n) as [it _]. exact it. Qed. Lemma le_ind : forall P : nat -> Prop, (forall n, (forall m, m < n -> P m) -> P n) -> forall n, P n. intros P ind_lt n. assert (main : forall m, m <= n -> P m). induction n. intros m mle0. apply ind_lt. intros p pltm. omega. intros m mleSn. assert (disj : m <= n \/ m = S n). apply NPeano.Nat.le_succ_r. exact mleSn. destruct disj as [mlen | misSn]. apply IHn. exact mlen. rewrite misSn. apply ind_lt. intros p pltSn. apply IHn. omega. apply main. omega. Qed. Lemma mod2_lt' : forall n, mod2 n < 2. Proof. induction n as [p IHp] using le_ind. destruct p as [|q]. simpl. omega. destruct q as [|q']. simpl. omega. simpl. apply IHp. omega. Qed.