UniAna.infra.FirstDiff

Require Import Lia.
Require Export ListExtra DecTac.

Lemma first_diff' (A : Type) `{EqDec A eq} (l1 l2 : list A)
(Hneq : l1 <> l2)
(Hlen : length l1 = length l2)
(Hnnil1 : l1 <> nil)
(Hnnil2 : l2 <> nil)
: exists a1 a2 l' l1' l2', a1 <> a2 /\ l1 = l' ++ a1 :: l1' /\ l2 = l' ++ a2 :: l2'.
Proof.
assert (forall (l : list A), l <> nil -> length l > 0) as Hlengt.
{ clear. intros. destruct l;cbn;[congruence|lia]. }
eapply Hlengt in Hnnil1; eapply Hlengt in Hnnil2. clear Hlengt.
revert dependent l2. induction l1; intros; destruct l2; cbn in *.
1: congruence. 1-2: lia.
destruct l1,l2; cbn in *; only 2,3: congruence.
- exists a, a0, nil, nil, nil. split_conj; cbn; eauto. contradict Hneq. subst; eauto.
- decide' (a == a0).
+ exploit' IHl1;[lia|]. specialize (IHl1 (a2 :: l2)). exploit IHl1.
* contradict Hneq. f_equal;eauto.
* cbn; lia.
* destructH. exists a0, a3, (a :: l'), l1', l2'. split_conj; eauto.
1,2: cbn; f_equal; eauto.
+ exists a, a0, nil, (a1 :: l1), (a2 :: l2). split_conj; eauto.
Qed.

Lemma first_diff (A : Type) `{EqDec A eq} (l1 l2 : list A)
(Hneq : l1 <> l2)
(Hlen : length l1 = length l2)
(Hnnil1 : l1 <> nil)
(Hnnil2 : l2 <> nil)
: exists a1 a2 l' l1' l2', a1 <> a2 /\ l1 = l1' ++ a1 :: l' /\ l2 = l2' ++ a2 :: l'.
Proof.
specialize (@first_diff' _ _ _ (rev l1) (rev l2)) as Hfi.
exploit Hfi; cycle -1.
- destructH.
rewrite <-rev_involutive in Hfi2. eapply rev_injective in Hfi2.
rewrite rev_app_distr in Hfi2. rewrite rev_cons in Hfi2.
rewrite <-rev_involutive in Hfi3. eapply rev_injective in Hfi3.
rewrite rev_app_distr in Hfi3. rewrite rev_cons in Hfi3.
exists a1, a2, (rev l'), (rev l1'), (rev l2').
rewrite <-app_assoc in Hfi2,Hfi3. cbn in *. firstorder.
- contradict Hneq. eapply rev_injective; eauto.
- rewrite !rev_length; eauto.
- contradict Hnnil1. destruct l1;cbn in *;[auto|congruence'].
- contradict Hnnil2. destruct l2;cbn in *;[auto|congruence'].
Qed.