DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
101 Commits 1 Branch 0 Tags 1.6 MiB
6fe8dc2a02
Commit Graph

101 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Danila Fedorin
66dfe14207 Prove that restrict needs the key in both maps 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-08-04 00:07:10 -07:00
Danila Fedorin
56147cfc82 Implement map intersection 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-08-03 23:46:26 -07:00
Danila Fedorin
7e1f70210b Remove trailing space 2023-07-30 22:26:05 -07:00
Danila Fedorin
77e2572157 Tweak the style of the Semilattice instance 2023-07-30 21:50:28 -07:00
Danila Fedorin
1b7a3f02eb Add an instance of Semilattice for Map. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-30 20:36:19 -07:00
Danila Fedorin
a4eaa6269f Prove idempotence 2023-07-30 20:11:02 -07:00
Danila Fedorin
fceee34cee Finish associativity proof 2023-07-30 19:54:38 -07:00
Danila Fedorin
eca6181494 List all the cases for the other direction 2023-07-30 19:25:46 -07:00
Danila Fedorin
2c839db924 Prove associativity of maps (in one direction) 2023-07-30 19:09:16 -07:00
Danila Fedorin
1e4e8000cf Rename union-preserves to properly match what's being preserved 2023-07-30 17:57:06 -07:00
Danila Fedorin
70b85c99cc Rename the new provenance type and remove the old version 2023-07-30 16:45:02 -07:00
Danila Fedorin
de2f202bdf Use an expression-based provenance to make enumerating cases easier 
This should come in handy for the associativity proof.
 2023-07-30 16:43:07 -07:00
Danila Fedorin
6039c1dfab Rename 'merge' to 'union' 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-30 15:18:09 -07:00
Danila Fedorin
d786e6bf48 Eschew proof-by-symmetry 2023-07-30 14:16:35 -07:00
Danila Fedorin
af0066eaa7 Rearrange a few functions 2023-07-30 13:49:38 -07:00
Danila Fedorin
eaee73236f More tweaks to naming and style 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-30 13:46:52 -07:00
Danila Fedorin
26db4cc86c Remove unnecessary -right prefix in theorem name. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-30 13:21:03 -07:00
Danila Fedorin
b066db9829 Use inferred variables for proofs where possible 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-30 13:19:15 -07:00
Danila Fedorin
4033a1b33d Prove most of commutativity by relying on in-dec. 
The "no" case still needs to be dismissed, but that can probably
be done by some lemma about keys in maps.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-28 00:05:41 -07:00
Danila Fedorin
77b8b6fad9 Finally prove the provenance properties of merge. 2023-07-26 20:58:41 -07:00
Danila Fedorin
461732244a Finish all in/not-in proofs. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-26 20:40:28 -07:00
Danila Fedorin
12217e6928 Reformat the code to roughly fit into 80 columns. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-26 17:31:09 -07:00
Danila Fedorin
489b0532df Add intermediate state for insertion proofs 2023-07-25 22:58:42 -07:00
Danila Fedorin
6b51cd4050 Reorganize a bit and start on provenance 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-25 19:56:47 -07:00
Danila Fedorin
88a712fa98 Implement the more powerful Map-functional theorem 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-25 18:22:24 -07:00
Danila Fedorin
c9ab1152c4 Minor cleanup of Map module 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-25 00:10:57 -07:00
Danila Fedorin
850984ec15 Do away with implicit arguments in some places where they can't be inferred 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-24 23:58:14 -07:00
Danila Fedorin
4aea9a0358 Migrate Maps to including a uniqueness proof 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-24 23:55:09 -07:00
Danila Fedorin
c2bc1c5421 Move the implementation details into a private module 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-24 23:12:04 -07:00
Danila Fedorin
232bd65809 Add uniqueness preservation proof for merge 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-24 23:02:43 -07:00
Danila Fedorin
87a476ab9e Add proofs of uniqueness preservation for map insert 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-24 22:51:40 -07:00
Danila Fedorin
c50195942d Start moving away from purely list-based maps. 
The eventual goal is to make a map be a list and a proof
that all the keys are unique.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-24 20:38:34 -07:00
Danila Fedorin
f2e72b54ce Define unique as a data type to match stdlib All and Any 2023-07-23 21:34:24 -07:00
Danila Fedorin
d9c18fe483 Prove that maps are functional assuming uniqueness 2023-07-23 17:50:25 -07:00
Danila Fedorin
ab7ed2039a Add a generic Map module and prove its induced equivalence relation 2023-07-23 00:51:34 -07:00
Danila Fedorin
8febffc8e3 Add an equivalence constraint on lattice relations. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-15 15:16:51 -07:00
Danila Fedorin
971d75bb2b Parameterize by equivalence type 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-15 14:40:11 -07:00
Danila Fedorin
46ff4465f2 Git rid of the bundles (for now) use IsWhatever 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-15 13:12:21 -07:00
Danila Fedorin
7b993827bf Delete the unneeded <= relation from instances 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-15 12:18:50 -07:00
Danila Fedorin
09d2125aea Add note to self 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-14 22:45:17 -07:00
Danila Fedorin
cdca2528e9 Add a lattice instance for products 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-14 21:49:47 -07:00
Danila Fedorin
3b29ee0f74 Add a Semilattice isntance for Products. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-14 21:20:16 -07:00
Danila Fedorin
1ee6682c1a Factor the Semilattice instances for Nat into their own module 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-14 19:59:07 -07:00
Danila Fedorin
c9b514e9af Add a preorder instance for product 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-14 19:42:29 -07:00
Danila Fedorin
2b3d429631 Get started on a semilattice instances for products 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-14 18:42:29 -07:00
Danila Fedorin
bac68b95f1 Add a Lattice instance for natural numbers. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-14 18:18:17 -07:00
Danila Fedorin
c6dddb177e Get started on a lattice instance for naturals. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-13 23:22:29 -07:00
Danila Fedorin
422ea93edb Finish up the Nat semilattices 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-07-13 21:55:51 -07:00
Danila Fedorin
97a3f25fd2 [WIP] Start lattice and semilattice proofs for Nat 2023-04-06 23:08:49 -07:00
Danila Fedorin
8b805be9d3 Add a map from natural numbers for use as a lattice transformer 2023-04-04 21:08:41 -07:00