The Coq mailing list

[Igor Jirkov <igorjirkov AT gmail.com>]

Hello.

I did as Pierre-Yves said and it worked perfectly (I already have eqType instance for trees through a mechanism similar to one found in GenTree). I have yet to dive into this syntax though. Thanks!

Unfortunately, I don't think I can use the GenTree.tree type as it only holds the real data in its leaves.

I am also much grateful to Zoe and George for stating interesting and useful facts I did not yet know about.

---

Igor Jirkov

2014-08-27 17:40 GMT+04:00 Georges Gonthier <gonthier AT microsoft.com>:

  Hello,
  In order to be able to compare values of type sorted_tree T or tree T, you must be able to compare values of type T. This may be implicit from the properties of R, but would be better and more conveniently expressed by making T an eqType.
   Container types like T and sorted_tree T typically lift combinatorial properties of their elements; for example, the GenTree.tree T type in choice.v (a superset of your tree type) lifts the eqType, choiceType and countType structures of its element type. This example also shows you an easy way to implement this lifting, if you don't particularly care about the exact definition of comparison/choice/enumeration functions: just provide a pair of encode/decode functions to a known container type (you could use GenTree.tree), and use the PcanXxxMixin family of mixins.
  As Pierre-Yves points out, defining an instance of subType for sorted_tree (which only requires you to define its tree projector) will let you lift all the combinatorial structures from tree, using the [xxxMixin  of T by <:] forms (see the eqType.v and choice.v documentation). You will also get a few utilities (insub/insubd/val/Sub) that help working and reasoning with this sort of dependent type, in particular in combination with ssreflect's Prop-irrelevance support, and the transparent steps and evar patterns new to Ssreflect 1.5.

    Cheers,
Georges

-----Original Message-----
From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Strub, Pierre-Yves
Sent: 27 August 2014 13:51
To: coq-club AT inria.fr
Cc: coq-club-request AT inria.fr; Zoe Paraskevopoulou
Subject: Re: [Coq-Club] ssreflect eqtype instance

Hi,

The ssreflect library already provides subType (in eqtype.v) canonical structure for that case. See for example the definition of n.-tuple
(tuple.v) as a subtype of sequences of length n.

Regards,
-- Pierre-Yves.

On 2014-08-27 14:38, Zoe Paraskevopoulou wrote:
> Hi,
>
> If you use a decisional procedure to determine if the tree is sorted
> you can use proof irrelevance for boolean equality proofs to prove
> Equality.axiom.
> For example if you define the following
>
> Inductive sorted_tree := SortedTree (t: tree T) (proof: sorted_dec t =
> true).
>
> you can have that
>
> forall b, (proof1 proof2: b = true), proof1 = proof2
>
> as a direct corollary of Eqdep_dec.eq_proofs_unicity.
>
> Hope this helps,
> Zoe
>
> On Aug 27, 2014, at 12:43 PM, Igor Jirkov wrote:
>
>> Hello
>>
>> Could someone please point me at the explanation of how I can define
>> eqType for my own types?
>>
>> About my task: I have defined a type of 'sorted tree' as a pair of
>> tree and predicate of it being sorted:
>>
>> Inductive tree (T : Type) : Type := Node : T -> seq (tree T) -> tree
>> TInductive tree (T : Type) : Type := Node : T -> seq (tree T) -> tree
>> T
>>
>> Definition value (t: tree T) : T := match t with | Node v _ => v end.
>>
>> Definition children (t: tree T) := match t with | Node _ cs => cs
>> end.
>>
>> Fixpoint is_tree_sorted t := match t with
>> |Node v cs => sorted R (map value cs) && all is_tree_sorted cs
>> end.
>>
>> Inductive sorted_tree := SortedTree (t: tree T) (proof:
>> is_tree_sorted t).
>>
>> Using the same trick as with natural numbers won't work I think
>> (because there an Equality.axiom is used).
>>
>> ---
>> Igor Jirkov