From c2c3ceae8a2eabed33028bfff306c5664d0b42f2 Mon Sep 17 00:00:00 2001 From: Georges Gonthier Date: Wed, 27 Feb 2019 19:07:29 +0100 Subject: 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. --- mathcomp/solvable/burnside_app.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'mathcomp/solvable') diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v index 10cbbaa..34c1c7c 100644 --- a/mathcomp/solvable/burnside_app.v +++ b/mathcomp/solvable/burnside_app.v @@ -686,10 +686,10 @@ move=> p; rewrite inE. by do ?case/orP; move/eqP=> <- a; rewrite !(permM, permE); case: a; do 6?case. Qed. -Definition sop (p : {perm cube}) : seq cube := val (val (val p)). +Definition sop (p : {perm cube}) : seq cube := fgraph (val p). Lemma sop_inj : injective sop. -Proof. by do 2!apply: (inj_comp val_inj); apply: val_inj. Qed. +Proof. by move=> p1 p2 /val_inj/(can_inj fgraphK)/val_inj. Qed. Definition prod_tuple (t1 t2 : seq cube) := map (fun n : 'I_6 => nth F0 t2 n) t1. @@ -700,7 +700,7 @@ Proof. by move=> x n0; rewrite -pvalE unlock enum_rank_ord (tnth_nth F0). Qed. Lemma prod_t_correct : forall (x y : {perm cube}) (i : cube), (x * y) i = nth F0 (prod_tuple (sop x) (sop y)) i. Proof. -move=> x y i; rewrite permM -!sop_spec (nth_map F0) // size_tuple /=. +move=> x y i; rewrite permM -!sop_spec [RHS](nth_map F0) // size_tuple /=. by rewrite card_ord ltn_ord. Qed. -- cgit v1.2.3 From c5763504783b51bb5def88c82f55a0b99ebf9d67 Mon Sep 17 00:00:00 2001 From: Georges Gonthier Date: Mon, 4 Mar 2019 11:49:56 +0100 Subject: Compatibility fix for Coq issue coq/#9663 Coq currently fails to resolve Miller patterns against open evars (issue coq/#9663), in particular it fails to unify `T -> ?R` with `forall x : T, ?dR x` even when `?dR` does not have `x` in its context. As a result canonical structures and constructor notations for the new generalised dependent `finfun`s fail for the non-dependent use cases, which is an unacceptable regression. This commit mitigates the problem by specialising the canonical instances and most of the constructor notation to the non-dependent case, and introducing an alias of the `finfun_of` type that has canonical instances for the dependent case, to allow experimentation with that feature. With this fix the whole `MathComp` library compiles, with a few minor changes. The change in `integral_char` fixes a performance issue that appears to be the consequence of insufficient locking of both `finfun_eqType` and `cfIirr`; this will be explored in a further commit. --- mathcomp/solvable/burnside_app.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'mathcomp/solvable') diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v index 34c1c7c..f5f3719 100644 --- a/mathcomp/solvable/burnside_app.v +++ b/mathcomp/solvable/burnside_app.v @@ -694,8 +694,8 @@ Proof. by move=> p1 p2 /val_inj/(can_inj fgraphK)/val_inj. Qed. Definition prod_tuple (t1 t2 : seq cube) := map (fun n : 'I_6 => nth F0 t2 n) t1. -Lemma sop_spec : forall x (n0 : 'I_6), nth F0 (sop x) n0 = x n0. -Proof. by move=> x n0; rewrite -pvalE unlock enum_rank_ord (tnth_nth F0). Qed. +Lemma sop_spec x (n0 : 'I_6): nth F0 (sop x) n0 = x n0. +Proof. by rewrite nth_fgraph_ord pvalE. Qed. Lemma prod_t_correct : forall (x y : {perm cube}) (i : cube), (x * y) i = nth F0 (prod_tuple (sop x) (sop y)) i. -- cgit v1.2.3