Library term_algebra.term
Add LoadPath "basis".
Add LoadPath "list_extensions".
Require Import Recdef.
Require Import List.
Require Import closure.
Require Import more_list.
Require Import list_permut.
Require Import list_set.
Require Import Arith.
Require Import decidable_set.
Set Implicit Arguments.
The arity of a symbol contains the information about built-in theories as in CiME
Inductive arity_type : Set :=
| AC : arity_type
| C : arity_type
| Free : nat -> arity_type.
Module Type Signature.
There are almost no assumptions, except a decidable equality and an arity function.
Module Type Signature.
Declare Module Export Symb : decidable_set.S.
Parameter arity : Symb.A -> arity_type.
End Signature.
Module Type Term.
Declare Module Import F : Signature.
Declare Module Import X : decidable_set.S.
Notation symbol := Symb.A.
Notation eq_symbol_dec := Symb.eq_dec.
Notation variable := X.A.
Notation eq_variable_dec := X.eq_dec.
Declare Module VSet :
list_set.S with Definition EDS.A := X.A
with Definition EDS.eq_A := @eq X.A.
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.
Fixpoint var_list (t : term) : list variable :=
match t with
| Var x => (x :: nil)
| Term _ l =>
let var_list_list :=
(fix var_list_list (l : list term) {struct l} : list variable :=
match l with
| nil => @nil _
| t :: lt => var_list t ++ var_list_list lt
end) in
var_list_list l
end.
Fixpoint var_list_list (l : list term) {struct l} : list variable :=
match l with
| nil => nil
| t :: lt => var_list t ++ var_list_list lt
end.
Axiom var_list_unfold :
forall t,
var_list t = match t with
| Var x => (x :: nil)
| Term _ l => var_list_list l
end.
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 _ l =>
let size_list :=
(fix size_list (l : list term) {struct l} : nat :=
match l with
| nil => 0
| t :: lt => size t + size_list lt
end) in
1 + size_list l
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.
Fixpoint symb_in_term (f : symbol) (t:term) : bool :=
match t with
| Var _ => false
| Term g l =>
let symb_in_term_list :=
(fix symb_in_term_list f (l : list term) {struct l} : bool :=
match l with
| nil => false
| t :: lt => Bool.orb (symb_in_term f t) (symb_in_term_list f lt)
end) in
if (F.Symb.eq_dec f g)
then true
else symb_in_term_list f l
end.
Fixpoint symb_in_term_list f (l : list term) {struct l} : bool :=
match l with
| nil => false
| t :: lt => Bool.orb (symb_in_term f t) (symb_in_term_list f lt)
end.
Axiom symb_in_term_unfold :
forall f t, symb_in_term f t = match t with
| Var _ => false
| Term g l => if (F.Symb.eq_dec f g) then true else (symb_in_term_list f l)
end.
Axiom symb_in_term_list_app :
forall f l1 l2, symb_in_term_list f (l1 ++ l2) =
Bool.orb (symb_in_term_list f l1) (symb_in_term_list f l2).
Axiom symb_in_direct_subterm :
forall f l t g, In t l -> symb_in_term g t = true ->
symb_in_term g (Term f l) = true.
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}.
Axiom term_term_dec : forall x y:term*term, {x=y}+{~x=y}.
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 subterm_at_pos_dec :
forall t s, {p : list nat | subterm_at_pos t p = Some s}+{forall p, subterm_at_pos t p <> Some s}.
Axiom subterm_subterm :
forall t p s, subterm_at_pos t p = Some s -> (t=s) \/ (trans_clos direct_subterm s t).
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 var_in_subterm :
forall v s t p, subterm_at_pos t p = Some s -> In v (var_list s) -> In v (var_list t).
Axiom var_in_subterm2 :
forall v t, In v (var_list t) -> exists p, subterm_at_pos t p = Some (Var v).
Axiom symb_in_subterm :
forall f s t p, subterm_at_pos t p = Some s -> symb_in_term f s = true -> symb_in_term f t = true.
Axiom is_a_pos_exists_subterm :
forall t p, is_a_pos t p = true -> exists u, subterm_at_pos t p = Some u.
Axiom exists_subterm_is_a_pos :
forall t p u, subterm_at_pos t p = Some u -> is_a_pos t p = true.
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 replace_at_pos_replace_at_pos :
forall t p u u', replace_at_pos (replace_at_pos t u p) u' p = replace_at_pos t u' p.
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.
Axiom subterm_in_instantiated_term :
forall p s t sigma, subterm_at_pos (apply_subst sigma t) p = Some s ->
match subterm_at_pos t p with
| Some u' => s = apply_subst sigma u'
| None => exists v, exists q, exists q', p = q ++ q' /\
In v (var_list t) /\
subterm_at_pos t q = Some (Var v) /\
subterm_at_pos (apply_subst sigma (Var v)) q' = Some s
end.
Axiom subterm_in_subterm :
forall p q s t u, subterm_at_pos t p = Some s -> subterm_at_pos s q = Some u ->
subterm_at_pos t (p ++ q) = Some u.
Axiom subterm_in_subterm2 :
forall p q s t, subterm_at_pos t (p ++ q) = Some s ->
exists u, subterm_at_pos t p = Some u /\ subterm_at_pos u q = Some s.
Axiom replace_at_pos_in_replace_at_pos :
forall t s u p q, subterm_at_pos t p = Some s ->
replace_at_pos t u (p ++ q) =
replace_at_pos t (replace_at_pos s u q) p.
Fixpoint restrict_domain (lv : list variable) (sigma : substitution) {struct sigma} :=
match sigma with
| nil => nil
| (x,val) :: sigma' =>
if In_dec eq_variable_dec x lv
then (x,val) :: (restrict_domain lv sigma')
else restrict_domain lv sigma'
end.
Axiom restrict_domain_ok :
forall sigma lv t, (forall v, In v (var_list t) -> In v lv) ->
apply_subst sigma t = apply_subst (restrict_domain lv sigma) t.
Axiom restrict_domain_ok2 :
forall sigma lv x val, find eq_variable_dec x (restrict_domain lv sigma) = Some val ->
(In x lv /\ find eq_variable_dec x sigma = Some val).
Axiom remove_garbage_subst :
forall sigma : substitution ,
{sigma' : substitution | (forall x, find eq_variable_dec x sigma = find eq_variable_dec x sigma') /\
(forall x val, In (x,val) sigma' -> find eq_variable_dec x sigma' = Some val) /\
(forall x y val val' (tau tau' tau'' : substitution),
sigma' = tau ++ (x,val) :: tau' ++ (y,val') :: tau'' ->
x <> y)}.
Axiom subst_eq_vars :
forall t sigma sigma', (forall v, In v (var_list t) -> apply_subst sigma (Var v) = apply_subst sigma' (Var v))
<-> apply_subst sigma t = apply_subst sigma' t.
Axiom apply_subst_const :
forall t, var_list t = nil -> forall sigma, apply_subst sigma t = t.
Axiom matching : list (term * term) -> option substitution.
Axiom matching_unfold2 : forall pb,
matching pb =
match pb with
| nil => Some nil
| (patt, subj) :: pb =>
match patt with
| Var x =>
match matching pb with
| Some subst => merge X.eq_dec eq_term_dec ((x,subj) :: nil) subst
| None => None
end
| Term f l =>
match subj with
| Var _ => None
| Term g m =>
if F.Symb.eq_dec f g
then
match l with
| nil =>
match m with
| nil => matching pb
| sub1 :: lsub => None
end
| pat1 :: lpat =>
match m with
| nil => None
| sub1 :: lsub =>
match (matching ((pat1, sub1) :: nil)) with
| Some subst1 =>
match (matching ((Term f lpat, Term g lsub) :: pb)) with
| Some subst => merge X.eq_dec eq_term_dec subst1 subst
| None => None
end
| None => None
end
end
end
else None
end
end
end.
Axiom matching_correct :
forall pb sigma, matching pb = Some sigma ->
((forall v p s, In v (var_list p) -> In (p,s) pb -> find X.eq_dec v sigma <> None) /\
(forall v, find X.eq_dec v sigma <> None ->
exists p, exists s, In (p,s) pb /\ In v (var_list p)) /\
(forall p s, In (p,s) pb -> apply_subst sigma p = s)).
Axiom matching_complete :
forall pb sigma, (forall p s, In (p,s) pb -> apply_subst sigma p = s) ->
match matching pb with
| Some tau => forall v p s, In v (var_list p) -> In (p,s) pb ->
apply_subst tau (Var v) = apply_subst sigma (Var v)
| None => False
end.
End Term.
Module Make' (F1 : Signature) (X1 : decidable_set.S) <:
Term with Module F := F1 with Module X := X1.
Module Import F := F1.
Module Import X := X1.
Notation symbol := Symb.A.
Notation eq_symbol_dec := Symb.eq_dec.
Notation variable := X.A.
Notation eq_variable_dec := X.eq_dec.
Module EX := decidable_set.Convert (X).
Module VSet :
list_set.S with Definition EDS.A := X.A
with Definition EDS.eq_A := @eq X.A := list_set.Make (EX).
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.
Fixpoint var_list (t : term) : list variable :=
match t with
| Var x => (x :: nil)
| Term _ l =>
let var_list_list :=
(fix var_list_list (l : list term) {struct l} : list variable :=
match l with
| nil => nil
| t :: lt => var_list t ++ var_list_list lt
end) in
var_list_list l
end.
Fixpoint var_list_list (l : list term) {struct l} : list variable :=
match l with
| nil => nil
| t :: lt => var_list t ++ var_list_list lt
end.
Lemma var_list_unfold :
forall t,
var_list t = match t with
| Var x => (x :: nil)
| Term _ l => var_list_list l
end.
Proof.
intro t; destruct t as [x | f l]; trivial.
Qed.
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 _ l =>
let size_list :=
(fix size_list (l : list term) {struct l} : nat :=
match l with
| nil => 0
| t :: lt => size t + size_list lt
end) in
1 + size_list l
end.
Definition 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; apply (f_equal (fun n => S n)); induction l as [ | t l]; trivial.
simpl; rewrite IHl; trivial.
Defined.
Lemma size_ge_one : forall t, 1 <= size t.
Proof.
destruct t as [ x | f l ]; trivial.
rewrite size_unfold; auto with arith.
Qed.
Definition 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.
Defined.
Fixpoint symb_in_term (f : symbol) (t:term) : bool :=
match t with
| Var _ => false
| Term g l =>
let symb_in_term_list :=
(fix symb_in_term_list f (l : list term) {struct l} : bool :=
match l with
| nil => false
| t :: lt => Bool.orb (symb_in_term f t) (symb_in_term_list f lt)
end) in
if (F.Symb.eq_dec f g)
then true
else symb_in_term_list f l
end.
Fixpoint symb_in_term_list f (l : list term) {struct l} : bool :=
match l with
| nil => false
| t :: lt => Bool.orb (symb_in_term f t) (symb_in_term_list f lt)
end.
Lemma symb_in_term_unfold :
forall f t, symb_in_term f t = match t with
| Var _ => false
| Term g l => if (F.Symb.eq_dec f g) then true else (symb_in_term_list f l)
end.
Proof.
intros g t; destruct t as [x | f l]; trivial.
Qed.
Lemma symb_in_term_list_app :
forall f l1 l2, symb_in_term_list f (l1 ++ l2) =
Bool.orb (symb_in_term_list f l1) (symb_in_term_list f l2).
Proof.
intros f l1; induction l1 as [ | t l1]; intros l2.
simpl; trivial.
simpl; destruct (symb_in_term f t); simpl; trivial.
Qed.
Lemma symb_in_direct_subterm :
forall f l t g, In t l -> symb_in_term g t = true ->
symb_in_term g (Term f l) = true.
Proof.
intros f l t g t_in_l H.
rewrite symb_in_term_unfold.
destruct (Symb.eq_dec g f) as [_ | _]; trivial.
generalize t g t_in_l H; clear t g t_in_l H; induction l as [ | s l].
intros; contradiction.
simpl; intros t g [t_eq_s | t_in_l] H.
subst t.
rewrite H; trivial.
destruct (symb_in_term g s); trivial.
simpl; rewrite (IHl t); trivial.
Qed.
Definition eq_term_dec : forall t t':term, {t=t'}+{t<>t'}.
fix 1.
intro t;case t.
intros x t';case t'.
intros x';case (eq_variable_dec x x');intro Heq.
rewrite <- Heq;left;reflexivity.
right;intro abs;injection abs;intro Heq';elim Heq;exact Heq'.
intros f l';right;discriminate.
intros f l t';case t'.
intros x;right;discriminate.
intros f' l'.
case (eq_symbol_dec f f');intro Heq.
rewrite <- Heq.
2:right;intro abs;elim Heq;injection abs;auto.
assert ({l=l'}+{l<>l'}).
clear - eq_term_dec.
revert l l'.
fix eq_dec_list 1.
intros l l';case l.
case l'. left;reflexivity.
intros t l0;right;discriminate.
intros t l0.
case l'.
right;discriminate.
intros t' l'0.
case (eq_term_dec t t');intros t_eq_t'.
case (eq_dec_list l0 l'0);intros l_eq_l'.
left;rewrite <- t_eq_t';rewrite <- l_eq_l';reflexivity.
right;intro abs;elim l_eq_l';injection abs;auto.
right;intro abs;elim t_eq_t';injection abs;auto.
case H;intros l_eq_l'.
left;rewrite <- l_eq_l';reflexivity.
right;intro abs;elim l_eq_l';injection abs;auto.
Defined.
Definition term_term_dec : forall x y:term*term, {x=y}+{~x=y}.
intros [a b] [a' b'].
case (eq_term_dec a a').
case (eq_term_dec b b').
intros Heq1 Heq2;left;f_equal;assumption.
intros abs _;right;intro Heq;elim abs;injection Heq;intros;assumption.
intros abs;right;intro Heq;elim abs;injection Heq;intros;assumption.
Defined.
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.
Defined.
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 Hv Halg.
fix 1.
intro t;case t.
exact Hv.
intro a.
intro l. apply Halg.
revert l.
fix term_list_rec_3 1 .
intro l;case l.
simpl;intros t0 abs;elim abs.
intros t0 l0 t1 .
simpl.
intros H.
case (eq_term_dec t0 t1).
intros t_eq_t1.
rewrite <- t_eq_t1.
apply term_rec3.
intro t_eq_t1. assert (In t1 l0).
case H. intro abs;elim t_eq_t1;exact abs.
intro h;exact h.
apply term_list_rec_3 with l0.
exact H0.
Defined.
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.
Defined.
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.
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 Ar]; split; trivial.
clear Ar; 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 Ar]; split ; trivial; clear Ar; 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 Ar]; split.
clear Ar; 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 subterm_at_pos_dec :
forall t s, {p : list nat | subterm_at_pos t p = Some s}+{forall p, subterm_at_pos t p <> Some s}.
Proof.
fix 1.
intros t;case t;[intro x| intros f l].
(intro s;case s;[intro x'| intros f' l']).
case (eq_variable_dec x x');intro x_eq_x'.
rewrite <- x_eq_x';left;exists (@nil nat);reflexivity.
right;intro p;case p;simpl;[intro abs;elim x_eq_x';injection abs;auto|intros;discriminate].
right;intro p;case p;simpl;intros;discriminate.
intro s;case (eq_term_dec (Term f l) s);intro t_eq_t'.
rewrite <- t_eq_t'. left;exists (@nil nat);reflexivity.
assert (forall t, In t l -> forall s, {p : list nat | subterm_at_pos t p = Some s} +
{(forall p : list nat, subterm_at_pos t p <> Some s)}).
clear - subterm_at_pos_dec.
revert l.
fix subterm_at_pos_dec_list 1.
intro l;case l;[|intros t l'].
simpl;intros t abs;elim abs.
simpl;intros t' Hin.
case (eq_term_dec t t');intro t_eq_t'.
rewrite <- t_eq_t'.
apply subterm_at_pos_dec.
assert (In t' l').
case Hin.
intro abs;elim t_eq_t';exact abs.
intro h;exact h.
apply subterm_at_pos_dec_list with l'.
exact H.
assert (forall s,{n :nat & {t:term & {p | (nth_error l n) = Some t /\ subterm_at_pos t p = Some s}}} + {(forall t, In t l -> forall p, subterm_at_pos t p <> Some s)}).
clear -H.
revert l H;fix 1.
intro l;case l;[|intros t l'].
right;simpl;intros t abs;elim abs.
intros H s.
simpl in H.
case (H t (or_introl _ (refl_equal t)) s).
intro h. left;exists 0;exists t. case h.
intros p Hp;exists p;split;auto.
intros Ht.
assert ( {n:nat & {t : term &
{p : list nat | nth_error l' n = Some t /\ subterm_at_pos t p = Some s}}} +
{(forall t : term,
In t l' ->
forall p : list nat, subterm_at_pos t p <> Some s)}).
apply subterm_at_pos_dec.
intros t0 H0 s0.
apply H.
right;exact H0.
case H0.
intros [n [ t0 [p [h1 h2]]]].
left;exists (S n);exists t0;exists p.
split.
simpl;exact h1.
exact h2.
intro Hl'.
right.
simpl;intros t0 Hin p Hp.
case Hin;intro H'in.
red in Ht. apply Ht with p.
rewrite H'in;exact Hp.
red in Hl';apply Hl' with t0 p.
exact H'in.
exact Hp.
case (H0 s).
intros [n [t0 [ p [h1 h2]]]].
left;exists (n::p).
simpl.
rewrite h1;exact h2.
intros.
right;intro p;case p;simpl;intros.
intros abs;elim t_eq_t';injection abs;auto.
case_eq (nth_error l n0).
intros t0 H1.
apply n.
case (nth_error_ok_in _ _ H1).
intros l1 [l2 [_ h]].
rewrite h.
apply in_or_app;right;simpl;left;reflexivity.
intros;discriminate.
Defined.
Lemma subterm_subterm :
forall t p s, subterm_at_pos t p = Some s -> (t=s) \/ (trans_clos direct_subterm s t).
Proof.
intros t p; generalize t; clear t; induction p as [ | i p]; intros t s Sub; simpl in Sub.
injection Sub; intros; subst; left; trivial.
destruct t as [v | f l].
discriminate.
right; assert (H := nth_error_ok_in i l);
destruct (nth_error l i) as [ti | ].
destruct (H _ (refl_equal _)) as [l1 [l2 [L H']]].
destruct (IHp _ _ Sub) as [ti_eq_s | Subi].
subst; apply t_step; simpl; apply in_or_app; right; left; trivial.
apply trans_clos_is_trans with ti; trivial.
subst; apply t_step; simpl; apply in_or_app; right; left; trivial.
discriminate.
Qed.
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.
destruct (H tj (refl_equal _)) as [l1 [l2 [_ H']]]; subst l; simpl;
apply in_or_app; right; left; 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.
destruct (ti_in_l _ (refl_equal _)) as [l1 [l2 [_ H']]]; subst l; simpl;
apply in_or_app; right; left; trivial.
Qed.
Lemma var_in_subterm :
forall v s t p, subterm_at_pos t p = Some s -> In v (var_list s) -> In v (var_list t).
Proof.
intros v s t p; generalize s t; clear s t; induction p as [ | i p]; intros s t H v_in_s.
simpl in H; injection H; clear H; intros; subst; trivial.
simpl in H; destruct t as [ | g l].
discriminate.
assert (H' := nth_error_ok_in i l).
destruct (nth_error l i) as [ti | ].
destruct (H' _ (refl_equal _)) as [l1 [l2 [L H'']]]; subst l.
rewrite var_list_unfold.
clear H' L; induction l1 as [ | t1 l].
simpl; apply in_or_app; left; apply (IHp s ti); trivial.
simpl; apply in_or_app; right; apply IHl.
discriminate.
Qed.
Lemma var_in_subterm2 :
forall v t, In v (var_list t) -> exists p, subterm_at_pos t p = Some (Var v).
Proof.
intros v t; pattern t; apply term_rec3; clear t.
intros x [v_eq_x | v_in_nil]; [exists (@nil nat); subst; trivial | contradiction].
intros f l; rewrite var_list_unfold; simpl.
induction l as [ | t l]; intros IH v_in_l.
contradiction.
simpl in v_in_l; destruct (in_app_or _ _ _ v_in_l) as [v_in_t | v_in_l'].
destruct (IH t (or_introl _ (refl_equal _)) v_in_t) as [p Sub].
exists (0 :: p); simpl; trivial.
destruct (IHl (tail_prop _ IH) v_in_l') as [p Sub]; trivial.
destruct p as [ | i p]; simpl in Sub.
discriminate.
exists (S(i) :: p); simpl; trivial.
Qed.
Lemma symb_in_subterm :
forall f s t p, subterm_at_pos t p = Some s -> symb_in_term f s = true -> symb_in_term f t = true.
Proof.
intros f s t p; generalize s t; clear s t; induction p as [ | i p]; intros s t H f_in_s.
simpl in H; injection H; clear H; intros; subst; trivial.
simpl in H; destruct t as [ | g l].
discriminate.
assert (H' := nth_error_ok_in i l).
destruct (nth_error l i) as [ti | ].
destruct (H' _ (refl_equal _)) as [l1 [l2 [L H'']]]; subst l.
rewrite symb_in_term_unfold.
destruct (Symb.eq_dec f g); trivial.
rewrite symb_in_term_list_app.
destruct (symb_in_term_list f l1); simpl; trivial.
rewrite (IHp s ti); trivial.
discriminate.
Qed.
Lemma is_a_pos_exists_subterm :
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.
Lemma exists_subterm_is_a_pos :
forall t p u, subterm_at_pos t p = Some u -> is_a_pos t p = true.
Proof.
intro t; pattern t; apply term_rec3; clear t.
intros v [ | i p] u H; simpl in H; [simpl; trivial | discriminate].
intros f l IHl [ | i p] u H.
simpl; trivial.
simpl; simpl in H; assert (H1 := nth_error_ok_in i l).
destruct (nth_error l i) as [ ti | ].
destruct (H1 _ (refl_equal _)) as [l1 [l2 [L H2]]]; subst l.
apply IHl with u; trivial.
apply in_or_app; right; left; trivial.
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 replace_at_pos_replace_at_pos :
forall t p u u', replace_at_pos (replace_at_pos t u p) u' p = replace_at_pos t u' p.
Proof.
intro t; pattern t; apply term_rec3; clear t.
intros v [ | i p] u u'; simpl; trivial.
intros f l IH [ | i p] u u'.
simpl; trivial.
do 3 rewrite replace_at_pos_unfold.
apply (f_equal (fun l => Term f l)).
generalize i p; clear i p;
induction l as [ | t l ]; intros i p.
simpl; trivial.
destruct i as [ | i]; simpl.
rewrite IH; trivial; left; trivial.
rewrite IHl; trivial; intros; apply IH; 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.
Lemma subterm_in_instantiated_term :
forall p s t sigma, subterm_at_pos (apply_subst sigma t) p = Some s ->
match subterm_at_pos t p with
| Some u' => s = apply_subst sigma u'
| None => exists v, exists q, exists q', p = q ++ q' /\
In v (var_list t) /\
subterm_at_pos t q = Some (Var v) /\
subterm_at_pos (apply_subst sigma (Var v)) q' = Some s
end.
Proof.
intro p; induction p as [ | i p]; intros s t sigma Sub.
simpl in Sub; injection Sub; clear Sub; intros; subst; simpl; trivial.
simpl; simpl in Sub; destruct t as [v | f l].
exists v.
simpl in Sub; destruct (find eq_variable_dec v sigma) as [v_sigma | ].
exists (@nil nat); exists (i :: p); repeat split; trivial.
left; trivial.
discriminate.
simpl in Sub.
assert (H := nth_error_map (apply_subst sigma) l i).
destruct (nth_error (map (apply_subst sigma) l) i) as [ti_sigma | ].
assert (H' := nth_error_ok_in i l).
destruct (nth_error l i) as [ti | ].
destruct (H' _ (refl_equal _)) as [l1 [l2 [L H''']]]; clear H'; subst;
generalize (IHp _ _ _ Sub).
destruct (subterm_at_pos ti p) as [u | ]; trivial.
intros [v [q [q' [p_eq_qq' [v_in_ti [Sub' Sub'']]]]]].
exists v; exists (length l1 :: q); exists q'; repeat split; trivial.
subst p; trivial.
apply var_in_subterm with ti (length l1 :: nil); trivial.
simpl; rewrite nth_error_at_pos; trivial.
simpl; rewrite nth_error_at_pos; trivial.
contradiction.
discriminate.
Qed.
Lemma subterm_in_subterm :
forall p q s t u, subterm_at_pos t p = Some s -> subterm_at_pos s q = Some u ->
subterm_at_pos t (p ++ q) = Some u.
Proof.
intro p; induction p as [ | i p]; intros q s t u Sub1 Sub2.
simpl in Sub1; injection Sub1; clear Sub1; intros; subst; trivial.
simpl in Sub1; simpl; destruct t as [v | f l].
discriminate.
destruct (nth_error l i) as [ti | ].
apply IHp with s; trivial.
discriminate.
Qed.
Lemma subterm_in_subterm2 :
forall p q s t, subterm_at_pos t (p ++ q) = Some s ->
exists u, subterm_at_pos t p = Some u /\ subterm_at_pos u q = Some s.
Proof.
intro p; induction p as [ | i p]; intros q s t Sub.
exists t; split; trivial.
simpl in Sub; destruct t as [v | f l].
discriminate.
generalize (nth_error_ok_in i l); destruct (nth_error l i) as [ti | ].
intro H; destruct (H _ (refl_equal _)) as [l1 [l2 [L H']]]; clear H.
destruct (IHp q s ti Sub) as [u [Sub' H'']].
exists u; subst; simpl; rewrite nth_error_at_pos; split; trivial.
discriminate.
Qed.
Lemma replace_at_pos_in_replace_at_pos :
forall t s u p q, subterm_at_pos t p = Some s ->
replace_at_pos t u (p ++ q) =
replace_at_pos t (replace_at_pos s u q) p.
Proof.
intros t s u p; generalize t s u; clear t s u;
induction p as [ | i p]; intros t s u q Sub.
simpl in Sub; injection Sub; intros; subst; trivial.
destruct t as [ | f l ]; trivial.
simpl app; simpl in Sub; do 2 rewrite replace_at_pos_unfold.
apply (f_equal (fun l => Term f l)).
generalize i Sub; clear i Sub; induction l as [ | t l]; simpl; intros i Sub; trivial.
destruct i as [ | i]; simpl in Sub.
rewrite (IHp t s u q); trivial.
rewrite IHl; trivial.
Qed.
Fixpoint restrict_domain (lv : list variable) (sigma : substitution) {struct sigma} :=
match sigma with
| nil => nil
| (x,val) :: sigma' =>
if In_dec eq_variable_dec x lv
then (x,val) :: (restrict_domain lv sigma')
else restrict_domain lv sigma'
end.
Lemma restrict_domain_ok :
forall sigma lv t, (forall v, In v (var_list t) -> In v lv) ->
apply_subst sigma t = apply_subst (restrict_domain lv sigma) t.
Proof.
intros sigma lv t; pattern t; apply term_rec3; clear t.
intros v v_in_lv; induction sigma as [ | [x val] sigma]; simpl; trivial.
assert (v_in_lv' := v_in_lv v (or_introl _ (refl_equal _))).
destruct (eq_variable_dec v x) as [v_eq_x | v_diff_x].
subst x; destruct (In_dec eq_variable_dec v lv) as [_ | v_not_in_lv];
[simpl | absurd (In v lv); trivial].
destruct (eq_variable_dec v v) as [_ | v_diff_v]; [idtac | absurd (v = v)]; trivial.
simpl in IHsigma; rewrite IHsigma.
destruct (In_dec eq_variable_dec x lv) as [x_in_lv | x_not_in_lv]; simpl; trivial.
destruct (eq_variable_dec v x) as [v_eq_x | _]; [absurd (v = x) | idtac]; trivial.
intros f l IHl var_list_list_l_in_lv; simpl; apply (f_equal (fun l => Term f l)).
apply map_eq; intros t t_in_l; apply IHl; trivial.
intros v v_in_t; apply var_list_list_l_in_lv.
rewrite var_list_unfold; destruct (In_split _ _ t_in_l) as [l' [l'' H]]; subst l.
clear IHl var_list_list_l_in_lv t_in_l; induction l' as [ | t' l']; simpl.
apply in_or_app; left; trivial.
apply in_or_app; right; trivial.
Qed.
Lemma restrict_domain_ok2 :
forall sigma lv x val, find eq_variable_dec x (restrict_domain lv sigma) = Some val ->
(In x lv /\ find eq_variable_dec x sigma = Some val).
Proof.
intro sigma; induction sigma as [ | [x xval] sigma]; simpl; intros lv v vval H.
discriminate.
destruct (In_dec eq_variable_dec x lv) as [x_in_lv | x_not_in_lv].
simpl in H; destruct (eq_variable_dec v x) as [v_eq_x | v_diff_x].
subst; split; trivial.
apply IHsigma; trivial.
destruct (eq_variable_dec v x) as [v_eq_x | v_diff_x].
subst; destruct (IHsigma lv x vval H) as [x_in_lv _]; absurd (In x lv); trivial.
destruct (IHsigma lv v vval H) as [x_in_lv H']; split; trivial.
Qed.
Lemma remove_garbage_subst :
forall sigma : substitution,
{sigma' : substitution | (forall x, find eq_variable_dec x sigma = find eq_variable_dec x sigma') /\
(forall x val, In (x,val) sigma' -> find eq_variable_dec x sigma' = Some val) /\
(forall x y val val' (tau tau' tau'' : substitution),
sigma' = tau ++ (x,val) :: tau' ++ (y,val') :: tau'' ->
x <> y)}.
Proof.
intro sigma; induction sigma as [ | [x val] sigma].
exists (nil : substitution); repeat split; trivial.
intros; contradiction.
intros x y val val' [ | [z vl''] tau] tau' tau'' H; discriminate.
destruct IHsigma as [sigma' [H1 [H2 H3]]].
case_eq (find eq_variable_dec x sigma').
intros val' H; destruct (find_mem eq_variable_dec _ _ H) as [sigma1 [sigma2 H']].
exists ((x,val) :: sigma1 ++ sigma2); repeat split.
intros y; simpl; destruct (eq_variable_dec y x) as [y_eq_x | x_diff_y]; [trivial | idtac].
rewrite (H1 y); rewrite H'; clear sigma' H1 H2 H3 H H';
induction sigma1 as [ | [x1 val1] sigma1]; simpl.
destruct (eq_variable_dec y x) as [y_eq_x | _]; [absurd (y = x) | idtac]; trivial.
destruct (eq_variable_dec y x1) as [y_eq_x1 | y_diff_x1]; [idtac | apply IHsigma1]; trivial.
simpl; intros y val'' [H4 | H4].
injection H4; clear H4; intros; subst.
destruct (eq_variable_dec y y) as [_ | y_diff_y]; [idtac | absurd (y = y)]; trivial.
destruct (eq_variable_dec y x) as [y_eq_x | y_diff_x].
absurd (y = x); trivial.
destruct (in_app_or _ _ _ H4) as [H5 | H5];
destruct (In_split _ _ H5) as [tau1 [tau2 H6]]; subst.
apply (H3 x x val'' val' tau1 tau2 sigma2); rewrite <- ass_app; trivial.
apply (H3 x x val' val'' sigma1 tau1 tau2); trivial.
rewrite <- (H2 y val''); subst sigma'.
rewrite find_diff; trivial.
intro; subst y; absurd (x=x); trivial.
apply in_insert; trivial.
clear sigma H1 H2.
intros x1 y val1 valy [ | [z zval] tau] tau' tau''; simpl; intro H'';
simpl in H''; injection H''; clear H''; intros; subst.
assert (yvaly_in_sigma12 : In (y,valy) (sigma1 ++ sigma2)).
rewrite H0; apply in_or_app; right; left; trivial.
destruct (in_app_or _ _ _ yvaly_in_sigma12) as [yvaly_in_sigma1 | yvaly_in_sigma2].
destruct (In_split _ _ yvaly_in_sigma1) as [tau1 [tau2 H']].
intro x1_eq_y; apply (H3 y x1 valy val' tau1 tau2 sigma2); subst; trivial.
rewrite <- ass_app; trivial.
destruct (In_split _ _ yvaly_in_sigma2) as [tau1 [tau2 H']].
apply (H3 x1 y val' valy sigma1 tau1 tau2); subst; trivial.
destruct (insert_2 _ _ _ _ _ (z,val') _ _ H0) as [tau1 [tau2 [tau3 H4]]].
apply (H3 _ _ _ _ _ _ _ H4).
intro H4; exists ((x,val) :: sigma'); repeat split.
intros y; simpl; destruct (eq_variable_dec y x) as [y_eq_x | y_diff_x]; [idtac | apply H1]; trivial.
simpl; intros y valy [H | H].
injection H; clear H; intros; subst.
destruct (eq_variable_dec y y) as [_ | y_diff_y]; [idtac | absurd (y = y)]; trivial.
destruct (eq_variable_dec y x) as [y_eq_x | y_diff_x].
subst y; absurd (In (x,valy) sigma'); trivial;
apply find_not_found with eq_variable_dec; trivial.
apply H2; trivial.
intros y z valy valz [ | [u valu] tau] tau' tau'' H; simpl in H; injection H; clear H; intros; subst.
intro y_eq_z; subst y; apply (find_not_found eq_variable_dec _ valz _ H4).
apply in_or_app; right; left; trivial.
apply (H3 _ _ _ _ _ _ _ (refl_equal _)).
Qed.
Lemma subst_eq_vars :
forall t sigma sigma', (forall v, In v (var_list t) -> apply_subst sigma (Var v) = apply_subst sigma' (Var v))
<-> apply_subst sigma t = apply_subst sigma' t.
Proof.
intros t sigma sigma'; split.
pattern t; apply term_rec3; clear t.
intros v H; apply H; left; trivial.
intros f l IHl H.
simpl; apply (f_equal (fun l => Term f l)).
apply map_eq; intros t t_in_l; apply IHl; trivial.
intros v v_in_t; apply H.
destruct (In_split _ _ t_in_l) as [l1 [l2 H']]; subst.
apply var_in_subterm with t (length l1 :: nil); trivial.
simpl; rewrite nth_error_at_pos; trivial.
pattern t; apply term_rec3; clear t.
intros v H; simpl; intros x [x_eq_v | F]; [subst; trivial | contradiction].
intros f l IHl H; simpl in H; injection H; clear H; intro H.
intros v v_in_l; rewrite var_list_unfold in v_in_l; induction l as [ | t l].
contradiction.
simpl in H; injection H; clear H; intros H H'.
simpl in v_in_l.
destruct (in_app_or _ _ _ v_in_l) as [v_in_t | v_in_l'].
apply IHl with t; trivial.
left; trivial.
apply IHl0; trivial.
intros s s_in_l H'' x x_in_s; apply (IHl s); trivial.
right; trivial.
Qed.
Lemma apply_subst_const :
forall t, var_list t = nil -> forall sigma, apply_subst sigma t = t.
Proof.
intros t; pattern t; apply term_rec3; clear t.
intros v H; discriminate.
intros f l IHl H sigma.
simpl; apply (f_equal (fun l => Term f l)).
pattern l at 2; rewrite <- map_id.
apply map_eq; intros t t_in_l; apply IHl; trivial.
rewrite var_list_unfold in H; generalize t t_in_l; clear IHl sigma t t_in_l.
induction l as [ | a l].
intros; contradiction.
simpl; intros t [t_eq_a | t_in_l].
subst a; simpl in H; destruct (var_list t); trivial; discriminate.
apply IHl; trivial; simpl in H; destruct (var_list a); trivial; discriminate.
Qed.
Definition o_list_size pb1 pb2 :=
list_size (fun st => size (fst (B:=term) st)) pb1 <
list_size (fun st => size (fst (B:=term) st)) pb2.
Lemma wf_size : well_founded o_list_size.
Proof.
unfold well_founded, o_list_size.
intros pb; apply Acc_intro.
generalize (list_size (fun st : term * term => size (fst st)) pb); clear pb.
intro n; induction n as [ | n].
intros y Abs; absurd (list_size (fun st : term * term => size (fst st)) y < 0); auto with arith.
intros y Sy; inversion Sy; subst.
apply Acc_intro; intros x Sx; apply IHn; trivial.
apply IHn; trivial.
Defined.
Lemma matching_call1 :
forall patt subj pb, o_list_size pb ((patt, subj) :: pb).
Proof.
intros patt sibj pb;
unfold o_list_size; simpl.
pattern (list_size (fun st : term * term => size (fst st)) pb); rewrite <- plus_O_n.
apply plus_lt_compat_r.
unfold lt; apply size_ge_one; trivial.
Qed.
Lemma matching_call2 :
forall pat sub f lpat g lsub pb,
o_list_size ((pat,sub) :: nil) ((Term f (pat :: lpat), Term g (sub :: lsub)) :: pb).
Proof.
intros pat sub f lpat g lsub pb; unfold o_list_size; simpl.
auto with arith.
Qed.
Lemma matching_call3 :
forall pat sub f lpat g lsub pb,
o_list_size ((Term f lpat, Term g lsub):: pb) ((Term f (pat :: lpat), Term g (sub :: lsub)) :: pb).
Proof.
intros pat sub f lpat g lsub pb; unfold o_list_size; simpl.
apply lt_n_S.
rewrite <- plus_assoc.
pattern ((fix size_list (l : list term) : nat :=
match l with
| nil => 0
| t :: lt => size t + size_list lt
end) lpat + list_size (fun st : term * term => size (fst st)) pb);
rewrite <- plus_O_n.
apply plus_lt_compat_r.
unfold lt; apply size_ge_one; trivial.
Qed.
Definition F_matching:
forall pb (mrec : forall p, o_list_size p pb -> option substitution),
option substitution.
Proof.
intros [ | [patt subj] pb] mrec.
exact (Some nil).
assert (Size := matching_call1 patt subj pb).
destruct patt as [x | f l].
set (o_subst := mrec _ Size).
destruct o_subst as [subst | None].
exact (merge X.eq_dec eq_term_dec ((x,subj) :: nil) subst).
exact None.
destruct subj as [x | g m].
exact None.
destruct (F.Symb.eq_dec f g) as [f_eq_g | f_diff_g].
destruct l as [ | pat lpat]; destruct m as [ | sub lsub].
set (o_subst := mrec _ Size).
destruct o_subst as [subst | None].
exact (Some subst).
exact None.
exact None.
exact None.
assert (Size1 := matching_call2 pat sub f lpat g lsub pb).
set (o_subst1 := mrec _ Size1).
destruct o_subst1 as [subst1 | ].
assert (Size2 :=matching_call3 pat sub f lpat g lsub pb).
set (o_subst2 := mrec _ Size2).
destruct o_subst2 as [subst2 | ].
exact (merge X.eq_dec eq_term_dec subst1 subst2).
exact None.
exact None.
exact None.
Defined.
Definition matching : list (term * term) -> option substitution :=
Fix wf_size (fun l => option substitution) F_matching.
Lemma matching_unfold :
forall l : list (term*term), matching l = @F_matching l (fun y _ => matching y).
Proof.
intros lpb; unfold matching.
refine (Fix_eq _ _ _ _ lpb).
clear lpb; intros lpb F G H.
unfold F_matching; destruct lpb as [ | [patt subj] lpb]; simpl; auto.
destruct patt as [x | f l]; destruct subj as [y | g m]; simpl; auto.
rewrite H; trivial.
rewrite H; trivial.
destruct (F.Symb.eq_dec f g); trivial.
destruct l as [ | pat lpat]; destruct m as [ | sub lsub]; trivial.
rewrite H; trivial.
do 2 rewrite H; trivial.
Qed.
Lemma matching_unfold2 : forall pb,
matching pb =
match pb with
| nil => Some nil
| (patt, subj) :: pb =>
match patt with
| Var x =>
match matching pb with
| Some subst => merge X.eq_dec eq_term_dec ((x,subj) :: nil) subst
| None => None
end
| Term f l =>
match subj with
| Var _ => None
| Term g m =>
if F.Symb.eq_dec f g
then
match l with
| nil =>
match m with
| nil => matching pb
| sub1 :: lsub => None
end
| pat1 :: lpat =>
match m with
| nil => None
| sub1 :: lsub =>
match (matching ((pat1, sub1) :: nil)) with
| Some subst1 =>
match (matching ((Term f lpat, Term g lsub) :: pb)) with
| Some subst => merge X.eq_dec eq_term_dec subst1 subst
| None => None
end
| None => None
end
end
end
else None
end
end
end.
Proof.
intros pb; rewrite matching_unfold; unfold F_matching; simpl.
destruct pb as [ | [patt subj] pb]; trivial.
destruct patt as [ x | f l]; trivial.
destruct subj as [x | g m]; trivial.
destruct (F.Symb.eq_dec f g) as [f_eq_g | f_diff_g]; trivial.
destruct l as [ | pat1 lpat]; destruct m as [ | sub1 lsub]; trivial.
destruct (matching pb); trivial.
Qed.
Lemma matching_correct_aux :
forall pb sigma, matching pb = Some sigma ->
((forall v t1 t2, In (v,t1) sigma -> In (v,t2) sigma -> t1 = t2) /\
(forall v p s, In v (var_list p) -> In (p,s) pb -> find X.eq_dec v sigma <> None) /\
(forall v, find X.eq_dec v sigma <> None ->
exists p, exists s, In (p,s) pb /\ In v (var_list p)) /\
(forall p s, In (p,s) pb -> apply_subst sigma p = s)).
Proof.
intro pb; pattern pb; apply (well_founded_ind wf_size); clear pb.
intros [ | [patt subj] pb] IH sigma H; rewrite matching_unfold2 in H.
injection H; clear H; intros; subst; repeat split; trivial;
intros; try contradiction.
simpl in H; absurd (@None term = None); trivial.
destruct patt as [ x | f l].
assert (H' := IH _ (matching_call1 _ _ _)).
destruct (matching pb) as [subst | ].
generalize (H' _ (refl_equal _)); clear H'; intros [IH1 [IH2 [IH4 IH3]]].
assert (H' := merge_correct X.eq_dec eq_term_dec ((x,subj) :: nil) subst IH1).
rewrite H in H'; destruct H' as [H1 [H2 H3]].
split.
intros v t1 t2 Ht1 Ht2.
assert (H'' := merge_inv X.eq_dec eq_term_dec ((x,subj) :: nil) subst).
rewrite H in H''.
apply H'' with v; trivial.
intros w u1 u2 [wu1_eq_xs | wu1_in_nil] [wu2_eq_xs | wu2_in_nil]; try contradiction.
injection wu1_eq_xs; intros; subst;
injection wu2_eq_xs; intros; subst; trivial.
split.
intros v p s v_in_p [ps_eq_xsubj | ps_in_pb].
injection ps_eq_xsubj; clear ps_eq_xsubj; intros; subst; simpl.
destruct v_in_p as [v_eq_x | v_in_nil]; [subst v | contradiction].
rewrite (H1 x s).
discriminate.
simpl; destruct (X.eq_dec x x) as [_ | x_diff_x]; trivial; absurd (x=x); trivial.
assert (K2 := IH2 v p s v_in_p ps_in_pb).
case_eq (find eq_variable_dec v subst).
intros v_subst H'.
rewrite (H2 _ _ H'); discriminate.
intros H'; rewrite H' in K2; absurd (@None term = None); trivial.
split.
intros v H'; assert (H3v := H3 v).
destruct (find eq_variable_dec v sigma) as [v_sigma | ].
destruct (H3v v_sigma (refl_equal _)) as [case1 | case2].
simpl in case1; destruct (eq_variable_dec v x) as [v_eq_x | v_diff_x].
subst v; exists (Var x); exists subj; split; left; trivial.
discriminate.
destruct (IH4 v) as [p [s [ps_in_pb v_in_p]]].
rewrite case2; discriminate.
exists p; exists s; split; trivial; right; trivial.
absurd (@None term = None); trivial.
intros p s [ps_eq_xsubj | ps_in_pb].
assert (K1 := H1 x subj).
injection ps_eq_xsubj; clear ps_eq_xsubj; intros; subst; simpl.
rewrite K1; trivial.
simpl; destruct (X.eq_dec x x) as [_ | x_diff_x]; trivial; absurd (x=x); trivial.
assert (K2 : forall v, In v (var_list p) -> find eq_variable_dec v subst <> None).
intros v v_in_p; apply IH2 with p s; trivial.
assert (KK2 : forall v, In v (var_list p) -> apply_subst subst (Var v) = apply_subst sigma (Var v)).
intros v v_in_p; generalize (K2 v v_in_p) (H2 v); simpl.
destruct (find eq_variable_dec v subst) as [v_subst | ].
clear K2; intros _ K2; rewrite (K2 _ (refl_equal _)); trivial.
intro; absurd (@None term = None); trivial.
rewrite <- (IH3 _ _ ps_in_pb).
symmetry.
generalize KK2; clear s ps_in_pb K2 KK2; pattern p; apply term_rec3; clear p.
intros v KK2; apply KK2; left; trivial.
intros f l IHl KK2.
assert (IHl' : forall t, In t l -> apply_subst subst t = apply_subst sigma t).
intros t t_in_l; apply IHl; trivial.
intros v v_in_t; apply KK2.
destruct (In_split _ _ t_in_l) as [l1 [l2 H']]; subst l.
apply (@var_in_subterm v t (Term f (l1 ++ t :: l2)) (length l1 :: nil)); trivial.
simpl; rewrite nth_error_at_pos; trivial.
simpl; apply (f_equal (fun l => Term f l)).
apply map_eq; trivial.
discriminate.
destruct subj as [x | g m].
discriminate.
destruct (Symb.eq_dec f g) as [f_eq_g | f_diff_g].
destruct l as [ | pat1 lpat]; destruct m as [ | sub1 lsub].
destruct (IH _ (matching_call1 _ _ _) sigma H) as [H1 [H2 [H4 H3]]].
split; trivial.
split.
intros v p s v_in_p [ps_eq_ff | ps_in_pb].
injection ps_eq_ff; intros; subst.
contradiction.
apply H2 with p s; trivial.
split.
intros v H'; destruct (H4 _ H') as [p [s [ps_in_pb v_in_p]]].
exists p; exists s; split; trivial; right; trivial.
intros p s [ps_eq_ff | ps_in_pb].
injection ps_eq_ff; intros; subst; simpl; trivial.
apply H3; trivial.
discriminate.
discriminate.
assert (H' := IH _ (matching_call2 pat1 sub1 f lpat g lsub pb)).
destruct (matching ((pat1,sub1) :: nil)) as [subst1 | ].
generalize (H' _ (refl_equal _)); clear H'; intros [IH1 [IH2 [IH4 IH3]]].
assert (H' := IH _ (matching_call3 pat1 sub1 f lpat g lsub pb)).
destruct (matching ((Term f lpat, Term g lsub) :: pb)) as [subst | ].
generalize (H' _ (refl_equal _)); clear H'; intros [IH1' [IH2' [IH4' IH3']]].
assert (H' := merge_correct X.eq_dec eq_term_dec subst1 subst IH1').
rewrite H in H'; destruct H' as [H1 [H2 H3]].
split.
intros v t1 t2 Ht1 Ht2.
assert (H'' := merge_inv X.eq_dec eq_term_dec subst1 subst).
rewrite H in H''.
apply H'' with v; trivial.
split.
intros v p s v_in_p [ps_eq_patsub | ps_in_pb].
injection ps_eq_patsub; clear ps_eq_patsub; intros; subst; simpl.
simpl in v_in_p; destruct (in_app_or _ _ _ v_in_p) as [v_in_pat1 | v_in_lpat].
assert (K2 := IH2 v pat1 sub1 v_in_pat1 (or_introl _ (refl_equal _))).
case_eq (find eq_variable_dec v subst1).
intros v_subst H'.
rewrite (H1 _ _ H'); discriminate.
intros H'; rewrite H' in K2; absurd (@None term = None); trivial.
assert (K2 := IH2' v (Term g lpat) (Term g lsub) v_in_lpat (or_introl _ (refl_equal _))).
case_eq (find eq_variable_dec v subst).
intros v_subst H'.
rewrite (H2 _ _ H'); discriminate.
intros H'; rewrite H' in K2; absurd (@None term = None); trivial.
assert (K2 := IH2' v p s v_in_p (or_intror _ ps_in_pb)).
case_eq (find eq_variable_dec v subst).
intros v_subst H'.
rewrite (H2 _ _ H'); discriminate.
intros H'; rewrite H' in K2; absurd (@None term = None); trivial.
split.
intros v H'; assert (H3v := H3 v).
destruct (find eq_variable_dec v sigma) as [v_sigma | ].
destruct (H3v v_sigma (refl_equal _)) as [case1 | case2].
destruct (IH4 v) as [p [s [ps_in_pb v_in_p]]].
rewrite case1; discriminate.
exists (Term f (pat1 :: lpat)); exists (Term g (sub1 :: lsub)); split.
left; trivial.
destruct ps_in_pb as [ps_eq_pat1sub1 | ps_in_nil].
injection ps_eq_pat1sub1; clear ps_eq_pat1sub1; intros; subst p s.
simpl; apply in_or_app; left; trivial.
contradiction.
destruct (IH4' v) as [p [s [ps_in_pb v_in_p]]].
rewrite case2; discriminate.
destruct ps_in_pb as [ps_eq_patsub | ps_in_pb].
exists (Term f (pat1 :: lpat)); exists (Term g (sub1 :: lsub)); split.
left; trivial.
injection ps_eq_patsub; clear ps_eq_patsub; intros; subst p s.
simpl; apply in_or_app; right; trivial.
exists p; exists s; split; trivial; right; trivial.
absurd (@None term = None); trivial.
intros p s [ps_eq_patsub | ps_in_pb].
injection ps_eq_patsub; clear ps_eq_patsub; intros; subst; simpl.
replace (apply_subst sigma pat1) with sub1.
apply (f_equal (fun l => Term g (sub1 :: l))).
assert (K := IH3' _ _ (or_introl _ (refl_equal _))).
simpl in K; injection K; clear K; intro K.
rewrite <- K; symmetry; apply map_eq.
intros p p_in_lpat.
assert (K2 : forall v, In v (var_list p) -> find eq_variable_dec v subst <> None).
intros v v_in_p; apply IH2' with (Term g lpat) (Term g lsub); trivial.
destruct (In_split _ _ p_in_lpat) as [lpat1 [lpat2 H']]; subst lpat.
apply (@var_in_subterm v p (Term g (lpat1 ++ p :: lpat2)) (length lpat1 :: nil)); trivial.
simpl; rewrite nth_error_at_pos; trivial.
left; trivial.
assert (KK2 : forall v, In v (var_list p) -> apply_subst subst (Var v) = apply_subst sigma (Var v)).
intros v v_in_p; generalize (K2 v v_in_p) (H2 v); simpl.
destruct (find eq_variable_dec v subst) as [v_subst | ].
clear K2; intros _ K2; rewrite (K2 _ (refl_equal _)); trivial.
intro; absurd (@None term = None); trivial.
generalize KK2; clear p_in_lpat K2 KK2; pattern p; apply term_rec3; clear p.
intros v KK2; apply KK2; left; trivial.
intros f l IHl KK2.
assert (IHl' : forall t, In t l -> apply_subst subst t = apply_subst sigma t).
intros t t_in_l; apply IHl; trivial.
intros v v_in_t; apply KK2.
destruct (In_split _ _ t_in_l) as [l1 [l2 H']]; subst l.
apply (@var_in_subterm v t (Term f (l1 ++ t :: l2)) (length l1 :: nil)); trivial.
simpl; rewrite nth_error_at_pos; trivial.
simpl; apply (f_equal (fun l => Term f l)).
apply map_eq; trivial.
assert (K := IH3 _ _ (or_introl _ (refl_equal _))).
simpl in K; injection K; clear K; intro K.
rewrite <- K; symmetry.
assert (K2 : forall v, In v (var_list pat1) -> find eq_variable_dec v subst1 <> None).
intros v v_in_pat1; apply IH2 with pat1 sub1; trivial.
left; trivial.
assert (KK2 : forall v, In v (var_list pat1) -> apply_subst subst1 (Var v) = apply_subst sigma (Var v)).
intros v v_in_pat1; generalize (K2 v v_in_pat1) (H1 v); simpl.
destruct (find eq_variable_dec v subst1) as [v_subst1 | ].
clear K2; intros _ K2; rewrite (K2 _ (refl_equal _)); trivial.
intro; absurd (@None term = None); trivial.
symmetry;
generalize KK2; clear K2 KK2 IH2 IH3 IH4 IH K; pattern pat1; apply term_rec3; clear pat1.
intros v KK2; apply KK2; left; trivial.
intros f l IHl KK2.
assert (IHl' : forall t, In t l -> apply_subst subst1 t = apply_subst sigma t).
intros t t_in_l; apply IHl; trivial.
intros v v_in_t; apply KK2.
destruct (In_split _ _ t_in_l) as [l1 [l2 H']]; subst l.
apply (@var_in_subterm v t (Term f (l1 ++ t :: l2)) (length l1 :: nil)); trivial.
simpl; rewrite nth_error_at_pos; trivial.
simpl; apply (f_equal (fun l => Term f l)).
apply map_eq; trivial.
assert (K2 : forall v, In v (var_list p) -> find eq_variable_dec v subst <> None).
intros v v_in_p; apply IH2' with p s; trivial; right; trivial.
assert (KK2 : forall v, In v (var_list p) -> apply_subst subst (Var v) = apply_subst sigma (Var v)).
intros v v_in_p; generalize (K2 v v_in_p) (H2 v); simpl.
destruct (find eq_variable_dec v subst) as [v_subst | ].
clear K2; intros _ K2; rewrite (K2 _ (refl_equal _)); trivial.
intro; absurd (@None term = None); trivial.
rewrite <- (IH3' _ _ (or_intror _ ps_in_pb)).
symmetry.
generalize KK2; clear s ps_in_pb K2 KK2; pattern p; apply term_rec3; clear p.
intros v KK2; apply KK2; left; trivial.
intros f' l IHl KK2.
assert (IHl' : forall t, In t l -> apply_subst subst t = apply_subst sigma t).
intros t t_in_l; apply IHl; trivial.
intros v v_in_t; apply KK2.
destruct (In_split _ _ t_in_l) as [l1 [l2 H']]; subst l.
apply (@var_in_subterm v t (Term f' (l1 ++ t :: l2)) (length l1 :: nil)); trivial.
simpl; rewrite nth_error_at_pos; trivial.
simpl; apply (f_equal (fun l => Term f' l)).
apply map_eq; trivial.
discriminate.
discriminate.
discriminate.
Qed.
Lemma matching_correct :
forall pb sigma, matching pb = Some sigma ->
((forall v p s, In v (var_list p) -> In (p,s) pb -> find X.eq_dec v sigma <> None) /\
(forall v, find X.eq_dec v sigma <> None ->
exists p, exists s, In (p,s) pb /\ In v (var_list p)) /\
(forall p s, In (p,s) pb -> apply_subst sigma p = s)).
Proof.
intros pb sigma H; generalize (matching_correct_aux pb H); intuition.
Qed.
Lemma matching_complete :
forall pb sigma, (forall p s, In (p,s) pb -> apply_subst sigma p = s) ->
match matching pb with
| Some tau => forall v p s, In v (var_list p) -> In (p,s) pb ->
apply_subst tau (Var v) = apply_subst sigma (Var v)
| None => False
end.
Proof.
intro pb; pattern pb; apply (well_founded_ind wf_size); clear pb.
intros [ | [patt subj] pb] IH sigma H;
rewrite matching_unfold2.
intros; contradiction.
destruct patt as [ x | f l].
assert (H' := IH _ (matching_call1 _ _ _)).
assert (Correct' := matching_correct_aux pb).
case_eq (matching pb).
intros subst matching_pb_eq_subst.
destruct (Correct' _ matching_pb_eq_subst) as [C1 [C2 [C4 C3]]]; clear Correct'.
assert (H'' := merge_correct X.eq_dec eq_term_dec ((x,subj) :: nil) subst C1).
case_eq (merge eq_variable_dec eq_term_dec ((x, subj) :: nil) subst).
intros tau matching_pb_eq_tau; rewrite matching_pb_eq_tau in H''.
destruct H'' as [H1 [H2 H3]].
intros v p s v_in_p [ps_eq_xsubj | ps_in_pb].
injection ps_eq_xsubj; clear ps_eq_xsubj; intros; subst.
destruct v_in_p as [v_eq_x | v_in_nil]; [idtac | contradiction].
subst v; rewrite (H (Var x) s (or_introl _ (refl_equal _))).
simpl; rewrite (H1 x s); trivial.
simpl; destruct (X.eq_dec x x) as [_ | x_diff_x]; trivial; absurd (x=x); trivial.
assert (tailH : forall p s, In (p,s) pb -> apply_subst sigma p = s).
intros; apply H; right; trivial.
assert (Hsigma := IH pb (matching_call1 (Var x) subj pb) sigma tailH).
rewrite matching_pb_eq_subst in Hsigma.
rewrite <- (Hsigma v p s v_in_p ps_in_pb).
simpl; assert (K2 := C2 v p s v_in_p ps_in_pb).
case_eq (find eq_variable_dec v subst).
intros v_subst H''; rewrite (H2 _ _ H''); trivial.
intros H''; rewrite H'' in K2; absurd (@None term = None); trivial.
intro matching_pb_eq_none; rewrite matching_pb_eq_none in H''.
destruct H'' as [v [t1 [t2 [H1 [H2 t1_diff_t2]]]]].
destruct (C4 v) as [p [s [ps_in_pb v_in_p]]].
rewrite H2; discriminate.
assert (tailH : forall p s, In (p,s) pb -> apply_subst sigma p = s).
intros; apply H; right; trivial.
assert (Hsigma := IH pb (matching_call1 (Var x) subj pb) sigma tailH).
rewrite matching_pb_eq_subst in Hsigma.
assert (Hv := Hsigma v p s v_in_p ps_in_pb); simpl in Hv.
rewrite H2 in Hv.
simpl in H1; destruct (eq_variable_dec v x) as [v_eq_x | v_diff_x]; [idtac | discriminate].
subst v; injection H1; clear H1; intros; subst subj.
assert (Hv' := H (Var x) t1 (or_introl _ (refl_equal _))).
simpl in Hv'; rewrite Hv' in Hv.
absurd (t1 = t2); subst; trivial.
intro matching_pb_eq_none; rewrite matching_pb_eq_none in H'.
apply (H' sigma).
intros; apply H; right; trivial.
destruct subj as [x | g m].
assert (H' := H (Term f l) (Var x) (or_introl _ (refl_equal _))); simpl in H'.
discriminate.
destruct (Symb.eq_dec f g) as [f_eq_g | f_diff_g].
destruct l as [ | pat1 lpat]; destruct m as [ | sub1 lsub].
assert (tailH : forall p s, In (p,s) pb -> apply_subst sigma p = s).
intros; apply H; right; trivial.
assert (Hsigma := IH pb (matching_call1 _ _ pb) sigma tailH).
destruct (matching pb) as [tau | ].
intros v p s v_in_p [ps_eq_ff | ps_in_pb].
injection ps_eq_ff; intros; subst; simpl in v_in_p; contradiction.
apply Hsigma with p s; trivial.
contradiction.
assert (H' := H (Term f nil) (Term g (sub1 :: lsub)) (or_introl _ (refl_equal _))); simpl in H'.
discriminate.
assert (H' := H (Term f (pat1 :: lpat)) (Term g nil) (or_introl _ (refl_equal _))); simpl in H'.
discriminate.
assert (H' := IH _ (matching_call2 pat1 sub1 f lpat g lsub pb)).
assert (Correct := matching_correct_aux ((pat1,sub1) :: nil)).
case_eq (matching ((pat1,sub1) :: nil)).
intros subst1 matching_pat1sub1_eq_subst1.
destruct (Correct _ matching_pat1sub1_eq_subst1) as [C1 [C2 [C4 C3]]]; clear Correct.
assert (H'' := IH _ (matching_call3 pat1 sub1 f lpat g lsub pb)).
assert (Correct' := matching_correct_aux ((Term f lpat, Term g lsub) :: pb)).
case_eq (matching ((Term f lpat, Term g lsub) :: pb)).
intros subst matching_pb_eq_subst.
destruct (Correct' _ matching_pb_eq_subst) as [C1' [C2' [C4' C3']]]; clear Correct'.
assert (H''' := merge_correct X.eq_dec eq_term_dec subst1 subst C1').
assert (headH : forall p s, In (p,s) ((pat1,sub1) :: nil) -> apply_subst sigma p = s).
intros p s [ps_eq_pat1sub1 | ps_in_nil]; [idtac | contradiction].
injection ps_eq_pat1sub1; clear ps_eq_pat1sub1; intros; subst p s.
assert (K := H _ _ (or_introl _ (refl_equal _))).
simpl in K; injection K; intros; subst; trivial.
assert (Hsigma1 := IH _ (matching_call2 pat1 sub1 f lpat g lsub pb) sigma headH).
rewrite matching_pat1sub1_eq_subst1 in Hsigma1.
assert (tailH : forall p s, In (p,s) ((Term f lpat, Term g lsub) :: pb) -> apply_subst sigma p = s).
intros p s [ps_eq_patsub | ps_in_pb].
injection ps_eq_patsub; clear ps_eq_patsub; intros; subst p s.
assert (K := H _ _ (or_introl _ (refl_equal _))).
simpl in K; injection K; intros; subst; trivial.
apply H; right; trivial.
assert (Hsigma := IH _ (matching_call3 pat1 sub1 f lpat g lsub pb) sigma tailH).
rewrite matching_pb_eq_subst in Hsigma.
case_eq (merge eq_variable_dec eq_term_dec subst1 subst).
intros tau matching_pb_eq_tau; rewrite matching_pb_eq_tau in H'''.
destruct H''' as [H1 [H2 H3]].
intros v p s v_in_p [ps_eq_pat_sub | ps_in_pb].
injection ps_eq_pat_sub; clear ps_eq_pat_sub; intros; subst p s.
rewrite var_list_unfold in v_in_p; simpl in v_in_p.
destruct (in_app_or _ _ _ v_in_p) as [v_in_pat1 | v_in_lpat]; clear v_in_p.
rewrite <- (Hsigma1 v _ _ v_in_pat1 (or_introl _ (refl_equal _))).
simpl; assert (K2 := C2 v _ _ v_in_pat1 (or_introl _ (refl_equal _))).
case_eq (find eq_variable_dec v subst1).
intros v_subst1 H'''; rewrite (H1 _ _ H'''); trivial.
intros H'''; rewrite H''' in K2; absurd (@None term = None); trivial.
assert (K := Hsigma v (Term f lpat) (Term g lsub)).
simpl in K; generalize (K v_in_lpat (or_introl _ (refl_equal _))); clear K; intro K.
simpl; assert (K2 := C2' v (Term f lpat) (Term g lsub)).
simpl in K2; generalize (K2 v_in_lpat (or_introl _ (refl_equal _))); clear K2; intro K2.
case_eq (find eq_variable_dec v subst).
intros v_subst H'''; rewrite (H2 _ _ H'''); trivial.
rewrite H''' in K; trivial.
intros H'''; rewrite H''' in K2; absurd (@None term = None); trivial.
assert (K := Hsigma v p s v_in_p (or_intror _ ps_in_pb)).
simpl; assert (K2 := C2' v p s v_in_p (or_intror _ ps_in_pb)).
simpl in K; case_eq (find eq_variable_dec v subst).
intros v_subst H'''; rewrite (H2 _ _ H'''); trivial.
rewrite H''' in K; trivial.
intros H'''; rewrite H''' in K2; absurd (@None term = None); trivial.
intro matching_pb_eq_none; rewrite matching_pb_eq_none in H'''.
destruct H''' as [v [t1 [t2 [H1 [H2 t1_diff_t2]]]]].
destruct (C4 v) as [p [s [ps_in_pb v_in_p]]].
rewrite H1; discriminate.
assert (H1v := Hsigma1 v p s v_in_p ps_in_pb); simpl in H1v.
rewrite H1 in H1v.
destruct (C4' v) as [p' [s' [ps'_in_pb v_in_p']]].
rewrite H2; discriminate.
assert (H2v := Hsigma v p' s' v_in_p' ps'_in_pb); simpl in H2v.
rewrite <- H2v in H1v.
rewrite H2 in H1v.
absurd (t1 = t2); subst; trivial.
intro matching_pb_eq_none; rewrite matching_pb_eq_none in H''.
apply (H'' sigma).
intros p s [ps_eq_patsub | ps_in_pb].
injection ps_eq_patsub; clear ps_eq_patsub; intros; subst p s.
assert (K := H _ _ (or_introl _ (refl_equal _))).
simpl in K; injection K; intros; subst; trivial.
apply H; right; trivial.
intro matching_pb_eq_none; rewrite matching_pb_eq_none in H'.
apply (H' sigma).
intros p s [ps_eq_patsub | ps_in_pb].
injection ps_eq_patsub; clear ps_eq_patsub; intros; subst p s.
assert (K := H _ _ (or_introl _ (refl_equal _))).
simpl in K; injection K; intros; subst; trivial.
contradiction.
absurd (f=g); trivial.
assert (K := H _ _ (or_introl _ (refl_equal _))).
simpl in K; injection K; intros; subst; trivial.
Qed.
End Make'.
Module Make (F1 : Signature) (X1 : decidable_set.S) :
Term with Module F := F1 with Module X := X1 := Make' F1 X1.