proposition: Lemma list_gt_list_is_sound_mem_equiv : forall rpo_infos n lg ls, (forall t t' :term, mem equiv t ls -> mem equiv t' lg -> size t + size t' <= n) -> match list_gt_list (rpo_eval rpo_infos n) lg ls with | Some true => forall s, mem equiv s ls -> exists g, mem equiv g lg /\ rpo_eval rpo_infos n g s = Some Greater_than | _ => True end.
proof: Proof. intros rpo_infos n lg ls H0. assert (forall t t' : term, mem equiv t ls -> mem equiv t' lg -> size t' + size t <= n). intros. assert (H0':= H0 t t'). assert (size t + size t' <= n). tauto. lia. induction ls as [ | s ls]. simpl; intros; contradiction. unfold list_gt_list; simpl. assert (match list_gt_list (rpo_eval rpo_infos n) lg ls with | Some true => forall s : term, mem equiv s ls -> exists g : term, mem equiv g lg /\ rpo_eval rpo_infos n g s = Some Greater_than | Some false => True | None => True end). apply IHls. intros t t' H'. apply H0. simpl. tauto. clear IHls. intros. apply H. simpl. right. trivial. simpl. trivial. clear IHls. generalize (list_exists_option_is_sound ( fun g : term => match rpo_eval rpo_infos n g s with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) lg). destruct (list_exists_option (fun g : term => match rpo_eval rpo_infos n g s with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) lg) as [[ | ] | ]. intros [g [g_in_ls H']]. generalize H1. unfold list_gt_list. destruct ( list_forall_option (fun s0 : term => list_exists_option (fun g0 : term => match rpo_eval rpo_infos n g0 s0 with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) lg) ls) as [[ | ] | ]. intros H0' u [s_eq_u | u_in_ls]. exists g; split. apply in_mem. assumption. assert (H1':= in_mem g lg). assert (H2': mem equiv g lg). auto. assert (H3':= equiv_rpo_eval). assert (H3:= H3' n rpo_infos g s u); clear H3'. assert (H4':= H0' s). assert (H5: rpo_eval rpo_infos n g u = rpo_eval rpo_infos n g s). assert (H6:= equiv_same_size). assert (H6':= H6 u s); clear H6. assert (size u = size s). auto. apply H3. apply H. simpl. tauto. assumption. apply H. simpl. left. reflexivity. assumption. assumption. rewrite H5. generalize H'. destruct (rpo_eval rpo_infos n g s) as [[ | | | ] | ]; intros. discriminate. discriminate. trivial. discriminate. discriminate. assert (H10':= H0' u); clear H0'. assert (H0': exists g : term, mem equiv g lg /\ rpo_eval rpo_infos n g u = Some Greater_than). apply H10'. trivial. trivial. trivial. trivial. intros _; destruct (list_forall_option (fun s0 : term => list_exists_option (fun g0 : term => match rpo_eval rpo_infos n g0 s0 with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) lg) ls) as [[ | ] | ]; 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)