-
Notifications
You must be signed in to change notification settings - Fork 3
/
AnnotatedFix.v
46 lines (43 loc) · 1.33 KB
/
AnnotatedFix.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
Require Import Coq.Lists.List.
Require Export SystemFR.Judgments.
Require Export SystemFR.AnnotatedTactics.
Require Export SystemFR.ErasedFix.
Opaque reducible_values.
Lemma annotated_reducible_fix_strong_induction:
forall Θ Γ ts T n y p,
~(n ∈ fv_context Γ) ->
~(y ∈ fv_context Γ) ->
~(p ∈ fv_context Γ) ->
~(n ∈ fv T) ->
~(n ∈ fv ts) ->
~(y ∈ fv T) ->
~(y ∈ fv ts) ->
~(p ∈ fv T) ->
~(p ∈ fv ts) ->
~(n ∈ Θ) ->
~(y ∈ Θ) ->
~(p ∈ Θ) ->
NoDup (n :: y :: p :: nil) ->
wf (erase_term ts) 1 ->
wf T 1 ->
subset (fv T) (support Γ) ->
subset (fv ts) (support Γ) ->
is_annotated_type T ->
is_annotated_term ts ->
cbv_value (erase_term ts) ->
[[ Θ;
(p, T_equiv (fvar y term_var) (tfix T ts)) ::
(y, T_forall (T_refine T_nat (binary_primitive Lt (lvar 0 term_var) (fvar n term_var))) T) ::
(n, T_nat) ::
Γ ⊨
open 0 (open 1 ts (fvar n term_var)) (fvar y term_var) :
open 0 T (fvar n term_var) ]]
->
[[ Θ; Γ ⊨ tfix T ts : T_forall T_nat T ]].
Proof.
intros; apply open_reducible_fix_strong_induction with n y p;
repeat step || erase_open ||
(rewrite (open_none (erase_term ts)) in * by auto) ||
(rewrite erase_type_shift in *);
side_conditions.
Qed.