The Coq mailing list

["Strub, Pierre-Yves" <pierre-yves AT strub.nu>]

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