QuantumLib.Prelim

Require Export Bool.
Require Export Arith.
Require Export Reals.
Require Export Psatz.
Require Export Program.
Require Export List.

Export ListNotations.

Notation "¬ b" := (negb b) (at level 75, right associativity). Infix "⊕" := xorb (at level 20).

Lemma xorb_nb_b : ∀ b, (¬ b) ⊕ b = true.
Lemma xorb_b_nb : ∀ b, b ⊕ (¬ b) = true.

Lemma xorb_involutive_l : ∀ b b', b ⊕ (b ⊕ b') = b'.
Lemma xorb_involutive_r : ∀ b b', b ⊕ b' ⊕ b' = b.

Lemma andb_xorb_dist : ∀ b b1 b2, b && (b1 ⊕ b2) = (b && b1) ⊕ (b && b2).

Lemma Sn_minus_1 : ∀ (n : nat), S n - 1 = n.

Lemma beq_reflect : ∀ x y, reflect (x = y) (x =? y).

Lemma blt_reflect : ∀ x y, reflect (x < y) (x <? y).

Lemma ble_reflect : ∀ x y, reflect (x ≤ y) (x <=? y).

#[export] Hint Resolve blt_reflect ble_reflect beq_reflect : bdestruct.

Ltac bdestruct X :=
  let H := fresh in let e := fresh "e" in
   evar (e: Prop);
   assert (H: reflect e X); subst e;
    [eauto with bdestruct
    | destruct H as [H|H];
       [ | try first [apply not_lt in H | apply not_le in H]]].

Ltac bdestructΩ X := bdestruct X; simpl; try lia.

Ltac bdestruct_all :=
  repeat match goal with
  | |- context[?a <? ?b] ⇒ bdestruct (a <? b)
  | |- context[?a <=? ?b] ⇒ bdestruct (a <=? b)
  | |- context[?a =? ?b] ⇒ bdestruct (a =? b)
  end; try (exfalso; lia).

Lemma if_dist : ∀ (A B : Type) (b : bool) (f : A → B) (x y : A),
  f (if b then x else y) = if b then f x else f y.

Lemma f_equal_inv : ∀ {A B} (x : A) (f g : A → B), f = g → f x = g x.

Lemma f_equal2_inv : ∀ {A B C} x y (f g : A → B → C), f = g → f x y = g x y.

Lemma f_equal_gen : ∀ {A B} (f g : A → B) a b, f = g → a = b → f a = g b.

Definition curry {A B C : Type} (f : A × B → C) : (A → B → C) :=
  fun x y ⇒ f (x,y).

Definition uncurry {A B C : Type} (f : A → B → C) : (A × B → C) :=
  fun p ⇒ f (fst p) (snd p).

Notation "l !! i" := (nth_error l i) (at level 20).

Fixpoint remove_at {A} (i : nat) (ls : list A) :=
  match i, ls with
  | _ ,[] ⇒ []
  | 0 , _ :: ls' ⇒ ls'
  | S i', a :: ls' ⇒ a :: remove_at i' ls'
  end.

Fixpoint update_at {A} (ls : list A) (i : nat) (a : A) : list A :=
  match ls, i with
  | [] , _ ⇒ []
  | _ :: ls', 0 ⇒ a :: ls'
  | b :: ls', S i' ⇒ b :: update_at ls' i' a
  end.

Lemma update_length : ∀ A (l: list A) (a : A) (n : nat),
    length (update_at l n a) = length l.

Lemma repeat_combine : ∀ A n1 n2 (a : A),
  List.repeat a n1 ++ List.repeat a n2 = List.repeat a (n1 + n2).

Lemma rev_repeat : ∀ A (a : A) n, rev (repeat a n) = repeat a n.

Lemma firstn_repeat_le : ∀ A (a : A) m n, (m ≤ n)%nat →
  firstn m (repeat a n) = repeat a m.

Lemma firstn_repeat_ge : ∀ A (a : A) m n, (m ≥ n)%nat →
  firstn m (repeat a n) = repeat a n.

Lemma firstn_repeat : ∀ A (a : A) m n,
  firstn m (repeat a n) = repeat a (min m n).

Lemma skipn_repeat : ∀ A (a : A) m n,
  skipn m (repeat a n) = repeat a (n-m).

Lemma skipn_length : ∀ {A} (l : list A) n,
  length (skipn n l) = (length l - n)%nat.
  Transparent skipn.
  Opaque skipn.

Lemma nth_firstn : ∀ {A} i n (l : list A) d,
  (i < n)%nat → nth i (firstn n l) d = nth i l d.

Definition maybe {A} (o : option A) (default : A) : A :=
  match o with
  | Some a ⇒ a
  | None ⇒ default
  end.

Ltac simpl_rewrite lem :=
  let H := fresh "H" in
  specialize lem as H; simpl in H; rewrite H; clear H.

Ltac simpl_rewrite' lem :=
  let H := fresh "H" in
  specialize lem as H; simpl in H; rewrite <- H; clear H.

Ltac simpl_rewrite_h lem hyp :=
  let H := fresh "H" in
  specialize lem as H; simpl in H; rewrite <- H in hyp; clear H.

