proposition: Lemma rpo_eval_terminates : forall rpo_infos n t1 t2, size t1 + size t2 <= n -> rpo_eval rpo_infos n t1 t2 <> None.
proof: Proof. intros rpo_infos n; induction n as [ | n]. intros t1 t2 St1; 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]. intros t1 t2 St; rewrite rpo_eval_equation. case (mem_bool eq_tt_bool (t1, t2) (rpo_l rpo_infos)). intro;discriminate. case (mem_bool eq_tt_bool (t2, t1) (rpo_l rpo_infos)). intro;discriminate. case (mem_bool eq_tt_bool (t1, t2) (equiv_l rpo_infos)). intro;discriminate. case (mem_bool eq_tt_bool (t2, t1) (equiv_l rpo_infos)). intro;discriminate. assert (T := @equiv_eval_terminates rpo_infos (S n) t1 t2 St); destruct (equiv_eval rpo_infos (S n) t1 t2) as [ [ | ] | ]; try discriminate. destruct t1 as [v1 | f1 l1]; destruct t2 as [v2 | f2 l2]. discriminate. destruct (var_in_term_list v1 l2); discriminate. destruct (var_in_term_list v2 l1); discriminate. 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 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 end) l1) as [ [ | ] | ]. intros _; simpl; discriminate. 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 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 end) l2) as [ [ | ] | ]. intros _; simpl; discriminate. intros _; simpl; destruct (prec_eval f1 f2); try discriminate. destruct (status Prec f1). case (Nat.eqb (length l1) (length l2) || leb (length l1) (bb rpo_infos) && leb (length l2) (bb rpo_infos)). apply lexico_eval_fully_evaluates. intros t1 t1_in_l1; apply IHn. 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. apply Nat.add_le_mono_r; apply size_direct_subterm; trivial. intros t2 t2_in_l2; apply IHn. apply le_S_n; refine (Nat.le_trans _ _ _ _ St); rewrite Nat.add_comm; replace (S (size t2 + size (Term f1 l1))) with (S (size t2) + size (Term f1 l1)); trivial; rewrite Nat.add_comm; apply Nat.add_le_mono_l; apply size_direct_subterm; trivial. intros t1 t2 t1_in_l1 t2_in_l2; apply IHn. 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. apply size_direct_subterm; trivial. apply Nat.lt_le_incl; apply size_direct_subterm; trivial. discriminate. generalize (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 [ [[ | t1' l1'] [ | t2' l2']] | ]. intros _; discriminate. intros _; discriminate. intros _; discriminate. intros [ll [H [P1 [P2 H']]]]. apply mult_eval_fully_evaluates. intros t1 t2 t1_in_l1' t2_in_l2'; apply IHn. 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. apply size_direct_subterm; simpl; rewrite (in_permut_in P1); apply in_or_app; left; trivial. apply Nat.lt_le_incl; apply size_direct_subterm; simpl; rewrite (in_permut_in P2); apply in_or_app; left; trivial. intros t1 t2 t1_in_l1' t2_in_l2'; apply IHn. apply le_S_n; refine (Nat.le_trans _ _ _ _ St); replace (S (size t2 + size t1)) with (S (size t2) + size t1); trivial. rewrite Nat.add_comm; apply Nat.add_le_mono. apply Nat.lt_le_incl; apply size_direct_subterm; simpl; rewrite (in_permut_in P1); apply in_or_app; left; trivial. apply size_direct_subterm; simpl; rewrite (in_permut_in P2); apply in_or_app; left; trivial. intros [t1 [t2 [t1_in_l1 [t2_in_l2 H]]]]; assert (H' := @equiv_eval_terminates rpo_infos n t1 t2); destruct (equiv_eval rpo_infos n t1 t2) as [ [ | ] | ]. discriminate. discriminate. intros _; apply H'; trivial. 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. apply size_direct_subterm; trivial. apply Nat.lt_le_incl; apply size_direct_subterm; trivial. 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 _; discriminate. intros _; discriminate. intros [u1 [u1_in_l1 H]]; assert (H' := IHn u1 (Term f2 l2)); destruct (rpo_eval rpo_infos n u1 (Term f2 l2)) as [ [ | | | ] | ]. discriminate. discriminate. discriminate. discriminate. apply H'. apply le_S_n; refine (Nat.le_trans _ _ _ _ St); replace (S (size u1 + size (Term f2 l2))) with (S (size u1) + size (Term f2 l2)); trivial; apply Nat.add_le_mono_r; apply size_direct_subterm; trivial. 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 _; discriminate. intros _; discriminate. intros [u2 [u2_in_l2 H]]; assert (H' := IHn (Term f1 l1) u2); destruct (rpo_eval rpo_infos n (Term f1 l1) u2) as [ [ | | | ] | ]. discriminate. discriminate. discriminate. discriminate. apply H'. apply le_S_n; refine (Nat.le_trans _ _ _ _ St); rewrite Nat.add_comm; replace (S (size u2 + size (Term f1 l1))) with (S (size u2) + size (Term f1 l1)); trivial; rewrite Nat.add_comm; apply Nat.add_le_mono_l; apply size_direct_subterm; trivial. intros [[u2 [u2_in_l2 H]] _]; assert (H' := IHn (Term f1 l1) u2); destruct (rpo_eval rpo_infos n (Term f1 l1) u2) as [ [ | | | ] | ]. discriminate. discriminate. discriminate. discriminate. apply H'. apply le_S_n; refine (Nat.le_trans _ _ _ _ St); rewrite Nat.add_comm; replace (S (size u2 + size (Term f1 l1))) with (S (size u2) + size (Term f1 l1)); trivial; rewrite Nat.add_comm; apply Nat.add_le_mono_l; apply size_direct_subterm; trivial. intros [[u1 [u1_in_l1 H]] _]; assert (H' := IHn u1 (Term f2 l2)); destruct (rpo_eval rpo_infos n u1 (Term f2 l2)) as [ [ | | | ] | ]. discriminate. discriminate. discriminate. discriminate. apply H'. apply le_S_n; refine (Nat.le_trans _ _ _ _ St); replace (S (size u1 + size (Term f2 l2))) with (S (size u1) + size (Term f2 l2)); trivial; apply Nat.add_le_mono_r; apply size_direct_subterm; trivial. intros _; apply T; 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)