Require Import List Lia.
Import ListNotations.

Require Import ssreflect ssrbool ssrfun.

Set Default Proof Using "Type".
Set Default Goal Selector "!".

(* Generic facts *)

(* duplicates argument *)
Fact copy {A : Type} : A -> A * A.
Proof. done. Qed.

(* transforms a goal (A -> B) -> C into goals A and B -> C *)
Lemma unnest : forall (A B C : Type), A -> (B -> C) -> (A -> B) -> C.
Proof. auto. Qed.

Lemma iter_plus {X: Type} {f: X -> X} {x: X} {n m: nat} : Nat.iter n f (Nat.iter m f x) = Nat.iter (n + m) f x.
Proof. elim: n; [done | by move=> n /= ->]. Qed.

Fact iter_last {X: Type} {f: X -> X} {n x} : Nat.iter n f (f x) = Nat.iter (1+n) f x.
Proof. elim: n x; [done | by move=> n /= + x => ->]. Qed.

(* induction principle wrt. a decreasing measure f *)
(* example: elim /(measure_ind length) : l. *)
Lemma measure_ind {X : Type} (f : X -> nat) (P : X -> Prop) :
  (forall x, (forall y, f y < f x -> P y) -> P x) -> forall (x : X), P x.
Proof.
  apply : well_founded_ind.
  apply : Wf_nat.well_founded_lt_compat. move => *. by eassumption.
Qed.
Arguments measure_ind {X}.

(* List facts *)

Section ForallNorm.
Variable T : Type.
Variable P : T -> Prop.

Lemma Forall_nilP : Forall P [] <-> True.
Proof. by constructor. Qed.

Lemma Forall_consP {a A} : Forall P (a :: A) <-> P a /\ Forall P A.
Proof. constructor=> [H | [? ?]]; [by inversion H | by constructor]. Qed.

Lemma Forall_singletonP {a} : Forall P [a] <-> P a.
Proof. rewrite Forall_consP Forall_nilP. by constructor=> [[? ?] | ?]. Qed.

Lemma Forall_appP {A B}: Forall P (A ++ B) <-> Forall P A /\ Forall P B.
Proof.
  elim: A; first by (constructor; by [|case]).
  move=> ? ? IH /=. by rewrite ?Forall_consP IH and_assoc.
Qed.

(* use: rewrite ?Forall_norm *)
Definition Forall_norm := (@Forall_appP, @Forall_singletonP, @Forall_consP, @Forall_nilP).

Lemma Forall_appI {A B}: Forall P A -> Forall P B -> Forall P (A ++ B).
Proof. move=> ? ?. apply /Forall_appP. by constructor. Qed.
End ForallNorm.

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 incl_nth_error {X: Type} {Gamma Gamma': list X} :
  incl Gamma Gamma' -> exists ξ, forall x, nth_error Gamma x = nth_error Gamma' (ξ x).
Proof.
  elim: Gamma Gamma'.
  - move=> Gamma' _. exists (fun x => length Gamma').
    move=> [|x] /=; apply /esym; by apply /nth_error_None.
  - move=> x Gamma IH Gamma'. rewrite /incl -Forall_forall Forall_norm Forall_forall.
    move=> [/(@In_nth_error _ _ _) [nx] Hnx /IH] [ξ ].
    exists (fun y => if y is S y then ξ y else nx). by case.
Qed.

Lemma Forall_mapP {X Y : Type} {P : Y -> Prop} {f : X -> Y} {l : list X} :
  Forall P (map f l) <-> Forall (fun x => P (f x)) l.
Proof.
  elim: l.
  - move=> /=. by constructor.
  - move=> a l IH /=. by rewrite ? Forall_norm IH.
Qed.

Lemma Forall_seqP {P : nat -> Prop} {m n: nat} :
  Forall P (seq m n) <-> (forall i, m <= i < m + n -> P i).
Proof. rewrite Forall_forall. constructor; move=> H ? ?; apply H; by apply /in_seq. Qed.

Lemma Forall2_consE {X Y: Type} {R: X -> Y -> Prop} {x y l1 l2} :
  Forall2 R (x :: l1) (y :: l2) -> R x y /\ Forall2 R l1 l2.
Proof. move=> H. by inversion H. Qed.

Lemma Forall2_length_eq {X Y: Type} {R: X -> Y -> Prop} {l1 l2} :
  Forall2 R l1 l2 -> length l1 = length l2.
Proof.
  elim: l1 l2.
  - move=> [| ? ?] H; first done. by inversion H.
  - move=> ? ? IH [| ? ?] /= H; inversion H. congr S. by apply: IH.
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.

(* construct choice function for a list over nat *)
Lemma list_choice {P : nat -> nat -> Prop} {l: list nat} : Forall (fun i : nat => exists n : nat, P i n) l ->
  exists φ, Forall (fun i : nat => P i (φ i)) l.
Proof.
  elim /rev_ind: l.
  - move=> ?. exists id. by constructor.
  - move=> k l IH. rewrite Forall_app. move=> [/IHHφ]] /(@Forall_inv _ _ _) [n Hn].
    exists (fun i => if PeanoNat.Nat.eq_dec i k then n else φ i).
    rewrite Forall_app. constructor.
    + move: Hφ. rewrite ?Forall_forall => H i.
      case: (PeanoNat.Nat.eq_dec _ _); [by move=> /= -> | by move=> *; apply: H].
    + constructor; last done. by case: (PeanoNat.Nat.eq_dec _ _).
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 map_id' {X: Type} {f: X -> X} {l: list X} : (forall x, f x = x) -> map f l = l.
Proof. move=> ?. rewrite -[RHS]map_id. by apply: map_ext => ?. Qed.

Lemma is_trueP {b1 b2: bool} : (is_true b1 <-> is_true b2) <-> b1 = b2.
Proof.
  case: b1; case: b2; rewrite /is_true; firstorder done.
Qed.