The Coq mailing list

[Zoe Paraskevopoulou <zoe.paraskevopoulou AT gmail.com>]

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

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail