proposition: Lemma equiv_eval_is_sound_weak : forall rpo_infos n t1 t2, equiv_eval rpo_infos n t1 t2 = Some true -> equiv t1 t2.
proof: Proof. intros rpo_infos n; induction n as [ | n]. intros; discriminate. destruct t1 as [v1 | f1 l1]; destruct t2 as [v2 | f2 l2]; simpl. generalize (X.eq_bool_ok v1 v2); case (X.eq_bool v1 v2); [intro v1_eq_v2 | intro v1_diff_v2]. subst; intuition; apply Eq. intro; discriminate. intro; discriminate. intro; discriminate. case_eq (mem_bool eq_tt_bool ((Term f1 l1), (Term f2 l2)) (equiv_l rpo_infos));simpl. intros H _ ;eapply find_is_sound with (1:=equiv_l_valid rpo_infos);auto. intros _. case_eq (prec_eq_bool Prec f1 f2); [intro f1_eq_f2 | intro f1_diff_f2]. case_eq (status Prec f1). intros Status. intro H; apply Eq_lex; trivial. assert (H1:= prec_eq_status). assert (H1':= H1 symbol Prec f1 f2). assert (status Prec f1 = status Prec f2). apply H1'; trivial. trivial. assert (H3:= prec_eq_bool_ok). assert (H3':= H3 symbol Prec f1 f2). rewrite f1_eq_f2 in H3'. trivial. rewrite <- H0. trivial. assert (H3:= prec_eq_bool_ok). assert (H3':= H3 symbol Prec f1 f2). rewrite f1_eq_f2 in H3'. trivial. generalize l1 l2 H; clear l1 l2 H; intro l; induction l as [ | t l]; intros [ | t' l'] H. apply Eq_list_nil. discriminate. discriminate. simpl in H; apply Eq_list_cons. apply IHn; destruct (equiv_eval rpo_infos n t t') as [ [ | ] | ]; trivial; discriminate. apply IHl; destruct (equiv_eval rpo_infos n t t') as [ [ | ] | ]; trivial; discriminate. intro Status. intro H; assert (H' := remove_equiv_eval_list_is_sound (equiv_eval rpo_infos n) l1 l2); destruct (remove_equiv_eval_list (equiv_eval rpo_infos n) l1 l2) as [ [l1' l2'] | ]. destruct H' as [ll [E_ll [P1 [P2 H']]]]; apply Eq_mul; trivial. assert (H1:= prec_eq_status). assert (H1':= H1 symbol Prec f1 f2). assert (status Prec f1 = status Prec f2). apply H1'; trivial. trivial. assert (H3:= prec_eq_bool_ok). assert (H3':= H3 symbol Prec f1 f2). rewrite f1_eq_f2 in H3'. trivial. rewrite <- H0. trivial. assert (H3:= prec_eq_bool_ok). assert (H3':= H3 symbol Prec f1 f2). rewrite f1_eq_f2 in H3'. trivial. destruct l1'; destruct l2'; try discriminate; simpl in P1; trivial. generalize l1 l2 P1 P2; clear l1 l2 P1 P2; induction ll as [ | [t1 t2] ll]; intros l1 l2 P1 P2. rewrite (permut_nil P1); rewrite (permut_nil P2); apply Pnil. destruct (permut_inv_right P1) as [t1' [l1' [l1'' [t1_eq_t1' [H'' Q1]]]]]; subst l1 t1'. destruct (permut_inv_right P2) as [t2' [l2' [l2'' [t2_eq_t2' [H'' Q2]]]]]; subst l2 t2'. simpl; apply permut_strong. apply IHn; apply E_ll; left; trivial. apply IHll; trivial. intros; apply E_ll; right; trivial. discriminate. intro; discriminate. 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)