[locally-nameless] disable emitting lc constraints for some rules

[rogerbosman]

I have an environment equivalence judgment that contains a rule that states that if two environments are equivalent, we can cons a binding on both and they will be equivalent:

E1 equiv E2
----------------------------- Var
E1; x : Sch equiv E2; x : Sch

The algorithm as described here will emit lc constraints "to guarantee the invariant that if a derivation holds, then the top-level terms involved are locally-closed". As we are in a System F-alike system with both term and type variables in locally nameless representation in this case this means adding a lc constraint on the typescheme Sch.

Inductive EnvEquiv : Env -> Env -> Prop :=    (* defn EnvEq *)
 | EnvEqVar : forall (Env1:Env) (x:termvar) (Sch5:Sch) (Env2:Env),
     lc_DSch Sch5 ->
     EnvEq Env1 Env2 ->
     EnvEq (Env_ConsVar Env1 x Sch5) (Env_ConsVar Env2 x Sch5)

The problem is that this invariant is only maintained for rules, and not for the environment itself. Therefore, environments may exist that store some open term, which means the equivalence relation now no longer is reflexive, since that would involve the case forall E1 E2 x Sch, E1 equiv E2 ==> E1; x : Sch equiv E2; x : Sch.

I would argue that the solution for this is to add a way for the lc constraints to not be generated for some rules. Two environments can be equivalent whilst storing terms that are not locally closed, as long as both store the same open term. Alternatively, this can be solved by also emitting lc constraints for the constructors of the environments, but I'm not sure that makes a lot of sense.

[sweirich]

I've found that one way to suppress lc constraints is to add the following formula:

 | nolc A                  :: M :: nolcA
    {{ tex }}
    {{ coq True }}

Then adding this formula to a hypothesis in a rule (as below) will supress the generation of that constraint.

psi1 <= psi2
  W1 <= W2
  x notin dom W1
  x notin dom W2
  nolc A
------------------------------------ :: ConsTm
  W1 ++ x:psi1 A <= W2 ++ x : psi2 A

I generally do this only for "auxiliary" relations --- those that aren't used to specify the system, but only exist to prove some property about it. Another alternative is to add an lc precondition to lemmas such as reflexivity. These preconditions are not difficult to satisfy because all judgements should imply that their constituents are locally closed.

[sweirich]

BTW, I've done this enough that I would like Ott to be able to take care of this supression without adding the trivial "True" precondition to my rules. I'm commenting here to show that that a workaround exists, but also that I have encountered the same issue.

[rogerbosman]

Thanks for your workaround, that works, although it has the trivial True like you describe

[rogerbosman]

I closed the issue by mistake, apologies