Subject reduction for PCF

Executable Specification

[View pcf.mod]

eval zero zero.
eval tt tt.
eval ff ff.
eval (succ M) (succ V) :- eval M V.
eval (pred M) zero :- eval M zero.
eval (pred M) V :- eval M (succ V).
eval (is_zero M) tt :- eval M zero.
eval (is_zero M) ff :- eval M (succ V).
eval (if M N1 N2) V :- eval M tt, eval N1 V.
eval (if M N1 N2) V :- eval M ff, eval N2 V.
eval (abs T R) (abs T R).
eval (app M N) V :- eval M (abs T R), eval (R N) V.
eval (rec T R) V :- eval (R (rec T R)) V.

of zero num.
of tt bool.
of ff bool.
of (succ M) num :- of M num.
of (pred M) num :- of M num.
of (is_zero M) bool :- of M num.
of (if M N1 N2) T :- of M bool, of N1 T, of N2 T.
of (abs T R) (arr T U) :- pi n\ (of n T => of (R n) U).
of (app M N) T :- of M (arr U T), of N U.
of (rec T R) T :- pi n\ (of n T => of (R n) T).

Reasoning

[View pcf.thm] [Show All Proofs] [Hide All Proofs]

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

%% Subject reduction for PCF

% Most cases are trivial consequences of the inductive hypothesis

Theorem subject_reduction :
  forall P V T, {eval P V} -> {of P T} -> {of V T}. [Show Proof][Hide Proof]
induction on 1. intros. case H1.
  search.
  search.
  search.
  case H2. apply IH to H3 H4. search.
  case H2. search.
  case H2. apply IH to H3 H4. case H5. search.
  case H2. search.
  case H2. search.
  case H2. apply IH to H4 H6. search.
  case H2. apply IH to H4 H7. search.
  search.

  % P = app M N
  case H2. apply IH to H3 H5. case H7.
    inst H8 with n1 = N. cut H9 with H6.
      apply IH to H4 H10. search.

  % P = rec T1 R
  case H2 (keep).
    inst H4 with n1 = rec T R.
      cut H5 with H2.
        apply IH to H3 H6. search.