Click on a command or tactic to see a detailed view of its use.

Specification "trans".

Import "util". [View util]

% Evaluation lemmas
Theorem nstep_is_nat : forall N M M',
  {nstep N M M'} -> {is_nat N}.
induction on 1. intros. case H1.
  search.
  apply IH to H3. search.
Theorem nstep'_is_nat : forall N M M',
  {nstep' N M M'} -> {is_nat N}.
induction on 1. intros. case H1.
  search.
  apply IH to H3. search.
Theorem val'_step'_absurd : forall V M,
  {val' V} -> {step' V M} -> false.
induction on 1. intros. case H1.
  case H2.
  case H2.
  case H2. backchain IH. backchain IH with V = V2. 
  case H2.
  case H2. backchain IH. backchain IH with V = E.
 
Theorem step'_det : forall M N N',
  {step' M N} -> {step' M N'} -> N = N'.
induction on 1. intros. case H1.
  % Case: pred'-1
  case H2.
    apply IH to H3 H4. search.
    case H3.
  % Case : pred'-2
  case H2.
    case H4.
    apply npred_det to H3 H4. search.
  % Case: plus'-1
  case H2.
    apply IH to H3 H4. search.
    apply val'_step'_absurd to H4 H3.
    case H3.
  % Case: plus'-2
  case H2.
    apply val'_step'_absurd to H3 H5.
    apply IH to H4 H6. search.
    case H4.
  % Case: plus'-3
  case H2.
    case H4.
    case H5.
    apply add_det to H3 H4. search.
  % Case: ifz'-1
  case H2.
    apply IH to H3 H4. search.
    case H3.
    case H3.
  % Case: ifz'-2
  case H2.
    case H3. 
    search.
  % Case: ifz'-3
  case H2.
    case H3.
    search.
  % Case: pair'-1
  case H2.
    apply IH to H3 H4. search.
    apply val'_step'_absurd to H4 H3.
  % Case: pair'-2
  case H2.
    apply val'_step'_absurd to H3 H5.
    apply IH to H4 H6. search.
  % Case: fst'-1
  case H2.
    apply IH to H3 H4. search.
    apply val'_step'_absurd to H4 H3.
  % Case: fst'-2
  case H2.
    apply val'_step'_absurd to H3 H4.
    search.
  % Case: snd'-1
  case H2.
    apply IH to H3 H4. search.
    apply val'_step'_absurd to H4 H3.
  % Case: snd'-2
  case H2.
    apply val'_step'_absurd to H3 H4.
    search.
  % Case: let'-1
  case H2.
    apply IH to H3 H4. search.
    apply val'_step'_absurd to H4 H3.
  % Case: let'-2
  case H2.
    apply val'_step'_absurd to H3 H4.
    search.
  % Case: app'-1
  case H2.
    apply IH to H3 H4. search.
    apply val'_step'_absurd to H4 H3.
    case H3.
  % Case: app'-2
  case H2.
    apply val'_step'_absurd to H3 H5.
    apply IH to H4 H6. search.
    apply val'_step'_absurd to H5 H4.
  % Case: app'-3
  case H2.
    case H4.
    apply val'_step'_absurd to H3 H5.
    search.
  % Case: clos'-1
  case H2.
    apply IH to H3 H4. search.
    apply val'_step'_absurd to H4 H3.
  % Case: clos'-2
  case H2.
    apply val'_step'_absurd to H3 H5.
    apply IH to H4 H6. search.
  % Case: open'-1
  case H2.
    apply IH to H3 H4. search.
    apply val'_step'_absurd to H4 H3.
  % Case: open'-2
  case H2.
    apply val'_step'_absurd to H3 H4.
    search.
   
Theorem nstep'_val'_det : forall N1 N2 M V1 V2,
  {val' V1} -> {val' V2} -> {nstep' N1 M V1} -> {nstep' N2 M V2} -> 
    N1 = N2 /\ V1 = V2.
induction on 3. intros. case H3.
  case H4.
    search.
    apply val'_step'_absurd to H1 H5.
  case H4.
    apply val'_step'_absurd to H2 H5.
    apply step'_det to H5 H7. apply IH to _ _ H6 H8. search.
Theorem eval'_det : forall E V V',
  {eval' E V} -> {eval' E V'} -> V = V'.
intros. case H1. case H2. 
  apply nstep'_val'_det to _ _ H3 H5. search.
Theorem nstep'_trans : forall K J M M' M'',
  {nstep' K M M'} -> {nstep' J M' M''} -> 
    exists N, {add K J N} /\ {nstep' N M M''}.
induction on 1. intros. case H1.
  search.
  apply IH to H4 H2. search.
Theorem nstep'_eval_closed : forall K M M' M'',
  {nstep' K M M'} -> {eval' M' M''} -> {eval' M M''}.
intros. case H2.
  apply nstep'_trans to H1 H3. search.
Theorem nstep_trans : forall K J M M' M'',
  {nstep K M M'} -> {nstep J M' M''} -> 
    exists N, {add K J N} /\ {nstep N M M''}.
induction on 1. intros. case H1.
  search.
  apply IH to H4 H2. search.
% Cannot step values
Theorem val_step_absurd : forall V M,
  {val V} -> {step V M} -> false.
induction on 1. intros. case H1.
  case H2.
  case H2.
  case H2. backchain IH. backchain IH with V = V2. 
  case H2.
Theorem eval'_refl : forall V,
  {val' V} -> {eval' V V}.
induction on 1. intros. case H1.
  search.
  search.
  apply IH to H2. apply IH to H3. search.
  search.
  apply IH to H2. apply IH to H3. search.
% Values can only take 0 steps in any evaluation
Theorem nstep_val_inv : forall J V V',
  {val V} -> {nstep J V V'} -> J = z /\ V = V'.
induction on 2. intros. case H2. 
  search. apply val_step_absurd to H1 H3.
Theorem nstep'_val'_inv : forall J V V',
  {val' V} -> {nstep' J V V'} -> J = z /\ V = V'.
induction on 2. intros. case H2. 
  search. apply val'_step'_absurd to H1 H3.
% Eval lemmas of pred
Theorem step_pred_result : forall M M',
  {step (pred M) M'} -> 
    (exists M'', M' = pred M'') \/ (exists N, M' = nat N).
intros. case H1. search. search.
Theorem nstep_pred_inv : forall V K M,
  {val V} -> {nstep K (pred M) V} -> 
    exists J N N', K = s J /\ {nstep J M (nat N)} /\ V = nat N' /\ {npred N N'}.
induction on 2. intros. case H2.
  case H1.
  apply step_pred_result to H3. case H5.
    apply IH to _ H4. case H3. search.
    apply nstep_val_inv to _ H4. case H3. search.
Theorem step'_pred_result : forall M M',
  {step' (pred' M) M'} -> 
    (exists M'', M' = pred' M'') \/ (exists N, M' = nat' N).
intros. case H1. search. search.
Theorem nstep'_pred_inv : forall V K M,
  {val' V} -> {nstep' K (pred' M) V} -> 
    exists J N N', K = s J /\ {nstep' J M (nat' N)} /\ V = nat' N' /\ {npred N N'}.
induction on 2. intros. case H2.
  case H1.
  apply step'_pred_result to H3. case H5.
    apply IH to _ H4. case H3. search.
    apply nstep'_val'_inv to _ H4. case H3. search.
Theorem nstep'_pred_fwd : forall K M N N',
  {nstep' K M (nat' N)} -> {npred N N'} -> {nstep' (s K) (pred' M) (nat' N')}.
induction on 1. intros. case H1.
  search.
  apply IH to H4 H2. search.
Theorem eval'_pred_fwd : forall M N N',
  {eval' M (nat' N)} -> {npred N N'} -> {eval' (pred' M) (nat' N')}.
intros. case H1. apply nstep'_pred_fwd to H3 H2. search.
Theorem eval''_pred_fwd: forall FE M M' N N',
  {eval'' (htm FE M) (nat' N)} -> {npred N N'} ->
  {hconstr M (x\pred' x) M'} -> {eval'' (htm FE M') (nat' N')}.
induction on 3. intros. case H3.
  case H1. apply eval'_pred_fwd to H4 H2. search.
  case H1. inst H4 with n1 = F.
    apply IH to H5 H2 H6. search.
% Eval lemmas of ifz
Theorem nstep_ifz_inv : forall V K M M1 M2,
  {is_nat K} -> {val V} -> {nstep K (ifz M M1 M2) V} -> 
    exists I J N, le J K /\ le I K /\
                  (({nstep J M (nat z)} /\ {nstep I M1 V}) \/
                   ({nstep J M (nat (s N))} /\ {nstep I M2 V})).
induction on 3. intros. case H3.
  case H2.
  case H4.
    apply IH to _ _ H5. case H1. search. case H9.
      exists I. exists (s J). exists z. left. split.
        backchain le_extend.
        backchain le_succ.                
        search.
      exists I. exists (s J). exists N1. right. split.
        backchain le_extend.
        backchain le_succ.
        search.
    exists N. exists z. exists z. left. split.
      search.
      backchain le_succ. backchain le_refl. case H1. search.
      search.
    exists N. exists z. exists N1. right. split.
      search.
      backchain le_succ. backchain le_refl. case H1. search.
      search.
Theorem nstep'_ifz_inv : forall V K M M1 M2,
  {is_nat K} -> {val' V} -> {nstep' K (ifz' M M1 M2) V} -> 
    exists I J N, le J K /\ le I K /\
                  (({nstep' J M (nat' z)} /\ {nstep' I M1 V}) \/
                   ({nstep' J M (nat' (s N))} /\ {nstep' I M2 V})).
induction on 3. intros. case H3.
  case H2.
  case H4.
    apply IH to _ _ H5. case H1. search. case H9.
      exists I. exists (s J). exists z. left. split.
        backchain le_extend.
        backchain le_succ.                
        search.
      exists I. exists (s J). exists N1. right. split.
        backchain le_extend.
        backchain le_succ.
        search.
    exists N. exists z. exists z. left. split.
      search.
      backchain le_succ. backchain le_refl. case H1. search.
      search.
    exists N. exists z. exists N1. right. split.
      search.
      backchain le_succ. backchain le_refl. case H1. search.
      search.
      
Theorem nstep'_ifz_fwd1 : forall N1 M N2 M1 M2 V, 
  {nstep' N1 M (nat' z)} -> {nstep' N2 M1 V} -> exists N,
    {add N1 N2 N} /\ {nstep' (s N) (ifz' M M1 M2) V}.
induction on 1. intros. case H1.
  search.
  apply IH to H4 H2 with M2 = M2. search.
Theorem eval'_ifz_fwd1 : forall M M1 M2 V,
  {eval' M (nat' z)} -> {eval' M1 V} -> {eval' (ifz' M M1 M2) V}.
intros. case H1. case H2.
 apply nstep'_ifz_fwd1 to H3 H5 with M2 = M2. search.
Theorem nstep'_ifz_fwd2 : forall N1 M N2 M1 M2 V N', 
  {nstep' N1 M (nat' (s N'))} -> {nstep' N2 M2 V} -> exists N,
    {add N1 N2 N} /\ {nstep' (s N) (ifz' M M1 M2) V}.
induction on 1. intros. case H1.
  search.
  apply IH to H4 H2 with M1 = M1. search.
Theorem eval'_ifz_fwd2 : forall M M1 M2 V N,
  {eval' M (nat' (s N))} -> {eval' M2 V} -> {eval' (ifz' M M1 M2) V}.
intros. case H1. case H2.
  apply nstep'_ifz_fwd2 to H3 H5 with M1 = M1. search.
Theorem eval''_ifz_fwd1 : forall FE1 FE2 FE3 FE FE12 M1 M2 M3 P V,
  {tm'' (htm FE3 M3)} -> {eval'' (htm FE1 M1) (nat' z)} -> {eval'' (htm FE2 M2) V} -> 
  {appd FE1 FE2 FE12} -> {appd FE12 FE3 FE} ->
  {hcombine3 M1 M2 M3 (x\y\z\ifz' x y z) P} ->
    {eval'' (htm FE P) V}.
induction on 6. intros. case H6.
  case H1. case H2. case H3. case H4. case H5.
    apply eval'_ifz_fwd1 to H8 H9 with M2 = M4. search.
  case H2. case H4. case H5. inst H7 with n1 = F.
    apply IH to _ H8 H3 H9 H10 H11. search.
  case H2. case H4. case H3. case H5. inst H7 with n1 = F.
    apply IH to _ _ H9 _ H10 H11. search.
  case H2. case H3. case H4. case H5. case H1.
    inst H11 with n1 = M. cut H12 with H10. inst H7 with n1 = M.
    apply IH to H13 _ _ _ _ H14. search.
Theorem eval''_ifz_fwd2 : forall N FE1 FE2 FE3 FE FE12 M1 M2 M3 P V,
  {tm'' (htm FE2 M2)} -> {eval'' (htm FE1 M1) (nat' (s N))} -> {eval'' (htm FE3 M3) V} -> 
  {appd FE1 FE2 FE12} -> {appd FE12 FE3 FE} ->
  {hcombine3 M1 M2 M3 (x\y\z\ifz' x y z) P} ->
    {eval'' (htm FE P) V}.
induction on 6. intros. case H6.
  case H1. case H2. case H3. case H4. case H5.
    apply eval'_ifz_fwd2 to H8 H9 with M1 = M5. search.
  case H2. case H4. case H5. inst H7 with n1 = F.
    apply IH to _ H8 H3 H9 H10 H11. search.
  case H2. case H4. case H1. case H5.
    inst H10 with n1 = M. cut H12 with H9. inst H7 with n1 = M.
    apply IH to H13 _ H3 _ _ H14. search.
  case H2. case H3. case H4. case H1. case H5.
    inst H7 with n1 = F. apply IH to _ _ H9 _ _ H11. search.
% Eval lemmas of let
Theorem nstep_let_inv : forall K M1 R V,
  {val V} -> {nstep K (let M1 R) V} -> exists K1 K2 K3 V1, K = s K3 /\
    {add K1 K2 K3} /\ {nstep K1 M1 V1} /\ {val V1} /\ {nstep K2 (R V1) V}.
induction on 2. intros. case H2. case H1. case H3.
  apply IH to _ H4. search.
  search.
Theorem nstep'_let_inv : forall K M1 R V,
  {val' V} -> {nstep' K (let' M1 R) V} -> exists K1 K2 K3 V1, K = s K3 /\
    {add K1 K2 K3} /\ {nstep' K1 M1 V1} /\ {val' V1} /\ {nstep' K2 (R V1) V}.
induction on 2. intros. case H2. case H1. case H3.
  apply IH to _ H4. search.
  search.
Theorem nstep'_let_fwd : forall N1 N2 R V M V',
  {val' V} -> {nstep' N1 M V} -> {nstep' N2 (R V) V'} -> exists N,
    {add N1 N2 N} /\ {nstep' (s N) (let' M R) V'}.
induction on 2. intros. case H2.
  search.
  apply IH to _ H5 H3 with R = R, V = V. search.
Theorem eval'_let_fwd : forall M R V V',
  {eval' M V} -> {eval' (R V) V'} -> {eval' (let' M R) V'}.
intros. case H1. case H2.
  apply nstep'_let_fwd to _ H3 H5 with R = R. search.
Theorem eval''_let_fwd : forall FE1 FE2 FE M1 M2 V1 V P,
  {eval'' (htm FE1 M1) V1} -> {eval'' (htm FE2 (M2 V1)) V} ->
  {hcombine_abs M1 M2 (x\y\let' x y) P} ->
  {appd FE1 FE2 FE} -> {eval'' (htm FE P) V}.
induction on 3. intros. case H3.
  case H1. case H2. case H4. 
    apply eval'_let_fwd to H5 H6 with R = M3. search.
  case H1. case H4. inst H5 with n1 = F.
    apply IH to H6 H2 H8 H7 with M2 = M2. search.
  case H1(keep). case H2. case H4. inst H5 with n1 = F.
    apply IH to H1 H7 H8 _ with M2 = (x\R x F). search.
% Eval lemmas of plus
Theorem nstep_plus_inv : forall V K M1 M2,
  {val V} -> {nstep K (plus M1 M2) V} -> exists J1 J2 J12 N1 N2 N3,
    {add J1 J2 J12} /\ K = s J12 /\ V = (nat N3) /\
    {nstep J1 M1 (nat N1)} /\ {nstep J2 M2 (nat N2)} /\ {add N1 N2 N3}.
induction on 2. intros. case H2.
  case H1.
  case H3.
    apply IH to _ H4. search.
    apply IH to _ H4. apply add_s to H7. search.
    case H4. search. case H6.
 
Theorem nstep'_plus_inv : forall V K M1 M2,
  {val' V} -> {nstep' K (plus' M1 M2) V} -> exists J1 J2 J12 N1 N2 N3,
    {add J1 J2 J12} /\ K = s J12 /\ V = (nat' N3) /\
    {nstep' J1 M1 (nat' N1)} /\ {nstep' J2 M2 (nat' N2)} /\ {add N1 N2 N3}.
induction on 2. intros. case H2.
  case H1.
  case H3.
    apply IH to _ H4. search.
    apply IH to _ H4. apply add_s to H7. search.
    case H4. search. case H6.
 
Theorem nstep'_plus_fwd1 : forall J2 N1 N2 N3 M2,
  {nstep' J2 M2 (nat' N2)} -> {add N1 N2 N3} ->
    {nstep' (s J2) (plus' (nat' N1) M2) (nat' N3)}.
induction on 1. intros. case H1.
  search.  
  apply IH to H4 _. search.
Theorem nstep'_plus_fwd : forall J1 J2 N1 N2 N3 M1 M2,
  {nstep' J1 M1 (nat' N1)} -> {nstep' J2 M2 (nat' N2)} -> {add N1 N2 N3} ->
    exists J3, {add J1 J2 J3} /\ {nstep' (s J3) (plus' M1 M2) (nat' N3)}.
induction on 1. intros. case H1. 
  apply nstep'_plus_fwd1 to H2 H3. search. 
  apply IH to H5 H2 H3. search.
Theorem eval'_plus_fwd : forall M1 M2 N1 N2 N3,
  {eval' M1 (nat' N1)} -> {eval' M2 (nat' N2)} -> {add N1 N2 N3} ->
    {eval' (plus' M1 M2) (nat' N3)}.
intros. case H1. case H2. 
  apply nstep'_plus_fwd to H4 H6 H3. search.
Theorem eval''_plus_fwd_aux : forall M1 M2 FE N1 N2 N3 P,
  {eval' M1 (nat' N1)} -> {eval'' (htm FE M2) (nat' N2)} ->
  {add N1 N2 N3} -> {hcombine (hbase M1) M2 (x\y\plus' x y) P} ->
    {eval'' (htm FE P) (nat' N3)}.
induction on 2. intros. case H2.
  case H4. apply eval'_plus_fwd to H1 H5 H3. search.
  case H4. inst H6 with n1 = F. apply IH to H1 H5 H3 H7. search.
Theorem eval''_plus_fwd : forall FE1 FE2 FE M1 M2 N1 N2 N3 P,
  {eval'' (htm FE1 M1) (nat' N1)} -> 
  {eval'' (htm FE2 M2) (nat' N2)} -> {add N1 N2 N3} -> 
  {appd FE1 FE2 FE} -> {hcombine M1 M2 (x\y\plus' x y) P} ->
    {eval'' (htm FE P) (nat' N3)}.
induction on 1. intros. case H1.
  case H4. backchain eval''_plus_fwd_aux.
  case H4. case H5. inst H8 with n1 = F.
    apply IH to H6 H2 H3 H7 H9. search.
% Eval lemmas of pairs
Theorem step_pair_inv : forall M1 M2 M',
  {step (pair M1 M2) M'} -> 
     (exists M1', M' = pair M1' M2 /\ {step M1 M1'}) \/ 
     (exists M2', {val M1} /\ M' = pair M1 M2' /\ {step M2 M2'}).
induction on 1. intros. case H1.
  search.
  search.
Theorem nstep_pair_inv : forall V K M1 M2,
  {val V} -> {nstep K (pair M1 M2) V} ->
     exists I J V1 V2, {add I J K} /\ 
       V = pair V1 V2 /\{nstep I M1 V1} /\ {nstep J M2 V2}.
induction on 2. intros. case H2.
  search.
  apply step_pair_inv to H3. case H5.
    apply IH to _ H4. search.
    apply IH to _ H4. exists I. exists (s J). exists V1. exists V2. split.
      backchain add_s. search. search. search.
Theorem step'_pair_inv : forall M1 M2 M',
  {step' (pair' M1 M2) M'} -> 
     (exists M1', M' = pair' M1' M2 /\ {step' M1 M1'}) \/ 
     (exists M2', {val' M1} /\ M' = pair' M1 M2' /\ {step' M2 M2'}).
induction on 1. intros. case H1.
  search.
  search.
Theorem nstep'_pair_inv : forall V K M1 M2,
  {val' V} -> {nstep' K (pair' M1 M2) V} ->
     exists I J V1 V2, {add I J K} /\ 
       V = pair' V1 V2 /\{nstep' I M1 V1} /\ {nstep' J M2 V2}.
induction on 2. intros. case H2.
  search.
  apply step'_pair_inv to H3. case H5.
    apply IH to _ H4. search.
    apply IH to _ H4. exists I. exists (s J). exists V1. exists V2. split.
      backchain add_s. search. search. search.
Theorem nstep'_pair_fwd1 : forall K V1 M2 M2',
  {val' V1} ->  {nstep' K M2 M2'} -> {nstep' K (pair' V1 M2) (pair' V1 M2')}.
induction on 2. intros. case H2. 
  search. 
  apply IH to _ H4. search.
Theorem nstep'_pair_fwd : forall V1 M1 M2 M2' I J,
  {val' V1} -> {nstep' I M1 V1} -> {nstep' J M2 M2'} -> 
    exists K, {add I J K} /\ {nstep' K (pair' M1 M2) (pair' V1 M2')}.
induction on 2. intros. case H2.
  apply nstep'_pair_fwd1 to _ H3. search.
  apply IH to _ H5 H3. search.
Theorem eval'_pair_fwd : forall M1 M2 V1 V2,
  {eval' M1 V1} -> {eval' M2 V2} -> {eval' (pair' M1 M2) (pair' V1 V2)}.
intros. case H1. case H2. apply nstep'_pair_fwd to _ H3 H5. search.
Theorem eval''_pair_fwd_aux : forall M1 M2 FE V1 V2 P,
  {eval' M1 V1} -> {eval'' (htm FE M2) V2} ->
  {hcombine (hbase M1) M2 (x\y\pair' x y) P} ->
    {eval'' (htm FE P) (pair' V1 V2)}.
induction on 3. intros. case H3.
  case H2. apply eval'_pair_fwd to H1 H4. search.
  case H2. inst H4 with n1 = F. apply IH to H1 H5 H6. search.
Theorem eval''_pair_fwd : forall FE1 FE2 FE M1 M2 V1 V2 P,
  {eval'' (htm FE1 M1) V1} -> {eval'' (htm FE2 M2) V2} -> 
  {appd FE1 FE2 FE} -> {hcombine M1 M2 (x\y\pair' x y) P} ->
    {eval'' (htm FE P) (pair' V1 V2)}.
induction on 1. intros. case H1.
  case H3. backchain eval''_pair_fwd_aux.
  case H3. case H4. inst H7 with n1 = F.
    apply IH to H5 _ _ H8. search.
Theorem nstep'_fst_pair : forall V1 V2 M N,
  {val' (pair' V1 V2)} -> {nstep' N M (pair' V1 V2)} -> 
    {nstep' (s N) (fst' M) V1}.
induction on 2. intros. case H2.
  search.
  apply IH to H1 H4. search.
    
Theorem eval'_fst_pair : forall M M1 M2,
  {eval' M (pair' M1 M2)} -> {eval' (fst' M) M1}.
intros. case H1.
  apply nstep'_fst_pair to H3 H2. case H3. search.
Theorem nstep'_snd_pair : forall V1 V2 M N,
  {val' (pair' V1 V2)} -> {nstep' N M (pair' V1 V2)} -> 
    {nstep' (s N) (snd' M) V2}.
induction on 2. intros. case H2.
  search.
  apply IH to H1 H4. search.
Theorem eval'_snd_pair : forall M M1 M2,
  {eval' M (pair' M1 M2)} -> {eval' (snd' M) M2}.
intros. case H1.
  apply nstep'_snd_pair to H3 H2. case H3. search.
% Lemmas of fst and snd
Theorem nstep_fst_inv : forall V K M,
  {val V} -> {nstep K (fst M) V} -> 
    exists K' V', K = s K' /\ {val V'} /\ {nstep K' M (pair V V')}.
induction on 2. intros. case H2.
  case H1.
  case H3. 
    apply IH to _ H4. search.
    case H5. apply nstep_val_inv to H6 H4. search.
Theorem nstep_snd_inv : forall V K M,
  {val V} -> {nstep K (snd M) V} -> 
    exists K' V', K = s K' /\ {val V'} /\ {nstep K' M (pair V' V)}.
induction on 2. intros. case H2.
  case H1.
  case H3. 
    apply IH to _ H4. search.
    case H5. apply nstep_val_inv to H7 H4. search.
Theorem nstep'_fst_inv : forall V K M,
  {val' V} -> {nstep' K (fst' M) V} -> 
    exists K' V', K = s K' /\ {val' V'} /\ {nstep' K' M (pair' V V')}.
induction on 2. intros. case H2.
  case H1.
  case H3. 
    apply IH to _ H4. search.
    case H5. apply nstep'_val'_inv to H6 H4. search.
Theorem eval'_fst_inv : forall M V,
  {eval' (fst' M) V} -> exists V', {eval' M (pair' V V')}.
intros. case H1.
  apply nstep'_fst_inv to H3 H2. search.
Theorem nstep'_fst_fwd : forall K V1 V2 M,
  {val' (pair' V1 V2)} -> {nstep' K M (pair' V1 V2)} -> 
    {nstep' (s K) (fst' M) V1}.
induction on 2. intros. case H2.
  search.
  apply IH to H1 H4. search.
Theorem eval'_fst_fwd : forall M V V',
  {eval' M (pair' V V')} -> {eval' (fst' M) V}.
intros. case H1. apply nstep'_fst_fwd to H3 H2. case H3. search.
Theorem eval''_fst_fwd: forall FE M M' V1 V2,
  {eval'' (htm FE M) (pair' V1 V2)} -> 
  {hconstr M (x\fst' x) M'} -> {eval'' (htm FE M') V1}.
induction on 2. intros. case H2.
  case H1. apply eval'_fst_fwd to H3. search.
  case H1. inst H3 with n1 = F.
    apply IH to H4 H5. search.
Theorem nstep'_snd_inv : forall V K M,
  {val' V} -> {nstep' K (snd' M) V} -> 
    exists K' V', K = s K' /\ {val' V'} /\ {nstep' K' M (pair' V' V)}.
induction on 2. intros. case H2.
  case H1.
  case H3. 
    apply IH to _ H4. search.
    case H5. apply nstep'_val'_inv to H7 H4. search.
Theorem eval'_snd_inv : forall M V,
  {eval' (snd' M) V} -> exists V', {eval' M (pair' V' V)}.
intros. case H1.
  apply nstep'_snd_inv to H3 H2. search.
Theorem nstep'_snd_fwd : forall K V1 V2 M,
  {val' (pair' V1 V2)} -> {nstep' K M (pair' V1 V2)} -> 
    {nstep' (s K) (snd' M) V2}.
induction on 2. intros. case H2.
  search.
  apply IH to H1 H4. search.
Theorem eval'_snd_fwd : forall M V V',
  {eval' M (pair' V V')} -> {eval' (snd' M) V'}.
intros. case H1. apply nstep'_snd_fwd to H3 H2. case H3. search.
Theorem eval''_snd_fwd: forall FE M M' V1 V2,
  {eval'' (htm FE M) (pair' V1 V2)} -> 
  {hconstr M (x\snd' x) M'} -> {eval'' (htm FE M') V2}.
induction on 2. intros. case H2.
  case H1. apply eval'_snd_fwd to H3. search.
  case H1. inst H3 with n1 = F.
    apply IH to H4 H5. search.
% Eval lemmas of application
Theorem nstep_app_inv : forall V K M1 M2,
  {val V} -> {nstep K (app M1 M2) V} -> exists J1 J2 J3 J23 J123 V2 R,
    {add J2 J3 J23} /\ {add J1 J23 J123} /\ K = s J123 /\
    {nstep J1 M1 (fix R)} /\ {nstep J2 M2 V2} /\ {val V2} /\
    {nstep J3 (R (fix R) V2) V}.
induction on 2. intros. case H2.
  case H1.
  case H3.
    apply IH to H1 H4. search.
    apply IH to H1 H4. apply add_s to H8. search. 
  search.
Theorem nstep'_app_fwd1 : forall N1 N2 M R V V',
  {val' V} ->  {nstep' N1 M V} -> {nstep' N2 (R V) V'} ->
    exists N3, {add N1 N2 N3} /\ {nstep' (s N3) (app' (abs' R) M) V'}.
induction on 2. intros. case H2. 
  search. 
  apply IH to _ H5 H3 with R = R. search.
Theorem nstep'_app_fwd2 : forall N1 N2 M1 M2 R V,
  {nstep' N1 M1 (abs' R)} -> {nstep' N2 (app' (abs' R) M2) V} ->
    exists N3, {add N1 N2 N3} /\ {nstep' N3 (app' M1 M2) V}.
induction on 1. intros. case H1.
  search.
  apply IH to H4 H2. search.
Theorem nstep'_app_inv : forall V K M1 M2,
  {val' V} -> {nstep' K (app' M1 M2) V} -> exists J1 J2 J3 J23 J123 V2 R,
    {add J2 J3 J23} /\ {add J1 J23 J123} /\ K = s J123 /\
    {nstep' J1 M1 (abs' R)} /\ {nstep' J2 M2 V2} /\ {val' V2} /\
    {nstep' J3 (R V2) V}.
induction on 2. intros. case H2.
  case H1.
  case H3.
    apply IH to H1 H4. search.
    apply IH to H1 H4. apply add_s to H8. search. 
  search.
Theorem eval'_app_fwd : forall M1 M2 R V1 V,
  {eval' M1 (abs' R)} -> {eval' M2 V1} -> {eval' (R V1) V} ->
    {eval' (app' M1 M2) V}.
intros. case H1. case H2. case H3.
  apply nstep'_app_fwd1 to _ H6 H8 with R = R.
  apply nstep'_app_fwd2 to H4 H11. search.

Theorem eval''_app_fwd : forall FE1 FE2 FE M1 M2 R V1 V P,
  {eval'' (htm FE1 M1) (abs' R)} -> {eval'' (htm FE2 M2) V1} ->
  {eval' (R V1) V} -> {hcombine M1 M2 (x\y\app' x y) P} ->
  {appd FE1 FE2 FE} -> {eval'' (htm FE P) V}.
induction on 4. intros. case H4.
  case H1. case H2. case H5.
    apply eval'_app_fwd to H6 H7 H3. search.
  case H1. case H5. inst H6 with n1 = F.
    apply IH to H7 H2 H3 H9 H8.  search.
  case H1(keep). case H2. case H5.
    inst H6 with n1 = F. apply IH to H1 H8 H3 H9 _. search.
% Eval lemmas of closures
Theorem nstep'_clos_fwd1 : forall M M' K V,
  {val' V} -> {nstep' K M M'} -> {nstep' K (clos' V M) (clos' V M')}.
induction on 2. intros. case H2.
  search.
  apply IH to _ H4 with V = V. search.
Theorem nstep'_clos_fwd : forall I J V1 M1 M2 M2',
  {val' V1} -> {nstep' I M1 V1} -> {nstep' J M2 M2'} -> 
    exists K, {add I J K} /\ {nstep' K (clos' M1 M2) (clos' V1 M2')}.
induction on 2. intros. case H2.
  apply nstep'_clos_fwd1 to H1 H3. search.
  apply IH to _ H5 H3. search.
Theorem eval'_clos_fwd : forall M1 M2 V1 V2,
  {eval' M1 V1} -> {eval' M2 V2} -> {eval' (clos' M1 M2) (clos' V1 V2)}.
intros. case H1. case H2. apply nstep'_clos_fwd to _ H3 H5. search.
Theorem step'_clos_inv : forall M1 M2 M',
  {step' (clos' M1 M2) M'} -> 
     (exists M1', M' = clos' M1' M2 /\ {step' M1 M1'}) \/ 
     (exists M2', {val' M1} /\ M' = clos' M1 M2' /\ {step' M2 M2'}).
induction on 1. intros. case H1.
  search.
  search.
Theorem nstep'_clos_inv : forall V K M1 M2,
  {val' V} -> {nstep' K (clos' M1 M2) V} ->
     exists K1 K2 V1 V2, {add K1 K2 K} /\ 
       V = clos' V1 V2 /\{nstep' K1 M1 V1} /\ {nstep' K2 M2 V2}.
induction on 2. intros. case H2.
  search.
  apply step'_clos_inv to H3. case H5.
    apply IH to _ H4. search.
    apply IH to _ H4. exists K1. exists (s K2). exists V1. exists V2. split.
      backchain add_s. search. search. search.
Theorem eval''_clos_fwd_aux : forall M1 M2 FE V1 V2 P,
  {eval' M1 V1} -> {eval'' (htm FE M2) V2} ->
  {hcombine (hbase M1) M2 (x\y\clos' x y) P} ->
    {eval'' (htm FE P) (clos' V1 V2)}.
induction on 2. intros. case H2.
  case H3. apply eval'_clos_fwd to H1 H4. search.
  case H3. inst H5 with n1 = F. apply IH to H1 H4 H6. search.
Theorem eval''_clos_fwd : forall FE1 FE2 FE M1 M2 V1 V2 P,
  {eval'' (htm FE1 M1) V1} -> {eval'' (htm FE2 M2) V2} ->
  {appd FE1 FE2 FE} -> {hcombine M1 M2 (x\y\clos' x y) P} ->
    {eval'' (htm FE P) (clos' V1 V2)}.
induction on 1. intros. case H1.
  case H3. backchain eval''_clos_fwd_aux.
  case H3. case H4. inst H7 with n1 = F.
    apply IH to H5 H2 H6 H8. search.

Theorem nstep'_open_fwd : forall N1 N2 F E M R V,
  {val' (clos' F E)} -> {nstep' N1 M (clos' F E)} ->
    {nstep' N2 (R F E) V} -> exists N3, 
      {add N1 N2 N3} /\ {nstep' (s N3) (open' M R) V}.
induction on 2. intros. case H2.
  search.
  apply IH to _ H5 H3 with R = R. search.
Theorem eval'_open_fwd : forall M1 M2 R VE V2 V,
  {eval' M1 (clos' (abs' R) VE)} -> {eval' M2 V2} -> 
    {eval' (R (pair' (clos' (abs' R) VE) (pair' V2 VE))) V} -> 
      {eval' (open' M1 (f\e\app' f (pair' M1 (pair' M2 e)))) V}.
intros. case H1. case H2. case H5(keep).
  assert exists N3, {nstep' N3 (pair' M1 (pair' M2 VE)) 
                               (pair' (clos' (abs' R) VE) (pair' V2 VE))}.
    apply nstep'_pair_fwd to H7 H6 _ with M2 = VE, M2' = VE.
    apply nstep'_pair_fwd to H5 H4 H11.
    search.
  case H10.
  case H3.
  apply nstep'_app_fwd1 to _ H11 H12 with R = R.
  apply nstep'_open_fwd to _ H4 H15 with R = (f\e\app' f (pair' M1 (pair' M2 e))).
  search.
Theorem nstep'_open_inv : forall K M1 R V,
  {val' V} -> {nstep' K (open' M1 R) V} -> exists K1 K2 K3 F E, K = s K3 /\
    {add K1 K2 K3} /\ {nstep' K1 M1 (clos' F E)} /\ {val' (clos' F E)} /\ 
    {nstep' K2 (R F E) V}.
induction on 2. intros. case H2. case H1. case H3.
  apply IH to _ H4. search.
  search.
Theorem nstep'_open_inv_sp : forall K V M1 M2,
  {val' V} -> {nstep' K (open' M1 (f\e\app' f (pair' M1 (pair' M2 e)))) V} -> 
    exists K1 K2 K3 K12 K123 K1231 F E V2, 
      K = s (s K1231) /\ {add K1 K2 K12} /\ {add K12 K3 K123} /\ {add K123 K1 K1231} /\
      {nstep' K1 M1 (clos' (abs' F) E)} /\ {val' E} /\ 
      {nstep' K2 M2 V2} /\ {val' V2} /\
      {nstep' K3 (F (pair' (clos' (abs' F) E) (pair' V2 E))) V}.
intros.
  apply nstep'_open_inv to H1 H2. apply nstep'_app_inv to _ H6. case H5.
  apply nstep'_val'_inv to H13 H9. case H8. 
  apply nstep'_is_nat to H2. case H15. apply add_comm to _ H3. case H17.
  apply nstep'_pair_inv to _ H10. case H11. apply nstep'_pair_inv to _ H21.
  apply nstep'_val'_inv to _ H26. case H23. apply nstep'_val'_det to _ _ H4 H20.
  apply nstep'_is_nat to H21. apply add_comm to _ H24. case H30.
  exists I. exists J. exists J3. exists J2. exists J123. exists N3. search.
Theorem eval''_open_fwd : forall FE1 FE2 FE F E M1 M2 V2 V P,
  {eval'' (htm FE1 M1) (clos' (abs' F) E)} -> {eval'' (htm FE2 M2) V2} ->
  {eval' (F (pair' (clos' (abs' F) E) (pair' V2 E))) V} ->
  {hcombine M1 M2 (x\y\open' x (f\e\app' f (pair' x (pair' y e)))) P} ->
  {appd FE1 FE2 FE} -> {eval'' (htm FE P) V}.
induction on 4. intros. case H4.
  case H1. case H2. case H5.
    apply eval'_open_fwd to H6 H7 H3. search.
  case H1. case H5. inst H6 with n1 = F1.
    apply IH to H7 H2 H3 H9 H8.  search.
  case H1(keep). case H2. case H5.
    inst H6 with n1 = F1. apply IH to H1 H8 H3 H9 _. search.
 

%% Determinism for eval''
Theorem eval''_det : forall E V V',
  {eval'' E V} -> {eval'' E V'} -> V = V'.
induction on 1. intros. case H1.
  case H2. apply eval'_det to H3 H4. search.
  case H2. apply IH to H3 H4. search.