RedPRL/sml-redprl

Dependent rewriting rule

Closed this issue · 10 comments

favonia commented

@cangiuli Is this true? This is probably the last step to finish semi-simplicial types.

G, a:A >> M = N in B
G >> P = Q in A
---------------------------------
G >> M[P/a] = N[Q/a] in B[P/a]
G >> M[P/a] = N[Q/a] in B[Q/a]

I wonder how to unify all the rewriting rules into one.

cangiuli commented

Unless I'm misreading, the first conclusion should be the substitution rule; G >> B[P/a] = B[Q/a] should also follow from the hypotheses, and the second conclusion should follow from the two previous facts. Is this not currently provable?

favonia commented

Probably not, but I am not sure. The current rewrite can only do a part or the whole judgment. Doing it part by part is doomed. Doing it as a whole will hit the well-formedness of equality types, which demands lots of well-typedness.

favonia commented

So, it seems this is the only structural rule that is not implemented in RedPRL yet, and I am stuck because of this.

Somehow we were able to merge all other substitution rules into one powerful rewrite. Not sure how to do this one.

favonia commented

By the way, I feel we should check other features of rewrite which are not listed in the papers.

jonsterling commented

@favonia I'm still a little confused; what's wrong with trying to rewrite one equality type to another? I imagine it does induce a lot of auxiliary subgoals, but aren't those somehow necessary?

favonia commented

Because those auxiliary goals are (probably) not provable in the current RedPRL, but in this case some of them are actually true, and we want them to be (easily) provable.

jonsterling commented

@favonia Re: the auxiliary subgoals, does your thesis have to do with the fact that for an express "Eq(A; M; N)" to be a type, it has to be true?

Let me describe systematically how I think one ought to be able to prove this:

  1. First show that B[P/a] = B[Q/a] type; this is provable using the existing rewrite, and the fact that B is a family of types (which we must have somewhere anyway).
  2. Next show that M[P/a] = N[P/a] in B[P/a]; this follows from functionality. Is this derivable in RedPRL? It at least seems like it must be admissible / derivable for each specific M,N,P.
  3. Next show that M[Q/a] = N[Q/a] in B[Q/a]; same as above.
  4. By transitivity and (1,2,3), we have either of the conclusions you wanted.

Does this make sense, or did I miss something?

favonia commented

How did you apply transitivity when M[P/a], N[P/a], M[Q/a] and N[Q/a] can all potentially differ? The difficulty will show up, for example, when you try to move from N[P/a] to N[Q/a]. You have to adjust other parts as well, and the current rewrite seems too weak.

jonsterling commented

I see what you mean, but I still think this is provable by several rewrites. I believe that having to do several rewrites is dumb, though, and we should maybe have a better rule that can do it all at once (somehow).

favonia commented

Maybe, but again I do not see how to prove that using the current rewrite.