This file contains some useful tactics for proving instances of OrderedType. For tactics dealing with ordered types (order) and sets (fsetdec), see respectively OrderedType.v and SetDecide.v. For more details about the following tactics, see "docs/GenerateOT.tex". The following tactics are useful to prove instances for your own datatypes. There is one tactic for each of these 5 properties : reflexivity, symmetry and transitivity of the equality relation, transitivity and irreflexivity of the strict order relation. They work for relations defined inductively ; for example, lets say you have the datatype Inductive t := | t1 : A → t | t2 : B → C → t where A, B and C are types that already have instances. There are two main ways of defining the equality and order on t in a 'canonical' way : using inductives
   Inductive t_eq : t → t → Prop :=
   | eq_t1 : ∀ a a',
     a === a' → t_eq (t1 a) (t1 a')
   | eq_t2 : ∀ b b' c c',
     b === b' → c === c' → t_eq (t2 b c) (t2 b' c').
   

   Inductive t_lt : t → t → Prop :=
   | lt_t1_t1 : ∀ a a',
     a <<< a' → t_lt (t1 a) (t1 a')
   | lt_t1_t2 : ∀ a b c,
     t_lt (t1 a) (t2 b c)
   | lt_t2_t2_1 : ∀ b b' c c',
     b <<< b' → t_lt (t2 b c) (t2 b' c')
   | lt_t2_t2_2 : ∀ b b' c c',
     b === b' → c <<< c' → t_lt (t2 b c) (t2 b' c').
   

or using functions
   Definition t_eq (x y : t) : Prop :=
     match x, y with
     | t1 a, t1 a' ⇒ a === a'
     | t2 b c, t2 b' c' ⇒ b === b' ∧ c === c'
     | _, _ ⇒ False
     end.
   

   Definition t_lt (x y : t) : Prop :=
     match x, y with
     | t1 a, t1 a' ⇒ a <<< a'
     | t1 _, t2 _ _ ⇒ True
     | t2 b c, t2 b' c' ⇒ b <<< b' ∨ (b === b' ∧ c <<< c')
     | _, _ ⇒ False
     end.
   

The tactics are only designed for the first version of these specifications.

Tactics for inductives without recursion, nor parameters

Equivalence

StrictOrder

compare_spec

Tactics for inductives with recursion, but no parameters

Equivalence

StrictOrder

compare_spec

Tactics for mutual inductives, but no parameters

Equivalence

StrictOrder

compare_spec