proposition: Lemma lexico_eval_is_sound : forall (p : term -> term -> option comp) s1 s2 l1 l2, match lexico_eval p s1 s2 l1 l2 with | Some Equivalent => (exists ll, (forall t1 t2, In (t1,t2) ll -> p t1 t2 = Some Equivalent) /\ l1 = map (fun st => fst st) ll /\ l2 = map (fun st => snd st) ll) | Some Less_than => (l1 = nil /\ l2 <> nil) \/ (exists ll, exists t2, exists l2', (forall t1 t2, In (t1,t2) ll -> p t1 t2 = Some Equivalent) /\ l1 = map (fun st => fst st) ll /\ l2 = map (fun st => snd st) ll ++ t2 :: l2') \/ (exists ll, exists t1, exists t2, exists l1', exists l2', (forall t1 t2, In (t1,t2) ll -> p t1 t2 = Some Equivalent) /\ p t1 t2 = Some Less_than /\ (forall t1, In t1 l1 -> ((exists t2, In t2 l2 /\ (p t1 t2 = Some Equivalent \/ p t1 t2 = Some Less_than)) \/ p s2 t1 = Some Greater_than)) /\ l1 = map (fun st => fst st) ll ++ t1 :: l1' /\ l2 = map (fun st => snd st) ll ++ t2 :: l2') | Some Greater_than => (l1 <> nil /\ l2 = nil) \/ (exists ll, exists t1, exists l1', (forall t1 t2, In (t1,t2) ll -> p t1 t2 = Some Equivalent) /\ l1 = map (fun st => fst st) ll ++ t1 :: l1' /\ l2 = map (fun st => snd st) ll) \/ (exists ll, exists t1, exists t2, exists l1', exists l2', (forall t1 t2, In (t1,t2) ll -> p t1 t2 = Some Equivalent) /\ p t1 t2 = Some Greater_than /\ (forall t2, In t2 l2 -> ((exists t1, In t1 l1 /\ (p t1 t2 = Some Equivalent \/ p t1 t2 = Some Greater_than)) \/ p s1 t2 = Some Greater_than)) /\ l1 = map (fun st => fst st) ll ++ t1 :: l1' /\ l2 = map (fun st => snd st) ll ++ t2 :: l2') | _ => True end.
proof: Proof. intros p s1 s2 l1; induction l1 as [ | t1 l1]; intros [ | t2 l2]. simpl; exists (@nil (term * term)); simpl; intuition. simpl; left; split; [apply eq_refl | discriminate]. simpl; left; split; [discriminate | apply eq_refl]. simpl; case_eq (p t1 t2); [idtac | trivial]. intros [ | | | ] Ht; generalize (IHl1 l2). case_eq (lexico_eval p s1 s2 l1 l2); [intros [ | | | ] Hl | trivial]. intros [ll [Hll [H1 H2]]]; exists ((t1,t2) :: ll); split. simpl; intros u1 u2 [u1u2_eq_t1t2 | u1u2_in_ll]; [injection u1u2_eq_t1t2; intros; subst | apply Hll]; assumption. simpl; split; subst; apply eq_refl. intros [[H1 H2] | [[ll [a2 [l2' [Hll [H1 H2]]]]] | [ll [a1 [a2 [l1' [l2' [Hll [Ha [H [H1 H2]]]]]]]]]]]. right; left; subst; destruct l2 as [ | a2 l2]. discriminate. exists ((t1,t2) :: nil); exists a2; exists l2; split. simpl; intros u1 u2 [u1u2_eq_t1t2 | u1u2_in_nil]; [injection u1u2_eq_t1t2; intros; subst; assumption | contradiction]. split; apply eq_refl. right; left; exists ((t1,t2) :: ll); exists a2; exists l2'; split. simpl; intros u1 u2 [u1u2_eq_t1t2 | u1u2_in_ll]; [injection u1u2_eq_t1t2; intros; subst | apply Hll]; assumption. split; subst; apply eq_refl. do 2 right; exists ((t1,t2) :: ll); exists a1; exists a2; exists l1'; exists l2'; split. simpl; intros u1 u2 [u1u2_eq_t1t2 | u1u2_in_ll]; [injection u1u2_eq_t1t2; intros; subst | apply Hll]; assumption. split. assumption. split. intros u [t1_eq_u | u_in_l1]. subst u; left; exists t2; split; left; trivial. destruct (H _ u_in_l1) as [[u2 [u2_in_l2 H']] | H']. left; exists u2; split; [right | idtac]; assumption. right; assumption. split; subst; apply eq_refl. intros [[H1 H2] | [[ll [a1 [l1' [Hll [H1 H2]]]]] | [ll [a1 [a2 [l1' [l2' [Hll [Ha [H [H1 H2]]]]]]]]]]]. right; left; subst; destruct l1 as [ | a1 l1]. discriminate. exists ((t1,t2) :: nil); exists a1; exists l1; split. simpl; intros u1 u2 [u1u2_eq_t1t2 | u1u2_in_nil]; [injection u1u2_eq_t1t2; intros; subst; assumption | contradiction]. split; apply eq_refl. right; left; exists ((t1,t2) :: ll); exists a1; exists l1'; split. simpl; intros u1 u2 [u1u2_eq_t1t2 | u1u2_in_ll]; [injection u1u2_eq_t1t2; intros; subst | apply Hll]; assumption. split; subst; apply eq_refl. do 2 right; exists ((t1,t2) :: ll); exists a1; exists a2; exists l1'; exists l2'; split. simpl; intros u1 u2 [u1u2_eq_t1t2 | u1u2_in_ll]; [injection u1u2_eq_t1t2; intros; subst | apply Hll]; assumption. split. assumption. split. intros u [t2_eq_u | u_in_l2]. subst u; left; exists t1; split; left; trivial. destruct (H _ u_in_l2) as [[u1 [u1_in_l1 H']] | H']. left; exists u1; split; [right | idtac]; assumption. right; assumption. split; subst; apply eq_refl. trivial. case_eq (lexico_eval p s1 s2 l1 l2). intros [ | | | ] Hl. intros [ll [Hll [H1 H2]]]. generalize (term_gt_list_is_sound p s2 (t1 :: l1)). destruct (term_gt_list p s2 (t1 :: l1)) as [[ | ] | ]. intro H; do 2 right; exists (@nil (term * term)); exists t1; exists t2; exists l1; exists l2; split. intros; contradiction. split. assumption. split. intros u u_in_t1l1; right; apply H; trivial. simpl; split; subst; apply eq_refl. trivial. trivial. intros [[H1 H2] | [[ll [a2 [l2' [Hll [H1 H2]]]]] | [ll [a1 [a2 [l1' [l2' [Hll [Ha [H [H1 H2]]]]]]]]]]]; generalize (term_gt_list_is_sound p s2 (t1 :: l1)); destruct (term_gt_list p s2 (t1 :: l1)) as [[ | ] | ]; intro H'; trivial; do 2 right; exists (@nil (term * term)); exists t1; exists t2; exists l1; exists l2; split. intros; contradiction. split. assumption. split. intros u u_in_t1l1; right; apply H'; assumption. split; apply eq_refl. intros; contradiction. split. assumption. split. intros u u_in_t1l1; right; apply H'; assumption. split; apply eq_refl. intros; contradiction. split. assumption. split. intros u u_in_t1l1; right; apply H'; assumption. split; apply eq_refl. intros _. generalize (term_gt_list_is_sound p s2 (t1 :: l1)); destruct (term_gt_list p s2 (t1 :: l1)) as [[ | ] | ]; intro H'; trivial. do 2 right; exists (@nil (term * term)); exists t1; exists t2; exists l1; exists l2; split. intros; contradiction. split. assumption. split. intros u u_in_t1l1; right; apply H'; assumption. split; apply eq_refl. intros _. generalize (term_gt_list_is_sound p s2 (t1 :: l1)); destruct (term_gt_list p s2 (t1 :: l1)) as [[ | ] | ]; intro H'; trivial. do 2 right; exists (@nil (term * term)); exists t1; exists t2; exists l1; exists l2; split. intros; contradiction. split. assumption. split. intros u u_in_t1l1; right; apply H'; assumption. split; apply eq_refl. intros _. generalize (term_gt_list_is_sound p s2 (t1 :: l1)); destruct (term_gt_list p s2 (t1 :: l1)) as [[ | ] | ]; intro H'; trivial. do 2 right; exists (@nil (term * term)); exists t1; exists t2; exists l1; exists l2; split. intros; contradiction. split. assumption. split. intros u u_in_t1l1; right; apply H'; assumption. split; apply eq_refl. case_eq (lexico_eval p s1 s2 l1 l2). intros [ | | | ] Hl. intros [ll [Hll [H1 H2]]]. generalize (term_gt_list_is_sound p s1 (t2 :: l2)). destruct (term_gt_list p s1 (t2 :: l2)) as [[ | ] | ]. intro H; do 2 right; exists (@nil (term * term)); exists t1; exists t2; exists l1; exists l2; split. intros; contradiction. split. assumption. split. intros u u_in_t1l2; right; apply H; trivial. simpl; split; subst; apply eq_refl. trivial. trivial. intros [[H1 H2] | [[ll [a2 [l2' [Hll [H1 H2]]]]] | [ll [a1 [a2 [l1' [l2' [Hll [Ha [H [H1 H2]]]]]]]]]]]; generalize (term_gt_list_is_sound p s1 (t2 :: l2)); destruct (term_gt_list p s1 (t2 :: l2)) as [[ | ] | ]; intro H'; trivial; do 2 right; exists (@nil (term * term)); exists t1; exists t2; exists l1; exists l2; split. intros; contradiction. split. assumption. split. intros u u_in_t2l2; right; apply H'; assumption. split; apply eq_refl. intros; contradiction. split. assumption. split. intros u u_in_t2l2; right; apply H'; assumption. split; apply eq_refl. intros; contradiction. split. assumption. split. intros u u_in_t2l2; right; apply H'; assumption. split; apply eq_refl. intros _. generalize (term_gt_list_is_sound p s1 (t2 :: l2)); destruct (term_gt_list p s1 (t2 :: l2)) as [[ | ] | ]; intro H'; trivial. do 2 right; exists (@nil (term * term)); exists t1; exists t2; exists l1; exists l2; split. intros; contradiction. split. assumption. split. intros u u_in_t2l2; right; apply H'; assumption. split; apply eq_refl. intros _. generalize (term_gt_list_is_sound p s1 (t2 :: l2)); destruct (term_gt_list p s1 (t2 :: l2)) as [[ | ] | ]; intro H'; trivial. do 2 right; exists (@nil (term * term)); exists t1; exists t2; exists l1; exists l2; split. intros; contradiction. split. assumption. split. intros u u_in_t2l2; right; apply H'; assumption. split; apply eq_refl. intros _. generalize (term_gt_list_is_sound p s1 (t2 :: l2)); destruct (term_gt_list p s1 (t2 :: l2)) as [[ | ] | ]; intro H'; trivial. do 2 right; exists (@nil (term * term)); exists t1; exists t2; exists l1; exists l2; split. intros; contradiction. split. assumption. split. intros u u_in_t2l2; right; apply H'; assumption. split; apply eq_refl. 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)