proposition: Lemma rpo_eval_is_sound_weak : forall rpo_infos n t1 t2, match rpo_eval rpo_infos n t1 t2 with | Some Equivalent => equiv t1 t2 | Some Greater_than => rpo rpo_infos.(bb) t2 t1 | Some Less_than => rpo rpo_infos.(bb) t1 t2 | _ => True end.
proof: Proof. intros rpo_infos n; induction n as [ | n]. intros t1 t2. simpl. case_eq (mem_bool eq_tt_bool (t1, t2) (rpo_l rpo_infos)). intros Hfind;apply (find_is_sound (rpo rpo_infos.(bb)) _ (rpo_l_valid rpo_infos) _ _ (Hfind)). intro; case_eq (mem_bool eq_tt_bool (t2, t1) (rpo_l rpo_infos)). intros Hfind;apply (find_is_sound (rpo rpo_infos.(bb)) _ (rpo_l_valid rpo_infos) _ _ (Hfind)). intro. case_eq (mem_bool eq_tt_bool (t1, t2) (equiv_l rpo_infos)). intros Hfind;apply (find_is_sound equiv _ (equiv_l_valid rpo_infos) _ _ (Hfind)). intro; case_eq (mem_bool eq_tt_bool (t2, t1) (equiv_l rpo_infos)). intro Hfind. symmetry. apply (find_is_sound equiv _ (equiv_l_valid rpo_infos) _ _ (Hfind)). tauto. intros t1 t2; rewrite rpo_eval_equation. case_eq (mem_bool eq_tt_bool (t1, t2) (rpo_l rpo_infos)). intros Hfind;apply (find_is_sound (rpo rpo_infos.(bb)) _ (rpo_l_valid rpo_infos) _ _ (Hfind)). intros _; case_eq (mem_bool eq_tt_bool (t2, t1) (rpo_l rpo_infos)). intros Hfind;apply (find_is_sound (rpo rpo_infos.(bb)) _ (rpo_l_valid rpo_infos) _ _ (Hfind)). intros _. case_eq (mem_bool eq_tt_bool (t1, t2) (equiv_l rpo_infos)). intros Hfind;apply (find_is_sound equiv _ (equiv_l_valid rpo_infos) _ _ (Hfind)). intros _; case_eq (mem_bool eq_tt_bool (t2, t1) (equiv_l rpo_infos)). intro Hfind. symmetry. apply (find_is_sound equiv _ (equiv_l_valid rpo_infos) _ _ (Hfind)). intros _. assert (E1 := equiv_eval_is_sound_weak rpo_infos (S n) t1 t2); destruct (equiv_eval rpo_infos (S n) t1 t2) as [ [ | ] | ]. apply E1; trivial. clear E1; assert (H : forall v f l, var_in_term_list v l = true -> rpo rpo_infos.(bb) (Var v) (Term f l)). intros v f l H; apply trans_clos_subterm_rpo; trivial. assert (H' : (In (Var v) l \/ (exists t, In t l /\ trans_clos direct_subterm (Var v) t)) -> trans_clos direct_subterm (Var v) (Term f l)). intros [v_in_l | [t [t_in_l H']]]. left; trivial. apply trans_clos_is_trans with t; trivial; left; trivial. apply H'; clear H'. generalize H; clear H; pattern l; refine (list_rec3 size _ _ _); clear l. intros m; induction m as [ | m]; intros [ | t l] L. intros; discriminate. simpl in L; absurd (1 <= 0); auto with arith; refine (Nat.le_trans _ _ _ _ L); apply Nat.le_trans with (size t); auto with arith; apply size_ge_one. intros; discriminate. simpl in L; assert (Sl : list_size size l <= m). apply le_S_n; refine (Nat.le_trans _ _ _ _ L); apply (Nat.add_le_mono_r 1 (size t) (list_size size l)); apply size_ge_one. destruct t as [v' | f' l']; rewrite var_in_term_list_equation. generalize (X.eq_bool_ok v v'); case (X.eq_bool v v'); [intros v_eq_v' _ | intro v_diff_v']. left; subst; left; trivial. intro H; destruct (IHm _ Sl H) as [v_in_l | [t [t_in_l H']]]. left; right; trivial. right; exists t; split; trivial; right; trivial. assert (Sl' : list_size size l' <= m). apply le_S_n; refine (Nat.le_trans _ _ _ _ L); rewrite size_unfold; simpl; apply le_n_S; auto with arith. generalize (IHm _ Sl'); destruct (var_in_term_list v l'). intro H; destruct (H (eq_refl _)) as [v_in_l' | [t [t_in_l' H']]]. right; exists (Term f' l'); split. left; trivial. left; trivial. right; exists (Term f' l'); split. left; trivial. apply trans_clos_is_trans with t; trivial; left; trivial. intros _; generalize (IHm _ Sl); destruct (var_in_term_list v l). intro H; destruct (H (eq_refl _)) as [v_in_l' | [t [t_in_l' H']]]. left; right; trivial. right; exists t; split; trivial; right; trivial. intros; discriminate. destruct t1 as [v1 | f1 l1]; destruct t2 as [v2 | f2 l2]; trivial. generalize (H v1 f2 l2); destruct (var_in_term_list v1 l2); intro H'; trivial; apply H'; trivial. generalize (H v2 f1 l1); destruct (var_in_term_list v2 l1); intro H'; trivial; apply H'; trivial. generalize (list_exists_option_is_sound (fun t : term => match rpo_eval rpo_infos n t (Term f2 l2) with | Some Equivalent => Some true | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None (A:=bool) end) l1); destruct (list_exists_option (fun t : term => match rpo_eval rpo_infos n t (Term f2 l2) with | Some Equivalent => Some true | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None (A:=bool) end) l1) as [ [ | ] | ]. intros [t1 [t1_in_l1 t1_gt_f2l2]]; simpl; apply Subterm with t1; trivial. apply in_impl_mem; trivial. exact Eq. generalize (IHn t1 (Term f2 l2)); destruct (rpo_eval rpo_infos n t1 (Term f2 l2)) as [ [ | | | ] | ]; try discriminate. intro H1; apply Equiv; symmetry; trivial. intro H1; apply Lt; trivial. intros _; generalize (list_exists_option_is_sound (fun t : term => match rpo_eval rpo_infos n (Term f1 l1) t with | Some Equivalent => Some true | Some Less_than => Some true | Some Greater_than => Some false | Some Uncomparable => Some false | None => None (A:=bool) end) l2); destruct (list_exists_option (fun t : term => match rpo_eval rpo_infos n (Term f1 l1) t with | Some Equivalent => Some true | Some Less_than => Some true | Some Greater_than => Some false | Some Uncomparable => Some false | None => None (A:=bool) end) l2) as [ [ | ] | ]. intros [t2 [t2_in_l2 t2_gt_f1l1]]; simpl; apply Subterm with t2; trivial. apply in_impl_mem; trivial. exact Eq. generalize (IHn (Term f1 l1) t2); destruct (rpo_eval rpo_infos n (Term f1 l1) t2) as [ [ | | | ] | ]; try discriminate. intro; apply Equiv; trivial. intro; apply Lt; trivial. intros _; generalize (prec_eval_is_sound f1 f2); destruct (prec_eval f1 f2). intro f1_eq_f2. assert (Sf1:status Prec f1 = status Prec f2). apply prec_eq_status; trivial. destruct (status Prec f2). rewrite Sf1. simpl; assert (H' := lexico_eval_is_sound (rpo_eval rpo_infos n) (Term f1 l1) (Term f2 l2) l1 l2). destruct (lexico_eval (rpo_eval rpo_infos n) (Term f1 l1) (Term f2 l2) l1 l2) as [ [ | | | ] | ]. destruct H' as [ll [E_ll [H1 H2]]]. rewrite (f_equal (@length _) H1); rewrite (f_equal (@length _) H2); do 2 rewrite length_map. rewrite Nat.eqb_refl; simpl. apply (@Eq_lex f1 f2 l1 l2 Sf1). assert (H3:= prec_eq_status). assert (H3':= H3 symbol Prec f1 f2). assert (H4: status Prec f1 = status Prec f2). apply H3'; trivial. rewrite <- H4; trivial. trivial. subst l1 l2; induction ll as [ | [t1 t2] ll]; simpl. apply Eq_list_nil. apply Eq_list_cons. generalize (IHn t1 t2); rewrite (E_ll _ _ (or_introl _ (eq_refl _))); intro; assumption. apply IHll; intros; apply E_ll; right; assumption. case_eq (Nat.eqb (length l1) (length l2)); simpl. intro L; apply (@Top_eq_lex rpo_infos.(bb) f1 f2 l2 l1 Sf1). assert (H3:= prec_eq_status). assert (H3':= H3 symbol Prec f1 f2). assert (H4: status Prec f1 = status Prec f2). apply H3'; trivial. rewrite <- H4; trivial. trivial. left; apply sym_eq; apply Nat.eqb_eq; assumption. destruct H' as [[H1 H2] | [[ll [t2 [l2' [ _ [H1 H2]]]]] | [ll [t1 [t2 [l1' [l2' [Hll [Ht [H' [H1 H2]]]]]]]]]]]. destruct l2 as [ | a2 l2]; [apply False_rect; apply H2; apply eq_refl | subst l1; discriminate]. subst l1 l2; rewrite length_app in L; do 2 rewrite length_map in L. apply False_rect; generalize (proj1 (Nat.eqb_eq _ _) L); clear L; induction ll as [ | [u1 u2] ll]. discriminate. intro L; injection L; clear L; intro L; apply IHll; assumption. clear L H'; subst l1 l2; induction ll as [ | [u1 u2] ll]. simpl; constructor 1; generalize (IHn t1 t2); rewrite Ht; intro; assumption. simpl; constructor 2. generalize (IHn u1 u2); rewrite (Hll _ _ (or_introl _ (eq_refl _))); intro; assumption. apply IHll; intros; apply Hll; right; assumption. destruct H' as [[H1 H2] | [[ll [t2 [l2' [_ [H1 H2]]]]] | [ll [t1 [t2 [l1' [l2' [Hll [Ht [H' [H1 H2]]]]]]]]]]]. intros; subst l1; contradiction. subst l1 l2; rewrite length_app in L; do 2 rewrite length_map in L. apply False_rect; generalize (proj1 (Nat.eqb_eq _ _) L); clear L; induction ll as [ | [u1 u2] ll]. discriminate. intro L; injection L; clear L; intro L; apply IHll; assumption. intros u u_in_l1; rewrite mem_in_eq in u_in_l1; destruct u_in_l1 as [u' [u_eq_u' u'_in_l1]]. destruct (H' _ u'_in_l1) as [ [u2 [u2_in_l2 u'_le_u2]] | H'']. apply Subterm with u2. apply in_impl_mem; trivial. intros; apply Eq. destruct u'_le_u2 as [u'_eq_u2 | u'_lt_u2]. left; transitivity u'; trivial. generalize (IHn u' u2); rewrite u'_eq_u2; intro; assumption. right; rewrite (equiv_rpo_equiv_2 _ u_eq_u'); generalize (IHn u' u2); rewrite u'_lt_u2; intro; assumption. rewrite (equiv_rpo_equiv_2 _ u_eq_u'); generalize (IHn (Term f2 l2) u'); rewrite H''; intro; assumption. intros _; generalize (leb_complete (length l1) (rpo_infos.(bb))); case (leb (length l1) rpo_infos.(bb)); [idtac | simpl; trivial]. generalize (leb_complete (length l2) (rpo_infos.(bb))); case (leb (length l2) (bb rpo_infos)); simpl; [idtac | trivial]. intros L2 L1; apply (@Top_eq_lex rpo_infos.(bb) f1 f2 l2 l1 Sf1). assert (H3:= prec_eq_status). assert (H3':= H3 symbol Prec f1 f2). assert (H4: status Prec f1 = status Prec f2). apply H3'; trivial. rewrite <- H4; trivial. trivial. right; split; [apply L1 | apply L2]; apply eq_refl. clear L1 L2; destruct H' as [[H1 H2] | [[ll [t2 [l2' [Hll [H1 H2]]]]] | [ll [t1 [t2 [l1' [l2' [Hll [Ht [H' [H1 H2]]]]]]]]]]]. subst l1; destruct l2 as [ | a2 l2]; [apply False_rect; apply H2; apply eq_refl | constructor 3]. subst l1 l2; induction ll as [ | [u1 u2] ll]. simpl; constructor 3. simpl; constructor 2. generalize (IHn u1 u2); rewrite (Hll _ _ (or_introl _ (eq_refl _))); intro; assumption. apply IHll; intros; apply Hll; right; assumption. clear H'; subst l1 l2; induction ll as [ | [u1 u2] ll]. simpl; constructor 1; generalize (IHn t1 t2); rewrite Ht; intro; assumption. simpl; constructor 2. generalize (IHn u1 u2); rewrite (Hll _ _ (or_introl _ (eq_refl _))); intro; assumption. apply IHll; intros; apply Hll; right; assumption. clear L1 L2; destruct H' as [[H1 H2] | [[ll [t2 [l2' [Hll [H1 H2]]]]] | [ll [t1 [t2 [l1' [l2' [Hll [Ht [H' [H1 H2]]]]]]]]]]]. intros; subst l1; contradiction. intros u u_in_l1; rewrite mem_in_eq in u_in_l1; destruct u_in_l1 as [u' [u_eq_u' u'_in_l1]]. subst l1; rewrite in_map_iff in u'_in_l1; destruct u'_in_l1 as [[u1 u2] [H1 K2]]. apply Subterm with u2. subst l2; rewrite <- mem_or_app; left; apply in_impl_mem. apply Eq. rewrite in_map_iff; exists (u1,u2); split; trivial. simpl in H1; subst u1; left; transitivity u'; trivial. generalize (IHn u' u2); rewrite (Hll _ _ K2); intro; assumption. intros u u_in_l1; rewrite mem_in_eq in u_in_l1; destruct u_in_l1 as [u' [u_eq_u' u'_in_l1]]. destruct (H' _ u'_in_l1) as [ [u2 [u2_in_l2 u'_le_u2]] | H'']. apply Subterm with u2. apply in_impl_mem; trivial. intros; apply Eq. destruct u'_le_u2 as [u'_eq_u2 | u'_lt_u2]. left; transitivity u'; trivial. generalize (IHn u' u2); rewrite u'_eq_u2; intro; assumption. right; rewrite (equiv_rpo_equiv_2 _ u_eq_u'); generalize (IHn u' u2); rewrite u'_lt_u2; intro; assumption. rewrite (equiv_rpo_equiv_2 _ u_eq_u'); generalize (IHn (Term f2 l2) u'); rewrite H''; intro; assumption. case_eq (Nat.eqb (length l1) (length l2)); simpl. assert (Sf2: status Prec f2 = Lex). assert (H3:= prec_eq_status). assert (H3':= H3 symbol Prec f1 f2). assert (H4: status Prec f1 = status Prec f2). apply H3'; trivial. rewrite <- H4; trivial. trivial. intro L; apply (@Top_eq_lex rpo_infos.(bb) f2 f1 l1 l2 Sf2). trivial. apply prec_eq_sym; trivial. left; apply Nat.eqb_eq; assumption. destruct H' as [[H1 H2] | [[ll [t1 [l1' [ _ [H1 H2]]]]] | [ll [t1 [t2 [l1' [l2' [Hll [Ht [H' [H1 H2]]]]]]]]]]]. destruct l1 as [ | a1 l1]; [apply False_rect; apply H1; apply eq_refl | subst l2; discriminate]. subst l1 l2; rewrite length_app in L; do 2 rewrite length_map in L. apply False_rect; generalize (proj1 (Nat.eqb_eq _ _) L); clear L; induction ll as [ | [u1 u2] ll]. discriminate. intro L; injection L; clear L; intro L; apply IHll; assumption. clear L H'; subst l1 l2; induction ll as [ | [u1 u2] ll]. simpl; constructor 1; generalize (IHn t1 t2); rewrite Ht; intro; assumption. simpl; constructor 2. symmetry; generalize (IHn u1 u2); rewrite (Hll _ _ (or_introl _ (eq_refl _))); intro; assumption. apply IHll; intros; apply Hll; right; assumption. destruct H' as [[H1 H2] | [[ll [t1 [l1' [_ [H1 H2]]]]] | [ll [t1 [t2 [l1' [l2' [Hll [Ht [H' [H1 H2]]]]]]]]]]]. intros; subst l2; contradiction. subst l1 l2; rewrite length_app in L; do 2 rewrite length_map in L. apply False_rect; generalize (proj1 (Nat.eqb_eq _ _) L); clear L; induction ll as [ | [u1 u2] ll]. discriminate. intro L; injection L; clear L; intro L; apply IHll; assumption. intros u u_in_l2; rewrite mem_in_eq in u_in_l2; destruct u_in_l2 as [u' [u_eq_u' u'_in_l2]]. destruct (H' _ u'_in_l2) as [ [u1 [u1_in_l1 u'_le_u1]] | H'']. apply Subterm with u1. apply in_impl_mem; trivial. intros; apply Eq. destruct u'_le_u1 as [u'_eq_u1 | u'_lt_u1]. left; transitivity u'; trivial. symmetry; generalize (IHn u1 u'); rewrite u'_eq_u1; intro; assumption. right; rewrite (equiv_rpo_equiv_2 _ u_eq_u'); generalize (IHn u1 u'); rewrite u'_lt_u1; intro; assumption. rewrite (equiv_rpo_equiv_2 _ u_eq_u'); generalize (IHn (Term f1 l1) u'); rewrite H''; intro; assumption. intros _; generalize (leb_complete (length l1) (rpo_infos.(bb))); case (leb (length l1) rpo_infos.(bb)); [idtac | simpl; trivial]. generalize (leb_complete (length l2) (rpo_infos.(bb))); case (leb (length l2) (bb rpo_infos)); simpl; [idtac | trivial]. assert (H3:= prec_eq_status). assert (H3':= H3 symbol Prec f1 f2). assert (H4: status Prec f1 = status Prec f2). apply H3'; trivial. assert (Sf2: status Prec f2 = Lex). rewrite <- H4; trivial. intros L2 L1; apply (@Top_eq_lex rpo_infos.(bb) f2 f1 l1 l2 Sf2). trivial. apply prec_eq_sym; trivial. right; split; [apply L2 | apply L1]; apply eq_refl. clear L1 L2; destruct H' as [[H1 H2] | [[ll [t1 [l2' [Hll [H1 H2]]]]] | [ll [t1 [t2 [l1' [l2' [Hll [Ht [H' [H1 H2]]]]]]]]]]]. subst l2; destruct l1 as [ | a1 l2]; [apply False_rect; apply H1; apply eq_refl | constructor 3]. subst l1 l2; induction ll as [ | [u1 u2] ll]. simpl; constructor 3. simpl; constructor 2. symmetry; generalize (IHn u1 u2); rewrite (Hll _ _ (or_introl _ (eq_refl _))); intro; assumption. apply IHll; intros; apply Hll; right; assumption. clear H'; subst l1 l2; induction ll as [ | [u1 u2] ll]. simpl; constructor 1; generalize (IHn t1 t2); rewrite Ht; intro; assumption. simpl; constructor 2. symmetry; generalize (IHn u1 u2); rewrite (Hll _ _ (or_introl _ (eq_refl _))); intro; assumption. apply IHll; intros; apply Hll; right; assumption. clear L1 L2; destruct H' as [[H1 H2] | [[ll [t1 [l1' [Hll [H1 H2]]]]] | [ll [t1 [t2 [l1' [l2' [Hll [Ht [H' [H1 H2]]]]]]]]]]]. intros; subst l2; contradiction. intros u u_in_l2; rewrite mem_in_eq in u_in_l2; destruct u_in_l2 as [u' [u_eq_u' u'_in_l2]]. subst l2; rewrite in_map_iff in u'_in_l2; destruct u'_in_l2 as [[u1 u2] [K1 K2]]. apply Subterm with u1. subst l1; rewrite <- mem_or_app; left; apply in_impl_mem. apply Eq. rewrite in_map_iff; exists (u1,u2); split; trivial. simpl in K1; subst u2; left; transitivity u'; trivial. symmetry; generalize (IHn u1 u'); rewrite (Hll _ _ K2); intro; assumption. intros u u_in_l2; rewrite mem_in_eq in u_in_l2; destruct u_in_l2 as [u' [u_eq_u' u'_in_l2]]. destruct (H' _ u'_in_l2) as [ [u1 [u1_in_l1 u'_le_u1]] | H'']. apply Subterm with u1. apply in_impl_mem; trivial. intros; apply Eq. destruct u'_le_u1 as [u'_eq_u1 | u'_lt_u1]. left; transitivity u'; trivial. symmetry; generalize (IHn u1 u'); rewrite u'_eq_u1; intro; assumption. right; rewrite (equiv_rpo_equiv_2 _ u_eq_u'); generalize (IHn u1 u'); rewrite u'_lt_u1; intro; assumption. rewrite (equiv_rpo_equiv_2 _ u_eq_u'); generalize (IHn (Term f1 l1) u'); rewrite H''; intro; assumption. case (Nat.eqb (length l1) (length l2) || leb (length l1) (bb rpo_infos) && leb (length l2) (bb rpo_infos)); trivial. case (Nat.eqb (length l1) (length l2) || leb (length l1) (bb rpo_infos) && leb (length l2) (bb rpo_infos)); trivial. assert (H3:= prec_eq_status). assert (H3':= H3 symbol Prec f1 f2). assert (H4: status Prec f1 = status Prec f2). apply H3'; trivial. assert (Sf2: status Prec f2 = Mul). rewrite <- H4; trivial. simpl; assert (H' := remove_equiv_eval_list_is_sound (equiv_eval rpo_infos n) l1 l2). rewrite Sf1. destruct (remove_equiv_eval_list (equiv_eval rpo_infos n) l1 l2) as [ [[ | t1' l1'] [ | t2' l2']] | ]. destruct H' as [ll [E_ll [P1 [P2 _]]]]. apply (@Eq_mul f1 f2 l1 l2 Sf1); trivial. simpl in P1; simpl in P2. apply permut0_trans with (map (fun st : term * term => fst st) ll); trivial. apply equiv_equiv. apply permut_impl with (@eq term); trivial; intros; subst; reflexivity. apply permut0_trans with (map (fun st : term * term => snd st) ll); trivial. apply equiv_equiv. assert (E_ll' : forall t1 t2, In (t1,t2) ll -> equiv t1 t2). intros t1 t2 t1t2_in_ll; assert (H' := equiv_eval_is_sound_weak rpo_infos n t1 t2); rewrite (E_ll t1 t2 t1t2_in_ll) in H'; apply H'; trivial. clear E_ll P1 P2; induction ll as [ | [t1 t2] ll]. reflexivity. simpl; rewrite <- permut0_cons. apply IHll. intros; apply E_ll'; right; trivial. apply equiv_equiv. apply E_ll'; left; trivial. symmetry; apply permut_impl with (@eq term); trivial; intros; subst; reflexivity. destruct H' as [ll [E_ll [P1 [P2 _]]]]. apply Top_eq_mul; trivial. apply (@List_mul _ t2' l2' nil l1); trivial. reflexivity. transitivity ((t2' :: l2') ++ (map (fun st : term * term => snd st) ll)). apply permut_impl with (@eq term); trivial; intros; subst; reflexivity. rewrite app_comm_cons; rewrite <- permut_app1. transitivity (map (fun st : term * term => fst st) ll). symmetry. assert (E_ll' : forall t1 t2, In (t1,t2) ll -> equiv t1 t2). intros t1 t2 t1t2_in_ll; assert (H' := equiv_eval_is_sound_weak rpo_infos n t1 t2); rewrite (E_ll t1 t2 t1t2_in_ll) in H'; apply H'; trivial. clear E_ll P1 P2; induction ll as [ | [t1 t2] ll]. reflexivity. simpl; rewrite <- permut0_cons. apply IHll. intros; apply E_ll'; right; trivial. apply equiv_equiv. apply E_ll'; left; trivial. symmetry; apply permut_impl with (@eq term); trivial; intros; subst; reflexivity. apply equiv_equiv. intros; contradiction. destruct H' as [ll [E_ll [P1 [P2 _]]]]. apply Top_eq_mul; trivial. apply prec_eq_sym; trivial. apply (@List_mul _ t1' l1' nil l2); trivial. reflexivity. transitivity ((t1' :: l1') ++ (map (fun st : term * term => fst st) ll)). apply permut_impl with (@eq term); trivial; intros; subst; reflexivity. rewrite app_comm_cons; rewrite <- permut_app1. transitivity (map (fun st : term * term => snd st) ll). assert (E_ll' : forall t1 t2, In (t1,t2) ll -> equiv t1 t2). intros t1 t2 t1t2_in_ll; assert (H' := equiv_eval_is_sound_weak rpo_infos n t1 t2); rewrite (E_ll t1 t2 t1t2_in_ll) in H'; apply H'; trivial. clear E_ll P1 P2; induction ll as [ | [t1 t2] ll]. reflexivity. simpl; rewrite <- permut0_cons. apply IHll. intros; apply E_ll'; right; trivial. apply equiv_equiv. apply E_ll'; left; trivial. symmetry; apply permut_impl with (@eq term); trivial; intros; subst; reflexivity. apply equiv_equiv. intros; contradiction. assert (H'' := mult_eval_is_sound_weak (rpo_eval rpo_infos n) (t1' :: l1') (t2' :: l2')). destruct (mult_eval (rpo_eval rpo_infos n) (t1' :: l1') (t2' :: l2')) as [ [ | | | ] | ]. contradiction. destruct H' as [ll [E_ll [P1 [P2 _]]]]. assert (E_ll' : forall t1 t2, In (t1,t2) ll -> equiv t1 t2). intros t1 t2 t1t2_in_ll; assert (H' := equiv_eval_is_sound_weak rpo_infos n t1 t2); rewrite (E_ll t1 t2 t1t2_in_ll) in H'; apply H'; trivial. apply Top_eq_mul; trivial. apply (@List_mul _ t2' l2' (t1' :: l1') (map (fun st : term * term => fst st) ll)); trivial. apply permut_impl with (@eq term); trivial; intros; subst; reflexivity. transitivity ((t2' :: l2') ++ map (fun st : term * term => snd st) ll). apply permut_impl with (@eq term); trivial; intros; subst; reflexivity. rewrite app_comm_cons; rewrite <- permut_app1. clear E_ll P1 P2; induction ll as [ | [t1 t2] ll]. reflexivity. simpl; rewrite <- permut0_cons. apply IHll. intros; apply E_ll'; right; trivial. apply equiv_equiv. symmetry; apply E_ll'; left; trivial. apply equiv_equiv. intros u1 u1_mem_l1'. destruct (mem_split_set _ _ equiv_bool_ok _ _ u1_mem_l1') as [u1' [k1 [k1' [u1_eq_u1' [H' _]]]]]. simpl in u1_eq_u1'; simpl in H'. assert (u1'_in_l1' : In u1' (t1' :: l1')). rewrite H'; apply in_or_app; right; left; trivial. destruct (H'' _ u1'_in_l1') as [u2 [u2_in_l2' u1_lt_u2]]; exists u2; split. apply in_impl_mem; trivial. exact Eq. assert (H''' := IHn u2 u1'). rewrite u1_lt_u2 in H'''. rewrite (equiv_rpo_equiv_2 _ u1_eq_u1'); trivial. destruct H' as [ll [E_ll [P1 [P2 _]]]]. assert (E_ll' : forall t1 t2, In (t1,t2) ll -> equiv t1 t2). intros t1 t2 t1t2_in_ll; assert (H' := equiv_eval_is_sound_weak rpo_infos n t1 t2); rewrite (E_ll t1 t2 t1t2_in_ll) in H'; apply H'; trivial. apply Top_eq_mul; trivial. apply prec_eq_sym; trivial. apply (@List_mul _ t1' l1' (t2' :: l2') (map (fun st : term * term => fst st) ll)); trivial. transitivity ((t2' :: l2') ++ map (fun st : term * term => snd st) ll). apply permut_impl with (@eq term); trivial; intros; subst; reflexivity. rewrite <- permut_app1. clear E_ll P1 P2; induction ll as [ | [t1 t2] ll]. reflexivity. simpl; rewrite <- permut0_cons. apply IHll. intros; apply E_ll'; right; trivial. apply equiv_equiv. symmetry; apply E_ll'; left; trivial. apply equiv_equiv. apply permut_impl with (@eq term); trivial; intros; subst; reflexivity. intros u2 u2_mem_l2'. destruct (mem_split_set _ _ equiv_bool_ok _ _ u2_mem_l2') as [u2' [k2 [k2' [u2_eq_u2' [H' _]]]]]. simpl in u2_eq_u2'; simpl in H'. assert (u2'_in_l2' : In u2' (t2' :: l2')). rewrite H'; apply in_or_app; right; left; trivial. destruct (H'' _ u2'_in_l2') as [u1 [u1_in_l1' u2_lt_u1]]; exists u1; split. apply in_impl_mem; trivial. exact Eq. assert (H''' := IHn u1 u2'). rewrite u2_lt_u1 in H'''. rewrite (equiv_rpo_equiv_2 _ u2_eq_u2'); trivial. trivial. trivial. trivial. intro f1_lt_f2; simpl. generalize (list_forall_option_is_sound (fun t : term => match rpo_eval rpo_infos n t (Term f2 l2) with | Some Equivalent => Some false | Some Less_than => Some true | Some Greater_than => Some false | Some Uncomparable => Some false | None => None (A:=bool) end) l1); destruct (list_forall_option (fun t : term => match rpo_eval rpo_infos n t (Term f2 l2) with | Some Equivalent => Some false | Some Less_than => Some true | Some Greater_than => Some false | Some Uncomparable => Some false | None => None (A:=bool) end) l1) as [ [ | ] | ]. intros l1_lt_s2; apply Top_gt; trivial. intros t1 t1_mem_l1; destruct (mem_split_set _ _ equiv_bool_ok _ _ t1_mem_l1) as [t1' [k1 [k1' [t1_eq_t1' [H' _]]]]]. simpl in t1_eq_t1'; simpl in H'. assert (t1'_in_l1 : In t1' l1). rewrite H'; apply in_or_app; right; left; trivial. rewrite (equiv_rpo_equiv_2 _ t1_eq_t1'). assert (H'' := l1_lt_s2 t1' t1'_in_l1). assert (H''' := IHn t1' (Term f2 l2)); destruct (rpo_eval rpo_infos n t1' (Term f2 l2)) as [ [ | | | ] | ]; trivial; discriminate. trivial. trivial. intro f2_lt_f1; simpl. generalize (list_forall_option_is_sound (fun t : term => match rpo_eval rpo_infos n (Term f1 l1) t with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None (A:=bool) end) l2); destruct (list_forall_option (fun t : term => match rpo_eval rpo_infos n (Term f1 l1) t with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None (A:=bool) end) l2) as [ [ | ] | ]. intros s1_gt_l2; apply Top_gt; trivial. intros t2 t2_mem_l2; destruct (mem_split_set _ _ equiv_bool_ok _ _ t2_mem_l2) as [t2' [k2 [k2' [t2_eq_t2' [H' _]]]]]. simpl in t2_eq_t2'; simpl in H'. assert (t2'_in_l2 : In t2' l2). rewrite H'; apply in_or_app; right; left; trivial. rewrite (equiv_rpo_equiv_2 _ t2_eq_t2'). assert (H'' := s1_gt_l2 t2' t2'_in_l2). assert (H''' := IHn (Term f1 l1) t2'); destruct (rpo_eval rpo_infos n (Term f1 l1) t2') as [ [ | | | ] | ]; trivial; discriminate. trivial. trivial. simpl; trivial. simpl; trivial. simpl; trivial. trivial. Qed.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)