search

uwplse / pumpkin-pi

An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
MIT License
49 stars 9 forks source link

Support for lifting inductive relations #13

Closed nateyazdani closed 6 years ago

nateyazdani commented 6 years ago

This adds support for lifting inductive relations across an ornament for one of its index types. The Caching module was updated to expose declaration and look-up of liftings by global_reference, rather than a constr, in order to avoid universe complications when declaring the corresponding components of a lifted inductive relation and its base as liftings (see do_lift_ind in the Lift module). For the moment, the interface is a single Vernacular command Lift Inductive <base_ind> by <orn> <orn_inv> with <suffix>, where <suffix> is appended to the type/constructor names of <base_ind> to get the type/constructor names for the new inductive type. The file coq/Indtype.v gives examples of lifting inductive relations and then subsequently lifting proofs involving them.

nateyazdani commented 6 years ago

Right now, an inductive relation won't be automatically lifted while lifting a function or proof. Doing so requires choosing names for the lifted inductive relation's type and constructors, and there really isn't any good default.

All tests pass (sorry, meant to say that in the initial summary). I've tried to run the together.sh script a few times, but it keeps failing. I installed the datamash command, but now the script produces the following error output (seemingly near the end of the run):

head: illegal line count -- -1
head: illegal line count -- -1
head: illegal line count -- -1
head: illegal line count -- -1
head: illegal line count -- -1
head: illegal line count -- -1
head: illegal line count -- -1
sed: 1: "together/sizes.out": undefined label 'ogether/sizes.out'
sed: 1: "together/sizes.out": undefined label 'ogether/sizes.out'
Sanity checking out/inorder/avlUP100.out and out/inorder/avl100.out.
cat: out/inorder/avl100.out: No such file or directory

That aside, I've addressed all requested changes.

nateyazdani commented 6 years ago

Here are the run-time medians that I've managed to get from the script:

inorder-avl100 : 3
inorder-avl20 : 3
inorder-avl40 : 3
inorder-avl60 : 3
inorder-avl80 : 3
inorder-avlUP100 : 23949.5
inorder-avlUP20 : 38
inorder-avlUP40 : 450.5
inorder-avlUP60 : 3168.5
inorder-avlUP80 : 5844
inorder-baseUP100 : 0
inorder-baseUP10000 : 82.5
inorder-baseUP20 : 0
inorder-baseUP2000 : 14.5
inorder-baseUP40 : 0
inorder-baseUP4000 : 46.5
inorder-baseUP60 : 0
inorder-baseUP6000 : 47.5
inorder-baseUP80 : 0
inorder-baseUP8000 : 70.5
inorder-sized10000 : 93
inorder-sized2000 : 16.5
inorder-sized4000 : 38.5
inorder-sized6000 : 49.5
inorder-sized8000 : 64.5
inorder-sizedUP10000 : 152.5
inorder-sizedUP2000 : 26.5
inorder-sizedUP4000 : 54.5
inorder-sizedUP6000 : 124
inorder-sizedUP8000 : 114
postorder-avl100 : 3
postorder-avl20 : 3
postorder-avl40 : 3
postorder-avl60 : 3
postorder-avl80 : 3
postorder-avlUP100 : 24218
postorder-avlUP20 : 33.5
postorder-avlUP40 : 441
postorder-avlUP60 : 3150
postorder-avlUP80 : 5796.5
postorder-baseUP100 : 0
postorder-baseUP10000 : 110
postorder-baseUP20 : 0
postorder-baseUP2000 : 17.5
postorder-baseUP40 : 0
postorder-baseUP4000 : 31.5
postorder-baseUP60 : 0
postorder-baseUP6000 : 70.5
postorder-baseUP80 : 0
postorder-baseUP8000 : 62.5
postorder-sized10000 : 90.5
postorder-sized2000 : 16
postorder-sized4000 : 31
postorder-sized6000 : 58
postorder-sized8000 : 62.5
postorder-sizedUP10000 : 158
postorder-sizedUP2000 : 28
postorder-sizedUP4000 : 55
postorder-sizedUP6000 : 91
postorder-sizedUP8000 : 125.5
preorder-avl100 : 3.5
preorder-avl20 : 3
preorder-avl40 : 3
preorder-avl60 : 3
preorder-avl80 : 3
preorder-avlUP100 : 25850.5
preorder-avlUP20 : 49
preorder-avlUP40 : 481
preorder-avlUP60 : 3415
preorder-avlUP80 : 6334
preorder-baseUP100 : 0
preorder-baseUP10000 : 76.5
preorder-baseUP20 : 0
preorder-baseUP2000 : 18
preorder-baseUP40 : 0
preorder-baseUP4000 : 29.5
preorder-baseUP60 : 0
preorder-baseUP6000 : 45.5
preorder-baseUP80 : 0
preorder-baseUP8000 : 64.5
preorder-sized10000 : 120.5
preorder-sized2000 : 15
preorder-sized4000 : 38.5
preorder-sized6000 : 47
preorder-sized8000 : 78
preorder-sizedUP10000 : 160
preorder-sizedUP2000 : 29.5
preorder-sizedUP4000 : 55
preorder-sizedUP6000 : 90.5
preorder-sizedUP8000 : 141
search-avl100 : 10.5
search-avl20 : 3
search-avl40 : 4
search-avl60 : 5
search-avl80 : 7
search-avlUP100 : 5698.5
search-avlUP20 : 12
search-avlUP40 : 129
search-avlUP60 : 819.5
search-avlUP80 : 1526
search-baseUP100 : 9
search-baseUP20 : 3
search-baseUP40 : 4
search-baseUP60 : 5.5
search-baseUP80 : 6.5
tlringer commented 6 years ago

Ah, I just saw your comment: "Right now, an inductive relation won't be automatically lifted while lifting a function or proof. Doing so requires choosing names for the lifted inductive relation's type and constructors, and there really isn't any good default."

Sorry, getting used to this interface.

Please cut an issue for that.

nateyazdani commented 6 years ago

I opened an issue for automatic lifting of inductive relations during function/proof lifting, as requested. I'll respond to the other things inline.

nateyazdani commented 6 years ago

I think that I've followed up with all feedback; please let me know if I missed something.