search

DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq
MIT License
198 stars 50 forks source link

Heterogeneous relations-related files from prop_typ formalization #188

Closed euisuny closed 3 years ago

euisuny commented 3 years ago

As requested from need in HELIX proofs.

This is a series of files that characterize heterogeneous relations, i.e. relations of type forall A B, A -> B -> Prop, and related category theory formalizations.

Tagging @YaZko for review.

YaZko commented 3 years ago

Thanks for the PR @euisuny!
We need to clean up redundant definitions notably in Basics.Basics, and double check that using the HeterogeneousRelations module instead directly works out before merging.

I'm a little bit worried about subrelationH being a class too, I don't remember why we did that but that's almost certainly a bad idea, I think we'll have to change that as well before merging.

euisuny commented 3 years ago

@YaZko Made the changes, there are some mysterious rewrite looping cases again.

Specifically, this occurs in:

  1. Eq/Eq.v rewrite looping in hypothesis -- resolved by using forward reasoning (assert).
  2. Interp/HandlerFacts.v L189 -- resolved with Typeclasses eauto := 7. (5 or 6 doesn't work. :\ ) Modulo these hacks, everything seems to work fine now.
YaZko commented 3 years ago

@euisuny Thanks! However I don't think we can afford to push diverging instances in Master. I'll take a look later this morning at the culprits and see if I can find a non-hacky way to resolve them.

YaZko commented 3 years ago

I fixed the few issues I could see, that looks good to me.

@Lysxia : Do you want to double check the patch seems fine to be merged in master or should we go ahead?