proposition: Lemma decompose_term_aux : forall t sigma, (forall x u, In (x,u) sigma -> match u with | Var _ => True | Term f l => (match F.arity f with Free n => n | _ => 2 end) <> length l end) -> (forall x u v, In (x,u) sigma -> In (x,v) sigma -> u = v) -> (forall x y u, In (x,u) sigma -> In (y,u) sigma -> x = y) -> {s : term & {tau : substitution | let sigma' := tau ++ sigma in t = apply_subst sigma' s /\ well_formed s /\ (forall x u, In (x,u) sigma' -> match u with | Var _ => True | Term f l => (match F.arity f with Free n => n | _ => 2 end) <> length l end) /\ (forall x u v, In (x,u) sigma' -> In (x,v) sigma' -> u = v) /\ (forall x y u, In (x,u) sigma' -> In (y,u) sigma' -> x = y) /\ (forall x, In x (var_list s) -> In x (map (@fst _ _) sigma'))}}.
proof: Proof. intro t; pattern t; apply term_rec3; clear t. intros v sigma h1 h2 h3. generalize (mem_bool_ok _ _ T.eq_bool_ok (Var v) (map (@snd _ _) sigma)). case (mem_bool T.eq_bool (Var v) (map (@snd _ _) sigma)); [intro v_in_sig | intro v_not_in_sig]. destruct (mem_map_set _ _ T.eq_bool_ok _ _ _ v_in_sig) as [[x u] [v_eq_u v_in_sig']]. simpl in v_eq_u; subst u. exists (Var x); exists nil; split. simpl; rewrite (subst_aux sigma h2 _ _ v_in_sig'); trivial. split. apply eq_refl. split. apply h1. split. apply h2. split. apply h3. intros z [z_eq_x | z_in_nil]; [rewrite in_map_iff; exists (x,Var v); split; trivial | contradiction]. set (m := (S (maxl _ (map (fun xt => (inject_inv (fst xt), snd xt)) sigma)))). exists (Var (inject m)); exists ((inject m, Var v ) :: nil). split. simpl. rewrite eq_var_bool_refl; apply eq_refl. split. apply eq_refl. split. simpl; intros x u [xu_eq_mv | xu_in_sigma]. injection xu_eq_mv; intros; subst x u; trivial. apply (h1 x u xu_in_sigma). split. simpl. intros x u u' [xu_eq_mv | xu_in_sigma] [xu'_eq_mv | xu'_in_sigma]. injection xu_eq_mv; injection xu'_eq_mv; intros; subst; trivial. injection xu_eq_mv; clear xu_eq_mv; intros; subst x u. absurd (m < m). auto with arith. apply le_n_S. apply (maxl_is_max _ (map (fun xt : T1.variable * T1.term => (inject_inv (fst xt), snd xt)) sigma) m u'). rewrite in_map_iff. exists (inject m, u'); split; trivial. simpl; rewrite Hinject2; trivial. injection xu'_eq_mv; clear xu'_eq_mv; intros; subst x u'. absurd (m < m). auto with arith. apply le_n_S. apply (maxl_is_max _ (map (fun xt : T1.variable * T1.term => (inject_inv (fst xt), snd xt)) sigma) m u). rewrite in_map_iff. exists (inject m, u); split; trivial. simpl; rewrite Hinject2; trivial. apply (h2 x); trivial. split. simpl. intros x y u [xu_eq_mv | xu_in_sigma] [yu_eq_mv | yu_in_sigma]. injection xu_eq_mv; injection yu_eq_mv; intros; subst; trivial. injection xu_eq_mv; clear xu_eq_mv; intros; subst x u. apply False_rect; apply v_not_in_sig; apply in_impl_mem. reflexivity. rewrite in_map_iff; exists (y, Var v); split; trivial. injection yu_eq_mv; clear yu_eq_mv; intros; subst y u. apply False_rect; apply v_not_in_sig; apply in_impl_mem. reflexivity. rewrite in_map_iff; exists (x, Var v); split; trivial. apply (h3 x y u); trivial. intros z [z_eq_m | z_in_nil]. left; trivial. contradiction. intros f l Hl sigma h1 h2 h3. generalize (mem_bool_ok _ _ T.eq_bool_ok (Term f l) (map (@snd _ _) sigma)). case (mem_bool T.eq_bool (Term f l) (map (@snd _ _) sigma)); [intro fl_in_sig | intro fl_not_in_sig]. destruct (mem_map_set _ _ T.eq_bool_ok _ _ _ fl_in_sig) as [[x u] [fl_eq_u fl_in_sig']]. simpl in fl_eq_u; subst u. exists (Var x); exists nil; split. simpl; rewrite (subst_aux sigma h2 _ _ fl_in_sig'); trivial. split. apply eq_refl. split. apply h1. split. apply h2. split. apply h3. intros z [z_eq_x | z_in_nil]; [rewrite in_map_iff; exists (x,Term f l); split; trivial | contradiction]. destruct (eq_nat_dec (length l) (match F.arity f with Free n => n | _ => 2 end)) as [Wf | not_Wf]. assert (Aux : {ls : list T1.term & {tau : T1.substitution | let sigma' := tau ++ sigma in l = map (T1.apply_subst sigma') ls /\ (forall si, In si ls -> well_formed si) /\ (forall (x : T1.variable) (u : T1.term), In (x, u) sigma' -> match u with | T1.Var _ => True | T1.Term f0 l0 => match T1.F.arity f0 with | AC => 2 | C => 2 | Free n => n end <> length l0 end) /\ (forall (x : T1.variable) (u v : T1.term), In (x, u) sigma' -> In (x, v) sigma' -> u = v) /\ (forall (x y : T1.variable) (u : T1.term), In (x, u) sigma' -> In (y, u) sigma' -> x = y) /\ (forall x : T1.variable, In x (T1.var_list_list ls) -> In x (map (@fst _ _) sigma'))}}). clear f fl_not_in_sig Wf. revert sigma h1 h2 h3; induction l as [ | t l]; intros sigma h1 h2 h3. exists nil; exists nil; repeat split; trivial. intros; contradiction. intros; contradiction. destruct IHl with sigma as [ls [tau [H0 [Wls [H1 [H2 [H3 H4]]]]]]]; trivial. apply (tail_set _ Hl). destruct (Hl t (or_introl _ (eq_refl _)) (tau ++ sigma) H1 H2 H3) as [s [tau' [K0 [Ws [K1 [K2 [K3 K4]]]]]]]. exists (s :: ls); exists (tau' ++ tau); rewrite <- ass_app; repeat split; trivial. simpl; apply f_equal2. assumption. rewrite H0. apply map_eq. intros u u_in_ls; rewrite <- subst_eq_vars. intros v v_in_u. simpl; rewrite (find_app X.eq_bool v tau' (tau ++ sigma)). generalize (mem_bool_ok _ _ X.eq_bool_ok v (map (fun st : T1.variable * T1.term => fst st) tau')). case (mem_bool X.eq_bool v (map (fun st : T1.variable * T1.term => fst st) tau')); [intro v_in_tau' | intro v_not_in_tau']; trivial. case_eq (find X.eq_bool v tau'); [intros v_val v_tau' | intro v_tau']. case_eq (find X.eq_bool v (tau ++ sigma)); [intros v_val' v_tau | intro v_tau]. apply (K2 v). apply in_or_app; right. destruct (find_mem _ _ X.eq_bool_ok _ _ v_tau) as [v' [tau1 [tau2 [v_eq_v' H]]]]. subst v'; rewrite H; apply in_or_app; right; left; apply eq_refl. apply in_or_app; left. destruct (find_mem _ _ X.eq_bool_ok _ _ v_tau') as [v' [tau1 [tau2 [v_eq_v' H]]]]. subst v'; rewrite H; apply in_or_app; right; left; apply eq_refl. assert (H : In v (map (@fst _ _) (tau ++ sigma))). apply H4. destruct (in_split _ _ u_in_ls) as [ls1 [ls2 H]]; rewrite H. rewrite var_list_list_app; apply in_or_app; right. simpl; apply in_or_app; left; assumption. rewrite in_map_iff in H; destruct H as [[v' u'] [v_eq_v' H]]; simpl in v_eq_v'; subst v'. apply False_rect. apply (find_not_found X.eq_bool v v u' (tau ++ sigma) v_tau (eq_var_bool_refl v) H). destruct (mem_map_set _ _ X.eq_bool_ok _ v tau' v_in_tau') as [[v' u'] [v_eq_v' v_in_tau'']]; simpl in v_eq_v'; subst v'. apply False_rect. apply (find_not_found X.eq_bool v v u' tau' v_tau' (eq_var_bool_refl v) v_in_tau''). simpl; intros si [si_eq_s | si_in_ls]; [subst; assumption | apply Wls; assumption]. simpl; intros v v_in_sls; destruct (in_app_or _ _ _ v_in_sls) as [v_in_s | v_in_ls]; clear v_in_sls. apply K4; assumption. rewrite map_app; apply in_or_app; right; apply H4; assumption. destruct Aux as [ls [tau [H0 [Wls [H1 [H2 [H3 H4]]]]]]]. exists (Term f ls); exists tau; repeat split; trivial. simpl; apply f_equal; assumption. apply well_formed_fold; split. exact Wls. rewrite H0 in Wf; rewrite length_map in Wf; destruct (F.arity f); assumption. set (m := (S (maxl _ (map (fun xt => (inject_inv (fst xt), snd xt)) sigma)))). exists (Var (inject m)); exists ((inject m, Term f l ) :: nil). split. simpl; rewrite eq_var_bool_refl; apply eq_refl. split. apply eq_refl. split. simpl; intros x u [xu_eq_mv | xu_in_sigma]. injection xu_eq_mv; intros; subst x u. intro L; apply not_Wf; apply sym_eq; assumption. apply (h1 x u xu_in_sigma). split. simpl. intros x u u' [xu_eq_mv | xu_in_sigma] [xu'_eq_mv | xu'_in_sigma]. injection xu_eq_mv; injection xu'_eq_mv; intros; subst; trivial. injection xu_eq_mv; clear xu_eq_mv; intros; subst x u. absurd (m < m). auto with arith. apply le_n_S. apply (maxl_is_max _ (map (fun xt : T1.variable * T1.term => (inject_inv (fst xt), snd xt)) sigma) m u'). rewrite in_map_iff. exists (inject m, u'); split; trivial. simpl; rewrite Hinject2; trivial. injection xu'_eq_mv; clear xu'_eq_mv; intros; subst x u'. absurd (m < m). auto with arith. apply le_n_S. apply (maxl_is_max _ (map (fun xt : T1.variable * T1.term => (inject_inv (fst xt), snd xt)) sigma) m u). rewrite in_map_iff. exists (inject m, u); split; trivial. simpl; rewrite Hinject2; trivial. apply (h2 x); trivial. split. simpl. intros x y u [xu_eq_mv | xu_in_sigma] [yu_eq_mv | yu_in_sigma]. injection xu_eq_mv; injection yu_eq_mv; intros; subst; trivial. injection xu_eq_mv; clear xu_eq_mv; intros; subst x u. apply False_rect; apply fl_not_in_sig; apply in_impl_mem. reflexivity. rewrite in_map_iff; exists (y, Term f l); split; trivial. injection yu_eq_mv; clear yu_eq_mv; intros; subst y u. apply False_rect; apply fl_not_in_sig; apply in_impl_mem. reflexivity. rewrite in_map_iff; exists (x, Term f l); split; trivial. apply (h3 x y u); trivial. intros z [z_eq_m | z_in_nil]. left; trivial. contradiction. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)