% consistency.elf
%
% Contents:
%
%   1. Tedious reasoning-by-contradiction lemmas.
%   2. consistency (single-step)
%   3. consistency* (multi-step)
%

absurdity/step* :
   % If
         absurd
      -> {E1 : exp}
   % then
         step* E1 E2
    -> type.
%mode   absurdity/step* +Absurd +E1 -X.
%worlds ()     (absurdity/step* _ _ _).
%total  Absurd (absurdity/step* Absurd _ _).


absurdity/step*2 :
   % If
        absurd
     -> {E1 : exp}
   % then
        is-value V2
     -> step* E1 V2
   -> type.
%mode   absurdity/step*2 +Absurd +E1 -IsVal -Step*.
%worlds ()     (absurdity/step*2 _ _ _ _).
%total  Absurd (absurdity/step*2 Absurd _ _ _).


absurdity/elab :
   % If
        absurd
     -> {E : exp} {A : ty} {M : tm}
   % then
        elab E A M
 -> type.
%mode absurdity/elab +Absurd +E +A +M -X.
%worlds ()     (absurdity/elab _ _ _ _ _).
%total  Absurd (absurdity/elab Absurd _ _ _ _).


%
% Consistency theorem
%
consistency :
  % If
      {Elab : elab E A M}     % . |- e : A \elto M
      {P : pacifier}          % unsound workaround; see base.elf
      steptm M M'             % M \steptm M'
  % then
   -> step* E E'              % e \stepe e'
   -> elab E' A M'            % e' : A \elto M'
 -> type.
%mode consistency +Elab +Pacifier +Steptm
                  -Steps -Elab2.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  Cases for   elab/sectintro
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

