proposition: Lemma PermSorted : forall (l l' : list positive), Permutation.Permutation l l' -> StronglySorted (fun x x0 : positive => is_true (x <=? x0)%positive) l -> StronglySorted (fun x x0 : positive => is_true (x <=? x0)%positive) l' -> l = l'.
proof: Proof. intro l; induction l. intro l'; induction l'. reflexivity. intro HPerm. apply Permutation.Permutation_nil_cons in HPerm. intuition. intro l'; induction l'. intro HPerm. apply Permutation.Permutation_sym in HPerm. apply Permutation.Permutation_nil_cons in HPerm. intuition. intros HPerm Hl Hl'. assert (HIna' : In a (a :: l)) by (apply in_eq). assert (HIna : In a (a0 :: l')) by (apply Permutation.Permutation_in with (a :: l); assumption). assert (HIna0' : In a0 (a0 :: l')) by (apply in_eq). assert (HIna0 : In a0 (a :: l)) by (apply Permutation.Permutation_in with (a0 :: l'); apply Permutation.Permutation_sym in HPerm;assumption). clear HIna'; clear HIna0'; apply in_inv in HIna; apply in_inv in HIna0. elim HIna; clear HIna; intro HIna; elim HIna0; clear HIna0; intro HIna0; try (rewrite HIna in *); try (rewrite <- HIna0 in *). assert (HPerm' : Permutation.Permutation l l') by (apply Permutation.Permutation_app_inv_l with (a :: nil); simpl; assumption). apply OCPSortedTl in Hl; apply OCPSortedTl in Hl'. apply IHl in HPerm'; try assumption. rewrite HPerm'; reflexivity. assert (HPerm' : Permutation.Permutation l l') by (apply Permutation.Permutation_app_inv_l with (a :: nil); simpl; assumption). apply OCPSortedTl in Hl; apply OCPSortedTl in Hl'. apply IHl in HPerm'; try assumption. rewrite HPerm'; reflexivity. assert (HPerm' : Permutation.Permutation l l') by (apply Permutation.Permutation_app_inv_l with (a :: nil); simpl; assumption). apply OCPSortedTl in Hl; apply OCPSortedTl in Hl'. apply IHl in HPerm'; try assumption. rewrite HPerm'; reflexivity. assert (Hle1 := Hl); assert (Hle2 := Hl'). apply StronglySorted_inv in Hle1; apply StronglySorted_inv in Hle2. destruct Hle1 as [Hclear Hle1]; clear Hclear; destruct Hle2 as [Hclear Hle2]; clear Hclear. assert (Haa0 : (forall x, In x l -> is_true (Pos.leb a x))) by (apply Forall_forall; assumption). assert (Ha0a : (forall x, In x l' -> is_true (Pos.leb a0 x))) by (apply Forall_forall; assumption). apply Ha0a in HIna. apply Haa0 in HIna0. unfold is_true in *. apply Pos.leb_le in HIna; apply Pos.leb_le in HIna0. assert (H := Pos.le_antisym a0 a HIna HIna0). rewrite H in *. assert (HPerm' : Permutation.Permutation l l') by (apply Permutation.Permutation_app_inv_l with (a :: nil); simpl; assumption). apply OCPSortedTl in Hl; apply OCPSortedTl in Hl'. apply IHl in HPerm'; try assumption. rewrite HPerm'; reflexivity. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms