proposition: Lemma prec_eval_is_sound : forall f1 f2, match prec_eval f1 f2 with | Equivalent => prec_eq Prec f1 f2 | Less_than => prec Prec f1 f2 | Greater_than => prec Prec f2 f1 | Uncomparable => ~ prec_eq Prec f1 f2 /\ ~prec Prec f1 f2 /\ ~prec Prec f2 f1 end.
proof: Proof. intros f1 f2; unfold prec_eval. case_eq (prec_eq_bool Prec f1 f2). intros. assert (H1:= prec_eq_bool_ok). assert (H1':= H1 symbol Prec f1 f2). rewrite H in H1'. trivial. intro. case_eq (prec_bool Prec f1 f2). intros. assert (H1:= prec_bool_ok). assert (H1':= H1 symbol Prec f1 f2). rewrite H0 in H1'. trivial. intros. case_eq (prec_bool Prec f2 f1). intro prec'. assert (H1:= prec_bool_ok). assert (H1':= H1 symbol Prec f2 f1). rewrite prec' in H1'. trivial. intros. split. assert (H3:= prec_eq_bool_ok). assert (H3':= H3 symbol Prec f1 f2). rewrite H in H3'. trivial. split. assert (H3:= prec_bool_ok). assert (H3':= H3 symbol Prec f1 f2). rewrite H0 in H3'. trivial. assert (H3:= prec_bool_ok). assert (H3':= H3 symbol Prec f2 f1). rewrite H1 in H3'. 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)