Skip to content

Commit

Permalink
simplification
Browse files Browse the repository at this point in the history
  • Loading branch information
HuStmpHrrr committed May 4, 2024
1 parent f0ee34a commit 9335bd6
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 25 deletions.
7 changes: 0 additions & 7 deletions theories/Core/Axioms.v
Original file line number Diff line number Diff line change
@@ -1,8 +1 @@
Require Export Coq.Logic.FunctionalExtensionality.

Lemma exists_absorption :
forall (A : Type) (P : A -> Prop) (Q : Prop),
(exists x : A, P x) /\ Q <-> (exists x : A, P x /\ Q).
Proof.
firstorder.
Qed.
20 changes: 2 additions & 18 deletions theories/Core/Semantic/PERLemmas.v
Original file line number Diff line number Diff line change
Expand Up @@ -198,7 +198,7 @@ Proof.
eauto using per_univ_elem_right_irrel.
Qed.

Lemma per_univ_elem_cross_irrel1 : forall i A B R B' R',
Lemma per_univ_elem_cross_irrel : forall i A B R B' R',
per_univ_elem i A B R ->
per_univ_elem i B' A R' ->
R = R'.
Expand All @@ -209,17 +209,6 @@ Proof.
eauto using per_univ_elem_right_irrel.
Qed.

Lemma per_univ_elem_cross_irrel2 : forall i A B R A' R',
per_univ_elem i A B R ->
per_univ_elem i B A' R' ->
R = R'.
Proof.
intros.
apply per_univ_elem_sym in H.
destruct_all.
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 }},
Expand All @@ -235,12 +224,7 @@ Ltac do_per_univ_elem_irrel_rewrite1 :=
| 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_irrel1; eassumption); subst;
try rewrite <- H in *)
| 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_cross_irrel2; eassumption); subst;
(let H := fresh "H" in assert (R1 = R2) as H by (eapply per_univ_elem_cross_irrel; eassumption); subst;
try rewrite <- H in *)
end.

Expand Down

0 comments on commit 9335bd6

Please sign in to comment.