proposition: Lemma mult_eval_is_sound_weak_equiv : forall rpo_infos n l1 l2, (forall t t' :term, mem equiv t l1 -> mem equiv t' l2 -> size t + size t' <= n) -> match mult_eval (rpo_eval rpo_infos n) l1 l2 with | Some Equivalent => False | Some Less_than => forall t1, mem equiv t1 l1 -> exists t2, mem equiv t2 l2 /\ (size t2 + size t1 <= n -> rpo_eval rpo_infos n t2 t1 = Some Greater_than) | Some Greater_than => forall t2, mem equiv t2 l2 -> exists t1, mem equiv t1 l1 /\ (size t1 + size t2 <= n -> rpo_eval rpo_infos n t1 t2 = Some Greater_than) | _ => True end.
proof: Proof. intros rpo_infos n l1 l2 H; unfold mult_eval. assert (forall t t' : term, mem equiv t l2 -> mem equiv t' l1 -> size t + size t' <= n). intros t t'. assert (mem equiv t' l1 -> mem equiv t l2 -> size t' + size t <= n). apply H. intros H1' H2. assert (size t' + size t <= n). auto. lia. generalize (list_gt_list_is_sound_mem_equiv rpo_infos l1 l2 H0). destruct (list_gt_list (rpo_eval rpo_infos n) l1 l2) as [[ | ] | ]. trivial. intros H' t2 H1. assert (H2':= H' t2); clear H'. assert (H3: exists g : term, mem equiv g l1 /\ rpo_eval rpo_infos n g t2 = Some Greater_than). auto. destruct H3. exists x. assert (H': size x + size t2 <= n). apply H. apply H2. assumption. split. apply H2. intro; apply H2. intros. generalize (list_gt_list_is_sound_mem_equiv rpo_infos l2 l1 H). destruct (list_gt_list (rpo_eval rpo_infos n) l2 l1) as [[ | ] | ]. intros H' t2 H1'. assert (H2':= H' t2); clear H'. assert (H3: exists g : term, mem equiv g l2 /\ rpo_eval rpo_infos n g t2 = Some Greater_than). auto. destruct H3. exists x. assert (H': size x + size t2 <= n). apply H0. apply H2. assumption. split. apply H2. intro; apply H2. trivial. 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)