proposition: Lemma lexico_eval_fully_evaluates : forall p s1 s2 l1 l2, (forall t1, In t1 l1 -> p s2 t1 <> None) -> (forall t2, In t2 l2 -> p s1 t2 <> None) -> (forall t1 t2, In t1 l1 -> In t2 l2 -> p t1 t2 <> None) -> lexico_eval p s1 s2 l1 l2 <> None.
proof: Proof. intros p s1 s2 l1; induction l1 as [ | t1 l1]; intros [ | t2 l2] Es2 Es1 E; simpl; try discriminate. assert (H := E t1 t2 (or_introl _ (eq_refl _)) (or_introl _ (eq_refl _))); destruct (p t1 t2) as [ [ | | | ] | ]. apply IHl1; intros; [apply Es2 | apply Es1 | apply E]; right; trivial. unfold term_gt_list; simpl. generalize (list_forall_option_is_sound (fun t : term => match p s2 t with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) l1); destruct (list_forall_option (fun t : term => match p s2 t with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) l1) as [ [ | ] | ]. clear H; assert (H := Es2 t1 (or_introl _ (eq_refl _))). destruct (p s2 t1) as [ [ | | | ] | ]. intros _; discriminate. intros _; discriminate. intros _; discriminate. intros _; discriminate. intros _; apply H; trivial. clear H; assert (H := Es2 t1 (or_introl _ (eq_refl _))). destruct (p s2 t1) as [ [ | | | ] | ]. intros _; discriminate. intros _; discriminate. intros _; discriminate. intros _; discriminate. intros _; apply H; trivial. intros [u1 [u1_in_l1 pt1s2_eq_none]]. assert (H' := Es2 _ (or_intror _ u1_in_l1)). destruct (p s2 u1) as [ [ | | | ] | ]; trivial. discriminate. discriminate. discriminate. discriminate. absurd (@None comp = None); trivial. unfold term_gt_list; simpl. generalize (list_forall_option_is_sound (fun t : term => match p s1 t with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) l2); destruct (list_forall_option (fun t : term => match p s1 t with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) l2) as [ [ | ] | ]. clear H; assert (H := Es1 t2 (or_introl _ (eq_refl _))). destruct (p s1 t2) as [ [ | | | ] | ]. intros _; discriminate. intros _; discriminate. intros _; discriminate. intros _; discriminate. intros _; apply H; trivial. clear H; assert (H := Es1 t2 (or_introl _ (eq_refl _))). destruct (p s1 t2) as [ [ | | | ] | ]. intros _; discriminate. intros _; discriminate. intros _; discriminate. intros _; discriminate. intros _; apply H; trivial. intros [u2 [u2_in_l2 ps1u2_eq_none]]. assert (H' := Es1 _ (or_intror _ u2_in_l2)). destruct (p s1 u2) as [ [ | | | ] | ]; trivial. discriminate. discriminate. discriminate. discriminate. absurd (@None comp = None); trivial. discriminate. 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)