SystemFR/NormalizationSing.v at main · epfl-lara/SystemFR · GitHub

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
Require Export SystemFR.DeltaBetaReduction.
Require Export SystemFR.ErasedSingleton.
Require Export SystemFR.ReducibilityEquivalent.

Opaque reducible_values.

Lemma open_reduce_singleton:
  forall Θ Γ T t t',
    wf t 0 ->
    wf t' 0 ->
    [ Θ; Γ ⊨ t ≡ t' ] ->
    [ Θ; Γ ⊨ T_singleton T t = T_singleton T t' ].
Proof.
  unfold open_equivalent_types, equivalent_types;
    repeat step || simp_red || top_level_unfold open_equivalent || t_instantiate_sat3 ||
           rewrite shift_nothing2 in * by eauto with wf;
    t_closer;
    try solve [ eexists; repeat step || open_none; eauto using equivalent_trans, equivalent_sym ].
Qed.

Lemma open_nsing_helper:
  forall Θ Γ U T t t' t'',
    wf t 0 ->
    wf t' 0 ->
    wf t'' 0 ->
    wf T 0 ->
    wf U 0 ->
    is_erased_term t ->
    is_erased_term t'' ->
    is_erased_type U ->
    is_erased_type T ->
    subset (fv U) (support Γ) ->
    subset (fv T) (support Γ) ->
    [ Θ; Γ ⊨ t ≡ t' ] ->
    [ Θ; Γ ⊨ t : U ] ->
    [ Θ; Γ ⊨ t' : T_singleton T t'' ] ->
    [ Θ; Γ ⊨ T_singleton U t = T_singleton T t'' ].
Proof.
  unfold T_singleton;
    repeat step || unfold open_equivalent_types || unfold equivalent_types || simp_red ||
           open_none || unfold open_equivalent in * ||
           unfold open_reducible in * || t_instantiate_sat3 ||
           (rewrite shift_nothing2 in * by eauto with wf);
    t_closer.

  - apply reducible_expr_value; eauto with values.
    eapply reducibility_equivalent2; eauto using equivalent_sym; steps; t_closer.
    apply reducibility_equivalent2 with (psubstitute t' l term_var); steps;
      eauto using equivalent_sym;
      eauto using reducible_type_refine2;
      t_closer.

  - eexists; steps.
    unfold reduces_to in H22; repeat step || simp_red || open_none.
    eapply equivalent_trans; eauto.
    eapply equivalent_trans; eauto.
    eapply equivalent_trans; eauto; equivalent_star.

  - apply reducible_expr_value; eauto with values.
    eapply reducibility_equivalent2; eauto using equivalent_sym; steps; t_closer.

    unfold reduces_to in H22; repeat step || simp_red || open_none.
    eapply reducibility_equivalent2; eauto; steps; t_closer.
    eapply reducibility_equivalent2; eauto; steps; t_closer.
    eapply equivalent_trans; eauto; equivalent_star.

  - eexists; steps.
    unfold reduces_to in H22; repeat step || simp_red || open_none.
    eapply equivalent_trans; eauto.
    eapply equivalent_trans; eauto using equivalent_sym.
    apply equivalent_trans with (psubstitute t' l term_var);
      try solve [ apply equivalent_sym; equivalent_star ];
      eauto using equivalent_sym.
Qed.

Lemma open_nsing:
  forall Γ U T t t' t'',
    wf t 0 ->
    wf t' 0 ->
    wf t'' 0 ->
    wf T 0 ->
    wf U 0 ->
    is_erased_term t ->
    is_erased_term t'' ->
    is_erased_type U ->
    is_erased_type T ->
    subset (fv U) (support Γ) ->
    subset (fv T) (support Γ) ->
    [ Γ ⊨ t ⤳* t' ] ->
    [ Γ ⊫ t : U ] ->
    [ Γ ⊫ t' : T_singleton T t'' ] ->
    [ Γ ⊫ T_singleton U t = T_singleton T t'' ].
Proof.
  eauto using open_nsing_helper, delta_beta_obs_equiv.
Qed.