Library term_orderings.term_o
Add LoadPath "basis".
Require Import Relations.
Require Import List.
Require Import list_sort.
Require Import term.
Set Implicit Arguments.
Module Type Term_ordering,
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}.
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.
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.
A functor building a Module Term_ordering from a term algebra
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.
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.
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.