Top.TestEqualityEnv
Require Import Helpers.
Require Import Library.
Require Import TestHelpers.
Require Import GMu.TestEquality.
Require Import Translation.
Axiom gngc_simple : ∀ x y i, GN x ≠ GC y i.
Axiom AiBi : ∀ i j, Ai i ≠ Bi j.
Axiom AiAi : ∀ i j, i ≠ j → Ai i ≠ Ai j.
Axiom BiBi : ∀ i j, i ≠ j → Bi i ≠ Bi j.
Axiom pmatch_data : pmatch ≠ data.
Parameter snglhelper : trm_label.
Parameter refl : trm_label. (* TODO automatically generating constructor ids *)
Definition env_pretyp : typ :=
{ GN Eq ==
μ
{Ai 1 >: ⊥ <: ⊤} ∧ {Ai 2 >: ⊥ <: ⊤}
∧ {pmatch ⦂ ∀ ({GenT >: ⊥ <: ⊤})
∀ ( ∀ (ssuper ↓ GC Eq 0 ∧ {{super}} ) (super ↓ GenT))
(super ↓ GenT)
}
}
∧ { GC Eq 0 ==
μ
super ↓ GN Eq
∧ {Bi 1 >: ⊥ <: ⊤}
∧ {Ai 1 == this ↓ Bi 1} ∧ {Ai 2 == this ↓ Bi 1}
∧ {data ⦂ ssuper ↓ Unit}
}
∧ { refl ⦂ ∀ ({Bi 1 >: ⊥ <: ⊤}) ((super ↓ GN Eq) ∧ {Ai 1 == this ↓ Bi 1} ∧ {Ai 2 == this ↓ Bi 1}) }
(* we should also take unit here, as the data arg, but that seems unnecessary *)
(* ∧ { refl ⦂ ∀ ({Bi 1 >: ⊥ <: ⊤}) ((super ↓ GC Eq 0) ∧ {Bi 1 == this ↓ Bi 1}) } *)
.
Definition env_typ : typ :=
μ (env_pretyp).
Definition env_trm : trm :=
let_trm
(ν (env_pretyp)
{(
{ GN Eq ⦂=
μ
{Ai 1 >: ⊥ <: ⊤} ∧ {Ai 2 >: ⊥ <: ⊤}
∧ {pmatch ⦂ ∀ ({GenT >: ⊥ <: ⊤})
∀ ( ∀ (ssuper ↓ GC Eq 0 ∧ {{super}} ) (super ↓ GenT))
(super ↓ GenT)
}
},
{ GC Eq 0 ⦂=
μ
super ↓ GN Eq
∧ {Bi 1 >: ⊥ <: ⊤}
∧ {Ai 1 == this ↓ Bi 1} ∧ {Ai 2 == this ↓ Bi 1}
∧ {data ⦂ ssuper ↓ Unit}
},
{ refl :=
λ ({Bi 1 >: ⊥ <: ⊤}) let_trm (
ν(
{Ai 1 == this ↓ Bi 1} ∧ {Ai 2 == this ↓ Bi 1}
∧ {pmatch ⦂ ∀ ({GenT >: ⊥ <: ⊤})
∀ ( ∀ ((ref 3) ↓ GC Eq 0 ∧ {{super}} ) (super ↓ GenT))
(super ↓ GenT)
}
∧ {Bi 1 == super ↓ Bi 1}
∧ {data ⦂ {{(ref 3) • mkUnit}} }
) {(
{Ai 1 ⦂= this ↓ Bi 1}, (* TODO this or super *)
{Ai 2 ⦂= this ↓ Bi 1},
{pmatch :=
λ ({GenT >: ⊥ <: ⊤})
λ ( ∀ ((ref 3) ↓ GC Eq 0 ∧ {{super}} ) (super ↓ GenT))
(* TODO may need a let for self *)
trm_let
(ν({snglhelper ⦂ {{ref 3}} }) {( {snglhelper := ref 3} )})
(trm_app super (this • snglhelper))
},
{Bi 1 ⦂= super ↓ Bi 1},
{data := (ref 3) • mkUnit}
)}
)
}
)}
).
Lemma env_types : ∀ lib,
empty & lib ¬ libType ⊢ open_trm_p (pvar lib) env_trm : open_typ_p (pvar lib) env_typ.
Proof.
intros.
cbv. crush.
apply_fresh ty_let as env.
- apply_fresh ty_new_intro as self_env.
crush.
repeat apply ty_defs_cons; try apply ty_defs_one;
crush.
1: {
invert_label.
false× gngc_simple.
}
apply ty_def_all.
apply_fresh ty_all_intro as BTL. crush.
cleanup.
apply_fresh ty_let as res.
1: {
apply_fresh ty_new_intro as self_res.
crush.
repeat apply ty_defs_cons; try apply ty_defs_one;
crush.
- invert_label.
false× AiAi.
- apply ty_def_all.
apply_fresh ty_all_intro as pmTL; crush.
apply_fresh ty_all_intro as case_refl; crush.
apply_fresh ty_let as Pself.
+ apply_fresh ty_new_intro as self_helper.
apply ty_defs_one.
eapply ty_def_path.
cbn. apply ty_var. solve_bind.
+ crush.
fold ((pvar Pself) • snglhelper).
assert (HR: pvar pmTL ↓ GenT = open_typ_p ((pvar Pself) • snglhelper) (pvar pmTL ↓ GenT)) by crush.
rewrite HR.
eapply ty_all_elim.
× apply ty_var; solve_bind.
× match goal with
| [ |- ?G ⊢ ?t : ?A ∧ ?B ] ⇒
assert (G ⊢ t : B)
end.
1: {
apply ty_new_elim.
match goal with
| [ |- ?G ⊢ ?t : ?T ] ⇒
assert (HR2: T = open_typ_p (pvar Pself) T) by crush
end.
rewrite HR2.
apply ty_rec_elim.
apply ty_var. solve_bind.
}
cleanup.
apply ty_and_intro; auto.
crush.
fold ((pvar Pself) • snglhelper).
apply ty_sngl with (pvar self_res); auto.
match goal with
| [ |- context [ {GC Eq 0 == ?T} ] ] ⇒
apply ty_sub with T
end.
2: {
subsel2.
var_subtyp.
- apply ty_var; solve_bind.
- solve_subtyp_and.
}
apply ty_rec_intro.
crush.
repeat apply ty_and_intro;
try solve [var_subtyp2; solve_subtyp_and].
-- match goal with
| [ |- context [ {GN Eq == ?T} ] ] ⇒
apply ty_sub with T
end.
++ apply ty_rec_intro.
crush.
var_subtyp2.
eapply subtyp_trans; try apply subtyp_and11.
eapply subtyp_trans; try apply subtyp_and11.
repeat apply intersection_order; auto.
++ subsel2.
var_subtyp.
** apply ty_var; solve_bind.
** solve_subtyp_and.
-- var_subtyp2.
eapply subtyp_trans; try apply subtyp_and11.
eapply subtyp_trans; try apply subtyp_and12.
apply subtyp_typ; auto.
-- apply ty_rcd_intro.
fold ((pvar lib) • mkUnit).
apply ty_sngl with ((pvar lib) • mkUnit).
++ apply ty_new_elim.
var_subtyp2.
solve_subtyp_and.
++ apply ty_new_elim.
var_subtyp_mu2.
solve_subtyp_and.
- invert_label.
false× AiBi.
- invert_label.
false× AiBi.
- eapply ty_def_path.
fold ((pvar lib) • mkUnit).
apply ty_new_elim.
var_subtyp_mu2.
eapply subtyp_trans; try apply subtyp_and11.
apply subtyp_and12.
- invert_label.
false× pmatch_data.
}
crush.
repeat apply ty_and_intro.
+ match goal with
| [ |- context [ {GN Eq == ?T} ] ] ⇒
apply ty_sub with T
end.
× apply ty_rec_intro.
crush.
var_subtyp_mu2.
eapply subtyp_trans; try apply subtyp_and11.
eapply subtyp_trans; try apply subtyp_and11.
repeat apply intersection_order; auto.
× subsel2.
var_subtyp.
-- apply ty_var; solve_bind.
-- solve_subtyp_and.
+ var_subtyp_mu2.
solve_subtyp_and.
apply subtyp_typ;
[subsel2 | subsel1];
var_subtyp_mu2;
solve_subtyp_and.
+ var_subtyp_mu2.
repeat
match goal with
| [ |- ?G ⊢ ?A ∧ ?B <: ?C ] ⇒
match B with
| typ_rcd {?N == ?T} ⇒
match C with
| typ_rcd {N == ?U} ⇒
eapply subtyp_trans; try apply subtyp_and12
| _ ⇒
eapply subtyp_trans; try apply subtyp_and11
end
| C ⇒
apply subtyp_and12
| _ ⇒
eapply subtyp_trans; try apply subtyp_and11
end
end.
apply subtyp_typ;
[subsel2 | subsel1];
var_subtyp_mu2;
solve_subtyp_and.
- crush.
Qed.
Require Import Library.
Require Import TestHelpers.
Require Import GMu.TestEquality.
Require Import Translation.
Axiom gngc_simple : ∀ x y i, GN x ≠ GC y i.
Axiom AiBi : ∀ i j, Ai i ≠ Bi j.
Axiom AiAi : ∀ i j, i ≠ j → Ai i ≠ Ai j.
Axiom BiBi : ∀ i j, i ≠ j → Bi i ≠ Bi j.
Axiom pmatch_data : pmatch ≠ data.
Parameter snglhelper : trm_label.
Parameter refl : trm_label. (* TODO automatically generating constructor ids *)
Definition env_pretyp : typ :=
{ GN Eq ==
μ
{Ai 1 >: ⊥ <: ⊤} ∧ {Ai 2 >: ⊥ <: ⊤}
∧ {pmatch ⦂ ∀ ({GenT >: ⊥ <: ⊤})
∀ ( ∀ (ssuper ↓ GC Eq 0 ∧ {{super}} ) (super ↓ GenT))
(super ↓ GenT)
}
}
∧ { GC Eq 0 ==
μ
super ↓ GN Eq
∧ {Bi 1 >: ⊥ <: ⊤}
∧ {Ai 1 == this ↓ Bi 1} ∧ {Ai 2 == this ↓ Bi 1}
∧ {data ⦂ ssuper ↓ Unit}
}
∧ { refl ⦂ ∀ ({Bi 1 >: ⊥ <: ⊤}) ((super ↓ GN Eq) ∧ {Ai 1 == this ↓ Bi 1} ∧ {Ai 2 == this ↓ Bi 1}) }
(* we should also take unit here, as the data arg, but that seems unnecessary *)
(* ∧ { refl ⦂ ∀ ({Bi 1 >: ⊥ <: ⊤}) ((super ↓ GC Eq 0) ∧ {Bi 1 == this ↓ Bi 1}) } *)
.
Definition env_typ : typ :=
μ (env_pretyp).
Definition env_trm : trm :=
let_trm
(ν (env_pretyp)
{(
{ GN Eq ⦂=
μ
{Ai 1 >: ⊥ <: ⊤} ∧ {Ai 2 >: ⊥ <: ⊤}
∧ {pmatch ⦂ ∀ ({GenT >: ⊥ <: ⊤})
∀ ( ∀ (ssuper ↓ GC Eq 0 ∧ {{super}} ) (super ↓ GenT))
(super ↓ GenT)
}
},
{ GC Eq 0 ⦂=
μ
super ↓ GN Eq
∧ {Bi 1 >: ⊥ <: ⊤}
∧ {Ai 1 == this ↓ Bi 1} ∧ {Ai 2 == this ↓ Bi 1}
∧ {data ⦂ ssuper ↓ Unit}
},
{ refl :=
λ ({Bi 1 >: ⊥ <: ⊤}) let_trm (
ν(
{Ai 1 == this ↓ Bi 1} ∧ {Ai 2 == this ↓ Bi 1}
∧ {pmatch ⦂ ∀ ({GenT >: ⊥ <: ⊤})
∀ ( ∀ ((ref 3) ↓ GC Eq 0 ∧ {{super}} ) (super ↓ GenT))
(super ↓ GenT)
}
∧ {Bi 1 == super ↓ Bi 1}
∧ {data ⦂ {{(ref 3) • mkUnit}} }
) {(
{Ai 1 ⦂= this ↓ Bi 1}, (* TODO this or super *)
{Ai 2 ⦂= this ↓ Bi 1},
{pmatch :=
λ ({GenT >: ⊥ <: ⊤})
λ ( ∀ ((ref 3) ↓ GC Eq 0 ∧ {{super}} ) (super ↓ GenT))
(* TODO may need a let for self *)
trm_let
(ν({snglhelper ⦂ {{ref 3}} }) {( {snglhelper := ref 3} )})
(trm_app super (this • snglhelper))
},
{Bi 1 ⦂= super ↓ Bi 1},
{data := (ref 3) • mkUnit}
)}
)
}
)}
).
Lemma env_types : ∀ lib,
empty & lib ¬ libType ⊢ open_trm_p (pvar lib) env_trm : open_typ_p (pvar lib) env_typ.
Proof.
intros.
cbv. crush.
apply_fresh ty_let as env.
- apply_fresh ty_new_intro as self_env.
crush.
repeat apply ty_defs_cons; try apply ty_defs_one;
crush.
1: {
invert_label.
false× gngc_simple.
}
apply ty_def_all.
apply_fresh ty_all_intro as BTL. crush.
cleanup.
apply_fresh ty_let as res.
1: {
apply_fresh ty_new_intro as self_res.
crush.
repeat apply ty_defs_cons; try apply ty_defs_one;
crush.
- invert_label.
false× AiAi.
- apply ty_def_all.
apply_fresh ty_all_intro as pmTL; crush.
apply_fresh ty_all_intro as case_refl; crush.
apply_fresh ty_let as Pself.
+ apply_fresh ty_new_intro as self_helper.
apply ty_defs_one.
eapply ty_def_path.
cbn. apply ty_var. solve_bind.
+ crush.
fold ((pvar Pself) • snglhelper).
assert (HR: pvar pmTL ↓ GenT = open_typ_p ((pvar Pself) • snglhelper) (pvar pmTL ↓ GenT)) by crush.
rewrite HR.
eapply ty_all_elim.
× apply ty_var; solve_bind.
× match goal with
| [ |- ?G ⊢ ?t : ?A ∧ ?B ] ⇒
assert (G ⊢ t : B)
end.
1: {
apply ty_new_elim.
match goal with
| [ |- ?G ⊢ ?t : ?T ] ⇒
assert (HR2: T = open_typ_p (pvar Pself) T) by crush
end.
rewrite HR2.
apply ty_rec_elim.
apply ty_var. solve_bind.
}
cleanup.
apply ty_and_intro; auto.
crush.
fold ((pvar Pself) • snglhelper).
apply ty_sngl with (pvar self_res); auto.
match goal with
| [ |- context [ {GC Eq 0 == ?T} ] ] ⇒
apply ty_sub with T
end.
2: {
subsel2.
var_subtyp.
- apply ty_var; solve_bind.
- solve_subtyp_and.
}
apply ty_rec_intro.
crush.
repeat apply ty_and_intro;
try solve [var_subtyp2; solve_subtyp_and].
-- match goal with
| [ |- context [ {GN Eq == ?T} ] ] ⇒
apply ty_sub with T
end.
++ apply ty_rec_intro.
crush.
var_subtyp2.
eapply subtyp_trans; try apply subtyp_and11.
eapply subtyp_trans; try apply subtyp_and11.
repeat apply intersection_order; auto.
++ subsel2.
var_subtyp.
** apply ty_var; solve_bind.
** solve_subtyp_and.
-- var_subtyp2.
eapply subtyp_trans; try apply subtyp_and11.
eapply subtyp_trans; try apply subtyp_and12.
apply subtyp_typ; auto.
-- apply ty_rcd_intro.
fold ((pvar lib) • mkUnit).
apply ty_sngl with ((pvar lib) • mkUnit).
++ apply ty_new_elim.
var_subtyp2.
solve_subtyp_and.
++ apply ty_new_elim.
var_subtyp_mu2.
solve_subtyp_and.
- invert_label.
false× AiBi.
- invert_label.
false× AiBi.
- eapply ty_def_path.
fold ((pvar lib) • mkUnit).
apply ty_new_elim.
var_subtyp_mu2.
eapply subtyp_trans; try apply subtyp_and11.
apply subtyp_and12.
- invert_label.
false× pmatch_data.
}
crush.
repeat apply ty_and_intro.
+ match goal with
| [ |- context [ {GN Eq == ?T} ] ] ⇒
apply ty_sub with T
end.
× apply ty_rec_intro.
crush.
var_subtyp_mu2.
eapply subtyp_trans; try apply subtyp_and11.
eapply subtyp_trans; try apply subtyp_and11.
repeat apply intersection_order; auto.
× subsel2.
var_subtyp.
-- apply ty_var; solve_bind.
-- solve_subtyp_and.
+ var_subtyp_mu2.
solve_subtyp_and.
apply subtyp_typ;
[subsel2 | subsel1];
var_subtyp_mu2;
solve_subtyp_and.
+ var_subtyp_mu2.
repeat
match goal with
| [ |- ?G ⊢ ?A ∧ ?B <: ?C ] ⇒
match B with
| typ_rcd {?N == ?T} ⇒
match C with
| typ_rcd {N == ?U} ⇒
eapply subtyp_trans; try apply subtyp_and12
| _ ⇒
eapply subtyp_trans; try apply subtyp_and11
end
| C ⇒
apply subtyp_and12
| _ ⇒
eapply subtyp_trans; try apply subtyp_and11
end
end.
apply subtyp_typ;
[subsel2 | subsel1];
var_subtyp_mu2;
solve_subtyp_and.
- crush.
Qed.