proposition: Lemma Case3 : forall f l, defined R3 f -> ( forall t : term, In t l -> Acc (one_step (@union term (@union term R1 R3) (@union term R2 (Pi pi V0 V1)))) t) -> Acc (ddp_step (@union term (@union term R1 R3) (@union term R2 (Pi pi V0 V1)))) (Term f l).
proof: Proof. intros f l D3 IHl. assert (H : Interp_dom (@union term R1 R3) (@union term R2 (Pi pi V0 V1)) (Term f l)). intros [ | i p] g k Sub D2. simpl in Sub; injection Sub; clear Sub; intros; subst g k. inversion D2 as [g k u [H2 | HPi]]; subst. apply False_rect; apply (Incomp23 f (Def R2 f k u H2) D3). apply False_rect; inversion HPi; subst f; apply (Incomp3' D3). simpl in Sub; assert (H := nth_error_ok_in i l); destruct (nth_error l i) as [ti | ]; [idtac | discriminate]. destruct (H _ (eq_refl _)) as [ls1 [ls2 [L H']]]; clear H; subst l. assert (Hti : Interp_dom (@union term R1 R3) (@union term R2 (Pi pi V0 V1)) ti). apply acc_interp_dom. apply IHl; apply in_or_app; right; left; trivial. apply (Hti p); trivial. assert (D3' : match Term f l with | Var _ => False | Term g _ => defined R3 g end). trivial. assert (Ts := T3 _ H). assert (IHl' : forall t, direct_subterm t (Term f l) -> Acc (one_step (@union term (@union term R1 R3) (@union term R2 (Pi pi V0 V1)))) t). simpl; trivial. generalize (Term f l) Ts D3' IHl'; clear f l H Ts D3' IHl D3 IHl'. intros t Acc_t; induction Acc_t as [[ v | _f l] Acc_t IH]; intros D3 IHl. contradiction. apply Acc_intro; intros t H. assert (Simple_step : forall l (IH : forall y : term, rdp_step (axiom (ddp R3)) (@union term (@union term R1 R3) (@union term R2 (Pi pi V0 V1))) y (Term _f l) -> match y with | Var _ => False | Term g _ => defined R3 g end -> (forall t : term, direct_subterm t y -> Acc (one_step (@union term (@union term R1 R3) (@union term R2 (Pi pi V0 V1)))) t) -> Acc (ddp_step (@union term (@union term R1 R3) (@union term R2 (Pi pi V0 V1)))) y) (D3 : defined R3 _f) (IHl : forall t : term, direct_subterm t (Term _f l) -> Acc (one_step (@union term (@union term R1 R3) (@union term R2 (Pi pi V0 V1)))) t) (t : term) (H : axiom (ddp (@union term (@union term R1 R3) (@union term R2 (Pi pi V0 V1)))) t (Term _f l)), Acc (ddp_step (@union term (@union term R1 R3) (@union term R2 (Pi pi V0 V1)))) t). clear l Acc_t IH D3 IHl t H; intros l IH D3 IHl t _Hm. inversion _Hm as [_t _s sigma Hm K1 K2]; clear _Hm; subst. destruct Hm as [Hm _Sub]; inversion Hm as [s [ v | f' k'] p g'' k'' t_R_s Sub Df'' H1 H']; clear Hm; subst. destruct p; discriminate. destruct _s as [ v | g k]. absurd (@union term (@union term R1 R3) (@union term R2 (Pi pi V0 V1)) (Term f' k') (Var v)); trivial. apply R132_var'. assert (t_R3_s : R3 (Term f' k') (Term g k)). simpl in K2; injection K2; clear K2; intros H' f_eq_g; subst g l. destruct t_R_s as [[ H1 | H3] | [H2 | HPi]]; trivial. apply False_rect; apply (Incomp13 _f (Def _ _ _ _ H1) D3). apply False_rect; apply (Incomp23 _f (Def _ _ _ _ H2) D3). apply False_rect; inversion HPi; subst _f; apply (Incomp3' D3). assert (Hm' : axiom (ddp (@union term (@union term R1 R2) (@union term R3 (Pi pi V0 V1)))) (apply_subst sigma (Term g'' k'')) (Term _f l)). rewrite <- K2; apply instance. split; [idtac | trivial]. refine (Dp (@union term (@union term R1 R2) (@union term R3 (Pi pi V0 V1))) _ (Term f' k') p g'' k'' _ _ _); trivial. right; left; trivial. inversion Df'' as [h'' l'' u'' [[H1 | H3] | [H2 | Hpi]]]; subst. apply (Def (@union term (@union term R1 R2) (@union term R3 (Pi pi V0 V1))) g'' l'' u''); left; left; trivial. apply (Def (@union term (@union term R1 R2) (@union term R3 (Pi pi V0 V1))) g'' l'' u''); right; left; trivial. apply (Def (@union term (@union term R1 R2) (@union term R3 (Pi pi V0 V1))) g'' l'' u''); left; right; trivial. apply (Def (@union term (@union term R1 R2) (@union term R3 (Pi pi V0 V1))) g'' l'' u''); right; right; trivial. destruct (split_dp_top _ _ _ _ Hm') as [D12' | DD3]; clear Hm'. destruct D12' as [Df Dg]. absurd (defined (@union term R1 R2) _f); trivial. intros D12f; inversion D12f as [f'' k''' u [H1 | H2]]; subst. apply (Incomp13 _f (Def R1 _f k''' u H1) D3). apply (Incomp23 _f (Def R2 _f k''' u H2) D3). assert (D123 : match Term g'' k'' with | Var _ => False | Term f _ => defined R3 f \/ defined (@union _ R1 R2) f end). destruct DD3 as [[_ D3'] | [_ D12]]; [left | right]; trivial. clear DD3. generalize (Term g'' k'') p _Sub Sub D123; clear g'' k'' p _Sub Sub Df'' D123. intro t; pattern t; apply term_rec2; clear t. intro n; induction n as [ | n]; intros t St p _Sub Sub D123. absurd (1 <= 0); auto with arith; apply Nat.le_trans with (size t); trivial; apply size_ge_one. assert (IHk'' : forall s q, subterm_at_pos t q = Some s -> Acc (one_step (@union term (@union term R1 R3) (@union term R2 (Pi pi V0 V1)))) (apply_subst sigma s)). intro s; pattern s; apply term_rec2; clear s. intro m; induction m as [ | m]; intros s Ss q Sub'. absurd (1 <= 0); auto with arith; apply Nat.le_trans with (size s); trivial; apply size_ge_one. destruct s as [v | g3 k3]. assert (v_in_s : In v (var_list (Term g k))). apply R3_reg with (Term f' k'); trivial. apply var_in_subterm with (Var v) (p ++ q). apply subterm_in_subterm with t; trivial. left; trivial. destruct (var_in_subterm2 _ _ (in_impl_mem (@eq _) (fun a => eq_refl a) _ _ v_in_s)) as [q' Sub'']. destruct q' as [ | i q']. discriminate. assert (H'' := nth_error_ok_in i k). simpl in Sub''; destruct (nth_error k i) as [si | ]. destruct (H'' _ (eq_refl _)) as [l1 [l2 [L1 H''']]]. apply acc_subterms_3 with q' (apply_subst sigma si). apply IHl. simpl in K2; injection K2; clear K2; intros; subst. simpl; rewrite map_app; apply in_or_app; right; left; trivial. assert (Sub3 := subterm_at_pos_apply_subst_apply_subst_subterm_at_pos si q' sigma). rewrite Sub'' in Sub3; trivial. discriminate. assert (Hk3 : forall s, In s k3 -> Acc (one_step (@union term (@union term R1 R3) (@union term R2 (Pi pi V0 V1)))) (apply_subst sigma s)). intros s' s'_in_k3; destruct (In_split _ _ s'_in_k3) as [k3' [k3'' H]]; subst k3. apply IHm with (q ++ (length k3' :: nil)). apply le_S_n. apply Nat.le_trans with (size (Term g3 (k3' ++ s' :: k3''))); trivial. apply size_direct_subterm; trivial. apply subterm_in_subterm with (Term g3 (k3' ++ s' :: k3'')); trivial. simpl; rewrite nth_error_at_pos; trivial. destruct (subterm_at_pos_dec (Term g k) (Term g3 k3)) as [[[ | i q'] _Sub'] | not_Sub]. apply ddp_simple_criterion_local. apply R132_var'. apply R132_reg'. apply def_dec132'. apply IH; trivial. apply Rdp_step with l. left. rewrite <- K2; apply instance. assert (H''' := Dp R3 _ _ (p ++ q) g3 k3 t_R3_s). split. apply H'''. apply subterm_in_subterm with t; trivial. injection _Sub'; intros; subst; apply (Def R3 _ _ _ t_R3_s). intros i q''; intro H3; simpl in _Sub'; injection _Sub'; intros; subst g3 k3; absurd (size (Term g k) < size (Term g k)). auto with arith. generalize (size_subterm_at_pos (Term g k) i q''). rewrite H3; trivial. simpl in _Sub'; injection _Sub'; intros; subst g3 k3; apply (Def R3 g _ _ t_R3_s). simpl; intros s s_in_k3; rewrite in_map_iff in s_in_k3; destruct s_in_k3 as [s' [H s'_in_k3]]; subst. apply Hk3; trivial. simpl; intros s s_in_k3; rewrite in_map_iff in s_in_k3; destruct s_in_k3 as [s' [H s'_in_k3]]; subst. apply Hk3; trivial. simpl in _Sub'. generalize (nth_error_ok_in i k); destruct (nth_error k i) as [ti | ]; [idtac | discriminate]. intros H''; destruct (H'' _ (eq_refl _)) as [l1' [l2' [L H3]]]; clear H''; subst k. apply acc_subterms_3 with q' (apply_subst sigma ti). apply IHl. simpl; injection K2; clear K2; intros; subst. rewrite in_map_iff; exists ti; split; trivial; apply in_or_app; right; left; trivial. generalize (subterm_at_pos_apply_subst_apply_subst_subterm_at_pos ti q' sigma). rewrite _Sub'; trivial. destruct (def_dec132' g3) as [Cg3 | Dg3]. simpl; apply acc_subterms; trivial. apply R132_var'. intros s s_in_k3; rewrite in_map_iff in s_in_k3; destruct s_in_k3 as [s' [H s'_in_k3]]; subst. apply Hk3; trivial. destruct q as [ | i q]. simpl in Sub'; injection Sub'; clear Sub'; intros; subst t. destruct D123 as [Dg | Dg]. assert (H : rdp_step (axiom (ddp R3)) (@union term (@union term R1 R3) (@union term R2 (Pi pi V0 V1))) (Term g3 (map (apply_subst sigma) k3)) (Term _f l)). apply Rdp_step with l. left. rewrite <- K2; refine (instance _ (Term g3 k3) _ sigma _). simpl in K2; injection K2; clear K2; intros H' _f_eq_g; subst g l. split. apply (Dp R3 (Term _f k) (Term f' k') p g3 k3); trivial. intros i p'; apply not_Sub. apply ddp_simple_criterion_local. apply R132_var'. apply R132_reg'. apply def_dec132'. apply IH; simpl; trivial. intros s s_in_k3; rewrite in_map_iff in s_in_k3; destruct s_in_k3 as [s' [H'' s'_in_k3]]; subst. apply Hk3; trivial. simpl; intros s s_in_k3; rewrite in_map_iff in s_in_k3; destruct s_in_k3 as [s' [H'' s'_in_k3]]; subst. apply Hk3; trivial. apply ddp_simple_criterion_local. apply R132_var'. apply R132_reg'. apply def_dec132'. apply Acc_incl with (ddp_step (@union term (@union term R1 R2) (@union term R3 (Pi pi V0 V1)))). apply ddp_step_incl. intros t1 t2 [[H1 | H3] | [H2 | HPi]]. do 2 left; trivial. right; left; trivial. left; right; trivial. do 2 right; trivial. apply (Case12 g3 (map (apply_subst sigma) k3)); trivial. intros [ | i r] g4 k4 Sub'' Dg4. simpl in Sub''; injection Sub''; clear Sub''; intros; subst. apply False_rect; apply (Incomp123' g4); trivial. simpl in Sub''. assert (H'' := nth_error_map (apply_subst sigma) k3 i). destruct (nth_error (map (apply_subst sigma) k3) i) as [ti | ]. assert (H''' := nth_error_ok_in i k3). destruct (nth_error k3 i) as [si | ]. destruct (H''' _ (eq_refl _)) as [l1 [l2 [L1 H'''']]]. assert (si_in_lr : In si k3). subst k3; apply in_or_app; right; left; trivial. apply acc_subterms_3 with r ti; trivial. subst; rewrite Dummy; apply IHm with (length l1 :: nil); trivial. apply le_S_n. apply Nat.le_trans with (size (Term g3 (l1 ++ si :: l2))); trivial. apply size_direct_subterm; trivial. simpl; rewrite nth_error_at_pos; trivial. contradiction. discriminate. simpl; intros s s_in_k3; rewrite in_map_iff in s_in_k3; destruct s_in_k3 as [s' [H'' s'_in_k3]]; subst. apply Hk3; trivial. apply ddp_simple_criterion_local. apply R132_var'. apply R132_reg'. apply def_dec132'. apply IHn with (p ++ i :: q). apply le_S_n. apply Nat.le_trans with (size t); trivial. generalize (size_subterm_at_pos t i q). rewrite Sub'; trivial. intros j q' Sub''; apply (not_Sub (j :: q')); trivial. apply subterm_in_subterm with t; trivial. destruct Dg3 as [g' l' u [[H1 | H3] | [H2 | Hpi]]]. right; apply (Def (@union _ R1 R2) g' l' u); left; trivial. left; apply (Def R3 g' l' u); trivial. right; apply (Def (@union _ R1 R2) g' l' u); right; trivial. apply False_rect; destruct (P3 _ _ t_R3_s g') as [F _]; apply F. apply (symb_in_subterm g' _ p Sub). apply (symb_in_subterm g' _ (i :: q) Sub'). simpl; generalize (F.Symb.eq_bool_ok g' g'); case (F.Symb.eq_bool g' g'); [intros _ | intros g_diff_g; absurd (g'=g')]; trivial. inversion Hpi; subst; trivial. simpl; intros s s_in_k3; rewrite in_map_iff in s_in_k3; destruct s_in_k3 as [s' [H'' s'_in_k3]]; subst. apply Hk3; trivial. apply acc_one_step_acc_ddp. apply R132_var'. apply IHk'' with (@nil nat); trivial. inversion H as [g k l' s'' l_R_l' Hm]; clear H; subst. apply (Simple_step l'); trivial. intros [v | g k] H D3' Iu. contradiction. apply IH; trivial. inversion H as [g' k' l'' s''' l'_R_l'' Hm']; clear H; subst. apply Rdp_step with l''; trivial. apply refl_trans_clos_is_trans with l'; trivial. simpl; intros u' u'_in_l'. assert (H : exists u, In u l /\ (refl_trans_clos (one_step (@union term (@union term R1 R3) (@union term R2 (Pi pi V0 V1)))) u' u)). generalize l l' l_R_l' u'_in_l'. intro k1; induction k1 as [ | t1 k1]; intros [ | t2 k2] H u_in_k1. contradiction. generalize (refl_trans_clos_one_step_list_length_eq H); intro; discriminate. contradiction. rewrite refl_trans_clos_one_step_list_head_tail in H. destruct H as [Ht1t2 Hk1k2]. simpl in u_in_k1; destruct u_in_k1 as [u_eq_t2 | u_in_k2]. exists t1; split. left; trivial. subst; assumption. destruct (IHk1 k2 Hk1k2 u_in_k2) as [u [u_in_k1 H]]. exists u; split. right; trivial. assumption. destruct H as [u [u_in_l H]]. inversion H as [u'' | u1' u1 H1]; clear H; subst. apply IHl; simpl; trivial. assert (Acc_u : Acc (rwr (@union term (@union term R1 R3) (@union term R2 (Pi pi V0 V1)))) u). rewrite <- acc_one_step. apply IHl; trivial. apply Acc_incl with (trans_clos (one_step (@union term (@union term R1 R3) (@union term R2 (Pi pi V0 V1))))). do 3 intro; left; assumption. apply Acc_inv with u; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)