Ssreflect Users Discussion List

[Cyril Cohen <>]

Le 05/07/2013 14:29, Georges Gonthier a écrit :
>   You are probably right, we could use D : pred aT; it's likely the case 
> that the declaration dates back to an early version of finset where the 
> second
> argument of imset was restricted to a {set _}.
>   One disadvantage of this declaration, though, is that it makes it 
> difficult to provide D as an explicit arguments to, say, eq_imset, because 
> {set _}s are not allowed to coerce  (pred _). This is a general issue in 
> both fintype and finset. The solution would be to use pred_class (defined 
> in ssrbool.v) rather than pred as the type of generic predicates (or 
> rather, a variant of pred_class that allows specifying the domain type), 
> but that's a somewhat larger refactoring job.

Oh, I see!

Thus I tried to introduce.
Notation pred_class_of T := (pred_sort (predPredType T)).
in ssrbool,
and replaced many preconditions of the form
(D : pred T) by (D : pred_class_of T) in finset, finfun and fintype.

Now we can provide a set S or (mem S), when a pred_class_of T is expected.
But if there was an hypothesis of the form (P i) in our lemma (where P has 
type
pred_class_of T), and if P is instanciated to a set S or (mem S), we get a
subgoal (S i) instead of (i \in S).

I think the problem for mem is the coercion pred_of_mem which is inserted when
providing a (mem_pred T) where a (pred_class_of T) is expected. This prevents
the coercion pred_of_mem_pred (used to keep the form _ \in _) from being 
inserted.

I have two possible solutions for now:
1/ replace (mem S) by [pred x in S] where the problem happens. I partially
checked the FT proof: up to PFSection1, there are 4 occurences to change.
2/ replace the coercion pred_of_mem by a simple definition (in the coercion
graph, this coercion is redundant anyway), then everything works (I tested 
this
option on the full FT proof), but I don't have a good idea how this would
impact the interactive use.

However, I don't understand how to fix the problem when we directly put a set
(but it may not be that important since with set it didn't work before 
anyway).

Cheers,
-- 
Cyril