proposition: Lemma rpo_closure : forall s t u, (rpo t s -> rpo u t -> rpo u s) /\ (rpo s t -> rpo t s -> False) /\ (rpo s s -> False) /\ (rpo_eq s t -> rpo_eq t s -> s = t).
proof: Proof. intros s t u; cut (forall triple : term * (term * term), match triple with | (s,(t,u)) => (rpo t s -> rpo u t -> rpo u s) /\ (rpo s t -> rpo t s -> False) /\ (rpo s s -> False) /\ (rpo_eq s t -> rpo_eq t s -> s = t) end). intros H; apply (H (s,(t,u))). clear s t u; intro triple; pattern triple; refine (well_founded_ind wf_size3 _ _ triple); clear triple. intros x IH; destruct x; rename t into s; destruct p; rename t0 into u; destruct s. intuition. inversion H. inversion H0. inversion H. inversion_clear H0; trivial; inversion H1. rename s into f; cut (rpo (Term f l) (Term f l) -> False). intro Anti0; cut (rpo (Term f l) t -> rpo t (Term f l) -> False). intro Anti; intuition. inversion H. subst t0 f0 l0; inversion H5; clear H5. subst t t0; apply (Subterm f l u s); trivial; apply Lt; trivial. subst s0 t0; apply (Subterm f l u s); trivial; elim (IH (s,(t,u))); intuition. apply Lt; trivial. apply lex1; trivial. subst t f0 l0; inversion H0. subst u f0 l0; inversion H7; clear H7. subst t t0; apply (rpo_subterm _ _ H); trivial. subst s0 t0; elim (IH (Term f l,(s,t))); intuition; apply lex2; trivial. subst u f0 l0; rename g0 into h; rename l'0 into l''; apply Top_gt. apply prec_transitive with g; trivial. intros; elim (IH (Term f l,(Term g l',s'))); intuition; apply lex3; trivial. subst f0 l0 u; rename l'0 into l''; apply Top_gt; trivial. intros; elim (IH (Term f l, (Term g l',s'))); intuition; apply lex3; trivial. subst u f0 l0; rename l'0 into l''; apply Top_gt; trivial. inversion H7; subst l0 l'0. intros s' In_s'; generalize (in_permut_in s' In_s' H1); clear In_s'; intro In_s'; elim (in_app_or _ _ _ In_s'); clear In_s'; intro In_s'. elim (IH (Term f l, (Term g l', s'))); intuition. apply H11; elim (H3 s' In_s'); intros tj H'; elim H'; clear H'; intros In_tj H'; apply (Subterm g l' s' tj); [ refine (in_permut_in tj _ (list_permut_sym H2)); rewrite app_comm_cons; apply in_or_app; left | apply Lt ]; trivial. apply lex3; refine (in_permut_in s' _ (list_permut_sym H1)); apply in_or_app; left; trivial. apply (rpo_subterm _ _ H); refine (in_permut_in s' _ (list_permut_sym H2)); rewrite app_comm_cons; apply in_or_app; right; trivial. subst f0 l0 t; inversion H0. subst t f0 l0; inversion H8; clear H8. subst s t; apply H6; trivial. subst s s0; elim (IH (Term f l, (t,u))); intuition; apply lex2; trivial. subst u f0 l0; rename l'0 into l''; apply Top_gt; trivial; intros; elim (IH (Term f l, (Term f l', s'))); intuition; apply lex3; trivial. subst f0 l0 u; rename l'0 into l''; apply Top_eq_lex; trivial. generalize l' l'' H5 H8 IH; clear l' l'' H3 H5 H6 Anti Anti0 H H4 H8 H9 IH H0; induction l; intros l' l'' H4 H6 IH; inversion H4. subst l' t l'0; inversion H6. subst l'' t l0; apply List_gt; elim (IH (a,(s,s0))); intuition. apply lex1; trivial; left; trivial. rewrite H7; trivial. apply lex1; trivial; left; trivial. apply List_gt; trivial. subst l'' s0 l'; rewrite (rpo_lex_same_length _ _ H1); trivial. subst l' l'0 s; inversion H6. apply List_gt; trivial; rewrite H5; apply rpo_lex_same_length; trivial. subst l'' s l'; apply List_eq; apply IHl with l0; trivial; intros; apply IH; apply o_size3_trans with (Term f l, (Term f l0, Term f l1)); trivial; apply lex1_bis. intros; elim (IH (Term f l,(Term f l', s'))); intuition; apply lex3; trivial. absurd (Lex = Mul); [ discriminate | rewrite <- H3; rewrite <- H7; trivial ]. subst t f0 l0; inversion H0. subst t f0 l0; inversion H7; clear H7. subst s t; apply (rpo_subterm _ _ H); trivial. subst s0 t; elim (IH (Term f l, (s, u))); intuition; [ apply H2; trivial; apply (rpo_subterm _ _ H) | apply lex2 ]; trivial. apply Top_gt; trivial; subst u l0 f0; intros s' In_s'; elim (IH (Term f l, (Term f l', s'))); intuition; apply lex3; trivial. absurd (Lex = Mul); [ discriminate | rewrite <- H3; rewrite <- H4; trivial ]. subst u f0 l0; apply Top_eq_mul; trivial; inversion H5; subst l'1 l0; inversion H7; subst l'1 l0; rename l'0 into l''; rewrite app_comm_cons in H9; elim (ac_syntactic _ _ _ _ (list_permut_trans (list_permut_sym H1) H9)); intros lcc H'; elim H'; clear H'; intros lcg H'; elim H'; clear H'; intros lsc H'; elim H'; clear H'; intros lsg H'; elim H'; clear H'; intros P1 H'; elim H'; clear H'; intros P2 H'; elim H'; clear H'; intros P3 P4; apply (List_mul a (lg ++ lcg) (ls0 ++ lsc) lcc). rewrite <- ass_app; apply list_permut_trans with (ls0 ++ lc0); trivial; apply context_list_permut_app1; trivial. apply list_permut_trans with (lcc ++ lsc); trivial; apply list_permut_app_app. apply list_permut_trans with (a :: lg ++ lc); trivial; apply context_list_permut_cons; rewrite <- ass_app; apply context_list_permut_app1; apply list_permut_trans with (lcc ++ lcg); trivial; apply list_permut_app_app. intros b In_b; elim (in_app_or _ _ _ In_b); clear In_b; intro In_b. elim (H10 b In_b); intros a' H'; elim H'; clear H'; intros In_a' H'; elim (in_app_or _ _ _ (in_permut_in a' In_a' P4)); clear In_a'; intro In_a'. exists a'; split; trivial; rewrite app_comm_cons; apply in_or_app; right; trivial. assert (In a' ls). refine (in_permut_in a' _ (list_permut_sym P2)); apply in_or_app; right; trivial. elim (H3 a' H11); intros a'' H''; elim H''; intros; exists a''; assert (In a'' (a :: lg ++ lcg)). rewrite app_comm_cons; apply in_or_app; left; trivial. split; trivial; elim (IH (a'',(a',b))); intuition; apply lex1; refine (in_permut_in a'' _ (list_permut_sym H2)); trivial; rewrite app_comm_cons; apply in_or_app; left; trivial. assert (In b ls). refine (in_permut_in b _ (list_permut_sym P2)); apply in_or_app; left; trivial. elim (H3 b H11); intros a'' H''; elim H''; intros; exists a''; split; trivial. rewrite app_comm_cons; apply in_or_app; left; trivial. inversion_clear H; trivial; inversion_clear H0; trivial; generalize (Anti H1 H); contradiction. intros lt_s_t lt_t_s; inversion lt_t_s; clear lt_t_s. subst t0 f0 l0; inversion H3; clear H3. subst t t0; elim (IH (s, (Term f l, u))); intuition; [ apply H1; trivial; apply (Subterm f l s s); trivial; apply Eq | apply lex1 ]; trivial. subst s0 t0; elim (IH (s,(t,(Term f l)))); intuition. apply Anti0; apply (Subterm f l (Term f l) s); trivial; apply Lt; trivial. apply lex1; trivial. subst t f0 l0; inversion lt_s_t; clear lt_s_t. subst t f0 l0; inversion H5; clear H5. subst t s; apply Anti0; apply H3; trivial. subst s s0; elim (IH (Term f l, (t,u))); intuition; apply lex2; trivial. subst g0 l'0 f0 l0; apply prec_antisym with f; trivial; apply prec_transitive with g; trivial. subst f0 l'0 g l0; apply prec_antisym with f; trivial. subst f0 l'0 g l0; apply prec_antisym with f; trivial. subst t f0 l0; inversion lt_s_t; clear lt_s_t. subst t f0 l0; inversion H6; clear H6. subst s t; apply Anti0; trivial; apply H4; trivial. subst s s0; elim (IH (Term f l, (t,u))); intuition; apply lex2; trivial. apply prec_antisym with f; trivial. generalize l' IH H3 H6; subst f0 l'0 l0; clear Anti0 H1 H3 H4 IH H5 H6 H7; induction l; intros; inversion H3; clear H3. subst t l'0 l'1; inversion H6; clear H6. subst s0 l1 t l0; elim (IH (a,(s,u))); intuition; apply lex1; left; trivial. subst s; elim (IH (a, (Term f (a::l0),u))); intuition; apply lex1; left; trivial. subst s l'0 l'1; inversion H6; clear H6. elim (IH (a, (Term f (a::l0),u))); intuition; apply lex1; left; trivial. subst l'0 s l1; apply IHl with l0; trivial; intros; apply IH; apply o_size3_trans with (Term f l, (Term f l0, u)); trivial; apply lex1_bis. absurd (Lex = Mul); [ discriminate | rewrite <- H1; rewrite <- H5; trivial ]. subst t f0 l0; inversion lt_s_t. subst t f0 l0; inversion H3; subst l0 l'0. elim (in_app_or _ _ _ (in_permut_in s H4 H)); intro In_s. elim (H1 s In_s); intros a' H'; elim H'; clear H'; intros In_a' H'; apply Anti0; apply (Subterm f l (Term f l) a'). refine (in_permut_in a' _ (list_permut_sym H0)); rewrite app_comm_cons; apply in_or_app; left; trivial. inversion H5; subst s; apply Lt; trivial; elim (IH (a',(t,(Term f l)))); intuition; apply lex1; refine (in_permut_in a' _ (list_permut_sym H0)); rewrite app_comm_cons; apply in_or_app; left; trivial. apply Anti0; apply (Subterm f l (Term f l) s); trivial; refine (in_permut_in s _ (list_permut_sym H0)); rewrite app_comm_cons; apply in_or_app; right; trivial. apply prec_antisym with f; trivial. absurd (Lex = Mul); [ discriminate | rewrite <- H2; rewrite <- H4; trivial ]. subst f0 l'0 l0; apply Anti0; apply Top_eq_mul; trivial; inversion H3; subst l'0 l0; inversion H5; subst l'0 l0. rewrite app_comm_cons in H7; elim (ac_syntactic _ _ _ _ (list_permut_trans (list_permut_sym H) H7)); intros lcc H'; elim H'; clear H'; intros lcg H'; elim H'; clear H'; intros lsc H'; elim H'; clear H'; intros lsg H'; elim H'; clear H'; intros P1 H'; elim H'; clear H'; intros P2 H'; elim H'; clear H'; intros P3 P4; apply (List_mul a (lg ++ lcg) (ls0 ++ lsc) lcc). rewrite <- ass_app; apply list_permut_trans with (ls0 ++ lc0); trivial; apply context_list_permut_app1; trivial; apply list_permut_trans with (lcc ++ lsc); trivial; apply list_permut_app_app. apply list_permut_trans with (a :: lg ++ lc); trivial; apply context_list_permut_cons; rewrite <- ass_app; apply context_list_permut_app1; apply list_permut_trans with (lcc ++ lcg); trivial; apply list_permut_app_app. intros b In_b; elim (in_app_or _ _ _ In_b); clear In_b; intro In_b. elim (H8 b In_b); intros a' H'; elim H'; clear H'; intros In_a' H'; elim (in_app_or _ _ _ (in_permut_in a' In_a' P4)); clear In_a'; intro In_a'. exists a'; split; trivial; rewrite app_comm_cons; apply in_or_app; right; trivial. assert (In a' ls). refine (in_permut_in a' _ (list_permut_sym P2)); apply in_or_app; right; trivial. elim (H1 a' H9); intros a'' H''; elim H''; intros; exists a''; assert (In a'' (a :: lg ++ lcg)). rewrite app_comm_cons; apply in_or_app; left; trivial. split; trivial; elim (IH (a'',(a',b))); intuition; apply lex1; refine (in_permut_in a'' _ (list_permut_sym H0)); trivial; rewrite app_comm_cons; apply in_or_app; left; trivial. assert (In b ls). refine (in_permut_in b _ (list_permut_sym P2)); apply in_or_app; left; trivial. elim (H1 b H9); intros a'' H''; elim H''; intros; exists a''; split; trivial. rewrite app_comm_cons; apply in_or_app; left; trivial. intro lt_s_s; inversion lt_s_s; clear lt_s_s. inversion H3; clear H3. subst t0 f0 l0 t1 s; absurd (size (Term f l) < size (Term f l)); auto with arith; apply (size_direct_subterm (Term f l) (Term f l) H2). subst t0 f0 l0 s0 t1. elim (IH (s,(Term f l, s))); intuition. apply H1; trivial; apply (Subterm f l s s); trivial; apply Eq; trivial. apply lex1; trivial. apply prec_antisym with f; trivial. subst f0 l' l0; clear H4; induction l; inversion H3. elim (IH (a,(t,u))); intuition; apply lex1; left; trivial. subst s l0 l'; apply IHl; trivial; intros; apply IH; apply o_size3_trans with (Term f l, (t, u)); trivial; apply lex1_bis. subst f0 l0 l'; inversion H3. subst l' l0; assert (list_permut ls (a :: lg)). apply remove_context_list_permut_app2 with lc; rewrite <- app_comm_cons; apply list_permut_trans with l; trivial; apply list_permut_sym; trivial. assert (forall b, In b ls -> (exists a', In a' ls /\ rpo b a')). intros b In_b; elim (H1 b In_b); intros a' H'; exists a'; intuition; refine (in_permut_in _ _ (list_permut_sym H4)); trivial. assert (forall v, In v ls -> In v l). intros; refine (in_permut_in _ _ (list_permut_sym H)); apply in_or_app; left; trivial. assert (1 <= length ls). rewrite (list_permut_length H4); simpl; auto with arith. generalize H5 H6; clear a lg H4 H5 H6 H2 H3 H0 H1 H; induction ls; intros. absurd (1 <= 0); auto with arith. destruct ls. elim (H5 a (or_introl _ (refl_equal _))); intros a' H'; elim H'; clear H'; intros In_a' lt_a_a'; elim In_a'; clear In_a'; intro In_a'. subst a'; elim (IH (a,(t,u))); intuition; apply lex1; apply H6; left; trivial. contradiction. apply IHls. simpl; auto with arith. intros b In_b; elim (H5 b). intros a' H'; elim H'; clear H'; intros In_a' lt_b_a'; elim In_a'; clear In_a'; intro In_a'. subst a'; elim (H5 a (or_introl _ (refl_equal _))); intros a'' H''; elim H''; clear H''; intros In_a'' lt_a_a''; elim In_a''; clear In_a''; intros In_a''. subst a''; elim (IH (a,(t,u))); intuition; apply lex1; apply H6; left; trivial. exists a''; split; trivial. elim (IH (a'',(a,b))); intuition; apply lex1; apply H6; right; trivial. exists a'; split; trivial. right; trivial. intros; apply H6; right; trivial. Qed.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term