Library rpo.term
Add LoadPath "../prelude".
Require Import List.
Require Import more_list.
Require Import list_permut.
Require Import list_set.
Require Import Arith.
Set Implicit Arguments.
Module Type Signature.
There are almost no assumptions, except a decidable equality and an arity function.
Module Type Signature.
Parameter symb : Set.
Axiom eq_symbol_dec : forall f1 f2 : symb, {f1 = f2} + {f1 <> f2}.
The arity of a symbol contains also the information about built-in theories as in CiME
Inductive arity_type : Set :=
| AC : arity_type
| C : arity_type
| Free : nat -> arity_type.
Parameter arity : symb -> arity_type.
End Signature.
Module Type Variables.
Parameter var : Set.
Axiom eq_variable_dec : forall v1 v2 : var, {v1 = v2} + {v1 <> v2}.
End Variables.
Module Type Term.
Declare Module F : Signature.
Declare Module X : Variables.
Definition symbol := F.symb.
Definition variable := X.var.
Import F.
Import X.
Ltac destruct_arity f n Af :=
generalize (refl_equal (arity f)); pattern f at 1; destruct (arity f) as [ | | n]; intro Af.
Definition of terms.
Arity is not taken into account, and terms may be hill-formed.
Inductive term : Set :=
| Var : variable -> term
| Term : symbol -> list term -> term.
Definition direct_subterm t1 t2 : Prop :=
match t2 with
| Var _ => False
| Term _ l => In t1 l
end.
Definition and a few properties of the size of a term.
Fixpoint size (t:term) : nat :=
match t with
| Var v => 1
| Term f l => 1 + fold_left (fun size_acc e => size_acc + size e) l 0
end.
Axiom size_unfold :
forall t, size t = match t with
| Var _ => 1
| Term f l => 1 + list_size size l
end.
Axiom size_ge_one : forall t, 1 <= size t.
Axiom size_direct_subterm :
forall t1 t2, direct_subterm t1 t2 -> size t1 < size t2.
Section Recursion.
Variable P : term -> Type.
Variable Pl : list term -> Type.
Axiom term_rec2 : (forall n t, size t <= n -> P t) -> forall t, P t.
Axiom term_rec3 :
(forall v, P (Var v)) -> (forall f l, (forall t, In t l -> P t) -> P (Term f l)) -> forall t, P t.
Axiom term_rec4 :
(forall v, P (Var v)) -> (forall f l, Pl l -> P (Term f l)) ->
(forall l, (forall t, In t l -> P t) -> Pl l) -> forall t, P t.
End Recursion.
Section DoubleRecursion.
Variable P2 : term -> term -> Type.
Variable Pl2 : list term -> list term -> Type.
Axiom term_rec7 :
(forall v1 t2, P2 (Var v1) t2) ->
(forall t1 v2, P2 t1 (Var v2)) ->
(forall f1 f2 l1 l2, Pl2 l1 l2 -> P2 (Term f1 l1) (Term f2 l2)) ->
(forall l1 l2, (forall t1 t2, In t1 l1 -> In t2 l2 -> P2 t1 t2) -> Pl2 l1 l2) ->
forall t1 t2, P2 t1 t2.
Axiom term_rec8 :
(forall v1 t2, P2 (Var v1) t2) ->
(forall t1 v2, P2 t1 (Var v2)) ->
(forall f1 f2 l1 l2, Pl2 l1 l2 -> P2 (Term f1 l1) (Term f2 l2)) ->
(forall l1 l2, (forall t1 t2, In t1 l1 -> In t2 l2 -> P2 t1 t2) -> Pl2 l1 l2) ->
forall l1 l2, Pl2 l1 l2.
End DoubleRecursion.
Axiom eq_term_dec : forall t1 t2:term, {t1 = t2} + {t1 <> t2}.
Declare Module Term_eq_dec : decidable_set.S with Definition A:= term
with Definition eq_A_dec := eq_term_dec.
Fixpoint well_formed (t:term) : Prop :=
match t with
| Var _ => True
| Term f l =>
let well_formed_list :=
(fix well_formed_list (l:list term) : Prop :=
match l with
| nil => True
| h :: tl => well_formed h /\ well_formed_list tl
end) in
well_formed_list l /\
(match arity f with
| Free n => length l = n
| _ => length l = 2
end)
end.
Axiom well_formed_unfold :
forall t, well_formed t ->
match t with
| Var _ => True
| Term f l =>
(forall u, In u l -> well_formed u) /\
(match arity f with
| Free n => length l = n
| _ => length l = 2
end)
end.
Axiom well_formed_fold :
forall t,
match t with
| Var _ => True
| Term f l =>
(forall u, In u l -> well_formed u) /\
(match arity f with
| Free n => length l = n
| _ => length l = 2
end)
end -> well_formed t.
Fixpoint well_formed_list (l : list term) : Prop :=
match l with
| nil => True
| h :: tl => well_formed h /\ well_formed_list tl
end.
Definition substitution := list (variable * term).
Fixpoint apply_subst (sigma : substitution) (t : term) {struct t} : term :=
match t with
| Var v =>
match find eq_variable_dec v sigma with
| None => t
| Some v_sigma => v_sigma
end
| Term f l => Term f (map (apply_subst sigma) l)
end.
Axiom empty_subst_is_id : forall t, apply_subst nil t = t.
Axiom empty_subst_is_id_list : forall l, map (apply_subst nil) l = l.
Composition of substitutions.
Definition map_subst (f : variable -> term -> term) sigma :=
map (fun x =>
match (x : variable * term) with
| (v, v_sigma) => (v, f v v_sigma)
end)
sigma.
Definition subst_comp sigma1 sigma2 :=
(map_subst (fun _ t => apply_subst sigma1 t) sigma2)
++
(map_subst (fun v t =>
match find eq_variable_dec v sigma2 with
| None => t
| Some v_sigma2 => apply_subst sigma1 v_sigma2
end)
sigma1).
Axiom subst_comp_is_subst_comp_aux1 :
forall v sigma f,
find eq_variable_dec v (map_subst f sigma) =
match find eq_variable_dec v sigma with
| None => None
| Some t => Some (f v t)
end.
Axiom subst_comp_is_subst_comp :
forall sigma1 sigma2 t,
apply_subst (subst_comp sigma1 sigma2) t =
apply_subst sigma1 (apply_subst sigma2 t).
Well-formed substitutions.
Definition well_formed_subst sigma :=
forall v, match find eq_variable_dec v sigma with
| None => True
| Some t => well_formed t
end.
Axiom well_formed_apply_subst :
forall sigma, well_formed_subst sigma ->
forall t, well_formed t -> well_formed (apply_subst sigma t).
Fixpoint is_a_pos (t : term) (p : list nat) {struct p}: bool :=
match p with
| nil => true
| i :: q =>
match t with
| Var _ => false
| Term _ l =>
match nth_error l i with
| Some ti => is_a_pos ti q
| None => false
end
end
end.
Fixpoint subterm_at_pos (t : term) (p : list nat) {struct p}: option term :=
match p with
| nil => Some t
| i :: q =>
match t with
| Var _ => None
| Term _ l =>
match nth_error l i with
| Some ti => subterm_at_pos ti q
| None => None
end
end
end.
Axiom size_subterm_at_pos :
forall t i p, match subterm_at_pos t (i :: p) with
| Some u => size u < size t
| None => True
end.
Axiom is_a_pos_exists_subtem :
forall t p, is_a_pos t p = true -> exists u, subterm_at_pos t p = Some u.
Fixpoint replace_at_pos (t u : term) (p : list nat) {struct p} : term :=
match p with
| nil => u
| i :: q =>
match t with
| Var _ => t
| Term f l =>
let replace_at_pos_list :=
(fix replace_at_pos_list j (l : list term) {struct l}: list term :=
match l with
| nil => nil
| h :: tl =>
match j with
| O => (replace_at_pos h u q) :: tl
| S k => h :: (replace_at_pos_list k tl)
end
end) in
Term f (replace_at_pos_list i l)
end
end.
Fixpoint replace_at_pos_list (l : list term) (u : term) (i : nat) (p : list nat)
{struct l}: list term :=
match l with
| nil => nil
| h :: tl =>
match i with
| O => (replace_at_pos h u p) :: tl
| S j => h :: (replace_at_pos_list tl u j p)
end
end.
Axiom replace_at_pos_unfold :
forall f l u i q,
replace_at_pos (Term f l) u (i :: q) = Term f (replace_at_pos_list l u i q).
Axiom replace_at_pos_is_replace_at_pos1 :
forall t u p, is_a_pos t p = true ->
subterm_at_pos (replace_at_pos t u p) p = Some u.
Axiom replace_at_pos_is_replace_at_pos2 :
forall t p u, subterm_at_pos t p = Some u -> replace_at_pos t u p = t.
Axiom subterm_at_pos_apply_subst_apply_subst_subterm_at_pos :
forall t p sigma,
match subterm_at_pos t p with
| Some u =>
subterm_at_pos (apply_subst sigma t) p = Some (apply_subst sigma u)
| None => True
end.
Axiom replace_at_pos_list_replace_at_pos_in_subterm :
forall l1 ui l2 u i p, length l1 = i ->
replace_at_pos_list (l1 ++ ui :: l2) u i p =
l1 ++ (replace_at_pos ui u p) :: l2.
End Term.
Module Make (F1 : Signature) (X1 : Variables) <:
Term with Module F := F1 with Module X := X1.
Module F := F1.
Module X := X1.
Definition symbol := F.symb.
Definition variable := X.var.
Import F.
Import X.
Module DecVar <: decidable_set.S.
Definition A := variable.
Lemma eq_A_dec : forall x y : A, { x = y } + { x <> y }.
Proof.
apply eq_variable_dec.
Qed.
End DecVar.
Module VSet <: list_set.S with Definition DS.A := variable :=
list_set.Make (DecVar).
Definition of terms.
Arity is not taken into account, and terms may be ill-formed.
Inductive term : Set :=
| Var : variable -> term
| Term : symbol -> list term -> term.
Definition direct_subterm t1 t2 : Prop :=
match t2 with
| Var _ => False
| Term _ l => In t1 l
end.
Definition and a few properties of the size of a term.
Fixpoint size (t:term) : nat :=
match t with
| Var v => 1
| Term f l => 1 + fold_left (fun size_acc e => size_acc + size e) l 0
end.
Lemma size_unfold :
forall t,
size t = match t with
| Var _ => 1
| Term f l => 1 + list_size size l
end.
Proof.
intro t; destruct t as [x | f l]; trivial.
simpl; rewrite list_size_fold; trivial.
Qed.
Lemma size_ge_one : forall t, 1 <= size t.
Proof.
destruct t as [ x | f l ]; trivial.
rewrite size_unfold; auto with arith.
Qed.
Lemma size_direct_subterm :
forall t1 t2, direct_subterm t1 t2 -> size t1 < size t2.
Proof.
intros t1 t2; unfold direct_subterm; destruct t2 as [ x | f l ].
contradiction.
rewrite (size_unfold (Term f l)).
induction l as [ | t l]; simpl; intuition.
subst; auto with arith.
apply lt_le_trans with (1 + list_size size l); trivial;
simpl; auto with arith.
Qed.
Section Recursion.
Variable P : term -> Type.
Variable Pl : list term -> Type.
Definition term_rec2 : (forall n t, size t <= n -> P t) -> forall t, P t.
Proof.
intros H t; apply (H (size t) t); apply le_n.
Qed.
Definition term_rec3 :
(forall v, P (Var v)) -> (forall f l, (forall t, In t l -> P t) -> P (Term f l)) -> forall t, P t.
Proof.
intros Hvar Hterm; apply term_rec2; induction n; intros t Size_t.
absurd (1 <= 0); auto with arith;
apply le_trans with (size t); trivial; apply size_ge_one.
destruct t as [ x | f l ]; trivial;
apply Hterm; intros; apply IHn;
apply lt_n_Sm_le;
apply lt_le_trans with (size (Term f l)); trivial;
apply size_direct_subterm; trivial.
Qed.
Definition term_rec4 :
(forall v, P (Var v)) -> (forall f l, Pl l -> P (Term f l)) ->
(forall l, (forall t, In t l -> P t) -> Pl l) -> forall t, P t.
Proof.
intros Hvar Hterm Hlist; apply term_rec2;
induction n; intros t Size_t.
absurd (1<=0); auto with arith;
apply le_trans with (size t); trivial; apply size_ge_one.
destruct t as [ x | f l ]; trivial;
apply Hterm; apply Hlist; intros t In_t; apply IHn;
apply lt_n_Sm_le;
apply lt_le_trans with (size (Term f l)); trivial;
apply size_direct_subterm; trivial.
Qed.
End Recursion.
Section DoubleRecursion.
Variable P2 : term -> term -> Type.
Variable Pl2 : list term -> list term -> Type.
Definition term_rec7 :
(forall v1 t2, P2 (Var v1) t2) ->
(forall t1 v2, P2 t1 (Var v2)) ->
(forall f1 f2 l1 l2, Pl2 l1 l2 -> P2 (Term f1 l1) (Term f2 l2)) ->
(forall l1 l2, (forall t1 t2, In t1 l1 -> In t2 l2 -> P2 t1 t2) -> Pl2 l1 l2) ->
forall t1 t2, P2 t1 t2.
Proof.
intros Hvt Htv Hterm Hlist.
intro t1; pattern t1; apply term_rec2; induction n; clear t1;
intros t1 Size_t1.
absurd (1<=0); auto with arith;
apply le_trans with (size t1); trivial; apply size_ge_one.
destruct t1 as [ x1 | f1 l1 ]; trivial.
destruct t2 as [ x2 | f2 l2 ]; trivial.
apply Hterm; apply Hlist; intros t1 t2 In_t1 In_t2; apply IHn;
apply lt_n_Sm_le;
apply lt_le_trans with (size (Term f1 l1)); trivial;
apply size_direct_subterm; trivial.
Qed.
Definition term_rec8 :
(forall v1 t2, P2 (Var v1) t2) ->
(forall t1 v2, P2 t1 (Var v2)) ->
(forall f1 f2 l1 l2, Pl2 l1 l2 -> P2 (Term f1 l1) (Term f2 l2)) ->
(forall l1 l2, (forall t1 t2, In t1 l1 -> In t2 l2 -> P2 t1 t2) -> Pl2 l1 l2) ->
forall l1 l2, Pl2 l1 l2.
Proof.
intros Hvt Htv Hterm Hlist l1 l2;
apply Hlist;
intros; apply term_rec7; trivial.
Defined.
End DoubleRecursion.
Theorem eq_term_dec :
forall t1 t2:term, {t1 = t2} + {t1 <> t2}.
Proof.
intro t1; pattern t1; apply term_rec3.
intro x1; destruct t2 as [ x2 | f2 l2].
destruct (eq_variable_dec x1 x2) as [x1_eq_x2 | x1_diff_x2].
left; subst; trivial.
right; intro H; apply x1_diff_x2; inversion H; trivial.
right; discriminate.
intros f1 l1 Hrec t2; destruct t2 as [x2 | f2 l2].
right; discriminate.
destruct (eq_symbol_dec f1 f2) as [f1_eq_f2 | f1_diff_f2].
subst; assert (Hrec_list : forall l2, {l1 = l2} + {l1 <> l2}).
clear f2 l2; induction l1 as [ | a1 l1].
intro l2; destruct l2 as [ | a2 l2]; [left; trivial | right; discriminate].
intro l2; destruct l2 as [ | a2 l2].
right; discriminate.
assert (In_a1 : In a1 (a1 :: l1)). left; trivial.
destruct (Hrec a1 In_a1 a2) as [a1_eq_a2 | a1_diff_a2].
assert (Hrec_l1 : forall t, In t l1 -> forall t2, {t = t2} + {t <> t2}).
intros; apply Hrec; right; trivial.
subst; destruct (IHl1 Hrec_l1 l2) as [l1_eq_l2 | l1_diff_l2];
[ left; subst
| right; intro H; apply l1_diff_l2; inversion H] ; trivial.
right; intro H; apply a1_diff_a2; inversion H; trivial.
destruct (Hrec_list l2) as [l1_eq_l2 | l1_diff_l2];
[ left; subst
| right; intro H; apply l1_diff_l2; inversion H] ; trivial.
right; intro H; apply f1_diff_f2; inversion H; trivial.
Qed.
Module Term_eq_dec : decidable_set.S with Definition A:= term
with Definition eq_A_dec := eq_term_dec.
Definition A := term.
Definition eq_A_dec := eq_term_dec.
End Term_eq_dec.
Fixpoint well_formed (t:term) : Prop :=
match t with
| Var _ => True
| Term f l =>
let well_formed_list :=
(fix well_formed_list (l:list term) : Prop :=
match l with
| nil => True
| h :: tl => well_formed h /\ well_formed_list tl
end) in
well_formed_list l /\
(match arity f with
| Free n => length l = n
| _ => length l = 2
end)
end.
Lemma well_formed_unfold :
forall t, well_formed t ->
match t with
| Var _ => True
| Term f l =>
(forall u, In u l -> well_formed u) /\
(match arity f with
| Free n => length l = n
| _ => length l = 2
end)
end.
Proof.
intros t; destruct t as [ x | f l ]; trivial.
intros [Wl A]; split; trivial.
clear A; induction l as [ | t l].
contradiction.
generalize Wl; clear Wl; intros [Wa Wl] u [Eq_u_a | In_u].
subst u; trivial.
apply IHl; trivial.
Qed.
Lemma well_formed_fold :
forall t,
match t with
| Var _ => True
| Term f l =>
(forall u, In u l -> well_formed u) /\
(match arity f with
| Free n => length l = n
| _ => length l = 2
end)
end -> well_formed t.
Proof.
intros t; destruct t as [ x | f l ]; trivial.
intros [Wl A]; split ; trivial; clear A; induction l as [ | t l]; trivial; split.
apply Wl; left; trivial.
apply IHl; intros; apply Wl; right; trivial.
Qed.
Fixpoint well_formed_list (l : list term) : Prop :=
match l with
| nil => True
| h :: tl => well_formed h /\ well_formed_list tl
end.
Definition substitution := list (variable * term).
Fixpoint apply_subst (sigma : substitution) (t : term) {struct t} : term :=
match t with
| Var v =>
match find eq_variable_dec v sigma with
| None => t
| Some v_sigma => v_sigma
end
| Term f l => Term f (map (apply_subst sigma) l)
end.
Lemma empty_subst_is_id : forall t, apply_subst nil t = t.
Proof.
intro t; pattern t; apply term_rec3; clear t; trivial.
intros f l IH; simpl; apply (f_equal (fun l => Term f l));
induction l as [ | t l]; trivial; simpl; rewrite (IH t).
rewrite IHl; trivial.
intros; apply IH; right; trivial.
left; trivial.
Qed.
Lemma empty_subst_is_id_list : forall l, map (apply_subst nil) l = l.
Proof.
intro l; induction l as [ | t l]; simpl;
[idtac | rewrite empty_subst_is_id; rewrite IHl];
trivial.
Qed.
Composition of substitutions.
Definition map_subst (f : variable -> term -> term) sigma :=
map (fun x =>
match (x : variable * term) with
| (v, v_sigma) => (v, f v v_sigma)
end)
sigma.
Definition subst_comp sigma1 sigma2 :=
(map_subst (fun _ t => apply_subst sigma1 t) sigma2)
++
(map_subst (fun v t =>
match find eq_variable_dec v sigma2 with
| None => t
| Some v_sigma2 => apply_subst sigma1 v_sigma2
end)
sigma1).
Lemma subst_comp_is_subst_comp_aux1 :
forall v sigma f,
find eq_variable_dec v (map_subst f sigma) =
match find eq_variable_dec v sigma with
| None => None
| Some t => Some (f v t)
end.
Proof.
intros v sigma f; induction sigma as [ | [v1 a1] sigma ].
simpl; trivial.
simpl; elim (eq_variable_dec v v1); intro v_eq_v1; trivial;
subst v; trivial.
Qed.
Lemma subst_comp_is_subst_comp_aux2 :
forall v sigma1 sigma2,
find (B:= term) eq_variable_dec v (sigma1 ++ sigma2) =
match find eq_variable_dec v sigma1 with
| Some _ => find eq_variable_dec v sigma1
| None => find eq_variable_dec v sigma2
end.
Proof.
intros v sigma1 sigma2;
induction sigma1 as [ | [v1 a1] sigma1] ; trivial.
simpl; elim (eq_variable_dec v v1); intro v_eq_v1; trivial.
Qed.
Theorem subst_comp_is_subst_comp :
forall sigma1 sigma2 t,
apply_subst (subst_comp sigma1 sigma2) t =
apply_subst sigma1 (apply_subst sigma2 t).
Proof.
intros sigma1 sigma2 t; pattern t; apply term_rec3; clear t.
intro v; unfold subst_comp;
simpl; rewrite subst_comp_is_subst_comp_aux2;
do 2 rewrite subst_comp_is_subst_comp_aux1;
destruct (find eq_variable_dec v sigma2); trivial; simpl;
destruct (find eq_variable_dec v sigma1); trivial.
intros f l IH; simpl; apply (f_equal (fun l => Term f l));
induction l as [ | a l]; trivial.
simpl; rewrite (IH a).
rewrite IHl; trivial.
intros; apply IH; right; trivial.
left; trivial.
Qed.
Well-formed substitutions.
Definition well_formed_subst sigma :=
forall v, match find eq_variable_dec v sigma with
| None => True
| Some t => well_formed t
end.
Theorem well_formed_apply_subst :
forall sigma, well_formed_subst sigma ->
forall t, well_formed t -> well_formed (apply_subst sigma t).
Proof.
intros sigma W_sigma t; pattern t;
apply term_rec3.
intros v _; simpl; generalize (W_sigma v);
destruct (find eq_variable_dec v sigma); trivial.
intros f l Hrec [Wl A]; split.
clear A; induction l as [ | a l]; simpl; trivial;
inversion_clear Wl as [Wa Wl']; split.
apply Hrec; trivial; left; trivial.
apply IHl; trivial; intros; apply Hrec; trivial; right; trivial.
rewrite length_map; trivial.
Qed.
Fixpoint is_a_pos (t : term) (p : list nat) {struct p}: bool :=
match p with
| nil => true
| i :: q =>
match t with
| Var _ => false
| Term _ l =>
match nth_error l i with
| Some ti => is_a_pos ti q
| None => false
end
end
end.
Fixpoint subterm_at_pos (t : term) (p : list nat) {struct p}: option term :=
match p with
| nil => Some t
| i :: q =>
match t with
| Var _ => None
| Term _ l =>
match nth_error l i with
| Some ti => subterm_at_pos ti q
| None => None
end
end
end.
Lemma size_subterm_at_pos :
forall t i p, match subterm_at_pos t (i :: p) with
| Some u => size u < size t
| None => True
end.
Proof.
intros t i p; generalize t i; clear t i; induction p as [ | j p].
intros [ v | f l ] j; simpl subterm_at_pos; cbv iota beta; trivial.
generalize (nth_error_ok_in j l); destruct (nth_error l j) as [tj | ]; [idtac | trivial].
intro H; apply size_direct_subterm; simpl; apply H; trivial.
intros [ v | f l ] i; simpl subterm_at_pos; cbv iota beta; trivial.
generalize (nth_error_ok_in i l); destruct (nth_error l i) as [ti | ]; [idtac | trivial].
intro ti_in_l; generalize (IHp ti j); simpl subterm_at_pos;
destruct ti as [vi | fi li]; trivial.
generalize (nth_error_ok_in j li); destruct (nth_error li j) as [tij | ]; [idtac | trivial].
intro tij_in_li; destruct (subterm_at_pos tij p) as [ u | ]; trivial.
intro H; apply lt_trans with (size (Term fi li)); trivial.
apply size_direct_subterm; simpl; apply ti_in_l; trivial.
Qed.
Lemma is_a_pos_exists_subtem :
forall t p, is_a_pos t p = true -> exists u, subterm_at_pos t p = Some u.
Proof.
intros t p; generalize t; clear t; induction p as [ | i q ].
intros t _; exists t; trivial.
intros t; destruct t as [ x | f l ]; simpl.
intros; discriminate.
destruct (nth_error l i) as [ ti | ].
intro; apply IHq; trivial.
intros; discriminate.
Qed.
Fixpoint replace_at_pos (t u : term) (p : list nat) {struct p} : term :=
match p with
| nil => u
| i :: q =>
match t with
| Var _ => t
| Term f l =>
let replace_at_pos_list :=
(fix replace_at_pos_list j (l : list term) {struct l}: list term :=
match l with
| nil => nil
| h :: tl =>
match j with
| O => (replace_at_pos h u q) :: tl
| S k => h :: (replace_at_pos_list k tl)
end
end) in
Term f (replace_at_pos_list i l)
end
end.
Fixpoint replace_at_pos_list (l : list term) (u : term) (i : nat) (p : list nat)
{struct l}: list term :=
match l with
| nil => nil
| h :: tl =>
match i with
| O => (replace_at_pos h u p) :: tl
| S j => h :: (replace_at_pos_list tl u j p)
end
end.
Lemma replace_at_pos_unfold :
forall f l u i q,
replace_at_pos (Term f l) u (i :: q) = Term f (replace_at_pos_list l u i q).
Proof.
intros f l u i q; simpl; apply (f_equal (fun l => Term f l));
generalize u i q; clear u i q;
induction l as [| t l]; intros u i q; trivial.
simpl; destruct i as [ | i ]; trivial.
rewrite <- IHl; trivial.
Qed.
Lemma replace_at_pos_is_replace_at_pos1 :
forall t u p, is_a_pos t p = true ->
subterm_at_pos (replace_at_pos t u p) p = Some u.
Proof.
intro t; pattern t; apply term_rec3; clear t.
intros x u p; destruct p as [ | i q ]; trivial;
intros; discriminate.
intros f l IHl u p; destruct p as [ | i q ]; trivial.
rewrite replace_at_pos_unfold; simpl; generalize i q; clear i q;
induction l as [ | t l ]; intros i q.
destruct i as [ | i ]; simpl; intros; discriminate.
destruct i as [ | i ]; simpl.
intros; apply (IHl t); trivial; left; trivial.
intros; apply IHl0; intros; trivial; apply IHl; trivial; right; trivial.
Qed.
Lemma replace_at_pos_is_replace_at_pos2 :
forall t p u, subterm_at_pos t p = Some u -> replace_at_pos t u p = t.
Proof.
intro t; pattern t; apply term_rec3; clear t.
intros v p u; destruct p as [ | i q ]; intro H; inversion_clear H; trivial.
intros f l IHl p; destruct p as [ | i q ].
intros u H; inversion_clear H; trivial.
intros u H; rewrite replace_at_pos_unfold;
apply (f_equal (fun l => Term f l)); generalize i q u H; clear i q u H;
induction l as [ | t l ]; intros i q u H.
destruct i as [ | i ]; simpl; intros; discriminate.
destruct i as [ | i ]; simpl.
rewrite IHl; trivial; left; trivial.
rewrite IHl0; trivial; intros; apply IHl; trivial; right; trivial.
Qed.
Lemma subterm_at_pos_apply_subst_apply_subst_subterm_at_pos :
forall t p sigma,
match subterm_at_pos t p with
| Some u =>
subterm_at_pos (apply_subst sigma t) p = Some (apply_subst sigma u)
| None => True
end.
Proof.
intro t; pattern t; apply term_rec3; clear t.
intros v p; destruct p as [ | i q ]; simpl; trivial.
intros f l IHl p; destruct p as [ | i q ]; simpl; trivial.
assert (H : forall (l : list term) i,
match nth_error l i with
| Some li => In li l
| None => True end).
clear IHl l i; intro l;
induction l as [ | t l ]; intro i; destruct i as [ | i ]; simpl; trivial.
left; trivial.
generalize (IHl i); destruct (nth_error l i); trivial; intros; right; trivial.
generalize i; clear i; induction l as [ | l ll ];
intros i; destruct i as [ | i ]; simpl; trivial.
intros; apply IHl; left; trivial.
intro sigma; apply IHll; intros; apply IHl; right; trivial.
Qed.
Lemma replace_at_pos_list_replace_at_pos_in_subterm :
forall l1 ui l2 u i p, length l1 = i ->
replace_at_pos_list (l1 ++ ui :: l2) u i p =
l1 ++ (replace_at_pos ui u p) :: l2.
Proof.
intros l1; induction l1 as [ | u1 l1 ]; intros ui l2 u i p L; simpl in L.
subst i; trivial.
destruct i as [ | i ].
discriminate.
simpl; rewrite IHl1; trivial.
inversion L; trivial.
Qed.
End Make.