SHARE
TWEET

Untitled

a guest Jul 19th, 2019 100 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. (* Syntax. *)
  2.  
  3. Inductive t
  4.   := t_true
  5.    | t_false
  6.    | if_then_else : t -> t -> t -> t.
  7.  
  8. Inductive v := v_true | v_false.
  9.  
  10. (* Semantics. *)
  11.  
  12. Inductive step : t -> t -> Prop
  13.   := step_true : forall t2 t3, step (if_then_else t_true t2 t3) t2
  14.    | step_false : forall t2 t3, step (if_then_else t_false t2 t3) t3
  15.    | step_if : forall t1 t1' t2 t3, step t1 t1' -> step (if_then_else t1 t2 t3) (if_then_else t1' t2 t3).
  16.  
  17. Definition val t := match t with t_true | t_false => True | _ => False end.
  18.  
  19. Lemma val_stuck : forall t t', val t -> ~ step t t'.
  20.   intros t t' Ht; induction 1; contradiction Ht.
  21. Qed.
  22.  
  23. Lemma determinacy : forall t t' t'', step t t' -> step t t'' -> t' = t''.
  24.   intros t t' t'' Ht.
  25.   generalize dependent t''.
  26.   induction Ht.
  27.   (* We proceed by induction on a derivation of [step t t'] *)
  28.   - (* Suppose the last rule applied was [step_true].
  29.        We have [if true then t2 else t3 -> t''] and wish to show that [t2 = t'']. *)
  30.     (* The only way we could've gotten the assumption [if true then t2 else t3 -> t'']
  31.        is if t2 = t'': *)
  32.     inversion 1.
  33.     + (* Suppose the last rule applied in the proof of [if true then t2 else t3 -> t'']
  34.          was step_true. Then t2 = t'' as desired. *) reflexivity.
  35.       (* The last rule couldn't have been step_false, because our assumption is
  36.          [if true then t2 else t3 -> t''] and step_false would only be able to give us
  37.          [if false then t2 else t3 -> t'']. *)
  38.     + (* Now suppose the last rule applied was step_if. That is, the proof tree looks like
  39.  
  40.                                true -> t1'
  41.           --------------------------------------------------- step_if
  42.            if true then t2 else t3 -> if t1' then t2 else t3
  43.  
  44.          for some t1', where t'' = if t1' then t2 else t3.
  45.  
  46.          This is clearly impossible: true -> t1' is never derivable, because constants
  47.          don't step to anything (by lemma val_stuck). *)
  48.       apply val_stuck in H4; [contradiction|exact I].
  49.     (* This completes the first case of the induction. *)
  50.   - (* The second case (where we suppose the last rule applied was [step_false] is largely
  51.        analogous to the first one. *)
  52.     inversion 1; auto; apply val_stuck in H4; [contradiction|exact I].
  53.   - (* Finally, suppose the last rule applied was [step_if]. *)
  54.     intros t''.
  55.     (* We have [if t1 then t2 else t3 -> t''] and [t1 -> t1'] and our induction hypothesis
  56.        says that, for any t4, [t1 -> t4 implies t1' = t4].
  57.        We wish to show that [if t1' then t2 else t3 -> t'']. *)
  58.     (* Because we know that [t1 -> t1'], [t1] can't be a value (by val_stuck again).
  59.        Thus, the last rule applied in the proof of [if t1 then t2 else t3 -> t'']
  60.        must have been step_if: *)
  61.     inversion 1; subst.
  62.     + (* The last rule couldn't have been step_true. *)
  63.       apply val_stuck in Ht; [contradiction|exact I].
  64.     + (* The last rule couldn't have been step_false. *)
  65.       apply val_stuck in Ht; [contradiction|exact I].
  66.     + (* The last rule was step_if; i.e. the proof of our assumption
  67.          [if t1 then t2 else t3 -> t''] must've looked like
  68.      
  69.                            t1 -> t4
  70.          ----------------------------------------------
  71.          if t1 then t2 else t3 -> if t4 then t2 else t3
  72.  
  73.          for some t4, where t'' = if t4 then t2 else t3.
  74.  
  75.       We wish to show that [if t1' then t2 else t3 = if t4 then t2 else t3].
  76.       It's sufficient to show that t1' = t4.
  77.       This follows from our induction hypothesis:
  78.         Our induction hypothesis says that, for any t5, [t1 -> t5 implies t1' = t5].
  79.         Since we know t1 -> t4, we instantiate t5 := t4 to get t1' = t4 as desired. *)
  80.       rewrite (IHHt _ H4).
  81.       reflexivity.
  82. Qed.
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top