proposition: Lemma test2: forall (l' l: list E), NoDup l -> NoDup l' -> incl l' l -> exists lsorted, Permutation lsorted l' /\ (forall a b, In a lsorted -> In b lsorted -> (find lsorted a 0 <= find lsorted b 0 <-> find l a 0 <= find l b 0)).
proof: Proof. induction l'; intros l Hl; intros. exists nil. split. apply perm_nil. intros. contradiction. assert (exists lsorted : list E, Permutation lsorted l' /\ (forall a b : E, In a lsorted -> In b lsorted -> find lsorted a 0 <= find lsorted b 0 <-> find l a 0 <= find l b 0)). apply IHl'. auto. apply NoDup_cons_1 in H; auto. unfold incl; intros. apply H0. right; auto. clear IHl'. destruct H1 as [lsorted [? ?]]. assert (Ha: ~ In a lsorted). unfold not; intros. apply (Permutation_in (l':=l')) in H3. 2: auto. apply NoDup_cons_2 in H; contradiction. assert (Hsorted_NoDup: NoDup lsorted). apply (Permutation_NoDup (l:=l')). apply Permutation_sym; auto. apply NoDup_cons_1 in H; auto. set (k:= find l a 0) in *. assert (exists l1 l2, lsorted = l1++l2 /\ (forall x, In x l1 -> find l x 0 < find l a 0) /\ (forall x, In x l2 -> find l a 0 <= find l x 0)). { clear H1. induction lsorted. exists nil; exists nil. split. rewrite app_nil_r; auto. split; intros; contradiction. destruct (Z.lt_ge_cases (find l a0 0) (find l a 0)); rename H1 into Ha0. ++ assert (exists l1 l2 : list E, lsorted = l1 ++ l2 /\ (forall x : E, In x l1 -> find l x 0 < find l a 0) /\ (forall x : E, In x l2 -> find l a 0 <= find l x 0)). { apply IHlsorted. 2: { unfold not; intros. apply Ha. right; auto. } 2: { apply NoDup_cons_1 in Hsorted_NoDup; auto. } intros. split; intros. apply H2. right; auto. right; auto. apply NoDup_cons_2 in Hsorted_NoDup. simpl. destruct (E_EqDec a0 a1). hnf in e; subst a0; contradiction. destruct (E_EqDec a0 b). hnf in e; subst a0; contradiction. replace 1 with (1+0) by lia. do 2 rewrite find_accum_add1. lia. apply H2 in H4. 2: right; auto. 2: right; auto. simpl in H4. apply NoDup_cons_2 in Hsorted_NoDup. destruct (E_EqDec a0 a1). hnf in e; subst a0; contradiction. destruct (E_EqDec a0 b). hnf in e; subst a0; contradiction. replace 1 with (1+0) in H4 by lia. do 2 rewrite find_accum_add1 in H4. lia. } clear IHlsorted. destruct H1 as [l1 [l2 [? [? ?]]]]. exists (a0::l1). exists l2. split. simpl. rewrite H1; auto. split; intros. destruct H5. subst x; auto. apply H3; auto. apply H4; auto. ++ exists nil. exists (a0::lsorted). split. auto. split; intros. contradiction. destruct H1. subst x. auto. apply (Z.le_trans _ (find l a0 0)). auto. apply H2. left; auto. right; auto. rewrite find_cons. apply find_lbound. } destruct H3 as [l1 [l2 [? [? ?]]]]. subst lsorted. exists (l1++a::l2). split. { apply NoDup_Permutation. apply NoDup_app_inv. apply NoDup_app_l in Hsorted_NoDup; auto. apply NoDup_cons. unfold not; intros; apply Ha. apply in_or_app; right; auto. apply NoDup_app_r in Hsorted_NoDup; auto. unfold not; intros. destruct H6. subst x. apply Ha. apply in_or_app; left; auto. assert (~ In x l2). apply (NoDup_app_not_in E l1 l2); auto. contradiction. auto. split; intros. apply in_app_or in H3; destruct H3. right. apply (Permutation_in (l:=l1++l2)); auto. apply in_or_app; left; auto. destruct H3. subst x. left; auto. right. apply (Permutation_in (l:=l1++l2)); auto. apply in_or_app; right; auto. apply in_or_app. destruct H3. subst x. right; left; auto. apply (Permutation_in (l':=l1++l2)) in H3. 2: apply Permutation_sym; auto. apply in_app_or in H3; destruct H3. left; auto. right; right; auto. } intros. apply in_app_or in H3. apply in_app_or in H6. specialize H2 with a0 b. destruct H3; destruct H6. ** rewrite (find_app_In1 l1 (a::l2)) by auto. rewrite find_app_In1 by auto. rewrite find_app_In1 in H2 by auto. rewrite find_app_In1 in H2 by auto. apply H2. apply in_or_app. left; auto. apply in_or_app; left; auto. ** rewrite find_app_In1 by auto. assert (~ In b l1). unfold not; intros. destruct H6. subst b. apply Ha. apply in_or_app; left; auto. assert (~ In b l2). apply (NoDup_app_not_in E l1 l2); auto. contradiction. rewrite find_app_notIn1 by auto. destruct H6. subst b. split; intros. apply Z.le_lteq. left; apply H4; auto. apply (Z.le_trans _ (Zlength l1 + 0)). apply find_ubound. pose proof (find_lbound (a::l2) a 0); lia. split; intros. apply (Z.le_trans _ (find l a 0)). apply Z.le_lteq. left; apply H4; auto. apply H5; auto. apply (Z.le_trans _ (Zlength l1 + 0)). apply find_ubound. pose proof (find_lbound (a::l2) b 0); lia. ** assert (~ In a0 l1). unfold not; intros. destruct H3. subst a0. apply Ha. apply in_or_app; left; auto. assert (~ In a0 l2). apply (NoDup_app_not_in E l1 l2); auto. contradiction. rewrite find_app_notIn1 by auto. rewrite find_app_In1 by auto. split; intros. assert (find l1 b 0 < Zlength l1 + 0). apply find_In_ubound; auto. rewrite Z.add_0_r in H9. assert (0 <= find (a::l2) a0 0). apply find_lbound. lia. destruct H3. subst a0. **** assert (find l b 0 < find l a 0). apply H4; auto. lia. **** assert (find l b 0 < find l a0 0). apply (Z.lt_le_trans _ (find l a 0)). apply H4; auto. apply H5; auto. lia. ** assert (~ In a0 l1). unfold not; intros. destruct H3. subst a0. apply Ha. apply in_or_app; left; auto. assert (~ In a0 l2). apply (NoDup_app_not_in E l1 l2); auto. contradiction. assert (~ In b l1). unfold not; intros. destruct H6. subst b. apply Ha. apply in_or_app; left; auto. assert (~ In b l2). apply (NoDup_app_not_in E l1 l2); auto. contradiction. rewrite find_app_notIn1 by auto. rewrite find_app_notIn1 by auto. rewrite find_app_notIn1 in H2 by auto. rewrite find_app_notIn1 in H2 by auto. destruct H3; destruct H6. **** subst a0. subst b. split; intros; lia. **** subst a0. rewrite find_cons. split; intros. apply H5; auto. pose proof (find_lbound (a::l2) b 0); lia. **** subst b. rewrite find_cons. split; intros. assert (0 < find (a::l2) a0 0). simpl. destruct (E_EqDec a a0). hnf in e. subst a0. exfalso; apply Ha. apply in_or_app; right; auto. pose proof (find_lbound l2 a0 1). lia. lia. apply Z.le_lteq in H6. destruct H6. assert (find l a 0 <= find l a0 0). apply H5; auto. lia. assert (incl l' l). unfold incl; intros. apply H0. right; auto. apply (find_eq l a0 a 0) in H6. subst a0. rewrite find_cons; lia. auto. apply H9. apply (Permutation_in (l:= (l1++l2))); auto. apply in_or_app; right; auto. apply H0. left; auto. **** rewrite <- H2. 2: apply in_or_app; right; auto. 2: apply in_or_app; right; auto. simpl. destruct (E_EqDec a a0). hnf in e; subst a0. exfalso; apply Ha. apply in_or_app; right; auto. destruct (E_EqDec a b). hnf in e; subst b. exfalso; apply Ha. apply in_or_app; right; auto. replace 1 with (1+0) by lia. do 2 rewrite find_accum_add1. split; intros; lia. Qed.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext