PROOF.bend

bend-prot@0.1.0.0 · 539 lines · 0 definitions

1import Base
2import bend-prot@0.1.0.0/LAWS.bend as Laws
3import bend-prot@0.1.0.0/topology.bend as T
4import bend-prot@0.1.0.0/protein.bend as P
5
6# Proofs for LAWS.bend. Three shapes recur:
7# - Nil laws hold by computation: the empty list matches the Nil{} branch,
8#   which returns the identity element directly.
9# - Step/singleton laws hold by computation too: one unfolding exposes the
10#   head term identically on both sides (F32 subterms stay stuck but equal).
11# - Annihilation laws (contacts_nil_right, min_link2_nil_right) induct on
12#   the atom list; each step rewrites with a symmetrized induction
13#   hypothesis, since % rewrites right-to-left, then closes by computation.
14
15def Laws.count_below_nil(qp, c2):
16  {==}
17
18def Laws.has_close_nil(qp, min2):
19  {==}
20
21def Laws.sum_dist2_nil(qp):
22  {==}
23
24def Laws.contacts_between_nil(ys, c2):
25  {==}
26
27def Laws.min_dist2_nil(qp):
28  {==}
29
30def Laws.complex_atoms_nil():
31  {==}
32
33def Laws.lj_nil(eps, sig2, c2):
34  {==}
35
36def Laws.rmsd_nil():
37  {==}
38
39def Laws.sasa_nil(rad, rc2, area_pt):
40  {==}
41
42def Laws.sd_fuel0(xs, eps, sig2, c2, dt):
43  {==}
44
45def Laws.count_cons(h, t, qp, c2):
46  {==}
47
48def Laws.contacts_cons(x, xt, ys, c2):
49  {==}
50
51def Laws.sumd2_count_cons(h, t, qp):
52  {==}
53
54def Laws.coord_cons(x, xt, ys, c2):
55  {==}
56
57def Laws.min_dist2_cons(h, t, qp):
58  {==}
59
60def Laws.min_link2_cons(h, t, ys):
61  {==}
62
63def Laws.lj_row_cons(pi, eps, sig2, c2, h, t):
64  {==}
65
66def Laws.lj_total_cons(h, t, ys, eps, sig2, c2):
67  {==}
68
69def Laws.coul_row_cons(pi, qi, ke, c2, h, t, qh, qt):
70  {==}
71
72def Laws.coul_total_cons(h, t, qh, qt, ys, qs_e, ke, c2):
73  {==}
74
75def Laws.sd_sweep_cons(h, t, f, ft, dt):
76  {==}
77
78def Laws.pair_sumd2_cons(x, xt, y, yt):
79  {==}
80
81def Laws.rmsd_to_all_cons(q, h, t):
82  {==}
83
84def Laws.count_single(h, qp, c2):
85  {==}
86
87def Laws.has_close_single(h, qp, min2):
88  {==}
89
90def Laws.min_single(s, e, x, y, z, qx, qy, qz):
91  {==}
92
93def Laws.rg_about_nil(qp):
94  {==}
95
96def Laws.rmsd_single(s, e, x, y, z):
97  {==}
98
99def Laws.rng_next_0():
100  {==}
101
102def Laws.rng_next_1():
103  {==}
104
105def Laws.sasa_single():
106  {==}
107
108def Laws.pair_trunc_right(x, xt):
109  {==}
110
111def Laws.coul_trunc_charges(h, t, ys, qs, ke, c2):
112  {==}
113
114def Laws.sd_trunc_forces(h, t, dt):
115  {==}
116
117def Laws.contacts_nil_right(xs, c2):
118  match xs:
119    case Nil{}:
120      {==}
121    case h <> +t:
122      match h:
123        case P.Atom{serial, elem, pos}:
124          +c2b = c2
125          %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}
126          {==}
127
128def Laws.min_link2_nil_right(xs):
129  match xs:
130    case Nil{}:
131      {==}
132    case h <> +t:
133      match h:
134        case P.Atom{serial, elem, pos}:
135          %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>}
136          {==}
137
138def Laws.rmsd_checked_some(x, y):
139  {==}
140
141def Laws.rmsd_checked_none(x):
142  {==}
143
144def Laws.append_atoms_assoc(xs, ys, zs):
145  match xs:
146    case Nil{}:
147      {==}
148    case h <> t:
149      %Laws.append_atoms_assoc(t, ys, zs) : {h <> P.append_atoms(P.append_atoms(t, ys), zs) == h <> _ : List<&2, P.Atom>}
150      {==}
151
152def Laws.flatten_residues_append(xs, ys):
153  match xs:
154    case Nil{}:
155      {==}
156    case h <> +t:
157      match h:
158        case P.Residue{seq, atoms}:
159          +ysb = ys
160          %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>}
161          %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>}
162          {==}
163
164def Laws.add_zero_right(b):
165  match b:
166    case 0n:
167      {==}
168    case 1n+p:
169      %Laws.add_zero_right(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
170      {==}
171
172def Laws.add_succ_right(b, a):
173  match b:
174    case 0n:
175      {==}
176    case 1n+q:
177      %Laws.add_succ_right(q, a) : {1n+Nat.add(q, 1n+a) == 1n+_ : Nat}
178      {==}
179
180def Laws.add_comm(a, b):
181  match a:
182    case 0n:
183      %Laws.add_zero_right(b) : {_ == Nat.add(b, 0n) : Nat}
184      {==}
185    case 1n++p:
186      +bb = b
187      %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}
188      %Laws.add_comm(p, bb) : {1n+Nat.add(p, bb) == 1n+_ : Nat}
189      {==}
190
191def Laws.count_atoms_append(xs, ys):
192  match xs:
193    case Nil{}:
194      {==}
195    case h <> t:
196      %Laws.count_atoms_append(t, ys) : {1n+P.count_atoms(P.append_atoms(t, ys)) == 1n+_ : Nat}
197      {==}
198
199def Laws.count_flatten_eq(rs):
200  match rs:
201    case Nil{}:
202      {==}
203    case h <> +t:
204      match h:
205        case P.Residue{seq, +atoms}:
206          %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}
207          %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}
208          %Laws.add_comm(P.count_atoms(atoms), P.count_atoms_in(t)) : {Nat.add(P.count_atoms(atoms), P.count_atoms_in(t)) == _ : Nat}
209          {==}
210
211def Laws.complex_flatten_eq(chains):
212  %Laws.count_flatten_eq(P.flatten_chains_residues(chains)) : {_ == P.count_atoms(P.flatten_residues(P.flatten_chains_residues(chains))) : Nat}
213  {==}
214
215def Laws.pow10_3():
216  {==}
217
218def Laws.elem_iron():
219  {==}
220
221def Laws.elem_carbon():
222  {==}
223
224def Laws.atom_line_yes():
225  {==}
226
227def Laws.atom_line_no():
228  {==}
229
230def Laws.atom_lines_nil():
231  {==}
232
233def Laws.atom_lines_keep():
234  {==}
235
236def Laws.parse_f32_one():
237  {==}
238
239def Laws.parse_f32_neg():
240  {==}
241
242def Laws.parse_f32_bad():
243  {==}
244
245def Laws.pdb_num_atoms():
246  {==}
247
248def Laws.pdb_num_residues():
249  {==}
250
251def Laws.pdb_num_chains():
252  {==}
253
254def Laws.pdb_skipped_0():
255  {==}
256
257def Laws.pdb_skipped_1():
258  {==}
259
260def Laws.pdb_bad_atoms():
261  {==}
262
263def Laws.pdb_first_elem():
264  {==}
265
266def Laws.sasa_total_cons(h, t):
267  {==}
268
269def Laws.count_par4_nil(qp, c2):
270  {==}
271
272def Laws.count_par4_step(h1, h2, h3, h4, t, qp, c2):
273  {==}
274
275def Laws.count_par4_small(h, qp, c2):
276  {==}
277
278def Laws.lj_row_par4_nil(pi, eps, sig2, c2):
279  {==}
280
281def Laws.lj_row_par4_step(pi, eps, sig2, c2, h1, h2, h3, h4, t):
282  {==}
283
284def Laws.lj_row_par4_small(pi, eps, sig2, c2, h):
285  {==}
286
287def Laws.lj_eps_c():
288  {==}
289
290def Laws.lj_eps_h():
291  {==}
292
293def Laws.lj_sig_o():
294  {==}
295
296def Laws.lj_sig_default():
297  {==}
298
299def Laws.lj_row_elem_cons(si, pi, c2, h, t):
300  {==}
301
302def Laws.lj_total_elem_cons(h, t, ys, c2):
303  {==}
304
305def Laws.bond_total_nil(k):
306  {==}
307
308def Laws.bond_total_cons(xs, s1, s2, t, k):
309  {==}
310
311def Laws.angle_total_nil(k, eq):
312  {==}
313
314def Laws.angle_total_cons(xs, sa, sb, sc, t, k, eq):
315  {==}
316
317def Laws.pos_of_serial_none(s):
318  {==}
319
320def Laws.pos_of_serial_some():
321  {==}
322
323def Laws.bonded12_nil(a, b):
324  {==}
325
326def Laws.bonded12_hit():
327  {==}
328
329def Laws.bonded12_miss():
330  {==}
331
332def Laws.neighbors_one():
333  {==}
334
335def Laws.excluded13_one():
336  {==}
337
338def Laws.excluded_both():
339  {==}
340
341def Laws.flatten_bonds_one():
342  {==}
343
344def Laws.lj_row_excl_nil(si, pi, eps, sig2, c2, bonds):
345  {==}
346
347def Laws.lj_total_excl_nil(ys, eps, sig2, c2, bonds):
348  {==}
349
350def Laws.coul_row_excl_nil(si, pi, qi, ke, c2, bonds):
351  {==}
352
353def Laws.coul_total_excl_nil(ys, qs_e, ke, c2, bonds):
354  {==}
355
356def Laws.lj_row_elem_excl_nil(si, se, pi, c2, bonds):
357  {==}
358
359def Laws.lj_total_elem_excl_nil(ys, c2, bonds):
360  {==}
361
362def Laws.lj_row_elem_excl_hit():
363  {==}
364
365def Laws.lj_row_elem_excl_link():
366  {==}
367
368def Laws.conect_lines_nil():
369  {==}
370
371def Laws.conect_keep():
372  {==}
373
374def Laws.parse_conect_one():
375  {==}
376
377def Laws.parse_conect_none():
378  {==}
379
380def Laws.mass_c():
381  {==}
382
383def Laws.mass_h():
384  {==}
385
386def Laws.coul_frow_cons(pi, qi, ke, c2, h, t, qh, qt):
387  {==}
388
389def Laws.coul_forces_cons(h, t, qh, qt, ys, qs_e, ke, c2):
390  {==}
391
392def Laws.coul_frow_nil(pi, qi, ke, c2):
393  {==}
394
395def Laws.lj_row_pbc_cons(pi, eps, sig2, c2, box, h, t):
396  {==}
397
398def Laws.lj_total_pbc_cons(h, t, ys, eps, sig2, c2, box):
399  {==}
400
401def Laws.lj_row_pbc_nil(pi, eps, sig2, c2, box):
402  {==}
403
404def Laws.lj_frow_pbc_cons(pi, eps, sig2, c2, box, h, t):
405  {==}
406
407def Laws.lj_forces_pbc_cons(h, t, ys, eps, sig2, c2, box):
408  {==}
409
410def Laws.lj_forces_pbc_nil(ys, eps, sig2, c2, box):
411  {==}
412
413def Laws.cov_rad_c():
414  {==}
415
416def Laws.infer_row_nil(si, pi, ei):
417  {==}
418
419def Laws.infer_row_cons(si, pi, ei, h, t):
420  {==}
421
422def Laws.infer_total_nil():
423  {==}
424
425def Laws.bond_forces_nil(bonds, k):
426  {==}
427
428def Laws.bond_forces_cons(h, t, bonds, k):
429  {==}
430
431def Laws.dyn_of_atoms_nil():
432  {==}
433
434def Laws.dyn_of_atoms_cons(h, t):
435  {==}
436
437def Laws.dyn_atoms_nil():
438  {==}
439
440def Laws.vv_scale_nil(lam):
441  {==}
442
443def Laws.vv_scale_cons(h, t, lam):
444  {==}
445
446def Laws.vv_half_nil(dt):
447  {==}
448
449def Laws.vv_half_cons(h, t, dt):
450  {==}
451
452def Laws.vv_full_nil(dt):
453  {==}
454
455def Laws.vv_full_cons(h, t, dt):
456  {==}
457
458def Laws.ke_sim_nil():
459  {==}
460
461def Laws.md_run_zero(ds, qs, bonds, p, dt, tau, temp0, n):
462  {==}
463
464def Laws.min_run_zero(ds, qs, bonds, p, dt):
465  {==}
466
467
468def Laws.zero_charges_nil():
469  {==}
470
471def Laws.zero_charges_cons(h, t):
472  {==}
473
474def Laws.sd_norm_sweep_nil(dt):
475  {==}
476
477def Laws.maxforce2_nil():
478  {==}
479
480def Laws.dyn_set_force_nil(fs):
481  {==}
482
483def Laws.add_forces_nil():
484  {==}
485
486def Laws.add_forces_cons(x, xt, y, yt):
487  {==}
488
489def Laws.pairs_of_flat_nil():
490  {==}
491
492def Laws.pairs_of_flat_cons(x, y, t):
493  {==}
494
495def Laws.pad_left_golden():
496  {==}
497
498def Laws.pad_right_golden():
499  {==}
500
501def Laws.fmt_u32_golden():
502  {==}
503
504def Laws.elem_sym_golden():
505  {==}
506
507def Laws.tpl_has_bond_ala():
508  {==}
509
510def Laws.tpl_has_bond_miss():
511  {==}
512
513def Laws.tpl_has_bond_unknown():
514  {==}
515
516def Laws.tpl_has_bond_his():
517  {==}
518
519def Laws.tpl_row_nil(a):
520  {==}
521
522def Laws.tpl_row_cons(a, h, t):
523  {==}
524
525def Laws.tpl_total_nil():
526  {==}
527
528def Laws.parse_tpl_golden():
529  {==}
530
531def Laws.neighbors_except_golden():
532  {==}
533
534def Laws.fan_triples_golden():
535  {==}
536
537def Laws.angle_triples_auto_golden():
538  {==}
539