proposition: Lemma equiv_rpo_eval: forall n rpo_infos t s u, size t + size u <= n -> size t + size s <= n -> equiv u s -> rpo_eval rpo_infos n t u = rpo_eval rpo_infos n t s.
proof: Proof. intros n rpo_infos t s u tu ts H. assert (H1:= equiv_rpo_equiv_1). assert (H2:= rpo_eval_is_complete_less_greater). assert (H3:= rpo_eval_is_complete). assert (H2':= H2 rpo_infos n t u). assert (H2'':= H2 rpo_infos n t s); clear H2. assert (H3':= H3 rpo_infos n t u). assert (H3'':= H3 rpo_infos n t s); clear H3. assert (H31: match rpo_eval rpo_infos n t s with | Some Equivalent => equiv t s | Some Less_than => rpo (bb rpo_infos) t s | Some Greater_than => rpo (bb rpo_infos) s t | Some Uncomparable => ~ equiv t s /\ ~ rpo (bb rpo_infos) t s /\ ~ rpo (bb rpo_infos) s t | None => False end). apply H3''; trivial. assert (H32: match rpo_eval rpo_infos n t u with | Some Equivalent => equiv t u | Some Less_than => rpo (bb rpo_infos) t u | Some Greater_than => rpo (bb rpo_infos) u t | Some Uncomparable => ~ equiv t u /\ ~ rpo (bb rpo_infos) t u /\ ~ rpo (bb rpo_infos) u t | None => False end). apply H3'; trivial. clear H3'' H3'. destruct (rpo_eval rpo_infos n t u) as [[ | | | ] | ]. destruct (rpo_eval rpo_infos n t s) as [[ | | | ] | ]. trivial. assert (H':= @Equivalence_Transitive _ _ equiv_equiv t u s). assert (H1': equiv t s). auto. assert (H2: rpo_eval rpo_infos n s t = Some Greater_than). tauto. assert (H3:= rpo_eval_is_complete_equivalent). assert (H3':= H3 rpo_infos n s t). assert (H4': size s + size t <=n). lia. assert (H4: rpo_eval rpo_infos n s t = Some Equivalent). rewrite H2 in H3'. assert (H5':= @Equivalence_Symmetric _ _ equiv_equiv t s). assert (H5: equiv s t). apply H5'; assumption. auto. rewrite H2 in H4. discriminate. assert (H':= @Equivalence_Transitive _ _ equiv_equiv t u s). assert (H1': equiv t s). auto. clear H2' H2''. assert (H4: rpo_eval rpo_infos n s t = Some Less_than). assert (H3:= rpo_eval_is_complete_less_greater). assert (H6:= H3 rpo_infos n s t). apply H6. lia. assumption. assert (H3:= rpo_eval_is_complete_equivalent). assert (H3':= H3 rpo_infos n s t). assert (H5':= @Equivalence_Symmetric _ _ equiv_equiv t s). assert (H6: equiv s t). auto. assert (H4': size s + size t <=n). lia. rewrite H4 in H3'. assert (Some Less_than = Some Equivalent). auto. discriminate. clear H2' H2''. destruct H31. assert (H':= @Equivalence_Transitive _ _ equiv_equiv t u s). tauto. contradict H31. destruct (rpo_eval rpo_infos n t s) as [[ | | | ] | ]. trivial. assert (H5':= @Equivalence_Symmetric _ _ equiv_equiv u s). assert (H5'': equiv s u). auto. assert (H':= @Equivalence_Transitive _ _ equiv_equiv t s u). assert (H1': equiv t u). auto. assert (H2: rpo_eval rpo_infos n u t = Some Greater_than). tauto. assert (H3:= rpo_eval_is_complete_equivalent). assert (H3':= H3 rpo_infos n u t). assert (H4': size u + size t <=n). lia. assert (H4: rpo_eval rpo_infos n u t = Some Equivalent). rewrite H2 in H3'. assert (H6':= @Equivalence_Symmetric _ _ equiv_equiv t u). assert (H5: equiv u t). apply H6'; assumption. auto. rewrite H2 in H4. discriminate. trivial. rewrite (equiv_rpo_equiv_1 _ H) in H32. assert (H2:= rpo_eval_is_complete_less_greater); clear H2' H2''. assert (H2':= H2 rpo_infos n t s). assert (H2'':= H2 rpo_infos n s t). assert (H4': size s + size t <=n). lia. assert (H5: rpo_eval rpo_infos n t s = Some Less_than). tauto. assert (H5': rpo_eval rpo_infos n t s = Some Greater_than). tauto. rewrite H5 in H5'; discriminate. destruct H31 as (H41, (H42, H43)). rewrite (equiv_rpo_equiv_1 _ H) in H32. contradiction. contradiction. destruct (rpo_eval rpo_infos n t s) as [[ | | | ] | ]. trivial. assert (H5':= @Equivalence_Symmetric _ _ equiv_equiv t s). assert (H5'': equiv s t). auto. assert (H':= @Equivalence_Transitive _ _ equiv_equiv u s t). assert (H1': equiv u t). auto. assert (H3:= rpo_eval_is_complete_equivalent). assert (H3':= H3 rpo_infos n u t). assert (H4': size u + size t <=n). lia. assert (H4: rpo_eval rpo_infos n u t = Some Equivalent). auto. assert (H2:= rpo_eval_is_complete_less_greater); clear H2' H2''. assert (H2':= H2 rpo_infos n u t). assert (rpo_eval rpo_infos n u t = Some Less_than). tauto. rewrite H0 in H4. discriminate. rewrite <- (equiv_rpo_equiv_1 _ H) in H31. assert (H2:= rpo_eval_is_complete_less_greater); clear H2' H2''. assert (H2':= H2 rpo_infos n t u). assert (H2'':= H2 rpo_infos n u t). assert (H4': size u + size t <=n). lia. assert (H5: rpo_eval rpo_infos n t u = Some Less_than). tauto. assert (H5': rpo_eval rpo_infos n t u = Some Greater_than). tauto. rewrite H5 in H5'; discriminate. trivial. destruct H31 as (H41, (H42, H43)). rewrite -> (equiv_rpo_equiv_2 _ H) in H32. contradiction. contradiction. destruct (rpo_eval rpo_infos n t s) as [[ | | | ] | ]. trivial. destruct H32 as (H41, (H42, H43)). assert (H5':= @Equivalence_Symmetric _ _ equiv_equiv u s). assert (H5'': equiv s u). auto. assert (H':= @Equivalence_Transitive _ _ equiv_equiv t s u). tauto. destruct H32 as (H41, (H42, H43)). rewrite <- (equiv_rpo_equiv_1 _ H) in H31. contradiction. destruct H32 as (H41, (H42, H43)). rewrite <- (equiv_rpo_equiv_2 _ H) in H31. contradiction. trivial. contradiction. destruct (rpo_eval rpo_infos n t s) as [[ | | | ] | ]; contradiction. 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)