GMuAnnot.Equations
Require Import GMuAnnot.Prelude.
Require Import GMuAnnot.Infrastructure.
Open Scope list_scope.
(* Proofs regarding proposition 2.1 from the paper *)
Section SimpleEquationProperties.
Variable Σ : GADTEnv.
Lemma teq_reflexivity : ∀ Δ T,
entails_semantic Σ Δ (T ≡ T).
cbn.
intros.
auto.
Qed.
Lemma teq_symmetry : ∀ Δ T U,
entails_semantic Σ Δ (T ≡ U) →
entails_semantic Σ Δ (U ≡ T).
cbn. intros.
symmetry.
auto.
Qed.
Lemma teq_transitivity : ∀ Δ T U V,
entails_semantic Σ Δ (T ≡ U) →
entails_semantic Σ Δ (U ≡ V) →
entails_semantic Σ Δ (T ≡ V).
cbn. intros.
transitivity (subst_tt' U Θ); auto.
Qed.
Lemma subst_has_no_fv : ∀ Σ Δ Θ,
subst_matches_typctx Σ Δ Θ →
(∀ X U, List.In (X, U) Θ → fv_typ U = \{}).
induction 1; introv Hin.
- false.
- cbn in Hin.
destruct Hin as [Hin | Hin].
+ inversions Hin.
lets Hfv: wft_gives_fv H.
cbn in Hfv.
apply¬ fset_extens.
+ apply× IHsubst_matches_typctx.
- apply× IHsubst_matches_typctx.
Qed.
Lemma teq_axiom : ∀ Δ T U,
List.In (tc_eq (T ≡ U)) Δ →
entails_semantic Σ Δ (T ≡ U).
unfold entails_semantic.
induction Δ; introv Hin M.
- contradiction.
- cbn in Hin.
destruct Hin as [Hin | Hin].
+ subst. inversion M.
easy.
+ inversion M; auto.
cbn.
repeat rewrite subst_tt_inside; auto.
× f_equal.
apply IHΔ; auto.
× introv Uin.
lets Fr: subst_has_no_fv Uin.
-- eauto.
-- rewrite Fr. apply notin_empty.
× introv Uin.
lets Fr: subst_has_no_fv Uin.
-- eauto.
-- rewrite Fr. apply notin_empty.
Qed.
End SimpleEquationProperties.
Ltac fold_from_list :=
repeat progress match goal with
| [ H: context[LibList.fold_right (fun (x : var) (acc : fset var) ⇒ \{ x} \u acc) \{} ?L] |- _ ] ⇒
fold (from_list L) in H
| |- context[LibList.fold_right (fun (x : var) (acc : fset var) ⇒ \{ x} \u acc) \{} ?L] ⇒
fold (from_list L)
end.
Lemma notin_from_list : ∀ As (A : var),
¬ (List.In A As) →
A \notin from_list As.
intros.
intro HF.
lets [A' [Hin Heq]]: in_from_list HF.
subst.
auto.
Qed.
Lemma spawn_unit_subst : ∀ Σ As,
DistinctList As →
∃ Θ, length Θ = length As ∧ subst_matches_typctx Σ (tc_vars As) Θ ∧ substitution_sources Θ = from_list As.
induction As as [| Ah Ats]; introv ADist.
- cbn.
∃ (@nil (var × typ)).
splits¬.
constructor.
- inversions ADist.
destruct IHAts as [LT [Len [Match Src]]]; auto.
∃ ((Ah, typ_unit) :: LT).
splits.
+ cbn. auto.
+ constructor;
fold (List.map tc_var Ats);
fold (tc_vars Ats);
auto.
× rewrite Src.
apply¬ notin_from_list.
× apply notin_dom_tc_vars.
apply¬ notin_from_list.
+ cbn.
fold_from_list.
fold (substitution_sources LT).
rewrite Src.
trivial.
Qed.
Lemma only_vars_is_tc_vars : ∀ Δ,
(∀ tc, List.In tc Δ → ∃ A, tc = tc_var A) →
∃ As, Δ = tc_vars As.
induction Δ as [| [A | eq] Δt].
- cbn. intros. ∃ (@nil var). cbn. trivial.
- cbn. intro Hin.
lets× [Ats EQ]: IHΔt.
∃ (A :: Ats). cbn.
fold (tc_vars Ats).
f_equal.
auto.
- cbn. intro Hin.
false¬ Hin. congruence.
Qed.
Lemma contradictory_env_test_0 : ∀ Σ Δ,
entails_semantic Σ Δ (typ_unit ≡ (typ_unit ** typ_unit)) →
contradictory_bounds Σ Δ.
introv Heq.
unfold contradictory_bounds.
intros.
unfold entails_semantic in ×.
introv Hmatch.
exfalso.
lets HF: Heq Hmatch.
rewrite subst_ttΘ_fresh in HF.
- rewrite subst_ttΘ_fresh in HF.
+ false.
+ cbn. rewrite union_empty_r.
rewrite¬ inter_empty_r.
- cbn.
rewrite¬ inter_empty_r.
Qed.
Lemma subst_ttΘ_into_abs : ∀ Θ A B,
subst_tt' (A ==> B) Θ
=
(subst_tt' A Θ) ==> (subst_tt' B Θ).
induction Θ as [| [X T] Θ]; cbn in *; trivial.
Qed.
Lemma subst_ttΘ_into_tuple : ∀ Θ A B,
subst_tt' (A ** B) Θ
=
(subst_tt' A Θ) ** (subst_tt' B Θ).
induction Θ as [| [X T] Θ]; cbn in *; trivial.
Qed.
Lemma contradictory_env_test : ∀ Σ Δ A B C D,
entails_semantic Σ Δ ((A ==> B) ≡ (C ** D)) →
contradictory_bounds Σ Δ.
introv Heq.
unfold contradictory_bounds.
intros.
unfold entails_semantic in ×.
introv Hmatch.
exfalso.
lets HF: Heq Hmatch.
rewrite subst_ttΘ_into_abs in HF.
rewrite subst_ttΘ_into_tuple in HF.
congruence.
Qed.
Lemma empty_is_not_contradictory : ∀ Σ,
¬ (contradictory_bounds Σ emptyΔ).
intros.
intro HF.
unfold contradictory_bounds in HF.
asserts M: (subst_matches_typctx Σ emptyΔ (@nil (var×typ)));
try econstructor.
lets F: HF typ_unit (typ_unit ** typ_unit) (@nil (var × typ)) M.
cbn in F.
false.
Qed.
Lemma typing_exfalso : ∀ Σ Δ E e T1 T2 TT,
{Σ, Δ, E} ⊢(TT) e ∈ T1 →
contradictory_bounds Σ Δ →
wft Σ Δ T2 →
{Σ, Δ, E} ⊢(Tgen) e ∈ T2.
introv Typ Bounds.
eapply typing_eq; eauto.
Qed.
Lemma inversion_typing_eq : ∀ Σ Δ E e T TT,
{Σ, Δ, E} ⊢(TT) e ∈ T →
∃ T',
{Σ, Δ, E} ⊢(Treg) e ∈ T' ∧ entails_semantic Σ Δ (T ≡ T').
introv Htyp.
lets Htyp2: Htyp.
induction Htyp;
try match goal with
| [ H: {Σ, Δ, E} ⊢(Treg) ?e ∈ ?T |- _ ] ⇒
∃ T; split~; auto using teq_reflexivity
end.
lets [T' [IHTyp IHeq]]: IHHtyp Htyp.
∃ T'.
split¬.
eauto using teq_symmetry, teq_transitivity.
Qed.
Lemma subst_has_no_fv2 : ∀ Σ Δ Θ Y,
subst_matches_typctx Σ Δ Θ →
(∀ A U, List.In (A, U) Θ → Y \notin fv_typ U).
introv M Hin.
lets EQ: subst_has_no_fv M Hin.
rewrite EQ.
auto.
Qed.
Lemma inversion_eq_arrow : ∀ Σ Δ TA1 TB1 TA2 TB2,
entails_semantic Σ Δ ((TA1 ==> TB1) ≡ (TA2 ==> TB2)) →
entails_semantic Σ Δ (TA1 ≡ TA2) ∧
entails_semantic Σ Δ (TB1 ≡ TB2).
introv Sem; cbn in ×.
split~;
introv M;
lets EQ: Sem M;
repeat rewrite subst_tt_prime_reduce_arrow in EQ;
inversion¬ EQ.
Qed.
Lemma inversion_eq_tuple : ∀ Σ Δ TA1 TB1 TA2 TB2,
entails_semantic Σ Δ ((TA1 ** TB1) ≡ (TA2 ** TB2)) →
entails_semantic Σ Δ (TA1 ≡ TA2) ∧
entails_semantic Σ Δ (TB1 ≡ TB2).
introv Sem; cbn in ×.
split~;
introv M;
lets EQ: Sem M;
repeat rewrite subst_tt_prime_reduce_tuple in EQ;
inversion¬ EQ.
Qed.
Lemma inversion_eq_typ_all : ∀ Σ Δ T U,
entails_semantic Σ Δ (typ_all T ≡ typ_all U) →
entails_semantic Σ Δ (T ≡ U).
introv Sem; cbn in ×.
introv M;
lets EQ: Sem M;
repeat rewrite subst_tt_prime_reduce_typ_all in EQ;
inversion¬ EQ.
Qed.
Lemma inversion_eq_typ_gadt : ∀ Σ Δ Ts Us N,
List.length Ts = List.length Us →
entails_semantic Σ Δ (typ_gadt Ts N ≡ typ_gadt Us N) →
List.Forall2 (fun T U ⇒ entails_semantic Σ Δ (T ≡ U)) Ts Us.
introv Len Sem.
apply F2_iff_In_zip.
split¬.
intros T U In.
cbn in ×.
introv M.
lets EQ: Sem M.
repeat rewrite subst_tt_prime_reduce_typ_gadt in EQ.
inversion EQ as [EQ2].
lets¬ : lists_map_eq EQ2 In.
Qed.
Lemma equations_from_lists_map : ∀ F F1 F2 Ts Us,
List.length Ts = List.length Us →
(∀ T U, List.In (T,U) (zip Ts Us) → F (tc_eq (T ≡ U)) = tc_eq (F1 T ≡ F2 U)) →
List.map F (equations_from_lists Ts Us)
=
equations_from_lists (List.map F1 Ts) (List.map F2 Us).
induction Ts as [| T Ts]; destruct Us as [| U Us];
introv Len; try solve [inversion¬ Len].
introv EQ.
cbn.
fold (equations_from_lists Ts Us).
fold (equations_from_lists (List.map F1 Ts) (List.map F2 Us)).
f_equal.
- apply EQ. cbn. auto.
- apply× IHTs.
introv In.
apply EQ. cbn. auto.
Qed.
Require Import GMuAnnot.Infrastructure.
Open Scope list_scope.
(* Proofs regarding proposition 2.1 from the paper *)
Section SimpleEquationProperties.
Variable Σ : GADTEnv.
Lemma teq_reflexivity : ∀ Δ T,
entails_semantic Σ Δ (T ≡ T).
cbn.
intros.
auto.
Qed.
Lemma teq_symmetry : ∀ Δ T U,
entails_semantic Σ Δ (T ≡ U) →
entails_semantic Σ Δ (U ≡ T).
cbn. intros.
symmetry.
auto.
Qed.
Lemma teq_transitivity : ∀ Δ T U V,
entails_semantic Σ Δ (T ≡ U) →
entails_semantic Σ Δ (U ≡ V) →
entails_semantic Σ Δ (T ≡ V).
cbn. intros.
transitivity (subst_tt' U Θ); auto.
Qed.
Lemma subst_has_no_fv : ∀ Σ Δ Θ,
subst_matches_typctx Σ Δ Θ →
(∀ X U, List.In (X, U) Θ → fv_typ U = \{}).
induction 1; introv Hin.
- false.
- cbn in Hin.
destruct Hin as [Hin | Hin].
+ inversions Hin.
lets Hfv: wft_gives_fv H.
cbn in Hfv.
apply¬ fset_extens.
+ apply× IHsubst_matches_typctx.
- apply× IHsubst_matches_typctx.
Qed.
Lemma teq_axiom : ∀ Δ T U,
List.In (tc_eq (T ≡ U)) Δ →
entails_semantic Σ Δ (T ≡ U).
unfold entails_semantic.
induction Δ; introv Hin M.
- contradiction.
- cbn in Hin.
destruct Hin as [Hin | Hin].
+ subst. inversion M.
easy.
+ inversion M; auto.
cbn.
repeat rewrite subst_tt_inside; auto.
× f_equal.
apply IHΔ; auto.
× introv Uin.
lets Fr: subst_has_no_fv Uin.
-- eauto.
-- rewrite Fr. apply notin_empty.
× introv Uin.
lets Fr: subst_has_no_fv Uin.
-- eauto.
-- rewrite Fr. apply notin_empty.
Qed.
End SimpleEquationProperties.
Ltac fold_from_list :=
repeat progress match goal with
| [ H: context[LibList.fold_right (fun (x : var) (acc : fset var) ⇒ \{ x} \u acc) \{} ?L] |- _ ] ⇒
fold (from_list L) in H
| |- context[LibList.fold_right (fun (x : var) (acc : fset var) ⇒ \{ x} \u acc) \{} ?L] ⇒
fold (from_list L)
end.
Lemma notin_from_list : ∀ As (A : var),
¬ (List.In A As) →
A \notin from_list As.
intros.
intro HF.
lets [A' [Hin Heq]]: in_from_list HF.
subst.
auto.
Qed.
Lemma spawn_unit_subst : ∀ Σ As,
DistinctList As →
∃ Θ, length Θ = length As ∧ subst_matches_typctx Σ (tc_vars As) Θ ∧ substitution_sources Θ = from_list As.
induction As as [| Ah Ats]; introv ADist.
- cbn.
∃ (@nil (var × typ)).
splits¬.
constructor.
- inversions ADist.
destruct IHAts as [LT [Len [Match Src]]]; auto.
∃ ((Ah, typ_unit) :: LT).
splits.
+ cbn. auto.
+ constructor;
fold (List.map tc_var Ats);
fold (tc_vars Ats);
auto.
× rewrite Src.
apply¬ notin_from_list.
× apply notin_dom_tc_vars.
apply¬ notin_from_list.
+ cbn.
fold_from_list.
fold (substitution_sources LT).
rewrite Src.
trivial.
Qed.
Lemma only_vars_is_tc_vars : ∀ Δ,
(∀ tc, List.In tc Δ → ∃ A, tc = tc_var A) →
∃ As, Δ = tc_vars As.
induction Δ as [| [A | eq] Δt].
- cbn. intros. ∃ (@nil var). cbn. trivial.
- cbn. intro Hin.
lets× [Ats EQ]: IHΔt.
∃ (A :: Ats). cbn.
fold (tc_vars Ats).
f_equal.
auto.
- cbn. intro Hin.
false¬ Hin. congruence.
Qed.
Lemma contradictory_env_test_0 : ∀ Σ Δ,
entails_semantic Σ Δ (typ_unit ≡ (typ_unit ** typ_unit)) →
contradictory_bounds Σ Δ.
introv Heq.
unfold contradictory_bounds.
intros.
unfold entails_semantic in ×.
introv Hmatch.
exfalso.
lets HF: Heq Hmatch.
rewrite subst_ttΘ_fresh in HF.
- rewrite subst_ttΘ_fresh in HF.
+ false.
+ cbn. rewrite union_empty_r.
rewrite¬ inter_empty_r.
- cbn.
rewrite¬ inter_empty_r.
Qed.
Lemma subst_ttΘ_into_abs : ∀ Θ A B,
subst_tt' (A ==> B) Θ
=
(subst_tt' A Θ) ==> (subst_tt' B Θ).
induction Θ as [| [X T] Θ]; cbn in *; trivial.
Qed.
Lemma subst_ttΘ_into_tuple : ∀ Θ A B,
subst_tt' (A ** B) Θ
=
(subst_tt' A Θ) ** (subst_tt' B Θ).
induction Θ as [| [X T] Θ]; cbn in *; trivial.
Qed.
Lemma contradictory_env_test : ∀ Σ Δ A B C D,
entails_semantic Σ Δ ((A ==> B) ≡ (C ** D)) →
contradictory_bounds Σ Δ.
introv Heq.
unfold contradictory_bounds.
intros.
unfold entails_semantic in ×.
introv Hmatch.
exfalso.
lets HF: Heq Hmatch.
rewrite subst_ttΘ_into_abs in HF.
rewrite subst_ttΘ_into_tuple in HF.
congruence.
Qed.
Lemma empty_is_not_contradictory : ∀ Σ,
¬ (contradictory_bounds Σ emptyΔ).
intros.
intro HF.
unfold contradictory_bounds in HF.
asserts M: (subst_matches_typctx Σ emptyΔ (@nil (var×typ)));
try econstructor.
lets F: HF typ_unit (typ_unit ** typ_unit) (@nil (var × typ)) M.
cbn in F.
false.
Qed.
Lemma typing_exfalso : ∀ Σ Δ E e T1 T2 TT,
{Σ, Δ, E} ⊢(TT) e ∈ T1 →
contradictory_bounds Σ Δ →
wft Σ Δ T2 →
{Σ, Δ, E} ⊢(Tgen) e ∈ T2.
introv Typ Bounds.
eapply typing_eq; eauto.
Qed.
Lemma inversion_typing_eq : ∀ Σ Δ E e T TT,
{Σ, Δ, E} ⊢(TT) e ∈ T →
∃ T',
{Σ, Δ, E} ⊢(Treg) e ∈ T' ∧ entails_semantic Σ Δ (T ≡ T').
introv Htyp.
lets Htyp2: Htyp.
induction Htyp;
try match goal with
| [ H: {Σ, Δ, E} ⊢(Treg) ?e ∈ ?T |- _ ] ⇒
∃ T; split~; auto using teq_reflexivity
end.
lets [T' [IHTyp IHeq]]: IHHtyp Htyp.
∃ T'.
split¬.
eauto using teq_symmetry, teq_transitivity.
Qed.
Lemma subst_has_no_fv2 : ∀ Σ Δ Θ Y,
subst_matches_typctx Σ Δ Θ →
(∀ A U, List.In (A, U) Θ → Y \notin fv_typ U).
introv M Hin.
lets EQ: subst_has_no_fv M Hin.
rewrite EQ.
auto.
Qed.
Lemma inversion_eq_arrow : ∀ Σ Δ TA1 TB1 TA2 TB2,
entails_semantic Σ Δ ((TA1 ==> TB1) ≡ (TA2 ==> TB2)) →
entails_semantic Σ Δ (TA1 ≡ TA2) ∧
entails_semantic Σ Δ (TB1 ≡ TB2).
introv Sem; cbn in ×.
split~;
introv M;
lets EQ: Sem M;
repeat rewrite subst_tt_prime_reduce_arrow in EQ;
inversion¬ EQ.
Qed.
Lemma inversion_eq_tuple : ∀ Σ Δ TA1 TB1 TA2 TB2,
entails_semantic Σ Δ ((TA1 ** TB1) ≡ (TA2 ** TB2)) →
entails_semantic Σ Δ (TA1 ≡ TA2) ∧
entails_semantic Σ Δ (TB1 ≡ TB2).
introv Sem; cbn in ×.
split~;
introv M;
lets EQ: Sem M;
repeat rewrite subst_tt_prime_reduce_tuple in EQ;
inversion¬ EQ.
Qed.
Lemma inversion_eq_typ_all : ∀ Σ Δ T U,
entails_semantic Σ Δ (typ_all T ≡ typ_all U) →
entails_semantic Σ Δ (T ≡ U).
introv Sem; cbn in ×.
introv M;
lets EQ: Sem M;
repeat rewrite subst_tt_prime_reduce_typ_all in EQ;
inversion¬ EQ.
Qed.
Lemma inversion_eq_typ_gadt : ∀ Σ Δ Ts Us N,
List.length Ts = List.length Us →
entails_semantic Σ Δ (typ_gadt Ts N ≡ typ_gadt Us N) →
List.Forall2 (fun T U ⇒ entails_semantic Σ Δ (T ≡ U)) Ts Us.
introv Len Sem.
apply F2_iff_In_zip.
split¬.
intros T U In.
cbn in ×.
introv M.
lets EQ: Sem M.
repeat rewrite subst_tt_prime_reduce_typ_gadt in EQ.
inversion EQ as [EQ2].
lets¬ : lists_map_eq EQ2 In.
Qed.
Lemma equations_from_lists_map : ∀ F F1 F2 Ts Us,
List.length Ts = List.length Us →
(∀ T U, List.In (T,U) (zip Ts Us) → F (tc_eq (T ≡ U)) = tc_eq (F1 T ≡ F2 U)) →
List.map F (equations_from_lists Ts Us)
=
equations_from_lists (List.map F1 Ts) (List.map F2 Us).
induction Ts as [| T Ts]; destruct Us as [| U Us];
introv Len; try solve [inversion¬ Len].
introv EQ.
cbn.
fold (equations_from_lists Ts Us).
fold (equations_from_lists (List.map F1 Ts) (List.map F2 Us)).
f_equal.
- apply EQ. cbn. auto.
- apply× IHTs.
introv In.
apply EQ. cbn. auto.
Qed.