-
Notifications
You must be signed in to change notification settings - Fork 3
/
AnnotatedNat.v
56 lines (52 loc) · 1.29 KB
/
AnnotatedNat.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
Require Import Coq.Lists.List.
Require Export SystemFR.Judgments.
Require Export SystemFR.AnnotatedTactics.
Require Export SystemFR.ErasedNat.
Lemma annotated_reducible_zero:
forall Θ Γ,
[[ Θ; Γ ⊨ zero : T_nat ]].
Proof.
eauto using open_reducible_zero.
Qed.
Lemma annotated_reducible_succ:
forall Θ Γ t,
[[ Θ; Γ ⊨ t : T_nat ]] ->
[[ Θ; Γ ⊨ succ t : T_nat ]].
Proof.
eauto using open_reducible_succ.
Qed.
Lemma annotated_reducible_match:
forall Θ Γ tn t0 ts T n p,
~(p ∈ fv ts) ->
~(p ∈ fv t0) ->
~(p ∈ fv tn) ->
~(p ∈ fv T) ->
~(p ∈ fv_context Γ) ->
~(n ∈ fv tn) ->
~(n ∈ fv ts) ->
~(n ∈ fv T) ->
~(n ∈ fv_context Γ) ->
~(n = p) ->
~(n ∈ Θ) ->
~(p ∈ Θ) ->
wf ts 1 ->
wf t0 0 ->
subset (fv t0) (support Γ) ->
subset (fv ts) (support Γ) ->
is_annotated_term ts ->
[[ Θ; Γ ⊨ tn : T_nat ]] ->
[[ Θ; (p, T_equiv tn zero) :: Γ ⊨ t0 : T ]] ->
[[ Θ; (
(p, T_equiv tn (succ (fvar n term_var))) ::
(n, T_nat) ::
Γ
) ⊨
open 0 ts (fvar n term_var) :
T
]]
->
[[ Θ; Γ ⊨ tmatch tn t0 ts : T ]].
Proof.
repeat step || erase_open.
apply open_reducible_match with n p; repeat step || erase_open; side_conditions.
Qed.