Set Implicit Arguments. Require Import List. Require Import Arith Ring Div2 Recdef. Require Import Omega. Require Import ZArith. (** Provides Z.zero, Z.one, Z.add and Z.mul and a %Z notation scope *) (** Definitional classes. Bas Spitters, Eelis van der Weegen: Type Classes for Mathematics in Type Theory. Idea: one class per symbol. *) Class MonoidOp A := monop : A -> A -> A. Class MonoidUnit A := monunit : A. Typeclasses Transparent MonoidOp MonoidUnit. (** Definitional classes are transparent definitions, not records. *) Print MonoidUnit. Print monunit. Infix "*" := monop : monoid. Notation eps := monunit. (** Definitional classes for properties *) Class Associative {A} (f : A -> A -> A) := assoc : forall x y z, f x (f y z) = f (f x y) z. Class LeftUnit {A} (f : A -> A -> A) u := leftu : forall x, f u x = x. Class RightUnit {A} (f : A -> A -> A) u := rightu : forall x, f x u = x. Class Monoid {A} (dot : MonoidOp A) (unit : MonoidUnit A) := { dot_assoc :> Associative dot; one_left :> LeftUnit dot unit; one_right :> RightUnit dot unit }. (** Redoing the power development in that representation: *) Generalizable Variables A. Instance z_zero : MonoidUnit Z := 0%Z. Instance z_one : MonoidUnit Z := 1%Z. Instance z_plus: MonoidOp Z := Zplus. Instance z_mult: MonoidOp Z := Zmult. Instance Z_zero_plus_mon : Monoid z_plus z_zero | 1. Proof. constructor; red; intros; unfold z_plus, z_zero, monop, monunit; omega. Qed. Instance Z_one_mult_mon : Monoid z_mult z_one | 2. Proof. constructor; red; intros; unfold z_mult, z_one, monop, monunit; try omega. now rewrite Zmult_assoc. Qed. Section Power. (** Generalization of the remaining arguments (now refered to by overloaded notations). Context is like variables. *) Context `{Monoid A}. Local Open Scope monoid. Fixpoint power (a : A) (n : nat) := match n with | 0%nat => eps | S p => a * (power a p) end. Lemma power_of_unit : forall n, power eps n = eps. Proof. induction n as [|p Hp];simpl; [|rewrite Hp;simpl;rewrite one_left];trivial. Qed. Lemma power_square x n : power (x * x) n = power x (2 * n). Proof. induction n; simpl. auto. rewrite <- plus_n_O. rewrite IHn. assert (n + S n = 1 + 2 * n) by omega. rewrite H0. simpl. now rewrite <- dot_assoc. Qed. Function binary_power_mult (acc x : A) (n : nat) {measure (fun i=>i) n} : A (* acc * (power x n) *) := match n with | 0%nat => acc | S n' => if Even.even_odd_dec n then binary_power_mult acc (x * x) (div2 n) else binary_power_mult (acc * x) (x * x) (div2 n) end. Proof. intros;apply lt_div2; auto with arith. intros;apply lt_div2; auto with arith. Defined. Definition binary_power (x : A) (n : nat) := binary_power_mult eps x n. Lemma even_div2 n : (Even.even n -> 2 * div2 n = n)%nat /\ (Even.odd n -> 2 * div2 n = n - 1)%nat. Proof. assert (oddH:=Div2.odd_double). assert(evenH:=Div2.even_double). split; intros. specialize (evenH _ H0). rewrite evenH at 2. unfold double; omega. specialize (oddH _ H0). rewrite oddH at 2. unfold double; omega. Qed. Lemma minus_n_0 n : (n - 0 = n)%nat. Proof. now rewrite minus_n_O. Qed. Lemma binary_spec_aux x n acc : acc * power x n = binary_power_mult acc x n. Proof. functional induction (binary_power_mult acc x n). simpl; intros. rewrite one_right. reflexivity. intros. simpl. destruct n'. inversion _x. inversion H1. simpl power. simpl div2 in IHa. rewrite <- IHa. simpl. rewrite !dot_assoc. f_equal. rewrite power_square. destruct (even_div2 n'). rewrite H0; trivial. inversion _x. inversion H3; trivial. rewrite <- IHa. rewrite <- dot_assoc. f_equal. rewrite power_square. destruct (even_div2 (S n')). rewrite H1; trivial. simpl. now rewrite minus_n_0. Qed. Lemma binary_spec x n : power x n = binary_power x n. Proof. (* Left as an exercise. Hint: tail recursive functions need a generalized induction hypothesis. Function provides a tactic [functional induction (f n)] for every [Function f]... *) pose (binary_spec_aux x n eps). rewrite one_left in e. apply e. Qed. End Power. (** Rings, Matrices. Use a new [ring] scope to distinguish between the 0 and the 1 of the ring and new RingPlus, RingMult etc.. definitional classes for the various new operations. *) Module Rings. Class RingZero A := rzero :> MonoidUnit A. Class RingOne A := rone :> MonoidUnit A. Class RingMult A := rmult :> MonoidOp A. Class RingPlus A := rplus :> MonoidOp A. Delimit Scope ring_scope with ring. Notation "0" := rzero : ring_scope. Notation "1" := rone : ring_scope. Notation " x + y " := (rplus x%ring y%ring) : ring_scope. Notation " x * y " := (rmult x%ring y%ring) : ring_scope. Instance Z_rzero : RingZero Z := z_zero. Instance Z_rone : RingOne Z := z_one. Instance Z_rmult : RingMult Z := z_mult. Instance Z_rplus : RingPlus Z := z_plus. Typeclasses Transparent Z_rzero Z_rone Z_rmult Z_rplus. Typeclasses Transparent rzero rone rmult rplus. Class Commutative {A} (f : A -> A -> A) := comm : forall x y, f x y = f y x. Class Distributive {A} (f g : A -> A -> A) := distr : forall x y z, f (g x y) z = g (f x z) (f y z). Typeclasses Transparent RingZero RingOne RingPlus RingMult. (* Square 2x2 matrices actually form a non-commutative semiring *) Class SemiRing {A} (rzer : RingZero A) (ron : RingOne A) (rplu: RingPlus A) (rmul: RingMult A) := { zero_plus_mon :> @Monoid A rplus rzero; one_mult_mon :> @Monoid A rmult rone ; plus_comm :> Commutative rplus ; ring_mult_0 :> forall x : A, (0 * x = 0)%ring; mult_plus_distr :> Distributive rmult rplus }. Class Ring {A} (rzer : RingZero A) (ron : RingOne A) (rplu: RingPlus A) (rmul: RingMult A) := { ring_semi :> @SemiRing A _ _ _ _; mult_comm :> Commutative rmult }. Instance Z_semiring : SemiRing Z_rzero Z_rone Z_rplus Z_rmult := { zero_plus_mon := Z_zero_plus_mon; one_mult_mon := Z_one_mult_mon }. Proof. try red; intros; unfold Z_rzero, Z_rone, Z_rmult, Z_rplus, z_zero, z_plus, z_mult, z_one, monop, monunit; try omega. apply Zplus_comm. reflexivity. try red; intros; unfold Z_rzero, Z_rone, Z_rmult, Z_rplus, z_zero, z_plus, z_mult, z_one, monop, monunit; try omega. apply Z.mul_add_distr_r. Defined. (* Z is a commutative case *) Instance Z_ring : Ring Z_rzero Z_rone Z_rplus Z_rmult := { }. Proof. try red; intros; unfold Z_rzero, Z_rone, Z_rmult, Z_rplus, z_zero, z_plus, z_mult, z_one, monop, monunit; try omega. apply Zmult_comm. Defined. Local Open Scope ring_scope. Example foo : Z := 0 + 1 * 1. Section Matrices. Context `{Ring A}. Inspect 5. Record matrix := { c00 : A; c01 : A; c10 : A; c11 : A }. Global Instance matrix_zero : RingZero matrix := { rzero := {| c00 := 0; c01 := 0; c10 := 0; c11 := 0 |} }. (** Defined as the ring operation, so when we apply monoid overloaded operators to mzero we get back the ring operator under it. *) Global Instance matrix_mzero : MonoidUnit matrix | 2 := rzero. Global Instance matrix_one : RingOne matrix := { rone := {| c00 := 1; c01 := 0; c10 := 0; c11 := 1 |} }. Global Instance matrix_mone : MonoidUnit matrix | 1 (* prefer over zero *) := rone. Global Instance matrix_plus : RingPlus matrix := { rplus x y := {| c00 := x.(c00) + y.(c00); c01 := x.(c01) + y.(c01); c10 := x.(c10) + y.(c10); c11 := x.(c11) + y.(c11) |} }. Global Instance matrix_mult : RingMult matrix := { rmult x y := {| c00 := (x.(c00) * y.(c00)) + (x.(c01) * y.(c10)); c01 := x.(c00) * y.(c01) + x.(c01) * y.(c11); c10 := x.(c10) * y.(c00) + x.(c11) * y.(c10); c11 := x.(c10) * y.(c01) + x.(c11) * y.(c11) |} }. Global Instance matrix_mplus : MonoidOp matrix | 2 := rplus. Global Instance matrix_mmult : MonoidOp matrix | 1 (* prefer over plus *) := rmult. (* To solve some complicated obligations, we can just use the ring tactic *) Definition rt : @semi_ring_theory A rzero rone rplus rmult (@eq A). Proof. constructor. apply leftu. apply comm. apply assoc. apply leftu. apply ring_mult_0. apply comm. apply assoc. apply distr. Qed. Add Ring Aring : rt. Global Instance matrix_ring : @SemiRing matrix _ _ _ _. Proof. constructor. constructor; red; intros; unfold monop, monunit. destruct x, y, z; unfold matrix_plus, matrix_plus, rplus; simpl. f_equal; apply assoc. destruct x; unfold matrix_plus, matrix_mzero, matrix_zero, rzero, rplus; simpl. f_equal; apply leftu. destruct x; unfold rzero, rone, rplus, rmult; unfold matrix_one, matrix_mone, matrix_plus, matrix_mult, matrix_mzero, matrix_zero; simpl. f_equal; apply rightu. constructor; red; intros; unfold monop, monunit. destruct x, y, z; unfold rmult; unfold matrix_mult, matrix_plus; simpl. f_equal; ring. destruct x; unfold rmult, rone; unfold matrix_mult, matrix_one, matrix_mone; simpl. f_equal; ring. destruct x; unfold rmult, rone; unfold matrix_mult, matrix_one, matrix_mone; simpl. f_equal; ring. destruct x, y; unfold rmult, rplus, rone; unfold matrix_mult, matrix_plus, matrix_one, matrix_mone; simpl. f_equal; ring. destruct x; unfold rmult, rzero; unfold matrix_mult, matrix_zero, matrix_mzero; simpl. f_equal; ring. destruct x, y, z; unfold rmult, rplus, rone; unfold matrix_mult, matrix_plus, matrix_one, matrix_mone; simpl. f_equal; ring. Qed. End Matrices. End Rings. Import Rings. (** Matrices of integers: *) Notation M2_mat := (@matrix Z). Instance M2_ring : @SemiRing M2_mat _ _ _ _ := matrix_ring. (** Tests *) Open Scope Z_scope. Unset Printing All. Definition fibmat : M2_mat := Build_matrix 1 1 1 0. Compute power fibmat 40. Fixpoint fib (n : nat) := match n with | 0%nat | 1%nat => 1 | S (S n as n') => fib n' + fib n end. Definition fibonacci (n:nat) := c00 (power fibmat n). Definition binary_power_fibonacci (n:nat) := c00 (binary_power fibmat n). (* Time Compute fib 33. *) (* Time Compute fibonacci 33. *) (* Time Compute fibonacci 6000. *) (* Exercise: prove it indeed builds the fibonacci sequence! *) (* Useful to not unfold blindly as there is a nested case analysis *) Definition fib0 : fib 0 = 1 := eq_refl. Definition fib1 : fib 1 = 1 := eq_refl. Definition fibSSn n : fib (S (S n)) = fib (S n) + fib n := eq_refl. Hint Rewrite fib0 fib1 fibSSn : fib. (* Left as an exercise. - You should be able to show that matrix addition and multiplication have the following property: [forall m m' : M2 Z, m * m' + m' = (m + 1) * m'] - Show that [forall m m' : M2 Z, (topleft m + topleft m')%Z = topleft (m + m')]. - The proof follows by _well-founded_ induction on [n], using these two lemmas and the monoid laws on matrices. *) Open Local Scope ring_scope. Lemma c00_add (m m' : @matrix Z) : c00 m + c00 m' = c00 (m + m'). Proof. reflexivity. Qed. Require Import Setoid. Lemma ring_plus_mult `{SemiRing A} (m m' : A) : (m * m' + m' = (m + 1) * m'). Proof. setoid_rewrite distr. apply f_equal. now rewrite leftu. Qed. Lemma fibonacci_correct n : fibonacci n = fib n. Proof. induction n using lt_wf_ind. destruct n. - reflexivity. - destruct n. * reflexivity. * autorewrite with fib. do 2 rewrite <- H by auto with arith. unfold fibonacci. rewrite c00_add. apply f_equal. simpl. unfold monop, matrix_mmult. rewrite ring_plus_mult. rewrite dot_assoc. (* Eval compute in (fibmat + 1)%ring. Eval compute in (fibmat * fibmat)%ring. *) reflexivity. Qed. Print Assumptions fibonacci_correct. (* Should be closed under the global context! *)