HyPre.util.PreSuffix
Require Import Program.Equality Lia.
Require Export ListExtra.
From Coq Require Import Classes.EquivDec.
Import ListNotations.
From Coq Require Import Decidable.
From HyPre Require Import Tac.
Notation "x ⊆ y" := (incl x y) (at level 50).
Inductive prefix {A : Type} : list A -> list A -> Prop :=
| PreSame l : prefix l l
| PreStep {a l l'} : prefix l l' -> prefix l (a :: l').
Lemma prefix_cons_in {A : Type} `{EqDec A eq} (a : A) l l' : prefix (a :: l) l' -> In a l'.
Proof.
intro Q. revert dependent l. induction l'; cbn in *; intros l Q.
- inversion Q.
- destruct (a == a0).
+ auto.
+ inversion Q; subst.
* exfalso; apply c; reflexivity.
* eauto.
Qed.
Inductive suffix {A : Type} : list A -> list A -> Prop :=
| SufSame l : suffix l l
| SufStep {a l l'} : suffix l l' -> suffix l (l' :r: a).
Fixpoint prefix_nincl {A : Type} `{EqDec A eq} (a : A) (l : list A) : list A :=
match l with
| nil => nil
| b :: l => if a == b then l else prefix_nincl a l
end.
Lemma prefix_nincl_prefix {A : Type} `{EqDec A eq} (a : A) l :
In a l -> prefix (a :: prefix_nincl a l) l.
Proof.
intros Q.
induction l; cbn;
inversion Q.
- subst a0. destruct (a == a); [|exfalso; apply c; reflexivity].
econstructor.
- destruct (a == a0).
+ destruct e. econstructor.
+ econstructor. eauto.
Qed.
Lemma prefix_cons {A : Type} (l l' : list A) :
forall a, prefix (a :: l) l' -> prefix l l'.
Proof.
intros a H. dependent induction H.
- econstructor. econstructor.
- econstructor. eapply IHprefix; eauto.
Qed.
Lemma prefix_trans {A : Type} (l1 l2 l3 : list A) :
prefix l1 l2 -> prefix l2 l3 -> prefix l1 l3.
Proof.
revert l1 l3. induction l2; intros l1 l3 pre1 pre2; inversion pre1; inversion pre2; subst; eauto.
econstructor. eapply IHl2; eauto. eapply prefix_cons; eauto.
Qed.
Global Instance prefix_Transitive (A : Type) : Transitive (@prefix A).
Proof.
unfold Transitive.
eapply prefix_trans.
Qed.
Lemma in_prefix_in {A : Type} `{EqDec A eq} (a : A) l l' :
In a l -> prefix l l' -> In a l'.
Proof.
intros Hin Hpre. induction l.
- inversion Hin.
- destruct (a == a0).
+ destruct e. eapply prefix_cons_in; eauto.
+ eapply IHl; eauto.
* destruct Hin; [exfalso; subst; apply c; reflexivity|assumption].
* eapply prefix_cons; eauto.
Qed.
Fixpoint suffix_nincl {A : Type} `{EqDec A eq} (a : A) (l : list A) : list A :=
match l with
| nil => nil
| b :: l => if a == b then nil else b :: suffix_nincl a l
end.
Lemma suffix_nil {A : Type} (l : list A) : suffix nil l.
apply rcons_ind; [econstructor|].
intros. econstructor; eauto.
Qed.
Ltac rinduction L := revert dependent L; intro L; eapply rcons_ind with (l:=L); intros.
Lemma suffix_cons {A : Type} a (l l': list A) :
suffix l l' -> suffix (a :: l) (a :: l').
Proof.
intros post.
- induction post.
+ econstructor.
+ rewrite <-cons_rcons_assoc. econstructor. assumption.
Qed.
Lemma suffix_eq {A : Type} (l1 l2 : list A) :
suffix l1 l2 <-> exists l2', l2 = l1 ++ l2'.
Proof.
split.
- intro post. induction post.
+ exists nil. apply app_nil_end.
+ destruct IHpost as [l2' IH].
exists (l2' :r: a). rewrite IH. rewrite app_assoc. reflexivity.
- intros [l2' H]. subst l2.
rinduction l2'.
+ rewrite <-app_nil_end. econstructor.
+ rewrite app_assoc. econstructor. eauto.
Qed.
Lemma cons_suffix {A : Type} a b (l l': list A) :
suffix (a :: l) (b :: l') -> suffix l l'.
Proof.
intros post. apply suffix_eq. apply suffix_eq in post as [l1' leq].
exists l1'. inversion leq. reflexivity.
Qed.
Lemma suffix_app {A : Type} (l1 l2 l' : list A) :
suffix (l' ++ l1) (l' ++ l2) -> suffix l1 l2.
Proof.
revert l1 l2. induction l'; intros; cbn; eauto.
apply IHl'. cbn in H. inversion H.
- rewrite H2. econstructor.
- eapply cons_suffix; eauto.
Qed.
Lemma suffix_nincl_suffix {A : Type} `{EqDec A eq} a l : suffix (suffix_nincl a l) l.
Proof.
induction l; cbn; [econstructor; reflexivity|].
destruct (a == a0); cbn; eauto using suffix_nil, suffix_cons.
Qed.
Lemma suffix_nil_nil {A : Type} (l : list A) :
suffix l nil -> l = nil.
Proof.
intro H. inversion H; eauto. destruct l'; cbn in H0; congruence.
Qed.
Lemma prefix_nil_nil {A : Type} (l : list A) :
prefix l nil -> l = nil.
Proof.
intro H. inversion H; eauto.
Qed.
Lemma suffix_rcons_nil_eq {A : Type} l (a b : A) :
suffix (l :r: a) (b :: nil) -> a = b /\ l = nil.
Proof.
intros post. apply suffix_eq in post as [l2' post]. destruct l; cbn in *; eauto.
- inversion post; eauto.
- inversion post. destruct l; cbn in H1; congruence.
Qed.
Lemma suffix_nincl_spec {A : Type} `{EqDec A eq} (a : A) l :
In a l -> suffix (suffix_nincl a l :r: a) l.
Proof.
intros ina.
induction l; inversion ina.
- subst a0. cbn. destruct equiv_dec;[|exfalso; apply c; reflexivity].
cbn. apply suffix_cons, suffix_nil.
- cbn. destruct equiv_dec; cbn.
+ destruct e; apply suffix_cons, suffix_nil.
+ apply suffix_cons. eauto.
Qed.
Lemma suffix_nincl_invariant {A : Type} `{EqDec A eq} (a : A) l :
~ In a l -> suffix_nincl a l = l.
Proof.
intros nin.
induction l; cbn; eauto.
destruct equiv_dec.
- destruct e. exfalso. apply nin. econstructor; eauto.
- rewrite IHl; eauto. contradict nin. econstructor 2; eauto.
Qed.
Lemma suffix_incl {A : Type} (l l' : list A) : suffix l l' -> incl l l'.
Proof.
intros post. induction post.
- apply incl_refl.
- apply incl_appl; eauto.
Qed.
Lemma suffix_hd_eq (A : Type) (a b : A) l l' :
suffix (a :: l) (b :: l') -> a = b.
Proof.
intro post. eapply suffix_eq in post as [l2' pst].
cbn in pst. inversion pst. eauto.
Qed.
Lemma suffix_order_destruct' {A : Type} (l1 l2 l3 : list A) :
suffix l1 l3 -> suffix l2 l3 -> length l1 <= length l2 -> suffix l1 l2.
Proof.
revert l1 l3. induction l2; intros l1 l3 post1 post2 len; cbn in *.
- destruct l1; cbn in len; [econstructor|lia].
- destruct l1; [eapply suffix_nil|].
destruct l3; [eapply suffix_nil_nil in post1; congruence|].
eapply suffix_hd_eq in post1 as aeq. destruct aeq.
eapply suffix_hd_eq in post2 as aeq. destruct aeq.
eapply suffix_cons, IHl2. 1,2: eapply cons_suffix; eauto. cbn in len. lia.
Qed.
Lemma suffix_order_destruct {A : Type} (l1 l2 l3 : list A) :
suffix l1 l3 -> suffix l2 l3 -> suffix l1 l2 \/ suffix l2 l1.
Proof.
intros post1 post2.
destruct (Nat.ltb (length l1) (length l2)) eqn:H.
- left. eapply suffix_order_destruct'; eauto. eapply PeanoNat.Nat.ltb_lt in H. lia.
- right. eapply suffix_order_destruct'; eauto. eapply PeanoNat.Nat.ltb_nlt in H. lia.
Qed.
Lemma suffix_step_left {A : Type} (l l' : list A) a :
suffix (l :r: a) l' -> suffix l l'.
Proof.
intros.
remember (l :r: a) as l0.
induction H. subst l0.
- econstructor. econstructor.
- econstructor; eauto.
Qed.
Lemma suffix_length {A : Type} (l l' : list A) :
suffix l l' -> length l <= length l'.
Proof.
intros post. induction post.
- reflexivity.
- rewrite length_rcons. rewrite IHpost. lia.
Qed.
Lemma suffix_order {A : Type} (l1 l2 l' : list A) (a : A) :
~ In a l1 -> In a l2 -> suffix l1 l' -> suffix l2 l' -> suffix l1 l2.
Proof.
intros nin1 in2 pst1 pst2. eapply suffix_order_destruct'; eauto.
eapply suffix_order_destruct in pst1; eauto. clear pst2.
destruct pst1.
{ exfalso. apply suffix_incl in H. firstorder. }
apply suffix_length; eauto.
Qed.
Lemma suffix_elem {A : Type} `{EqDec A eq} (a:A) l l':
length l > 0 -> suffix l (a :: l') -> In a l.
Proof.
intros len post.
destruct l.
{ cbn in len; lia. }
eapply suffix_hd_eq in post.
subst a0. econstructor; eauto.
Qed.
Lemma suffix_trans {A : Type} (l l' l'': list A) :
suffix l l' -> suffix l' l'' -> suffix l l''.
Proof.
intros post1; revert l''.
induction post1; intros l'' post2.
- induction post2; econstructor; eauto.
- apply IHpost1. eapply suffix_step_left; eauto.
Qed.
Lemma suffix_nincl_nincl {A : Type} `{EqDec A eq} (a : A) l :
~ In a (suffix_nincl a l).
Proof.
induction l; cbn; eauto. destruct (a == a0).
- tauto.
- contradict IHl. inversion IHl.
+ subst a0. exfalso; apply c; reflexivity.
+ assumption.
Qed.
Definition prefix_incl : forall (A : Type) (l l' : list A), prefix l l' -> l ⊆ l'
:= fun (A : Type) (l l' : list A) (post : prefix l l') =>
@prefix_ind A (fun l0 l'0 : list A => l0 ⊆ l'0) (fun l0 : list A => incl_refl l0)
(fun (a : A) (l0 l'0 : list A) (_ : prefix l0 l'0) (IHpost : l0 ⊆ l'0) =>
incl_appr (a :: nil) IHpost) l l' post.
Lemma prefix_in_list {A : Type} l (a:A) :
In a l
-> exists l', prefix (a :: l') l.
Proof.
intro Hin.
induction l.
- inversion Hin.
- destruct Hin;[subst;exists l; cbn;econstructor|].
eapply IHl in H. destruct H as [l' H]. exists l'. cbn; econstructor; assumption.
Qed.
Lemma prefix_nil {A : Type} (l : list A) : prefix nil l.
Proof.
induction l; econstructor; firstorder.
Qed.
Lemma prefix_NoDup {A : Type} (l l' : list A) : prefix l l' -> NoDup l' -> NoDup l.
Proof.
intros Hpre Hnd. induction Hpre; eauto.
inversion Hnd; subst; eauto.
Qed.
Section Pre.
Variable A : Type.
Lemma prefix_eq :
forall (l1 l2 : list A), prefix l1 l2 <-> (exists l2' : list A, l2 = l2' ++ l1).
Proof.
intros.
split;intros.
- induction H.
+ exists nil; cbn; eauto.
+ destructH. exists (a :: l2'). cbn. f_equal;eauto.
- destructH. rewrite H.
revert dependent l2.
induction l2'; intros;cbn;econstructor;eauto.
Qed.
Lemma prefix_length `{EqDec A eq} (l1 l2 : list A)
(Hpre : prefix l1 l2)
(Hlen : length l1 = length l2)
: l1 = l2.
Proof.
eapply prefix_eq in Hpre. destructH. subst l2.
destruct l2';cbn in *; eauto.
exfalso.
rewrite app_length in Hlen. lia.
Qed.
Lemma prefix_rev_suffix (l l' : list A)
(Hpre : prefix l l')
: suffix (rev l) (rev l').
Proof.
induction Hpre.
- econstructor.
- rewrite rev_cons. econstructor;eauto.
Qed.
Lemma prefix_rev_suffix' (l l' : list A)
(Hpre : prefix (rev l) (rev l'))
: suffix l l'.
Proof.
rewrite <-(rev_involutive l).
rewrite <-(rev_involutive l').
eapply prefix_rev_suffix;eauto.
Qed.
Lemma suffix_rev_prefix (l l' : list A)
(Hpost : suffix l l')
: prefix (rev l) (rev l').
Proof.
induction Hpost.
- econstructor.
- rewrite rev_rcons. econstructor;eauto.
Qed.
Lemma suffix_rev_prefix' (l l' : list A)
(Hpost : suffix (rev l) (rev l'))
: prefix l l'.
Proof.
rewrite <-(rev_involutive l).
rewrite <-(rev_involutive l').
eapply suffix_rev_prefix;eauto.
Qed.
Lemma prefix_order_destruct
: forall l3 l4 l5 : list A, prefix l3 l5 -> prefix l4 l5 -> prefix l3 l4 \/ prefix l4 l3.
Proof.
intros.
eapply prefix_rev_suffix in H. eapply prefix_rev_suffix in H0.
eapply suffix_order_destruct in H;eauto.
destruct H;[right|left]; eapply suffix_rev_prefix';eauto.
Qed.
Lemma prefix_length_eq `{EqDec A eq} (l1 l2 l : list A)
(Hlen : length l1 = length l2)
(Hpre1 : prefix l1 l)
(Hpre2 : prefix l2 l)
: l1 = l2.
Proof.
eapply prefix_order_destruct in Hpre1 as Hor;eauto.
destruct Hor as [Hor|Hor]; eapply prefix_length in Hor; eauto; symmetry; eauto.
Qed.
Lemma prefix_induction {P : list A -> Prop}
: P nil
-> (forall (a : A) (l : list A) (l' : list A), P l' -> prefix (a :: l') l -> P l)
-> forall l : list A, P l.
Proof.
intros Hbase Hstep l. induction l;eauto.
eapply Hstep;eauto. econstructor.
Qed.
Lemma prefix_ex_cons (l l' : list A) (a : A)
: prefix l l' -> exists a', prefix (a' :: l) (a :: l').
Proof.
intros Hpre. revert a. induction Hpre; intros b.
- exists b. econstructor.
- specialize (IHHpre a). destructH. eexists. econstructor. eauto.
Qed.
Lemma suffix_ex_cons
: forall (l l' : list A) (a : A), suffix l l' -> exists a' : A, suffix (l :r: a') (l' :r: a).
Proof.
intros. eapply suffix_rev_prefix in H. eapply prefix_ex_cons in H. destructH.
exists a'. eapply prefix_rev_suffix'. do 2 rewrite rev_rcons. eauto.
Qed.
Lemma rcons_inj (l l' : list A) (a b : A)
: l ++ [a] = l' ++ [b] -> l = l' /\ a = b.
Proof.
revert dependent l'.
induction l;intros.
- cbn in H. destruct l';cbn in *;eauto.
+ split;inversion H;eauto.
+ inversion H. congruence'.
- destruct l';cbn in *.
+ inversion H. congruence'.
+ inversion H. subst. split;[f_equal|];eapply IHl;eauto.
Qed.
Lemma suffix_rcons_rcons (l l' : list A) (a a' : A)
: suffix (l ++ [a]) (l' ++ [a']) -> suffix l l'.
Proof.
intros Hpost.
eapply suffix_eq in Hpost. destructH.
revert dependent a. revert a' l.
induction l2';intros.
- rewrite app_nil_r in Hpost. eapply rcons_inj in Hpost. destructH. subst. constructor.
- eapply suffix_step_left. eapply IHl2'. rewrite <-app_cons_assoc. eauto.
Qed.
Lemma tl_prefix (l : list A)
: prefix (tl l) l.
Proof.
induction l;cbn;econstructor;eauto. econstructor.
Qed.
Lemma prefix_tl (l l' : list A) (a : A)
: prefix (a :: l) l' -> prefix l (tl l').
Proof.
clear. intros. inversion H;subst;cbn.
- econstructor.
- eapply prefix_cons;eauto.
Qed.
Lemma prefix_rcons (l l' : list A) (a : A)
(Hpref : prefix l l')
: prefix (l :r: a) (l' :r: a).
Proof.
clear - Hpref.
revert dependent l.
induction l';intros l Hpref;cbn.
- destruct l;cbn.
+ econstructor.
+ inversion Hpref.
- inversion Hpref;subst.
+ cbn. econstructor.
+ econstructor. eapply IHl';eauto.
Qed.
Lemma suffix_firstn (l l' : list A)
: firstn ( |l'| ) l = l' <-> suffix l' l.
Proof.
split; intro H.
- rewrite <-H.
remember (|l'|) as n. clear.
revert l. induction n.
+ cbn. eapply suffix_nil.
+ intros l. destruct l.
* cbn. econstructor;auto.
* cbn. eapply suffix_cons;eauto.
- revert dependent l. induction l';intros;cbn;auto.
destruct l. 1: inversion H;congruence'.
f_equal.
+ symmetry;eapply suffix_hd_eq;eauto.
+ eapply IHl'. eapply cons_suffix;eauto.
Qed.
Lemma prefix_lastn (l l' : list A)
: lastn ( |l'| ) l = l' <-> prefix l' l.
Proof.
split; intro H.
- eapply suffix_rev_prefix'.
eapply suffix_firstn.
eapply rev_rev_eq.
rewrite rev_involutive.
rewrite rev_length.
unfold lastn in H.
assumption.
- eapply prefix_rev_suffix in H.
eapply suffix_firstn in H.
eapply rev_rev_eq in H.
rewrite rev_involutive in H.
rewrite rev_length in H.
unfold lastn.
assumption.
Qed.
Global Instance prefix_Reflexive : Reflexive (@prefix A).
Proof.
econstructor.
Qed.
Global Instance suffix_Reflexive : Reflexive (@suffix A).
Proof.
econstructor.
Qed.
Lemma prefix_dec (B : Type) `{EqDec B eq} (l l' : list B) : decidable (prefix l l').
Proof.
revert l;induction l';intros l.
- destruct l;[left; eapply prefix_nil|]. right. intro N. inversion N.
- destruct (IHl' l).
+ left. econstructor;eauto.
+ destruct (list_eqdec H l (a :: l')).
* left. rewrite e. econstructor.
* right. contradict c. inversion c.
-- intro N. eapply N. reflexivity.
-- eauto.
Qed.
Lemma prefix_antisym (l l' : list A)
(H : prefix l l')
(Q : prefix l' l)
: l = l'.
Proof.
eapply prefix_eq in H.
eapply prefix_eq in Q.
do 2 destructH.
rewrite Q in H.
rewrite app_assoc in H.
induction (l2'0 ++ l2') eqn:E.
- destruct l2'0.
+ cbn in E. rewrite E in Q. cbn in Q. eauto.
+ cbn in E. congruence.
- exfalso. cbn in H. clear - H.
revert dependent a. revert l0. induction l';intros.
+ congruence.
+ destruct l0;cbn in H.
* inversion H. subst. eapply IHl'. instantiate (1:=nil). cbn. eapply H2.
* inversion H. subst. eapply IHl'. rewrite app_cons_assoc in H2.
eapply H2.
Qed.
Lemma prefix_cons_cons (a a' : A) l l' :
prefix (a :: l) (a' :: l') -> prefix l l'.
Proof.
intros H. dependent induction H; cbn.
- econstructor.
- destruct l'.
+ inversion H.
+ econstructor. eapply IHprefix; eauto.
Qed.
Lemma prefix_nincl_prefix' `{EqDec A eq} (l : list A) a
: prefix (prefix_nincl a l) l.
Proof.
induction l;cbn;eauto.
- econstructor.
- destruct (a == a0).
+ econstructor. econstructor.
+ econstructor. eauto.
Qed.
End Pre.
Lemma suffix_map {A B : Type} (f : A -> B) :
forall l l', suffix l l' -> suffix (map f l) (map f l').
Proof.
intros ? ? Hpost.
induction Hpost;[econstructor|rewrite map_rcons;econstructor;assumption].
Qed.
Lemma prefix_map_fst (A B : Type) (l l' : list (A * B))
(Hpre: prefix l l')
: prefix (map fst l) (map fst l').
Proof.
induction Hpre.
- econstructor.
- destruct a. cbn. econstructor;eauto.
Qed.
Lemma suffix_map_fst (A B : Type) (l l' : list (A * B))
(Hpre: suffix l l')
: suffix (map fst l) (map fst l').
Proof.
eapply prefix_rev_suffix'.
do 2 rewrite <-map_rev.
eapply prefix_map_fst.
eapply suffix_rev_prefix;eauto.
Qed.
Lemma prefix_len_leq (A : Type) (l l' : list A)
(Hpre : prefix l l')
: | l | <= | l' |.
Proof.
induction Hpre;cbn;eauto.
Qed.
Lemma in_suffix_in {A : Type} l l' (a : A)
: a ∈ l -> suffix l l' -> a ∈ l'.
Proof.
intros Hin Hpost.
revert dependent l.
induction l'.
- intros. eapply suffix_nil_nil in Hpost. subst. inversion Hin.
- intros.
destruct l as [| b l].
+ inversion Hin.
+ simpl in Hin.
destruct Hin.
* left. symmetry. rewrite H in Hpost. eauto using suffix_hd_eq.
* right. eauto using cons_suffix.
Qed.
Lemma prefix_fst_prefix {S T : Type} (a b : list (S * T))
(Hprefix: prefix a b)
: prefix (map fst a) (map fst b).
Proof.
induction Hprefix.
- econstructor.
- simpl. econstructor. eauto.
Qed.
Lemma prefix_cycle (A : Type) (l : list A) a
: prefix (a :: l) l -> False.
Proof.
revert a.
induction l;cbn;intros.
- inversion H.
- inversion H.
+ exfalso;eapply list_cycle;eauto.
+ eapply prefix_cons in H2. eauto.
Qed.
Lemma prefix_length_le {A : Type} (l1 l2 : list A)
: prefix l1 l2 -> | l1 | <= | l2 |.
Proof.
intros H.
induction H.
- econstructor.
- cbn. lia.
Qed.
Lemma prefix_app_r {X : Type} (l1 l2 l3 : list X)
: prefix l1 l3 -> prefix l1 (l2 ++ l3).
Proof.
induction l2;cbn;intros.
- assumption.
- econstructor.
eapply IHl2;eauto.
Qed.
Definition infix {X : Type} (l l' : list X)
:= exists l0 l2, l' = l2 ++ l ++ l0.
Require Export ListExtra.
From Coq Require Import Classes.EquivDec.
Import ListNotations.
From Coq Require Import Decidable.
From HyPre Require Import Tac.
Notation "x ⊆ y" := (incl x y) (at level 50).
Inductive prefix {A : Type} : list A -> list A -> Prop :=
| PreSame l : prefix l l
| PreStep {a l l'} : prefix l l' -> prefix l (a :: l').
Lemma prefix_cons_in {A : Type} `{EqDec A eq} (a : A) l l' : prefix (a :: l) l' -> In a l'.
Proof.
intro Q. revert dependent l. induction l'; cbn in *; intros l Q.
- inversion Q.
- destruct (a == a0).
+ auto.
+ inversion Q; subst.
* exfalso; apply c; reflexivity.
* eauto.
Qed.
Inductive suffix {A : Type} : list A -> list A -> Prop :=
| SufSame l : suffix l l
| SufStep {a l l'} : suffix l l' -> suffix l (l' :r: a).
Fixpoint prefix_nincl {A : Type} `{EqDec A eq} (a : A) (l : list A) : list A :=
match l with
| nil => nil
| b :: l => if a == b then l else prefix_nincl a l
end.
Lemma prefix_nincl_prefix {A : Type} `{EqDec A eq} (a : A) l :
In a l -> prefix (a :: prefix_nincl a l) l.
Proof.
intros Q.
induction l; cbn;
inversion Q.
- subst a0. destruct (a == a); [|exfalso; apply c; reflexivity].
econstructor.
- destruct (a == a0).
+ destruct e. econstructor.
+ econstructor. eauto.
Qed.
Lemma prefix_cons {A : Type} (l l' : list A) :
forall a, prefix (a :: l) l' -> prefix l l'.
Proof.
intros a H. dependent induction H.
- econstructor. econstructor.
- econstructor. eapply IHprefix; eauto.
Qed.
Lemma prefix_trans {A : Type} (l1 l2 l3 : list A) :
prefix l1 l2 -> prefix l2 l3 -> prefix l1 l3.
Proof.
revert l1 l3. induction l2; intros l1 l3 pre1 pre2; inversion pre1; inversion pre2; subst; eauto.
econstructor. eapply IHl2; eauto. eapply prefix_cons; eauto.
Qed.
Global Instance prefix_Transitive (A : Type) : Transitive (@prefix A).
Proof.
unfold Transitive.
eapply prefix_trans.
Qed.
Lemma in_prefix_in {A : Type} `{EqDec A eq} (a : A) l l' :
In a l -> prefix l l' -> In a l'.
Proof.
intros Hin Hpre. induction l.
- inversion Hin.
- destruct (a == a0).
+ destruct e. eapply prefix_cons_in; eauto.
+ eapply IHl; eauto.
* destruct Hin; [exfalso; subst; apply c; reflexivity|assumption].
* eapply prefix_cons; eauto.
Qed.
Fixpoint suffix_nincl {A : Type} `{EqDec A eq} (a : A) (l : list A) : list A :=
match l with
| nil => nil
| b :: l => if a == b then nil else b :: suffix_nincl a l
end.
Lemma suffix_nil {A : Type} (l : list A) : suffix nil l.
apply rcons_ind; [econstructor|].
intros. econstructor; eauto.
Qed.
Ltac rinduction L := revert dependent L; intro L; eapply rcons_ind with (l:=L); intros.
Lemma suffix_cons {A : Type} a (l l': list A) :
suffix l l' -> suffix (a :: l) (a :: l').
Proof.
intros post.
- induction post.
+ econstructor.
+ rewrite <-cons_rcons_assoc. econstructor. assumption.
Qed.
Lemma suffix_eq {A : Type} (l1 l2 : list A) :
suffix l1 l2 <-> exists l2', l2 = l1 ++ l2'.
Proof.
split.
- intro post. induction post.
+ exists nil. apply app_nil_end.
+ destruct IHpost as [l2' IH].
exists (l2' :r: a). rewrite IH. rewrite app_assoc. reflexivity.
- intros [l2' H]. subst l2.
rinduction l2'.
+ rewrite <-app_nil_end. econstructor.
+ rewrite app_assoc. econstructor. eauto.
Qed.
Lemma cons_suffix {A : Type} a b (l l': list A) :
suffix (a :: l) (b :: l') -> suffix l l'.
Proof.
intros post. apply suffix_eq. apply suffix_eq in post as [l1' leq].
exists l1'. inversion leq. reflexivity.
Qed.
Lemma suffix_app {A : Type} (l1 l2 l' : list A) :
suffix (l' ++ l1) (l' ++ l2) -> suffix l1 l2.
Proof.
revert l1 l2. induction l'; intros; cbn; eauto.
apply IHl'. cbn in H. inversion H.
- rewrite H2. econstructor.
- eapply cons_suffix; eauto.
Qed.
Lemma suffix_nincl_suffix {A : Type} `{EqDec A eq} a l : suffix (suffix_nincl a l) l.
Proof.
induction l; cbn; [econstructor; reflexivity|].
destruct (a == a0); cbn; eauto using suffix_nil, suffix_cons.
Qed.
Lemma suffix_nil_nil {A : Type} (l : list A) :
suffix l nil -> l = nil.
Proof.
intro H. inversion H; eauto. destruct l'; cbn in H0; congruence.
Qed.
Lemma prefix_nil_nil {A : Type} (l : list A) :
prefix l nil -> l = nil.
Proof.
intro H. inversion H; eauto.
Qed.
Lemma suffix_rcons_nil_eq {A : Type} l (a b : A) :
suffix (l :r: a) (b :: nil) -> a = b /\ l = nil.
Proof.
intros post. apply suffix_eq in post as [l2' post]. destruct l; cbn in *; eauto.
- inversion post; eauto.
- inversion post. destruct l; cbn in H1; congruence.
Qed.
Lemma suffix_nincl_spec {A : Type} `{EqDec A eq} (a : A) l :
In a l -> suffix (suffix_nincl a l :r: a) l.
Proof.
intros ina.
induction l; inversion ina.
- subst a0. cbn. destruct equiv_dec;[|exfalso; apply c; reflexivity].
cbn. apply suffix_cons, suffix_nil.
- cbn. destruct equiv_dec; cbn.
+ destruct e; apply suffix_cons, suffix_nil.
+ apply suffix_cons. eauto.
Qed.
Lemma suffix_nincl_invariant {A : Type} `{EqDec A eq} (a : A) l :
~ In a l -> suffix_nincl a l = l.
Proof.
intros nin.
induction l; cbn; eauto.
destruct equiv_dec.
- destruct e. exfalso. apply nin. econstructor; eauto.
- rewrite IHl; eauto. contradict nin. econstructor 2; eauto.
Qed.
Lemma suffix_incl {A : Type} (l l' : list A) : suffix l l' -> incl l l'.
Proof.
intros post. induction post.
- apply incl_refl.
- apply incl_appl; eauto.
Qed.
Lemma suffix_hd_eq (A : Type) (a b : A) l l' :
suffix (a :: l) (b :: l') -> a = b.
Proof.
intro post. eapply suffix_eq in post as [l2' pst].
cbn in pst. inversion pst. eauto.
Qed.
Lemma suffix_order_destruct' {A : Type} (l1 l2 l3 : list A) :
suffix l1 l3 -> suffix l2 l3 -> length l1 <= length l2 -> suffix l1 l2.
Proof.
revert l1 l3. induction l2; intros l1 l3 post1 post2 len; cbn in *.
- destruct l1; cbn in len; [econstructor|lia].
- destruct l1; [eapply suffix_nil|].
destruct l3; [eapply suffix_nil_nil in post1; congruence|].
eapply suffix_hd_eq in post1 as aeq. destruct aeq.
eapply suffix_hd_eq in post2 as aeq. destruct aeq.
eapply suffix_cons, IHl2. 1,2: eapply cons_suffix; eauto. cbn in len. lia.
Qed.
Lemma suffix_order_destruct {A : Type} (l1 l2 l3 : list A) :
suffix l1 l3 -> suffix l2 l3 -> suffix l1 l2 \/ suffix l2 l1.
Proof.
intros post1 post2.
destruct (Nat.ltb (length l1) (length l2)) eqn:H.
- left. eapply suffix_order_destruct'; eauto. eapply PeanoNat.Nat.ltb_lt in H. lia.
- right. eapply suffix_order_destruct'; eauto. eapply PeanoNat.Nat.ltb_nlt in H. lia.
Qed.
Lemma suffix_step_left {A : Type} (l l' : list A) a :
suffix (l :r: a) l' -> suffix l l'.
Proof.
intros.
remember (l :r: a) as l0.
induction H. subst l0.
- econstructor. econstructor.
- econstructor; eauto.
Qed.
Lemma suffix_length {A : Type} (l l' : list A) :
suffix l l' -> length l <= length l'.
Proof.
intros post. induction post.
- reflexivity.
- rewrite length_rcons. rewrite IHpost. lia.
Qed.
Lemma suffix_order {A : Type} (l1 l2 l' : list A) (a : A) :
~ In a l1 -> In a l2 -> suffix l1 l' -> suffix l2 l' -> suffix l1 l2.
Proof.
intros nin1 in2 pst1 pst2. eapply suffix_order_destruct'; eauto.
eapply suffix_order_destruct in pst1; eauto. clear pst2.
destruct pst1.
{ exfalso. apply suffix_incl in H. firstorder. }
apply suffix_length; eauto.
Qed.
Lemma suffix_elem {A : Type} `{EqDec A eq} (a:A) l l':
length l > 0 -> suffix l (a :: l') -> In a l.
Proof.
intros len post.
destruct l.
{ cbn in len; lia. }
eapply suffix_hd_eq in post.
subst a0. econstructor; eauto.
Qed.
Lemma suffix_trans {A : Type} (l l' l'': list A) :
suffix l l' -> suffix l' l'' -> suffix l l''.
Proof.
intros post1; revert l''.
induction post1; intros l'' post2.
- induction post2; econstructor; eauto.
- apply IHpost1. eapply suffix_step_left; eauto.
Qed.
Lemma suffix_nincl_nincl {A : Type} `{EqDec A eq} (a : A) l :
~ In a (suffix_nincl a l).
Proof.
induction l; cbn; eauto. destruct (a == a0).
- tauto.
- contradict IHl. inversion IHl.
+ subst a0. exfalso; apply c; reflexivity.
+ assumption.
Qed.
Definition prefix_incl : forall (A : Type) (l l' : list A), prefix l l' -> l ⊆ l'
:= fun (A : Type) (l l' : list A) (post : prefix l l') =>
@prefix_ind A (fun l0 l'0 : list A => l0 ⊆ l'0) (fun l0 : list A => incl_refl l0)
(fun (a : A) (l0 l'0 : list A) (_ : prefix l0 l'0) (IHpost : l0 ⊆ l'0) =>
incl_appr (a :: nil) IHpost) l l' post.
Lemma prefix_in_list {A : Type} l (a:A) :
In a l
-> exists l', prefix (a :: l') l.
Proof.
intro Hin.
induction l.
- inversion Hin.
- destruct Hin;[subst;exists l; cbn;econstructor|].
eapply IHl in H. destruct H as [l' H]. exists l'. cbn; econstructor; assumption.
Qed.
Lemma prefix_nil {A : Type} (l : list A) : prefix nil l.
Proof.
induction l; econstructor; firstorder.
Qed.
Lemma prefix_NoDup {A : Type} (l l' : list A) : prefix l l' -> NoDup l' -> NoDup l.
Proof.
intros Hpre Hnd. induction Hpre; eauto.
inversion Hnd; subst; eauto.
Qed.
Section Pre.
Variable A : Type.
Lemma prefix_eq :
forall (l1 l2 : list A), prefix l1 l2 <-> (exists l2' : list A, l2 = l2' ++ l1).
Proof.
intros.
split;intros.
- induction H.
+ exists nil; cbn; eauto.
+ destructH. exists (a :: l2'). cbn. f_equal;eauto.
- destructH. rewrite H.
revert dependent l2.
induction l2'; intros;cbn;econstructor;eauto.
Qed.
Lemma prefix_length `{EqDec A eq} (l1 l2 : list A)
(Hpre : prefix l1 l2)
(Hlen : length l1 = length l2)
: l1 = l2.
Proof.
eapply prefix_eq in Hpre. destructH. subst l2.
destruct l2';cbn in *; eauto.
exfalso.
rewrite app_length in Hlen. lia.
Qed.
Lemma prefix_rev_suffix (l l' : list A)
(Hpre : prefix l l')
: suffix (rev l) (rev l').
Proof.
induction Hpre.
- econstructor.
- rewrite rev_cons. econstructor;eauto.
Qed.
Lemma prefix_rev_suffix' (l l' : list A)
(Hpre : prefix (rev l) (rev l'))
: suffix l l'.
Proof.
rewrite <-(rev_involutive l).
rewrite <-(rev_involutive l').
eapply prefix_rev_suffix;eauto.
Qed.
Lemma suffix_rev_prefix (l l' : list A)
(Hpost : suffix l l')
: prefix (rev l) (rev l').
Proof.
induction Hpost.
- econstructor.
- rewrite rev_rcons. econstructor;eauto.
Qed.
Lemma suffix_rev_prefix' (l l' : list A)
(Hpost : suffix (rev l) (rev l'))
: prefix l l'.
Proof.
rewrite <-(rev_involutive l).
rewrite <-(rev_involutive l').
eapply suffix_rev_prefix;eauto.
Qed.
Lemma prefix_order_destruct
: forall l3 l4 l5 : list A, prefix l3 l5 -> prefix l4 l5 -> prefix l3 l4 \/ prefix l4 l3.
Proof.
intros.
eapply prefix_rev_suffix in H. eapply prefix_rev_suffix in H0.
eapply suffix_order_destruct in H;eauto.
destruct H;[right|left]; eapply suffix_rev_prefix';eauto.
Qed.
Lemma prefix_length_eq `{EqDec A eq} (l1 l2 l : list A)
(Hlen : length l1 = length l2)
(Hpre1 : prefix l1 l)
(Hpre2 : prefix l2 l)
: l1 = l2.
Proof.
eapply prefix_order_destruct in Hpre1 as Hor;eauto.
destruct Hor as [Hor|Hor]; eapply prefix_length in Hor; eauto; symmetry; eauto.
Qed.
Lemma prefix_induction {P : list A -> Prop}
: P nil
-> (forall (a : A) (l : list A) (l' : list A), P l' -> prefix (a :: l') l -> P l)
-> forall l : list A, P l.
Proof.
intros Hbase Hstep l. induction l;eauto.
eapply Hstep;eauto. econstructor.
Qed.
Lemma prefix_ex_cons (l l' : list A) (a : A)
: prefix l l' -> exists a', prefix (a' :: l) (a :: l').
Proof.
intros Hpre. revert a. induction Hpre; intros b.
- exists b. econstructor.
- specialize (IHHpre a). destructH. eexists. econstructor. eauto.
Qed.
Lemma suffix_ex_cons
: forall (l l' : list A) (a : A), suffix l l' -> exists a' : A, suffix (l :r: a') (l' :r: a).
Proof.
intros. eapply suffix_rev_prefix in H. eapply prefix_ex_cons in H. destructH.
exists a'. eapply prefix_rev_suffix'. do 2 rewrite rev_rcons. eauto.
Qed.
Lemma rcons_inj (l l' : list A) (a b : A)
: l ++ [a] = l' ++ [b] -> l = l' /\ a = b.
Proof.
revert dependent l'.
induction l;intros.
- cbn in H. destruct l';cbn in *;eauto.
+ split;inversion H;eauto.
+ inversion H. congruence'.
- destruct l';cbn in *.
+ inversion H. congruence'.
+ inversion H. subst. split;[f_equal|];eapply IHl;eauto.
Qed.
Lemma suffix_rcons_rcons (l l' : list A) (a a' : A)
: suffix (l ++ [a]) (l' ++ [a']) -> suffix l l'.
Proof.
intros Hpost.
eapply suffix_eq in Hpost. destructH.
revert dependent a. revert a' l.
induction l2';intros.
- rewrite app_nil_r in Hpost. eapply rcons_inj in Hpost. destructH. subst. constructor.
- eapply suffix_step_left. eapply IHl2'. rewrite <-app_cons_assoc. eauto.
Qed.
Lemma tl_prefix (l : list A)
: prefix (tl l) l.
Proof.
induction l;cbn;econstructor;eauto. econstructor.
Qed.
Lemma prefix_tl (l l' : list A) (a : A)
: prefix (a :: l) l' -> prefix l (tl l').
Proof.
clear. intros. inversion H;subst;cbn.
- econstructor.
- eapply prefix_cons;eauto.
Qed.
Lemma prefix_rcons (l l' : list A) (a : A)
(Hpref : prefix l l')
: prefix (l :r: a) (l' :r: a).
Proof.
clear - Hpref.
revert dependent l.
induction l';intros l Hpref;cbn.
- destruct l;cbn.
+ econstructor.
+ inversion Hpref.
- inversion Hpref;subst.
+ cbn. econstructor.
+ econstructor. eapply IHl';eauto.
Qed.
Lemma suffix_firstn (l l' : list A)
: firstn ( |l'| ) l = l' <-> suffix l' l.
Proof.
split; intro H.
- rewrite <-H.
remember (|l'|) as n. clear.
revert l. induction n.
+ cbn. eapply suffix_nil.
+ intros l. destruct l.
* cbn. econstructor;auto.
* cbn. eapply suffix_cons;eauto.
- revert dependent l. induction l';intros;cbn;auto.
destruct l. 1: inversion H;congruence'.
f_equal.
+ symmetry;eapply suffix_hd_eq;eauto.
+ eapply IHl'. eapply cons_suffix;eauto.
Qed.
Lemma prefix_lastn (l l' : list A)
: lastn ( |l'| ) l = l' <-> prefix l' l.
Proof.
split; intro H.
- eapply suffix_rev_prefix'.
eapply suffix_firstn.
eapply rev_rev_eq.
rewrite rev_involutive.
rewrite rev_length.
unfold lastn in H.
assumption.
- eapply prefix_rev_suffix in H.
eapply suffix_firstn in H.
eapply rev_rev_eq in H.
rewrite rev_involutive in H.
rewrite rev_length in H.
unfold lastn.
assumption.
Qed.
Global Instance prefix_Reflexive : Reflexive (@prefix A).
Proof.
econstructor.
Qed.
Global Instance suffix_Reflexive : Reflexive (@suffix A).
Proof.
econstructor.
Qed.
Lemma prefix_dec (B : Type) `{EqDec B eq} (l l' : list B) : decidable (prefix l l').
Proof.
revert l;induction l';intros l.
- destruct l;[left; eapply prefix_nil|]. right. intro N. inversion N.
- destruct (IHl' l).
+ left. econstructor;eauto.
+ destruct (list_eqdec H l (a :: l')).
* left. rewrite e. econstructor.
* right. contradict c. inversion c.
-- intro N. eapply N. reflexivity.
-- eauto.
Qed.
Lemma prefix_antisym (l l' : list A)
(H : prefix l l')
(Q : prefix l' l)
: l = l'.
Proof.
eapply prefix_eq in H.
eapply prefix_eq in Q.
do 2 destructH.
rewrite Q in H.
rewrite app_assoc in H.
induction (l2'0 ++ l2') eqn:E.
- destruct l2'0.
+ cbn in E. rewrite E in Q. cbn in Q. eauto.
+ cbn in E. congruence.
- exfalso. cbn in H. clear - H.
revert dependent a. revert l0. induction l';intros.
+ congruence.
+ destruct l0;cbn in H.
* inversion H. subst. eapply IHl'. instantiate (1:=nil). cbn. eapply H2.
* inversion H. subst. eapply IHl'. rewrite app_cons_assoc in H2.
eapply H2.
Qed.
Lemma prefix_cons_cons (a a' : A) l l' :
prefix (a :: l) (a' :: l') -> prefix l l'.
Proof.
intros H. dependent induction H; cbn.
- econstructor.
- destruct l'.
+ inversion H.
+ econstructor. eapply IHprefix; eauto.
Qed.
Lemma prefix_nincl_prefix' `{EqDec A eq} (l : list A) a
: prefix (prefix_nincl a l) l.
Proof.
induction l;cbn;eauto.
- econstructor.
- destruct (a == a0).
+ econstructor. econstructor.
+ econstructor. eauto.
Qed.
End Pre.
Lemma suffix_map {A B : Type} (f : A -> B) :
forall l l', suffix l l' -> suffix (map f l) (map f l').
Proof.
intros ? ? Hpost.
induction Hpost;[econstructor|rewrite map_rcons;econstructor;assumption].
Qed.
Lemma prefix_map_fst (A B : Type) (l l' : list (A * B))
(Hpre: prefix l l')
: prefix (map fst l) (map fst l').
Proof.
induction Hpre.
- econstructor.
- destruct a. cbn. econstructor;eauto.
Qed.
Lemma suffix_map_fst (A B : Type) (l l' : list (A * B))
(Hpre: suffix l l')
: suffix (map fst l) (map fst l').
Proof.
eapply prefix_rev_suffix'.
do 2 rewrite <-map_rev.
eapply prefix_map_fst.
eapply suffix_rev_prefix;eauto.
Qed.
Lemma prefix_len_leq (A : Type) (l l' : list A)
(Hpre : prefix l l')
: | l | <= | l' |.
Proof.
induction Hpre;cbn;eauto.
Qed.
Lemma in_suffix_in {A : Type} l l' (a : A)
: a ∈ l -> suffix l l' -> a ∈ l'.
Proof.
intros Hin Hpost.
revert dependent l.
induction l'.
- intros. eapply suffix_nil_nil in Hpost. subst. inversion Hin.
- intros.
destruct l as [| b l].
+ inversion Hin.
+ simpl in Hin.
destruct Hin.
* left. symmetry. rewrite H in Hpost. eauto using suffix_hd_eq.
* right. eauto using cons_suffix.
Qed.
Lemma prefix_fst_prefix {S T : Type} (a b : list (S * T))
(Hprefix: prefix a b)
: prefix (map fst a) (map fst b).
Proof.
induction Hprefix.
- econstructor.
- simpl. econstructor. eauto.
Qed.
Lemma prefix_cycle (A : Type) (l : list A) a
: prefix (a :: l) l -> False.
Proof.
revert a.
induction l;cbn;intros.
- inversion H.
- inversion H.
+ exfalso;eapply list_cycle;eauto.
+ eapply prefix_cons in H2. eauto.
Qed.
Lemma prefix_length_le {A : Type} (l1 l2 : list A)
: prefix l1 l2 -> | l1 | <= | l2 |.
Proof.
intros H.
induction H.
- econstructor.
- cbn. lia.
Qed.
Lemma prefix_app_r {X : Type} (l1 l2 l3 : list X)
: prefix l1 l3 -> prefix l1 (l2 ++ l3).
Proof.
induction l2;cbn;intros.
- assumption.
- econstructor.
eapply IHl2;eauto.
Qed.
Definition infix {X : Type} (l l' : list X)
:= exists l0 l2, l' = l2 ++ l ++ l0.
Strictprefix
Section StrictPre.
Variable (A : Type).
Definition Strictprefix' :=
fun (l l' : list A) => exists a : A, prefix (a :: l) l'.
Lemma prefix_strictprefix:
forall (e : A) (x ϕ : list A), prefix ϕ x -> Strictprefix' ϕ (e :: x).
Proof.
intros e x ϕ Hϕ1.
unfold Strictprefix'. cbn.
revert dependent e.
induction Hϕ1; intros.
- exists e; econstructor.
- specialize(IHHϕ1 a). destructH. exists a0. econstructor. auto.
Qed.
Lemma Strictprefix_well_founded : well_founded (Strictprefix').
Proof.
unfold well_founded.
intros.
induction a.
- econstructor. intros. unfold Strictprefix' in *. destructH. inversion H.
- constructor. intros.
unfold Strictprefix' in H.
destructH. cbn in *. inversion H;subst.
+ subst. auto.
+ eapply IHa. unfold Strictprefix'. exists a1. cbn. auto.
Qed.
End StrictPre.