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/ssreflect/binomial.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'mathcomp/ssreflect/binomial.v') diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v index 1f0ae16..c99e296 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -365,10 +365,10 @@ Lemma card_inj_ffuns_on D T (R : pred T) : Proof. rewrite -card_uniq_tuples. have bijFF: {on (_ : pred _), bijective (@Finfun D T)}. - by exists val => // x _; apply: val_inj. -rewrite -(on_card_preimset (bijFF _)); apply: eq_card => t. -rewrite !inE -(codom_ffun (Finfun t)); congr (_ && _); apply: negb_inj. -by rewrite -has_predC has_map enumT has_filter -size_eq0 -cardE. + by exists fgraph => x _; [apply: FinfunK | apply: fgraphK]. +rewrite -(on_card_preimset (bijFF _)); apply: eq_card => /= t. +rewrite !inE -(big_andE predT) -big_filter big_all -all_map. +by rewrite -[injectiveb _]/(uniq _) [map _ _]codom_ffun FinfunK. Qed. Lemma card_inj_ffuns D T : -- cgit v1.2.3