-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathErasedEquivalentSplit.v
138 lines (132 loc) · 4.69 KB
/
ErasedEquivalentSplit.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
Require Export SystemFR.SatisfiesLemmas.
Require Export SystemFR.ErasedEquivalentIte.
Require Export SystemFR.ErasedEquivalentMatch.
Opaque reducible_values.
Lemma equivalent_split_bool:
forall ρ Γ1 Γ2 b t t' x l,
~(x ∈ fv b) ->
~(x ∈ fv t) ->
~(x ∈ fv t') ->
~(x ∈ fv_context Γ1) ->
~(x ∈ fv_context Γ2) ->
subset (fv b) (support Γ2) ->
[ support ρ; Γ2 ⊨ b : T_bool ] ->
valid_interpretation ρ ->
(forall l,
satisfies (reducible_values ρ) (Γ1 ++ (x, T_equiv b ttrue) :: Γ2) l ->
[ substitute t l ≡ substitute t' l ]) ->
(forall l,
satisfies (reducible_values ρ) (Γ1 ++ (x, T_equiv b tfalse) :: Γ2) l ->
[ substitute t l ≡ substitute t' l ]) ->
satisfies (reducible_values ρ) (Γ1 ++ Γ2) l ->
[ substitute t l ≡ substitute t' l ].
Proof.
unfold open_reducible,reduces_to;
repeat step || simp_red || satisfies_cut || t_instantiate_sat3 || t_sat_add;
eauto 2 with b_equiv_subst;
try solve [ eapply satisfies_insert2; eauto; t_closer ].
Qed.
Lemma equivalent_split_nat:
forall ρ Γ1 Γ2 n t t' x y l,
~(x ∈ fv_context Γ1) ->
~(x ∈ fv_context Γ2) ->
~(x ∈ fv n) ->
~(x ∈ fv t) ->
~(x ∈ fv t') ->
~(y ∈ fv_context Γ1) ->
~(y ∈ fv_context Γ2) ->
~(y ∈ fv n) ->
~(y ∈ fv t) ->
~(y ∈ fv t') ->
~(x = y) ->
subset (fv n) (support Γ2) ->
[ support ρ; Γ2 ⊨ n : T_nat ] ->
valid_interpretation ρ ->
(forall l,
satisfies (reducible_values ρ) (Γ1 ++ (x, T_equiv n zero) :: Γ2) l ->
[ substitute t l ≡ substitute t' l ]) ->
(forall l,
satisfies (reducible_values ρ)
(Γ1 ++ (x, T_equiv n (succ (fvar y term_var))) :: (y, T_nat) :: Γ2)
l ->
[ substitute t l ≡ substitute t' l ]) ->
satisfies (reducible_values ρ) (Γ1 ++ Γ2) l ->
[ substitute t l ≡ substitute t' l ].
Proof.
unfold open_reducible,reduces_to;
repeat step || t_instantiate_sat3 || simp_red || satisfies_cut.
force_invert is_nat_value; repeat step || t_sat_add;
eauto 2 with b_equiv_subst;
try solve [ eapply satisfies_insert2; eauto; t_closer ];
try solve [ eapply satisfies_insert_nat_succ; eauto; t_closer ].
Qed.
Lemma reducible_equivalent_ite:
forall ρ Γ t1 t2 t3 t x l,
~(x ∈ fv_context Γ) ->
~(x ∈ fv t1) ->
~(x ∈ fv t2) ->
~(x ∈ fv t3) ->
~(x ∈ fv t) ->
is_erased_term t2 ->
is_erased_term t3 ->
wf t2 0 ->
wf t3 0 ->
subset (fv t2) (support Γ) ->
subset (fv t3) (support Γ) ->
valid_interpretation ρ ->
[ support ρ; Γ ⊨ t1 : T_bool ] ->
satisfies (reducible_values ρ) Γ l ->
(forall l,
satisfies (reducible_values ρ) ((x, T_equiv t1 ttrue) :: Γ) l ->
[ substitute t2 l ≡ substitute t l ]) ->
(forall l,
satisfies (reducible_values ρ) ((x, T_equiv t1 tfalse) :: Γ) l ->
[ substitute t3 l ≡ substitute t l ]) ->
[ ite (substitute t1 l) (substitute t2 l) (substitute t3 l) ≡ substitute t l ].
Proof.
unfold open_reducible;
repeat step || apply equivalent_ite || t_instantiate_sat3 || simp_red ||
t_deterministic_star || unfold reduces_to in * || t_sat_add;
eauto 2 with b_equiv_subst;
t_closer;
try solve [ eapply satisfies_insert3; eauto; t_closer ].
Qed.
Lemma reducible_equivalent_match:
forall ρ Γ tn t0 ts t n p l,
~(p ∈ fv_context Γ) ->
~(p ∈ fv tn) ->
~(p ∈ fv ts) ->
~(p ∈ fv t0) ->
~(p ∈ fv t) ->
~(n ∈ fv_context Γ) ->
~(n ∈ fv ts) ->
~(n ∈ fv tn) ->
~(n ∈ fv t) ->
~(n = p) ->
[ support ρ; Γ ⊨ tn : T_nat ] ->
valid_interpretation ρ ->
is_erased_term t0 ->
is_erased_term ts ->
wf t0 0 ->
wf ts 1 ->
subset (fv t0) (support Γ) ->
subset (fv ts) (support Γ) ->
(forall l,
satisfies (reducible_values ρ) ((p, T_equiv tn zero) :: Γ) l ->
[ substitute t0 l ≡ substitute t l ]) ->
(forall l,
satisfies (reducible_values ρ)
((p, T_equiv tn (succ (fvar n term_var))) :: (n, T_nat) :: Γ)
l ->
[ substitute (open 0 ts (fvar n term_var)) l ≡ substitute t l ]) ->
satisfies (reducible_values ρ) Γ l ->
[ tmatch (substitute tn l) (substitute t0 l) (substitute ts l) ≡ substitute t l ].
Proof.
unfold open_reducible,reduces_to; repeat step || t_instantiate_sat3 || simp_red.
eapply equivalent_match; eauto;
repeat step || t_sat_add || step_inversion is_nat_value;
eauto 2 with b_equiv_subst;
t_closer;
try solve [ eapply satisfies_insert3; eauto; t_closer ];
try solve [ eapply satisfies_cons_nat_succ; eauto; t_closer ].
Qed.