- :
      consistency (elab/sectintro Elab1 Elab2)
                  P
                  (steptm/pair1 Step1)
                  (step*/left (step/split) Step*1M)
                  (elab/sectintro (elab/merge1 Elab1') (elab/merge2 Elab2))
   <- consistency Elab1 P Step1 (Step*1 : step* E E1') Elab1'
   <- step*merge1 E Step*1 Step*1M.

- :
      consistency (elab/sectintro Elab1 Elab2)
                  P
                  (steptm/pair2 _ Step2)
                  (step*/left (step/split) Step*2M)
                  (elab/sectintro (elab/merge1 Elab1) (elab/merge2 Elab2'))
   <- consistency Elab2 P Step2 (Step*2 : step* E E2') Elab2'
   <- step*merge2 E Step*2 Step*2M.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  Cases for   elab/sectelim{1,2}
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- :
       consistency (elab/sectelim1 Elab) P (steptm/fst0 Step) Steps (elab/sectelim1 Elab')
    <- consistency Elab P Step Steps Elab'.

- :
       consistency (elab/sectelim1 Elab)
                   _
                   (steptm/fst (is-valuetm/pair _ IsValtm2))
                   Step*
                   ElabOut
     <-
       elab-sect _ Elab _ Step* ElabOut _ _ _.


- :
       consistency (elab/sectelim2 Elab) P (steptm/snd0 Step) Steps (elab/sectelim2 Elab')
    <- consistency Elab P Step Steps Elab'.

- :
       consistency (elab/sectelim2 Elab)
                   _
                   (steptm/snd (is-valuetm/pair _ IsValtm2))
                   Step*
                   ElabOut
     <-
       elab-sect _ Elab _ _ _ _ Step* ElabOut.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  Cases for   elab/merge{1,2}
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

- :
       consistency (elab/merge1 Elab1) P Step (step*/left (step/unmerge left) Step*) Elab
    <- consistency Elab1 P Step Step* Elab.

- :
       consistency (elab/merge2 Elab2) P Step (step*/left (step/unmerge right) Step*) Elab
    <- consistency Elab2 P Step Step* Elab.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  Cases for   elab/unintro{1,2}
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- :
       consistency (elab/unintro1 Elab) P (steptm/inl0 Step) Steps (elab/unintro1 Elab')
    <- consistency Elab P Step Steps Elab'.
- :
       consistency (elab/unintro2 Elab) P (steptm/inr0 Step) Steps (elab/unintro2 Elab')
    <- consistency Elab P Step Steps Elab'.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  Cases for   elab/fix
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 - :
       consistency (elab/fix Elab1)
                   _
                   (steptm/fix)
                   (step*/left (step/fix) step*/zero)
                   (Elab1 _ _ (elab/fix Elab1)).



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  Cases for   elab/unintro{1,2}
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- :
       consistency (elab/unintro1 Elab) P (steptm/inl0 Step) Steps (elab/unintro1 Elab')
    <- consistency Elab P Step Steps Elab'.
- :
       consistency (elab/unintro2 Elab) P (steptm/inr0 Step) Steps (elab/unintro2 Elab')
    <- consistency Elab P Step Steps Elab'.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  Cases for   elab/unelim  and  elab/direct
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

consistency/unelim-case0 :
   {Fill : fill EC EH}
      consistency (elab/unelim Fill Elab0 Elab1 Elab2)
                  P
                  (steptm/case0 Step0)
                  Step*
                  (elab/unelim Fill Elab0' Elab1 Elab2)
   <-
      consistency Elab0 P Step0 Step*0 Elab0'
   <-
      step*eval-context _ _ Step*0 _ Fill Step*
   .

consistency/unelim-case1 :
   {Fill : fill EC EH}
       consistency (elab/unelim Fill Elab0 Elab1 Elab2)
                   P
                   (steptm/case1 IsValM00)
                   (step*/zero)
                   (Elab1 _ _ Elab00)
    <-
       elab-inl Elab0 Elab00
    .

consistency/unelim-case2 :
   {Fill : fill EC EH}
       consistency (elab/unelim Fill Elab0 Elab1 Elab2)
                   P
                   (steptm/case2 IsValM00)
                   (step*/zero)
                   (Elab2 _ _ Elab00)
    <-
       elab-inr Elab0 Elab00
    .


consistency/direct-arg :
       consistency (elab/direct Fill Elab0 Elab1)
                   P
                   (steptm/app2 _ Step0)
                   Step*
                   (elab/direct Fill Elab0' Elab1)
    <-
       consistency Elab0 P Step0 Step*0 Elab0'
    <-
       step*eval-context _ _ Step*0 _ Fill Step*
    .

consistency/direct-let-beta :
       consistency (elab/direct Fill Elab0 Elab1)
                   P
                   (steptm/beta IsValM0)
                   (step*/zero)
                   (Elab1 _ _ Elab0)
    .


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  Cases for   elab/arrelim
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


consistency/app-contradiction :
      consistency (elab/arrelim Elab1 Elab2) _ (steptm/app2 IsValtm1 Step2) Steps Elab2'
   <- value-mono IsValtm1 Elab1 _ Elab1' MidpointIsVal NotApp
   <- app-not-app NotApp ABSURDITY
   <- absurdity/step* ABSURDITY (app (app E11 E12) E2) Steps
   <- absurdity/elab  ABSURDITY _ _ _ Elab2'.

- :
      consistency (elab/arrelim Elab1 Elab2) P (steptm/app2 IsValtm1 Step2) StepsApp (elab/arrelim Elab1' Elab2')
   <- value-mono IsValtm1 Elab1 Steps1 Elab1' IsVal1 NotApp
   <- step*app1 _ Steps1 StepsApp1
   <- consistency Elab2 P Step2 Steps2 Elab2'
   <- step*app2 _ IsVal1 Steps2 StepsApp2
   <- step*append StepsApp1 StepsApp2 StepsApp.

%
% The next two cases use `pacify' to convince Twelf that
%
%     elab/arrelim Elab1 Elab2
%
% is smaller than
%
%     elab/arrelim (elab/merge1 Elab1) Elab2
% and
%     elab/arrelim (elab/merge2 Elab1) Elab2.
%

- :
       consistency (elab/arrelim (elab/merge1 Elab1) Elab2) P
                   Steptm
                   (step*/left (step/app1 (step/unmerge left)) Step*)
                   ElabOut
    <- pacify P Psmall                   % unsafe, depends on %trustme; see base.elf
    <- 
       consistency (elab/arrelim Elab1 Elab2) Psmall
                   Steptm Step* ElabOut.

- :
       consistency (elab/arrelim (elab/merge2 Elab1) Elab2) P
                   Steptm
                   (step*/left (step/app1 (step/unmerge right)) Step*)
                   ElabOut
    <- pacify P Psmall                  % unsafe, depends on %trustme; see base.elf
    <-
       consistency (elab/arrelim Elab1 Elab2) Psmall
                   Steptm Step* ElabOut.


consistency/app/app1 :
       consistency (elab/arrelim D1 D2) P (steptm/app1 Step1) StepsOut (elab/arrelim D1' D2)
    <- consistency D1 P Step1 Steps D1' 
    <- step*app1 _ Steps StepsOut.


consistency/app/beta  : 
   {Efun : exp} {Earg : exp} {Ebody : exp -> exp} {Varg : exp}
      {StepsApp : step* (app Efun Earg) (app (lam Ebody) Varg)}
      {IsValArg : is-value Varg}
      {StepsAppBeta : step* (app Efun Earg) (Ebody Varg)}
      {StepsFunApp : step* (app Efun Earg) (app (lam Ebody) Earg)}
      {StepsArgApp : step* (app (lam Ebody) Earg) (app (lam Ebody) Varg)}
      {StepsArg : step* Earg Varg}
      {Marg : tm}  {A : ty}  {IsValMarg : is-valuetm Marg}
      {Elab2 : elab Earg A Marg}
      {Elab2' : elab Varg A Marg}
      {NotApp : exp-not-app Earg}
      {StepsFun : step* Efun (lam Ebody)}
      {B : ty} {Mbody : tm -> tm}
      {Elab1 : elab Efun (arr A B) (lamtm Mbody)}
      {ElabBody : {e : exp} {m : tm}
                  elab e A m -> elab (Ebody e) B (Mbody m)}

         consistency (elab/arrelim Elab1 Elab2) P (steptm/beta IsValMarg) StepsAppBeta (ElabBody Varg Marg Elab2')
%
% Function could be a merge; use "elab-arr" to step it to a lambda:
%
      <-
         elab-arr Elab1
                  (StepsFun  :  step* Efun (lam ([x:exp] Ebody x)))
                  (ElabBody : {e:exp} {m:tm} elab e A m -> elab (Ebody e) B (Mbody m))
      <-
         step*app1 Earg
                   StepsFun
                   (StepsFunApp %{ : step* (app Efun Earg) (app (val (lam ([x:exp] Ebody x))) Earg) }%  )
%
% Argument could be a merge; use "value-mono" to get StepsArg
%
    <- value-mono IsValMarg Elab2 StepsArg Elab2' IsValArg NotApp
    <- step*app2 _ (is-value/lam) StepsArg StepsArgApp
%
% Step the function, then step the argument...
%
    <- step*append StepsFunApp StepsArgApp StepsApp
    <-
%
% ...and finally, add a step/beta.
%
         step*snoc StepsApp
                   (step/beta IsValArg : step (app (lam ([x:exp] Ebody x)) (Varg)) (Ebody (Varg)))
                   StepsAppBeta
    .


%worlds ()              (consistency _ _ _ _ _).
%total  {Pacifier Elab} (consistency Elab Pacifier Step _ _).
      % lexicographic ordering, Pacifier first


%
% consistency*: extending consistency to multiple steps resulting in a value
%
consistency* :
   % If
         elab E A M
      -> is-valuetm W
      -> steptm* M W
   % then
      -> step* E V
      -> is-value V
      -> elab V A W
    -> type.

%mode consistency* +ElabE +IsValtm +Stepstm
                   -Steptm -IsVal -ElabV.


consistency*/zero :

         consistency* ElabE IsValtm steptm*/zero Steps1 IsVal ElabE'
      <- value-mono IsValtm ElabE Steps1 ElabE' IsVal _.


consistency*/left :

        consistency* ElabE IsValtm (steptm*/left Steptm Stepstm) Steps IsVal ElabV
     <- consistency ElabE pacifier/i Steptm Steps1 ElabE'
     <- consistency* ElabE' IsValtm Stepstm Steps2 IsVal ElabV
     <- step*append Steps1 Steps2 Steps.

%worlds ()      (consistency* _      _       _       _ _ _).
%total  Stepstm (consistency* ElabE IsValtm Stepstm  _ _ _).