diff options
| author | Georges Gonthier | 2019-02-27 19:07:29 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2019-04-01 17:42:28 +0200 |
| commit | c2c3ceae8a2eabed33028bfff306c5664d0b42f2 (patch) | |
| tree | f2ad780c73b919e0d64162ac02ab89918168d73a /mathcomp/algebra/matrix.v | |
| parent | cd958350ffb6836a4e9e02716fc19b1a1d1177cd (diff) | |
Making {fun ...} structural and extending it to dependent functions
Construct `finfun_of` directly from a bespoke indexed inductive type,
which both makes it structurally positive (and therefore usable as a
container in an `Inductive` definition), and accommodates naturally
dependent functions.
This is still WIP, because this PR exposed a serious shortcoming of
the Coq unification algorithm’s implantation of Miller patterns. This
bug defeats the inference of `Canonical` structures for `{ffun S -> T}`
when the instances are defined in the dependent case!
This causes unmanageable regressions starting in `matrix.v`, so I
have not been able to check for any impact past that. I’m pushing this
commit so that the Coq issue may be addressed.
Made `fun_of_fin` structurally decreasing: Changed the primitive
accessor of `finfun_of` from `tfgraph` to the `Funclass` coercion
`fun_of_fin`. This will make it possible to define recursive functions
on inductive types built using finite functions. While`tfgraph` is
still useful to transport the tuple canonical structures to
`finfun_of`, it is no longer central to the theory so its role has
been reduced.
Diffstat (limited to 'mathcomp/algebra/matrix.v')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 2580741..f87fb78 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -215,7 +215,7 @@ Definition mx_val A := let: Matrix g := A in g. Canonical matrix_subType := Eval hnf in [newType for mx_val]. Fact matrix_key : unit. Proof. by []. Qed. -Definition matrix_of_fun_def F := Matrix [ffun ij => F ij.1 ij.2]. +Definition matrix_of_fun_def F := Matrix [ffun ij => F ij.1 ij.2 : R]. Definition matrix_of_fun k := locked_with k matrix_of_fun_def. Canonical matrix_unlockable k := [unlockable fun matrix_of_fun k]. @@ -277,7 +277,8 @@ Notation "\row_ ( j < n ) E" := (@matrix_of_fun _ 1 n matrix_key (fun _ j => E)) Notation "\row_ j E" := (\row_(j < _) E) : ring_scope. Definition matrix_eqMixin (R : eqType) m n := - Eval hnf in [eqMixin of 'M[R]_(m, n) by <:]. + @SubEqMixin (@finfun_eqType _ (fun=> _)) _ (matrix_subType R m n). +(* Eval hnf in [eqMixin of 'M[R]_(m, n) by <:]. *) Canonical matrix_eqType (R : eqType) m n:= Eval hnf in EqType 'M[R]_(m, n) (matrix_eqMixin R m n). Definition matrix_choiceMixin (R : choiceType) m n := |