From Coq Require Import Lia List Init.Nat PeanoNat.
From PCF2.external Require Import SR.
From PCF2.external.Synthetic Require Import Definitions DecidabilityFacts.
Set Default Goal Selector "!".

Ltac inv H := inversion H; subst; clear H.

Lemma iter_succ_r (n: nat) (A: Type) (f: A -> A) (x: A):
    iter (S n) f x = iter n f (f x).
Proof.
    now rewrite PeanoNat.Nat.iter_succ_r.
Qed.

Lemma iter_succ_l (n: nat) (A: Type) (f: A -> A) (x: A):
    iter (S n) f x = f (iter n f x).
Proof.
    now rewrite PeanoNat.Nat.iter_succ.
Qed.

Lemma rev_nth_error1 {A: Type} (l: list A) n (a: A):
     n < length l -> nth_error l n = nth_error (rev l) (length l - S n).
Proof.
    intros H. rewrite (nth_error_nth' (rev l) a). 2: simpl_list; lia.
    rewrite <- rev_length.
    rewrite <- rev_nth. 2: simpl_list; lia.
    simpl_list. now rewrite <- nth_error_nth'.
Qed.

Lemma rev_nth_error2 {A: Type} (l: list A) n (a: A):
     n < length l -> nth_error l (length l - S n) = nth_error (rev l) n.
Proof.
    intros H. rewrite nth_error_nth' with (d := a). 2: lia.
    rewrite <- rev_nth. 2: easy. rewrite <- nth_error_nth'.
    1: easy. now simpl_list.
Qed.

Definition eq_dec X := decidable (fun p: X * X => fst p = snd p).

Lemma bool_eq_dec:
    eq_dec bool.
Proof.
    unfold eq_dec.
    rewrite decidable_iff.
    constructor. intros [b1 b2].
    destruct b1, b2; firstorder; right; easy.
Qed.

Lemma list_eq_dec {A: Type}:
    eq_dec A -> eq_dec (list A).
Proof.
    intros dec_A. unfold eq_dec in *.
    rewrite decidable_iff in dec_A. destruct dec_A as [dec_A].
    rewrite decidable_iff. constructor.
    intros [l1 l2]. induction l1 in l2 |-*.
    - destruct l2; firstorder. now right.
    - destruct l2. 1: now right.
    destruct (IHl1 l2), (dec_A (a, a0)).
    {left. cbn in *. intuition congruence. }
    all: right; cbn in *; intuition congruence.
Qed.

Lemma pair_eq_dec {A B: Type}:
    eq_dec A -> eq_dec B -> eq_dec (prod A B).
Proof.
    intros dec_A dec_B. unfold eq_dec in *.
    rewrite decidable_iff in dec_A. destruct dec_A as [dec_A].
    rewrite decidable_iff in dec_B. destruct dec_B as [dec_B].
    rewrite decidable_iff. constructor.
    intros [[a1 b1] [a2 b2]]. destruct (dec_A (a1, a2)), (dec_B (b1, b2)).
    all: cbn in *.
    1: left; intuition congruence.
    all: right; intuition congruence.
Qed.

Lemma rules_eq_decidable:
    eq_dec (str * str).
Proof.
    apply pair_eq_dec.
    all: apply list_eq_dec, bool_eq_dec.
Qed.

Lemma list_eq {A: Type} (l l': list A):
    length l = length l' -> (forall n a a', nth_error l n = Some a -> nth_error l' n = Some a' -> a = a') -> l = l'.
Proof.
    intros len H. induction l as [| a l] in l', len, H |-*.
    - now destruct l'.
    - destruct l' as [| a' l'].
    1: easy.
    enough (H': a = a' /\ l = l').
    { destruct H' as [eq_1 eq_2]. now subst. }
    split.
    1: now apply (H 0).
    apply IHl.
    1: now injection len.
    intros n s t H_s H_t. now apply (H (S n)).
Qed.

Lemma nat_ord_dec (n m: nat):
    (n <= m) + (n > m).
Proof.
    induction n in m |-*.
    1: left; lia.
    destruct m.
    1: right; lia.
    destruct (IHn m).
    1: left; lia.
    right; lia.
Qed.

Lemma leb_le_true:
    forall n m, leb n m = true <-> n <= m.
Proof.
    apply Nat.leb_le.
Qed.

Lemma leb_le_false:
    forall n m, leb n m = false <-> n > m.
Proof.
    intros n m. split.
    - intros H. assert (H1: ~ leb n m = true) by now destruct (leb n m).
        rewrite leb_le_true in H1. lia.
    - intros H. assert (H1: ~ n <= m) by lia. rewrite <- leb_le_true in H1.
        now destruct (leb n m).
Qed.

Lemma ltb_lt_true:
    forall n m, ltb n m = true <-> n < m.
Proof.
    apply Nat.ltb_lt.
Qed.

Lemma ltb_lt_false:
    forall n m, ltb n m = false <-> n >= m.
Proof.
    intros n m. split.
    - intros H. assert (H1: ~ ltb n m = true) by now destruct (ltb n m).
        rewrite ltb_lt_true in H1. lia.
    - intros H. assert (H1: ~ n < m) by lia. rewrite <- ltb_lt_true in H1.
        now destruct (ltb n m).
Qed.

Lemma arith_technical m n o:
    n > m -> n <= m + o -> exists n', n' < o /\ n = m + 1 + n'.
Proof.
intros H1 H2. induction n in m, H1, H2 |-*.
    - lia.
    - destruct m.
        + exists n. lia.
        + assert (eq1: n > m) by lia. assert (eq2: n <= m + o) by lia.
        destruct (IHn m eq1 eq2) as [n' Hn']. exists n'. lia.
Qed.

Lemma arith_technical' m n o:
    n >= m -> n < m + o -> exists n', n' < o /\ n = m + n'.
Proof.
intros H1 H2. induction m in n, H1, H2 |-*.
    - exists n. lia.
    - destruct n.
        + exists m. lia.
        + assert (eq1: n >= m) by lia. assert (eq2: n < m + o) by lia.
        destruct (IHm n eq1 eq2) as [n' Hn']. exists n'. lia.
Qed.

Definition diff n m := (n - m) + (m - n).

Lemma diff1 n m:
  n >= m -> diff n m = n - m.
Proof.
  intros ?. unfold diff. lia.
Qed.

Lemma diff2 n m:
  n < m -> diff n m = m - n.
Proof.
  intros ?. unfold diff. lia.
Qed.