import Base
import ./LAWS.bend as Laws
import ./topology.bend as T
import ./protein.bend as P

# Proofs for LAWS.bend. Three shapes recur:
# - Nil laws hold by computation: the empty list matches the Nil{} branch,
#   which returns the identity element directly.
# - Step/singleton laws hold by computation too: one unfolding exposes the
#   head term identically on both sides (F32 subterms stay stuck but equal).
# - Annihilation laws (contacts_nil_right, min_link2_nil_right) induct on
#   the atom list; each step rewrites with a symmetrized induction
#   hypothesis, since % rewrites right-to-left, then closes by computation.

def Laws.count_below_nil(qp, c2):
  {==}

def Laws.has_close_nil(qp, min2):
  {==}

def Laws.sum_dist2_nil(qp):
  {==}

def Laws.contacts_between_nil(ys, c2):
  {==}

def Laws.min_dist2_nil(qp):
  {==}

def Laws.complex_atoms_nil():
  {==}

def Laws.lj_nil(eps, sig2, c2):
  {==}

def Laws.rmsd_nil():
  {==}

def Laws.sasa_nil(rad, rc2, area_pt):
  {==}

def Laws.sd_fuel0(xs, eps, sig2, c2, dt):
  {==}

def Laws.count_cons(h, t, qp, c2):
  {==}

def Laws.contacts_cons(x, xt, ys, c2):
  {==}

def Laws.sumd2_count_cons(h, t, qp):
  {==}

def Laws.coord_cons(x, xt, ys, c2):
  {==}

def Laws.min_dist2_cons(h, t, qp):
  {==}

def Laws.min_link2_cons(h, t, ys):
  {==}

def Laws.lj_row_cons(pi, eps, sig2, c2, h, t):
  {==}

def Laws.lj_total_cons(h, t, ys, eps, sig2, c2):
  {==}

def Laws.coul_row_cons(pi, qi, ke, c2, h, t, qh, qt):
  {==}

def Laws.coul_total_cons(h, t, qh, qt, ys, qs_e, ke, c2):
  {==}

def Laws.sd_sweep_cons(h, t, f, ft, dt):
  {==}

def Laws.pair_sumd2_cons(x, xt, y, yt):
  {==}

def Laws.rmsd_to_all_cons(q, h, t):
  {==}

def Laws.count_single(h, qp, c2):
  {==}

def Laws.has_close_single(h, qp, min2):
  {==}

def Laws.min_single(s, e, x, y, z, qx, qy, qz):
  {==}

def Laws.rg_about_nil(qp):
  {==}

def Laws.rmsd_single(s, e, x, y, z):
  {==}

def Laws.rng_next_0():
  {==}

def Laws.rng_next_1():
  {==}

def Laws.sasa_single():
  {==}

def Laws.pair_trunc_right(x, xt):
  {==}

def Laws.coul_trunc_charges(h, t, ys, qs, ke, c2):
  {==}

def Laws.sd_trunc_forces(h, t, dt):
  {==}

def Laws.contacts_nil_right(xs, c2):
  match xs:
    case Nil{}:
      {==}
    case h <> +t:
      match h:
        case P.Atom{serial, elem, pos}:
          +c2b = c2
          %Equal.sym(Nat, T.contacts_between(t, Laws.empty_atoms(), c2b), 0n, Laws.contacts_nil_right(t, c2b)) : {Nat.add(_, T.contacts_of_head(P.Atom{serial, elem, pos}, Laws.empty_atoms(), c2b)) == 0n : Nat}
          {==}

def Laws.min_link2_nil_right(xs):
  match xs:
    case Nil{}:
      {==}
    case h <> +t:
      match h:
        case P.Atom{serial, elem, pos}:
          %Equal.sym(Maybe<&2, F32>, T.min_link2(t, Laws.empty_atoms()), None{}, Laws.min_link2_nil_right(t)) : {T.min_maybe(_, T.head_link(P.Atom{serial, elem, pos}, Laws.empty_atoms())) == None{} : Maybe<&2, F32>}
          {==}

def Laws.rmsd_checked_some(x, y):
  {==}

def Laws.rmsd_checked_none(x):
  {==}

def Laws.append_atoms_assoc(xs, ys, zs):
  match xs:
    case Nil{}:
      {==}
    case h <> t:
      %Laws.append_atoms_assoc(t, ys, zs) : {h <> P.append_atoms(P.append_atoms(t, ys), zs) == h <> _ : List<&2, P.Atom>}
      {==}

def Laws.flatten_residues_append(xs, ys):
  match xs:
    case Nil{}:
      {==}
    case h <> +t:
      match h:
        case P.Residue{seq, atoms}:
          +ysb = ys
          %Equal.sym(List<&2, P.Atom>, P.flatten_residues(P.append_residues(t, ys)), P.append_atoms(P.flatten_residues(t), P.flatten_residues(ys)), Laws.flatten_residues_append(t, ysb)) : {P.append_atoms(atoms, _) == P.append_atoms(P.append_atoms(atoms, P.flatten_residues(t)), P.flatten_residues(ys)) : List<&2, P.Atom>}
          %Laws.append_atoms_assoc(atoms, P.flatten_residues(t), P.flatten_residues(ysb)) : {_ == P.append_atoms(P.append_atoms(atoms, P.flatten_residues(t)), P.flatten_residues(ys)) : List<&2, P.Atom>}
          {==}

