proposition: Lemma diff_index_p : forall a b, a <> b -> {i | select a i <> select b i}.
proof: Proof. intros a b. assert (Hcomp:forall (k:key), exists e, compare k k = EQ e). { intro k. case_eq (compare k k); try (intro H; now elim (lt_not_eq _ _ H)). intros e He. now exists e. } assert (HInd: forall x y (xS:Sorted _ x) (yS:Sorted _ y) (xD:NoDefault x) (yD:NoDefault y), let a := Build_farray xS xD in let b := Build_farray yS yD in a <> b -> {i : key | select a i <> select b i}). { clear a b. intros x y. case_eq (list_eq_dec (@eq_dec _ (Raw.ke_dec key_dec elt_dec)) x y). - intros e He. subst x. intros xS yS xD yD a b. subst a b. rewrite (proof_irrelevance _ xS yS), (proof_irrelevance _ xD yD). intro H. elim H. reflexivity. - intros n _ xS yS xD yD a b _. subst a b. revert x y n xS yS xD yD. { induction x as [ |[xk xe] xs IHxs]; intros [ |[yk ye] ys]. - intro H; now elim H. - intros _ xS yS xD yD. exists yk. unfold select, find. simpl. destruct (Hcomp yk) as [e ->]. unfold NoDefault in yD. intro H. subst ye. elim (yD yk). unfold Raw.MapsTo. constructor. apply Raw.eqke_refl. - intros _ xS yS xD yD. exists xk. unfold select, find. simpl. destruct (Hcomp xk) as [e ->]. unfold NoDefault in xD. intro H. subst xe. elim (xD xk). unfold Raw.MapsTo. constructor. apply Raw.eqke_refl. - intros H xS yS xD yD. case_eq (compare xk yk). + intros l Hl. exists xk. unfold select, find. simpl. destruct (Hcomp xk) as [e ->]. rewrite Hl. unfold NoDefault in xD. intro H1; subst xe. apply (xD xk). unfold Raw.MapsTo. constructor. apply Raw.eqke_refl. + intros e _. subst xk. case_eq (eq_dec xe ye). * intros e _. subst ye. assert (H1:xs <> ys) by (intro H1; rewrite H1 in H; now apply H). assert (xsS : Sorted (Raw.ltk key_ord) xs) by now inversion xS. assert (ysS : Sorted (Raw.ltk key_ord) ys) by now inversion yS. assert (xsD:NoDefault xs) by exact (nodefault_tail xD). assert (ysD:NoDefault ys) by exact (nodefault_tail yD). destruct (IHxs _ H1 xsS ysS xsD ysD) as [i Hi]. { case_eq (compare i yk). - intros l Hl. rewrite (lt_select_default xsS xsD) in Hi. + rewrite (lt_select_default ysS ysD) in Hi. * now elim Hi. * { intro xe0. apply (InfA_ltA _ (y:=(yk, xe))). - simpl. unfold Raw.ltk. simpl. auto. - now inversion yS. } + intro xe0. apply (InfA_ltA _ (y:=(yk, xe))). * simpl. unfold Raw.ltk. simpl. auto. * now inversion xS. - intros l Hl. rewrite (lt_select_default xsS xsD) in Hi. + rewrite (lt_select_default ysS ysD) in Hi. * now elim Hi. * intro xe0. inversion yS as [ |a l0 H3 H4 H0]; subst. apply (HdRelElt H4). + intro xe0. inversion xS as [ |a l0 H3 H4 H0]; subst. apply (HdRelElt H4). - intros l Hl. exists i. unfold select, find. simpl. now rewrite Hl. } * intros n Hn. exists yk. unfold select, find. simpl. now destruct (Hcomp yk) as [e ->]. + intros l Hl. exists yk. unfold select, find. simpl. destruct (Hcomp yk) as [e ->]. case_eq (compare yk xk). * intros m Hm. unfold NoDefault in yD. intro H1; subst ye. apply (yD yk). unfold Raw.MapsTo. constructor. apply Raw.eqke_refl. * intros f _. subst yk. now elim (lt_not_eq _ _ l). * intros f _. now elim (lt_not_eq _ _ (lt_trans _ _ _ l f)). } } intro H. apply (HInd (this a) (this b) (sorted a) (sorted b) (nodefault a) (nodefault b)). destruct a as [aL aS aD]. simpl. destruct b as [bL bS bD]. simpl. auto. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance