• API
• FAQ
• Tools
• Archive
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.

Top