proposition: Lemma PosToPathPrefixFreeAux : forall (x y : positive), (x <> y) -> le (length (posToPathAux y)) (length(posToPathAux x)) -> PrefixFree [posToPath x; posToPath y].
proof: Proof. intros x y H Leq. apply FreeCons; [ apply FreeCons ; [ constructor | intros p Contra; inversion Contra] | ]. intros. inversion H0; subst; clear H0; [ | inversion H2]. unfold posToPath in *; simpl in *; repeat rewrite <- app_assoc in *. pose proof (lengthSplit1 Leq) as Hyp. inversion Hyp as [pair Split]; clear Hyp. destruct pair as [l0 l1]. pose proof (lengthSplit2 Split) as AppHyp. pose proof (lengthSplit3 Split) as LenHyp. pose proof (lengthPathEven y) as Hyp; inversion Hyp as [n LenN]; subst; clear Hyp. assert (XHyp : pathToPosAux (l0 ++ l1 ++ [Right]) (fun x => x) = Some x); [ rewrite app_assoc; rewrite AppHyp; apply posPathInj | ]. rewrite <- LenHyp in LenN. pose proof (evenPathAux [Right] LenN XHyp) as Even. inversion Even as [f' HF]; clear Even. inversion HF as [HF1 HF2]; clear HF. rewrite <- AppHyp in H1. rewrite <- app_assoc in H1. destruct (list_eq_dec Direction_eq_dec (posToPathAux y) l0). - subst. apply app_inv_head in H1. destruct l1. * simpl in AppHyp; rewrite app_nil_r in AppHyp. assert (posToPathAux y ++ [Right] = posToPathAux x ++ [Right]) by (rewrite AppHyp; auto). assert (posToPath y = posToPath x) by (unfold posToPath; auto). assert (pathToPos (posToPath y) = pathToPos (posToPath x)) by (rewrite H2; auto). repeat rewrite posPathInj in H3. congruence. * assert (Contra : hd_error (s :: l1) = Some Left). eapply pathBeginsLeft. + unfold not; intros; congruence. + instantiate (1 := [Right]); unfold not; intros; congruence. + instantiate (1:= x); instantiate (1:=f'). rewrite <- HF2. apply XHyp. simpl in Contra. inversion Contra; subst. simpl in H1. congruence. - eapply listAppNeq. * apply Direction_eq_dec. * instantiate (1 := l0). instantiate (1 := posToPathAux y). eauto. * eassumption. * eapply H1. Qed.
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets