-
Notifications
You must be signed in to change notification settings - Fork 3
/
AnnotatedEquivalentInContext.v
42 lines (35 loc) · 1.67 KB
/
AnnotatedEquivalentInContext.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
Require Import Coq.Lists.List.
Require Export SystemFR.AnnotatedTactics.
Require Export SystemFR.Judgments.
Require Export SystemFR.EquivalentStar.
Opaque reducible_values.
Lemma annotated_equivalent_refine_equivalent:
forall Θ Γ Γ' x T p,
is_annotated_term p ->
~ x ∈ pfv p term_var ->
(forall z, z ∈ pfv p term_var -> z ∈ support Γ -> False) ->
[[ Θ; Γ ++ (x, T_refine T p) :: Γ' ⊨ open 0 p (fvar x term_var) ≡ ttrue ]].
Proof.
unfold open_equivalent;
repeat step || satisfies_cut || rewrite erase_context_append in * || step_inversion satisfies || list_utils || simp_red.
rewrite substitute_append2; repeat step || fv_open || t_fv_erase || list_utils || erase_open || t_substitutions;
eauto with fv;
try solve [ equivalent_star ].
apply (satisfies_y_in_support _ _ _ _ _ _ x0) in H3; repeat step;
side_conditions.
Qed.
Lemma annotated_equivalence_in_context:
forall Θ Γ Γ' x e1 e2,
(forall z, z ∈ pfv e1 term_var -> z ∈ support Γ -> False) ->
(forall z, z ∈ pfv e2 term_var -> z ∈ support Γ -> False) ->
[[ Θ; Γ ++ (x, T_equiv e1 e2) :: Γ' ⊨ e1 ≡ e2 ]].
Proof.
unfold open_equivalent;
repeat step || satisfies_cut || rewrite erase_context_append in * || step_inversion satisfies || list_utils || simp_red.
rewrite substitute_append2; repeat step || fv_open || t_fv_erase || list_utils || t_substitutions.
- rewrite substitute_append2; repeat step || fv_open || t_fv_erase || list_utils || t_substitutions.
apply (satisfies_y_in_support _ _ _ _ _ _ x0) in H2; repeat step;
side_conditions.
- apply (satisfies_y_in_support _ _ _ _ _ _ x0) in H2; repeat step;
side_conditions.
Qed.