60 lines
1.6 KiB
Coq
60 lines
1.6 KiB
Coq
Require Import subsequences.
|
|
Require Import Sorting.Permutation.
|
|
|
|
Require Import Nat.
|
|
Require Import PeanoNat.
|
|
Require Import List.
|
|
|
|
|
|
Import ListNotations.
|
|
|
|
|
|
|
|
Definition permutation_mapping {X: Type} (u v base : list X) :=
|
|
exists p l, Permutation base p
|
|
/\ map Some u = map (nth_error base) l
|
|
/\ map Some v = map (nth_error p) l.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Definition incl_without_eq {X: Type} (u v : list X) :=
|
|
exists l, map Some u = map (nth_error v) l.
|
|
|
|
|
|
Lemma incl_without_eq_incl {X: Type}:
|
|
forall (u v : list X), incl_without_eq u v -> incl u v.
|
|
Proof.
|
|
intro u. induction u; intro v; intro H. easy. destruct H.
|
|
destruct x. symmetry in H. apply nil_cons in H. contradiction.
|
|
inversion H. apply incl_cons.
|
|
symmetry in H1. apply nth_error_In in H1. assumption.
|
|
apply IHu. exists x. assumption.
|
|
Qed.
|
|
|
|
|
|
Lemma incl_incl_without_eq {X: Type}:
|
|
forall (u v : list X), incl u v -> incl_without_eq u v.
|
|
Proof.
|
|
intro u. induction u; intro v; intro H. exists nil. easy.
|
|
apply incl_cons_inv in H. destruct H. apply IHu in H0. destruct H0.
|
|
apply In_nth_error in H. destruct H. exists (x0 :: x).
|
|
simpl. rewrite H. rewrite H0. reflexivity.
|
|
Qed.
|
|
|
|
|
|
|
|
Lemma permutation_mapping_self {X: Type} :
|
|
forall (u base : list X), incl u base -> permutation_mapping u u base.
|
|
Proof.
|
|
intro u. induction u; intro base; intro H; exists base.
|
|
exists nil. split; easy. apply incl_cons_inv in H. destruct H.
|
|
apply IHu in H0. destruct H0. destruct H0. destruct H0. destruct H1.
|
|
apply In_nth_error in H. destruct H. exists (x1 :: x0).
|
|
split. easy. split; simpl; rewrite H; rewrite H1; reflexivity.
|
|
Qed.
|
|
|
|
|