OpSemProofs.properties_of_relations
Require Import Coq.Classes.RelationClasses.
Require Import utils.
Require Import syntax.
Require Import relations.
Require Import integration.
Require Import utils.
Require Import syntax.
Require Import relations.
Require Import integration.
Lemma A_rel_symmetric' {τ} :
Symmetric (V_rel τ) ->
Symmetric (A_rel τ).
Proof.
repeat intro.
apply eq_sym.
apply H0, H, Hv.
Qed.
Lemma E_rel_symmetric' {τ} :
Symmetric (V_rel τ) ->
Symmetric (E_rel τ).
Proof.
repeat intro.
apply eq_sym.
apply H0.
apply A_rel_symmetric'; auto.
Qed.
Instance V_rel_symmetric {τ} : Symmetric (V_rel τ).
Proof.
repeat intro.
induction τ. {
apply eq_sym.
exact H.
} {
destruct H.
constructor.
intros.
apply E_rel_symmetric'; auto.
apply H.
apply IHτ1.
exact H0.
}
Qed.
Instance E_rel_symmetric {τ} : Symmetric (E_rel τ)
:= E_rel_symmetric' V_rel_symmetric.
Instance A_rel_symmetric {τ} : Symmetric (A_rel τ)
:= A_rel_symmetric' V_rel_symmetric.
Instance G_rel_symmetric {Γ} : Symmetric (G_rel Γ).
Proof.
repeat intro.
induction Γ; dep_destruct (x, y). {
constructor.
} {
dep_destruct H.
constructor; auto.
symmetry.
assumption.
}
Qed.
Instance rel_expr_symmetric {Γ τ} : Symmetric (related_exprs Γ τ).
Proof.
intros e0 e1 He ? ? ?.
symmetry.
apply He.
symmetry.
auto.
Qed.
Instance A_rel_transitive' {τ} :
Transitive (V_rel τ) ->
Transitive (A_rel τ).
Proof.
intros ? x y z Hxy Hyz.
intros v0 v1 Hv.
transitivity (y v0); auto.
apply Hxy.
transitivity v1; [| symmetry]; exact Hv.
Qed.
Instance E_rel_transitive' {τ} :
Transitive (V_rel τ) ->
Transitive (E_rel τ).
Proof.
intros ? x y z Hxy Hyz.
repeat intro.
transitivity (μ y A0); auto.
apply Hxy.
transitivity A1; [| symmetry]; exact HA.
Qed.
Instance V_rel_transitive {τ} :
Transitive (V_rel τ).
Proof.
repeat intro.
induction τ.
{
transitivity y; assumption.
} {
destruct H.
remember (v_lam body1).
destruct H0.
dep_destruct Heqv.
rename body0 into x_body, body1 into y_body, body3 into z_body.
constructor.
intros.
eapply (E_rel_transitive' IHτ2 _); [| apply H0; eauto].
apply H.
eapply IHτ1; eauto.
symmetry.
auto.
}
Qed.
Instance E_rel_transitive {τ} : Transitive (E_rel τ)
:= E_rel_transitive' V_rel_transitive.
Instance A_rel_transitive {τ} : Transitive (A_rel τ)
:= A_rel_transitive' V_rel_transitive.
Instance G_rel_transitive {Γ} : Transitive (G_rel Γ).
Proof.
repeat intro.
induction Γ; dep_destruct (x, y, z). {
constructor.
} {
dep_destruct H.
dep_destruct H1.
constructor. {
etransitivity; eauto.
} {
eapply IHΓ; eauto.
}
}
Qed.
Instance rel_expr_transitive {Γ τ} : Transitive (related_exprs Γ τ).
Proof.
intros x y z Hxy Hyz ? ? ?.
transitivity (proj1_sig (close ρ0 y)). {
apply Hxy.
transitivity ρ1; [| symmetry]; exact Hρ.
} {
apply Hyz.
exact Hρ.
}
Qed.
Instance E_rel_reflexive {τ} : Reflexive (E_rel τ).
Proof.
intro e.
pose proof (fundamental_property e _ _ G_rel_nil).
elim_sig_exprs.
elim_erase_eqs.
auto.
Qed.
Instance V_rel_reflexive {τ} : Reflexive (V_rel τ).
Proof.
intros v.
destruct v using wt_val_rect; subst; simpl in *. {
reflexivity.
} {
constructor.
repeat intro.
pose proof fundamental_property body as fp.
specialize (fp _ _ (G_rel_cons H G_rel_nil)).
elim_sig_exprs.
elim_erase_eqs.
apply fp; auto.
}
Qed.
Lemma A_rel_subidentity {τ} {A0 A1 : Event (val τ)}
: A_rel τ A0 A1 -> A0 = A1.
Proof.
intros.
extensionality v.
apply H.
reflexivity.
Qed.
Instance G_rel_reflexive {Γ} : Reflexive (G_rel Γ).
Proof.
repeat intro.
induction Γ; dep_destruct x. {
constructor.
} {
constructor; auto.
reflexivity.
}
Qed.
Instance rel_expr_reflexive {Γ τ} : Reflexive (related_exprs Γ τ)
:= fundamental_property.
Lemma same_substitution_suffices {Γ τ} (e0 e1 : expr Γ τ) :
(forall (ρ : wt_env Γ),
E_rel τ (proj1_sig (close ρ e0)) (proj1_sig (close ρ e1))) ->
(EXP Γ ⊢ e0 ≈ e1 : τ).
Proof.
intros ? ρ0 ρ1 Hρ.
transitivity (proj1_sig (close ρ0 e1)). {
apply H.
} {
apply fundamental_property; auto.
}
Qed.
Lemma relate_exprs {Γ τ} (e0 e1 : expr Γ τ) :
(forall ρ A, μ (proj1_sig (close ρ e0)) A = μ (proj1_sig (close ρ e1)) A) ->
(EXP Γ ⊢ e0 ≈ e1 : τ).
Proof.
intros.
apply same_substitution_suffices; auto.
repeat intro.
rewrite (A_rel_subidentity HA).
apply H.
Qed.