Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Streamline some proofs #54

Merged
merged 1 commit into from
May 6, 2024
Merged

Streamline some proofs #54

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 12 additions & 11 deletions theories/Core/Semantic/EvaluateLemmas.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,14 +64,15 @@ End functional_eval.
#[export]
Hint Resolve functional_eval_exp functional_eval_natrec functional_eval_app functional_eval_sub : mcltt.

Ltac functional_eval_rewrite_clear :=
repeat match goal with
| H1 : {{ ⟦ ~?M ⟧ ~?p ↘ ~?m1 }}, H2 : {{ ⟦ ~?M ⟧ ~?p ↘ ~?m2 }} |- _ =>
assert (m1 = m2) by mauto; subst; clear H2
| H1 : {{ $| ~?m & ~?n |↘ ~?r1 }}, H2 : {{ $| ~?m & ~?n |↘ ~?r2 }} |- _ =>
assert (r1 = r2) by mauto; subst; clear H2
| H1 : {{ rec ~?m ⟦return ~?A | zero -> ~?MZ | succ -> ~?MS end⟧ ~?p ↘ ~?r1 }}, H2 : {{ rec ~?m ⟦return ~?A | zero -> ~?MZ | succ -> ~?MS end⟧ ~?p ↘ ~?r2 }} |- _ =>
assert (r1 = r2) by mauto; subst; clear H2
| H1 : {{ ⟦ ~?σ ⟧s ~?p ↘ ~?p1 }}, H2 : {{ ⟦ ~?σ ⟧s ~?p ↘ ~?p2 }} |- _ =>
assert (p1 = p2) by mauto; subst; clear H2
end.
Ltac functional_eval_rewrite_clear1 :=
match goal with
| H1 : {{ ⟦ ~?M ⟧ ~?p ↘ ~?m1 }}, H2 : {{ ⟦ ~?M ⟧ ~?p ↘ ~?m2 }} |- _ =>
clean replace m2 with m1 by mauto; clear H2
| H1 : {{ $| ~?m & ~?n |↘ ~?r1 }}, H2 : {{ $| ~?m & ~?n |↘ ~?r2 }} |- _ =>
clean replace r2 with r1 by mauto; clear H2
| H1 : {{ rec ~?m ⟦return ~?A | zero -> ~?MZ | succ -> ~?MS end⟧ ~?p ↘ ~?r1 }}, H2 : {{ rec ~?m ⟦return ~?A | zero -> ~?MZ | succ -> ~?MS end⟧ ~?p ↘ ~?r2 }} |- _ =>
clean replace r2 with r1 by mauto; clear H2
| H1 : {{ ⟦ ~?σ ⟧s ~?p ↘ ~?p1 }}, H2 : {{ ⟦ ~?σ ⟧s ~?p ↘ ~?p2 }} |- _ =>
clean replace p2 with p1 by mauto; clear H2
end.
Ltac functional_eval_rewrite_clear := repeat functional_eval_rewrite_clear1.
37 changes: 0 additions & 37 deletions theories/Core/Semantic/PER.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -169,43 +169,6 @@ Section Per_univ_elem_ind_def.

End Per_univ_elem_ind_def.

Lemma rel_mod_eval_ex_pull :
forall (A : Type) (P : domain -> domain -> relation domain -> A -> Prop) {T p T' p'} R,
rel_mod_eval (fun a b R => exists x : A, P a b R x) T p T' p' R <->
exists x : A, rel_mod_eval (fun a b R => P a b R x) T p T' p' R.
Proof.
split; intros.
- destruct H.
destruct H1 as [? ?].
eexists; econstructor; eauto.
- do 2 destruct H; econstructor; eauto.
Qed.

Lemma rel_mod_eval_simp_ex :
forall (A : Type) (P : domain -> domain -> relation domain -> Prop) (Q : domain -> domain -> relation domain -> A -> Prop) {T p T' p'} R,
rel_mod_eval (fun a b R => P a b R /\ exists x : A, Q a b R x) T p T' p' R <->
exists x : A, rel_mod_eval (fun a b R => P a b R /\ Q a b R x) T p T' p' R.
Proof.
split; intros.
- destruct H.
destruct H1 as [? [? ?]].
eexists; econstructor; eauto.
- do 2 destruct H; econstructor; eauto.
firstorder.
Qed.

Lemma rel_mod_eval_simp_and :
forall (P : domain -> domain -> relation domain -> Prop) (Q : relation domain -> Prop) {T p T' p'} R,
rel_mod_eval (fun a b R => P a b R /\ Q R) T p T' p' R <->
rel_mod_eval P T p T' p' R /\ Q R.
Proof.
split; intros.
- destruct H.
destruct H1 as [? ?].
split; try econstructor; eauto.
- do 2 destruct H; econstructor; eauto.
Qed.

