Print ex.
Print sig.
Print proj2.
Print proj1.
Check proj1_sig.
Check proj2_sig.
Print sigT.
Search projT2.
Check projT2.
Print sumor.
Locate "exists".

Module Interval.
  Definition t (low high: nat): Type :=
    {x:nat | (x >= low) /\ (x <= high)}.

  Context {low high: nat}.
  Definition add (a b: t low high): t low high.
  Proof.
    refine(
    let (a, pfa) := a in
    let (b, pfb) := b in
    exist _ (a+b) _).
    split. 
    - induction a.
      + simpl. 
        destruct pfb; assumption.
      + simpl.
  Abort.
End Interval.

Definition i28: Type := Interval.t 2 8.

Definition n1: i28.
  (* unfold i28. *)
  (* unfold Interval.t. *)
  refine (exist _ 3 _).
  split; repeat constructor.
Qed.

Ltac ivtac n :=
  match goal with
  | |- Interval.t _ _ =>
      refine (exist _ n _);
      split; repeat constructor
  | |- {_:nat | _ >=_ /\ _ <= _} =>
      refine (exist _ n _);
      split; repeat constructor
  end.

(* Ltac ivtacGen low high n := *)
(*   match goal with *)
(*   | |- interval _ _ => *)
(*       refine (exist _ n _); *)
(*       split; repeat constructor *)
(*   end. *)

Definition n2: i28.
  unfold i28.
  ivtac 5.
Defined.

(* Ltac ivtac n := *)
(*   match goal with *)
(*   | H: _ |- exist _ _ => idtac *)
(*   end. *)
  

(*   | {x:nat | x >=_ /\ x <= _} => *)
(*       refine (exist _ n _); *)
(*       split; repeat constructor. *)
(* end *)


From mathcomp Require Import all_ssreflect all_algebra.
(* From mathcomp Require Import algebra.matrix. *)
(* Check matrix. *)

Check bool.
Print RingType.
Print ringType.
Print GRing.Ring.type.
Print GRing.Ring.class_of.

Local Open Scope type_scope.
Local Open Scope ring_scope.

Fail Example diagonal := \matrix_(i < 3, j < 7) if i == j then 1 else 0.
Fail Example diagonal := \matrix_(i < 3, j < 7) (if i == j then 1 else 0).

Check \matrix_(i<3, j<7) (fun i j => if i==j then 1 else 0).
Fail Compute \matrix_(i<3, j<7) if (i:nat)==j then 1 else 0.
(*
The command has indeed failed with message:
In environment
i : ordinal_finType 3
j : ordinal_finType 7
Unable to unify "?t0" with "?t@{b:=(i : nat) == j}" (cannot satisfy
constraint "?t0" == "?t@{b:=(i : nat) == j}").
*)
Fail Compute \matrix_(i<3, j<7) if (i==j :> nat) then 1 else 0.
(*
The command has indeed failed with message:
In environment
i : ordinal_finType 3
j : ordinal_finType 7
Unable to unify "?t0" with "?t@{b:=i == j :> nat}" (cannot satisfy constraint
"?t0" == "?t@{b:=i == j :> nat}").
*)
Fail Example eg1 := \matrix_(i<3, j<7) (fun (i:'I_3) (j:'I_7) => if (i==j :> nat) then 1 else 0).
Fail Example eg1 := \matrix_(i<3, j<7) (fun (i:'I_3) (j:'I_7) => if (i:nat) == j then 1 else 0).
Check \matrix_(i<3, j<7) if (i==j:>nat) then 1%:Z else 0.
Fail Check \matrix_(i<3, j<7) if (i:nat)==j then 1 else 0.
Fail Check \matrix_(i<3, j<7) (fun i:'I_3 j => if i==j then 1 else 0).
Check 1%:M.
Check const_mx (Some false): 'M_3.

Definition M2 : 'M[int]_(2,2) := \matrix_(i,j < 2) 3%:Z.
Example eg1: 'M[int]_ (3, 7) := \matrix_(i<3, j<7) 8%:Z.
Example eg2: 'M[int]_ (3, 7) := \matrix_(i<3, j<7) 8.
Check 3%:Z.
Print Scope Z_scope.
Print Scopes.
Example eg3 := \matrix_(i<3, j<7)
  (fun i j => if i==j :> nat then 1 else 0%:Z).
Locate "&&".
Example eg6 := \matrix_(i<3, j<7)
  (if (i==0) && (j==1) then (Some true) else (Some false)).
(* Example eg6 := \matrix_(i<3, j<7) *)
(*   (if (i==0) && (j==1) then 1 else 0%:Z). *)
(* Example eg6 := \matrix_(i<3, j<7) *)
(*   (if ((i==0) && (j==1)) then 1 else 0%:Z). *)
(* Example eg6 := \matrix_(i<3, j<7) *)
(*   (fun i j => if ((i=0:>nat) && (j=1):>nat) then 1 else 0%:Z). *)
(* Example eg6 := \matrix_(i<3, j<7) *)
(*   (fun i j => if (i=0 && j=1):>nat then 1 else 0%:Z). *)

Example eg7: 'rV_2 :=
  \row_(i<2) (if i==0 then true else false).
Check 1%:M: 'M_2.
Check eg7.

Example eg8: 'cV_2 :=
  \col_(i<2) (if i!=0 then true else false).
Check eg7 *m eg8.

Example eg7ob: 'rV_2 :=
  \row_(i<2) (if i==0 then Some true else Some false).
Example eg8ob: 'cV_2 :=
  \col_(i<2) (if i!=0 then Some true else Some false).



Example eg4 := \matrix_(i<3, j<3) (i+j).
(* Example eg4 := \matrix_(i<3, j<3) *)
(*   (fun i j => i+j%:Z). *)
(* Compute eg4 0 1. *)
Check mxE tt eg4.

Locate "=2".

Example eg5 := \matrix_(i<3, j<3) (Some (Nat.eqb i j)).
Check map_mx (fun x =>
  match x with
  | Some true => None
  | _ => x
  end).
Definition eg5' := map_mx (fun x =>
  match x with
  | Some true => None
  | _ => x
  end) eg5.


