-
Notifications
You must be signed in to change notification settings - Fork 3
/
ErasedEquivalent.v
40 lines (34 loc) · 1.09 KB
/
ErasedEquivalent.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
Require Import Coq.Strings.String.
Require Export SystemFR.RedTactics.
Opaque reducible_values.
Opaque makeFresh.
Lemma equivalent_weaken:
forall ρ Γ x T u v l,
subset (fv u) (support Γ) ->
subset (fv v) (support Γ) ->
(forall l,
satisfies (reducible_values ρ) Γ l ->
[ substitute u l ≡ substitute v l ]) ->
satisfies (reducible_values ρ) ((x, T) :: Γ) l ->
[ substitute u l ≡ substitute v l ].
Proof.
intros.
repeat step || step_inversion satisfies || t_substitutions.
Qed.
Lemma equivalent_error:
forall Θ ρ Γ t T l,
[ Θ; Γ ⊨ t : T ] ->
valid_interpretation ρ ->
satisfies (reducible_values ρ) Γ l ->
support ρ = Θ ->
[ notype_err ≡ substitute t l ] ->
False.
Proof.
repeat step || t_instantiate_sat2 ||
equivalence_instantiate (app (notype_lambda ttrue) (lvar 0 term_var)).
unshelve epose proof (H7 _);
repeat step || t_invert_star || step_inversion cbv_value.
unfold reduces_to in *; steps.
eapply star_trans;
eauto using star_one, scbv_step_same with cbvlemmas values smallstep.
Qed.