[coq] [mathcomp] make matrix to vector function
This commit is contained in:
parent
e72f7c7457
commit
c49c2c3d96
|
@ -0,0 +1,245 @@
|
||||||
|
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. *)
|
||||||
|
|
||||||
|
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.
|
||||||
|
|
||||||
|
Definition M3 : '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).
|
||||||
|
|
||||||
|
Example eg4 := \matrix_(i<3, j<3)
|
||||||
|
(fun i j => i+j%:Z).
|
||||||
|
Compute eg4 0 1.
|
||||||
|
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 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 *)
|
||||||
|
|
||||||
|
|
||||||
|
Fail Check MatrixFormula.seq_of_rV eg4.
|
||||||
|
From CoqEAL Require Import hrel param refinements trivial_seq seqmx.
|
||||||
|
|
||||||
|
|
||||||
|
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 mapped := Vector.map (fun cid => f r cid) cids in
|
||||||
|
_
|
||||||
|
end).
|
||||||
|
assert ((size (ord_enum cols)) = cols).
|
||||||
|
by rewrite size_ord_enum.
|
||||||
|
move: mapped.
|
||||||
|
by rewrite (length_size (ord_enum cols)) H.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Check Vector.fold_right.
|
||||||
|
|
||||||
|
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).
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Compute mkMat (fun_of_matrix eg4).
|
||||||
|
|
||||||
|
|
||||||
|
Definition mkseqmx_ord {A: Type} m n (f : 'I_m -> 'I_n -> A): nat.
|
||||||
|
Abort.
|
||||||
|
|
||||||
|
Require Import Extraction.
|
||||||
|
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).
|
Loading…
Reference in New Issue