# Library term_orderings.term_o

``` Add LoadPath "basis". Require Import Relations. Require Import List. Require Import list_sort. Require Import term. Set Implicit Arguments. ```

## Definition of a total and decidable ordering on terms from a total and decidable ordering on symbols and variables.

``` Module Type Term_ordering. Declare Module Import T : term.Term. Declare Module OF : ordered_set.S with Definition A := T.symbol. Declare Module OX : ordered_set.S with Definition A := T.variable. Definition A := term. Axiom eq_dec : forall e1 e2 : A, {e1 = e2} + {e1 <> e2}. ```

### Definition of the ordering.

``` Fixpoint o (t1 t2:term) {struct t1} : Prop :=   match t1, t2 with   | Var v1, Var v2 => OX.o v1 v2   | Var _, Term _ _ => False   | Term _ _, Var _ => True   | Term f1 l1, Term f2 l2 =>       if eq_symbol_dec f1 f2       then          let o_term_list :=            (fix o_term_list (l1:list term) : list term -> Prop :=               fun l2 =>                 match l1, l2 with                 | nil, nil => True                 | _ :: _, nil => True                 | nil, _ :: _ => False                 | h1 :: tl1, h2 :: tl2 =>                     if eq_term_dec h1 h2                     then o_term_list tl1 tl2                     else o h1 h2                 end) in          o_term_list l1 l2       else OF.o f1 f2   end. ```

### Properties of the ordering.

``` Axiom o_total : forall t1 t2 : term, {o t1 t2} + {o t2 t1}. Axiom o_proof : order term o. Axiom o_dec : forall t1 t2, {o t1 t2} + {~o t1 t2}. End Term_ordering. ```

## and total and decidable orderings on symbols and variables.

``` Module Make (T1: term.Term) (OF1 : ordered_set.S with Definition A := T1.symbol) (OX1 : ordered_set.S with Definition A := T1.variable) <:   Term_ordering with Module T := T1                           with Module OF := OF1                           with Module OX := OX1                           with Definition A := T1.term. Module Import T := T1. Module OF := OF1. Module OX := OX1. Import F. Import X. Definition A := term. Lemma eq_dec : forall e1 e2 : A, {e1 = e2} + {e1 <> e2}. Proof. intros; apply eq_term_dec. Defined. ```

### Definition of the ordering.

``` Fixpoint o (t1 t2:term) {struct t1} : Prop :=   match t1, t2 with   | Var v1, Var v2 => OX.o v1 v2   | Var _, Term _ _ => False   | Term _ _, Var _ => True   | Term f1 l1, Term f2 l2 =>       if eq_symbol_dec f1 f2       then          let o_term_list :=            (fix o_term_list (l1:list term) : list term -> Prop :=               fun l2 =>                 match l1, l2 with                 | nil, nil => True                 | _ :: _, nil => True                 | nil, _ :: _ => False                 | h1 :: tl1, h2 :: tl2 =>                     if eq_term_dec h1 h2                     then o_term_list tl1 tl2                     else o h1 h2                 end) in          o_term_list l1 l2       else OF.o f1 f2   end. Definition o_term_list :=   (fix o_term_list (l1:list term) : list term -> Prop :=      fun l2 =>        match l1, l2 with        | nil, nil => True        | _ :: _, nil => True        | nil, _ :: _ => False        | h1 :: tl1, h2 :: tl2 =>            if eq_term_dec h1 h2            then o_term_list tl1 tl2            else o h1 h2        end). Lemma o_term_list_is_o_term_list :   forall l1 l2,   o_term_list l1 l2 =   ((fix o_term_list (l : list term) : list term -> Prop :=     fun l' : list term =>     match l with     | nil => match l' with              | nil => True              | _ :: _ => False              end     | h :: tl =>         match l' with         | nil => True         | h' :: tl' => if eq_term_dec h h' then o_term_list tl tl' else o h h'         end    end)) l1 l2. Proof. induction l1; induction l2; trivial. Qed. ```

### Properties of the ordering.

