Equality Rules about uframeit

[Jazzpirate]

Ah, I see :) Well, two things:

1. Implicit morphisms will not do that, what you're talking about are basically implicit coercions: A term of type <Point, Point> can be coerced to have type Line and you want that coercion to happen implicitly. Florian has toyed around with implicit coercions before, but integrating them properly into the Solver is really difficult, so that idea was shelved for now. However, that is from the point of view of MMT. I would guess that that coercion would have to happen at a much earlier stage already, since I'm pretty sure FrameIT (the Unity-component, I mean) has to have some basic mechanism to assign things-in-the-game-world to parameters-of-a-scroll such that the game itself already doesn't allow you to map two points to a line in the scroll. Given an MMT-function LineConstructor: Point -> Point -> Line, which probably already exists, the game would already have to take care of inserting that constructor appropriately anyway, before MMT comes into play at all. Not sure if that is a solution for what you have in mind, since it implies moving some part of the logic to the Game away from MMT. But:
2. This is a slightly different problem from the original one. The original problem is about making MMT aware of the fact that two lines are logically equal. Your new problem is about coercing two things that have different types to have the same type and be equal.

[ComFreek]

For FrameWorld-1 the equality rules contributed by @Jazzpirate seem to be sufficient and a good solution. I still wonder why they don't work - as in not being picked up by the typechecker when proving judgements.
I think one of us would need to debug this, I could do this at the end of this week. (Please ping if I forget.)

For the general case, I still believe in having "implicit scroll conversions" (private bluenote). There I describe how we could use implicit morphisms if we modelled facts with theories & structures thereof. However, with that we cannot control which implicit morphisms are available in which level. This is something we need from a didactic's/game's POV.

@Jazzpirate In Coq, if you use the auto tactic to automatically solve proof goals, you can give it a database (auto myLocalDb) which records which lemmas you want it to try out. Does it make sense to having something similar here? Conceptually, probably yes. How so in the implementation?

[Jazzpirate]

I think one of us would need to debug this, I could do this at the end of this week. (Please ping if I forget.)

What makes this difficult for me is that the theories where they don't work are virtual/generated. If someone could dump them into an MMT-file that would make things a lot easier...

@ComFreek I'm slightly confused as to what in the FrameIT-MMT pipeline would be analogous to that...? The type-checking rules that the solver uses are determined by the theory that provides the context, and it uses all of them.

I just noticed one minor thing - the part where the rule isn't-but-should-be used is in a view, right? Does the theory that declares the view (Vectors3D or something like that) contained in the Meta-Theory of both domain and codomain of the view? If not, that could be a problem...

[ComFreek]

@richardmarcus Can you disable the now included permutation hack again, perhaps under a flag --disable-hack? Then I think we (I) can reconstruct the theories and view manually.

@Jazzpirate Re the auto part: afaik implicit morphisms are picked as they are checked. Let i: T' -> T be an implicit morphism known to MMT. Then, when typechecking a view v: S -> T, I can use T'-expressions in the RHS of the view assignments, right? And that I cannot prevent until I delete i: T' ->T entirely from the archive, right?

[Jazzpirate]

@ComFreek

Let i: T' -> T be an implicit morphism known to MMT. Then, when typechecking a view v: S -> T, I can use T'-expressions in the RHS of the view assignments, right?

Yes. More precisely: You have to be able to use T'-expressions in the RHS, since all T'-expressions are perfectly valid T-expressions.

And that I cannot prevent until I delete i: T' ->T entirely from the archive, right?

...thus changing T. The presence of the implicit morphism determines the valid syntax and semantics of T. What may not ever happen is that an implicit morphism T'->T exists, but T' is not used in checking an expression against T...

I still don't quite understand what you're aiming at though, sorry. Could you elaborate how that connects to the problem with the equality rules?

[ComFreek]

At first, we had to give slot assignments exactly in the form the scroll asks for. The equality rules you implemented were supposed to alleviate this problem by allowing slightly different assignments, namely dist b a to dist a b. I propose to go further and more general.

For example, let the scroll ask for a fact of type LineSegment (cf. ProblemTheory below). The user, however, would like to input two point facts instead.

(copied from my private bluenote)

theory LineSegment =
  start: vector |
  direction: normalizedVector |
  length: R |
|||

theory ProblemTheory =
  structure lineSegment : ?LineSegment = ||
|||

theory TwoPoints =
  a: vector ||
  b: vector ||
|||

implicit view v: ?LineSegment -> ?TwoPoints =
  start = a ||
  direction = normalize (b - a) ||
  length: norm (b - a) ||
|||

To allow this behavior of the user, I thought implicit morphisms were the right tool (cf. v above): every model of the codomain TwoPoints induces the the view a model of the domain LineSegment - exactly the semantics we want. But perhaps they are not the righ tool after all.

Conceptually, if a scroll asks for a fact of (model) type S and to his knowledge so far (e.g. on a per-level basis) allows conversion of T-models to S-models (via a view S -> T), then the user should be allowed to give a fact of (model) type T instead.