proposition: Lemma equiv_eval_is_complete_true : forall rpo_infos n t1 t2, size t1 + size t2 <= n -> equiv t1 t2 -> equiv_eval rpo_infos n t1 t2 = Some true.
proof: Proof. intros rpo_infos n; induction n as [ | n ]. intros t1 t2 St; absurd (1 <= 0); auto with arith. refine (Nat.le_trans _ _ _ _ St); apply Nat.le_trans with (size t1); [ apply size_ge_one | apply Nat.le_add_r]. intros t1 t2 St t1_eq_t2; inversion t1_eq_t2 as [ t | f g l1 l2 Sf Sg f_eq_g | f g l1 l2 Sf Sg f_eq_g P1 P2]; subst. destruct t2 as [v2 | f2 l2]; simpl. generalize (X.eq_bool_ok v2 v2); case (X.eq_bool v2 v2); [intros _ | intro v2_diff_v2; absurd (v2 = v2)]; trivial. case (mem_bool eq_tt_bool (Term f2 l2, Term f2 l2) (equiv_l rpo_infos)); [reflexivity | idtac]. case_eq (prec_eq_bool Prec f2 f2). intro H. clear H. assert (H : forall t2, In t2 l2 -> equiv_eval rpo_infos n t2 t2 = Some true). intros t2 t2_in_l2; apply IHn. apply le_S_n; refine (Nat.le_trans _ _ _ _ St); replace (S (size t2 + size t2)) with (S (size t2) + size t2); trivial; apply Nat.add_le_mono; [idtac | apply Nat.lt_le_incl]; apply size_direct_subterm; trivial. apply Eq. destruct (status Prec f2). clear St t1_eq_t2; induction l2 as [ | t2 l2]; simpl; trivial. rewrite (H t2); [rewrite IHl2 | left]; trivial; intros; apply H; right; trivial. assert (H' : remove_equiv_eval_list (equiv_eval rpo_infos n) l2 l2 = Some (nil,nil)). clear St t1_eq_t2; induction l2 as [ | t2 l2]; simpl; trivial. rewrite (H t2); [rewrite IHl2 | left]; trivial; intros; apply H; right; trivial. rewrite H'; trivial. intros H. assert (H2:= prec_eq_bool_ok). assert (H2':= H2 symbol Prec f2 f2). rewrite H in H2'. contradict H2'. apply prec_eq_refl. rewrite equiv_eval_equation. case (mem_bool eq_tt_bool (Term f l1, Term g l2) (equiv_l rpo_infos)); [reflexivity | idtac]. rewrite Sf; generalize (F.Symb.eq_bool_ok f f); case (F.Symb.eq_bool f f); [intros _ | intro f_diff_f; absurd (f = f); trivial]. assert (Size : 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; apply Nat.add_le_mono; [idtac | apply Nat.lt_le_incl]; apply size_direct_subterm; trivial. generalize l2 H Size; clear l2 H Size St t1_eq_t2; induction l1 as [ | t1 l1]; intros l2 H Size; inversion H as [ | s t2 l l2' t1_eq_t2 l1_eq_l2']; subst; simpl. case_eq (prec_eq_bool Prec f g). intros. trivial. intro eq_f_g. assert (H1:= prec_eq_bool_ok). assert (H1':= H1 symbol Prec f g ). rewrite eq_f_g in H1'. contradict H1'; trivial. rewrite (IHn t1 t2); trivial. apply IHl1; trivial. intros; apply Size; right; trivial. apply Size; left; trivial. assert (St' : 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; apply Nat.add_le_mono; [idtac | apply Nat.lt_le_incl]; apply size_direct_subterm; trivial. assert (T : forall t1 t2, In t1 l1 -> In t2 l2 -> equiv_eval rpo_infos n t1 t2 <> None). intros t1 t2 t1_in_l1 t2_in_l2; apply equiv_eval_terminates; apply St'; trivial. assert (H' : remove_equiv_eval_list (equiv_eval rpo_infos n) l1 l2 = Some (nil,nil)). generalize l2 P1 St' T; clear l2 P1 St t1_eq_t2 St' T; induction l1 as [ | t1 l1]; intros l2 P1 St' T; inversion P1 as [ | t1' t2 l1' l2' l2'' t1_eq_t2 l1_eq_l2]; trivial. assert (H' := remove_equiv_eval_is_sound (equiv_eval rpo_infos n) t1 l2). subst; simpl. destruct (remove_equiv_eval (equiv_eval rpo_infos n) t1 (l2' ++ t2 :: l2'')) as [ | | l']. assert (H'' := H' t2); rewrite (IHn t1 t2) in H''; trivial. assert (H''' : Some true = Some false). apply H''; apply in_or_app; right; left; trivial. discriminate. apply St'. left; trivial. apply in_or_app; right; left; trivial. assert False. destruct H' as [t' [t'_in_l2 H'']]. apply (T t1 t'); trivial; left; trivial. contradiction. destruct H' as [t' [t1_eq_t' P2]]. assert (H : l2' ++ t2 :: l2'' <> nil). destruct l2' as [ | t2' l2']; simpl; discriminate. assert (Q : list_permut.permut0 (eq (A:=term)) (t2 :: l2' ++ l2'') (l2' ++ t2 :: l2'')). apply Pcons; trivial. apply list_permut.permut_refl; intro; trivial. destruct (l2' ++ t2 :: l2'') as [ | t2' k2]. absurd (@nil term = nil); trivial. apply IHl1; trivial. apply permut0_trans with (l2' ++ l2''); trivial. apply equiv_equiv. assert (t1_eq_t'' : equiv t1 t'). apply (equiv_eval_is_sound_weak _ _ _ _ t1_eq_t'). assert (t2_eq_t' : equiv t2 t'). transitivity t1; trivial; symmetry; reflexivity || trivial. rewrite (@permut0_cons _ _ equiv_equiv _ _ (l2' ++ l2'') l' t2_eq_t'). apply permut_impl with (@eq term); trivial. intros; subst; apply Eq. apply list_permut.permut_trans with (t2' :: k2); trivial. intros a b c _ _ _ a_eq_b b_eq_c; subst; trivial. intros; apply St'. right; trivial. rewrite (in_permut_in P2); right; trivial. intros; apply T. right; trivial. rewrite (in_permut_in P2); right; trivial. rewrite equiv_eval_equation; rewrite Sf; rewrite H'. case (mem_bool eq_tt_bool (Term f l1, Term g l2) (equiv_l rpo_infos)); [reflexivity | idtac]. case_eq (prec_eq_bool Prec f g). intro; trivial. intro f_eq'_g. assert (H1:= prec_eq_bool_ok). assert (H1':= H1 symbol Prec f g). rewrite f_eq'_g in H1'. contradict H1'; 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)