path_via vs. transitivity

[JasonGross]

Continuing from @mikeshulman's https://github.com/HoTT/HoTT/pull/451#issuecomment-54104523:

I don't understand why we are so cavalier about replacing a tactic that's used throughout the library by a tactic that does something different. I think we should revert this change and then continue the discussion about the advantages and disadvantages of all possible options before making a decision.

My experience suggests that even if we manage to make transitivity "pretend" that it is just concat, eventually it will bite someone somewhere.

Also, there's undoubtedly a reason why we added auto with path_hints to path_via. Is the questionable advantage of calling the tactic "transitivity" worth having to type that manually every time we need it?

I'm weakly-to-moderately in favor of minimizing changes from the standard library of Coq. I predict that the difference between transitivity and concat will show its teeth when we start talking about paths between paths between paths, and try to rewrite with things there; we generally don't build paths with tactics, only paths between paths, and the syntactic difference won't really show up except in rewrite, I think. In this case, I have a simpl rewrite tactic in Tactics.v which will run simpl before doing the rewrite, and if we mark transitivity by Arguments transitivity A R _ / _ _ _ _ _., then I think we'll be fine.

[mikeshulman]

I think we build paths with tactics all the time. And while I think there is some value in trying to reuse definitions from the standard library, I see little value in forcing ourselves to use the same tactics as in the standard library, if we can define other tactics more specifically suited to our needs.

[JasonGross]

I think the value in keeping tactics from the standard library is ease of adjustment for people coming from vanila Coq. The fewer new names they have to learn, the easier things will be.

I'd prefer to wait until we're actually facing problems due to syntactic differences, and then use those examples to drive decisions away from compatibility.

[mikeshulman]

For the sake of argument, have a look at 964e409: it's possible to have the tactic be called transitivity and still produce (in the case of paths) terms that are literally concat without unfolding. I'm not necessarily sure that this is the right approach, but it's something to consider.

