proposition: Theorem rpo_mult_eval_rpo_mul_greater: forall rpo_infos n A B, (forall t t' :term, mem equiv t B -> mem equiv t' A -> size t + size t' <= n) -> rpo_mult_eval rpo_infos n A B = Some Greater_than -> rpo_mul rpo_infos.(bb) B A.
proof: Proof. intros rpo_infos n A B H1 H. unfold rpo_mult_eval in H. assert (H':= remove_equiv_eval_list_is_sound). case_eq (remove_equiv_eval_list (equiv_eval rpo_infos n) A B). intros p H3. rewrite H3 in H. destruct p. destruct l. destruct l0. discriminate. discriminate. destruct l0. assert (H2':= H' (equiv_eval rpo_infos n) A B); clear H' H. rewrite H3 in H2'. destruct H2' as (l', (H01, (H02, (H03, H4)))). apply (@List_mul _ t l nil (map (fun st : term * term => snd st) l')). apply permut0_eq_equiv. assumption. apply permut0_trans with (t :: l ++ map (fun st : term * term => fst st) l'). apply equiv_equiv. apply permut0_eq_equiv. assumption. assert (H2':= equiv_eval_lists (t::l) l' n rpo_infos H01). trivial. intros b H'. contradict H'. assert (H3':= H' (equiv_eval rpo_infos n) A B); clear H'. rewrite H3 in H3'. destruct H3' as (ll, (H01, (H02, (H03, H4)))). apply (@List_mul _ t l (t0 :: l0) ( map (fun st : term * term => snd st) ll)). apply permut0_eq_equiv. assumption. assert (H2':= equiv_eval_lists (t::l) ll n rpo_infos H01). apply permut0_trans with ((t :: l) ++ map (fun st : term * term => fst st) ll). apply equiv_equiv. apply permut0_eq_equiv. auto. auto. intros b H'. assert (H1':= mult_eval_is_sound_weak_equiv). assert (H1'':= H1' rpo_infos n (t :: l) (t0 :: l0)); clear H1'. assert (H6: (forall t1 t' : term, mem equiv t' (t :: l) -> mem equiv t1 (t0 :: l0) -> size t1 + size t' <= n)). intros t1 t2 H1' H2. clear H1''. apply H1. apply permut0_mem with (t0 :: l0) (map (fun st : term * term => snd st) ll). assumption. assumption. apply permut0_mem with (t :: l) (map (fun st : term * term => fst st) ll). assumption. assumption. assert (H1': match mult_eval (rpo_eval rpo_infos n) (t :: l) (t0 :: l0) with | Some Equivalent => False | Some Less_than => forall t1 : term, mem equiv t1 (t :: l) -> exists t2 : term, mem equiv t2 (t0 :: l0) /\ (size t2 + size t1 <= n -> rpo_eval rpo_infos n t2 t1 = Some Greater_than) | Some Greater_than => forall t2 : term, mem equiv t2 (t0 :: l0) -> exists t1 : term, mem equiv t1 (t :: l) /\ (size t1 + size t2 <= n -> rpo_eval rpo_infos n t1 t2 = Some Greater_than) | Some Uncomparable => True | None => True end). apply H1''. assert (forall t1 t' : term, mem equiv t' (t :: l) -> mem equiv t1 (t0 :: l0) -> size t' + size t1 <= n). intros t2 t'. assert (mem equiv t' (t :: l) -> mem equiv t2 (t0 :: l0) -> size t' + size t2 <= n). intros H1' H2. assert (H6':= H6 t' t2). assert (H0: size t2 + size t' <= n). auto. lia. assumption. intros. apply H0; trivial. clear H1''. rewrite H in H1'. assert (H1'':= H1' b); clear H1'. assert ( exists t1 : term, mem equiv t1 (t :: l) /\ (size t1 + size b <= n -> rpo_eval rpo_infos n t1 b = Some Greater_than)). apply H1''; trivial. clear H1''. destruct H0. destruct H0. exists x. split. trivial. assert (rpo_eval rpo_infos n x b = Some Greater_than). apply H2. assert (H6':= H6 b x). assert (size b + size x <= n). apply H6'. trivial. trivial. lia. assert (H6'':= rpo_eval_is_complete). assert (H6':= H6'' rpo_infos n x b); clear H6''. rewrite H2 in H6'. apply H6'. assert (H6'':= H6 b x). assert (size b + size x <= n). apply H6''. trivial. trivial. lia. assert (H6'':= H6 b x). assert (size b + size x <= n). apply H6''. trivial. trivial. lia. intro. rewrite H0 in H. assert (H'':= H' (equiv_eval rpo_infos n) A B); clear H'. rewrite H0 in H''. destruct H0. destruct H'' as (t1, (t2, (In_t1_A, (In_t2_B, H4)))). assert (H2:= mult_eval_is_sound_weak_equiv). assert (H2':= H2 rpo_infos n A B); clear H2. rewrite H in H2'. assert ( forall t2 : term, mem equiv t2 B -> exists t1 : term, mem equiv t1 A /\ (size t1 + size t2 <= n -> rpo_eval rpo_infos n t1 t2 = Some Greater_than)). apply H2';trivial. intros. assert (size t' + size t <= n). apply H1. trivial. trivial. lia. clear H2'. destruct A. unfold In in In_t1_A. contradict In_t1_A. apply (@List_mul _ t A B [] (t::A) B). rewrite <- app_nil_end. apply permut_refl. intros. reflexivity. rewrite <- app_nil_end. apply permut_refl. intros. reflexivity. intros. assert (H0':= H0 b); clear H0. assert (exists t1 : term, mem equiv t1 (t :: A) /\ (size t1 + size b <= n -> rpo_eval rpo_infos n t1 b = Some Greater_than)). apply H0'; trivial. destruct H0. exists x. split. destruct H0. trivial. destruct H0. assert (H1':= H1 b x). assert (size b + size x <= n). apply H1'; trivial. assert (size x + size b <= n). lia. assert (rpo_eval rpo_infos n x b = Some Greater_than). apply H3; trivial. assert (H8:= rpo_eval_is_sound_weak rpo_infos n x b ). rewrite H7 in H8. 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)