proposition: Lemma mult_eval_fully_evaluates : forall p l1 l2, (forall t1 t2, In t1 l1 -> In t2 l2 -> p t1 t2 <> None) -> (forall t1 t2, In t1 l1 -> In t2 l2 -> p t2 t1 <> None) -> mult_eval p l1 l2 <> None.
proof: Proof. intros p [ | t1 l1] l2 E E'; unfold mult_eval, list_gt_list. simpl; clear E; induction l2 as [ | t2 l2]; simpl. discriminate. destruct (list_forall_option (fun _ : term => Some false) l2) as [ [ | ] | ]. discriminate. discriminate. apply IHl2; intros; contradiction. generalize (list_forall_option_is_sound (fun s : term => list_exists_option (fun g : term => match p g s with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) (t1 :: l1)) l2); destruct (list_forall_option (fun s : term => list_exists_option (fun g : term => match p g s with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) (t1 :: l1)) l2) as [ [ | ] | ]. intros _; discriminate. intros _; generalize (list_forall_option_is_sound (fun s : term => list_exists_option (fun g : term => match p g s with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) l2) (t1 :: l1)); destruct (list_forall_option (fun s : term => list_exists_option (fun g : term => match p g s with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) l2) (t1 :: l1)) as [ [ | ] | ]. intros _; discriminate. intros _; discriminate. intros [u1 [u1_in_l1 H]]. assert (H' := list_exists_option_is_sound (fun g : term => match p g u1 with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) l2); rewrite H in H'. destruct H' as [ [u2 [u2_in_l2 pu1u2_eq_none]] _]. assert (H' := E' u1 u2 u1_in_l1 u2_in_l2); destruct (p u2 u1) as [ [ | | | ] | ]; trivial; discriminate. intros [u2 [u2_in_l2 H]]. assert (H' := list_exists_option_is_sound (fun g : term => match p g u2 with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) (t1 :: l1)); rewrite H in H'. destruct H' as [ [u1 [u1_in_l1 pu1u2_eq_none]] _]. assert (H' := E u1 u2 u1_in_l1 u2_in_l2); destruct (p u1 u2) as [ [ | | | ] | ]; trivial; discriminate. 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)