search

RedPRL / redtt

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
Apache License 2.0
204 stars 12 forks source link

add tactics for box,cap #410

Closed ecavallo closed 5 years ago

cangiuli commented 6 years ago

Can this tactic just print "Why are you trying to input a box???" (I agree there should probably be a tactic, but have a hard time imagining people using it.)

ecavallo commented 6 years ago

I think it has come up at least once, though i forget where. cap might be useful in paths.s2...

favonia commented 6 years ago

Can this tactic just print "Why are you trying to input a box???" (I agree there should probably be a tactic, but have a hard time imagining people using it.)

We can have --expert mode. (OTOH --favonia will print out more trolling messages.) RedPRL/algaett#23

clayrat commented 5 years ago

One possible use-case is for https://github.com/RedPRL/redtt/pull/457. The idea there is that you prove a certain lemma by introducing a relation P : susp A -> susp A -> type on props A (where P(N,N)=(), P(N,S)=A, P(S,N)=A, P(S,S)=() and meridians map to univalences) and then showing it's reflexive, implies identity and so on. So for showing reflexivity, you need to construct (x : susp A) -> P x x, which is easy for poles, but in the case of a meridian you get a pretty big box made out of univalences in the type. I might be doing something wrong, but it seems that you need to provide a term for that box directly?

favonia commented 5 years ago

I realized there is an annoying technical issue: box is empirically different from comp because you cannot reorder its faces arbitrarily. The core language never allows permutation, but I want to hide this aspect if possible.