-
Notifications
You must be signed in to change notification settings - Fork 3
/
AnnotatedTermLemmas.v
124 lines (108 loc) · 3.37 KB
/
AnnotatedTermLemmas.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
Require Import Coq.Strings.String.
Require Export SystemFR.TypeErasure.
Require Export SystemFR.TypeErasureLemmas.
Require Export SystemFR.Syntax.
Require Export SystemFR.Trees.
Require Export SystemFR.TreeLists.
Require Export SystemFR.Tactics.
Require Export SystemFR.AssocList.
Lemma annotated_term_type:
forall t,
is_annotated_term t ->
is_annotated_type t ->
False.
Proof.
destruct t; steps.
Qed.
Lemma annotated_open:
forall t k rep,
(is_annotated_term (open k t rep) -> is_annotated_term rep -> is_annotated_term t) /\
(is_annotated_type (open k t rep) -> is_annotated_term rep -> is_annotated_type t).
Proof.
induction t;
try solve [ repeat step || eapply_any; eauto using annotated_term_type with exfalso ].
Qed.
Lemma annotated_open_1:
forall t k rep,
is_annotated_term (open k t rep) ->
is_annotated_term rep ->
is_annotated_term t.
Proof.
apply annotated_open.
Qed.
Lemma annotated_open_2:
forall T k rep,
is_annotated_type (open k T rep) ->
is_annotated_term rep ->
is_annotated_type T.
Proof.
apply annotated_open.
Qed.
#[export]
Hint Immediate annotated_open_1: annot.
#[export]
Hint Immediate annotated_open_2: annot.
Lemma annotated_topen:
forall t k rep,
(is_annotated_term (topen k t rep) -> is_annotated_type rep -> is_annotated_term t) /\
(is_annotated_type (topen k t rep) -> is_annotated_type rep -> is_annotated_type t).
Proof.
induction t;
try solve [ repeat step || eapply_any; eauto using annotated_term_type with exfalso ].
Qed.
Lemma annotated_topen_1:
forall t k rep,
is_annotated_term (topen k t rep) ->
is_annotated_type rep ->
is_annotated_term t.
Proof.
apply annotated_topen.
Qed.
Lemma annotated_topen_2:
forall T k rep,
is_annotated_type (topen k T rep) ->
is_annotated_type rep ->
is_annotated_type T.
Proof.
apply annotated_topen.
Qed.
#[export]
Hint Immediate annotated_topen_1: annot.
#[export]
Hint Immediate annotated_topen_2: annot.
Lemma annotated_open_build:
forall t k rep,
(is_annotated_type t -> is_annotated_term rep -> is_annotated_type (open k t rep)) /\
(is_annotated_term t -> is_annotated_term rep -> is_annotated_term (open k t rep)).
Proof.
induction t; repeat step || eapply_any.
Qed.
#[export]
Hint Extern 50 => apply annotated_open_build; steps: annot.
Lemma annotated_topen_build:
forall t k V,
(is_annotated_type t -> is_annotated_type V -> is_annotated_type (topen k t V)) /\
(is_annotated_term t -> is_annotated_type V -> is_annotated_term (topen k t V)).
Proof.
induction t; repeat step || eapply_any.
Qed.
#[export]
Hint Extern 50 => apply annotated_topen_build; steps: annot.
Ltac t_annotated_open :=
match goal with
| H: is_annotated_term (open ?k ?t ?rep) |- is_annotated_term ?t =>
poseNew (Mark 0 "once");
apply annotated_open with k rep
| H: is_annotated_term (open _ (open ?k ?t ?rep) _) |- is_annotated_term ?t =>
poseNew (Mark 0 "once");
apply annotated_open with k rep
| H: is_annotated_type (open ?k ?t ?rep) |- is_annotated_type ?t =>
poseNew (Mark 0 "once");
apply annotated_open with k rep
| H: is_annotated_term (topen ?k ?t ?rep) |- is_annotated_term ?t =>
poseNew (Mark 0 "once");
apply annotated_topen with k rep
| H: is_annotated_type (topen ?k ?t ?rep) |- is_annotated_type ?t =>
poseNew (Mark 0 "once");
apply annotated_topen with k rep
end.