Definition rel_typ (i : nat) (A : typ) (p : env) (A' : typ) (p' : env) R' := rel_mod_eval (per_univ_elem i) A p A' p' R'.

Inductive per_ctx_env : ctx -> ctx -> relation env -> Prop :=
Expand Down
142 changes: 87 additions & 55 deletions theories/Core/Semantic/PERLemmas.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,43 @@ From Coq Require Import Lia PeanoNat Relations.Relation_Definitions RelationClas
From Equations Require Import Equations.
From Mcltt Require Import Axioms Base Domain Evaluate EvaluateLemmas LibTactics PER Readback ReadbackLemmas Syntax System.

(* Lemma rel_mod_eval_ex_pull : *)
(* forall (A : Type) (P : domain -> domain -> relation domain -> A -> Prop) {T p T' p'} R, *)
(* rel_mod_eval (fun a b R => exists x : A, P a b R x) T p T' p' R <-> *)
(* exists x : A, rel_mod_eval (fun a b R => P a b R x) T p T' p' R. *)
(* Proof. *)
(* split; intros. *)
(* - destruct H. *)
(* destruct H1 as [? ?]. *)
(* eexists; econstructor; eauto. *)
(* - do 2 destruct H; econstructor; eauto. *)
(* Qed. *)

(* Lemma rel_mod_eval_simp_ex : *)
(* forall (A : Type) (P : domain -> domain -> relation domain -> Prop) (Q : domain -> domain -> relation domain -> A -> Prop) {T p T' p'} R, *)
(* rel_mod_eval (fun a b R => P a b R /\ exists x : A, Q a b R x) T p T' p' R <-> *)
(* exists x : A, rel_mod_eval (fun a b R => P a b R /\ Q a b R x) T p T' p' R. *)
(* Proof. *)
(* split; intros. *)
(* - destruct H. *)
(* destruct H1 as [? [? ?]]. *)
(* eexists; econstructor; eauto. *)
(* - do 2 destruct H; econstructor; eauto. *)
(* firstorder. *)
(* Qed. *)

(* Lemma rel_mod_eval_simp_and : *)
(* forall (P : domain -> domain -> relation domain -> Prop) (Q : relation domain -> Prop) {T p T' p'} R, *)
(* rel_mod_eval (fun a b R => P a b R /\ Q R) T p T' p' R <-> *)
(* rel_mod_eval P T p T' p' R /\ Q R. *)
(* Proof. *)
(* split; intros. *)
(* - destruct H. *)
(* destruct H1 as [? ?]. *)
(* split; try econstructor; eauto. *)
(* - do 2 destruct H; econstructor; eauto. *)
(* Qed. *)

Lemma per_bot_sym : forall m n,
{{ Dom m ≈ n ∈ per_bot }} ->
{{ Dom n ≈ m ∈ per_bot }}.
Expand Down Expand Up @@ -84,6 +121,30 @@ Ltac per_univ_elem_econstructor :=
econstructor;
try rewrite <- per_univ_elem_equation_1 in *.

Ltac destruct_rel_by_assumption in_rel H :=
repeat
match goal with
| H' : {{ Dom ~?c ≈ ~?c' ∈ ?in_rel0 }} |- _ =>
tryif (unify in_rel0 in_rel)
then (destruct (H _ _ H') as []; destruct_all; mark_with H' 1)
else fail
end;
unmark_all_with 1.
Ltac destruct_rel_mod_eval :=
repeat
match goal with
| H : (forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ ?in_rel }}), rel_mod_eval _ _ _ _ _ _) |- _ =>
destruct_rel_by_assumption in_rel H; mark H
end;
unmark_all.
Ltac destruct_rel_mod_app :=
repeat
match goal with
| H : (forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ ?in_rel }}), rel_mod_app _ _ _ _ _) |- _ =>
destruct_rel_by_assumption in_rel H; mark H
end;
unmark_all.

