proposition: Lemma rpo_eval_is_complete_less_greater : forall rpo_infos n t1 t2, size t1 + size t2 <= n -> rpo rpo_infos.(bb) t1 t2 -> rpo_eval rpo_infos n t1 t2 = Some Less_than /\ rpo_eval rpo_infos n t2 t1 = Some Greater_than.
proof: Proof. intros rpo_infos n; induction n as [ | n]; intros t1 t2 St t1_lt_t2. absurd (1 <= 0); auto with arith; apply Nat.le_trans with (size t1 + size t2); trivial; apply Nat.le_trans with (1 + size t2); [apply Nat.le_add_r | apply Nat.add_le_mono_r; apply size_ge_one]. assert (TE := @equiv_eval_terminates rpo_infos _ _ _ St); assert (R := rpo_eval_is_sound_weak rpo_infos (S n) t1 t2); assert (T := @rpo_eval_terminates rpo_infos (S n) t1 t2 St). rewrite Nat.add_comm in St; assert (TE' := @equiv_eval_terminates rpo_infos _ _ _ St); assert (R' := rpo_eval_is_sound_weak rpo_infos (S n) t2 t1); assert (T' := @rpo_eval_terminates rpo_infos (S n) t2 t1 St). do 2 rewrite rpo_eval_equation; rewrite rpo_eval_equation in R; rewrite rpo_eval_equation in T; rewrite rpo_eval_equation in R'; rewrite rpo_eval_equation in T'. revert R T R' T'. case_eq (mem_bool eq_tt_bool (t1, t2) (rpo_l rpo_infos)); intro Heq_1; case_eq (mem_bool eq_tt_bool (t2, t1) (rpo_l rpo_infos)); intro Heq_2; case_eq (mem_bool eq_tt_bool (t1, t2) (equiv_l rpo_infos)); intro Heq_3; case_eq (mem_bool eq_tt_bool (t2, t1) (equiv_l rpo_infos)); intro Heq_4; intros R T R' T'; try (absurd (rpo rpo_infos.(bb) t1 t1);[ intro; apply (@rpo_antirefl rpo_infos.(bb) t1); trivial| apply rpo_trans with t2;assumption]); try (solve[intuition]); try (absurd (rpo rpo_infos.(bb) t1 t1); [intro; apply (@rpo_antirefl rpo_infos.(bb) t1); trivial | rewrite (@equiv_rpo_equiv_1 _ _ _ R') in t1_lt_t2; trivial]). clear Heq_1 Heq_2 Heq_3 Heq_4. destruct (equiv_eval rpo_infos (S n) t1 t2) as [ [ | ] | ]; destruct (equiv_eval rpo_infos (S n) t2 t1) as [ [ | ] | ]; try (absurd (rpo rpo_infos.(bb) t1 t1); [ intro; apply (@rpo_antirefl rpo_infos.(bb) t1); trivial | rewrite <- (equiv_rpo_equiv_1 _ R) in t1_lt_t2; trivial]); try solve[intuition]; try (absurd (rpo rpo_infos.(bb) t1 t1); [intro; apply (@rpo_antirefl rpo_infos.(bb) t1); trivial| rewrite (equiv_rpo_equiv_1 _ R') in t1_lt_t2; trivial]). clear TE TE'. destruct t1 as [v1 | f1 l1]; destruct t2 as [v2 | f2 l2]. inversion t1_lt_t2. rewrite (@var_case2 _ _ _ _ t1_lt_t2); split; trivial. inversion t1_lt_t2. assert (Sl : forall t1 t2, In t1 l1 -> In t2 l2 -> size t1 + size t2 <= n). intros t1 t2 t1_in_l1 t2_in_l2; apply le_S_n; refine (Nat.le_trans _ _ _ _ St); replace (S (size t1 + size t2)) with (S (size t1) + size t2); trivial; rewrite Nat.add_comm; apply Nat.add_le_mono. apply Nat.lt_le_incl; apply size_direct_subterm; trivial. apply size_direct_subterm; trivial. assert (IHl1l2 : forall t1 t2, In t1 l1 -> In t2 l2 -> rpo rpo_infos.(bb) t1 t2 -> rpo_eval rpo_infos n t1 t2 = Some Less_than /\ rpo_eval rpo_infos n t2 t1 = Some Greater_than). intros; apply IHn; trivial. apply Sl; trivial. assert (IHl2l1 : forall t1 t2, In t1 l1 -> In t2 l2 -> rpo rpo_infos.(bb) t2 t1 -> rpo_eval rpo_infos n t2 t1 = Some Less_than /\ rpo_eval rpo_infos n t1 t2 = Some Greater_than). intros; apply IHn; trivial. rewrite Nat.add_comm; apply Sl; trivial. assert (IHl1s2 : forall t1, In t1 l1 -> rpo rpo_infos.(bb) t1 (Term f2 l2) -> rpo_eval rpo_infos n t1 (Term f2 l2) = Some Less_than /\ rpo_eval rpo_infos n (Term f2 l2) t1 = Some Greater_than). intros; apply IHn; trivial. apply le_S_n; refine (Nat.le_trans _ _ _ _ St); replace (S (size t1 + size (Term f2 l2))) with (S (size t1) + size (Term f2 l2)); trivial; rewrite Nat.add_comm; apply Nat.add_le_mono_l. apply size_direct_subterm; trivial. assert (IHs2l1 : forall t1, In t1 l1 -> rpo rpo_infos.(bb) (Term f2 l2) t1 -> rpo_eval rpo_infos n (Term f2 l2) t1 = Some Less_than /\ rpo_eval rpo_infos n t1 (Term f2 l2) = Some Greater_than). intros; apply IHn; trivial. rewrite Nat.add_comm; apply le_S_n; refine (Nat.le_trans _ _ _ _ St); replace (S (size t1 + size (Term f2 l2))) with (S (size t1) + size (Term f2 l2)); trivial; rewrite Nat.add_comm; apply Nat.add_le_mono_l. apply size_direct_subterm; trivial. assert (IHs1l2 : forall t2, In t2 l2 -> rpo rpo_infos.(bb) (Term f1 l1) t2 -> rpo_eval rpo_infos n (Term f1 l1) t2 = Some Less_than /\ rpo_eval rpo_infos n t2 (Term f1 l1) = Some Greater_than). intros; apply IHn; trivial. rewrite Nat.add_comm; apply le_S_n; refine (Nat.le_trans _ _ _ _ St); replace (S (size t2 + size (Term f1 l1))) with (S (size t2) + size (Term f1 l1)); trivial; apply Nat.add_le_mono_r. apply size_direct_subterm; trivial. assert (IHl2s1 : forall t2, In t2 l2 -> rpo rpo_infos.(bb) t2 (Term f1 l1) -> rpo_eval rpo_infos n t2 (Term f1 l1) = Some Less_than /\ rpo_eval rpo_infos n (Term f1 l1) t2 = Some Greater_than). intros; apply IHn; trivial. apply le_S_n; refine (Nat.le_trans _ _ _ _ St); replace (S (size t2 + size (Term f1 l1))) with (S (size t2) + size (Term f1 l1)); trivial; apply Nat.add_le_mono_r. apply size_direct_subterm; trivial. inversion t1_lt_t2 as [ f2' l2' u1 s2 s2_in_l2 u1_le_s2 | f2' f1' l2' l1' f1_lt_f2 H | f g l2' l1' Sf Sg f_eq_g L l1_lt_l2 H | f g l2' l1' Sf Sg f_eq_g l1_lt_l2]; subst. split. 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 [ [ | ] | ]. simpl in R; destruct (rpo_closure rpo_infos.(bb) (Term f1 l1) (Term f2 l2) (Term f2 l2)) as [_ [Antisym _]]. apply False_rect; apply Antisym; trivial. assert (t1_lt_l2 : 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 = Some true). apply list_exists_option_is_complete_true. destruct (mem_split_set _ _ equiv_bool_ok _ _ s2_in_l2) as [s2' [l2' [l2'' [s2_eq_s2' [H _]]]]]. simpl in s2_eq_s2'; simpl in H. assert (s2'_in_l2 : In s2' l2). subst l2; apply in_or_app; right; left; trivial. exists s2'; split; trivial. rewrite (equiv_rpo_equiv_3 _ s2_eq_s2') in u1_le_s2. inversion u1_le_s2; subst. rewrite (@rpo_eval_is_complete_equivalent rpo_infos n (Term f1 l1) s2'); trivial. rewrite Nat.add_comm; apply le_S_n; refine (Nat.le_trans _ _ _ _ St); replace (S (size s2' + size (Term f1 l1))) with (S (size s2') + size (Term f1 l1)); trivial; apply Nat.add_le_mono_r. apply size_direct_subterm; simpl; trivial. destruct (IHs1l2 s2' s2'_in_l2 H0) as [H1 _]; rewrite H1; trivial. rewrite t1_lt_l2; simpl; trivial. absurd (@None comp = None); trivial. assert (l2_gt_t1 : list_exists_option (fun t : term => match rpo_eval rpo_infos n t (Term f1 l1) with | Some Equivalent => Some true | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None (A:=bool) end) l2 = Some true). apply list_exists_option_is_complete_true. destruct (mem_split_set _ _ equiv_bool_ok _ _ s2_in_l2) as [s2' [l2' [l2'' [s2_eq_s2' [H _]]]]]. simpl in s2_eq_s2'; simpl in H. assert (s2'_in_l2 : In s2' l2). subst l2; apply in_or_app; right; left; trivial. exists s2'; split; trivial. inversion u1_le_s2; subst. rewrite (@rpo_eval_is_complete_equivalent rpo_infos n s2' (Term f1 l1)); trivial. apply le_S_n; refine (Nat.le_trans _ _ _ _ St); replace (S (size s2' + size (Term f1 l1))) with (S (size s2') + size (Term f1 l1)); trivial; apply Nat.add_le_mono_r. apply size_direct_subterm; trivial. symmetry; transitivity s2; trivial. rewrite (equiv_rpo_equiv_1 _ s2_eq_s2') in H0. destruct (IHs1l2 s2' s2'_in_l2 H0) as [_ H2]; rewrite H2; trivial. rewrite l2_gt_t1; simpl; trivial. split; [clear R' T' | clear R T]. 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 [ [ | ] | ]. simpl in R. destruct (rpo_closure rpo_infos.(bb) (Term f1 l1) (Term f2 l2) (Term f2 l2)) as [_ [Antisym _]]. apply False_rect; apply Antisym; trivial. 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 [ [ | ] | ]. trivial. generalize (prec_eval_is_sound f1 f2); destruct (prec_eval f1 f2). intro. apply False_rect; apply (prec_antisym Prec f2); trivial. assert (H5: False). apply prec_not_prec_eq with symbol Prec f1 f2; trivial. contradict H5. intros _; assert (H' : 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 = Some true). apply list_forall_option_is_complete_true. intros u1 u1_in_l1; destruct (IHl1s2 u1 u1_in_l1) as [H1 _]. apply H; apply in_impl_mem; trivial. exact Eq. rewrite H1; trivial. rewrite H'; trivial. intro f2_lt_f1; apply False_rect; apply (prec_antisym Prec f1); apply prec_transitive with f2; trivial. intros [_ [not_f1_lt_f2 _]]; absurd (prec Prec f1 f2); trivial. absurd (@None comp = None); trivial. absurd (@None comp = None); trivial. destruct (list_exists_option (fun t : term => match rpo_eval rpo_infos n t (Term f1 l1) with | Some Equivalent => Some true | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None (A:=bool) end) l2) as [ [ | ] | ]. trivial. destruct (list_exists_option (fun t : term => match rpo_eval rpo_infos n (Term f2 l2) 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) l1) as [ [ | ] | ]. simpl in R'. destruct (rpo_closure rpo_infos.(bb) (Term f1 l1) (Term f2 l2) (Term f2 l2)) as [_ [Antisym _]]. apply False_rect; apply Antisym; trivial. generalize (prec_eval_is_sound f2 f1); destruct (prec_eval f2 f1). intro; apply False_rect; apply (prec_antisym Prec f1); trivial. assert (H5: False). apply prec_not_prec_eq with symbol Prec f1 f2; trivial. apply prec_eq_sym; trivial. contradict H5. intro f2_lt_f1; apply False_rect; apply (prec_antisym Prec f1); apply prec_transitive with f2; trivial. intros _; assert (H' : list_forall_option (fun t : term => match rpo_eval rpo_infos n (Term f2 l2) 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) l1 = Some true). apply list_forall_option_is_complete_true. intros u1 u1_in_l1; destruct (IHl1s2 u1 u1_in_l1) as [_ H2]. apply H; apply in_impl_mem; trivial. exact Eq. rewrite H2; trivial. rewrite H'; trivial. intros [_ [_ not_f1_lt_f2]]; absurd (prec Prec f1 f2); trivial. absurd (@None comp = None); trivial. absurd (@None comp = None); trivial. split; [clear R' T' | clear R T]. case_eq (Nat.eqb (length l1) (length l2) || leb (length l1) (bb rpo_infos) && leb (length l2) (bb rpo_infos)). clear L; intros L; rewrite L in R, T; clear L. set (s1 := Term f1 l1) in *; clearbody s1. set (s2 := Term f2 l2) in *; clearbody s2. destruct (list_exists_option (fun t : term => match rpo_eval rpo_infos n t s2 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 [ [ | ] | ]. simpl in R. destruct (rpo_closure rpo_infos.(bb) s1 s2 s2) as [_ [Antisym _]]. apply False_rect; apply Antisym; trivial. destruct (list_exists_option (fun t : term => match rpo_eval rpo_infos n s1 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 [ [ | ] | ]. trivial. simpl; generalize (prec_eval_is_sound f1 f2); destruct (prec_eval f1 f2). intros _; rewrite Sf; rewrite Sf in R; rewrite Sf in T; simpl in R; simpl in T. revert t1_lt_t2 H St IHl1l2 IHl2l1 IHl1s2 IHs2l1 IHs1l2 IHl2s1 R T l1_lt_l2 Sl. clear; revert s1 s2 l2; induction l1 as [ | t1 l1]; intros s1 s2 [ | t2 l2]; intros. inversion l1_lt_l2. apply eq_refl. inversion l1_lt_l2. inversion l1_lt_l2; subst. simpl; rewrite (proj1 (IHl1l2 _ _ (or_introl _ (eq_refl _)) (or_introl _ (eq_refl _)) H1)). unfold term_gt_list. assert (H' : list_forall_option (fun t : term => match rpo_eval rpo_infos n s2 t with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) (t1 :: l1) = Some true). apply list_forall_option_is_complete_true. intros u1 u1_in_t1l1. assert (u1_lt_s2 : rpo rpo_infos.(bb) u1 s2). apply H; apply in_impl_mem; trivial; exact Eq. rewrite (proj2 (IHl1s2 _ u1_in_t1l1 u1_lt_s2)); apply eq_refl. rewrite H'; apply eq_refl. simpl. assert (H' := @rpo_eval_is_complete_equivalent rpo_infos n t1 t2). generalize (H' (Sl _ _ (or_introl _ (eq_refl _)) (or_introl _ (eq_refl _))) H3); clear H'; intro H'; rewrite H'. apply IHl1; trivial. intros; apply H; right; assumption. intros; apply IHl1l2; trivial; right; assumption. intros; apply IHl2l1; trivial; right; assumption. intros; apply IHl1s2; trivial; right; assumption. intros; apply IHs2l1; trivial; right; assumption. intros; apply IHs1l2; trivial; right; assumption. intros; apply IHl2s1; trivial; right; assumption. simpl in R; rewrite H' in R; assumption. simpl in T; rewrite H' in T; assumption. intros; apply Sl; right; assumption. intro. assert (H4: False). apply prec_not_prec_eq with symbol Prec f1 f2; trivial. contradict H4. intro. assert (H4: False). apply prec_not_prec_eq with symbol Prec f2 f1; trivial. apply prec_eq_sym; trivial. contradict H4. intros [f2_diff_f2 _]; absurd (f2 = f2); trivial. simpl in T; absurd (@None comp = None); trivial. simpl in T; absurd (@None comp = None); trivial. contradict f2_diff_f2; trivial. simpl in T; absurd (@None comp = None); trivial. simpl in T; absurd (@None comp = None); trivial. destruct L as [L | [L1 L2]]. rewrite L; rewrite Nat.eqb_refl; intro; discriminate. rewrite (leb_correct _ _ L1); rewrite (leb_correct _ _ L2); rewrite orb_true_r; intro; discriminate. case_eq (Nat.eqb (length l2) (length l1) || leb (length l2) (bb rpo_infos) && leb (length l1) (bb rpo_infos)). clear L; intros L; rewrite L in R', T'; clear L. set (s1 := Term f1 l1) in *; clearbody s1. set (s2 := Term f2 l2) in *; clearbody s2. destruct (list_exists_option (fun t : term => match rpo_eval rpo_infos n t s1 with | Some Equivalent => Some true | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None (A:=bool) end) l2) as [ [ | ] | ]. trivial. destruct (list_exists_option (fun t : term => match rpo_eval rpo_infos n s2 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) l1) as [ [ | ] | ]. simpl in R'. destruct (rpo_closure rpo_infos.(bb) s2 s1 s2) as [_ [Antisym _]]. apply False_rect; apply Antisym; trivial. simpl; generalize (prec_eval_is_sound f2 f1); destruct (prec_eval f2 f1). intros _; rewrite Sg; rewrite Sg in R'; rewrite Sg in T'; simpl in R'; simpl in T'. revert t1_lt_t2 H St IHl1l2 IHl2l1 IHl1s2 IHs2l1 IHs1l2 IHl2s1 R' T' l1_lt_l2 Sl. clear; revert s1 s2 l1; induction l2 as [ | t2 l2]; intros s1 s2 [ | t1 l1]; intros. inversion l1_lt_l2. inversion l1_lt_l2. apply eq_refl. inversion l1_lt_l2; subst. simpl; rewrite (proj2 (IHl1l2 _ _ (or_introl _ (eq_refl _)) (or_introl _ (eq_refl _)) H1)). unfold term_gt_list. assert (H' : list_forall_option (fun t : term => match rpo_eval rpo_infos n s2 t with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) (t1 :: l1) = Some true). apply list_forall_option_is_complete_true. intros u1 u1_in_t1l1. assert (u1_lt_s2 : rpo rpo_infos.(bb) u1 s2). apply H; apply in_impl_mem; trivial; exact Eq. rewrite (proj2 (IHl1s2 _ u1_in_t1l1 u1_lt_s2)); apply eq_refl. rewrite H'; apply eq_refl. simpl. assert (H' := @rpo_eval_is_complete_equivalent rpo_infos n t2 t1). rewrite Nat.add_comm in H'; generalize (H' (Sl _ _ (or_introl _ (eq_refl _)) (or_introl _ (eq_refl _))) (@Equivalence_Symmetric _ _ equiv_equiv _ _ H3)); clear H'; intro H'; rewrite H'. apply IHl2; trivial. intros; apply H; right; assumption. intros; apply IHl1l2; trivial; right; assumption. intros; apply IHl2l1; trivial; right; assumption. intros; apply IHl1s2; trivial; right; assumption. intros; apply IHs2l1; trivial; right; assumption. intros; apply IHs1l2; trivial; right; assumption. intros; apply IHl2s1; trivial; right; assumption. simpl in R'; rewrite H' in R'; assumption. simpl in T'; rewrite H' in T'; assumption. intros; apply Sl; right; assumption. intro. assert (H4: False). apply prec_not_prec_eq with symbol Prec f2 f1; trivial. apply prec_eq_sym; trivial. contradict H4. intro. assert (H4: False). apply prec_not_prec_eq with symbol Prec f1 f2; trivial. contradict H4. intros [f2_diff_f2 _]; absurd (f2 = f2); trivial. contradict f2_diff_f2. apply prec_eq_sym; trivial. simpl in T'; absurd (@None comp = None); trivial. simpl in T'; absurd (@None comp = None); trivial. destruct L as [L | [L1 L2]]. rewrite L; rewrite Nat.eqb_refl; intro; discriminate. rewrite (leb_correct _ _ L1); rewrite (leb_correct _ _ L2); rewrite orb_true_r; intro; discriminate. set (s1 := Term f1 l1) in *. set (s2 := Term f2 l2) in *. split; [clear R' T' | clear R T]. destruct (list_exists_option (fun t : term => match rpo_eval rpo_infos n t s2 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 [ [ | ] | ]. simpl in R; destruct (rpo_closure rpo_infos.(bb) s1 s2 s2) as [_ [Antisym _]]. apply False_rect; apply Antisym; trivial. destruct (list_exists_option (fun t : term => match rpo_eval rpo_infos n s1 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 [ [ | ] | ]. trivial. simpl; generalize (prec_eval_is_sound f1 f2); destruct (prec_eval f1 f2). intros _; rewrite Sf; rewrite Sf in R; rewrite Sf in T; simpl in R; simpl in T. assert (H' := remove_equiv_eval_list_is_sound (equiv_eval rpo_infos n) l1 l2). case_eq (remove_equiv_eval_list (equiv_eval rpo_infos n) l1 l2). intros [l1' l2'] H; rewrite H in R, T, H'. assert (H'' : rpo_mul (bb rpo_infos) l1' l2'). destruct H' as [ll [Ell [P1 [P2 _]]]]. assert (Ell' : forall t1 t2, In (t1,t2) ll -> equiv t1 t2). intros t1 t2 t1t2_in_ll. generalize (equiv_eval_is_sound_weak rpo_infos n t1 t2). rewrite (Ell _ _ t1t2_in_ll); intro t1_eq_t2; apply t1_eq_t2; apply eq_refl. revert Ell' l1_lt_l2 P1 P2; clear; revert l1 l2 l1' l2'; induction ll as [ | [t1 t2] ll]; intros l1 l2 l1' l2' Ell l1_lt_l2 P1 P2. rewrite <- app_nil_end in P1. rewrite <- app_nil_end in P2. inversion l1_lt_l2; subst. apply (@List_mul _ a lg ls lc); trivial. transitivity l1; [symmetry; apply permut_impl with eq | idtac]; trivial. intros a' b a_eq_b; subst a'; apply Eq. transitivity l2; [symmetry; apply permut_impl with eq | idtac]; trivial. intros a' b a_eq_b; subst a'; apply Eq. apply (@rpo_mul_remove_equiv_aux rpo_infos.(bb) l1' l2' t1 t2). intros t _; apply (@rpo_antirefl rpo_infos.(bb) t); trivial. apply Ell; left; apply eq_refl. apply IHll with l1 l2; trivial. intros; apply Ell; right; assumption. refine (list_permut.permut_trans _ P1 _). intros; subst; apply eq_refl. apply list_permut.permut_sym. intros; subst; apply eq_refl. simpl; apply Pcons; [trivial | apply list_permut.permut_refl; intros; trivial]. refine (list_permut.permut_trans _ P2 _). intros; subst; apply eq_refl. apply list_permut.permut_sym. intros; subst; apply eq_refl. simpl; apply Pcons; [trivial | apply list_permut.permut_refl; intros; trivial]. destruct l1' as [ | t1' l1']; destruct l2' as [ | t2' l2']. absurd (rpo rpo_infos.(bb) s1 s1). intro; apply (@rpo_antirefl rpo_infos.(bb) s1); trivial. rewrite <- (equiv_rpo_equiv_1 _ R) in t1_lt_t2; trivial. trivial. absurd (rpo rpo_infos.(bb) s1 s1). intro; apply (@rpo_antirefl rpo_infos.(bb) s1); trivial. apply rpo_trans with s2; trivial. unfold mult_eval, list_gt_list; unfold mult_eval, list_gt_list in R,T. destruct (list_forall_option (fun t2 : term => list_exists_option (fun t1 : term => match rpo_eval rpo_infos n t1 t2 with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None (A:=bool) end) (t1' :: l1')) (t2' :: l2')) as [ [ | ] | ]. absurd (rpo rpo_infos.(bb) s1 s1). intro; apply (@rpo_antirefl rpo_infos.(bb) s1); trivial. apply rpo_trans with s2; trivial. assert (K : list_forall_option (fun t1 : term => list_exists_option (fun t2 : term => match rpo_eval rpo_infos n t2 t1 with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None (A:=bool) end) (t2' :: l2')) (t1' :: l1') = Some true). apply list_forall_option_is_complete_true. intros u1 u1_in_l1'; apply list_exists_option_is_complete_true. inversion H''; subst. assert (u1_in_l1 : In u1 l1). destruct H' as [ll [ _ [P1 _]]]. rewrite (in_permut_in P1); apply in_or_app; left; trivial. assert (u1_mem_ls_lc : mem equiv u1 (ls ++ lc)). rewrite <- (mem_permut0_mem equiv_equiv u1 H0); apply in_impl_mem; trivial. exact Eq. rewrite <- mem_or_app in u1_mem_ls_lc. destruct u1_mem_ls_lc as [u1_mem_ls | u1_mem_lc]. destruct (H2 _ u1_mem_ls) as [a' [a'_in_lg u1_lt_a']]. assert (a'_in_tl2' : mem equiv a' (t2' :: l2')). rewrite (mem_permut0_mem equiv_equiv a' H1). rewrite app_comm_cons; rewrite <- mem_or_app; left; assumption. rewrite mem_in_eq in a'_in_tl2'; destruct a'_in_tl2' as [a'' [a''_eq_a' a''_in_tl2']]. exists a''; split. assumption. assert (u1_lt_a'' : rpo (bb rpo_infos) u1 a''). rewrite <- (equiv_rpo_equiv_1 _ a''_eq_a'); trivial. assert (a''_in_l2 : In a'' l2). destruct H' as [ll [ _ [_ [P2 _]]]]. rewrite (in_permut_in P2); apply in_or_app; left; trivial. rewrite (proj2 (IHl1l2 u1 a'' u1_in_l1 a''_in_l2 u1_lt_a'')); apply eq_refl. assert (u1_mem_tl2' : exists u2, equiv u1 u2 /\ In u2 (t2' :: l2')). rewrite <- (mem_in_eq equiv). rewrite (mem_permut0_mem equiv_equiv u1 H1). rewrite app_comm_cons; rewrite <- mem_or_app; right; assumption. destruct u1_mem_tl2' as [u2 [u1_eq_u2 u2_in_tl2']]. destruct H' as [ll [ _ [_ [P2 H']]]]. assert (K := H' _ _ u1_in_l1' u2_in_tl2'). assert (Su : size u1 + size u2 <= n). apply Sl; [idtac | rewrite (in_permut_in P2); apply in_or_app; left]; assumption. apply False_rect; generalize (@equiv_eval_is_sound rpo_infos n u1 u2 Su); rewrite K; intro E; apply E; assumption. rewrite K; apply eq_refl. apply False_rect; apply T; apply eq_refl. intros H; rewrite H in T; apply False_rect; apply T; apply eq_refl. intro; apply False_rect; apply (prec_antisym Prec f2); trivial. assert (H4: False). apply prec_not_prec_eq with symbol Prec f1 f2; trivial. contradict H4. intro; apply False_rect; apply (prec_antisym Prec f1); trivial. assert (H4: False). apply prec_not_prec_eq with symbol Prec f2 f1; trivial. apply prec_eq_sym; trivial. contradict H4. intros [f2_diff_f2 _]; absurd (f2 = f2); trivial. contradict f2_diff_f2; trivial. apply False_rect; apply T; apply eq_refl. apply False_rect; apply T; apply eq_refl. destruct (list_exists_option (fun t : term => match rpo_eval rpo_infos n t s1 with | Some Equivalent => Some true | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None (A:=bool) end) l2) as [ [ | ] | ]. trivial. destruct (list_exists_option (fun t : term => match rpo_eval rpo_infos n s2 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) l1) as [ [ | ] | ]. simpl in R'; destruct (rpo_closure rpo_infos.(bb) s1 s2 s2) as [_ [Antisym _]]. apply False_rect; apply Antisym; trivial. simpl; generalize (prec_eval_is_sound f2 f1); destruct (prec_eval f2 f1). intros _; rewrite Sg; rewrite Sg in R'; rewrite Sg in T'; simpl in R'; simpl in T'. assert (H' := remove_equiv_eval_list_is_sound (equiv_eval rpo_infos n) l2 l1). case_eq (remove_equiv_eval_list (equiv_eval rpo_infos n) l2 l1). intros [l2' l1'] H; rewrite H in R', T', H'. assert (H'' : rpo_mul (bb rpo_infos) l1' l2'). destruct H' as [ll [Ell [P2 [P1 _]]]]. assert (Ell' : forall t1 t2, In (t1,t2) ll -> equiv t1 t2). intros t1 t2 t1t2_in_ll. generalize (equiv_eval_is_sound_weak rpo_infos n t1 t2). rewrite (Ell _ _ t1t2_in_ll); intro t1_eq_t2; apply t1_eq_t2; apply eq_refl. revert Ell' l1_lt_l2 P1 P2; clear; revert l1 l2 l1' l2'; induction ll as [ | [t2 t1] ll]; intros l1 l2 l1' l2' Ell l1_lt_l2 P1 P2. rewrite <- app_nil_end in P1. rewrite <- app_nil_end in P2. inversion l1_lt_l2; subst. apply (@List_mul _ a lg ls lc); trivial. transitivity l1; [symmetry; apply permut_impl with eq | idtac]; trivial. intros a' b a_eq_b; subst a'; apply Eq. transitivity l2; [symmetry; apply permut_impl with eq | idtac]; trivial. intros a' b a_eq_b; subst a'; apply Eq. apply (@rpo_mul_remove_equiv_aux rpo_infos.(bb) l1' l2' t1 t2). intros t _; apply (@rpo_antirefl rpo_infos.(bb) t); trivial. symmetry; apply Ell; left; apply eq_refl. apply IHll with l1 l2; trivial. intros; apply Ell; right; assumption. refine (list_permut.permut_trans _ P1 _). intros; subst; apply eq_refl. apply list_permut.permut_sym. intros; subst; apply eq_refl. simpl; apply Pcons; [trivial | apply list_permut.permut_refl; intros; trivial]. refine (list_permut.permut_trans _ P2 _). intros; subst; apply eq_refl. apply list_permut.permut_sym. intros; subst; apply eq_refl. simpl; apply Pcons; [trivial | apply list_permut.permut_refl; intros; trivial]. destruct l1' as [ | t1' l1']; destruct l2' as [ | t2' l2']. absurd (rpo rpo_infos.(bb) s2 s2). intro; apply (@rpo_antirefl rpo_infos.(bb) s2); trivial. rewrite <- (equiv_rpo_equiv_2 _ R') in t1_lt_t2; trivial. trivial. absurd (rpo rpo_infos.(bb) s2 s2). intro; apply (@rpo_antirefl rpo_infos.(bb) s2); trivial. apply rpo_trans with s1; trivial. unfold mult_eval, list_gt_list; unfold mult_eval, list_gt_list in R', T'. assert (K : list_forall_option (fun t2 : term => list_exists_option (fun t1 : term => match rpo_eval rpo_infos n t1 t2 with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None (A:=bool) end) (t2' :: l2')) (t1' :: l1') = Some true). apply list_forall_option_is_complete_true. intros u1 u1_in_l1'; apply list_exists_option_is_complete_true. inversion H''; subst. assert (u1_in_l1 : In u1 l1). destruct H' as [ll [ _ [_ [P1 _]]]]. rewrite (in_permut_in P1); apply in_or_app; left; trivial. assert (u1_mem_ls_lc : mem equiv u1 (ls ++ lc)). rewrite <- (mem_permut0_mem equiv_equiv u1 H0); apply in_impl_mem; trivial. exact Eq. rewrite <- mem_or_app in u1_mem_ls_lc. destruct u1_mem_ls_lc as [u1_mem_ls | u1_mem_lc]. destruct (H2 _ u1_mem_ls) as [a' [a'_in_lg u1_lt_a']]. assert (a'_in_tl2' : mem equiv a' (t2' :: l2')). rewrite (mem_permut0_mem equiv_equiv a' H1). rewrite app_comm_cons; rewrite <- mem_or_app; left; assumption. rewrite mem_in_eq in a'_in_tl2'; destruct a'_in_tl2' as [a'' [a''_eq_a' a''_in_tl2']]. exists a''; split. assumption. assert (u1_lt_a'' : rpo (bb rpo_infos) u1 a''). rewrite <- (equiv_rpo_equiv_1 _ a''_eq_a'); trivial. assert (a''_in_l2 : In a'' l2). destruct H' as [ll [ _ [P2 _]]]. rewrite (in_permut_in P2); apply in_or_app; left; trivial. rewrite (proj2 (IHl1l2 u1 a'' u1_in_l1 a''_in_l2 u1_lt_a'')); apply eq_refl. assert (u1_mem_tl2' : exists u2, equiv u1 u2 /\ In u2 (t2' :: l2')). rewrite <- (mem_in_eq equiv). rewrite (mem_permut0_mem equiv_equiv u1 H1). rewrite app_comm_cons; rewrite <- mem_or_app; right; assumption. destruct u1_mem_tl2' as [u2 [u1_eq_u2 u2_in_tl2']]. destruct H' as [ll [ _ [P2 [_ H']]]]. assert (K := H' _ _ u2_in_tl2' u1_in_l1'). assert (Su : size u2 + size u1 <= n). rewrite Nat.add_comm; apply Sl; [idtac | rewrite (in_permut_in P2); apply in_or_app; left]; assumption. apply False_rect; generalize (@equiv_eval_is_sound rpo_infos n u2 u1 Su); rewrite K; intro E; apply E. symmetry; assumption. rewrite K; apply eq_refl. intros H; rewrite H in T'; apply False_rect; apply T'; apply eq_refl. intro. assert (H4: False). apply prec_not_prec_eq with symbol Prec f2 f1; trivial. apply prec_eq_sym; trivial. contradict H4. intro; apply False_rect; apply (prec_antisym Prec f2); trivial. assert (H4: False). apply prec_not_prec_eq with symbol Prec f1 f2; trivial. contradict H4. intros [f2_diff_f2 _]; absurd (f2 = f2); trivial. contradict f2_diff_f2. apply prec_eq_sym; trivial. apply False_rect; apply T'; apply eq_refl. apply False_rect; apply T'; apply eq_refl. 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)