Ssreflect Users Discussion List

[Georges Gonthier <>]

  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:  [] On Behalf 
Of Strub, Pierre-Yves
Sent: 27 August 2014 13:51
To: 
Cc: ; 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