Respect for Functionality

[jozefg]

So this is a fun one. JonPRL's core sequence judgment is supposed to have a functionality requirement, essentially demanding that if H, x : A >> B(x) holds, then H >> B(a) = B(a') if H >> a = a' : A. Now if this isn't required all sorts of fun things can happen and currently it isn't.

The biggest offender that I'm aware of is creflexivity. It allows us to conclude that two variables are ceq when in fact they needn't be! f ~ f shouldn't hold if we're viewing f as a variable of type A -> B since we want to replace it with functions that are only pointwise equal.

I don't see an immediate good solution to this, we could require that creflexivity only apply to closed terms (really bad), we could add a goal forcing us to show that all the variables we assert are ceq are still ceq when replaced by only equal terms (my preferred option) or something else.

Thoughts?

[vrahli]

The problem is not creflexivity: x ~ x is true in any context because squiggle (and approximation) types are extensional. However, in a context where x : A -> B, you shouldn't be able to derive in general that x = x in Base (x ~ x is true though in that context). One rule which is not true in Nuprl is H |- x ~ x => H |- x = x in Base. Clearly, x : Top |- x ~ x is true but x : Top |- x = x in Base is not. Does that make sense?

(That shows that it would be great if we could link JonPRL to our Coq implementation. Someday I'll have time to actually work on that...)

On Tue, Sep 29, 2015 at 8:26 PM, Danny Gratzer notifications@github.com wrote:

So this is a fun one. JonPRL's core sequence judgment is supposed to have a functionality requirement, essentially demanding that if H, x : A >> B(x) holds, then H >> B(a) = B(a') if H >> a = a' : A. Now if this isn't required all sorts of fun things can happen and currently it isn't.

The biggest offender that I'm aware of is creflexivity. It allows us to conclude that two variables are ceq when in fact they needn't be! f ~ f shouldn't hold if we're viewing f as a variable of type A -> B since we want to replace it with functions that are only pointwise equal.

I don't see an immediate good solution to this, we could require that creflexivity only apply to closed terms (really bad), we could add a goal forcing us to show that all the variables we assert are ceq are still ceq when replaced by only equal terms (my preferred option) or something else.

Thoughts?

— Reply to this email directly or view it on GitHub https://github.com/jonsterling/JonPRL/issues/243.

http://www.cs.cornell.edu/~rahli/

[vrahli]

So basically MemberEq in refiner/rules/base.fun is not a valid rule.

On Tue, Sep 29, 2015 at 10:06 PM, vincent rahli vincent.rahli@gmail.com wrote:

The problem is not creflexivity: x ~ x is true in any context because squiggle (and approximation) types are extensional. However, in a context where x : A -> B, you shouldn't be able to derive in general that x = x in Base (x ~ x is true though in that context). One rule which is not true in Nuprl is H |- x ~ x => H |- x = x in Base. Clearly, x : Top |- x ~ x is true but x : Top |- x = x in Base is not. Does that make sense?

(That shows that it would be great if we could link JonPRL to our Coq implementation. Someday I'll have time to actually work on that...)

On Tue, Sep 29, 2015 at 8:26 PM, Danny Gratzer notifications@github.com wrote:

So this is a fun one. JonPRL's core sequence judgment is supposed to have a functionality requirement, essentially demanding that if H, x : A >> B(x) holds, then H >> B(a) = B(a') if H >> a = a' : A. Now if this isn't required all sorts of fun things can happen and currently it isn't.

The biggest offender that I'm aware of is creflexivity. It allows us to conclude that two variables are ceq when in fact they needn't be! f ~ f shouldn't hold if we're viewing f as a variable of type A -> B since we want to replace it with functions that are only pointwise equal.

I don't see an immediate good solution to this, we could require that creflexivity only apply to closed terms (really bad), we could add a goal forcing us to show that all the variables we assert are ceq are still ceq when replaced by only equal terms (my preferred option) or something else.

Thoughts?

— Reply to this email directly or view it on GitHub https://github.com/jonsterling/JonPRL/issues/243.

http://www.cs.cornell.edu/~rahli/

http://www.cs.cornell.edu/~rahli/

[jonsterling]

If nobody gets to it by the time I have time to do it, I'm going to replace Base.MemberEq with a rule (of variadic arity) that, for each premise in context, requires that it be a subtype of Base.

We'll then also probably want to add rules (whether primitive or derived) that express subtyping of Base for the common core types. @vrahli Does that sound all right?

(I am traveling for work this week, and next week I am visiting Bob's group at CMU; I may have time then, but am not sure what my activities will be at this point.)

[vrahli]

I've just finished proving rule_equal_in_base in https://github.com/vrahli/NuprlInCoq/blob/master/rules/rules_squiggle5.v. I'll work on adding this rule to JonPRL. My guess is that we only need two other rules: H x : Atom J |- x : Base and a similar one for Int.

On Wed, Sep 30, 2015 at 4:47 PM, Jonathan Sterling <notifications@github.com

wrote:

If nobody gets to it by the time I have time to do it, I'm going to replace Base.MemberEq with a rule (of variadic arity) that, for each premise in context, requires that it be a subtype of Base.

We'll then also probably want to add rules (whether primitive or derived) that express subtyping of Base for the common core types. @vrahli https://github.com/vrahli Does that sound all right?

(I am traveling for work this week, and next week I am visiting Bob's group at CMU; I may have time then, but am not sure what my activities will be at this point.)

— Reply to this email directly or view it on GitHub https://github.com/jonsterling/JonPRL/issues/243#issuecomment-144434505.

http://www.cs.cornell.edu/~rahli/

[jonsterling]

Ok, that sounds good! Just to reference it in this thread so that folks don't have to click through, the rule that will be added is:

   H |- a = b in Base
     By EqualInBase
     H |- a ~ b
     forall v in (free_vars a ++ free_vars b), H |- v in Base

We can add the following to the derivation calculus, I think:

datatype t = 
   (* ... *)
   | EQUAL_IN_BASE of int

fun arity (EQUAL_IN_BASE n) = #[0, n]

[vrahli]

Sorry, there was a mistake in my comment, the rule is actually

H |- a = b in Base By EqualInBase H |- a ~ b forall v in (free_vars a), H |- v in Base

i.e., we don't need to generate subgoals for the free variables of b.

The idea is that if you have to prove a = b in Base and you can prove

a ~ b, then first rewrite b into a in a = b in Base. You now have to

prove a = a in Base. To prove that a is in Base, it's enough to prove

that its free variables are all in Base.

Therefore, a simpler rule would be:

H |- a in Base By MemberOfBase forall v in (free_vars a), H |- v in Base

But I think the other one will be slightly easier to use.

On Wed, Sep 30, 2015 at 5:08 PM, Jonathan Sterling <notifications@github.com

wrote:

Ok, that sounds good! Just to reference it in this thread so that folks don't have to click through, the rule that will be added is:

H |- a = b in Base By EqualInBase H |- a ~ b forall v in (free_vars a ++ free_vars b), H |- v in Base

We can add the following to the derivation calculus, I think:

datatype t = (* ... *) | EQUAL_IN_BASE of int fun arity (EQUAL_IN_BASE n) = #[0, n]

— Reply to this email directly or view it on GitHub https://github.com/jonsterling/JonPRL/issues/243#issuecomment-144440658.

http://www.cs.cornell.edu/~rahli/

[jonsterling]

@vrahli Thanks for the clarification; definitely makes sense that we wouldn't have to prove it for FV(b)! This is the one, then:

   H |- a = b in Base
     By EqualInBase
     H |- a ~ b
     forall v in (free_vars a), H |- v in Base