-
Notifications
You must be signed in to change notification settings - Fork 3
/
AnnotatedQuant.v
76 lines (73 loc) · 2.07 KB
/
AnnotatedQuant.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
Require Export SystemFR.Judgments.
Require Export SystemFR.AnnotatedTactics.
Require Export SystemFR.ErasedQuant.
Lemma annotated_reducible_forall_inst:
forall Θ Γ t1 t2 U V,
is_annotated_type V ->
is_annotated_term t2 ->
wf t1 0 ->
wf t2 0 ->
wf V 1 ->
subset (fv t1) (support Γ) ->
subset (fv t2) (support Γ) ->
subset (fv V) (support Γ) ->
[[ Θ; Γ ⊨ t1 : T_forall U V ]] ->
[[ Θ; Γ ⊨ t2 : U ]] ->
[[ Θ; Γ ⊨ forall_inst t1 t2 : open 0 V t2 ]].
Proof.
intros.
rewrite erase_type_open; steps.
apply open_reducible_forall_inst with (erase_type U); steps; side_conditions.
Qed.
Lemma annotated_reducible_forall:
forall Θ Γ t A U V x,
~(x ∈ fv_context Γ) ->
~(x ∈ fv U) ->
~(x ∈ fv V) ->
~(x ∈ fv t) ->
~(x ∈ Θ) ->
wf U 0 ->
subset (fv U) (support Γ) ->
subset (fv t) (support Γ) ->
is_annotated_type V ->
[[ Θ; (x,U) :: Γ ⊨ t : open 0 V (fvar x term_var) ]] ->
[[ Θ; Γ ⊨ t : A ]] ->
[[ Θ; Γ ⊨ t : T_forall U V ]].
Proof.
intros; apply open_reducible_forall with x (erase_type A);
repeat step || erase_open;
side_conditions.
Qed.
Lemma annotated_reducible_exists_elim:
forall Θ Γ p U V x y t T,
~(x ∈ fv_context Γ) ->
~(y ∈ fv_context Γ) ->
~(x = y) ->
~(x ∈ fv t) ->
~(y ∈ fv t) ->
~(x ∈ fv T) ->
~(y ∈ fv T) ->
~(x ∈ Θ) ->
~(y ∈ Θ) ->
~(x ∈ fv U) ->
~(x ∈ fv V) ->
~(y ∈ fv U) ->
~(y ∈ fv V) ->
wf T 0 ->
wf U 0 ->
wf V 1 ->
wf t 1 ->
subset (fv U) (support Γ) ->
subset (fv V) (support Γ) ->
subset (fv T) (support Γ) ->
subset (fv t) (support Γ) ->
is_annotated_term t ->
is_annotated_type V ->
[[ Θ; Γ ⊨ p : T_exists U V ]] ->
[[ Θ; (y, open 0 V (fvar x term_var)) :: (x, U) :: Γ ⊨ open 0 t (fvar y term_var) : T ]] ->
[[ Θ; Γ ⊨ tlet p (T_exists U V) t : T ]].
Proof.
intros; apply open_reducible_exists_elim with (erase_type U) (erase_type V) x y;
repeat step || erase_open;
side_conditions.
Qed.