Library ac_matching.matching
Add LoadPath "basis".
Add LoadPath "term_algebra".
Add LoadPath "term_orderings".
Require Import Arith.
Require Import List.
Require Import more_list.
Require Import list_sort.
Require Import term.
Require Import ac.
Require Import cf_eq_ac.
Module Type S.
Declare Module Import Cf_eq_ac : cf_eq_ac.S.
Import Cf_eq_ac.Ac.
Import Sort.
Import EqTh.T.
Import F.
Import LPermut.
Record partly_solved_term : Set :=
mk_pst
{
head_symb : symbol;
new_var : variable;
closed_term : term
}.
Record matching_problem : Set :=
mk_pb
{
existential_vars : list variable;
unsolved_part : list (term * term);
solved_part : substitution;
partly_solved_part : list (variable * partly_solved_term)
}.
Definition is_rough_sol pb sigma :=
(forall t1 t2, In (t1,t2) pb.(unsolved_part) -> apply_cf_subst sigma t1 = t2) /\
(forall v, match find eq_variable_dec v pb.(partly_solved_part) with
| None => True
| Some pst =>
let l := (apply_cf_subst sigma (Var pst.(new_var))) :: pst.(closed_term) :: nil in
apply_cf_subst sigma (Var v) =
Term pst.(head_symb) (quicksort (flatten pst.(head_symb) l))
end) /\
(forall v, match find eq_variable_dec v pb.(solved_part) with
| None => True
| Some t => apply_cf_subst sigma (Var v) = t
end).
Definition is_sol pb sigma :=
exists sigma', is_rough_sol pb sigma' /\
(forall v, In v (existential_vars pb) \/
apply_cf_subst sigma (Var v) = apply_cf_subst sigma' (Var v)).
Fixpoint occurs_in_term (v : variable) (t : term) {struct t} : Prop :=
match t with
| Var v' => v=v'
| Term _ l =>
let occurs_in_term_list :=
(fix occurs_in_term_list v (l : list _) {struct l} : Prop :=
match l with
| nil => False
| h :: tl => (occurs_in_term v h) \/ (occurs_in_term_list v tl)
end) in
occurs_in_term_list v l
end.
Fixpoint occurs_in_term_list (v : variable) (l : list term) {struct l} : Prop :=
match l with
| nil => False
| cons h tl => (occurs_in_term v h) \/ (occurs_in_term_list v tl)
end.
Definition occurs_in_pb v pb :=
(occurs_in_term_list v (map (fun p => match p with | (t1,t2) => t1 end) pb.(unsolved_part))) \/
(match find eq_variable_dec v pb.(partly_solved_part) with
| None => False | Some _ => True end) \/
(match find eq_variable_dec v pb.(solved_part) with
| None => False | Some _ => True end).
Parameter fresh_var : matching_problem -> variable.
Parameter fresh_var_spec : forall pb, ~(occurs_in_pb (fresh_var pb) pb).
Definition ac_elementary_solve_term_term_term
pb f g lg list_of_terms l' list_of_equations : list matching_problem :=
map_without_repetition eq_term_dec
(fun t =>
match t with
| Term h _ =>
if eq_symbol_dec g h
then
match remove _ eq_term_dec t l' with
| None => None
| Some rmv =>
let t1' := build f list_of_terms in
let t2' := build f rmv in
Some
(mk_pb (existential_vars pb)
(cons ((Term g lg),t) (cons (t1',t2') list_of_equations))
(solved_part pb)
(partly_solved_part pb))
end
else None
| Var _ => None
end)
l'.
Definition ac_elementary_solve_term_var_with_val_term
pb f x_val list_of_terms l' list_of_equations : list matching_problem :=
match remove _ eq_term_dec x_val l' with
| None =>
match x_val with
| Var _ => nil
| Term g ll =>
if eq_symbol_dec f g
then
match remove_list ll l' with
| Some rmv =>
if le_gt_dec (length list_of_terms) (length rmv)
then
let t1' := build f list_of_terms in
let t2' := build f rmv in
let new_pb :=
mk_pb (existential_vars pb)
(cons (t1',t2') list_of_equations)
(solved_part pb)
(partly_solved_part pb) in
cons new_pb nil
else nil
| None => nil
end
else nil
end
| Some rmv =>
let t1' := build f list_of_terms in
let t2' := build f rmv in
let new_pb :=
mk_pb (existential_vars pb)
((t1',t2') :: list_of_equations)
(solved_part pb)
(partly_solved_part pb) in
new_pb :: nil
end.
Definition ac_elementary_solve_term_var_with_part_val_term
pb f x_part_val list_of_terms l' list_of_equations : list matching_problem :=
if (eq_symbol_dec f (head_symb x_part_val))
then
match remove _ eq_term_dec (closed_term x_part_val) l' with
| None => nil
| Some rmv =>
let t1' := build f (cons (Var (new_var x_part_val)) list_of_terms) in
let t2' := build f rmv in
let new_pb :=
mk_pb (existential_vars pb)
((t1',t2') :: list_of_equations)
(solved_part pb)
(partly_solved_part pb) in
new_pb :: nil
end
else
map_without_repetition eq_term_dec
(fun t =>
match t with
| Term h l''' =>
if eq_symbol_dec h (head_symb x_part_val)
then
match remove _ eq_term_dec (closed_term x_part_val) l''' with
| None => None
| Some rmv =>
match remove _ eq_term_dec t l' with
| None => None
| Some rmv2 =>
let y := new_var x_part_val in
let y_val := build h rmv in
let t1' := build f list_of_terms in
let t2' := build f rmv2 in
let new_pb :=
mk_pb (existential_vars pb)
((Var y, y_val) :: (t1',t2') :: list_of_equations)
(solved_part pb)
(partly_solved_part pb) in
Some new_pb
end
end
else None
| Var _ => None
end)
l'.
Definition ac_elementary_solve_term_var_without_val_term
pb f x list_of_terms l' list_of_equations : list matching_problem :=
map12_without_repetition eq_term_dec
(fun t =>
match remove _ eq_term_dec t l' with
| None => (None, None)
| Some rmv =>
let l'_without_t := rmv in
let t1' := build f list_of_terms in
let t2' := build f l'_without_t in
let new_pb :=
mk_pb (existential_vars pb)
((t1', t2') :: list_of_equations)
((x, t) :: (solved_part pb))
(partly_solved_part pb) in
if le_gt_dec (length l') ((length list_of_terms) + 1)
then (Some new_pb, None)
else
let y := fresh_var pb in
let t1'' := build f (Var y :: list_of_terms) in
let new_pb' :=
mk_pb (y :: existential_vars pb)
((t1'', t2') :: list_of_equations)
(solved_part pb)
((x, mk_pst f y t) :: (partly_solved_part pb)) in
(Some new_pb, Some new_pb')
end)
l'.
Definition ac_elementary_solve pb t1 t2 list_of_equations :=
match t1, t2 with
| (Term f (s :: list_of_terms as l)), (Term _ l') =>
match s with
| Term g lg =>
ac_elementary_solve_term_term_term
pb f g lg list_of_terms l' list_of_equations
| Var x =>
match find eq_variable_dec x (solved_part pb) with
| Some x_val =>
ac_elementary_solve_term_var_with_val_term
pb f x_val list_of_terms l' list_of_equations
| None =>
match find eq_variable_dec x (partly_solved_part pb) with
| Some x_part_val =>
ac_elementary_solve_term_var_with_part_val_term
pb f x_part_val list_of_terms l' list_of_equations
| None =>
ac_elementary_solve_term_var_without_val_term
pb f x list_of_terms l' list_of_equations
end
end
end
| (Term _ nil), (Term _ _) =>
let new_pb :=
mk_pb (existential_vars pb)
list_of_equations
(solved_part pb)
(partly_solved_part pb) in
new_pb :: nil
| _, _ => nil
end.
Definition solve pb : list matching_problem :=
match unsolved_part pb with
| (tt1,tt2 as e) :: list_of_equations =>
match tt1, tt2 with
| Var x, _ =>
match find eq_variable_dec x (solved_part pb) with
| Some x_val =>
if eq_term_dec x_val tt2
then
let new_pb :=
mk_pb (existential_vars pb)
list_of_equations (solved_part pb) (partly_solved_part pb) in
new_pb :: nil
else nil
| None =>
match find eq_variable_dec x (partly_solved_part pb) with
| Some x_part_val =>
match tt2 with
| Var _ => nil
| Term f2 l2 =>
if eq_symbol_dec (head_symb x_part_val) f2
then
let y := new_var x_part_val in
match remove _ eq_term_dec (closed_term x_part_val) l2 with
| Some rmv =>
let y_val := build f2 rmv in
let new_pb :=
mk_pb (existential_vars pb)
((Var y, y_val) :: list_of_equations)
(solved_part pb) (partly_solved_part pb) in
new_pb :: nil
| None => nil
end
else nil
end
| None =>
let new_pb :=
mk_pb (existential_vars pb)
list_of_equations ((x, tt2) :: (solved_part pb)) (partly_solved_part pb) in
new_pb :: nil
end
end
| Term f1 l1, Term f2 l2 =>
if eq_symbol_dec f1 f2
then
match arity f1 with
| Free _ =>
match fold_left2
(fun current_list_of_eqs t1 t2 => (t1,t2) :: current_list_of_eqs)
list_of_equations l1 l2 with
| Some new_list_of_equations =>
let new_pb :=
mk_pb (existential_vars pb)
new_list_of_equations (solved_part pb) (partly_solved_part pb) in
new_pb :: nil
| None => nil
end
| AC =>
if le_gt_dec (length l1) (length l2)
then ac_elementary_solve pb tt1 tt2 list_of_equations
else nil
| C =>
match l1, l2 with
| (s1 :: s2 :: nil), (t1 :: t2 :: nil) =>
let new_pb1 :=
mk_pb (existential_vars pb)
((s1,t1) :: (s2,t2) :: list_of_equations)
(solved_part pb) (partly_solved_part pb) in
let new_pb2 :=
mk_pb (existential_vars pb)
((s1,t2) :: (s2,t1) :: list_of_equations)
(solved_part pb) (partly_solved_part pb) in
new_pb1 :: new_pb2 :: nil
| _, _ => nil
end
end
else nil
| _, _ => nil
end
| nil => nil
end.
Fixpoint well_sorted_partly_solved_part (l : list (variable * partly_solved_term)) : Prop :=
match l with
| nil => True
| (v,p) :: tl =>
v <> new_var p /\
(forall v', 1 <= nb_occ eq_variable_dec v' tl -> v' <> new_var p) /\
well_sorted_partly_solved_part tl
end.
Definition well_formed_pb pb :=
(forall t1 t2, In (t1,t2) pb.(unsolved_part) ->
well_formed_cf t1 /\ well_formed_cf t2) /\
(forall v, match (find eq_variable_dec v pb.(solved_part)) with
| None => True
| Some t => well_formed_cf t
end) /\
(forall v, match (find eq_variable_dec v pb.(partly_solved_part)) with
| None => True
| Some pst =>
match arity pst.(head_symb) with
| AC => well_formed_cf pst.(closed_term) /\
match pst.(closed_term) with
| Var _ => True
| Term f _ => pst.(head_symb)<>f
end
| _ => False
end
end) /\
(forall v,
nb_occ eq_variable_dec v (solved_part pb) + nb_occ eq_variable_dec v (partly_solved_part pb) <= 1) /\
well_sorted_partly_solved_part (partly_solved_part pb) /\
(forall v p,
find eq_variable_dec v (partly_solved_part pb) = Some p -> occurs_in_pb (new_var p) pb).
Definition is_well_formed_sol pb sigma :=
(exists sigma', is_rough_sol pb sigma' /\
(forall v, In v (existential_vars pb) \/
apply_cf_subst sigma (Var v) = apply_cf_subst sigma' (Var v)) /\
(well_formed_cf_subst sigma')).
Axiom list_permut_occurs_in_term_list :
forall v l1 l2, permut l1 l2 -> occurs_in_term_list v l1 ->
occurs_in_term_list v l2.
Axiom add_new_var_to_rough_sol :
forall pb sigma t, well_formed_pb pb -> is_rough_sol pb sigma ->
(is_rough_sol pb ((fresh_var pb, t) :: sigma)).
End S.
Module Make (Cf_eq_ac1 : cf_eq_ac.S) : S with Module Cf_eq_ac := Cf_eq_ac1.
Module Import Cf_eq_ac := Cf_eq_ac1.
Import Ac.
Import EqTh.
Import T.
Import F.
Import X.
Import Sort.
Import LPermut.
Record partly_solved_term : Set :=
mk_pst
{
head_symb : symbol;
new_var : variable;
closed_term : term
}.
Record matching_problem : Set :=
mk_pb
{
existential_vars : list variable;
unsolved_part : list (term * term);
solved_part : substitution;
partly_solved_part : list (variable * partly_solved_term)
}.
Definition is_rough_sol pb sigma :=
(forall t1 t2, In (t1,t2) pb.(unsolved_part) -> apply_cf_subst sigma t1 = t2) /\
(forall v, match find eq_variable_dec v pb.(partly_solved_part) with
| None => True
| Some pst =>
let l := (apply_cf_subst sigma (Var pst.(new_var))) :: pst.(closed_term) :: nil in
apply_cf_subst sigma (Var v) =
Term pst.(head_symb) (quicksort (flatten pst.(head_symb) l))
end) /\
(forall v, match find eq_variable_dec v pb.(solved_part) with
| None => True
| Some t => apply_cf_subst sigma (Var v) = t
end).
Definition is_sol pb sigma :=
exists sigma', is_rough_sol pb sigma' /\
(forall v, In v (existential_vars pb) \/
apply_cf_subst sigma (Var v) = apply_cf_subst sigma' (Var v)).
Fixpoint occurs_in_term (v : variable) (t : term) {struct t} : Prop :=
match t with
| Var v' => v=v'
| Term _ l =>
let occurs_in_term_list :=
(fix occurs_in_term_list v (l : list _) {struct l} : Prop :=
match l with
| nil => False
| h :: tl => (occurs_in_term v h) \/ (occurs_in_term_list v tl)
end) in
occurs_in_term_list v l
end.
Fixpoint occurs_in_term_list (v : variable) (l : list term) {struct l} : Prop :=
match l with
| nil => False
| cons h tl => (occurs_in_term v h) \/ (occurs_in_term_list v tl)
end.
Definition occurs_in_pb v pb :=
(occurs_in_term_list v (map (fun p => match p with | (t1,t2) => t1 end) pb.(unsolved_part))) \/
(match find eq_variable_dec v pb.(partly_solved_part) with
| None => False | Some _ => True end) \/
(match find eq_variable_dec v pb.(solved_part) with
| None => False | Some _ => True end).
Parameter fresh_var : matching_problem -> variable.
Parameter fresh_var_spec : forall pb, ~(occurs_in_pb (fresh_var pb) pb).
Definition ac_elementary_solve_term_term_term
pb f g lg list_of_terms l' list_of_equations : list matching_problem :=
map_without_repetition eq_term_dec
(fun t =>
match t with
| Term h _ =>
if eq_symbol_dec g h
then
match remove _ eq_term_dec t l' with
| None => None
| Some rmv =>
let t1' := build f list_of_terms in
let t2' := build f rmv in
Some
(mk_pb (existential_vars pb)
(cons ((Term g lg),t) (cons (t1',t2') list_of_equations))
(solved_part pb)
(partly_solved_part pb))
end
else None
| Var _ => None
end)
l'.
Definition ac_elementary_solve_term_var_with_val_term
pb f x_val list_of_terms l' list_of_equations : list matching_problem :=
match remove _ eq_term_dec x_val l' with
| None =>
match x_val with
| Var _ => nil
| Term g ll =>
if eq_symbol_dec f g
then
match remove_list ll l' with
| Some rmv =>
if le_gt_dec (length list_of_terms) (length rmv)
then
let t1' := build f list_of_terms in
let t2' := build f rmv in
let new_pb :=
mk_pb (existential_vars pb)
(cons (t1',t2') list_of_equations)
(solved_part pb)
(partly_solved_part pb) in
cons new_pb nil
else nil
| None => nil
end
else nil
end
| Some rmv =>
let t1' := build f list_of_terms in
let t2' := build f rmv in
let new_pb :=
mk_pb (existential_vars pb)
((t1',t2') :: list_of_equations)
(solved_part pb)
(partly_solved_part pb) in
new_pb :: nil
end.
Definition ac_elementary_solve_term_var_with_part_val_term
pb f x_part_val list_of_terms l' list_of_equations : list matching_problem :=
if (eq_symbol_dec f (head_symb x_part_val))
then
match remove _ eq_term_dec (closed_term x_part_val) l' with
| None => nil
| Some rmv =>
let t1' := build f (cons (Var (new_var x_part_val)) list_of_terms) in
let t2' := build f rmv in
let new_pb :=
mk_pb (existential_vars pb)
((t1',t2') :: list_of_equations)
(solved_part pb)
(partly_solved_part pb) in
new_pb :: nil
end
else
map_without_repetition eq_term_dec
(fun t =>
match t with
| Term h l''' =>
if eq_symbol_dec h (head_symb x_part_val)
then
match remove _ eq_term_dec (closed_term x_part_val) l''' with
| None => None
| Some rmv =>
match remove _ eq_term_dec t l' with
| None => None
| Some rmv2 =>
let y := new_var x_part_val in
let y_val := build h rmv in
let t1' := build f list_of_terms in
let t2' := build f rmv2 in
let new_pb :=
mk_pb (existential_vars pb)
((Var y, y_val) :: (t1',t2') :: list_of_equations)
(solved_part pb)
(partly_solved_part pb) in
Some new_pb
end
end
else None
| Var _ => None
end)
l'.
Definition ac_elementary_solve_term_var_without_val_term
pb f x list_of_terms l' list_of_equations : list matching_problem :=
map12_without_repetition eq_term_dec
(fun t =>
match remove _ eq_term_dec t l' with
| None => (None, None)
| Some rmv =>
let l'_without_t := rmv in
let t1' := build f list_of_terms in
let t2' := build f l'_without_t in
let new_pb :=
mk_pb (existential_vars pb)
((t1', t2') :: list_of_equations)
((x, t) :: (solved_part pb))
(partly_solved_part pb) in
if le_gt_dec (length l') ((length list_of_terms) + 1)
then (Some new_pb, None)
else
let y := fresh_var pb in
let t1'' := build f (Var y :: list_of_terms) in
let new_pb' :=
mk_pb (y :: existential_vars pb)
((t1'', t2') :: list_of_equations)
(solved_part pb)
((x, mk_pst f y t) :: (partly_solved_part pb)) in
(Some new_pb, Some new_pb')
end)
l'.
Definition ac_elementary_solve pb t1 t2 list_of_equations :=
match t1, t2 with
| (Term f (s :: list_of_terms as l)), (Term _ l') =>
match s with
| Term g lg =>
ac_elementary_solve_term_term_term
pb f g lg list_of_terms l' list_of_equations
| Var x =>
match find eq_variable_dec x (solved_part pb) with
| Some x_val =>
ac_elementary_solve_term_var_with_val_term
pb f x_val list_of_terms l' list_of_equations
| None =>
match find eq_variable_dec x (partly_solved_part pb) with
| Some x_part_val =>
ac_elementary_solve_term_var_with_part_val_term
pb f x_part_val list_of_terms l' list_of_equations
| None =>
ac_elementary_solve_term_var_without_val_term
pb f x list_of_terms l' list_of_equations
end
end
end
| (Term _ nil), (Term _ _) =>
let new_pb :=
mk_pb (existential_vars pb)
list_of_equations
(solved_part pb)
(partly_solved_part pb) in
new_pb :: nil
| _, _ => nil
end.
Definition solve pb : list matching_problem :=
match unsolved_part pb with
| (tt1,tt2 as e) :: list_of_equations =>
match tt1, tt2 with
| Var x, _ =>
match find eq_variable_dec x (solved_part pb) with
| Some x_val =>
if eq_term_dec x_val tt2
then
let new_pb :=
mk_pb (existential_vars pb)
list_of_equations (solved_part pb) (partly_solved_part pb) in
new_pb :: nil
else nil
| None =>
match find eq_variable_dec x (partly_solved_part pb) with
| Some x_part_val =>
match tt2 with
| Var _ => nil
| Term f2 l2 =>
if eq_symbol_dec (head_symb x_part_val) f2
then
let y := new_var x_part_val in
match remove _ eq_term_dec (closed_term x_part_val) l2 with
| Some rmv =>
let y_val := build f2 rmv in
let new_pb :=
mk_pb (existential_vars pb)
((Var y, y_val) :: list_of_equations)
(solved_part pb) (partly_solved_part pb) in
new_pb :: nil
| None => nil
end
else nil
end
| None =>
let new_pb :=
mk_pb (existential_vars pb)
list_of_equations ((x, tt2) :: (solved_part pb)) (partly_solved_part pb) in
new_pb :: nil
end
end
| Term f1 l1, Term f2 l2 =>
if eq_symbol_dec f1 f2
then
match arity f1 with
| Free _ =>
match fold_left2
(fun current_list_of_eqs t1 t2 => (t1,t2) :: current_list_of_eqs)
list_of_equations l1 l2 with
| Some new_list_of_equations =>
let new_pb :=
mk_pb (existential_vars pb)
new_list_of_equations (solved_part pb) (partly_solved_part pb) in
new_pb :: nil
| None => nil
end
| AC =>
if le_gt_dec (length l1) (length l2)
then ac_elementary_solve pb tt1 tt2 list_of_equations
else nil
| C =>
match l1, l2 with
| (s1 :: s2 :: nil), (t1 :: t2 :: nil) =>
let new_pb1 :=
mk_pb (existential_vars pb)
((s1,t1) :: (s2,t2) :: list_of_equations)
(solved_part pb) (partly_solved_part pb) in
let new_pb2 :=
mk_pb (existential_vars pb)
((s1,t2) :: (s2,t1) :: list_of_equations)
(solved_part pb) (partly_solved_part pb) in
new_pb1 :: new_pb2 :: nil
| _, _ => nil
end
end
else nil
| _, _ => nil
end
| nil => nil
end.
Fixpoint well_sorted_partly_solved_part (l : list (variable * partly_solved_term)) : Prop :=
match l with
| nil => True
| (v,p) :: tl =>
v <> new_var p /\
(forall v', 1 <= nb_occ eq_variable_dec v' tl -> v' <> new_var p) /\
well_sorted_partly_solved_part tl
end.
Definition well_formed_pb pb :=
(forall t1 t2, In (t1,t2) pb.(unsolved_part) ->
well_formed_cf t1 /\ well_formed_cf t2) /\
(forall v, match (find eq_variable_dec v pb.(solved_part)) with
| None => True
| Some t => well_formed_cf t
end) /\
(forall v, match (find eq_variable_dec v pb.(partly_solved_part)) with
| None => True
| Some pst =>
match arity pst.(head_symb) with
| AC => well_formed_cf pst.(closed_term) /\
match pst.(closed_term) with
| Var _ => True
| Term f _ => pst.(head_symb)<>f
end
| _ => False
end
end) /\
(forall v,
nb_occ eq_variable_dec v (solved_part pb) + nb_occ eq_variable_dec v (partly_solved_part pb) <= 1) /\
well_sorted_partly_solved_part (partly_solved_part pb) /\
(forall v p,
find eq_variable_dec v (partly_solved_part pb) = Some p -> occurs_in_pb (new_var p) pb).
Lemma list_permut_occurs_in_term_list :
forall v l1 l2, permut l1 l2 -> occurs_in_term_list v l1 ->
occurs_in_term_list v l2.
Proof.
intros v;
cut (forall l l', occurs_in_term_list v l' -> occurs_in_term_list v (l ++ l')).
intros H l1; induction l1.
contradiction.
intros l2 P O.
assert (a_in_l2 : In a l2).
setoid_rewrite <- (list_permut.in_permut_in P); left; trivial.
destruct (In_split _ _ a_in_l2) as [l2' [l2'' H']]; subst l2.
elim O; clear O; intro O.
apply H; left; trivial.
setoid_rewrite <- permut_cons_inside in P.
generalize (IHl1 (l2' ++ l2'') P O).
clear l1 IHl1 P O; induction l2'.
intro; right; trivial.
simpl; intro O; destruct O as [ O | O ].
left; trivial.
right; apply IHl2'; trivial; apply in_or_app; right; left; trivial.
reflexivity.
intro l; induction l; trivial; right; apply IHl; trivial.
Qed.
Lemma add_new_var_to_subst :
forall t1 v t2 sigma, ~occurs_in_term v t1 ->
apply_cf_subst sigma t1 = apply_cf_subst ((v,t2) :: sigma) t1.
Proof.
intro t1; pattern t1; apply term_rec3; clear t1.
intros v v0 t2 sigma O; simpl; elim (eq_variable_dec v v0).
intro; subst v; cut False.
contradiction.
apply O; unfold occurs_in_term; trivial.
intros; trivial.
intros f l IH v t2 sigma O; simpl.
cut (map (apply_cf_subst sigma) l = map (apply_cf_subst ((v,t2) :: sigma)) l).
intro H; rewrite H; trivial.
simpl in O; induction l.
trivial.
simpl; cut (apply_cf_subst sigma a = apply_cf_subst ((v,t2) :: sigma) a).
intro H; rewrite H.
cut (map (apply_cf_subst sigma) l = map (apply_cf_subst ((v,t2) :: sigma)) l).
intro H1; rewrite H1; trivial.
apply IHl.
intros; apply IH; trivial; right; trivial.
unfold not; intro O'; apply O; right; trivial.
apply IH.
left; trivial.
unfold not; intro O'; apply O; left; trivial.
Qed.
Lemma add_new_var_to_rough_sol :
forall pb sigma t, well_formed_pb pb -> is_rough_sol pb sigma ->
(is_rough_sol pb ((fresh_var pb, t) :: sigma)).
Proof.
intros pb sigma t ; generalize (fresh_var_spec pb);
unfold occurs_in_pb, is_rough_sol;
intros O w S'; elim S'; clear S';
intros S1 S2; elim S2; clear S2;
intros S2 S3; split.
induction pb.(unsolved_part).
contradiction.
destruct a; intros t2 t3 I; elim I; clear I; intro I.
inversion I.
rewrite <- (add_new_var_to_subst t2 (fresh_var pb) t).
apply S1; left; trivial.
unfold not; intro O'; apply O.
left; left; subst t2; trivial.
apply IHl; trivial.
unfold not; intro O'; apply O; elim O'; clear O'; intro O'.
left; right; trivial.
right; trivial.
intros; apply S1; right; trivial.
elim w; clear w;
intros _ w; elim w; clear w;
intros _ w; elim w; clear w;
intros _ w; elim w; clear w;
intros _ w; elim w; clear w;
intros _ w; split.
intro v; generalize (S2 v);
cut (forall v', v=v' -> find eq_variable_dec v' (partly_solved_part pb) =
find eq_variable_dec v (partly_solved_part pb)).
case (find eq_variable_dec v (partly_solved_part pb)).
intros p F; generalize (F v (refl_equal _)); clear F; intro F.
repeat rewrite <- (add_new_var_to_subst); trivial.
unfold not; intro O'; apply O.
simpl in O'; rewrite O'.
apply (w v p F).
unfold not; intro O'; apply O.
simpl in O'; rewrite O'.
right; left; rewrite F; trivial.
trivial.
intros; subst v; trivial.
intro v; generalize (S3 v);
cut (forall v', v=v' -> find eq_variable_dec v' (solved_part pb) =
find eq_variable_dec v (solved_part pb)).
case (find eq_variable_dec v (solved_part pb)).
intros t0 F; simpl; elim (eq_variable_dec v (fresh_var pb)).
intro v_eq_fresh_var; absurd (v = fresh_var pb); trivial.
unfold not; intros _; apply O;
right; right; rewrite (F (fresh_var pb) v_eq_fresh_var); trivial.
trivial.
trivial.
intros; subst v; trivial.
Qed.
Definition is_well_formed_sol pb sigma :=
(exists sigma', is_rough_sol pb sigma' /\
(forall v, In v (existential_vars pb) \/
apply_cf_subst sigma (Var v) = apply_cf_subst sigma' (Var v)) /\
(well_formed_cf_subst sigma')).
End Make.