search

jonsterling / JonPRL

An proof refinement logic for computational type theory. Inspired by Nuprl. [For up-to-date development, see JonPRL's successor, RedPRL: https://github.com/redprl/sml-redprl]
http://www.jonprl.org
MIT License
109 stars 9 forks source link

Simplified inconsistent DecideEq rule #234

Closed jozefg closed 8 years ago

jozefg commented 8 years ago

This is one fix for #233. Instead of taking this C parameter we don't do that and instead just force the user to prove that each branch is equal at T.

This should be fine though because we give them this assumption of equality so in theory they can use that to vary T depending on what branch they're proving things in.

jonsterling commented 8 years ago

Huh! I didn't realize we could do that, but I guess it makes sense. I wonder if it is possible to similarly simplify the analogous rules (natrec-eq or neigh-ind-eq, etc.).

jozefg commented 8 years ago

@jonsterling It seems possible.. Or we could error on the side of more convenient for the user and make DecideEq complicated in the same way that those are. Either seems reasonable to me.

jozefg commented 8 years ago

Here's a quick demonstration of handling dependence with this rule

Theorem not-uhoh : [
  (x : unit + void) member(decide(x; a.a; b.b); decide(x; a.unit; b.void))
] {
  auto; eq-cd [unit, void]; auto;

  hyp-subst → <eq> [h.=(_; _; decide(h; _._; _._))];
  aux { elim #4; reduce; auto };

  reduce; auto
}.
jonsterling commented 8 years ago

I think it looks fine, in theory. Let's use sums as a way to test how this works out in practice, and if it doesn't result in much extra user-level complication, we can change the other rules to be like this.

jozefg commented 8 years ago

@jonsterling Sounds good to me!

jonsterling commented 8 years ago

I'll merge this once Travis succeeds—for some reason, our builds seem to be waiting a long time in their queue.