DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
150 Commits 1 Branch 0 Tags 2.2 MiB
c932210d37
Commit Graph

150 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Danila Fedorin
c932210d37 Re-expert monotonicity from Lattice 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-03 17:04:18 -08:00
Danila Fedorin
a8d26b1c48 Prove that join is monotonic in both arguments 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-03 16:51:57 -08:00
Danila Fedorin
2ddac38c3f Update with new changes to Agda 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-03 16:44:10 -08:00
Danila Fedorin
f00dabfc93 More cleanup to FiniteValueMap 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-02 16:23:33 -08:00
Danila Fedorin
01f4e02026 More cleanup to FiniteValueMap 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-02 16:05:42 -08:00
Danila Fedorin
fbbcd72037 Some early refactors of FiniteValueMap 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-02 15:18:10 -08:00
Danila Fedorin
03cdc65a7b Format AboveBelow a bit better (round two) 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-02 14:56:04 -08:00
Danila Fedorin
ec2b1ec3ba Format FiniteMap a little bit better 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-02 14:54:44 -08:00
Danila Fedorin
112dcb2208 Clean up AboveBelow slightly 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-02 14:34:15 -08:00
Danila Fedorin
8516f58b1d Remove helper comment. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-02 14:13:02 -08:00
Danila Fedorin
6cb6281bc2 Make main run the fixed point algorithm 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-01 23:42:10 -08:00
Danila Fedorin
0774946211 Expose decidability from Map modules 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-01 23:27:49 -08:00
Danila Fedorin
65d1590358 Prove monotonicity of lub in one argument 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-01 23:26:25 -08:00
Danila Fedorin
ae3e2c28b0 Create bundles and add a program to evaluate some code with finite maps 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-01 21:58:58 -08:00
Danila Fedorin
97a4165b58 Expose bundles from FiniteValueMap 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-01 21:35:40 -08:00
Danila Fedorin
754714d770 Restore bundles in IterProd 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-01 21:12:22 -08:00
Danila Fedorin
ae09a27f64 Prove that finite value-maps are finite height 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-01 21:03:23 -08:00
Danila Fedorin
ca90f6509c Re-write the IterProd proofs to couple lattice and finite height lattice 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-01 21:02:56 -08:00
Danila Fedorin
29898e738b Clean up a bit 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-01 19:08:29 -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
52e7a7a208 Prove distributivity in the other direction, too 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-01 19:07:59 -08:00
Danila Fedorin
8715d6d89c Finish proof of from distributivity 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-26 00:00:18 -08:00
Danila Fedorin
b083561629 Add most of the proof of from distributivity. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-25 20:28:07 -08:00
Danila Fedorin
3ad7db738a Prove that 'to' preserves equality 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-25 18:43:54 -08:00
Danila Fedorin
53a08b8f79 Prove that 'first' presrves equality 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-25 18:08:03 -08:00
Danila Fedorin
d6064ff752 Expose 'locate' and 'forget' from Map 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-25 18:07:50 -08:00
Danila Fedorin
d280f5afdf Make auxillary definitions private 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-25 14:06:45 -08:00
Danila Fedorin
b96bac5518 Prove the other direction for inverses. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-25 13:57:45 -08:00
Danila Fedorin
99fc21cef2 Expose 'subset-impl' from Map 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-25 13:57:28 -08:00
Danila Fedorin
2a06e6ae2d Adjust 'to' to make it easier to reason about 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-25 12:17:19 -08:00
Danila Fedorin
671ffc82df Define to-and-from functions from finite maps to tuples and prove one inverse direction 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-19 14:50:29 -08:00
Danila Fedorin
486b552b59 Try to generalize universe levels where possible 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-19 12:36:46 -08:00
Danila Fedorin
aafcb2683d Prove the transport of 'height lattice' property given an isomorphism 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-18 23:26:41 -08:00
Danila Fedorin
8c9f39ac35 Add some additional 'equivalence' definitions to Equivalence 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-18 21:46:42 -08:00
Danila Fedorin
6384f7006e Make 'lattice' public 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-18 20:18:38 -08:00
Danila Fedorin
b1c6b4c99a Expose bundles from Unit 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-11 21:20:05 -08:00
Danila Fedorin
5420bb808e Expose bundles from 'Prod' 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-11 21:16:41 -08:00
Danila Fedorin
4c0860f4c7 Expose bundle form MapSet 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-11 21:14:49 -08:00
Danila Fedorin
e89418d600 Expose bundle form 'Map' 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-11 21:12:49 -08:00
Danila Fedorin
bfb32092c2 Expose bundles and apply so renames to IterProd 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-11 21:10:51 -08:00
Danila Fedorin
6e26aa1580 Add a bundle to FiniteMap 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-11 21:02:43 -08:00
Danila Fedorin
27f40bd42e Add bundles to 'AboveBelow' 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-11 21:00:28 -08:00
Danila Fedorin
08f3f49640 Rename some definitions in Nat and expose bundle 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-11 20:56:21 -08:00
Danila Fedorin
a920608bef Tweak IterProd to expose more (including a bundle) 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-11 20:45:14 -08:00
Danila Fedorin
45f2babfa3 Fix typo in FixedHeightLattice definition 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-11 15:37:00 -08:00
Danila Fedorin
16c4d13242 Prove that iterated products are finite height 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-11 15:36:12 -08:00
Danila Fedorin
0ba4b46e16 Add proof of decidable equivalence for products 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-11 15:35:50 -08:00
Danila Fedorin
7e5cc1b316 Add an 'iterated product' lattice for A x A ... x A x B. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-11 14:19:41 -08:00
Danila Fedorin
33b7bc37f0 Add a 'FiniteHeightLattice' bundle 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-11 14:19:41 -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