Totality.
``` Theorem o_total :   forall t1 t2 : term, {o t1 t2} + {o t2 t1}. Proof. apply term_rec7 with (P2:= fun t1 t2 => {o t1 t2} + {o t2 t1}) (Pl2 := fun l1 l2 => {o_term_list l1 l2} + {o_term_list l2 l1}). intros x1 t2; destruct t2 as [ x2 | f2 l2 ]. destruct (OX.o_total x1 x2) as [o_x1_x2 | o_x2_x1]; [left|right]; trivial. right; simpl; trivial. intros t1 x2; destruct t1 as [ x1 | f1 l1]. destruct (OX.o_total x1 x2) as [o_x1_x2 | o_x2_x1]; [left|right]; trivial. left; simpl; trivial. intros f1 f2 l1 l2 Hrec; simpl; destruct (eq_symbol_dec f1 f2) as [f1_eq_f2 | f1_diff_f2]; destruct (eq_symbol_dec f2 f1) as [f2_eq_f1 | f2_diff_f1]. elim Hrec; intro o_l1_l2; [ left | right ]; trivial. absurd (f2 = f1); auto. absurd (f1 = f2); auto. apply OF.o_total. intro l1; induction l1 as [ | a1 l1]. destruct l2 as [ | a2 l2 ] ; [left | right]; simpl; trivial. destruct l2 as [ | a2 l2 ]. left; simpl; trivial. intro Hrec. simpl; destruct (eq_term_dec a1 a2) as [a1_eq_a2 | a1_diif_a2]; destruct (eq_term_dec a2 a1) as [a2_eq_a1 | a2_diff_a1]. apply IHl1; intros; apply Hrec; right; trivial. absurd (a2 = a1); auto. absurd (a1 = a2); auto. apply Hrec; left; trivial. Qed. ```
Antisymmetry
``` Theorem o_anti_sym :  forall t1 t2, o t1 t2 -> o t2 t1 -> t1 = t2. Proof. elim OX.o_proof; intros Rv Tv Av; elim OF.o_proof; intros Rs Ts As; apply (term_rec7 (fun t1 t2 => o t1 t2 -> o t2 t1 -> t1 = t2)  (fun l1 l2 => o_term_list l1 l2 -> o_term_list l2 l1 -> l1 = l2)). intros x1; destruct t2 as [ x2 | f2 l2 ]. simpl; intros H1 H2; rewrite (Av _ _ H1 H2); trivial. contradiction. intros t1 x2; destruct t1 as [ x1 | f1 l1 ]. simpl; intros H1 H2; rewrite (Av _ _ H1 H2); trivial. contradiction. intros f1 f2 l1 l2 Hrec; simpl; destruct (eq_symbol_dec f1 f2) as [f1_eq_f2 | f1_diff_f2]; destruct (eq_symbol_dec f2 f1) as [f2_eq_f1 | f2_diff_f1]. intros H1 H2; subst f1; rewrite (Hrec H1 H2); trivial. absurd (f2 =f1); auto. absurd (f1 =f2); auto. intros H1 H2; absurd (f1 = f2); trivial; apply (As _ _ H1 H2). intro l1; induction l1 as [ | a1 l1 ]. intros l2 _; destruct l2 as [ | a2 l2 ]; trivial; contradiction. intros l2 Hrec; destruct l2 as [ | a2 l2 ]. contradiction. simpl; elim (eq_term_dec a1 a2); intro a1_eq_a2; elim (eq_term_dec a2 a1); intro a2_eq_a1. intros H1 H2; subst a1; rewrite (IHl1 l2); trivial. intros t1 t2 In_t1 In_t2 H3 H4; apply Hrec; trivial; right; trivial. absurd (a2 = a1); auto. absurd (a1 = a2); auto. intros H3 H4; absurd (a1 = a2); trivial; apply Hrec; trivial; left; trivial. Qed. ```
`o_term` is an order.
``` Theorem o_proof : order term o. Proof. elim OX.o_proof; intros Rv Tv Av; elim OF.o_proof; intros Rs Ts As; assert (At : forall t1 t2, o t1 t2 -> o t2 t1 -> t1 = t2). intro t; pattern t; apply term_rec4 with (fun l1 => forall l2, o_term_list l1 l2 -> o_term_list l2 l1 -> l1 = l2). intros x1 t2; destruct t2 as [ x2 | f2 l2 ]. simpl; intros H1 H2; rewrite (Av _ _ H1 H2); trivial. contradiction. intros f1 l1 Hrec t2; destruct t2 as [ x2 | f2 l2 ]. contradiction. simpl; destruct (eq_symbol_dec f1 f2) as [f1_eq_f2 | f1_diff_f2]; destruct (eq_symbol_dec f2 f1) as [f2_eq_f1 | f2_diff_f1]. intros H1 H2; rewrite (Hrec l2 H1 H2); subst f1; trivial. absurd (f2 = f1); auto. absurd (f1 = f2); auto. intros H1 H2; absurd (f1 = f2); trivial; apply (As _ _ H1 H2). intros l1; induction l1 as [ | a1 l1 ]. intros _ l2; destruct l2 as [ | a2 l2 ]; trivial; contradiction. intros Hrec l2; destruct l2 as [ | a2 l2 ]. contradiction. simpl; destruct (eq_term_dec a1 a2) as [a1_eq_a2 | a1_diff_a2]; destruct (eq_term_dec a2 a1) as [a2_eq_a1 | a2_diff_a1]. intros H1 H2; subst a1; rewrite IHl1 with l2; trivial; intros; apply Hrec; trivial; right; trivial. absurd (a2 = a1); auto. absurd (a1 = a2); auto. intros H1 H2; absurd (a1 = a2); trivial; apply Hrec; trivial; left; trivial. intuition. unfold reflexive; intro t; pattern t; apply term_rec4 with (fun l => o_term_list l l); trivial. intros f l H; simpl; elim (eq_symbol_dec f f); intro f_eq_f; trivial; absurd (f=f); trivial. induction l as [ | a l ]; intro Hrec; simpl; trivial; elim (eq_term_dec a a); intro a_eq_a. apply IHl; intros; apply Hrec; right; trivial. absurd (a = a); trivial. unfold transitive; intro t; pattern t; apply term_rec4 with (fun l1 => forall l2 l3, o_term_list l1 l2 -> o_term_list l2 l3 -> o_term_list l1 l3); clear t. intros x1 t2 t3; destruct t2 as [ x2 | f2 l2 ]; destruct t3 as [ x3 | f3 l3 ]. simpl; apply Tv. contradiction. contradiction. contradiction. intros f1 l1 Hrec t2 t3; destruct t2 as [ x2 | f2 l2 ]; destruct t3 as [ x3 | f3 l3 ]; trivial. contradiction. simpl; destruct (eq_symbol_dec f1 f2) as [f1_eq_f2 | f1_diff_f2]; destruct (eq_symbol_dec f2 f3) as [f2_eq_f3 | f2_diff_f3]; destruct (eq_symbol_dec f1 f3) as [f1_eq_f3 | f1_diff_f3]. apply Hrec. absurd (f1 = f3); subst f2; trivial. absurd (f2 = f3); subst f1; trivial. subst f1; trivial. absurd (f1 = f2); subst f3; trivial. subst f2; trivial. intros H1 H2; absurd (f1 = f2); trivial; subst f3; rewrite (As _ _ H1 H2); trivial. apply Ts. intros l1 Hrec; induction l1 as [ | a1 l1 ]; intros l2 l3; destruct l2 as [ | a2 l2 ]; destruct l3 as [ | a3 l3 ]; trivial. contradiction. simpl; destruct (eq_term_dec a1 a2) as [a1_eq_a2 | a1_diff_a2]; destruct (eq_term_dec a2 a3) as [a2_eq_a3 | a2_diff_a3]; destruct (eq_term_dec a1 a3) as [a1_eq_a3 | a1_diff_a3]. apply IHl1; intros t1 In_t1 t2 t3; apply Hrec; right; trivial. absurd (a1 = a3); subst a2; trivial. absurd (a2 = a3); subst a1; trivial. subst a2; trivial. absurd (a1 = a2); subst a3; trivial. subst a2; trivial. intros H1 H2; absurd (a1 = a2); trivial; subst a3; rewrite (At _ _ H1 H2); trivial. apply Hrec; left; trivial. Qed. ```
Decidability.
``` Theorem o_dec :   forall t1 t2, {o t1 t2} + {~o t1 t2}. Proof. apply (term_rec7 (fun t1 t2 => {o t1 t2} + {~o t1 t2})  (fun l1 l2 => {o_term_list l1 l2} + {~o_term_list l1 l2})). intros x1 t2; destruct t2 as [ x2 | f2 l2 ]; simpl; [ apply OX.o_dec | right; auto ]. intros t1 x2; destruct t1 as [ x1 | f1 l1 ]; simpl; [ apply OX.o_dec | left; auto ]. intros f1 f2 l1 l2 Hrec; simpl; destruct (eq_symbol_dec f1 f2) as [f1_eq_f2 | f1_diff_f2]; [ apply Hrec | apply OF.o_dec ]. intro l1; induction l1 as [ | a1 l1 ]. intro l2; destruct l2 as [ | a2 l2 ]; simpl; auto. intros l2 Hrec; destruct l2 as [ | a2 l2 ]; simpl; auto. destruct (eq_term_dec a1 a2) as [a1_eq_a2 | a1_diff_a2]. apply IHl1; intros; apply Hrec; right; trivial. apply Hrec; left; trivial. Qed. End Make. ```