Still trying to get my brain around functions.v, there's a typical situation I don't see how to handle: an induced function.
Here is a small sample code to discuss the issue at hand:
From mathcomp Require Import all_ssreflect. From mathcomp.analysis Require Import boolp classical_sets. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Open Scope classical_set_scope. Section InitialProblem. Variable X Y Z: Type. Variable A: set X. Variable f: A -> Y. Variable B: set Y. Variable g: B -> Y. Hypothesis composable: forall a, f a \in B. Variable a: A. Check f a. Fail Check (g \o f) a. (* as expected *) (* FIXME: how to turn the fact `f a \in B` into some kind of typing judgement `f a: B`? => the question doesn't make sense as-is, but the situation is pretty usual in mathematics *) End InitialProblem. Section MinimalProblem. Variable Y: Type. Variable B: set Y. Variable b: Y. Hypothesis bB: b \in B. (* FIXME: better question: from this data, how to build a `whatever b bB` of type B ? *) (* `val` is essentially the reverse, if I get it right *) End MinimalProblem.
Last updated: Feb 05 2023 at 13:02 UTC