Lemma per_univ_elem_right_irrel_gen : forall i A B R,
per_univ_elem i A B R ->
forall A' B' R',
Expand All @@ -103,10 +164,9 @@ Proof.
extensionality c.
extensionality c'.
extensionality equiv_c_c'.
specialize (H1 _ _ equiv_c_c') as [? ? ? ? []].
specialize (H9 _ _ equiv_c_c') as [? ? ? ? ?].
destruct_rel_mod_eval.
functional_eval_rewrite_clear.
specialize (H5 _ _ _ eq_refl H9).
specialize (H12 _ _ _ eq_refl H5).
congruence.
Qed.

Expand All @@ -118,21 +178,12 @@ Proof.
intros. eauto using per_univ_elem_right_irrel_gen.
Qed.

Ltac per_univ_elem_right_irrel_rewrite :=
repeat match goal with
| H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A ≈ ~?B' ∈ per_univ_elem ?i ↘ ?R1 }} |- _ =>
mark H2
| H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A ≈ ~?B' ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
assert (R2 = R1) by (eapply per_univ_elem_right_irrel; eassumption); subst; mark H2
end; unmark_all.

Ltac functional_per_univ_elem_rewrite_clear :=
repeat match goal with
| H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }} |- _ =>
clear H2
| H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
assert (R2 = R1) by (eapply per_univ_elem_right_irrel; eassumption); subst; clear H2
end.
Ltac per_univ_elem_right_irrel_rewrite1 :=
match goal with
| H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A ≈ ~?B' ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
clean replace R2 with R1 by (eauto using per_univ_elem_right_irrel)
end.
Ltac per_univ_elem_right_irrel_rewrite := repeat per_univ_elem_right_irrel_rewrite1.

