Require Import List Lia.
Import ListNotations.
Require Import Undecidability.StackMachines.Util.Nat_facts.
Require Import ssreflect ssrbool ssrfun.
Set Default Goal Selector "!".
Lemma seq_last {m n} : seq m (1+n) = seq m n ++ [m + n].
Proof. have -> : 1+n = n+1 by lia. by rewrite seq_app. Qed.
(* nth_error facts *)
Lemma nth_error_map {X Y: Type} {f: X -> Y} {l: list X} {n: nat} :
nth_error (map f l) n = omap f (nth_error l n).
Proof.
elim: n l; first by case.
move=> n IH. case; first done.
move=> x l /=. by rewrite /nth_error -?/(nth_error _ _).
Qed.
Lemma nth_error_seq {m l n: nat} :
n < l -> nth_error (seq m l) n = Some (m+n).
Proof.
elim: n m l.
- move=> m [|l]; first by lia.
move=> /= _. congr Some. by lia.
- move=> n IH m [|l /= ?]; first by lia.
rewrite /nth_error -/(nth_error _ _) IH; [|congr Some]; by lia.
Qed.
Lemma repeat_appP {X: Type} {x: X} {n m: nat} :
repeat x n ++ repeat x m = repeat x (n+m).
Proof. by elim: n; [| move=> ? /= ->]. Qed.
Lemma repeat_app_appP {X: Type} {x: X} {xs: list X} {n m: nat} :
repeat x n ++ (repeat x m ++ xs) = repeat x (n+m) ++ xs.
Proof. by rewrite -repeat_appP app_assoc. Qed.
Lemma repeat_singP {X: Type} {x: X} :
[x] = repeat x 1.
Proof. done. Qed.
Lemma app_assoc' {X: Type} {xs ys zs: list X} :
(xs ++ ys) ++ zs = xs ++ ys ++ zs.
Proof. by rewrite app_assoc. Qed.
Lemma cons_repeat_app {X: Type} {x: X} {xs: list X} {m: nat} :
x :: (repeat x m ++ xs) = (repeat x (m+1) ++ xs).
Proof. by have ->: m + 1 = S m by lia. Qed.
Lemma app_singP {X: Type} {x: X} {l: list X} : [x] ++ l = x :: l.
Proof. done. Qed.
Lemma app_repeat_cons {X: Type} {n: nat} {x: X} {l: list X} : repeat x (1+n) ++ l = x :: (repeat x n ++ l).
Proof. done. Qed.
Lemma nth_error_Some_In_combineP {X: Type} {i} {x: X} {L: list X} :
nth_error L i = Some x <-> In (i, x) (combine (seq 0 (length L)) L).
Proof.
suff: forall j, nth_error L i = Some x <-> In (j+i, x) (combine (seq j (length L)) L) by move /(_ 0).
elim: L i.
{ by move=> [|i] j. }
move=> y L IH [|i] j /=.
- constructor.
+ move=> [->]. left. f_equal. by lia.
+ case; first by move=> [_ ->].
move /(@in_combine_l nat X). rewrite in_seq. by lia.
- rewrite (IH i (S j)).
have ->: S j + i = j + S i by lia. constructor.
+ move=> ?. by right.
+ by case; [move=> []; lia |].
Qed.
Lemma nth_error_combine_SomeP {X: Type} {i} {x: X} {L: list X} :
nth_error L i = Some x <-> nth_error (combine (seq 0 (length L)) L) i = Some (i, x).
Proof.
suff: forall j, nth_error L i = Some x <-> nth_error (combine (seq j (length L)) L) i = Some (j+i, x) by move /(_ 0).
elim: L i; first by case.
move=> y L IH [|i] j /=.
- have ->: j + 0 = j by lia.
by constructor; move=> [->].
- have ->: j + S i = S j + i by lia.
by apply: IH.
Qed.
Lemma nth_error_appP {X: Type} {l1 l2: list X} {i: nat} {x: X} :
nth_error (l1 ++ l2) i = Some x <->
((i < length l1 /\ nth_error l1 i = Some x) \/ (length l1 <= i /\ nth_error l2 (i - length l1) = Some x)).
Proof.
constructor.
- have [Hi | Hi]: i < length l1 \/ length l1 <= i by lia.
+ by rewrite nth_error_app1; firstorder done.
+ by rewrite nth_error_app2; firstorder done.
- move=> [[? ?]|[? ?]]; by [rewrite nth_error_app1 | rewrite nth_error_app2].
Qed.
Lemma NoDup_map {X Y: Type} {f : X -> Y} {l : list X} :
(forall x1 x2, f x1 = f x2 -> x1 = x2) -> NoDup l -> NoDup (map f l).
Proof.
move=> Hf. elim: l.
{ move=> ?. by apply: NoDup_nil. }
move=> x l IH /NoDup_cons_iff [Hx /IH Hfl] /=.
apply /NoDup_cons_iff. constructor; last done.
rewrite in_map_iff. by move=> [x'] [/Hf ->].
Qed.
Lemma legnth_flat_map {X Y: Type} {f: X -> list Y} {l: list X} {n: nat}:
(forall x, length (f x) <= n) ->
length (flat_map f l) <= n * length l.
Proof.
move=> Hf. elim: l.
- move=> * /=. by lia.
- move=> x l IH /=. rewrite app_length. have := Hf x. by lia.
Qed.
Lemma in_split_informative {X: Type} {x: X} {l: list X} : (forall (x y: X), {x = y} + {x <> y}) ->
In x l -> { '(l1, l2) | l = l1 ++ x :: l2 }.
Proof.
move=> H_dec. elim: l; first done.
move=> y l IH /=. case: (H_dec y x).
- move=> <- _. by exists ([], l).
- move=> ? Hxl. have : In x l by case: Hxl.
move /IH => [[l1 l2] ->]. by exists (y :: l1, l2).
Qed.
Lemma in_split_rest {X: Type} {x y: X} {L1 L2: list X} :
In y (L1 ++ x :: L2) -> x <> y -> In y (L1 ++ L2).
Proof. rewrite ?in_app_iff /=. by firstorder done. Qed.
Lemma in_app_l {X: Type} {x: X} {l1 l2: list X} : In x l1 -> In x (l1 ++ l2).
Proof. move=> ?. apply /in_app_iff. by left. Qed.
Lemma in_app_r {X: Type} {x: X} {l1 l2: list X} : In x l2 -> In x (l1 ++ l2).
Proof. move=> ?. apply /in_app_iff. by right. Qed.
Import ListNotations.
Require Import Undecidability.StackMachines.Util.Nat_facts.
Require Import ssreflect ssrbool ssrfun.
Set Default Goal Selector "!".
Lemma seq_last {m n} : seq m (1+n) = seq m n ++ [m + n].
Proof. have -> : 1+n = n+1 by lia. by rewrite seq_app. Qed.
(* nth_error facts *)
Lemma nth_error_map {X Y: Type} {f: X -> Y} {l: list X} {n: nat} :
nth_error (map f l) n = omap f (nth_error l n).
Proof.
elim: n l; first by case.
move=> n IH. case; first done.
move=> x l /=. by rewrite /nth_error -?/(nth_error _ _).
Qed.
Lemma nth_error_seq {m l n: nat} :
n < l -> nth_error (seq m l) n = Some (m+n).
Proof.
elim: n m l.
- move=> m [|l]; first by lia.
move=> /= _. congr Some. by lia.
- move=> n IH m [|l /= ?]; first by lia.
rewrite /nth_error -/(nth_error _ _) IH; [|congr Some]; by lia.
Qed.
Lemma repeat_appP {X: Type} {x: X} {n m: nat} :
repeat x n ++ repeat x m = repeat x (n+m).
Proof. by elim: n; [| move=> ? /= ->]. Qed.
Lemma repeat_app_appP {X: Type} {x: X} {xs: list X} {n m: nat} :
repeat x n ++ (repeat x m ++ xs) = repeat x (n+m) ++ xs.
Proof. by rewrite -repeat_appP app_assoc. Qed.
Lemma repeat_singP {X: Type} {x: X} :
[x] = repeat x 1.
Proof. done. Qed.
Lemma app_assoc' {X: Type} {xs ys zs: list X} :
(xs ++ ys) ++ zs = xs ++ ys ++ zs.
Proof. by rewrite app_assoc. Qed.
Lemma cons_repeat_app {X: Type} {x: X} {xs: list X} {m: nat} :
x :: (repeat x m ++ xs) = (repeat x (m+1) ++ xs).
Proof. by have ->: m + 1 = S m by lia. Qed.
Lemma app_singP {X: Type} {x: X} {l: list X} : [x] ++ l = x :: l.
Proof. done. Qed.
Lemma app_repeat_cons {X: Type} {n: nat} {x: X} {l: list X} : repeat x (1+n) ++ l = x :: (repeat x n ++ l).
Proof. done. Qed.
Lemma nth_error_Some_In_combineP {X: Type} {i} {x: X} {L: list X} :
nth_error L i = Some x <-> In (i, x) (combine (seq 0 (length L)) L).
Proof.
suff: forall j, nth_error L i = Some x <-> In (j+i, x) (combine (seq j (length L)) L) by move /(_ 0).
elim: L i.
{ by move=> [|i] j. }
move=> y L IH [|i] j /=.
- constructor.
+ move=> [->]. left. f_equal. by lia.
+ case; first by move=> [_ ->].
move /(@in_combine_l nat X). rewrite in_seq. by lia.
- rewrite (IH i (S j)).
have ->: S j + i = j + S i by lia. constructor.
+ move=> ?. by right.
+ by case; [move=> []; lia |].
Qed.
Lemma nth_error_combine_SomeP {X: Type} {i} {x: X} {L: list X} :
nth_error L i = Some x <-> nth_error (combine (seq 0 (length L)) L) i = Some (i, x).
Proof.
suff: forall j, nth_error L i = Some x <-> nth_error (combine (seq j (length L)) L) i = Some (j+i, x) by move /(_ 0).
elim: L i; first by case.
move=> y L IH [|i] j /=.
- have ->: j + 0 = j by lia.
by constructor; move=> [->].
- have ->: j + S i = S j + i by lia.
by apply: IH.
Qed.
Lemma nth_error_appP {X: Type} {l1 l2: list X} {i: nat} {x: X} :
nth_error (l1 ++ l2) i = Some x <->
((i < length l1 /\ nth_error l1 i = Some x) \/ (length l1 <= i /\ nth_error l2 (i - length l1) = Some x)).
Proof.
constructor.
- have [Hi | Hi]: i < length l1 \/ length l1 <= i by lia.
+ by rewrite nth_error_app1; firstorder done.
+ by rewrite nth_error_app2; firstorder done.
- move=> [[? ?]|[? ?]]; by [rewrite nth_error_app1 | rewrite nth_error_app2].
Qed.
Lemma NoDup_map {X Y: Type} {f : X -> Y} {l : list X} :
(forall x1 x2, f x1 = f x2 -> x1 = x2) -> NoDup l -> NoDup (map f l).
Proof.
move=> Hf. elim: l.
{ move=> ?. by apply: NoDup_nil. }
move=> x l IH /NoDup_cons_iff [Hx /IH Hfl] /=.
apply /NoDup_cons_iff. constructor; last done.
rewrite in_map_iff. by move=> [x'] [/Hf ->].
Qed.
Lemma legnth_flat_map {X Y: Type} {f: X -> list Y} {l: list X} {n: nat}:
(forall x, length (f x) <= n) ->
length (flat_map f l) <= n * length l.
Proof.
move=> Hf. elim: l.
- move=> * /=. by lia.
- move=> x l IH /=. rewrite app_length. have := Hf x. by lia.
Qed.
Lemma in_split_informative {X: Type} {x: X} {l: list X} : (forall (x y: X), {x = y} + {x <> y}) ->
In x l -> { '(l1, l2) | l = l1 ++ x :: l2 }.
Proof.
move=> H_dec. elim: l; first done.
move=> y l IH /=. case: (H_dec y x).
- move=> <- _. by exists ([], l).
- move=> ? Hxl. have : In x l by case: Hxl.
move /IH => [[l1 l2] ->]. by exists (y :: l1, l2).
Qed.
Lemma in_split_rest {X: Type} {x y: X} {L1 L2: list X} :
In y (L1 ++ x :: L2) -> x <> y -> In y (L1 ++ L2).
Proof. rewrite ?in_app_iff /=. by firstorder done. Qed.
Lemma in_app_l {X: Type} {x: X} {l1 l2: list X} : In x l1 -> In x (l1 ++ l2).
Proof. move=> ?. apply /in_app_iff. by left. Qed.
Lemma in_app_r {X: Type} {x: X} {l1 l2: list X} : In x l2 -> In x (l1 ++ l2).
Proof. move=> ?. apply /in_app_iff. by right. Qed.