proposition: Lemma list_gt_list_is_sound_false : forall p lg ls, list_gt_list p lg ls = Some false -> exists s, In s ls /\ forall g, In g lg -> (p g s = Some Less_than \/ p g s = Some Equivalent \/ p g s = Some Uncomparable).
proof: Proof. intros p lg ls; revert lg; induction ls as [ | s ls]; intro lg. unfold list_gt_list; simpl. intros. compute in H. discriminate. unfold list_gt_list; simpl. generalize (list_exists_option_is_sound (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) lg). destruct (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) lg) as [[ | ] | ]. intros [g [g_in_ls H]]. generalize (IHls lg); unfold list_gt_list; destruct (list_forall_option (fun s0 : term => list_exists_option (fun g0 : term => match p g0 s0 with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) lg) ls) as [[ | ] | ]. intros. discriminate. intros. destruct (p g s) as [[ | | | ] | ]. discriminate. discriminate. assert (exists s : term, In s ls /\ (forall g : term, In g lg -> (p g s = Some Less_than \/ p g s = Some Equivalent \/ p g s = Some Uncomparable))). apply H0; trivial. destruct H2. exists x. destruct H2. split. right. trivial. assumption. discriminate. discriminate. intros. discriminate. destruct (list_forall_option (fun s0 : term => list_exists_option (fun g0 : term => match p g0 s0 with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) lg) ls) as [[ | ] | ]. intros. exists s. split. left; trivial. intros. assert (H':= H g). assert (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 = Some false). apply H'; trivial. case_eq (p g s). destruct c. intros. rewrite H3 in H2. right. left; trivial. intros. rewrite H3 in H2. left; trivial. intros. rewrite H3 in H2. discriminate. intros. rewrite H3 in H2. right. right. trivial. intros. rewrite H3 in H2. discriminate. intros. exists s. split. left; trivial. intros. assert (H':= H g). assert (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 = Some false). apply H'; trivial. case_eq (p g s). destruct c. intros. rewrite H3 in H2. right. left; trivial. intros. rewrite H3 in H2. left; trivial. intros. rewrite H3 in H2. discriminate. intros. rewrite H3 in H2. right. right. trivial. intros. rewrite H3 in H2. discriminate. intros. discriminate. intros. 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)