# UniAna.infra.LastCommon

Require Import LastCommonTac DecTac Lia.

Section Lc.

Variable A : Type.

Lemma rcons_eq (a a' : A) l l' :
a = a' /\ l = l' <-> l :r: a = l' :r: a'.
Proof.
split.
- destruct (rcons_destruct l); intros; destruct H0; subst; reflexivity.
- intros. revert dependent l'.
induction l; induction l'; intros Heq; inversion Heq.
+ split; reflexivity.
+ congruence'.
+ congruence'.
+ specialize (IHl l' H1) as [aeq leq].
split; subst; reflexivity.
Qed.

Lemma postfix_first_occ_eq `{EqDec A eq} (l1 l2 l3 : list A) (a : A) :
~ In a l1 -> ~ In a l2 -> Postfix (l1 :r: a) l3 -> Postfix (l2 :r: a) l3
-> l1 = l2.
Proof.
intros in1 in2. intros.
assert (Postfix l1 (l2 :r: a)) as po1.
{
eapply postfix_order; eauto.
- eapply postfix_step_left; eauto.
}
assert (Postfix l2 (l1 :r: a)) as po2.
{
eapply postfix_order; eauto.
- eapply postfix_step_left; eauto.
}
revert dependent l2.
revert dependent l3.
induction l1; intros l3 post1 l2 in2 post2 po1 po2.
- cbn in post1.
apply postfix_incl in po2. clear - in2 po2.
destruct l2; eauto. specialize (po2 a0).
assert (In a0 (a :: nil)) as po' by (apply po2; econstructor; eauto).
inversion po'.
+ subst a. exfalso. apply in2. econstructor; eauto.
+ inversion H.
- destruct l2.
+ cbn in post2.
apply postfix_incl in po1. clear - in1 po1.
specialize (po1 a0).
assert (In a0 (a :: nil)) as po' by (apply po1; econstructor; eauto).
inversion po'.
* subst a. exfalso. apply in1. econstructor; eauto.
* inversion H.
+ rewrite cons_rcons_assoc in post1, post2.
eapply postfix_hd_eq in po1 as hd_eq1. subst a0.
assert (exists l3', l3 = a1 :: l3') as [l3' leq3].
{
destruct l3.
- cbn in post2. eapply postfix_nil_nil in post2. cbn in post2. congruence.
- exists l3. apply postfix_hd_eq in post1. subst a1. reflexivity.
}
subst l3.
erewrite IHl1 with (l2:=l2); eauto.
(* contradict in1. right. eauto.*)
* eapply cons_postfix; eauto.
(* contradict in2. right. eauto.*)
* eapply cons_postfix; eauto.
* rewrite cons_rcons_assoc in po1. eapply cons_postfix; eauto.
* rewrite cons_rcons_assoc in po1. eapply cons_postfix; eauto.
Qed.

Definition last_common `{EqDec A eq} (l1 l2 : list A) (s : A) :=
exists l1' l2', Postfix (l1' :r: s) l1 /\ Postfix (l2' :r: s) l2
/\ Disjoint l1' l2'
/\ ~ In s l1' /\ ~ In s l2'.

Definition last_common' `{EqDec A eq} (l1 l2 l1' l2' : list A) (s : A)
:= Postfix (l1' :r: s) l1 /\ Postfix (l2' :r: s) l2 /\ Disjoint l1' l2' /\ s l1' /\ s l2'.

Lemma last_common'_iff `(EqDec A eq) l1 l2 (a : A)
: last_common l1 l2 a <-> exists l1' l2', last_common' l1 l2 l1' l2' a.
Proof.
unfold last_common, last_common' in *. firstorder.
Qed.

Lemma last_common'_sym `{EqDec A eq} (l1 l2 l1' l2' : list A) (a : A)
(Hlc : last_common' l1' l2' l1 l2 a)
: last_common' l2' l1' l2 l1 a.
Proof.
unfold last_common' in *. destructH.
split_conj;eauto.
eapply Disjoint_sym. auto.
Qed.

Require Import ListOrder.

Lemma ne_last_common `{EqDec A eq} (l1 l2 : list A) (a : A) :
exists s, last_common (l1 ++ [a]) (l2 ++ [a]) s.
Proof.
unfold last_common.

(*    revert l2.
induction l1; intros l2.
- admit.
- specialize (IHl1 l2). destructH.
exists s, (a0 :: l1'), l2'. split_conj;eauto.
+ cbn. eapply postfix_cons. eauto.
+ admit. (* nope *)
+ *)

revert l2.
induction l1; intros l2; induction l2; cbn in *.
- exists a; exists nil; exists nil; cbn.
prove_last_common.
- exists a. exists nil.
destruct IHl2 as [s [l1' [l2' [post [post' [disj [in1 in2]]]]]]]. cbn.
destruct (a == a0).
+ destruct e. exists nil. prove_last_common.
+ exists (a0 :: l2'). prove_last_common.
- exists a. specialize (IHl1 nil).
destruct IHl1 as [s [l1' [l2' [post [post' [disj [in1 in2]]]]]]].
destruct (a == a0).
+ destruct e. exists nil, nil. cbn. prove_last_common.
+ exists ((a0 :: l1')), nil. cbn in post'. prove_last_common.
- specialize (IHl1 (a1 :: l2)).
rename a1 into a2. rename a0 into a1.

destruct IHl1 as [s1 [l11 [l12 [post11 [post12 [disj1 [in11 in12]]]]]]].
destruct IHl2 as [s2 [l21 [l22 [post21 [post22 [disj2 [in21 in22]]]]]]].

destruct (s1 == a2).
+ destruct e. exists s1. destruct (a1 == s1).
* destruct e. exists nil. exists nil. prove_last_common.
* exists ((a1 :: l11)). exists nil. prove_last_common.
+ destruct (s2 == a1).
* destruct e. exists s2, nil. destruct (s2 == a2).
-- destruct e. exists nil. prove_last_common.
-- exists ((a2 :: l22)). prove_last_common.
* destruct (a1 == a2).
-- destruct e. exists a1, nil, nil. prove_last_common.
-- (*destruct l12 as |b l12.
{ cbn in post12. eapply postfix_hd_eq in post12. subst. exfalso. apply c. reflexivity. }
replace b with a2 in *.  2: (cbn in post12; symmetry; eapply postfix_hd_eq;eauto).
clear b.
destruct l21 as |b l21.
{ cbn in post21. eapply postfix_hd_eq in post21. subst. exfalso. apply c0. reflexivity. }
replace b with a1 in *. 2: cbn in post21;symmetry; eapply postfix_hd_eq;eauto. clear b.*)

destruct (In_dec _ s1 l22).
++ exists s1, (a1 :: l11), l12. split_conj.
** prove_last_common.
** prove_last_common.
** apply disjoint_cons1. split; auto.

assert (Postfix l12 (a2 :: l22)).
{
eapply postfix_order with (a0:=s1); eauto.
(*- econstructor 2; eauto.*)
- eapply postfix_step_left; eauto.
- cbn. apply postfix_cons. eapply postfix_step_left; eauto.
}
apply postfix_incl in H1. apply id in disj2 as disj2'.
unfold Disjoint in disj2'.
unfold incl in H1. intro In12. apply H1 in In12. cbn in In12.
destruct In12 as [In12|In12]; [subst a1; apply c1; reflexivity|].
clear disj2.
assert (a1 l21) as disj2.
{ intro N. eapply disj2'. eauto. eapply In12. }
apply disj2. apply postfix_elem in post21; eauto.
--- eapply In_rcons in post21.
destruct post21; [subst a1; exfalso; apply c0; reflexivity|assumption].
--- destruct l21; cbn. lia. rewrite app_length. lia.
** assert (s1 =/= a1) as sa.
{
intro N. destruct N. apply postfix_elem in post21.
apply In_rcons in post21.
- destruct post21; [subst s1; apply c0; reflexivity|].
clear - disj2 H0 H1. firstorder.
- destruct l21; cbn. lia. rewrite app_length. lia.
}
prove_last_common.
** assumption.
++ destruct (s1 == s2) as [seq|sneq].
{
(*                  destruct l12 as |b l12.
{ cbn in post12. eapply postfix_hd_eq in post12. subst.
exfalso. apply c. reflexivity. }
replace b with a2 in *.  2: (cbn in post12; symmetry; eapply postfix_hd_eq;eauto).
clear b.
destruct l21 as |b l21.
{ cbn in post21. eapply postfix_hd_eq in post21. subst.
exfalso. apply c0. reflexivity. }
replace b with a1 in *. 2: cbn in post21;symmetry; eapply postfix_hd_eq;eauto.
clear b.*)

destruct seq.
assert (l21 = a1 :: l11 /\ l12 = a2 :: l22) as [lleq1 lleq2].
{
split.
- eapply postfix_first_occ_eq; eauto.
+ contradict in11. inversion in11.
* subst a1; exfalso; apply c0; reflexivity.
* eauto.
+ rewrite cons_rcons_assoc. apply postfix_cons. eauto.
- eapply postfix_first_occ_eq; eauto.
+ contradict in22. inversion in22.
* subst a2; exfalso; apply c; reflexivity.
* eauto.
+ rewrite cons_rcons_assoc. apply postfix_cons. eauto.
}
subst l12 l21.
exists s1, (a1 :: l11), (a2 :: l22).
split_conj.
- prove_last_common.
- prove_last_common.
- eapply disjoint_cons1. split; eauto.
eapply disjoint1 in disj2.
destruct (disj2) as [disj2' _].
cbn in disj2'. specialize (disj2' _ (or_introl eq_refl)).
contradict disj2'. cbn in disj2'.
destruct disj2'; [subst a2; exfalso; apply c1; reflexivity|eauto].
- eauto.
- eauto.
}
destruct (In_dec _ a2 (l21 :r: s2)) as [in_a0|nin_a0].
{
exists a2, (postfix_nincl a2 l21), nil.
split_conj.
- apply In_rcons in in_a0. destruct in_a0.
+ subst a2.
apply postfix_nincl_invariant in in21. rewrite in21. eauto.
+ eapply postfix_nincl_spec in H1.
eapply postfix_trans; eauto. eapply postfix_step_left; eauto.
- prove_last_common.
- prove_last_common.
- apply postfix_nincl_nincl.
- tauto.
}
exists s2, l21, (a2 :: l22).
split_conj.
** prove_last_common.
** prove_last_common.
** apply disjoint_cons2. split; eauto.
** assumption.
** assert (s2 =/= a2) as sa.
{
intro N. destruct N. apply nin_a0.
apply In_rcons. left. reflexivity.
}
prove_last_common.
Qed.

Lemma last_common_sym `{EqDec A eq} (l l' : list A) a
(Hlc : last_common l l' a)
: last_common l' l a.
Proof.
unfold last_common in *; firstorder.
Qed.

Lemma last_common_singleton1 `{EqDec A eq} (s a : A) l
(Hlc : last_common (a :: nil) l s)
: a = s.
Proof.
unfold last_common in Hlc. destructH. eapply postfix_rcons_nil_eq in Hlc0. firstorder.
Qed.

Lemma last_common_singleton2 `{EqDec A eq} (s a : A) l
(Hlc : last_common l (a :: nil) s)
: a = s.
Proof.
unfold last_common in Hlc. destructH. eapply postfix_rcons_nil_eq in Hlc2. firstorder.
Qed.

(* currently not used ! *)
Lemma last_common_app_eq1 `{EqDec A eq} (l1 l2 l1' l2' : list A) x
(Hlc : last_common' l1 l2 l1' l2' x)
: l1 = l1' ++ [x] ++ prefix_nincl x l1.
Proof.
unfold last_common' in Hlc. destructH.
eapply postfix_eq in Hlc0.

Admitted.

(* currently not used ! *)
Lemma last_common_app_eq2 `{EqDec A eq} (l1 l2 l1' l2' : list A) x
(Hlc : last_common' l1 l2 l1' l2' x)
: l2 = l2' ++ [x] ++ prefix_nincl x l2.
Proof.
eapply last_common'_sym in Hlc. eapply last_common_app_eq1;eauto.
Qed.

(* currently not used ! *)
Lemma last_common_in1 `{EqDec A eq} (l1 l2 : list A) x
(Hlc : last_common l1 l2 x)
: x l1.
Admitted.

(* currently not used ! *)
Lemma last_common_prefix `{EqDec A eq} (ll1 ll2 l1 l2 : list A)
(l1' l2' : list A) (x : A)
(Hlc : last_common' (l1 ++ [x] ++ ll1) (l2 ++ [x] ++ ll2) l1 l2 x)
(Hpre1 : Prefix l1' l1)
(Hpre2 : Prefix l2' l2)
: last_common' (l1' ++ [x] ++ ll1) (l2' ++ [x] ++ ll2) l1' l2' x.
Proof.
Admitted.
End Lc.