GMu.Progress

Require Import Prelude.
Require Import Infrastructure.
Require Import Regularity.
Require Import CanonicalForms.
Require Import Equations.

#[export] Hint Resolve binds_empty_inv.

Ltac empty_binding :=
  match goal with
  | H: binds ?x ?v empty |- _ ⇒ apply binds_empty_inv in H; contradiction
  | _ ⇒ fail "no empty bindings found"
  end.

Ltac IHT e :=
  match goal with
  | Ht: {?Σ, ?D, ?E} ⊢(?TT) e ∈ ?T |- _ ⇒
    match goal with
    | IH: ∀ T, ?P0 → {Σ, D, E} ⊢(?TT2) e ∈ T → ?P |- _ ⇒
      let H := fresh "IHt" in
      assert P as H; eauto
    end
  end.

Ltac generalize_typings :=
  match goal with
  | [ H: {?Σ, ?D, ?E} ⊢(?TT) ?e ∈ ?T |- _ ] ⇒
    match TT with
    | Tgen ⇒ fail 1
    | Treg ⇒ fail 1
    | _ ⇒ apply Tgen_from_any in H
    end
  end.

#[export] Hint Constructors value red.
Theorem progress_thm : progress.
Proof.
  unfold progress.
  introv Typ.
  assert (Hterm: term e).
  1: {
    eapply typing_implies_term; eauto.
  }
  apply Tgen_from_any in Typ. clear TT.

  gen T Hterm.
  induction e using trm_ind;
    introv TypGen Hterm;
    lets [T2 [TypReg EQ]]: inversion_typing_eq TypGen;
    inversion TypReg;
    inversion Hterm;
    subst;
    try solve [
          left×
        | repeat generalize_typings;
          forwards× [Hv1 | [e1' Hred1]]: IHe1;
          forwards× [Hv2 | [e2' Hred2]]: IHe2
        ]; clear TypGen EQ T; try rename T2 into T.
  - empty_binding.
  - repeat generalize_typings.
    forwards × [Hval | [? ?]]: IHe.
  - generalize_typings.
    forwards × [Hval | [? ?]]: IHe.
    lets [T' [Typ2 EQ]]: inversion_typing_eq H0.
    apply empty_eq_is_equivalent in EQ. subst.
    lets× [v1 [v2 ?]]: CanonicalFormTuple Typ2; subst.
    right×.
  - generalize_typings.
    forwards × [Hval | [? ?]]: IHe.
    lets [T' [Typ2 EQ]]: inversion_typing_eq H0.
    apply empty_eq_is_equivalent in EQ. subst.
    lets× [v1 [v2 ?]]: CanonicalFormTuple Typ2; subst.
    right×.
  - repeat generalize_typings.
    forwards × [Hval1 | [? ?]]: IHe1.
    forwards × [Hval2 | [? ?]]: IHe2.
    right.
    lets [T' [Typ2 EQ]]: inversion_typing_eq H5.
    apply empty_eq_is_equivalent in EQ. subst.
    lets× [v1 ?]: CanonicalFormAbs Typ2; subst.
    eexists.
    apply× red_beta.
  - repeat generalize_typings.
    forwards × [Hval1 | [? ?]]: IHe.
    right.
    lets [T' [Typ2 EQ]]: inversion_typing_eq H1.
    apply empty_eq_is_equivalent in EQ. subst.
    lets× [v1 ?]: CanonicalFormTAbs Typ2; subst.
    eexists.
    apply× red_tbeta.
  - repeat generalize_typings.
    right.
    eexists.
    eauto.
  - right.
    rename l into branches.
    repeat generalize_typings.
    forwards × [Hval1 | [? ?]]: IHe.
    lets [T' [Typ2 EQ]]: inversion_typing_eq H2.
    apply empty_eq_is_equivalent in EQ; subst.
    lets× [GCargs [cid [ctor_e ?]]]: CanonicalFormGadt Typ2; subst.
    inversions Typ2.
    match goal with
    | [ H1: binds ?g ?A Σ, H2: binds ?g ?B Σ |- _ ] ⇒
      let H := fresh "H" in
      lets H: binds_ext H1 H2;
        inversions H
    end.
    match goal with
    | [ Hnth: List.nth_error ?As ?i = Some ?A |- _ ] ⇒
      match goal with
      | [ Hlen: length As = length ?Bs |- _ ] ⇒
        lets× [[clA clT] [nth_cl inzip]]: nth_error_implies_zip Hnth Hlen
      end
    end.
    assert (clA = length GCargs).
    × match goal with
      | [ H: ∀ def clause, List.In (def, clause) ?A → clauseArity clause = Carity def |- _ ] ⇒
        lets*: H inzip
      end.
    × subst.
      eexists.
      eauto.
Qed.

Check progress_thm.