def Laws.add_zero_right(b):
  match b:
    case 0n:
      {==}
    case 1n+p:
      %Laws.add_zero_right(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
      {==}

def Laws.add_succ_right(b, a):
  match b:
    case 0n:
      {==}
    case 1n+q:
      %Laws.add_succ_right(q, a) : {1n+Nat.add(q, 1n+a) == 1n+_ : Nat}
      {==}

def Laws.add_comm(a, b):
  match a:
    case 0n:
      %Laws.add_zero_right(b) : {_ == Nat.add(b, 0n) : Nat}
      {==}
    case 1n++p:
      +bb = b
      %Equal.sym(Nat, Nat.add(bb, 1n+p), 1n+Nat.add(bb, p), Laws.add_succ_right(bb, p)) : {1n+Nat.add(p, bb) == _ : Nat}
      %Laws.add_comm(p, bb) : {1n+Nat.add(p, bb) == 1n+_ : Nat}
      {==}

def Laws.count_atoms_append(xs, ys):
  match xs:
    case Nil{}:
      {==}
    case h <> t:
      %Laws.count_atoms_append(t, ys) : {1n+P.count_atoms(P.append_atoms(t, ys)) == 1n+_ : Nat}
      {==}

def Laws.count_flatten_eq(rs):
  match rs:
    case Nil{}:
      {==}
    case h <> +t:
      match h:
        case P.Residue{seq, +atoms}:
          %Equal.sym(Nat, P.count_atoms(P.append_atoms(atoms, P.flatten_residues(t))), Nat.add(P.count_atoms(atoms), P.count_atoms(P.flatten_residues(t))), Laws.count_atoms_append(atoms, P.flatten_residues(t))) : {_ == Nat.add(P.count_atoms_in(t), P.count_atoms(atoms)) : Nat}
          %Equal.sym(Nat, P.count_atoms(P.flatten_residues(t)), P.count_atoms_in(t), Laws.count_flatten_eq(t)) : {Nat.add(P.count_atoms(atoms), _) == Nat.add(P.count_atoms_in(t), P.count_atoms(atoms)) : Nat}
          %Laws.add_comm(P.count_atoms(atoms), P.count_atoms_in(t)) : {Nat.add(P.count_atoms(atoms), P.count_atoms_in(t)) == _ : Nat}
          {==}

def Laws.complex_flatten_eq(chains):
  %Laws.count_flatten_eq(P.flatten_chains_residues(chains)) : {_ == P.count_atoms(P.flatten_residues(P.flatten_chains_residues(chains))) : Nat}
  {==}

def Laws.pow10_3():
  {==}

def Laws.elem_iron():
  {==}

def Laws.elem_carbon():
  {==}

def Laws.atom_line_yes():
  {==}

def Laws.atom_line_no():
  {==}

def Laws.atom_lines_nil():
  {==}

def Laws.atom_lines_keep():
  {==}

def Laws.parse_f32_one():
  {==}

def Laws.parse_f32_neg():
  {==}

def Laws.parse_f32_bad():
  {==}

def Laws.pdb_num_atoms():
  {==}

def Laws.pdb_num_residues():
  {==}

def Laws.pdb_num_chains():
  {==}

def Laws.pdb_skipped_0():
  {==}

def Laws.pdb_skipped_1():
  {==}

def Laws.pdb_bad_atoms():
  {==}

def Laws.pdb_first_elem():
  {==}

def Laws.sasa_total_cons(h, t):
  {==}

def Laws.count_par4_nil(qp, c2):
  {==}

def Laws.count_par4_step(h1, h2, h3, h4, t, qp, c2):
  {==}

def Laws.count_par4_small(h, qp, c2):
  {==}

def Laws.lj_row_par4_nil(pi, eps, sig2, c2):
  {==}

def Laws.lj_row_par4_step(pi, eps, sig2, c2, h1, h2, h3, h4, t):
  {==}

def Laws.lj_row_par4_small(pi, eps, sig2, c2, h):
  {==}

def Laws.lj_eps_c():
  {==}

def Laws.lj_eps_h():
  {==}

def Laws.lj_sig_o():
  {==}

def Laws.lj_sig_default():
  {==}

def Laws.lj_row_elem_cons(si, pi, c2, h, t):
  {==}

def Laws.lj_total_elem_cons(h, t, ys, c2):
  {==}

def Laws.bond_total_nil(k):
  {==}

def Laws.bond_total_cons(xs, s1, s2, t, k):
  {==}

def Laws.angle_total_nil(k, eq):
  {==}

def Laws.angle_total_cons(xs, sa, sb, sc, t, k, eq):
  {==}

def Laws.pos_of_serial_none(s):
  {==}

def Laws.pos_of_serial_some():
  {==}

def Laws.bonded12_nil(a, b):
  {==}

def Laws.bonded12_hit():
  {==}

def Laws.bonded12_miss():
  {==}

def Laws.neighbors_one():
  {==}

def Laws.excluded13_one():
  {==}

def Laws.excluded_both():
  {==}

def Laws.flatten_bonds_one():
  {==}

def Laws.lj_row_excl_nil(si, pi, eps, sig2, c2, bonds):
  {==}

def Laws.lj_total_excl_nil(ys, eps, sig2, c2, bonds):
  {==}

def Laws.coul_row_excl_nil(si, pi, qi, ke, c2, bonds):
  {==}

def Laws.coul_total_excl_nil(ys, qs_e, ke, c2, bonds):
  {==}

def Laws.lj_row_elem_excl_nil(si, se, pi, c2, bonds):
  {==}

def Laws.lj_total_elem_excl_nil(ys, c2, bonds):
  {==}

def Laws.lj_row_elem_excl_hit():
  {==}

def Laws.lj_row_elem_excl_link():
  {==}

def Laws.conect_lines_nil():
  {==}

def Laws.conect_keep():
  {==}

def Laws.parse_conect_one():
  {==}

def Laws.parse_conect_none():
  {==}

def Laws.mass_c():
  {==}

def Laws.mass_h():
  {==}

def Laws.coul_frow_cons(pi, qi, ke, c2, h, t, qh, qt):
  {==}

def Laws.coul_forces_cons(h, t, qh, qt, ys, qs_e, ke, c2):
  {==}

def Laws.coul_frow_nil(pi, qi, ke, c2):
  {==}

def Laws.lj_row_pbc_cons(pi, eps, sig2, c2, box, h, t):
  {==}

def Laws.lj_total_pbc_cons(h, t, ys, eps, sig2, c2, box):
  {==}

def Laws.lj_row_pbc_nil(pi, eps, sig2, c2, box):
  {==}

def Laws.lj_frow_pbc_cons(pi, eps, sig2, c2, box, h, t):
  {==}

def Laws.lj_forces_pbc_cons(h, t, ys, eps, sig2, c2, box):
  {==}

def Laws.lj_forces_pbc_nil(ys, eps, sig2, c2, box):
  {==}

def Laws.cov_rad_c():
  {==}

def Laws.infer_row_nil(si, pi, ei):
  {==}

def Laws.infer_row_cons(si, pi, ei, h, t):
  {==}

def Laws.infer_total_nil():
  {==}

def Laws.bond_forces_nil(bonds, k):
  {==}

def Laws.bond_forces_cons(h, t, bonds, k):
  {==}

def Laws.dyn_of_atoms_nil():
  {==}

def Laws.dyn_of_atoms_cons(h, t):
  {==}

def Laws.dyn_atoms_nil():
  {==}

def Laws.vv_scale_nil(lam):
  {==}

def Laws.vv_scale_cons(h, t, lam):
  {==}

def Laws.vv_half_nil(dt):
  {==}

def Laws.vv_half_cons(h, t, dt):
  {==}

def Laws.vv_full_nil(dt):
  {==}

def Laws.vv_full_cons(h, t, dt):
  {==}

def Laws.ke_sim_nil():
  {==}

def Laws.md_run_zero(ds, qs, bonds, p, dt, tau, temp0, n):
  {==}

def Laws.min_run_zero(ds, qs, bonds, p, dt):
  {==}


def Laws.zero_charges_nil():
  {==}

def Laws.zero_charges_cons(h, t):
  {==}

def Laws.sd_norm_sweep_nil(dt):
  {==}

def Laws.maxforce2_nil():
  {==}

def Laws.dyn_set_force_nil(fs):
  {==}

def Laws.add_forces_nil():
  {==}

def Laws.add_forces_cons(x, xt, y, yt):
  {==}

def Laws.pairs_of_flat_nil():
  {==}

def Laws.pairs_of_flat_cons(x, y, t):
  {==}

def Laws.pad_left_golden():
  {==}

def Laws.pad_right_golden():
  {==}

def Laws.fmt_u32_golden():
  {==}

def Laws.elem_sym_golden():
  {==}

def Laws.tpl_has_bond_ala():
  {==}

def Laws.tpl_has_bond_miss():
  {==}

def Laws.tpl_has_bond_unknown():
  {==}

def Laws.tpl_has_bond_his():
  {==}

def Laws.tpl_row_nil(a):
  {==}

def Laws.tpl_row_cons(a, h, t):
  {==}

def Laws.tpl_total_nil():
  {==}

def Laws.parse_tpl_golden():
  {==}

def Laws.neighbors_except_golden():
  {==}

def Laws.fan_triples_golden():
  {==}

def Laws.angle_triples_auto_golden():
  {==}