Overlapping Names, Wrong number of args in Coq output from subrules

[JoeyEremondi]

Here's a minimal example displaying the problem:

metavar var, X ::=
   {{ coq nat }} {{ coq-equality }}

indexvar n ::=  {{ coq nat }}

grammar

Kind, K :: kind_ ::= {{ coq-equality  }}
  | KindStar :: :: KindStar 
 
typexpr, T :: T_ ::=    {{ coq-equality }}                   
    | X                   ::   :: var                     
    | ForAll << X1 , .. , Xn >> .  T            ::   :: polyarrow
    |  [ X1 |-> tau1 .. Xn |-> taun ] T        :: M :: tsub  {{ coq (tsubst_typexpr [[X1 |-> tau1 .. Xn |-> taun]] [[T]]) }}

tau :: tau_ ::=    
    | X                   ::   :: var   
    
    formula :: 'formula_' ::=
      | judgement           ::   :: judgement
      | formula1 .. formulan :: :: dots

    subrules
      tau <:: T

    substitutions
      multiple typexpr X  :: tsubst 

    defns
      Jtype :: '' ::=

    defn
        |- T : K :: :: kind :: Kind by
       
        ------------------------------------ :: Var
        |- T : KindStar
     
    defn
        |- T <: T' :: :: sub :: Sub by
 
        </ |-  taun : KindStar // n />
        ------------------------------------------ :: InstL
        |-  ForAll << </ Xn // n /> >> .  T  <: [ </ Xn |-> taun // n /> ] T 

The InstL rule generates pretty bizarre Coq output. It quantifies over a list of type (var*typexpr*typexpr), when it should quantify over (var*typexpr).

Additionally, the pattern matching functions use matches of the form (X_,tau_,tau_), which Coq errors on due to the repeated variable names.

The problem goes away when I remove tau as a subrule for typexpr and just make tau and typexpr synonyms, so it must be related to the subrule construct somehow. Similarly, the problem goes away if I remove the premise of the InstL rule. It's like the compiler can't figure out that the tau1...taun in the premise are the same as in the conclusion.

Here's the raw Coq output:

(* generated by Ott 0.27 from: minimalTest.ott *)

Require Import Arith.
Require Import Bool.
Require Import List.
Require Import Ott.ott_list_core.


Definition typvar := nat.
Lemma eq_typvar: forall (x y : typvar), {x = y} + {x <> y}.
Proof.
  decide equality; auto with ott_coq_equality arith.
Defined.
Hint Resolve eq_typvar : ott_coq_equality.
Definition n := nat.

Inductive typexpr : Set := 
 | T_var (X:typvar)
 | T_polyarrow (_:list typvar) (T:typexpr).

Inductive Kind : Set := 
 | kind_KindStar : Kind.
Lemma eq_typexpr: forall (x y : typexpr), {x = y} + {x <> y}.
Proof.
  decide equality; auto with ott_coq_equality arith.
Defined.
Hint Resolve eq_typexpr : ott_coq_equality.
Lemma eq_Kind: forall (x y : Kind), {x = y} + {x <> y}.
Proof.
  decide equality; auto with ott_coq_equality arith.
Defined.
Hint Resolve eq_Kind : ott_coq_equality.

(** subrules *)
Definition is_tau_of_typexpr (T5:typexpr) : bool :=
  match T5 with
  | (T_var X) => (true)
  | (T_polyarrow X_list T) => false
end.

(** library functions *)
Fixpoint list_assoc A B (eq:forall a b:A,{a=b}+{a<>b}) (x:A) (l:list (A*B)) {struct l} : option B :=
  match l with
  | nil => None
  | cons (a,b) t => if (eq a x) then Some b else list_assoc A B eq x t
end.
Implicit Arguments list_assoc.


(** substitutions *)
Fixpoint tsubst_typexpr (sub:list (typvar*typexpr)) (T_6:typexpr) {struct T_6} : typexpr :=
  match T_6 with
  | (T_var X) => (match list_assoc eq_typvar X sub with None => (T_var X) | Some T5 => T5 end)
  | (T_polyarrow X_list T) => T_polyarrow X_list (tsubst_typexpr sub T)
end.

(** definitions *)

(* defns Jtype *)
Inductive kind : typexpr -> Kind -> Prop :=    (* defn kind *)
 | KindVar : forall (T:typexpr),
     kind T kind_KindStar
with sub : typexpr -> typexpr -> Prop :=    (* defn sub *)
 | SubInstL : forall (X_tau_tau_list:list (typvar*typexpr*typexpr)) (T:typexpr),
     (Forall (fun (tmp_:(typvar*typexpr*typexpr)) => match tmp_ with (X_,tau_,tau_) => Is_true (is_tau_of_typexpr tau_) end) X_tau_tau_list) ->
     (Forall (fun (tmp_:(typvar*typexpr*typexpr)) => match tmp_ with (X_,tau_,tau_) => Is_true (is_tau_of_typexpr tau_) end) X_tau_tau_list) ->
     (forall tau_, In tau_ (map (fun (pat_: (typvar*typexpr*typexpr)) => match pat_ with (X_,tau_,tau_) => tau_ end) X_tau_tau_list) -> (kind tau_ kind_KindStar)) ->
     sub (T_polyarrow (map (fun (pat_:(typvar*typexpr*typexpr)) => match pat_ with (X_,tau_,tau_) => X_ end ) X_tau_tau_list) T)  (tsubst_typexpr  (map (fun (pat_:(typvar*typexpr*typexpr)) => match pat_ with (X_,tau_,tau_) => (X_,tau_) end ) X_tau_tau_list)   T ) .

[JoeyEremondi]

So, after some debugging/tracing, the source of the problem is at this line

The result of nt_or_mv_of_systerms looks like this:

(( X[0], None), (n) )
(( tau[0], None), (n) )
(( tau[0], (tau,)), (n) )

The same term (tau) appears in the list twice, but with different data for the subntr_data, causing some stage of the process to see them as different terms. This explains why it only happens with the subterm relationship, but I don't (yet) understand subntr_data well enough to know where the problem is originating.

I'll keep investigating, but hopefully this info is helpful to someone who knows Ott internals better than I do.

[JoeyEremondi]

Just to further add info, I've now found that the problem is that in [ </ Xn |-> taun // n /> ], tau is parsed into a St_nonterm instead of St_nontermsub. This happens regardless of whether dot or comprehension list forms are used.

[PeterSewell]

On 12 February 2018 at 01:48, Joey Eremondi ***@***.***> wrote: Just to further add info, I've now found that the problem is that in [ </ Xn |-> taun // n /> ], tau is parsed into a St_nonterm instead of St_nontermsub. This happens regardless of whether dot or comprehension list forms are used.

I've no time right now to really look into this, sorry. But it looks to me as if that is a correct parse wrt the grammar - the T_tsub production has taus not their super-nonterminal. That suggests there might be a bug in the bounds analysis code, failing to coalesce nonterminals that are used in multiple subrule ways like this.

…

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#26 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AErM5qwhhcdS_--dae5fwmvgcWqKE3-Kks5tT5hTgaJpZM4R78To> .