Goal eg5 0 1 = Some false.
rewrite /eg5 !mxE /=. Abort.
Goal eg5' 1 1 = None.
rewrite /eg5' !mxE /=. Abort.

Print ordinal.
Check Ordinal (m:=3).
Fail Check Ordinal (_:3<5).

(* Has to be at least one row and one column *)
Definition matLinker {rows cols: nat}
  (mat: 'M[option bool]_(rows.+1, cols.+1))
  : 'M[option bool]_(rows.+1, cols.+1).
Proof.
refine (
  let colid := Ordinal (m:=cols) (n:=cols.+1) _ in
  let mapfn :=
    fun ob => match ob with
              | Some true => None
              | _ => ob
              end in
  let lastcol := col colid mat in
  let lastcol' := map_mx mapfn lastcol in
  let mat' := col' colid mat in
  let res := row_mx mat' lastcol' in _).
  move: mat' res.
  rewrite PeanoNat.Nat.pred_succ.
  by rewrite addn1.
  Unshelve.
  by [].
Show Proof.
Defined.

Check matLinker eg5.


Check eg4.
Fail Check eg4 _ 0 _ 0.
Compute eg4 0 0.
Check eg4 0 0.
Search (int_ZmodType -> nat -> int_ZmodType).
Check eg2 _ _.
Check eg4 _ _.
Check eg4 0 0.
Compute eg4 0 0.

Check matrix bool 3 4.
(* 'M_(3, 4) : predArgType *)
Check 'M_(3, 4).
(*
'M_(3, 4)
     : predArgType
where
?R : [ |- Type]
*)
Check 'M[bool]_(3, 4).
(* 'M_(3, 4) : predArgType *)


Local Open Scope ring_scope.

Lemma sum_odd_n (n: nat) : \sum_(0 <= i < n.*2 | odd i) i = n^2.
Proof.
  elim: n => [//=|n IH]; first by rewrite double0 -mulnn muln0 big_geq.
rewrite (@big_cat_nat _ _ _ n.*2) //=; last by rewrite -!addnn leq_add.
rewrite IH -!mulnn mulSnr mulnSr -addnA.
congr (_ + _).
rewrite big_ltn_cond ?ifF ?odd_double //.
rewrite big_ltn_cond /ifT ?oddS ?odd_double //=.
by rewrite big_geq ?addn0 -addnn addnS // -addnn addSn.
Qed.








Fail Check MatrixFormula.seq_of_rV eg4.
From CoqEAL Require Import hrel param refinements trivial_seq seqmx.

Check eg2.
Compute (addmx eg2 eg2) 1 1.
Check 1%:M.
Check 0%:M.
Check M.

Check mkseqmx_ord.
Check matrix_of_fun.
Check fun_of_matrix.
Check matrix_of_fun tt.
Check matrix_of_fun _ _ _ _ eg4.
Check fun_of_matrix eg4.

(* Example smx4 := mkseqmx_ord (fun_of_matrix eg4). *)
(* Check mkseqmx_ord (fun_of_matrix eg4). *)
(* Compute List.tl smx4. *)
(* Check smx4. *)

Locate "'I_".
Print ordinal.

Compute [seq x <- ord_enum 2 | false ].
Compute [seq x <- ord_enum 2 | true ].
Check filter.
Compute List.hd 1 (ord_enum 2).
Check List.hd (Ordinal _) (ord_enum 2).
Compute List.hd (Ordinal _) (ord_enum 2).
Check ord_enum 2.
Check ord_enum.

Require Import Bvector.
Print Ordinal.
Check Vector.of_list.


Lemma length_size {A:Type} (l: seq A): List.length l = size l.
Proof.  by []. Qed.

Lemma size_ord_enum n : size (ord_enum n) = n.
Proof.
  by rewrite -{3}(size_iota 0 n) -val_ord_enum size_map.
Restart.
  rewrite -{3}(size_iota 0 n).
  rewrite -val_ord_enum.
  by rewrite size_map.
Qed.

(* Goal forall n:nat, *)
(*   size (ord_enum n) = n. *)
(* Proof. *)
(*   move=> n. *)
(*   Search size. *)
(*   rewrite -{3}(size_iota 0 n). *)
(*   Search ord_enum. *)
(*   rewrite -val_ord_enum. *)
(*   Search size. *)
(*   by rewrite size_map. *)
(*   Search ord_enum. *)
(* Qed. *)

Definition mkRow {A:Type} {rows cols:nat}
  (r: 'I_rows) (f: 'I_rows -> 'I_cols -> A): Vector.t A cols.
refine(
  match r with
  | @Ordinal _ r' _ =>
      let cids := Vector.of_list (ord_enum cols) in (* list 'I_cols *)
      let rw := Vector.map (fun cid => f r cid) cids in
      _
  end).
  move: rw.
  by rewrite length_size size_ord_enum.
Defined.

Definition mkMat {A:Type} {rows cols:nat}
  (f: 'I_rows -> 'I_cols -> A): Vector.t (Vector.t A cols) rows.
Proof.
  refine(
      let rids := Vector.of_list (ord_enum rows) in (* list 'I_rows *)
      let rws := Vector.map (fun rid => mkRow rid f) rids in
      (* let res := Vector.fold_right (fun rw acc => rw ++ acc) rws [] in *)
      _).
  move: rws.
  (* by rewrite (length_size (ord_enum rows)) (size_ord_enum). *)
  by rewrite length_size size_ord_enum.
Defined.

Check (fun_of_matrix M2).
Check (fun_of_matrix eg3).

Definition xm2 := mkMat (fun_of_matrix M2).
Definition xm3 := mkMat (fun_of_matrix eg3).
Definition xm4 := mkMat (fun_of_matrix eg4).
Check 'M_(3,4).


Definition mkseqmx_ord {A: Type} m n (f : 'I_m -> 'I_n -> A): nat.
Abort.

Require Import Extraction.
Extraction Language Haskell.         
Require Import ExtrHaskellBasic.     
Require Import ExtrHaskellZInteger.
Require Import ExtrHaskellNatNum.

Check 0xff.
Definition nnnn: nat := 0xf.
Check 'rV[bool]_nnnn.
Check 'M_(0, 0).


Definition M0: 'M_0 :=
  \matrix_(i<0, j<0) false. 

Definition R0 (cols: nat) :=
  \matrix_(i<0, j<cols) false. 
Check R0 3.
Check \matrix_(i<1, j<0) true.
About bool.
About int.

Definition C0 (rows: nat): 'cV_0 :=
  \matrix_(i<0, j<cols) false. 
  \matrix_(i<0, j<0) (fun i j => if i==j :> nat then true else false). 

(* Extract Inductive "Vector.t _ n" => "Vec" [ "Nil" "(:>)" ]. *)
Extract Inductive Vector.t => "Vec" [ "Nil" "(:>)" ].
Recursive Extraction xm2.
Recursive Extraction eg3.

Example e1 := (ord_enum 2).
Recursive Extraction e1. (* Ocaml ran this! *)
Recursive Extraction smx4. (* Ocaml couldn't run this.. *)



Goal ((0 : 'M[int]_(2,2)) == 0).
by coqeal.
Abort.

Search (matrix _ _ _ -> seq _).
Search (seqmx).
Require Import Bvector.




Compute \matrix_(i<3, j<7) if i==j then 1 else 0.
Check \matrix_(i<3, j<7) if i==j then 1 else 0.
Check \matrix_(i, j) (fun i j => i = j).