(I did have to change a couple of the proofs in Bool.v, for reasons I don't entirely understand, but I don't think that's a bad thing; I found the original proofs pretty incomprehensible.)

[JasonGross]

I do not approve of 964e40968c941d4d2fcf5aab322c198b49f1dbaf. For one thing, the first will swallow error messages that might be useful, and give the unhelpful "no applicable tactic" or something similar instead. For another, I'm uncomfortable adding special cases in this manner.

I'd suggest using cbn or simpl to unfold the proof terms before using them, instead.

(I don't understand why you had to change those proofs, either; you don't need to, it seems, on the most recent trunk. (However, the most recent trunk breaks things in hit/Connectedness.v and causes a universe inconsistency in V.v, which was the source of my email to coq-club. It's still not clear to me if this is a genuine universe inconsistency or not, though I manged to work around bug 3559.))

[JasonGross]

If you want, I can make a pull request from 34d3e42b7f998a0f0a65f4d6a899d7634d00ad8e / my trans-concat branch.

[mikeshulman]

Your objection to 964e409 is fair; I just wanted to get us started thinking about other options. I'll have a look at your trans-concat branch, feel free to make a PR too if you want.

[JasonGross]

I'm weakly against having transitivity insert concat as a proof term; I'm generally a fan of compatibility where there's no strong reason to give it up. I'll make my branch a pull request if anyone requests me to, but I'm not going to do it unless asked. (It also breaks an apply in Flattening.v, which will need to be replaced by a refine. I'm still tracking down a small example to make a bug report, and I don't want to commit the work-around until I have a bug-tracker-number to reference.)

[mikeshulman]

By "compatibility" you mean having transitivity insert the same proof terms as the one in the standard library, i.e. without unfolding? Is there any real incompatibility though, since the terms are definitionally equal?

[JasonGross]

Yes, that's almost what I mean by compatibility. What I actually mean is "I want to depend as little as possible on differences from vanilla Coq". My perspective is, I think, "it'd be nice to reduce the number of things we redefine as Coq catches up with HoTT". That's why I'd be ~completely happy with a patch like

Infix "@" := (@transitivity _ _ _ _ _ _).
Notation "p ^" := (@symmetry _ _ _ _ _ p).
Notation "1" := (@reflexivity _ _ _ _).

where we're only changing display/parsing, and slightly less happy with a patch that changes the behavior of standard Coq tactics in a systematic way, and even less happy with a patch that changes the behavior of standard Coq tactics in an ad-hoc way.

[JasonGross]

In any case, though, this feels like a discussion mostly about style or bikeshedding, so I'm fine with submitting my branch as a pull request, and also fine with acceding to whatever the popular opinion says. (So far, @mikeshulman and I have been the only ones saying things. Do others have opinions?)

I may want to revisit this if and when Coq gets a standard library compatible with Set Universe Polymorphism, Set Primitive Projections and -indices-matter; I'd probably have stronger opinions then.

[JasonGross]

I've fixed the issue with Flattening.v; the problem was that my cbn was simplifying the argument to paths, which apply's unification couldn't handle. I've added an extra change in the tactics to fix this.

[mikeshulman]

My main worry about defining @ to mean transitivity is that some day far in the future, some poor schmuck (like me) is going to get stuck with the dreaded "unable to unify terms that look the same" error because one term has a transitivity in it and the other has a concat. Or something like that. So I'd be happier with your version where transitivity does an unfolding to insert concats.

I don't see much value in leaving standard things alone for its own sake. Smoothing the transition for standard Coqers is something tangible, but that's mostly satisfied as long as we name the tactic transitivity, whatever it does under the hood. If and when the Coq standard library becomes usable for HoTT, then that would be a horse of a different color, because we'd get some real benefit from using it. (That day seems to me to still be a ways off, though, if for no other reason than that the standard library is suffused with Prop.)

But I'd be very interested to hear opinions from anyone else!

[andrejbauer]

We have our own definition of equality, and we are unlikely to switch to the standard library in the near future. Therefore, it's not so strange to have our own proof of concatenation of paths. Now, it might be nice for the Coq folks to all the proof term transitivity or whatever it is called in the standard library. On the other hand, it might be beter to call it concat in order to emphasize the geometric view.

[spitters]

The tactics rewrite, reflexivity, symmetry and transitivity all fall back to the setoid versions. These versions should give the expected proof terms. @mattam82 made a recent generalization with rewriting in Type, so this should now also work with the HoTT equality. I haven't checked this yet.

On Wed, Sep 3, 2014 at 12:38 PM, Andrej Bauer notifications@github.com wrote:

We have our own definition of equality, and we are unlikely to switch to the standard library in the near future. Therefore, it's not so strange to have our own proof of concatenation of paths. Now, it might be nice for the Coq folks to all the proof term transitivity or whatever it is called in the standard library. On the other hand, it might be beter to call it concat in order to emphasize the geometric view.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/454#issuecomment-54278856.

[mikeshulman]

So @andrejbauer and @spitters , what specifically are you proposing?

[spitters]

To check whether the standard (type class based) tactics actually do what we want, as conjectured by @mattam82.

On Wed, Sep 3, 2014 at 4:21 PM, Mike Shulman notifications@github.com wrote:

So @andrejbauer https://github.com/andrejbauer and @spitters https://github.com/spitters , what specifically are you proposing?

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/454#issuecomment-54304273.

[mikeshulman]

Okay, maybe you could do that then? I'm a bit doubtful that the setoid versions will be any better; won't we just get terms involving Setoid_transitivity instead of transitivity?

[andrejbauer]

But surely the issue is not whether the proof term is called transitivity or concat (irrelevant), but what the transitivity tactic does, no?

[mikeshulman]

It's not irrelevant what the proof term is called; I want to be able to look at a proof term and see it written readably with @.

[JasonGross]

I'd give 95% probability to the tactics inserting typeclass names. There's been no reason in the past to care about proof terms like this, and no need to clutter Coq's code with such proof term manipulation. (And, often, I'll care more about it being fast than about what term it generates.)

@mikeshulman, what do you think of never using concat and inverse explicitly, and instead always using transitivity and symmetry, via the notations @ and ^?

[mikeshulman]

@JasonGross I might be okay with that. We could even turn it around: rather than defining the transitivity instance for paths to mean concat, we could define it directly (with the same definition we currently give for concat) and then define concat to mean transitivity.

[spitters]

It looks like this is already what we are doing, the Instances are there in Overture.

One experiment in Universe.v path_universe_V_uncurried shows that the proof term has a part: transitivity (path_universe_uncurried (equiv_inverse ((idmap o equiv_path A B) p))) p^

Class Transitive {A} (R : relation A) := transitivity : forall x y z, R x y -> R y z -> R x z.

This may indeed not what we want.

@mattam82 ?

On Wed, Sep 3, 2014 at 5:48 PM, Mike Shulman notifications@github.com wrote:

Okay, maybe you could do that then? I'm a bit doubtful that the setoid versions will be any better; won't we just get terms involving Setoid_transitivity instead of transitivity?

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/454#issuecomment-54317787.

[mikeshulman]

No, it is not what we are already doing.

[JasonGross]

@spitters, @mikeshulman is suggesting, I think,

Arguments transitive {A R _ x y z} _ _.

Instance transitive_paths {A} : Transitive (@paths A) | 0
  := fun x y z (p : x = y) (q : y = z) => match p, q with idpath, idpath => idpath end.

Arguments transitive_paths {A x y z} p q : simpl nomatch.

Notation concat := (transitivity (R := @paths _)) (only parsing).
Notation "@ 'concat'" := (fun A => @transitivity _ (@paths A) _ _ _ _) (only parsing).

Infix "@" := (@transitivity _ _ _ _ _ _).

(untested) There might be a few issues to be solved involving behavior of simpl.

[andrejbauer]

One important point of HoTT is that it is proof relevant. An early version of the HoTT library used fancy tactics heavily. We had to get rid of that and we inserted a lot of proof terms "by hand". Currently it seems that we are using more and more of the type class machinery. I would in general be weary of losing control over the proof terms, or using tactics that generate unreadable proof terms even in simple cases. For instance, if there are four layers of type classes on top of something as simple as concat, and special tricks need to be played before Coq reveals the "true" proof term, then I'd consider that a drawback. We should actually look at typical proofs, as they are constructed, and see if we can understand them.

[mikeshulman]

@andrejbauer I agree.

[spitters]

Thanks, I may find the time to look at it tomorrow.

On Wed, Sep 3, 2014 at 7:15 PM, Jason Gross notifications@github.com wrote:

@spitters https://github.com/spitters, @mikeshulman https://github.com/mikeshulman is suggesting, I think,

Arguments transitive {A R x y z} _. Instance transitive_paths {A} : Transitive (@paths A) | 0 := fun x y z (p : x = y) (q : y = z) => match p, q with idpath, idpath => idpath end. Arguments transitivepaths {A x y z} p q : simpl nomatch. Notation concat := (transitivity (R := @paths )) (only parsing).Notation "@ 'concat'" := (fun A => @transitivity (@paths A) _) (only parsing).

Infix "@" := (@transitivity ). `(untested) There might be a few issues to be solved involving behavior ofsimpl`.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/454#issuecomment-54331770.

[spitters]

I wonder how difficult it is to use emacs to turn Coq into something like agda, i.e. to use Show Proofs to convert an unfinished tactic proof into a proof term.

On Wed, Sep 3, 2014 at 8:14 PM, Andrej Bauer notifications@github.com wrote:

One important point of HoTT is that it is proof relevant. An early version of the HoTT library used fancy tactics heavily. We had to get rid of that and we inserted a lot of proof terms "by hand". Currently it seems that we are using more and more of the type class machinery. I would in general be weary of losing control over the proof terms, or using tactics that generate unreadable proof terms even in simple cases. For instance, if there are four layers of type classes on top of something as simple as concat, and special tricks need to be played before Coq reveals the "true" proof term, then I'd consider that a drawback. We should actually look at typical proofs, as they are constructed, and see if we can understand them.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/454#issuecomment-54341038.

[spitters]

This looks very finicky. Even if I put in the term printed for concat literally: Instance transitivepaths {A} : Transitive (@paths A) | 0:= fun (x y z : A) (p : x = y) (q : y = z) => match p in ( = a) return (a = z -> x = z) with | idpath => fun q0 : x = z => match q0 in (_ = a) return (x = a) with | idpath => idpath end end q.

Definition concat_pV_p {A : Type} {x y z : A} (p : x = z) (q : y = z) : (p @ q^) @ q = p := (match q as i return forall p, (p @ i^) @ i = p with idpath => fun p => match p with idpath => 1 end end) p.

breaks with

Error: Illegal application: The term "transitivity" of type "forall (A : Type) (R : relation A), Transitive R -> forall x y z : A, R x y -> R y z -> R x z" cannot be applied to the terms "A" : "Type" "paths" : "A -> A -> Type" "transitive_paths" : "Transitive paths" "x" : "A" "y" : "A" "y" : "A" "p1" : "x = y0" "1^" : "y = y" The 7th term has type "x = y0" which should be coercible to "x = y".

However, the one build by tactics works:

destruct q. destruct p. reflexivity. Show Proof. (match q as p0 in ( = y0) return (forall p1 : x = y0, (p1 @ p0^) @ p0 = p1) with | 1 => fun p0 : x = y => match p0 as p1 in ( = y0) return ((p1 @ 1^) @ 1 = p1) with | 1 => 1 end end p)

This doesn't look like progress to me, but I am probably overlooking something.

On Wed, Sep 3, 2014 at 10:57 PM, Bas Spitters b.a.w.spitters@gmail.com wrote:

Thanks, I may find the time to look at it tomorrow.

On Wed, Sep 3, 2014 at 7:15 PM, Jason Gross notifications@github.com wrote:

@spitters https://github.com/spitters, @mikeshulman https://github.com/mikeshulman is suggesting, I think,

Arguments transitive {A R x y z} _. Instance transitive_paths {A} : Transitive (@paths A) | 0 := fun x y z (p : x = y) (q : y = z) => match p, q with idpath, idpath => idpath end. Arguments transitivepaths {A x y z} p q : simpl nomatch. Notation concat := (transitivity (R := @paths )) (only parsing).Notation "@ 'concat'" := (fun A => @transitivity (@paths A) _) (only parsing).

Infix "@" := (@transitivity ). `(untested) There might be a few issues to be solved involving behavior ofsimpl`.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/454#issuecomment-54331770.

[andrejbauer]

I don't think anyone has the expectation that Coq can parse its own input. That's never been the case. What we want is proof terms that are not obfuscated by stuff.

[spitters]

OK. I could try and go ahead, but would be inclined to refold explicit proof terms with the tactic script. destruct q. destruct p. reflexivity. is more readable than: (match q as p0 in ( = y0) return (forall p1 : x = y0, (p1 @ p0^) @ p0 = p1) with | 1 => fun p0 : x = y => match p0 as p1 in ( = y0) return ((p1 @ 1^) @ 1 = p1) with | 1 => 1 end end p)

What do you think?

On Thu, Sep 4, 2014 at 1:10 PM, Andrej Bauer notifications@github.com wrote:

I don't think anyone has the expectation that Coq can parse its own input. That's never been the case. What we want is proof terms that are not obfuscated by stuff.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/454#issuecomment-54454296.

[andrejbauer]

I have no idea what we're discussing at this point. What are you doing?

[spitters]

@andrejbauer I was trying the approach using the type class rewriting with the changes suggested by @JasonGross below. It works to some extent, but seems to require more elaborated proof terms.

On Wed, Sep 3, 2014 at 7:15 PM, Jason Gross notifications@github.com wrote:

@spitters https://github.com/spitters, @mikeshulman https://github.com/mikeshulman is suggesting, I think,

Arguments transitive {A R x y z} _. Instance transitive_paths {A} : Transitive (@paths A) | 0 := fun x y z (p : x = y) (q : y = z) => match p, q with idpath, idpath => idpath end. Arguments transitivepaths {A x y z} p q : simpl nomatch. Notation concat := (transitivity (R := @paths )) (only parsing).Notation "@ 'concat'" := (fun A => @transitivity (@paths A) _) (only parsing).

Infix "@" := (@transitivity ). `(untested) There might be a few issues to be solved involving behavior ofsimpl`.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/454#issuecomment-54331770.

[mikeshulman]

I still have no idea what you're doing. What do you mean by 'works'? What is 'type class rewriting'? On Sep 4, 2014 6:14 AM, "Bas Spitters" notifications@github.com wrote:

@andrejbauer I was trying the approach using the type class rewriting with the changes suggested by @JasonGross below. It works to some extent, but seems to require more elaborated proof terms.

On Wed, Sep 3, 2014 at 7:15 PM, Jason Gross notifications@github.com wrote:

@spitters https://github.com/spitters, @mikeshulman https://github.com/mikeshulman is suggesting, I think,

Arguments transitive {A R x y z} _. Instance transitive_paths {A} : Transitive (@paths A) | 0 := fun x y z (p : x = y) (q : y = z) => match p, q with idpath, idpath => idpath end. Arguments transitivepaths {A x y z} p q : simpl nomatch. Notation concat := (transitivity (R := @paths )) (only parsing).Notation "@ 'concat'" := (fun A => @transitivity (@paths A) _) (only parsing).

Infix "@" := (@transitivity ). `(untested) There might be a few issues to be solved involving behavior ofsimpl`.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/454#issuecomment-54331770.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/454#issuecomment-54473262.

[JasonGross]

@spitters, I suspect the issue is that typechecking fails without typeclass resolution, but typeclass resolution resolves too much. What happens if you replace (@transitivity _ _ _ _ _ _). with (@transitivity _ _ (@transitive_paths _) _ _ _).?

@mikeshulman, you said:

We could even turn it around: rather than defining the transitivity instance for paths to mean concat, we could define it directly (with the same definition we currently give for concat) and then define concat to mean transitivity.

I think @spitters is attempting to push this change through the HoTT library and seeing how much it breaks (thanks!, Bas), based on the code I suggested at https://github.com/HoTT/HoTT/issues/454#issuecomment-54331770.

[andrejbauer]

I prefer to do homotopy type theory without magic.

[spitters]

I just got it to work. Will send a pull request soon.

On Thu, Sep 4, 2014 at 7:25 PM, Andrej Bauer notifications@github.com wrote:

I prefer to do homotopy type theory without magic.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/454#issuecomment-54513515.

[mikeshulman]

(For what it's worth, I consider the fact that Coq can't parse its own output to be a serious flaw, even if it's not likely to change soon.)

[mikeshulman]

@andrejbauer, do you have a specific proposal? Would you rather not use transitivity at all and go back to path_via?

[spitters]

It can (usually) if you use Set Printing All, but you may not want to do that.

On Thu, Sep 4, 2014 at 7:33 PM, Mike Shulman notifications@github.com wrote:

(For what it's worth, I consider the fact that Coq can't parse its own output to be a serious flaw, even if it's not likely to change soon.)

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/454#issuecomment-54514632.

[mikeshulman]

Usually, but not always. There ought to be a guaranteed way to get parseable output.

[spitters]

Sorry, I accidentally push to the main repo directly, will try to clean it up.

On Thu, Sep 4, 2014 at 7:34 PM, Mike Shulman notifications@github.com wrote:

@andrejbauer https://github.com/andrejbauer, do you have a specific proposal? Would you rather not use transitivity at all and go back to path_via?

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/454#issuecomment-54514768.

[spitters]

It is now here, will create a pull request soon. https://github.com/spitters/HoTT

Will git push -f origin 7cecb7c6e878686f6c21a8e66008efd8a5a6c3a8 reset the main repo to Mike's commit before mine?

Sorry for the mistake.

On Thu, Sep 4, 2014 at 7:38 PM, Mike Shulman notifications@github.com wrote:

Usually, but not always. There ought to be a guaranteed way to get parseable output.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/454#issuecomment-54515320.

[JasonGross]

@spitters, I'd use git push -f origin 7cecb7c:master to be sure, but I think your line will work too.

[spitters]

Few

On Thu, Sep 4, 2014 at 7:45 PM, Jason Gross notifications@github.com wrote:

@spitters https://github.com/spitters, I'd use git push -f origin 7cecb7c:master to be sure, but I think your line will work too.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/454#issuecomment-54516254.

[JasonGross]

With regard to reversibility of parsing, I think you'll also need a different universe representation, or the parser will need to accept universe names with dots; Type@{Top.1} isn't parseable. I've reported a bug. Did you have another example in mind where Set Printing All. Set Printing Depth 10000 (* or some other absurdly large number *). isn't sufficient to get parseable output?

[mikeshulman]

not off the top of my head.

[andrejbauer]

It's not really the user's task to explain what needs to be done to get parseable output. There simply should be a way to do it.

[spitters]

About using transitivity. HoTT is about the equivalence of = and <~>.

Compare: Require Import HoTT. Lemma path_trans {A B C:Type}: A=B -> B=C -> A=C. intros. by transitivity B. Show Proof. (* (fun (A B C : Type) (X : A = B) (X0 : B = C) => X @ X0) *) Qed.

Lemma equiv_trans {A B C}: A<~>B -> B <~>C -> A<~>C. intros. by transitivity B. Show Proof. (* (fun (A B C : Type) (X : A <~> B) (X0 : B <~> C) => transitivity X X0) *) Qed.

Using the notation (as in 9d6e15b43583bbfe93424a743c23c6814b1bbfbf) Infix "@" := (@transitivity ) (at level 20). we get: (fun (A B C : Type) (X : A <~> B) (X0 : B <~> C) => X @ X0)

[mikeshulman]

Closed by #459