Executable Specification

[View trans]

Reasoning

[View eval]

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}.

Theorem nstep'_is_nat : forall N M M',
  {nstep' N M M'} -> {is_nat N}.

Theorem val'_step'_absurd : forall V M,
  {val' V} -> {step' V M} -> false.
 
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. Theorem eval'_det : forall E V V', {eval' E V} -> {eval' E V'} -> V = V'. 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''}. Theorem nstep'_eval_closed : forall K M M' M'', {nstep' K M M'} -> {eval' M' M''} -> {eval' M M''}. 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''}. % Cannot step values Theorem val_step_absurd : forall V M, {val V} -> {step V M} -> false. Theorem eval'_refl : forall V, {val' V} -> {eval' V V}. % 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'. Theorem nstep'_val'_inv : forall J V V', {val' V} -> {nstep' J V V'} -> J = z /\ V = V'. % 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). 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'}. Theorem step'_pred_result : forall M M', {step' (pred' M) M'} -> (exists M'', M' = pred' M'') \/ (exists N, M' = nat' N). 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'}. Theorem nstep'_pred_fwd : forall K M N N', {nstep' K M (nat' N)} -> {npred N N'} -> {nstep' (s K) (pred' M) (nat' N')}. Theorem eval'_pred_fwd : forall M N N', {eval' M (nat' N)} -> {npred N N'} -> {eval' (pred' M) (nat' N')}. 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')}. % 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})). 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})). 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}. Theorem eval'_ifz_fwd1 : forall M M1 M2 V, {eval' M (nat' z)} -> {eval' M1 V} -> {eval' (ifz' M M1 M2) V}. 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}. Theorem eval'_ifz_fwd2 : forall M M1 M2 V N, {eval' M (nat' (s N))} -> {eval' M2 V} -> {eval' (ifz' M M1 M2) V}. 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}. 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}. % 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}. 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}. 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'}. Theorem eval'_let_fwd : forall M R V V', {eval' M V} -> {eval' (R V) V'} -> {eval' (let' M R) V'}. 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}. % 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}. 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}. 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)}. 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)}. 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)}. 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)}. 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)}. % 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'}). 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}. 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'}). 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}. Theorem nstep'_pair_fwd1 : forall K V1 M2 M2', {val' V1} -> {nstep' K M2 M2'} -> {nstep' K (pair' V1 M2) (pair' V1 M2')}. 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')}. Theorem eval'_pair_fwd : forall M1 M2 V1 V2, {eval' M1 V1} -> {eval' M2 V2} -> {eval' (pair' M1 M2) (pair' V1 V2)}. 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)}. 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)}. 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}. Theorem eval'_fst_pair : forall M M1 M2, {eval' M (pair' M1 M2)} -> {eval' (fst' M) M1}. 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}. Theorem eval'_snd_pair : forall M M1 M2, {eval' M (pair' M1 M2)} -> {eval' (snd' M) M2}. % 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')}. 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)}. 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')}. Theorem eval'_fst_inv : forall M V, {eval' (fst' M) V} -> exists V', {eval' M (pair' V V')}. 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}. Theorem eval'_fst_fwd : forall M V V', {eval' M (pair' V V')} -> {eval' (fst' M) V}. 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}. 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)}. Theorem eval'_snd_inv : forall M V, {eval' (snd' M) V} -> exists V', {eval' M (pair' V' V)}. 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}. Theorem eval'_snd_fwd : forall M V V', {eval' M (pair' V V')} -> {eval' (snd' M) V'}. 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}. % 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}. 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'}. 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}. 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}. 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}. 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}. % 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')}. 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')}. Theorem eval'_clos_fwd : forall M1 M2 V1 V2, {eval' M1 V1} -> {eval' M2 V2} -> {eval' (clos' M1 M2) (clos' V1 V2)}. 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'}). 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}. 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)}. 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)}. 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}. 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}. 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}. 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}. 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}. %% Determinism for eval'' Theorem eval''_det : forall E V V', {eval'' E V} -> {eval'' E V'} -> V = V'.