Case where both meta-substitutions associated with context variables are not pattern substitutions should not happen

[andreasabel]

% Strong normalization for simply-typed lambda-calculus in Beluga

LF ty : type =
  | base : ty
  | arr  : ty -> ty -> ty
  ;
%name ty A.

LF tm : ty -> type =
  | abs : (tm A -> tm B) -> tm (arr A B)
  | app : tm (arr A B) -> tm A -> tm B
  ;
%name tm M.

schema cxt = tm A; % some [a : ty] block tm a;

LF step : tm A -> tm A -> type =
  | rbeta : step (app (abs M) N) (M N)
  | rabs  : ({x : tm A} step (M x) (M' x)) -> step (abs M) (abs M')
  | rappl : step M M' -> step (app M N) (app M' N)
  | rappr : step N N' -> step (app M N) (app M N')
  ;

% Lemma: If [ρ]M ⇒ M' then M ⇒ N and M' = [ρ]N.

inductive ExStep : (g1 : cxt) (g2 : cxt)
  {M : [g1 |- tm A[]]} {#R : [g2 |-# g1]} {M' : [g2 |- tm A[]]} ctype =
  | Ex : [g1 |- step M N] -> ExStep [g1 |- M] [g2 |- #R] [g2 |- N[#R]]
  ;

rec invRenStep : {g1 : cxt} {M : [g1 |- tm A[]]} {#R : [g2 |-# g1]}
    [g2 |- step M[#R] M'] -> ExStep [g1 |- M] [g2 |- #R] [g2 |- M'] =
  / total m (invRenStep g1 g2 a m) /
  mlam g1, M, #R => fn s =>

  %% We would like to split on s, but limitations of Beluga force us
  %% to go the longer route and split on M, such that the renaming
  %% is pushed inside.
  case [ g1 |- M ] of

    %% Case application
    | [g1 |- app M1 M2] =>

      let ih : {#R : [g2 |-# g1]}  [g2 |- step (M1[#R]) M'] ->
               ExStep [g1 |- M] [g2 |- #R] [g2 |- M']
             = invRenStep [g1] [g1 |- M1] in

      %% We case on the function part.
      (case [g1 |- M1] of

      %% Case beta-redex
      | [g1 |- abs \ x. M1'] => (case s of
        %% We either contract the beta-redex...
        | [g2 |- rbeta] => Ex [g1 |- rbeta]
        %% ... or reduce in the left or right subterm
        | [g2 |- rappl S] =>
            let Ex [g1 |- S'] = ih [g2 |- #R] [g2 |- S]
              %% invRenStep [g1] [g1 |- M1] [g2 |- #R] [g2 |- S]
            in  Ex [g1 |- rappl S' ]
        | [g2 |- rappr S] =>
            let Ex [g1 |- S'] = invRenStep [g1] [g1 |- M2]  [g2 |- #R] [g2 |- S]
            in  Ex [g1 |- rappr S' ]
        )

      %% Case not beta-redex
      | [g1 |- M1] => (case s of
        %% We either reduce in the left subterm ...
        | [g2 |- rappl S] =>
            let Ex [g1 |- S'] = invRenStep [g1] [g1 |- M1] [g2 |- #R] [g2 |- S]
            in  Ex [g1 |- rappl S' ]
        %% ... or in the right subterm.
        | [g2 |- rappr S] =>
            let Ex [g1 |- S'] = invRenStep [g1] [g1 |- M2] [g2 |- #R] [g2 |- S]
            in  Ex [g1 |- rappr S' ]
        )
      )

    %% Case abstraction: reduction is in function body.
    | [g1 |- abs \x. M1] => let [g2 |- rabs \y. S] = s in
          let Ex [g1, x : tm A[] |- S'] =
            invRenStep [g1, x : tm _]
              [g1, x : tm _ |- M1] [g2, x : tm _ |- #R[..], x] [g2, y : tm _ |- S ] in
          Ex [g1 |- rabs \x. S']

    % Case variable: does not reduce
    | [g1 |- #p ] => impossible s
  ;