Lemma per_univ_elem_sym : forall i A B R,
per_univ_elem i A B R ->
Expand All @@ -141,7 +192,7 @@ Proof.
intros. induction H using per_univ_elem_ind; subst.
- split.
+ apply per_univ_elem_core_univ'; trivial.
+ intros. split; intros HD; destruct HD.
+ intros. split; intros [].
* specialize (H1 _ _ _ H0).
firstorder.
* specialize (H1 _ _ _ H0).
Expand All @@ -156,28 +207,24 @@ Proof.
intros.
assert (equiv_c'_c : in_rel c' c) by firstorder.
assert (equiv_c_c : in_rel c c) by (etransitivity; eassumption).
destruct (H1 _ _ equiv_c_c') as [? ? ? ? [? [? ?]]].
destruct (H1 _ _ equiv_c'_c) as [? ? ? ? [? [? ?]]].
destruct (H1 _ _ equiv_c_c) as [? ? ? ? [? [? ?]]].
destruct_rel_mod_eval.
econstructor; eauto.
functional_eval_rewrite_clear.
per_univ_elem_right_irrel_rewrite.
congruence.
assumption.

+ assert (forall a b : domain,
(forall (c c' : domain) (equiv_c_c' : in_rel c c'), rel_mod_app (out_rel c c' equiv_c_c') a c b c') ->
(forall (c c' : domain) (equiv_c_c' : in_rel c c'), rel_mod_app (out_rel c c' equiv_c_c') b c a c')). {
(forall (c c' : domain) (equiv_c_c' : in_rel c c'), rel_mod_app (out_rel c c' equiv_c_c') b c a c')).
{
intros.
assert (equiv_c'_c : in_rel c' c) by firstorder.
assert (equiv_c_c : in_rel c c) by (etransitivity; eassumption).
destruct (H1 _ _ equiv_c_c') as [? ? ? ? [? [? ?]]].
destruct (H1 _ _ equiv_c'_c) as [? ? ? ? [? [? ?]]].
destruct (H1 _ _ equiv_c_c) as [? ? ? ? [? [? ?]]].
destruct (H5 _ _ equiv_c'_c) as [? ? ? ? ?].
destruct_rel_mod_eval.
destruct_rel_mod_app.
functional_eval_rewrite_clear.
per_univ_elem_right_irrel_rewrite.
econstructor; eauto.
rewrite H17, H16.
firstorder.
}
firstorder.
Expand All @@ -191,10 +238,7 @@ Lemma per_univ_elem_left_irrel : forall i A B R A' R',
per_univ_elem i A' B R' ->
R = R'.
Proof.
intros.
apply per_univ_elem_sym in H.
apply per_univ_elem_sym in H0.
destruct_all.
intros * []%per_univ_elem_sym []%per_univ_elem_sym.
eauto using per_univ_elem_right_irrel.
Qed.

Expand All @@ -203,29 +247,22 @@ Lemma per_univ_elem_cross_irrel : forall i A B R B' R',
per_univ_elem i B' A R' ->
R = R'.
Proof.
intros.
apply per_univ_elem_sym in H0.
destruct_all.
intros * ? []%per_univ_elem_sym.
eauto using per_univ_elem_right_irrel.
Qed.

Ltac do_per_univ_elem_irrel_rewrite1 :=
match goal with
| H1 : {{ DF ~?A ≈ ~_ ∈ per_univ_elem ?i ↘ ?R1 }},
H2 : {{ DF ~?A ≈ ~_ ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
tryif unify R1 R2 then fail else
(let H := fresh "H" in assert (R1 = R2) as H by (eapply per_univ_elem_right_irrel; eassumption); subst;
try rewrite <- H in *)
clean replace R2 with R1 by (eauto using per_univ_elem_right_irrel)
| H1 : {{ DF ~_ ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }},
H2 : {{ DF ~_ ≈ ~?B ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
tryif unify R1 R2 then fail else
(let H := fresh "H" in assert (R1 = R2) as H by (eapply per_univ_elem_left_irrel; eassumption); subst;
try rewrite <- H in *)
clean replace R2 with R1 by (eauto using per_univ_elem_left_irrel)
| H1 : {{ DF ~?A ≈ ~_ ∈ per_univ_elem ?i ↘ ?R1 }},
H2 : {{ DF ~_ ≈ ~?A ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
tryif unify R1 R2 then fail else
(let H := fresh "H" in assert (R1 = R2) as H by (eapply per_univ_elem_cross_irrel; eassumption); subst;
try rewrite <- H in *)
(* Order matters less here as H1 and H2 cannot be exchanged *)
clean replace R2 with R1 by (symmetry; eauto using per_univ_elem_cross_irrel)
end.

Ltac do_per_univ_elem_irrel_rewrite :=
Expand All @@ -245,32 +282,27 @@ Proof with solve [mauto].
induction 1 using per_univ_elem_ind; intros * HT2;
invert_per_univ_elem HT2; clear HT2.
- split; mauto.
intros.
destruct H0, H2.
intros * [] [].
per_univ_elem_irrel_rewrite.
destruct (H1 _ _ _ H0 _ H2) as [? ?].
econstructor...
- split; try econstructor...
- per_univ_elem_irrel_rewrite.
rename in_rel0 into in_rel.
specialize (IHper_univ_elem _ equiv_a_a') as [? _].
split.
+ per_univ_elem_econstructor; mauto.
intros.
assert (equiv_c_c : in_rel c c) by (etransitivity; [ | symmetry]; eassumption).
specialize (H1 _ _ equiv_c_c) as [? ? ? ? [? ?]].
specialize (H9 _ _ equiv_c_c') as [].
destruct_rel_mod_eval.
per_univ_elem_irrel_rewrite.
firstorder (econstructor; eauto).
+ setoid_rewrite H2.
intros.
assert (equiv_c'_c' : in_rel c' c') by (etransitivity; [symmetry | ]; eassumption).
destruct (H1 _ _ equiv_c_c') as [? ? ? ? [? ?]].
specialize (H1 _ _ equiv_c'_c') as [? ? ? ? [? ?]].
specialize (H9 _ _ equiv_c'_c') as [].
specialize (H3 _ _ equiv_c_c') as [].
specialize (H4 _ _ equiv_c'_c') as [].
destruct_rel_mod_eval.
destruct_rel_mod_app.
per_univ_elem_irrel_rewrite.
firstorder (econstructor; eauto).

- split; try per_univ_elem_econstructor...
Qed.
19 changes: 10 additions & 9 deletions theories/Core/Semantic/ReadbackLemmas.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,12 +49,13 @@ End functional_read.
#[export]
Hint Resolve functional_read_nf functional_read_ne functional_read_typ : mcltt.

Ltac functional_read_rewrite_clear :=
repeat match goal with
| H1 : {{ Rnf ~?m in ?s ↘ ~?M1 }}, H2 : {{ Rnf ~?m in ?s ↘ ~?M2 }} |- _ =>
idtac H1; assert (M1 = M2) by mauto; subst; clear H2
| H1 : {{ Rne ~?m in ?s ↘ ~?M1 }}, H2 : {{ Rne ~?m in ?s ↘ ~?M2 }} |- _ =>
idtac H1; assert (M1 = M2) by mauto; subst; clear H2
| H1 : {{ Rtyp ~?m in ?s ↘ ~?M1 }}, H2 : {{ Rtyp ~?m in ?s ↘ ~?M2 }} |- _ =>
idtac H1; assert (M1 = M2) by mauto; subst; clear H2
end.
Ltac functional_read_rewrite_clear1 :=
match goal with
| H1 : {{ Rnf ~?m in ?s ↘ ~?M1 }}, H2 : {{ Rnf ~?m in ?s ↘ ~?M2 }} |- _ =>
clean replace M2 with M1 by mauto; clear H2
| H1 : {{ Rne ~?m in ?s ↘ ~?M1 }}, H2 : {{ Rne ~?m in ?s ↘ ~?M2 }} |- _ =>
clean replace M2 with M1 by mauto; clear H2
| H1 : {{ Rtyp ~?m in ?s ↘ ~?M1 }}, H2 : {{ Rtyp ~?m in ?s ↘ ~?M2 }} |- _ =>
clean replace M2 with M1 by mauto; clear H2
end.
Ltac functional_read_rewrite_clear := repeat functional_read_rewrite_clear1.
Loading
Loading