Ltac apply_with_obligations H :=
  match goal with
  | [|- ?P ?a] ⇒ match type of H with ?P ?a' ⇒
    replace a with a'; [apply H|]; trivial end
  | [|- ?P ?a ?b] ⇒ match type of H with ?P ?a' ?b' ⇒
    replace a with a'; [replace b with b'; [apply H|]|]; trivial end
  | [|- ?P ?a ?b ?c ] ⇒ match type of H with ?P ?a' ?b' ?c' ⇒
    replace a with a'; [replace b with b'; [replace c with c'; [apply H|]|]|]; trivial end
  | [|- ?P ?a ?b ?c ?d] ⇒ match type of H with ?P ?a' ?b' ?c' ?d' ⇒
    replace a with a'; [replace b with b'; [replace c with c'; [replace d with d'; [apply H|]|]|]|]; trivial end
  | [|- ?P ?a ?b ?c ?d ?e] ⇒ match type of H with ?P ?a' ?b' ?c' ?d' ?e' ⇒
    replace a with a'; [replace b with b'; [replace c with c'; [replace d with d'; [replace e with e'; [apply H|]|]|]|]|];
    trivial end
  | [|- ?P ?a ?b ?c ?d ?e ?f] ⇒ match type of H with ?P ?a' ?b' ?c' ?d' ?e' ?f' ⇒
    replace a with a'; [replace b with b'; [replace c with c'; [replace d with d'; [replace e with e'; [replace f with f';
    [apply H|]|]|]|]|]|]; trivial end
  | [|- ?P ?a ?b ?c ?d ?e ?f ?g] ⇒ match type of H with ?P ?a' ?b' ?c' ?d' ?e' ?f' ?g' ⇒
    replace a with a'; [replace b with b'; [replace c with c'; [replace d with d'; [replace e with e'; [replace f with f';
    [replace g with g'; [apply H|]|]|]|]|]|]|]; trivial end
  end.

Tactic Notation "gen" ident(X1) :=
  generalize dependent X1.
Tactic Notation "gen" ident(X1) ident(X2) :=
  gen X2; gen X1.
Tactic Notation "gen" ident(X1) ident(X2) ident(X3) :=
  gen X3; gen X2; gen X1.
Tactic Notation "gen" ident(X1) ident(X2) ident(X3) ident(X4) :=
  gen X4; gen X3; gen X2; gen X1.
Tactic Notation "gen" ident(X1) ident(X2) ident(X3) ident(X4) ident(X5) :=
  gen X5; gen X4; gen X3; gen X2; gen X1.

Lemma double_mult : ∀ (n : nat), (n + n = 2 × n)%nat.
Lemma pow_two_succ_l : ∀ x, (2^x × 2 = 2 ^ (x + 1))%nat.
Lemma pow_two_succ_r : ∀ x, (2 × 2^x = 2 ^ (x + 1))%nat.
Lemma double_pow : ∀ (n : nat), (2^n + 2^n = 2^(n+1))%nat.
Lemma pow_components : ∀ (a b m n : nat), a = b → m = n → (a^m = b^n)%nat.
Lemma pow_positive : ∀ a b, a ≠ 0 → 0 < a ^ b.

Ltac unify_pows_two :=
  repeat match goal with
  
  | [ |- context[ 4%nat ]] ⇒ replace 4%nat with (2^2)%nat by reflexivity
  | [ |- context[ (0 + ?a)%nat]] ⇒ rewrite plus_0_l
  | [ |- context[ (?a + 0)%nat]] ⇒ rewrite plus_0_r
  | [ |- context[ (1 × ?a)%nat]] ⇒ rewrite Nat.mul_1_l
  | [ |- context[ (?a × 1)%nat]] ⇒ rewrite Nat.mul_1_r
  | [ |- context[ (2 × 2^?x)%nat]] ⇒ rewrite <- Nat.pow_succ_r'
  | [ |- context[ (2^?x × 2)%nat]] ⇒ rewrite pow_two_succ_l
  | [ |- context[ (2^?x + 2^?x)%nat]] ⇒ rewrite double_pow
  | [ |- context[ (2^?x × 2^?y)%nat]] ⇒ rewrite <- Nat.pow_add_r
  | [ |- context[ (?a + (?b + ?c))%nat ]] ⇒ rewrite plus_assoc
  | [ |- (2^?x = 2^?y)%nat ] ⇒ apply pow_components; try lia
  end.

Definition subset_gen {X : Type} (l1 l2 : list X) :=
  ∀ (x : X), In x l1 → In x l2.

Fixpoint subset_gen' {X : Type} (l1 l2 : list X) :=
  match l1 with
  | [] ⇒ True
  | (l :: l1') ⇒ In l l2 ∧ subset_gen' l1' l2
  end.

Lemma subset_is_subset' : ∀ (X : Type) (l1 l2 : list X),
    subset_gen' l1 l2 ↔ subset_gen l1 l2.

Infix "⊆" := subset_gen (at level 70, no associativity).

Lemma subset_cons : ∀ (X : Type) (l1 l2 : list X) (x : X),
  l1 ⊆ l2 → l1 ⊆ (x :: l2).

Lemma subset_concat_l : ∀ (X : Type) (l1 l2 : list X),
  l1 ⊆ (l1 ++ l2).

Lemma subset_concat_r : ∀ (X : Type) (l1 l2 : list X),
  l1 ⊆ (l2 ++ l1).

Corollary subset_self : ∀ (X : Type) (l1 : list X),
  l1 ⊆ l1.

Lemma subsets_add : ∀ (X : Type) (l1 l2 l3 : list X),
  l1 ⊆ l3 → l2 ⊆ l3 → (l1 ++ l2) ⊆ l3.

Lemma subset_trans : ∀ (X : Type) (l1 l2 l3 : list X),
    l1 ⊆ l2 → l2 ⊆ l3 → l1 ⊆ l3.

#[export] Hint Resolve subset_concat_l subset_concat_r subset_self
                       subsets_add subset_trans : sub_db.

Lemma firstn_subset : ∀ {X : Type} (n : nat) (ls : list X),
    firstn n ls ⊆ ls.

Lemma skipn_subset : ∀ {X : Type} (n : nat) (ls : list X),
    skipn n ls ⊆ ls.

#[export] Hint Resolve firstn_subset skipn_subset : sub_db.