proposition: Theorem rpo_mult_eval_rpo_mul_less: 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 Less_than -> rpo_mul rpo_infos.(bb) A B.
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. 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 l0 nil (map (fun st : term * term => fst st) l)). apply permut0_eq_equiv. assumption. apply permut0_trans with (t :: l0 ++ map (fun st : term * term => snd st) l). apply equiv_equiv. apply permut0_eq_equiv. assumption. assert (H2':= equiv_eval_lists (t::l0) l n rpo_infos H01). apply permut0_sym. apply equiv_equiv. auto. intros b H'. contradict H'. destruct l0. discriminate. 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 _ t0 l0 (t :: l) ( map (fun st : term * term => fst st) ll)). apply permut0_eq_equiv. assumption. assert (H2':= equiv_eval_lists (t0::l0) ll n rpo_infos H01). apply permut0_trans with ((t0 :: l0) ++ map (fun st : term * term => snd st) ll). apply equiv_equiv. apply permut0_eq_equiv. auto. apply permut0_sym. apply equiv_equiv. 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 t2 t'). assert (size t2 + size t' <= n). auto. lia. 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''. intros t1' t2'. assert (H6':= H6 t2' t1'). intros. assert (size t2' + size t1' <= n). auto. lia. intros. apply H0. assumption. assumption. intros. apply H0. assumption. assumption. clear H1''; rewrite H in H1' . assert (H11 := H1' b). clear H1'. assert (H11': exists t2 : term, mem equiv t2 (t0 :: l0) /\ rpo_eval rpo_infos n t2 b = Some Greater_than). assert (exists t2 : term, size t2 + size b <= n -> mem equiv t2 (t0 :: l0) /\ rpo_eval rpo_infos n t2 b = Some Greater_than). auto. assert (H11': exists t2 : term, mem equiv t2 (t0 :: l0) /\ (size t2 + size b <= n -> rpo_eval rpo_infos n t2 b = Some Greater_than)). apply H11. assumption. clear H11. destruct H11'. exists x. tauto. assert (H11': exists t2 : term, mem equiv t2 (t0 :: l0) /\ (size t2 + size b <= n -> rpo_eval rpo_infos n t2 b = Some Greater_than)). apply H11. assumption. clear H11. destruct H11'. exists x. split. apply H2. destruct H2. apply H5. apply H6. assumption. assumption. destruct H11'. exists x. split. apply H0. destruct H0. assert (H6'':= rpo_eval_is_complete). assert (H6':= H6'' rpo_infos n x b); clear H6''. rewrite H2 in H6'. apply H6'. apply H6. assumption. assumption. 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 t1 : term, mem equiv t1 A -> exists t2 : term, mem equiv t2 B /\ (size t2 + size t1 <= n -> rpo_eval rpo_infos n t2 t1 = Some Greater_than)). apply H2';trivial. intros. assert (size t' + size t <= n). apply H1. trivial. trivial. lia. clear H2'. destruct B. unfold In in In_t2_B. contradict In_t2_B. apply (@List_mul _ t B A [] (t::B) A). 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 t2 : term, mem equiv t2 (t :: B) /\ (size t2 + size b <= n -> rpo_eval rpo_infos n t2 b = Some Greater_than)). apply H0'; trivial. destruct H0. exists x. split. destruct H0. trivial. destruct H0. assert (H1':= H1 x b). assert (size x + size b <= n). apply H1'; trivial. assert (rpo_eval rpo_infos n x b = Some Greater_than). apply H3; trivial. assert (H7:= rpo_eval_is_sound_weak rpo_infos n x b ). rewrite H6 in H7. 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)