Require Import QArith.

Open Scope Z_scope.
Open Scope Q_scope.

Check 0.
Check 2.


Coercion inject_Z : Z >-> Q.

Check 2.

Check 2+3.

Eval compute in 2+3.
Eval compute in 2/4 - 1/3 * 2.

Print Qmake.


Inductive matrix : Set := M (_ _ _ _ : Q).

(* Inductive matrix := M : Q -> Q -> Q -> Q -> matrix *)

Notation "[[ x11 , x12 ] , [ x21 , x22 ] ]" := (M x11 x12 x21 x22).

Check [[1,1],[0,0]].

Definition madd (m1 m2:matrix) :=
  let (x11,x12 , x21,x22) := m1 in
  let (y11,y12 , y21,y22) := m2 in
  [[x11+y11,x12+y12], [x21+y21,x22+y22]].

Notation "m1 + m2" := (madd m1 m2) : matrix_scope.


Check (1+3).

(*
Check ([[1,1],[4,1]] + [[1,1],[2,1]]).
*)
Open Scope matrix_scope.
Check ([[1,1],[4,1]] + [[1,1],[2,1]]).
Close Scope matrix_scope.
(*
Check ([[1,1],[4,1]] + [[1,1],[2,1]]).
*)


Delimit Scope matrix_scope with m.
Check ([[1,1],[4,1]] + [[1,1],[2,1]])%m.











Definition sum (m:matrix) := 
  let (x11,x12 , x21,x22) := m in
  x11+x22+x12+x21.

Arguments Scope sum [matrix_scope].

Check sum ([[1,1],[4,1]] + [[1,1],[2,1]]).




Bind Scope matrix_scope with matrix.

Definition det (m:matrix) := 
  let (x11,x12 , x21,x22) := m in
  x11*x22-x12*x21.

Print det.

Check det ([[1,1],[4,1]] + [[1,1],[2,1]]).


Check det ([[1+1,1],[0,0+1]] + [[1+1,1],[0,0+1]]).
Eval compute in det ([[1+1,1],[0,0+1]] + [[1+1,1],[0,0+1]]).





Definition mmult (m1 m2:matrix) :=
  let (x11,x12 , x21,x22) := m1 in
  let (y11,y12 , y21,y22) := m2 in
  [[x11*y11+x12*y21, x11*y12+x12*y22], 
   [x21*y11+x22*y21, x21*y12+x22*y22]].

Infix "*" := mmult : matrix_scope.

Check
  det ([[1+1,1],[0,0+1]] + [[1+1,1],[0,0+1]])
  + sum ([[1+1,4*6],[2,0+1]] * [[1+1,1],[0,0+1]]).

Eval compute in 
  det ([[1+1,1],[0,0+1]] + [[1+1,1],[0,0+1]])
  + sum ([[1+1,4*6],[2,0+1]] * [[1+1,1],[0,0+1]]).





Definition F1:=[[1,1],[1,0]].

Reserved Notation "'Ð' n" (at level 100).

Fixpoint fib n : matrix := 
  match n with
  | O => F1
  | S n' => (F1*(Ð n'))%m
  end
  where "'Ð' n":= (fib n).

Eval compute in Ð 10.





Definition mapm (m:matrix) f := 
  let (x11,x12 , x21,x22) := m in
    [[ f x11, f x12], [f x21, f x22]].

Notation "M | x => t " := (mapm M (fun x => t)) (at level 45).

Eval compute in (F1 + F1 | x => (2*x)%Q)%m.





Definition I := [[1,0],[0,1]].

(*
Notation "[| x1 , .. , xn |]" := (mmult x1 .. (mmult xn I) .. ).

Eval compute in [| F1, F1+F1, [[3,4],[4,2+3]] , F1*F1 |].
Eval compute in [| F1 |].
*)
Notation "[| x0 , x1 , .. , xn |]" := (mmult .. (mmult x0 x1) .. xn) (only parsing).

Eval compute in [| F1, F1+F1, [[3,4],[4,2+3]] , F1*F1 |].
(*
Eval compute in [| F1 |].
*)
Eval compute in [| F1, F1|].

Check (F1*F1)%m.

Locate "+".   
Locate "*".
Locate "Ð".
Locate "[[".
Locate ",".
Locate "|]".

Locate "exists".
Locate "(".

Print ex.

Print Grammar constr.


Print Z.
Print positive.

Check 6%positive.
Check (1~1~0~1%positive).