Ssreflect Users Discussion List

[(Emilio Jesús Gallego Arias)]

Dear Florent,

Florent Hivert 
<>
 writes:

> Thanks a lot for your code. It is indeed shorter than mine. After, rereading
> it and reworking it I'm not sure to understand why ? Is there a specific 
> trick
> you can pinpoint that made it shorter or simpler and that I can remember and
> reuse ? Or do you think, is it just that you know how to use ssreflect 
> tactics
> better than me.

I'm glad if it was of any help. IMVHO I wouldn't worry about the code
size; for me the hardest thing is to find good definitions, so they are
general and fit every use.

I don't know what more to say about proof style, I really must thank
strongly more experienced colleagues for their kind guidance and help.

Following their advice, I just try to imitate the style in the
library. I also to try to read and understand all the proofs and
definitions there before attempting my own.

Regarding your particular proof, I tried to use lighter dependent types
when transcribing your specification to Coq, in particular, avoiding
sumbool seems to work well inside the ssr framework.

I'd dare to say that a "light dependent types in algorithms" design
pattern is followed in the libraries and (I believe) mentioned in some
papers.

IMO in the long run, subType(s) tend to be more convenient to use than
their counterparts encoded as "type-families".

Compare:

a) eq : forall (x y : T) : { x = y } + { x <> y}.

vs

b) eq_op : T -> T -> bool
   eqP : [the usual type]

each approach has particular strong and weak points, but usually b) will
make your life easier in large proofs due to a more explicit "phase
separation". The cost to pay seems to be the bureaucracy of adding /eqP
to your proof scripts.

> For the sake of completeness, you missed the Hypothesis that the two
> intersecting block are in P in your cond_triv definition.
>
> Definition cond_triv P AB :=
>   [&& (AB.1 \in P), (AB.2 \in P), (AB.1 != AB.2) & (AB.1 :&: AB.2 != set0)].

Indeed, thanks! Note that you can drop the parens:

[&& AB.1 \in P, AB.2 \in P, AB.1 != AB.2 & AB.1 :&: AB.2 != set0].

thanks to the [&& ...] notation.

I would be very convenient to have a predType instance for pairs, so we
could write:

[&& AB \in (P,P), AB.1 != AB.2 & AB.1 :&: AB.2 != set0].

However, I couldn't manage to do it. I tried a hack:

> Inductive dup T := Dup of T & T.
>
> Coercion dup_to_pair T (d : dup T) := let: Dup x1 x2 := d in (x1, x2).
>
> Variables (T : Type) (pT : predType T).
>
> Definition mem_dup (l : dup pT) (e : dup T) : bool :=
>   (e.1 \in l.1) && (e.2 \in l.2).

But so far without success.

Best regards,
Emilio