 Danila Fedorin
|
a081edb881
|
Add a proof about filter's distributivity
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-09 23:06:49 -07:00 |
|
Danila Fedorin
|
be50c76cb1
|
Add more higher-order primitives
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-04-30 21:56:34 -07:00 |
|
Danila Fedorin
|
112a5087ef
|
Tentative start on proving correctness
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-04-30 19:20:02 -07:00 |
|
Danila Fedorin
|
ccb7abc501
|
Remove unused code from Utils
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-04-30 19:15:38 -07:00 |
|
Danila Fedorin
|
91b5d108f6
|
Simplify proofs about 'loop' using concatenation lemma
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-04-29 21:28:21 -07:00 |
|
Danila Fedorin
|
c00c8e3e85
|
Use different graph operations to implement construction
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-04-25 23:10:41 -07:00 |
|
Danila Fedorin
|
4fe0d147fa
|
Adjust 'Program' to have a graph and basic blocks
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-04-13 13:39:15 -07:00 |
|
Danila Fedorin
|
d4b0796715
|
Intermediate commit. Switch to *-based definition of <=.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-04-07 19:51:59 -07:00 |
|
Danila Fedorin
|
b505063771
|
Start working on proofs of Graph-related things
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-04-04 20:34:28 -07:00 |
|
Danila Fedorin
|
f21ebdcf46
|
Start working on the evaluation operation.
Proving monotonicity is the main hurdle here.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-10 18:13:01 -07:00 |
|
Danila Fedorin
|
1ccc6f08e5
|
Add more properties of uniqueness
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-09 13:54:01 -08:00 |
|
Danila Fedorin
|
332b7616cf
|
Prove that foldr is monotonic when input lists are pairwise monotonic
This should help prove that "join" is monotonic
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-07 21:53:45 -08:00 |
|
Danila Fedorin
|
3a537f54ba
|
Add a helpful utility function
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-01 19:08:11 -08:00 |
|
Danila Fedorin
|
6fe8dc2a02
|
Add an 'iterate' function to Utils
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-02-11 14:19:41 -08:00 |
|
Danila Fedorin
|
2b27e397b6
|
Add another utility proof
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-02-11 12:45:33 -08:00 |
|
Danila Fedorin
|
d718338759
|
Clean up 'Map' to hide implementation details, extract code
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-02-10 16:51:43 -08:00 |