From Stdlib Require Import ClassicalEpsilon.
From SMTLIB Require Import Utils Symbols Term Signature Theory Sorting Eval.
From SMTLIB.Theory Require Import Reals_Ints.

Open Scope smt_scope.


Definition s_seq : sortsymb := "Seq".
Definition τ_seq (τ : sort) : sort := SApp s_seq [τ].

Definition is_seqb (σ : sort) : bool :=
  match σ with
  | SApp s [_] ⇒ bool_decide (s = s_seq)
  | _ ⇒ false
  end.

Lemma is_seqb_false : ∀ σ, is_seqb σ = false ↔ ∀ σ', σ ≠ τ_seq σ'.
Proof.
  intros σ. split.
  - intros Hb σ' →. cbn in Hb. by rewrite bool_decide_eq_true_2 in Hb.
  - intros Hns. destruct σ as [u | s τs]; [reflexivity|].
    destruct τs as [| σ1 [| σ2 τs']]; [reflexivity| | reflexivity].
    cbn. apply bool_decide_eq_false_2. intros →. by apply (Hns σ1).
Qed.

Definition f_seq_empty : func := "seq.empty".
Definition f_seq_unit : func := "seq.unit".
Definition f_seq_concat : func := "seq.++".
Definition f_seq_len : func := "seq.len".
Definition f_seq_nth : func := "seq.nth".
Definition f_seq_contains : func := "seq.contains".
Definition f_seq_map : func := "seq.map".

Definition seq_funcs : gset func :=
      {[ f_seq_empty; f_seq_unit; f_seq_concat;
         f_seq_len; f_seq_nth; f_seq_contains; f_seq_map ]}.

Definition seq_empty σ := TApp f_seq_empty (Some (τ_seq σ)) [].
Definition seq_unit t := TApp f_seq_unit None [t].
Definition seq_concat t1 t2 := TApp f_seq_concat None [t1; t2].
Definition seq_len t := TApp f_seq_len None [t].
Definition seq_nth t1 t2 := TApp f_seq_nth None [t1; t2].
Definition seq_contains t1 t2 := TApp f_seq_contains None [t1; t2].
Definition seq_map t1 t2 := TApp f_seq_map None [t1; t2].

Inductive rank_seq : func → list sort → sort → Prop :=
| rank_f_seq_empty : rank_seq f_seq_empty [] (τ_seq τ_A)
| rank_f_seq_unit : rank_seq f_seq_unit [τ_A] (τ_seq τ_A)
| rank_f_seq_concat : rank_seq f_seq_concat [τ_seq τ_A; τ_seq τ_A] (τ_seq τ_A)
| rank_f_seq_len : rank_seq f_seq_len [τ_seq τ_A] σ_int
| rank_f_seq_nth : rank_seq f_seq_nth [τ_seq τ_A; σ_int] τ_A
| rank_f_seq_contains : rank_seq f_seq_contains [τ_seq τ_A; τ_seq τ_A] σ_bool
| rank_f_seq_map : rank_seq f_seq_map [τ_map τ_A τ_B; τ_seq τ_A] (τ_seq τ_B).

Program Definition Σ_seq : signature :=
  {|
    sort_symbols := {[ s_bool; s_map; s_int; s_seq ]};

    funcs f := f ∈ seq_funcs;
    funcs_dec f := decide (f ∈ seq_funcs);

    constructors := ∅;
    selectors := ∅;
    testers := ∅;

    constructors_for_sort (s : sortsymb) := ∅;

    arity (s : sortsymb) :=
      if identifier_eqb s_seq s
      then 1
      else if identifier_eqb s_map s
      then 2
      else 0;

    selectors_for_constructor (c : func) := [];
    tester_for_constructor (c : func) := c;
    constructor_for_tester (p : func) := p;

    sorts := ∅;

    rank := rank_seq;
  |}.
Next Obligation.
Proof. set_solver. Qed.
Next Obligation.
Proof. set_solver. Qed.
Next Obligation.
Proof. set_solver. Qed.
Next Obligation.
Proof. set_solver. Qed.
Next Obligation.
Proof. set_solver. Qed.
Next Obligation.
Proof. set_solver. Qed.
Next Obligation.
Proof. set_solver. Qed.
Next Obligation.
Proof. reflexivity. Qed.
Next Obligation.
Proof. reflexivity. Qed.
Next Obligation.
Proof. set_solver. Qed.
Next Obligation.
Proof. set_solver. Qed.
Next Obligation.
Proof. set_solver. Qed.
Next Obligation.
Proof. set_solver. Qed.
Next Obligation.
Proof. set_solver. Qed.
Next Obligation.
Proof.
  intros f τs τ Hf.
  inversion Hf; split; repeat constructor.
Qed.
Next Obligation. sauto. Qed.
Next Obligation.
Proof.
  intros f Hf.
  assert (Hf': f = f_seq_empty ∨ f = f_seq_unit ∨ f = f_seq_concat ∨ f = f_seq_len ∨ f = f_seq_nth ∨ f = f_seq_contains ∨ f = f_seq_map) by set_solver.
  clear Hf. destruct_or! Hf'; subst f; eexists; econstructor; constructor.
Qed.
Next Obligation.
Proof. set_solver. Qed.
Next Obligation.
Proof. set_solver. Qed.
Next Obligation.
Proof. set_solver. Qed.
Next Obligation.
Proof. set_solver. Qed.

Section SeqModels.

  Variable A : structure.
  Variable domain_σ_int : A.(domain) σ_int = Z.
  Variable domain_σ_seq : ∀ σ, A.(domain) (τ_seq σ) = list (A.(domain) σ).

  Definition cast_to_list σ := cast (domain_σ_seq σ).
  Definition cast_to_Z := cast domain_σ_int.
  Definition cast_to_map σ1 σ2 := cast (A.(domain_σ_map) σ1 σ2).
  Definition cast_to_bool := cast A.(domain_σ_bool).

  Definition models_f_seq_empty : Prop :=
    ∀ σ,
      let F := A.(interp) f_seq_empty [] (τ_seq σ) in
      cast_to_list σ F = [].

  Definition models_f_seq_unit : Prop :=
    ∀ σ v,
      let F := A.(interp) f_seq_unit [ σ ] (τ_seq σ) in
      cast_to_list σ (F v) = [ v ].

  Definition models_f_seq_concat : Prop :=
    ∀ σ l1 l2,
      let F := A.(interp) f_seq_concat [ τ_seq σ; τ_seq σ ] (τ_seq σ) in
      cast_to_list σ (F l1 l2)
      = (cast_to_list σ l1) ++ (cast_to_list σ l2).

  Definition models_f_seq_len : Prop :=
    ∀ σ l,
      let F := A.(interp) f_seq_len [ τ_seq σ ] σ_int in
      cast_to_Z (F l) = Z.of_nat $ length (cast_to_list σ l).

  Definition models_f_seq_nth : Prop :=
    ∀ σ l n i v,
      let F := A.(interp) f_seq_nth [ τ_seq σ; σ_int ] σ in
      (cast_to_list σ l) !! n = Some v →
      cast_to_Z i = Z.of_nat n →
      F l i = v.

  Definition models_f_seq_contains : Prop :=
    ∀ σ l1 l2,
      let F := A.(interp) f_seq_contains [ τ_seq σ; τ_seq σ ] σ_bool in
      (cast_to_list σ l2) `infix_of` (cast_to_list σ l1) ↔
      cast_to_bool (F l1 l2) = true.

  Definition models_f_seq_map : Prop :=
    ∀ σ1 σ2 l f,
      let F := A.(interp) f_seq_map [ τ_map σ1 σ2; τ_seq σ1 ] (τ_seq σ2) in
      map (cast_to_map σ1 σ2 f) (cast_to_list σ1 l)
      = cast_to_list σ2 (F f l).

  Record models_seq : Prop := {
    ms_empty : models_f_seq_empty;
    ms_unit : models_f_seq_unit;
    ms_concat : models_f_seq_concat;
    ms_len : models_f_seq_len;
    ms_nth : models_f_seq_nth;
    ms_contains: models_f_seq_contains;
    ms_map: models_f_seq_map;
  }.

End SeqModels.

Arguments ms_empty {_} {_} {_}.
Arguments ms_unit {_} {_} {_}.
Arguments ms_concat {_} {_} {_}.
Arguments ms_len {_} {_} {_}.
Arguments ms_nth {_} {_} {_}.
Arguments ms_contains {_} {_} {_}.
Arguments ms_map {_} {_} {_}.

Definition T_seq : pretheory :=
  {|
    pΣ := Σ_seq;
    pmodels A :=
      {HZ : A.(domain) σ_int = Z &
              {Hlist : ∀ σ, A.(domain) (τ_seq σ) = list (A.(domain) σ) &
                      models_seq A HZ Hlist}};
  |}.

Theorem T_seq_local : pretheory_local T_seq.
Proof.
  intros D Hbool Hmap i j Hagree [HZ [Hlist Hm]].
  ∃ HZ, Hlist.
  assert (Hrw : ∀ f, Σ_seq.(funcs) f → ∀ σs σ, j f σs σ = i f σs σ)
    by (intros f Hf σs σ; symmetry; exact (Hagree f Hf σs σ)).
  destruct Hm as [A1 A2 A3 A4 A5 A6 A7].
  constructor.
  - unfold models_f_seq_empty in A1 |- *; cbv zeta in A1 |- *;
    cbn [interp structure_of] in A1 |- *;
    intros; rewrite Hrw by set_solver; eapply A1; eauto.
  - unfold models_f_seq_unit in A2 |- *; cbv zeta in A2 |- *;
    cbn [interp structure_of] in A2 |- *;
    intros; rewrite Hrw by set_solver; eapply A2; eauto.
  - unfold models_f_seq_concat in A3 |- *; cbv zeta in A3 |- *;
    cbn [interp structure_of] in A3 |- *;
    intros; rewrite Hrw by set_solver; eapply A3; eauto.
  - unfold models_f_seq_len in A4 |- *; cbv zeta in A4 |- *;
    cbn [interp structure_of] in A4 |- *;
    intros; rewrite Hrw by set_solver; eapply A4; eauto.
  - unfold models_f_seq_nth in A5 |- *; cbv zeta in A5 |- *;
    cbn [interp structure_of] in A5 |- *;
    intros; rewrite Hrw by set_solver; eapply A5; eauto.
  - unfold models_f_seq_contains in A6 |- *; cbv zeta in A6 |- *;
    cbn [interp structure_of] in A6 |- *;
    intros; rewrite Hrw by set_solver; eapply A6; eauto.
  - unfold models_f_seq_map in A7 |- *; cbv zeta in A7 |- *;
    cbn [interp structure_of] in A7 |- *;
    intros; rewrite Hrw by set_solver; eapply A7; eauto.
Qed.

Section SeqInterpretable.

  Context (D : sort → Type).
  Context (witness : ∀ σ, D σ).
  Context (Hbool : D σ_bool = bool).
  Context (Hmap : ∀ σ1 σ2, D (τ_map σ1 σ2) = (D σ1 → D σ2)).
  Context (HZ : D σ_int = Z).
  Context (Hlist : ∀ σ, D (τ_seq σ) = list (D σ)).

  Local Notation base := (interp_const D witness).

  Local Definition seq_at {P : sort → Type} (σ : sort)
    (k : ∀ σ', P (τ_seq σ')) (base : ∀ σ, P σ) : P σ :=
    match σ as s return P s with
    | SApp sy [σ'] ⇒
        match decide (sy = s_seq) with
        | left H ⇒ eq_rect_r (fun x ⇒ P (SApp x [σ'])) (k σ') H
        | right _ ⇒ base (SApp sy [σ'])
        end
    | s ⇒ base s
    end.

  Local Lemma seq_at_τ_seq : ∀ P σ' k base,
      @seq_at P (τ_seq σ') k base = k σ'.
  Proof.
    intros P σ' k base. unfold seq_at, τ_seq.
    destruct (decide (s_seq = s_seq)) as [H | H]; [| by contradiction].
    by rewrite (Eqdep_dec.UIP_dec (fun x y ⇒ decide (x = y)) H eq_refl).
  Qed.

  Local Definition seq_empty_interp : ∀ σs σ, interpretation D σs σ :=
    fun σs σ ⇒
      match σs as l return interpretation D l σ with
      | [] ⇒ seq_at (P := D) σ (fun σ' ⇒ cast_sym (Hlist σ') []) witness
      | l ⇒ base l σ
      end.

  Local Definition seq_unit_interp : ∀ σs σ, interpretation D σs σ :=
    fun σs σ ⇒
      match σs as l return interpretation D l σ with
      | [σ1] ⇒
          fun v : D σ1 ⇒
            match decide (σ = τ_seq σ1) with
            | left H ⇒ eq_rect_r D (cast_sym (Hlist σ1) [v]) H
            | right _ ⇒ witness σ
            end
      | l ⇒ base l σ
      end.

  Local Definition seq_concat_interp : ∀ σs σ, interpretation D σs σ :=
    fun σs σ ⇒
      match σs as l return interpretation D l σ with
      | [σ1; σ2] ⇒
          fun (v1 : D σ1) (v2 : D σ2) ⇒
            seq_at (P := D) σ
              (fun σ' ⇒
                 match decide (σ1 = τ_seq σ'), decide (σ2 = τ_seq σ') with
                 | left H1, left H2 ⇒
                     cast_sym (Hlist σ')
                       (cast (Hlist σ') (eq_rect σ1 D v1 (τ_seq σ') H1)
                        ++ cast (Hlist σ') (eq_rect σ2 D v2 (τ_seq σ') H2))
                 | _, _ ⇒ witness (τ_seq σ')
                 end)
              witness
      | l ⇒ base l σ
      end.

  Local Definition seq_len_interp : ∀ σs σ, interpretation D σs σ :=
    fun σs σ ⇒
      match σs as l return interpretation D l σ with
      | [σ1] ⇒
          seq_at (P := fun s ⇒ D s → D σ) σ1
            (fun σ' (l : D (τ_seq σ')) ⇒
               match decide (σ = σ_int) with
               | left H ⇒
                   eq_rect_r D
                     (cast_sym HZ (Z.of_nat (length (cast (Hlist σ') l)))) H
               | right _ ⇒ witness σ
               end)
            (fun _ _ ⇒ witness σ)
      | l ⇒ base l σ
      end.

  Local Definition seq_nth_interp : ∀ σs σ, interpretation D σs σ :=
    fun σs σ ⇒
      match σs as l return interpretation D l σ with
      | [σ1; σ2] ⇒
          fun (l : D σ1) (i : D σ2) ⇒
            match decide (σ1 = τ_seq σ), decide (σ2 = σ_int) with
            | left H1, left H2 ⇒
                default (witness σ)
                  (cast (Hlist σ) (eq_rect σ1 D l (τ_seq σ) H1)
                   !! Z.to_nat (cast HZ (eq_rect σ2 D i σ_int H2)))
            | _, _ ⇒ witness σ
            end
      | l ⇒ base l σ
      end.

  Local Definition seq_contains_interp : ∀ σs σ, interpretation D σs σ :=
    fun σs σ ⇒
      match σs as l return interpretation D l σ with
      | [σ1; σ2] ⇒
          fun (l1 : D σ1) (l2 : D σ2) ⇒
            seq_at (P := fun s ⇒ D s → D σ) σ1
              (fun σ' (l1' : D (τ_seq σ')) ⇒
                 match decide (σ = σ_bool), decide (σ2 = τ_seq σ') with
                 | left H1, left H2 ⇒
                     eq_rect_r D
                       (cast_sym Hbool
                          (if excluded_middle_informative
                                (cast (Hlist σ') (eq_rect σ2 D l2 (τ_seq σ') H2)
                                 `infix_of` cast (Hlist σ') l1')
                           then true else false)) H1
                 | _, _ ⇒ witness σ
                 end)
              (fun _ _ ⇒ witness σ)
              l1
      | l ⇒ base l σ
      end.

  Local Definition seq_map_interp : ∀ σs σ, interpretation D σs σ :=
    fun σs σ ⇒
      match σs as l return interpretation D l σ with
      | [σ1; σ2] ⇒
          fun (fn : D σ1) (l : D σ2) ⇒
            seq_at (P := D) σ
              (fun σ_out ⇒
                 seq_at (P := fun s ⇒ D s → D (τ_seq σ_out)) σ2
                   (fun σ_in (l' : D (τ_seq σ_in)) ⇒
                      match decide (σ1 = τ_map σ_in σ_out) with
                      | left H ⇒
                          cast_sym (Hlist σ_out)
                            (map (cast (Hmap σ_in σ_out)
                                    (eq_rect σ1 D fn (τ_map σ_in σ_out) H))
                               (cast (Hlist σ_in) l'))
                      | right _ ⇒ witness (τ_seq σ_out)
                      end)
                   (fun _ _ ⇒ witness (τ_seq σ_out))
                   l)
              witness
      | l ⇒ base l σ
      end.

  Definition seq_interp : ∀ f σs σ, interpretation D σs σ :=
    interp_insert_func D f_seq_empty seq_empty_interp
   (interp_insert_func D f_seq_unit seq_unit_interp
   (interp_insert_func D f_seq_concat seq_concat_interp
   (interp_insert_func D f_seq_len seq_len_interp
   (interp_insert_func D f_seq_nth seq_nth_interp
   (interp_insert_func D f_seq_contains seq_contains_interp
   (interp_insert_func D f_seq_map seq_map_interp
   (fun _ ⇒ base))))))).

  Local Ltac seq_sym :=
    unfold seq_interp;
    repeat (rewrite interp_insert_func_ne; [| discriminate]);
    rewrite interp_insert_func_eq.

  Local Ltac dec_refl :=
    match goal with
    | |- context[decide ?P] ⇒
        let H := fresh "Hdec" in
        destruct (decide P) as [H | H]; [| by contradiction];
        rewrite (Eqdep_dec.UIP_dec (fun x y ⇒ decide (x = y)) H eq_refl)
    end.

  Theorem T_seq_interpretable :
    pretheory_interpretable T_seq D Hbool Hmap.
  Proof.
    ∃ seq_interp. ∃ HZ, Hlist.
    constructor;
      unfold models_f_seq_empty, models_f_seq_unit, models_f_seq_concat,
        models_f_seq_len, models_f_seq_nth, models_f_seq_contains,
        models_f_seq_map, cast_to_list, cast_to_Z, cast_to_bool, cast_to_map;
      cbv zeta; cbn [interp domain structure_of domain_σ_map].
    - intros σ. seq_sym. cbn [seq_empty_interp].
      rewrite seq_at_τ_seq. apply cast_cast_sym.
    - intros σ v. seq_sym. cbn [seq_unit_interp].
      repeat dec_refl. cbn [eq_rect_r eq_rect eq_sym]. apply cast_cast_sym.
    - intros σ l1 l2. seq_sym. cbn [seq_concat_interp].
      rewrite seq_at_τ_seq. repeat dec_refl. cbn [eq_rect].
      apply cast_cast_sym.
    - intros σ l. seq_sym. cbn [seq_len_interp].
      rewrite seq_at_τ_seq. repeat dec_refl.
      cbn [eq_rect_r eq_rect eq_sym]. apply cast_cast_sym.
    - intros σ l n i v Hnth Hi. seq_sym. cbn [seq_nth_interp].
      repeat dec_refl. cbn [eq_rect].
      rewrite Hi, Nat2Z.id, Hnth. reflexivity.
    - intros σ l1 l2. seq_sym. cbn [seq_contains_interp].
      rewrite seq_at_τ_seq. repeat dec_refl.
      cbn [eq_rect_r eq_rect eq_sym]. rewrite cast_cast_sym.
      destruct (excluded_middle_informative _) as [Hsub | Hsub].
      + split; [intros _; reflexivity | intros _; exact Hsub].
      + split; [intros Hc; contradiction | intros Hc; discriminate].
    - intros σ1 σ2 l fn. seq_sym. cbn [seq_map_interp].
      rewrite !seq_at_τ_seq. repeat dec_refl. cbn [eq_rect].
      symmetry. apply cast_cast_sym.
  Qed.

End SeqInterpretable.

Theorem seq_empty_has_sort : ∀ Σ σ,
    Σ_seq ⊑ Σ →
    monomorphic σ →
    Σ ⊢ seq_empty σ : τ_seq σ.
Proof.
  intros × Hsub Hmono.
  econstructor.
  - ∃ {[ u_A := σ ]}, [], (τ_seq τ_A). sauto lq:on.
  - reflexivity.
  - intros × Ht_i Hσ_i. inversion Ht_i.
Qed.

Theorem seq_unit_has_sort : ∀ Σ t σ,
    Σ_seq ⊑ Σ →
    monomorphic σ →
    (Σ ⊢ t : σ) →
    Σ ⊢ seq_unit t : τ_seq σ.
Proof.
  intros × Hsub Ht.
  econstructor.
  - ∃ {[ u_A := σ ]}, [τ_A], (τ_seq τ_A). sauto q:on dep:on.
  - intros × Hrank.
    eapply monomorphic_rank_conservative in Hrank; eauto.
    ecrush. set_solver.
  - reflexivity.
  - intros × Ht_i Hσ_i.
    rewrite list_lookup_singleton in Ht_i.
    destruct i; try congruence. simpl in ×.
    simplify_eq. assumption.
Qed.

Theorem seq_concat_has_sort : ∀ Σ t1 t2 σ,
    Σ_seq ⊑ Σ →
    monomorphic σ →
    (Σ ⊢ t1 : τ_seq σ) →
    (Σ ⊢ t2 : τ_seq σ) →
    Σ ⊢ seq_concat t1 t2 : τ_seq σ.
Proof.
  intros × Hsub Ht.
  econstructor.
  - ∃ {[ u_A := σ ]}, [τ_seq τ_A; τ_seq τ_A], (τ_seq τ_A).
    sauto qb:on dep:on.
  - intros × Hrank.
    eapply monomorphic_rank_conservative in Hrank; eauto.
    ecrush. set_solver.
  - reflexivity.
  - intros × Ht_i Hσ_i.
    destruct i; simpl in ×.
    + simplify_eq. assumption.
    + rewrite list_lookup_singleton in Ht_i.
      destruct i; try congruence. simpl in ×.
      simplify_eq. assumption.
Qed.

Lemma eval_seq_concat :
  ∀ Σ A θ σ t1 t2 (v1 v2 : A.(domain) (τ_seq σ)),
    Σ_seq ⊑ Σ →
    monomorphic σ →
    ⟦ t1 : τ_seq σ ⟧(Σ, A, θ) ⇓ v1 →
    ⟦ t2 : τ_seq σ ⟧(Σ, A, θ) ⇓ v2 →
    ⟦ seq_concat t1 t2 : τ_seq σ ⟧(Σ, A, θ)
      ⇓ interp_apply A.(domain)
         (A.(interp) f_seq_concat [τ_seq σ; τ_seq σ] (τ_seq σ))
         (HCons (τ_seq σ) [τ_seq σ] v1 (HCons (τ_seq σ) [] v2 HNil)).
Proof.
  intros Σ A θ σ t1 t2 v1 v2 Hsub Hmono Ht1 Ht2.
  unfold seq_concat. eapply E_TApp with (σs := [τ_seq σ; τ_seq σ])
    (vs := HCons (τ_seq σ) [τ_seq σ] v1 (HCons (τ_seq σ) [] v2 HNil)).
  - repeat constructor; [exact Ht1 | exact Ht2].
  - constructor.
  - ∃ {[ u_A := σ ]}, [τ_seq τ_A; τ_seq τ_A], (τ_seq τ_A).
    split; [apply (rank_extends Hsub); constructor|].
    split.
    + unfold monomorphic_instance_of. split.
      × unfold instance_of, τ_seq, τ_A; simpl.
        rewrite lookup_singleton_eq. reflexivity.
      × repeat constructor. exact Hmono.
    + constructor.
      × unfold monomorphic_instance_of. split.
        -- unfold instance_of, τ_seq, τ_A; simpl.
           rewrite lookup_singleton_eq. reflexivity.
        -- repeat constructor. exact Hmono.
      × constructor.
        -- unfold monomorphic_instance_of. split.
           ++ unfold instance_of, τ_seq, τ_A; simpl.
              rewrite lookup_singleton_eq. reflexivity.
           ++ repeat constructor. exact Hmono.
        -- constructor.
  - reflexivity.
Qed.

Theorem seq_len_has_sort : ∀ Σ t σ,
    Σ_seq ⊑ Σ →
    monomorphic σ →
    (Σ ⊢ t : τ_seq σ) →
    Σ ⊢ seq_len t : σ_int.
Proof.
  intros × Hsub Ht.
  econstructor.
  - ∃ {[ u_A := σ ]}, [τ_seq τ_A], σ_int. sauto dep:on.
  - intros × Hrank.
    eapply monomorphic_rank_conservative in Hrank; eauto.
    sauto. set_solver.
  - reflexivity.
  - intros × Ht_i Hσ_i.
    rewrite list_lookup_singleton in Ht_i.
    destruct i; try congruence. simpl in ×.
    simplify_eq. assumption.
Qed.

Lemma eval_seq_len :
  ∀ Σ A θ σ t (v : A.(domain) (τ_seq σ)),
    Σ_seq ⊑ Σ →
    monomorphic σ →
    ⟦ t : τ_seq σ ⟧(Σ, A, θ) ⇓ v →
    ⟦ seq_len t : σ_int ⟧(Σ, A, θ)
      ⇓ interp_apply A.(domain)
         (A.(interp) f_seq_len [τ_seq σ] σ_int)
         (HCons (τ_seq σ) [] v HNil).
Proof.
  intros Σ A θ σ t v Hsub Hmono Ht.
  unfold seq_len. eapply E_TApp with (σs := [τ_seq σ])
    (vs := HCons (τ_seq σ) [] v HNil).
  - repeat constructor. exact Ht.
  - constructor.
  - ∃ {[ u_A := σ ]}, [τ_seq τ_A], σ_int.
    split; [apply (rank_extends Hsub); constructor|].
    split.
    + unfold monomorphic_instance_of. split.
      × unfold instance_of. reflexivity.
      × repeat constructor.
    + constructor.
      × unfold monomorphic_instance_of. split.
        -- unfold instance_of, τ_seq, τ_A; simpl.
           rewrite lookup_singleton_eq. reflexivity.
        -- repeat constructor. exact Hmono.
      × constructor.
  - reflexivity.
Qed.

Theorem seq_nth_has_sort : ∀ Σ t1 t2 σ,
    Σ_seq ⊑ Σ →
    monomorphic σ →
    (Σ ⊢ t1 : τ_seq σ) →
    (Σ ⊢ t2 : σ_int) →
    Σ ⊢ seq_nth t1 t2 : σ.
Proof.
  intros × Hsub Ht.
  econstructor.
  - ∃ {[ u_A := σ ]}, [τ_seq τ_A; σ_int], τ_A.
    sauto qb:on dep:on.
  - intros × Hrank.
    eapply monomorphic_rank_conservative in Hrank; eauto.
    ecrush. set_solver.
  - reflexivity.
  - intros × Ht_i Hσ_i.
    destruct i; simpl in ×.
    + simplify_eq. assumption.
    + rewrite list_lookup_singleton in Ht_i.
      destruct i; try congruence. simpl in ×.
      simplify_eq. assumption.
Qed.

Lemma eval_seq_nth :
  ∀ Σ A θ σ t_seq t_i
         (v_seq : A.(domain) (τ_seq σ)) (v_i : A.(domain) σ_int),
    Σ_seq ⊑ Σ →
    monomorphic σ →
    ⟦ t_seq : τ_seq σ ⟧(Σ, A, θ) ⇓ v_seq →
    ⟦ t_i : σ_int ⟧(Σ, A, θ) ⇓ v_i →
    ⟦ seq_nth t_seq t_i : σ ⟧(Σ, A, θ)
      ⇓ interp_apply A.(domain)
         (A.(interp) f_seq_nth [τ_seq σ; σ_int] σ)
         (HCons (τ_seq σ) [σ_int] v_seq
           (HCons σ_int [] v_i HNil)).
Proof.
  intros Σ A θ σ t_seq t_i v_seq v_i Hsub Hmono Hseq Hi.
  unfold seq_nth. eapply E_TApp with (σs := [τ_seq σ; σ_int])
    (vs := HCons (τ_seq σ) [σ_int] v_seq
      (HCons σ_int [] v_i HNil)).
  - repeat constructor; [exact Hseq | exact Hi].
  - constructor.
  - ∃ {[ u_A := σ ]}, [τ_seq τ_A; σ_int], τ_A.
    split; [apply (rank_extends Hsub); constructor|].
    split.
    + unfold monomorphic_instance_of. split.
      × unfold instance_of, τ_A; simpl.
        rewrite lookup_singleton_eq. reflexivity.
      × exact Hmono.
    + constructor.
      × unfold monomorphic_instance_of. split.
        -- unfold instance_of, τ_seq, τ_A; simpl.
           rewrite lookup_singleton_eq. reflexivity.
        -- repeat constructor. exact Hmono.
      × constructor.
        -- unfold monomorphic_instance_of. split.
           ++ unfold instance_of. reflexivity.
           ++ repeat constructor.
        -- constructor.
  - reflexivity.
Qed.

Theorem seq_contains_has_sort : ∀ Σ t1 t2 σ,
    Σ_seq ⊑ Σ →
    monomorphic σ →
    (Σ ⊢ t1 : τ_seq σ) →
    (Σ ⊢ t2 : τ_seq σ) →
    Σ ⊢ seq_contains t1 t2 : σ_bool.
Proof.
  intros × Hsub Ht.
  econstructor.
  - ∃ {[ u_A := σ ]}, [τ_seq τ_A; τ_seq τ_A], σ_bool.
    sauto qb:on dep:on.
  - intros × Hrank.
    eapply monomorphic_rank_conservative in Hrank; eauto.
    ecrush. set_solver.
  - reflexivity.
  - intros × Ht_i Hσ_i.
    destruct i; simpl in ×.
    + simplify_eq. assumption.
    + rewrite list_lookup_singleton in Ht_i.
      destruct i; try congruence. simpl in ×.
      simplify_eq. assumption.
Qed.

Theorem seq_map_has_sort : ∀ Σ t1 t2 σ1 σ2,
    Σ_seq ⊑ Σ →
    monomorphic σ1 →
    monomorphic σ2 →
    (Σ ⊢ t1 : τ_map σ1 σ2) →
    (Σ ⊢ t2 : τ_seq σ1) →
    Σ ⊢ seq_map t1 t2 : τ_seq σ2.
Proof.
  intros × Hsub Ht.
  econstructor.
  - ∃ {[ u_A := σ1; u_B := σ2 ]}, [τ_map τ_A τ_B; τ_seq τ_A], (τ_seq τ_B).
    sauto.
  - intros × Hrank.
    eapply monomorphic_rank_conservative in Hrank; eauto.
    ecrush. set_solver.
  - reflexivity.
  - intros × Ht_i Hσ_i.
    destruct i; simpl in ×.
    + simplify_eq. assumption.
    + rewrite list_lookup_singleton in Ht_i.
      destruct i; try congruence. simpl in ×.
      simplify_eq. assumption.
Qed.

Definition generator_sort (Σ : signature) (σ : sort) : Prop :=
  adt_free Σ σ ∧ is_seqb σ = false.

Theorem generator_sort_irrelevant : ∀ Σ σ (H1 H2 : generator_sort Σ σ),
    H1 = H2.
Proof.
  intros Σ σ [Ha1 Hs1] [Ha2 Hs2].
  by rewrite (adt_free_irrelevant _ _ Ha1 Ha2),
    (Eqdep_dec.UIP_dec Bool.bool_dec Hs1 Hs2).
Qed.

Definition seq_sorts_not_adt (Σ : signature) : Prop :=
  ∀ σ, ¬ adt Σ (τ_seq σ).

Fixpoint seq_embeddableb (Σ : signature) (σ : sort) : bool :=
  match σ with
  | SApp s [σ1] ⇒
      if bool_decide (s = s_seq)
      then seq_embeddableb Σ σ1
      else bool_decide (embeddable_sort Σ (SApp s [σ1]))
  | _ ⇒ bool_decide (embeddable_sort Σ σ)
  end.

Definition seq_embeddable_sort (Σ : signature) (σ : sort) : Prop :=
  seq_embeddableb Σ σ = true.

Theorem seq_embeddable_sort_irrelevant :
  ∀ Σ σ (H1 H2 : seq_embeddable_sort Σ σ), H1 = H2.
Proof. intros Σ σ H1 H2. apply (Eqdep_dec.UIP_dec Bool.bool_dec). Qed.

Global Instance seq_embeddable_sort_dec (Σ : signature) (σ : sort) :
  Decision (seq_embeddable_sort Σ σ).
Proof. unfold seq_embeddable_sort. apply _. Defined.

Theorem seq_embeddable_leaf : ∀ Σ σ,
    is_seqb σ = false → embeddable_sort Σ σ → seq_embeddable_sort Σ σ.
Proof.
  intros Σ σ Hns Hi. unfold seq_embeddable_sort.
  destruct σ as [u | s τs]; [by apply (bool_decide_eq_true_2 (embeddable_sort Σ _)) |].
  destruct τs as [| σ1 [| σ2 τs']];
    [by apply (bool_decide_eq_true_2 (embeddable_sort Σ _))
    | | by apply (bool_decide_eq_true_2 (embeddable_sort Σ _))].
  cbn [seq_embeddableb]. cbn [is_seqb] in Hns. rewrite Hns.
  by apply (bool_decide_eq_true_2 (embeddable_sort Σ _)).
Qed.

Theorem embeddable_sort_of_seq_embeddable : ∀ Σ σ,
    is_seqb σ = false → seq_embeddable_sort Σ σ → embeddable_sort Σ σ.
Proof.
  intros Σ σ Hns Hi. unfold seq_embeddable_sort in Hi.
  destruct σ as [u | s τs]; [by apply (bool_decide_eq_true_1 (embeddable_sort Σ _)) |].
  destruct τs as [| σ1 [| σ2 τs']];
    [by apply (bool_decide_eq_true_1 (embeddable_sort Σ _))
    | | by apply (bool_decide_eq_true_1 (embeddable_sort Σ _))].
  cbn [seq_embeddableb] in Hi. cbn [is_seqb] in Hns. rewrite Hns in Hi.
  by apply (bool_decide_eq_true_1 (embeddable_sort Σ _)).
Qed.

Theorem seq_embeddable_seq : ∀ Σ σ,
    seq_embeddable_sort Σ σ → seq_embeddable_sort Σ (τ_seq σ).
Proof.
  intros Σ σ H. unfold seq_embeddable_sort, τ_seq.
  cbn [seq_embeddableb]. by rewrite (bool_decide_eq_true_2 (s_seq = s_seq) eq_refl).
Qed.

Theorem seq_embeddable_sort_elem : ∀ Σ σ,
    seq_embeddable_sort Σ (τ_seq σ) → seq_embeddable_sort Σ σ.
Proof.
  intros Σ σ H. unfold seq_embeddable_sort, τ_seq in ×.
  cbn [seq_embeddableb] in H. by rewrite (bool_decide_eq_true_2 (s_seq = s_seq) eq_refl) in H.
Qed.

Lemma generator_sort_of_seq_embeddable : ∀ Σ σ,
    is_seqb σ = false → ¬ adt Σ σ →
    seq_embeddable_sort Σ σ → generator_sort Σ σ.
Proof.
  intros Σ σ Hns Hnadt Hi. split; [| exact Hns].
  apply (adt_free_of_embeddable Σ σ); [| exact Hnadt].
  apply (embeddable_sort_of_seq_embeddable Σ σ); [exact Hns | exact Hi].
Qed.

Lemma not_τ_seq_SParam : ∀ u σ', SParam u ≠ τ_seq σ'.
Proof. intros u σ' H. discriminate. Qed.

Lemma not_τ_seq_nil : ∀ s σ', SApp s [] ≠ τ_seq σ'.
Proof. intros s σ' H. discriminate. Qed.

Lemma not_τ_seq_cons2 : ∀ s σ1 σ2 τs σ', SApp s (σ1 :: σ2 :: τs) ≠ τ_seq σ'.
Proof. intros s σ1 σ2 τs σ' H. discriminate. Qed.

Lemma not_τ_seq_symb : ∀ s σ0, s ≠ s_seq → ∀ σ', SApp s [σ0] ≠ τ_seq σ'.
Proof. intros s σ0 Hne σ' H. injection H as → _. contradiction. Qed.

Corollary seq_embeddable_sort_app_nil : ∀ Σ s,
    seq_embeddable_sort Σ (SApp s []).
Proof.
  intros Σ s. apply seq_embeddable_leaf;
    [reflexivity | apply embeddable_sort_app_nil].
Qed.

Section SeqGroundTerm.

  Variables (Σ : signature) (gen : ∀ σ, generator_sort Σ σ → Type).

  Unset Elimination Schemes.

  Inductive seq_ground_term : sort → Type :=
  | SGGen :
    ∀ σ (H : generator_sort Σ σ),
      gen σ H →
      seq_ground_term σ
  | SGSeq :
    ∀ σ,
      list (seq_ground_term σ) →
      seq_ground_term (τ_seq σ)
  | SGConstr :
    ∀ c σs δ s,
      s ∈ Σ.(sort_symbols) →
      sort_top_symbol δ = Some s →
      c ∈ Σ.(constructors_for_sort) s →
      monomorphic_rank Σ c σs δ →
      sort_wf Σ δ →
      hlist seq_ground_term σs →
      seq_ground_term δ.

  Set Elimination Schemes.

End SeqGroundTerm.

Arguments SGGen {_} {_}.
Arguments SGSeq {_} {_}.
Arguments SGConstr {_} {_}.

Definition seq_ground_term_constructor {Σ gen δ} (g : seq_ground_term Σ gen δ)
  : option func :=
  match g with
  | SGGen _ _ _ ⇒ None
  | SGSeq _ _ ⇒ None
  | SGConstr c _ _ _ _ _ _ _ _ _ ⇒ Some c
  end.

Lemma seq_ground_term_constructor_Some :
  ∀ Σ gen δ (g : seq_ground_term Σ gen δ) c,
    seq_ground_term_constructor g = Some c →
    ∃ σs s Hs Hδ Hc Hrank Hwf ws,
      g = SGConstr c σs δ s Hs Hδ Hc Hrank Hwf ws.
Proof.
  intros Σ gen δ g c Hg. destruct g; try discriminate.
  injection Hg as →. do 8 eexists. reflexivity.
Qed.

Section SeqGroundTermRect.

  Context (Σ : signature) (gen : ∀ σ, generator_sort Σ σ → Type).
  Context (P : ∀ σ, seq_ground_term Σ gen σ → Type).
  Context (Hgen : ∀ σ H (x : gen σ H), P σ (SGGen σ H x)).
  Context (Hseq : ∀ σ (gs : list (seq_ground_term Σ gen σ)),
              list_ForallT (P σ) gs → P (τ_seq σ) (SGSeq σ gs)).
  Context (Hconstr :
            ∀ c σs δ s Hs Hδ Hc Hrank Hwf (vs : hlist (seq_ground_term Σ gen) σs),
              hlist_ForallT (seq_ground_term Σ gen) P vs →
              P δ (SGConstr c σs δ s Hs Hδ Hc Hrank Hwf vs)).

  Fixpoint seq_ground_term_rect σ (g : seq_ground_term Σ gen σ) {struct g}
    : P σ g :=
    match g with
    | SGGen σ H x ⇒ Hgen σ H x
    | SGSeq σ gs ⇒
        Hseq σ gs
          ((fix go (l : list (seq_ground_term Σ gen σ)) {struct l}
              : list_ForallT (P σ) l :=
              match l with
              | [] ⇒ tt
              | g' :: l' ⇒ (seq_ground_term_rect σ g', go l')
              end) gs)
    | SGConstr c σs δ s Hs Hδ Hc Hrank Hwf vs ⇒
        Hconstr c σs δ s Hs Hδ Hc Hrank Hwf vs
          ((fix go σs' (ws : hlist (seq_ground_term Σ gen) σs') {struct ws}
              : hlist_ForallT (seq_ground_term Σ gen) P ws :=
              match ws with
              | HNil ⇒ tt
              | HCons σ' σs'' w ws' ⇒ (seq_ground_term_rect σ' w, go σs'' ws')
              end) σs vs)
    end.

End SeqGroundTermRect.

Lemma seq_ground_term_ind :
  ∀ (Σ : signature) (gen : ∀ σ, generator_sort Σ σ → Type)
    (P : ∀ σ, seq_ground_term Σ gen σ → Prop),
    (∀ σ H (x : gen σ H), P σ (SGGen σ H x)) →
    (∀ σ (gs : list (seq_ground_term Σ gen σ)),
        (∀ i g, gs !! i = Some g → P σ g) →
        P (τ_seq σ) (SGSeq σ gs)) →
    (∀ c σs δ s Hs Hδ Hc Hrank Hwf (vs : hlist (seq_ground_term Σ gen) σs),
        (∀ i p, hlist_lookup (seq_ground_term Σ gen) vs i = Some p →
                     P (projT1 p) (projT2 p)) →
        P δ (SGConstr c σs δ s Hs Hδ Hc Hrank Hwf vs)) →
    ∀ σ g, P σ g.
Proof.
  intros Σ gen P Hgen Hseq Hconstr.
  apply (seq_ground_term_rect Σ gen P Hgen).
  - intros σ gs Hall. apply Hseq. now apply list_ForallT_lookup.
  - intros c σs δ s Hs Hδ Hc Hrank Hwf vs Hall.
    apply Hconstr. now apply hlist_ForallT_lookup.
Qed.